summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-11-07Replace all the occurrences of `failwith ...` with `raise (Failure ...)`Son Ho1-1/+1
2022-10-28Take care of some TODOsSon Ho1-1/+1
2022-10-28Move some files to the Charon projectSon Ho1-13/+13
2022-10-27Fix some comment referencesSon Ho1-1/+1
2022-10-27Reorganize a bit the projectSon Ho1-0/+0
2022-10-26Update the code documentation to fix links and syntax issuesSon Ho1-147/+147
2022-09-22Update PureMicroPasses.inline_useless_var_reassignmentsSon Ho1-34/+33
2022-06-30Traduct globals body separately (WIP)Sidney Congard1-1/+4
2022-05-15Add a pass to cleanup the deconstructed ADTs and fix a small issueSon Ho1-11/+106
2022-05-04Make progress updating the codeSon Ho1-165/+26
2022-05-01Do more cleanupSon Ho1-9/+10
2022-05-01CleanupSon Ho1-24/+19
2022-05-01Rename "lvalue" to "pattern"Son Ho1-37/+37
2022-04-29Make progress on PureMicroPassesSon Ho1-168/+118
2022-04-29Merge the rvalues with the expressionsSon Ho1-1/+1
2022-04-27Make minor modificationsSon Ho1-3/+39
2022-04-27Fix various bugs when extracting with a state monadSon Ho1-19/+59
2022-04-27Fix the filtering of useless backward functionsSon Ho1-1/+6
2022-04-27Make more progressSon Ho1-12/+40
2022-04-26Make progress on the updatesSon Ho1-54/+11
2022-04-26Introduce the Abs expression and continue updating the codeSon Ho1-150/+73
2022-04-26Introduce the App expression, and make progress updating the codeSon Ho1-50/+51
2022-04-21Cleanup and update commentsSon Ho1-29/+44
2022-04-21Improve the generation of names for given back valuesSon Ho1-33/+156
2022-04-21Work on pretty namesSon Ho1-15/+79
2022-04-20Introduce mdplace to link meta information about the given back valuesSon Ho1-6/+10
2022-04-20Improve the generation of pretty names by correctly using theSon Ho1-1/+5
2022-03-04Fix a small issue with PureMicroPasses.get_body_min_var_counterSon Ho1-7/+20
2022-03-03In fun_id rename the variant Local to RegularSon Ho1-2/+2
2022-03-03Make good progress on adding support for external and opaqueSon Ho1-207/+267
2022-03-03Rename CFIM to LLBCSon Ho1-2/+2
2022-03-03Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho1-23/+23
2022-02-24Update the way function names are handledSon Ho1-1/+1
2022-02-24Finish writing the code which generates the state-error monadSon Ho1-0/+25
2022-02-23Start working on generating code which uses a state-error monadSon Ho1-25/+129
2022-02-23Make a minor modificationSon Ho1-2/+3
2022-02-23Inline more let-bindings and improve formattingSon Ho1-1/+14
2022-02-23Improve the code generation by inlining more let-bindingsSon Ho1-38/+91
2022-02-09Add a commentSon Ho1-1/+2
2022-02-09Make minor modifications and cleanupSon Ho1-3/+6
2022-02-09Implement the generation of `decreases` clauses in the definitionSon Ho1-2/+6
2022-02-09Make minor modificationsSon Ho1-9/+9
2022-02-09Implement filtering of useless forward functionsSon Ho1-6/+68
2022-02-09Update a commentSon Ho1-1/+3
2022-02-09Add definitions to Primitives.fst and start on improving/fixing theSon Ho1-6/+7
2022-02-08Make progress on implementing support for types and functions likeSon Ho1-1/+5
2022-02-04Work on decomposition of monadic let-bindings for F*Son Ho1-1/+86
2022-02-04Merge the switches over integers and the matches over enumerations inSon Ho1-19/+0
2022-02-04Update SymbolicToPure so that we don't construct tuples with exactly oneSon Ho1-1/+1
2022-02-04Filter the backward functions with no outputs in the micro passesSon Ho1-46/+66
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 14:31:45 +0000