summaryrefslogtreecommitdiff
path: root/src/PureMicroPasses.ml (unfollow)
Commit message (Expand)AuthorFilesLines
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
2022-02-03Fix a small issue with the unit typeSon Ho1-1/+3
2022-02-03Implement a micro pass to filter the box functionsSon Ho1-0/+55
2022-02-03Cleanup a bitSon Ho1-3/+4
2022-01-28Implement unfold_monadic_let_bindingsSon Ho1-28/+24
2022-01-28Make the pure expressions typedSon Ho1-49/+60
2022-01-28Make minor modificationsSon Ho1-16/+25
2022-01-28Make the scrutinee in Pure.Switch an expression rather than a valueSon Ho1-7/+7
2022-01-28Make minor modificationsSon Ho1-9/+23
2022-01-28Make administrative modificationsSon Ho1-10/+50
2022-01-28Make minor modificationsSon Ho1-12/+3
2022-01-28Finish implementing filter_unused_assignmentsSon Ho1-6/+118
2022-01-28Make more progress on filter_unused_assignmentsSon Ho1-4/+21
2022-01-28Make good progress on PureMicroPasses.filter_unused_assignmentsSon Ho1-7/+84
2022-01-28Make minor modifications to the use of reduce inSon Ho1-9/+42
2022-01-28Cleanup a bitSon Ho1-6/+10
2022-01-28Implement inline_useless_var_reassignmentsSon Ho1-6/+60
2022-01-28Implement the unit_vars_to_unit passSon Ho1-3/+23
2022-01-28Move some definitions to a new PureUtils.ml fileSon Ho1-7/+6
2022-01-28Finish implementing to_monadicSon Ho1-13/+41
2022-01-28Add a commentSon Ho1-0/+1
2022-01-28Implement get_expression_min_var_counterSon Ho1-3/+16
2022-01-28Start working on to_monadic and make the expression visitors anSon Ho1-7/+45
2022-01-28Remove the Return and Fail variants from Pure.expression and add aSon Ho1-10/+10
2022-01-28Change the type of [Pure.call.args] to [expression list] rather thanSon Ho1-8/+5
2022-01-28Make minor modificationsSon Ho1-1/+8
2022-01-28Simplify the let-bindings in the pure ASTSon Ho1-18/+23
2022-01-28Make substantial simplifications to the pure ASTSon Ho1-76/+54