summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Make progress on the HOL4 backendSon Ho1-10/+34
2023-06-04Make progress on extracting the HOL4 filesSon Ho1-15/+78
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho1-9/+13
2023-06-04Make good progress on generating code for HOL4Son Ho1-291/+906
2023-06-04Make more updates for the Lean backendSon Ho1-14/+27
2023-06-04Make minor modificationsSon Ho1-1/+9
2023-06-04Update Extract.mlSon Ho1-15/+35
2023-06-04Make extract_adt_cons call extract_adt_g_valueSon Ho1-54/+15
2023-06-04Make a minor fixSon Ho1-7/+1
2023-06-04Improve the generation of variant names for LeanSon Ho1-14/+21
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho1-1/+7
2023-06-04Add a special expression for structure creation/updateSon Ho1-51/+54
2023-06-04Update the extraction of Lean filesSon Ho1-14/+28
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho1-1/+1
2023-06-04Handle the "opaque_defs." prefix in a cleaner mannerSon Ho1-31/+70
2023-06-04Make minor modificationsSon Ho1-41/+89
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho1-16/+33
2023-06-04Update the generation of termination and decreases_by templates for LeanSon Ho1-23/+30
2023-06-04WIPJonathan Protzenko1-3/+6
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 Ho1-41/+48
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 Ho1-124/+135
2023-06-04All of the generated code is syntactically correctJonathan Protzenko1-4/+5
2023-06-04WIPJonathan Protzenko1-2/+8
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 Protzenko1-15/+136
2023-06-04WIP lots of stuffJonathan Protzenko1-9/+17
2023-06-04Fix a syntax errorJonathan Protzenko1-2/+6
2023-06-04Custom syntax support for structures in LeanJonathan Protzenko1-9/+34
2023-06-04More cosmetic improvementsJonathan Protzenko1-12/+20
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko1-9/+30
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-12/+11
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko1-1/+1
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-91/+197
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho1-3/+4
2023-02-03Fix various issues with the generation of code for the loopsSon Ho1-11/+18
2023-02-03Add a `Loop` node in the pure ASTSon Ho1-0/+3
2023-02-03Introduce new loop ids in Pure and keep track of the number of loops in a fun...Son Ho1-3/+4
2023-02-03Add loop ids to the pure functions identifiersSon Ho1-4/+10
2022-11-16Generate record field projectors for CoqSon Ho1-71/+228
2022-11-16Improve formattingSon Ho1-95/+116
2022-11-16Make minor modifications to the extractionSon Ho1-4/+13
2022-11-14Extract the Polonius examples in CoqSon Ho1-13/+16
2022-11-14Add a `-use-fuel` optionSon Ho1-7/+22
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho1-1/+12
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 08:04:07 +0000