summaryrefslogtreecommitdiff
path: root/compiler/ExtractBase.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-16Add a strict_names_map in the extraction_ctxSon Ho1-17/+38
2023-09-16Fix more issuesSon Ho1-1/+1
2023-09-16Fix issues with name collisionsSon Ho1-6/+18
2023-09-14Make progress on the extractionSon Ho1-5/+11
2023-09-14Fix some issues with the name collisionsSon Ho1-3/+29
2023-09-11Make progress on correctly handling trait method calls in the symbolic executionSon Ho1-6/+10
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-5/+17
2023-09-03Extract the trait decl methodsSon Ho1-15/+7
2023-09-03Make progress registering the trait decl method namesSon Ho1-14/+60
2023-09-03Do more cleanupSon Ho1-3/+3
2023-09-03Add the keep_fwd field in TranslateCore.pure_fun_translationSon Ho1-1/+1
2023-09-03Update TranslateCore.pure_fun_translationSon Ho1-1/+1
2023-09-03Make progress on extracting trait decls and merge gen_ctx and extraction_ctxSon Ho1-0/+4
2023-09-03Register the names for the trait declsSon Ho1-8/+70
2023-09-03Make more progressSon Ho1-0/+2
2023-09-03Make progress on the extractionSon Ho1-8/+55
2023-09-03Make progress on the extractionSon Ho1-10/+47
2023-09-03Improve the collision detectionSon Ho1-16/+54
2023-09-01Make good progress on Extract.mlSon Ho1-3/+44
2023-08-31Make progress on Extract and ExtractBaseSon Ho1-11/+22
2023-08-02Make more progressSon Ho1-0/+14
2023-08-02Make progressSon Ho1-0/+23
2023-08-02Make progressSon Ho1-6/+7
2023-07-06Use short names for the structure fields in LeanSon Ho1-14/+54
2023-07-06Improve the generated commentsSon Ho1-5/+33
2023-07-05Start using namespaces in the Lean backendSon Ho1-1/+3
2023-07-04Reorganize the Lean testsSon Ho1-0/+10
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 02:05:54 +0000