summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Custom syntax support for structures in LeanJonathan Protzenko2-20/+45
2023-06-04More cosmetic improvementsJonathan Protzenko1-12/+20
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko2-26/+47
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko3-38/+49
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko1-1/+1
2023-06-04Facilitate development by having a local Makefile invoke duneJonathan Protzenko2-0/+4
2023-06-04Initial Lean backend, WIPJonathan Protzenko7-118/+240
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-2/+3
2023-02-03Improve the pretty names generation for loopsSon Ho4-16/+59
2023-02-03Add a commentSon Ho1-0/+33
2023-02-03Split InterpreterLoops into several filesSon Ho12-4098/+4329
2023-02-03Implement a pass to filter the unused input arguments in the loop functionsSon Ho7-48/+377
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho3-12/+37
2023-02-03Improve the order of the loop input parametersSon Ho2-2/+41
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho5-5/+64
2023-02-03Add a comment for PrePasses.remove_shallow_borrowsSon Ho1-2/+87
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho2-0/+10
2023-02-03Fix a minor issueSon Ho1-1/+6
2023-02-03Implement a pass to filter shallow borrowsSon Ho3-7/+85
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho10-40/+291
2023-02-03Fix the comments for ocamldocSon Ho8-10/+11
2023-02-03Fix an issue with the translation of loops::clearSon Ho3-28/+72
2023-02-03Fix an issue in translate_forward_endSon Ho2-1/+3
2023-02-03Fix a minor issue in decompose_let_bindingsSon Ho5-4/+17
2023-02-03Add more loop examples and fix issuesSon Ho12-250/+594
2023-02-03Cleanup a bitSon Ho1-59/+18
2023-02-03Implement support for nested borrows in loops, and add loop testsSon Ho10-151/+999
2023-02-03Make minor modifications to improve the quality of the loop translationSon Ho4-15/+106
2023-02-03Make minor fixesSon Ho1-12/+14
2023-02-03Improve the loops' numberingSon Ho1-132/+149
2023-02-03Make another loop example workSon Ho1-30/+27
2023-02-03Implement a micro-pass to simplify the let-bindings followed by a returnSon Ho4-2/+101
2023-02-03Make a minor cleanup in InterpreterLoops.mlSon Ho1-55/+62
2023-02-03Make minor modifications and generate code for loopsSon Ho1-24/+28
2023-02-03Fix a minor bug in Interpreter.mlSon Ho2-9/+15
2023-02-03Fix various issues with the generation of code for the loopsSon Ho8-149/+416
2023-02-03Fix a small issue with SymbolicToPure.translate_loopSon Ho2-50/+43
2023-02-03Fix a minor issue with [translate_end_abstraction_loop]Son Ho1-3/+7
2023-02-03Fix another bugSon Ho7-39/+127
2023-02-03Fix some bugsSon Ho8-85/+175
2023-02-03Make good progress on updating SymbolicToPureSon Ho14-312/+877
2023-02-03Add a `Loop` node in the pure ASTSon Ho10-15/+97
2023-02-03Introduce new loop ids in Pure and keep track of the number of loops in a fun...Son Ho7-37/+69
2023-02-03Add loop ids to the pure functions identifiersSon Ho8-37/+80
2023-02-03Compute the SCCs of the functions to extract in Translate.mlSon Ho6-125/+183
2023-02-03Reorganize Translate.mlSon Ho1-165/+183
2023-02-03Implement ReorderDecls.mlSon Ho3-1/+152
2023-02-03Add an SCC.ml file for strongly connected componentsSon Ho5-3/+236
2023-02-03Make progress on Interpreter.mlSon Ho12-129/+293
2023-02-03Merge loop abs so that there is one abs per function input region groupSon Ho5-54/+387
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:18:26 +0000