| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Fix a last issue | Son Ho | 2024-03-08 | 2 | -51/+110 |
* | Fix an issue with the loops | Son Ho | 2024-03-08 | 1 | -1/+7 |
* | Make progress on fixing the loops | Son Ho | 2024-03-08 | 8 | -31/+70 |
* | Fix a small issue with the loops | Son Ho | 2024-03-08 | 2 | -7/+19 |
* | Fix some issues with the loops | Son Ho | 2024-03-08 | 3 | -140/+206 |
* | Do not fail in end_abstraction_aux if the abs disappeared | Son Ho | 2024-03-08 | 2 | -64/+80 |
* | Add logging information | Son Ho | 2024-03-08 | 3 | -0/+24 |
* | Update Print.ml | Son Ho | 2024-03-08 | 1 | -8/+8 |
* | Make progress on propagating the changes | Son Ho | 2024-03-08 | 14 | -949/+259 |
* | Remove the option to split fwd/back functions and update SymbolicToPure | Son Ho | 2024-03-08 | 5 | -776/+439 |
* | Update the code generated for tuple projectors | Son Ho | 2024-03-08 | 3 | -18/+47 |
* | Fix tuple indexing for Lean backend | Zyad Hassan | 2024-03-08 | 1 | -4/+33 |
* | Update the generation of constant bodies for Lean | Son Ho | 2024-03-08 | 1 | -2/+1 |
* | Update the code generation | Son Ho | 2024-03-08 | 2 | -7/+6 |
* | Start fixing the tests | Son Ho | 2024-02-02 | 1 | -1/+1 |
* | Make a minor modification | Son Ho | 2024-01-25 | 1 | -2/+2 |
* | Fix a minor issue when values are moved in the loops | Son Ho | 2024-01-25 | 6 | -188/+478 |
* | Fix an issue when deconstructing tuples in Coq | Son Ho | 2023-12-23 | 2 | -5/+8 |
* | Update the micro-passes | Son Ho | 2023-12-23 | 1 | -77/+94 |
* | Improve the micro passes to eliminate pattern `let f := fun x => g x` | Son Ho | 2023-12-23 | 1 | -2/+43 |
* | Fix minor issues | Son Ho | 2023-12-22 | 3 | -37/+103 |
* | Update the computation of the effect info for the loops | Son Ho | 2023-12-22 | 1 | -46/+95 |
* | Fix the output type of the loops backward functions | Son Ho | 2023-12-22 | 5 | -46/+65 |
* | Fix a minor issue with the extraction of loops when merging the fwd/back func... | Son Ho | 2023-12-22 | 1 | -11/+19 |
* | Annotate the bound vars in the lambdas for Coq | Son Ho | 2023-12-22 | 1 | -20/+36 |
* | Fix a minor extraction issue | Son Ho | 2023-12-22 | 1 | -1/+1 |
* | Add an option to split the fwd/back functions and fix a minor issue | Son Ho | 2023-12-22 | 2 | -7/+15 |
* | Update the library for F* | Son Ho | 2023-12-22 | 2 | -1/+15 |
* | Slightly update the formatting of the do blocks | Son Ho | 2023-12-22 | 1 | -24/+26 |
* | Fix an issue when merging the fwd/back functions of trait methods | Son Ho | 2023-12-22 | 4 | -19/+57 |
* | Improve the pure micro passes | Son Ho | 2023-12-21 | 2 | -3/+46 |
* | Fix issues when extracting stateful functions | Son Ho | 2023-12-21 | 2 | -41/+40 |
* | Fix several issues | Son Ho | 2023-12-21 | 3 | -81/+151 |
* | Improve PureMicroPasses.filter_useless to simplify the matches | Son Ho | 2023-12-21 | 1 | -1/+14 |
* | Use indices starting at 1 to make variable names unique at code gen | Son Ho | 2023-12-21 | 1 | -1/+1 |
* | Implement a micro-pass to simplify the let-bindings | Son Ho | 2023-12-21 | 1 | -0/+78 |
* | Simplify the type of the merged fwd/back functions | Son Ho | 2023-12-21 | 5 | -46/+153 |
* | Update the formatting of comments | Son Ho | 2023-12-21 | 1 | -8/+6 |
* | Filter the useless backward functions | Son Ho | 2023-12-21 | 1 | -75/+145 |
* | Update SymbolicToPure.ml for the loops | Son Ho | 2023-12-21 | 1 | -96/+125 |
* | Remove some asserts which are now useless | Son Ho | 2023-12-21 | 3 | -8/+4 |
* | Fix some issues in SymbolicToPure | Son Ho | 2023-12-21 | 1 | -25/+26 |
* | Fix a minor issue | Son Ho | 2023-12-21 | 1 | -2/+5 |
* | Make good progress on merging the fwd/back functions | Son Ho | 2023-12-21 | 8 | -87/+274 |
* | Reset Config.return_back_funs to false | Son Ho | 2023-12-19 | 1 | -1/+1 |
* | Remove SymbolicToPure.bs_ctx.loop_backward_outputs | Son Ho | 2023-12-19 | 2 | -33/+15 |
* | Simplify SymbolicToPure.bs_ctx.{backward_outputs, loop_backward_outputs} | Son Ho | 2023-12-19 | 2 | -100/+70 |
* | Remove the backwards field from SymbolicToPure.call_info | Son Ho | 2023-12-18 | 1 | -15/+5 |
* | Fix a minor mistake in SymbolicToPure | Son Ho | 2023-12-18 | 3 | -11/+15 |
* | Add some comments | Son Ho | 2023-12-18 | 1 | -16/+31 |