| Commit message (Expand) | Author | Age | Files | Lines |
* | Improve the command line arguments | Son Ho | 2022-02-04 | 1 | -6/+5 |
* | Make the micro passes config a parameter of Translate.translate_module | Son Ho | 2022-02-04 | 1 | -11/+8 |
* | Add generation of unit tests for the synthesized functions | Son Ho | 2022-02-04 | 1 | -24/+33 |
* | Remove the `open FStar.Mul` line from the generated files | Son Ho | 2022-02-04 | 1 | -2/+0 |
* | Update SymbolicToPure so that we don't construct tuples with exactly one | Son Ho | 2022-02-04 | 1 | -1/+1 |
* | Make minor modifications | Son Ho | 2022-02-03 | 1 | -0/+2 |
* | Implement ExtractToFStar.extract_typed_rvalue | Son Ho | 2022-02-03 | 1 | -1/+1 |
* | Make more progress on implementing function extraction | Son Ho | 2022-02-03 | 1 | -1/+1 |
* | Implement detection of non-recursive forward/backward functions groups when | Son Ho | 2022-02-02 | 1 | -9/+20 |
* | Start working on function extraction | Son Ho | 2022-02-02 | 1 | -6/+30 |
* | Make minor modifications to extract mutually recursive types | Son Ho | 2022-02-02 | 1 | -5/+19 |
* | Improve formatting even more | Son Ho | 2022-02-02 | 1 | -0/+3 |
* | Make minor improvements | Son Ho | 2022-02-02 | 1 | -0/+4 |
* | Fix more issues when extracting types to F* | Son Ho | 2022-02-02 | 1 | -1/+2 |
* | Start working on fixing the extraction of type definitions | Son Ho | 2022-02-02 | 1 | -6/+18 |
* | Start generating code for type definitions | Son Ho | 2022-02-02 | 1 | -2/+84 |
* | Make progress on PureToExtract | Son Ho | 2022-01-29 | 1 | -3/+1 |
* | Make administrative modifications | Son Ho | 2022-01-28 | 1 | -4/+11 |
* | Move some definitions to a new PureUtils.ml file | Son Ho | 2022-01-28 | 1 | -1/+2 |
* | Remove the Return and Fail variants from Pure.expression and add a | Son Ho | 2022-01-28 | 1 | -2/+20 |
* | Apply the micro-passes to the pure ASTs | Son Ho | 2022-01-28 | 1 | -11/+14 |
* | Make a lot of small modifications | Son Ho | 2022-01-28 | 1 | -35/+7 |
* | Make a minor cleaning | Son Ho | 2022-01-28 | 1 | -8/+0 |
* | Fix some issues with the naming of input variables | Son Ho | 2022-01-27 | 1 | -15/+15 |
* | Make minor modifications and create PureMicroPasses.ml | Son Ho | 2022-01-27 | 1 | -0/+1 |
* | Add name information upon initializing some variables in SymbolicToPure | Son Ho | 2022-01-27 | 1 | -7/+42 |
* | Add more printing facilities and fix minor bugs | Son Ho | 2022-01-27 | 1 | -0/+22 |
* | Add some printing facilities to SymbolicToPure | Son Ho | 2022-01-27 | 1 | -2/+3 |
* | Fix a mistake with the input symbolic values not being linked to the | Son Ho | 2022-01-27 | 1 | -10/+29 |
* | Make minor modifications and add comments | Son Ho | 2022-01-27 | 1 | -5/+12 |
* | Cleanup a bit by removing useless `open` | Son Ho | 2022-01-27 | 1 | -2/+0 |
* | Change the signatures of several functions in Interpreter.ml | Son Ho | 2022-01-27 | 1 | -14/+9 |
* | Implement Translate.translate_module_to_pure | Son Ho | 2022-01-27 | 1 | -5/+17 |
* | Implement Translate.translate_function | Son Ho | 2022-01-27 | 1 | -13/+145 |
* | Start working on Translate | Son Ho | 2022-01-27 | 1 | -33/+24 |
* | Make progress on translation | Son Ho | 2022-01-26 | 1 | -8/+18 |
* | Make progress on translation | Son Ho | 2022-01-26 | 1 | -0/+46 |