summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Make good progress on generating code for HOL4Son Ho1-2/+20
2023-06-04Improve the generation of variant names for LeanSon Ho1-0/+7
2023-06-04Handle the "opaque_defs." prefix in a cleaner mannerSon Ho1-62/+160
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho1-23/+40
2023-06-04Make minor fixes, improve formatting for Lean and generate code for all the t...Son Ho1-10/+8
2023-06-04All of the generated code is syntactically correctJonathan Protzenko1-4/+14
2023-06-04WIPJonathan Protzenko1-1/+3
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko1-0/+46
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko1-17/+17
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-1/+1
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-1/+1
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho1-9/+23
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho1-4/+6
2023-02-03Fix various issues with the generation of code for the loopsSon Ho1-8/+13
2023-02-03Introduce new loop ids in Pure and keep track of the number of loops in a fun...Son Ho1-25/+46
2023-02-03Add loop ids to the pure functions identifiersSon Ho1-9/+18
2022-11-14Add a `-use-fuel` optionSon Ho1-8/+8
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho1-2/+7
2022-11-14Make good progress on the Coq backendSon Ho1-5/+82
2022-11-10Update the way function names are handled in PureSon Ho1-48/+49
2022-11-10Reorganize branching symbolic expansions to prepare for the join operationSon Ho1-3/+13
2022-11-07Replace all the occurrences of `failwith ...` with `raise (Failure ...)`Son Ho1-13/+13
2022-10-27Move constant_value to PrimitiveValues.mlSon 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-46/+50
2022-09-22Update the name registration for globalsSon Ho1-3/+4
2022-09-22Make minor cleanupSon Ho1-19/+7
2022-08-11Correct last PR remarksSidney Congard1-7/+9
2022-07-29Create global declaration group, address PR changes but introduce bugsSidney Congard1-8/+24
2022-07-25Apply minor changes from PR commentsSidney Congard1-2/+2
2022-07-18Address much stuff of the PR, throw exceptions at remaining placesSidney Congard1-3/+4
2022-06-30Traduct globals body separately (WIP)Sidney Congard1-5/+13
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-7/+6
2022-06-08read globals from LLBC JSON into functionsSidney Congard1-0/+1
2022-04-26Introduce the App expression, and make progress updating the codeSon Ho1-2/+2
2022-03-03In fun_id rename the variant Local to RegularSon Ho1-6/+6
2022-03-03Rename CFIM to LLBCSon Ho1-2/+2
2022-03-03Add an Opaque variant to type_decl_kind and start updating the codeSon Ho1-2/+2
2022-03-03Move the names from Identifiers to NamesSon Ho1-9/+13
2022-03-03Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho1-22/+22
2022-02-24Update the way function names are handledSon Ho1-5/+15
2022-02-23Add the `State` assumed type in Pure.mlSon Ho1-1/+2
2022-02-23Add a commentSon Ho1-1/+18
2022-02-09Add a commentSon Ho1-0/+1
2022-02-09Cleanup a bitSon Ho1-10/+10
2022-02-09Implement the generation of `decreases` clauses in the definitionSon Ho1-0/+4
2022-02-09Start working on the generation of decrease clausesSon Ho1-0/+31
2022-02-09Improve a bit the quality of the generated code by adjusting theSon Ho1-38/+25
2022-02-08Fix some issuesSon Ho1-79/+91
2022-02-08Make progress on implementing support for types and functions likeSon Ho1-1/+9
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 15:33:32 +0000