| Commit message (Expand) | Author | Age | Files | Lines |
* | Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...decl | Son Ho | 2022-03-03 | 1 | -43/+43 |
* | Update the way function names are handled | Son Ho | 2022-02-24 | 1 | -2/+4 |
* | Start working on generating code which uses a state-error monad | Son Ho | 2022-02-23 | 1 | -6/+0 |
* | Add an option to control the translation to error monad or state-error | Son Ho | 2022-02-23 | 1 | -1/+7 |
* | Print the generated file headers with Printf rather than the formatter | Son Ho | 2022-02-10 | 1 | -32/+19 |
* | Cleanup a bit | Son Ho | 2022-02-09 | 1 | -21/+23 |
* | Make a minor modification | Son Ho | 2022-02-09 | 1 | -1/+1 |
* | Implement extration to different files | Son Ho | 2022-02-09 | 1 | -41/+121 |
* | Implement generation of template decrease clauses | Son Ho | 2022-02-09 | 1 | -0/+9 |
* | Implement the generation of `decreases` clauses in the definition | Son Ho | 2022-02-09 | 1 | -7/+19 |
* | Start implementing selection of the extracted definitions | Son Ho | 2022-02-09 | 1 | -37/+49 |
* | Add more command line arguments for the decrease clauses | Son Ho | 2022-02-09 | 1 | -0/+10 |
* | Start working on making the extraction more modular in order to generate | Son Ho | 2022-02-09 | 1 | -85/+120 |
* | Add logging information | Son Ho | 2022-02-09 | 1 | -4/+9 |
* | Start working on the generation of decrease clauses | Son Ho | 2022-02-09 | 1 | -1/+16 |
* | Introduce a translation config in Translate.ml | Son Ho | 2022-02-09 | 1 | -14/+19 |
* | Make minor improvements to the generated files | Son Ho | 2022-02-09 | 1 | -2/+5 |
* | Improve a bit the quality of the generated code by adjusting the | Son Ho | 2022-02-09 | 1 | -2/+2 |
* | Make minor modifications | Son Ho | 2022-02-09 | 1 | -1/+1 |
* | Implement filtering of useless forward functions | Son Ho | 2022-02-09 | 1 | -13/+29 |
* | Add a check to detect if forward/backward translations are mutually | Son Ho | 2022-02-09 | 1 | -1/+10 |
* | Add definitions to Primitives.fst and start on improving/fixing the | Son Ho | 2022-02-09 | 1 | -2/+2 |
* | Add type checking utilities for the pure ADT | Son Ho | 2022-02-08 | 1 | -2/+12 |
* | 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 |