| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | | Fix a minor issue in HOL4 | Son Ho | 2023-09-04 | 1 | -1/+1 |
* | | Fix minor issues | Son Ho | 2023-09-04 | 3 | -4/+16 |
* | | Implement extract_trait_impl | Son Ho | 2023-09-03 | 1 | -6/+160 |
* | | Extract the trait decl methods | Son Ho | 2023-09-03 | 2 | -34/+54 |
* | | Make progress registering the trait decl method names | Son Ho | 2023-09-03 | 2 | -31/+93 |
* | | Do more cleanup | Son Ho | 2023-09-03 | 3 | -9/+9 |
* | | Add the keep_fwd field in TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 4 | -35/+42 |
* | | Update TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 5 | -34/+33 |
* | | Update the type TranslateCore.fun_and_loops | Son Ho | 2023-09-03 | 4 | -34/+35 |
* | | Make progress on extracting trait decls and merge gen_ctx and extraction_ctx | Son Ho | 2023-09-03 | 3 | -98/+219 |
* | | Register the names for the trait decls | Son Ho | 2023-09-03 | 2 | -14/+154 |
* | | Make more progress | Son Ho | 2023-09-03 | 3 | -24/+67 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 3 | -61/+221 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -21/+264 |
* | | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -52/+138 |
* | | Improve the collision detection | Son Ho | 2023-09-03 | 1 | -16/+54 |
* | | Make good progress on Extract.ml | Son Ho | 2023-09-01 | 2 | -224/+237 |
* | | Update PureMicroPasses | Son Ho | 2023-09-01 | 2 | -44/+19 |
* | | Compute the normalized trait types maps and update Interpreter | Son Ho | 2023-09-01 | 6 | -70/+206 |
* | | Implement the normalization functions in AssociatedTypes | Son Ho | 2023-09-01 | 5 | -14/+335 |
* | | Make progress on Extract and ExtractBase | Son Ho | 2023-08-31 | 3 | -52/+132 |
* | | Update TranslateCore and factor out some definitions in PrintPure | Son Ho | 2023-08-31 | 2 | -42/+42 |
* | | Finish updating SymbolicToPure.ml | Son Ho | 2023-08-31 | 4 | -115/+212 |
* | | Start adding support for traits | Son Ho | 2023-08-31 | 31 | -776/+1258 |
* | | Regenerate the array tests | Son Ho | 2023-08-18 | 3 | -0/+25 |
* | | Add tests which use const generics as values | Son Ho | 2023-08-18 | 5 | -2/+17 |
* | | Update following the introduction of ConstantExpr | Son Ho | 2023-08-18 | 16 | -143/+220 |
* | | Make a minor modification | Son Ho | 2023-08-17 | 1 | -11/+0 |
|/ |
|
* | Merge pull request #34 from AeneasVerif/son_update_rustc | Son HO | 2023-08-09 | 18 | -41/+41 |
|\ |
|
| * | Update the nix flake | Son Ho | 2023-08-09 | 1 | -18/+18 |
| * | Update the nix flake and regenerate the code | Son Ho | 2023-08-09 | 18 | -26/+26 |
* | | Merge pull request #33 from AeneasVerif/son_refactor | Son HO | 2023-08-09 | 23 | -1495/+1513 |
|\| |
|
| * | Update the README | Son Ho | 2023-08-09 | 1 | -20/+21 |
| * | Regenerate the test files | Son Ho | 2023-08-08 | 18 | -1463/+1465 |
| * | Update the code following a refactor on Charon's side | Son Ho | 2023-08-08 | 4 | -12/+27 |
|/ |
|
* | Merge pull request #32 from AeneasVerif/son_arrays | Son HO | 2023-08-07 | 110 | -1184/+5804 |
|\ |
|
| * | Update the flake.lock | Son Ho | 2023-08-07 | 1 | -40/+58 |
| * | Regenerate the test files | Son Ho | 2023-08-07 | 6 | -60/+550 |
| * | Change some fun id names to use "Mut"/"Shared" as a suffix | Son Ho | 2023-08-07 | 5 | -66/+66 |
| * | Fix a heart beat issue in a Lean proof | Son Ho | 2023-08-04 | 1 | -0/+4 |
| * | Add an option to not override Hashmap.lean | Son Ho | 2023-08-04 | 4 | -3/+16 |
| * | Generate the array test files for Coq and F* | Son Ho | 2023-08-04 | 12 | -0/+1560 |
| * | Update the Makefile and regenerate the test files | Son Ho | 2023-08-04 | 28 | -63/+637 |
| * | Fix issues with the extraction and extend the primitive libraries for Coq and F* | Son Ho | 2023-08-04 | 5 | -32/+151 |
| * | Add a forgotten file | Son Ho | 2023-08-04 | 1 | -0/+1 |
| * | Generate the Array example in Lean | Son Ho | 2023-08-04 | 2 | -0/+295 |
| * | Make minor modifications | Son Ho | 2023-08-04 | 4 | -9/+9 |
| * | Add SliceLen as a primitive function and make minor adjustments | Son Ho | 2023-08-04 | 6 | -77/+100 |
| * | Add the UtilsBase.lean file | Son Ho | 2023-08-04 | 1 | -0/+10 |
| * | Start adding support for Arrays/Slices in the Lean library | Son Ho | 2023-08-04 | 9 | -49/+692 |