summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-1/+1
2023-10-26Fix more issues at extraction and factor out defs in ExtractBuiltinSon Ho1-6/+23
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-2391/+109
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-23/+22
2023-10-25Update following the addition of raw pointersSon Ho1-1/+4
2023-10-24Fix an issue coming from the modification for the opaque signaturesSon Ho1-12/+7
2023-10-24Fix a printing issue with scalar valuesSon Ho1-3/+5
2023-10-24Filter some type arguments for the builtin types/functionsSon Ho1-2/+65
2023-10-24Remove the possibility of generating opaque module signaturesSon Ho1-116/+51
2023-10-24Add support for builtin trait implementationsSon Ho1-2/+30
2023-10-24Fix various issues with the builtinsSon Ho1-34/+81
2023-10-23Make progress on handling the builtinsSon Ho1-42/+212
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-68/+77
2023-10-22Add more support for numeric operations, xor, rotateJonathan Protzenko1-4/+7
2023-10-20Start updating to handle function pointersSon Ho1-2/+2
2023-10-16Improve formatting of scalars in LeanSon Ho1-23/+10
2023-10-13Add supSon Ho1-1/+3
2023-10-06Slightly improve formatting of the generated codeSon Ho1-1/+6
2023-09-19Cleanup a bitSon Ho1-2/+2
2023-09-17Merge trans_ctx and decls_ctxSon Ho1-6/+2
2023-09-17Make progress on correctly extracting trait method callsSon Ho1-26/+84
2023-09-17Fix some issues with calls to trait methodsSon Ho1-9/+14
2023-09-17Fix some formatting issuesSon Ho1-2/+10
2023-09-17Fix several issues with the extractionSon Ho1-66/+98
2023-09-16Fix issues with name registration/lookupSon Ho1-2/+26
2023-09-16Fix more issuesSon Ho1-7/+6
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:35:38 +0000