summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-16Fix issues with name collisionsSon Ho1-7/+21
2023-09-14Make progress on the extractionSon Ho1-1/+9
2023-09-11Make progress on correctly handling trait method calls in the symbolic executionSon Ho1-2/+2
2023-09-10Add support for the trait associated constantsSon Ho1-1/+12
2023-09-07Fix some issuesSon Ho1-1/+0
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-1/+7
2023-09-04Fix a minor issue in HOL4Son Ho1-1/+1
2023-09-03Implement extract_trait_implSon Ho1-6/+160
2023-09-03Extract the trait decl methodsSon Ho1-19/+47
2023-09-03Make progress registering the trait decl method namesSon Ho1-17/+33
2023-09-03Do more cleanupSon Ho1-3/+5
2023-09-03Update TranslateCore.pure_fun_translationSon Ho1-1/+2
2023-09-03Update the type TranslateCore.fun_and_loopsSon Ho1-2/+2
2023-09-03Make progress on extracting trait decls and merge gen_ctx and extraction_ctxSon Ho1-5/+145
2023-09-03Register the names for the trait declsSon Ho1-6/+84
2023-09-03Make more progressSon Ho1-6/+13
2023-09-03Make progress on the extractionSon Ho1-53/+165
2023-09-03Make progress on the extractionSon Ho1-1/+12
2023-09-03Make progress on the extractionSon Ho1-26/+50
2023-09-01Make good progress on Extract.mlSon Ho1-221/+193
2023-08-31Make progress on Extract and ExtractBaseSon Ho1-41/+102
2023-08-18Update following the introduction of ConstantExprSon Ho1-0/+3
2023-08-07Change some fun id names to use "Mut"/"Shared" as a suffixSon Ho1-30/+30
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho1-12/+10
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho1-28/+30
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-10/+12
2023-08-03Fix an issue with the extraction of aggregated arraysSon Ho1-85/+133
2023-08-03Fix issuesSon Ho1-38/+77
2023-08-02Make more progressSon Ho1-75/+172
2023-08-02Make progressSon Ho1-34/+56
2023-07-12Make the `by inlit` implicitSon Ho1-1/+1
2023-07-06Use short names for the structure fields in LeanSon Ho1-4/+9
2023-07-06Improve the generated commentsSon Ho1-19/+65
2023-07-05Simplify the names used in Primitives.leanSon Ho1-16/+33
2023-07-05Simplify the generated names for the types in LeanSon Ho1-5/+12
2023-07-05Start using namespaces in the Lean backendSon Ho1-13/+15
2023-07-04Fix minor issuesSon Ho1-4/+10
2023-07-04Fix some issues with the extraction to LeanSon Ho1-48/+86
2023-07-04Reorganize the Lean testsSon Ho1-8/+6
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 09:04:32 +0000