summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-20/+22
2023-10-20Start updating to handle function pointersSon Ho1-16/+16
2023-10-13Add supSon Ho1-1/+1
2023-09-17Merge trans_ctx and decls_ctxSon Ho1-7/+4
2023-09-11Make progress on correctly handling trait method calls in the symbolic executionSon Ho1-14/+15
2023-09-03Add the keep_fwd field in TranslateCore.pure_fun_translationSon Ho1-15/+13
2023-09-03Update TranslateCore.pure_fun_translationSon Ho1-10/+10
2023-09-03Update the type TranslateCore.fun_and_loopsSon Ho1-8/+9
2023-09-03Make progress on the extractionSon Ho1-2/+6
2023-09-01Update PureMicroPassesSon Ho1-43/+18
2023-08-18Add tests which use const generics as valuesSon Ho1-2/+2
2023-08-18Update following the introduction of ConstantExprSon Ho1-4/+3
2023-08-07Change some fun id names to use "Mut"/"Shared" as a suffixSon Ho1-4/+4
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho1-1/+2
2023-08-03Fix an issue with the extraction of aggregated arraysSon Ho1-3/+3
2023-08-02Make progressSon Ho1-9/+37
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho1-2/+41
2023-06-04Start updating simplify_aggregatesSon Ho1-2/+43
2023-06-04Add a special expression for structure creation/updateSon Ho1-1/+109
2023-02-03Improve the pretty names generation for loopsSon Ho1-0/+2
2023-02-03Implement a pass to filter the unused input arguments in the loop functionsSon Ho1-14/+328
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho1-0/+13
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho1-0/+8
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho1-3/+26
2023-02-03Fix a minor issue in decompose_let_bindingsSon Ho1-2/+3
2023-02-03Improve the loops' numberingSon Ho1-132/+149
2023-02-03Implement a micro-pass to simplify the let-bindings followed by a returnSon Ho1-0/+63
2023-02-03Fix a minor bug in Interpreter.mlSon Ho1-1/+4
2023-02-03Fix various issues with the generation of code for the loopsSon Ho1-96/+287
2023-02-03Add a `Loop` node in the pure ASTSon Ho1-0/+18
2023-02-03Introduce new loop ids in Pure and keep track of the number of loops in a fun...Son Ho1-1/+1
2023-02-03Add loop ids to the pure functions identifiersSon Ho1-7/+8
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho1-4/+17
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-30/+140
2022-11-14Make good progress on the Coq backendSon Ho1-0/+1
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-1/+1
2022-11-11Fix some issues with the commentsSon Ho1-1/+1
2022-11-10Implement a Config.ml file which groups all the global options in referencesSon Ho1-74/+15
2022-11-10Update the way function names are handled in PureSon Ho1-16/+17
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