summaryrefslogtreecommitdiff
path: root/src/main.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Introduce a translation config in Translate.mlSon Ho2022-02-091-5/+11
|
* Update the Makefile so as not to generate and check traces anymoreSon Ho2022-02-091-14/+14
|
* Make minor modificationsSon Ho2022-02-091-5/+5
|
* Implement filtering of useless forward functionsSon Ho2022-02-091-0/+5
|
* Add definitions to Primitives.fst and start on improving/fixing theSon Ho2022-02-091-0/+1
| | | | generated F* file
* Fix some mistakes in the type conversion to pureSon Ho2022-02-081-0/+2
|
* Add an option to allow the presence of bottom values below borrowsSon Ho2022-02-081-1/+2
|
* Fix more issuesSon Ho2022-02-081-4/+4
|
* Implement pre-passes to update the AST before executing the interpreterSon Ho2022-02-081-0/+3
|
* Make a minor modifications to Makefile and main.mlSon Ho2022-02-081-2/+2
|
* Fix some issuesSon Ho2022-02-081-1/+1
|
* Make progress on implementing support for types and functions likeSon Ho2022-02-081-2/+11
| | | | Option and Vec
* Improve the command line argumentsSon Ho2022-02-041-21/+57
|
* Work on decomposition of monadic let-bindings for F*Son Ho2022-02-041-1/+2
|
* Make the micro passes config a parameter of Translate.translate_moduleSon Ho2022-02-041-1/+9
|
* Add generation of unit tests for the synthesized functionsSon Ho2022-02-041-1/+2
|
* Make minor modifications with regards to loggingSon Ho2022-02-041-0/+1
|
* Deactivate some logsSon Ho2022-02-041-4/+4
|
* Cleanup a bitSon Ho2022-02-031-3/+0
|
* Start generating code for type definitionsSon Ho2022-02-021-3/+1
|
* Rename ExtractToFstar to ExtractToFStarSon Ho2022-01-291-1/+1
|
* Start working on extraction to F*Son Ho2022-01-291-0/+1
|
* Start working on ExtractAstSon Ho2022-01-281-0/+1
|
* Make a lot of small modificationsSon Ho2022-01-281-0/+1
|
* Move some definitions from SymbolicToPure to PureToExtractSon Ho2022-01-271-1/+1
|
* Add more printing facilities and fix minor bugsSon Ho2022-01-271-1/+3
|
* Make minor modifications and add commentsSon Ho2022-01-271-1/+4
|
* Start testing translation to pureSon Ho2022-01-271-3/+7
|
* Cleanup a bit by removing useless `open`Son Ho2022-01-271-2/+0
|
* Implement Translate.translate_functionSon Ho2022-01-271-0/+1
|
* Implement the borrow_content case of end_abstraction_borrowsSon Ho2022-01-271-1/+1
|
* Fix various issuesSon Ho2022-01-261-2/+2
|
* Test the generation of the symbolic ASTSon Ho2022-01-261-1/+1
|
* Start working on signatures for the assumed functionsSon Ho2022-01-261-1/+1
|
* Fix a typoSon Ho2022-01-261-1/+1
|
* Remove SymbolicAstUtils.mlSon Ho2022-01-261-1/+0
|
* Implement SymbolicToPure.translate_fun_sigSon Ho2022-01-251-1/+2
|
* Start working on name generation for the synthesisSon Ho2022-01-241-0/+1
|
* Start working on printing for symbolic ASTSon Ho2022-01-241-0/+2
|
* Add invariant checks at the end of [end_borrow] and [end_abstraction]Son Ho2022-01-211-1/+1
|
* Start working on Pure.mlSon Ho2022-01-191-0/+1
|
* Start working on TypesAnalysisSon Ho2022-01-181-0/+1
|
* Implement greedy expansion of symbolic variables and expansion beforeSon Ho2022-01-141-1/+2
| | | | copy
* Start working on greedy symbolic value expansion and expansion beforeSon Ho2022-01-141-2/+10
| | | | assignment
* Update end_borrow to check if there are loans in borrowed valuesSon Ho2022-01-121-1/+1
|
* Merge remote-tracking branch 'refs/remotes/origin/main'Jonathan Protzenko2022-01-101-2/+15
|\
| * Make more modifications to loggingSon Ho2022-01-071-2/+5
| |
| * Add logging information for borrowsSon Ho2022-01-071-1/+2
| |
| * Make more improvements to loggingSon Ho2022-01-071-0/+1
| |
| * Improve logging and introduce eval_operands_prepareSon Ho2022-01-071-0/+8
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 14:55:13 +0000