summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-02-03Make minor modificationsSon Ho2-1/+11
2023-02-03Improve merge_abstractionsSon Ho3-6/+91
2023-02-03Improve the value visitors and some substitution functionsSon Ho3-23/+54
2023-02-03Make more progress on the joinsSon Ho1-142/+127
2023-02-03Make progress on the fixed point computationSon Ho6-400/+381
2023-02-03Make progress on the environment matchesSon Ho8-34/+279
2023-02-03Make more progressSon Ho1-61/+102
2023-02-03Make progress on environment matches and joinsSon Ho7-240/+1104
2023-02-03Make progress on environments matches and joinsSon Ho5-74/+563
2023-02-03Start implementing support for loopsSon Ho19-264/+1566
2022-11-16Do not introduce match on the fuel for non-recursive functionsSon Ho3-11/+50
2022-11-16Automatically generate the Makefile and _CoqProject files in the tests subdir...Son Ho1-0/+2
2022-11-16Generate record field projectors for CoqSon Ho3-83/+231
2022-11-16Change the name of the generated Coq modulesSon Ho1-1/+1
2022-11-16Improve formattingSon Ho2-99/+120
2022-11-16Make minor modifications to the extractionSon Ho1-4/+13
2022-11-14Extract the Polonius examples in CoqSon Ho1-13/+16
2022-11-14Add a `-use-fuel` optionSon Ho11-53/+272
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho12-29/+107
2022-11-14Improve the formatting of [if then else] expressionsSon Ho1-15/+24
2022-11-14Improve the formatting of the generated codeSon Ho2-33/+56
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho3-53/+172
2022-11-14Make minor modificationsSon Ho3-18/+0
2022-11-14Make good progress on the Coq backendSon Ho14-416/+1058
2022-11-14Reorganize the project to prepare for new backendsSon Ho7-29/+30
2022-11-11Fix some issues with the commentsSon Ho8-22/+19
2022-11-11Make a minor modificationSon Ho1-1/+1
2022-11-11Move the fstar files to the new backends directorySon Ho1-1/+1
2022-11-11Add a `bin` folderSon Ho1-3/+5
2022-11-11Make the Nix build workSon Ho2-290/+4
2022-11-10Factor out the symbolic execution for the forward/backward translationsSon Ho5-92/+77
2022-11-10Make a minor cleanupSon Ho5-46/+43
2022-11-10Implement a Config.ml file which groups all the global options in referencesSon Ho16-492/+388
2022-11-10Implement the generation of stateful backward functions (controlled by an opt...Son Ho10-208/+386
2022-11-10Update the way function names are handled in PureSon Ho8-142/+162
2022-11-10Reorganize branching symbolic expansions to prepare for the join operationSon Ho12-104/+184
2022-11-10Reorganize the symoblic expansions to separate the branching/non-branching onesSon Ho3-72/+95
2022-11-10Update `switch` to have a specific treatment of ADTsSon Ho9-196/+207
2022-11-07Update some commentsSon Ho2-14/+14
2022-11-07Rename "inactivated borrows" to "reserved borrows"Son Ho12-89/+91
2022-11-07Add some .mli filesSon Ho16-381/+642
2022-11-07Update InterpreterBorrowsSon Ho1-70/+35
2022-11-07Add ids to the dummy variablesSon Ho9-93/+139
2022-11-07Remove the argument [end_borrows] from prepare_lplace and drop_outer_loans_at...Son Ho3-52/+24
2022-11-07Deactivate filter_drop_assigns and implement remove_useless_cf_merges in PreP...Son Ho1-4/+107
2022-11-07Replace all the occurrences of `failwith ...` with `raise (Failure ...)`Son Ho17-148/+171
2022-11-07Fix an issue with drop_valueSon Ho2-28/+32
2022-10-28Update aeneas.opamSon Ho1-2/+2
2022-10-28Move the AssignGlobal case from statement to rvalueSon Ho5-40/+46
2022-10-28Make minor modificationsSon Ho4-7/+11
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 17:35:58 +0000