summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Improve the generation of variant names for LeanSon Ho3-15/+33
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho2-3/+48
2023-06-04Start updating simplify_aggregatesSon Ho1-2/+43
2023-06-04Add a special expression for structure creation/updateSon Ho9-182/+451
2023-06-04Don't create useless directories in LeanSon Ho1-2/+4
2023-06-04Update the extraction of Lean filesSon Ho2-25/+51
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho1-1/+1
2023-06-04Remove the symbolic interpreter testsSon Ho2-35/+0
2023-06-04Automate the generation of the lakefile.lean filesSon Ho2-120/+167
2023-06-04Add a check in Driver.mlSon Ho1-0/+12
2023-06-04Handle the "opaque_defs." prefix in a cleaner mannerSon Ho3-95/+253
2023-06-04Make minor modificationsSon Ho1-41/+89
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho5-61/+108
2023-06-04Update the generation of termination and decreases_by templates for LeanSon Ho2-28/+39
2023-06-04Add more checks in Driver.mlSon Ho2-3/+8
2023-06-04Print warnings for the Lean backend and loopsSon Ho1-8/+13
2023-06-04WIPJonathan Protzenko1-3/+6
2023-06-04More commentsJonathan Protzenko1-0/+8
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-2/+7
2023-06-04Improve formatting further by removing useless spacesSon Ho1-15/+22
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho2-43/+55
2023-06-04Improve formatting of the termination_by clausesSon Ho1-2/+8
2023-06-04Make minor fixes, improve formatting for Lean and generate code for all the t...Son Ho3-177/+203
2023-06-04All of the generated code is syntactically correctJonathan Protzenko2-8/+19
2023-06-04WIPJonathan Protzenko3-5/+30
2023-06-04Fix runaway indentationJonathan Protzenko1-4/+4
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko1-10/+15
2023-06-04Don't need extra variables for the decreases clausesJonathan Protzenko1-3/+9
2023-06-04WIP printing proper clausesJonathan Protzenko1-3/+58
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko3-16/+186
2023-06-04WIP lots of stuffJonathan Protzenko3-27/+47
2023-06-04Fix a syntax errorJonathan Protzenko1-2/+6
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:49:59 +0000