| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Implement a micro-pass to simplify the let-bindings followed by a return | Son Ho | 2023-02-03 | 4 | -2/+101 |
* | Make a minor cleanup in InterpreterLoops.ml | Son Ho | 2023-02-03 | 1 | -55/+62 |
* | Make minor modifications and generate code for loops | Son Ho | 2023-02-03 | 9 | -26/+213 |
* | Fix a minor bug in Interpreter.ml | Son Ho | 2023-02-03 | 2 | -9/+15 |
* | Fix various issues with the generation of code for the loops | Son Ho | 2023-02-03 | 8 | -149/+416 |
* | Fix a small issue with SymbolicToPure.translate_loop | Son Ho | 2023-02-03 | 2 | -50/+43 |
* | Fix a minor issue with [translate_end_abstraction_loop] | Son Ho | 2023-02-03 | 1 | -3/+7 |
* | Fix another bug | Son Ho | 2023-02-03 | 7 | -39/+127 |
* | Fix some bugs | Son Ho | 2023-02-03 | 8 | -85/+175 |
* | Make good progress on updating SymbolicToPure | Son Ho | 2023-02-03 | 14 | -312/+877 |
* | Add a `Loop` node in the pure AST | Son Ho | 2023-02-03 | 10 | -15/+97 |
* | Introduce new loop ids in Pure and keep track of the number of loops in a fun... | Son Ho | 2023-02-03 | 7 | -37/+69 |
* | Add loop ids to the pure functions identifiers | Son Ho | 2023-02-03 | 8 | -37/+80 |
* | Compute the SCCs of the functions to extract in Translate.ml | Son Ho | 2023-02-03 | 6 | -125/+183 |
* | Reorganize Translate.ml | Son Ho | 2023-02-03 | 1 | -165/+183 |
* | Implement ReorderDecls.ml | Son Ho | 2023-02-03 | 3 | -1/+152 |
* | Add an SCC.ml file for strongly connected components | Son Ho | 2023-02-03 | 5 | -3/+236 |
* | Make progress on Interpreter.ml | Son Ho | 2023-02-03 | 12 | -129/+293 |
* | Merge loop abs so that there is one abs per function input region group | Son Ho | 2023-02-03 | 5 | -54/+387 |
* | Make minor modifications | Son Ho | 2023-02-03 | 3 | -38/+63 |
* | Add detailed explanations in InterpreterLoops.ml | Son Ho | 2023-02-03 | 1 | -39/+405 |
* | Implement [match_ctx_with_target] | Son Ho | 2023-02-03 | 3 | -80/+635 |
* | End some borrows preemptively when computing loop joins | Son Ho | 2023-02-03 | 1 | -3/+14 |
* | Update the comments in Values and make minor modifications | Son Ho | 2023-02-03 | 7 | -120/+213 |
* | Remove the meta-value field from AMutBorrow | Son Ho | 2023-02-03 | 10 | -136/+144 |
* | Update a comment | Son Ho | 2023-02-03 | 1 | -1/+4 |
* | Remove the APrimitive variant from the avalues | Son Ho | 2023-02-03 | 7 | -25/+3 |
* | Remove the meta-values from the shared and reserved borrow values | Son Ho | 2023-02-03 | 15 | -162/+163 |
* | Make more fixes | Son Ho | 2023-02-03 | 2 | -86/+222 |
* | Make some fixes | Son Ho | 2023-02-03 | 5 | -33/+231 |
* | Make progress on checking that two environments are equivalent | Son Ho | 2023-02-03 | 3 | -177/+561 |
* | Improve some visitors and ctx_merge_regions | Son Ho | 2023-02-03 | 4 | -42/+76 |
* | Make minor modifications | Son Ho | 2023-02-03 | 2 | -1/+11 |
* | Improve merge_abstractions | Son Ho | 2023-02-03 | 3 | -6/+91 |
* | Improve the value visitors and some substitution functions | Son Ho | 2023-02-03 | 3 | -23/+54 |
* | Make more progress on the joins | Son Ho | 2023-02-03 | 1 | -142/+127 |
* | Make progress on the fixed point computation | Son Ho | 2023-02-03 | 6 | -400/+381 |
* | Make progress on the environment matches | Son Ho | 2023-02-03 | 8 | -34/+279 |
* | Make more progress | Son Ho | 2023-02-03 | 1 | -61/+102 |
* | Make progress on environment matches and joins | Son Ho | 2023-02-03 | 7 | -240/+1104 |
* | Make progress on environments matches and joins | Son Ho | 2023-02-03 | 5 | -74/+563 |
* | Start implementing support for loops | Son Ho | 2023-02-03 | 20 | -265/+1567 |
* | Add a nix derivation for the Coq proofs | Son Ho | 2022-11-16 | 4 | -7/+25 |
* | Do not introduce match on the fuel for non-recursive functions | Son Ho | 2022-11-16 | 6 | -678/+527 |
* | Automatically generate the Makefile and _CoqProject files in the tests subdir... | Son Ho | 2022-11-16 | 17 | -15/+53 |
* | Add the aeneas-verify-fstar derivation | Son Ho | 2022-11-16 | 8 | -17/+159 |
* | Generate record field projectors for Coq | Son Ho | 2022-11-16 | 13 | -778/+843 |
* | Change the name of the generated Coq modules | Son Ho | 2022-11-16 | 12 | -43/+43 |
* | Improve formatting | Son Ho | 2022-11-16 | 19 | -682/+707 |
* | Remove some comments from Hashmap.Properties.fst | Son Ho | 2022-11-16 | 1 | -60/+0 |