summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-14Make progress on the extractionSon Ho3-6/+24
2023-09-14Fix some issues with the name collisionsSon Ho1-3/+29
2023-09-13Fix some issuesSon Ho7-16/+81
2023-09-13Fix more issuesSon Ho4-40/+157
2023-09-13Make minor modificationsSon Ho5-47/+38
2023-09-11Make progress on correctly handling trait method calls in the symbolic executionSon Ho12-67/+221
2023-09-10Add support for the trait associated constantsSon Ho11-13/+83
2023-09-10Implement handling of trait method function callsSon Ho1-66/+115
2023-09-07Fix some issuesSon Ho2-15/+26
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho7-38/+112
2023-09-04Fix a minor issue in HOL4Son Ho1-1/+1
2023-09-04Fix minor issuesSon Ho2-3/+15
2023-09-03Implement extract_trait_implSon Ho1-6/+160
2023-09-03Extract the trait decl methodsSon Ho2-34/+54
2023-09-03Make progress registering the trait decl method namesSon Ho2-31/+93
2023-09-03Do more cleanupSon Ho3-9/+9
2023-09-03Add the keep_fwd field in TranslateCore.pure_fun_translationSon Ho4-35/+42
2023-09-03Update TranslateCore.pure_fun_translationSon Ho5-34/+33
2023-09-03Update the type TranslateCore.fun_and_loopsSon Ho4-34/+35
2023-09-03Make progress on extracting trait decls and merge gen_ctx and extraction_ctxSon Ho3-98/+219
2023-09-03Register the names for the trait declsSon Ho2-14/+154
2023-09-03Make more progressSon Ho3-24/+67
2023-09-03Make progress on the extractionSon Ho3-61/+221
2023-09-03Make progress on the extractionSon Ho6-21/+264
2023-09-03Make progress on the extractionSon Ho6-52/+138
2023-09-03Improve the collision detectionSon Ho1-16/+54
2023-09-01Make good progress on Extract.mlSon Ho2-224/+237
2023-09-01Update PureMicroPassesSon Ho2-44/+19
2023-09-01Compute the normalized trait types maps and update InterpreterSon Ho6-70/+206
2023-09-01Implement the normalization functions in AssociatedTypesSon Ho5-14/+335
2023-08-31Make progress on Extract and ExtractBaseSon Ho3-52/+132
2023-08-31Update TranslateCore and factor out some definitions in PrintPureSon Ho2-42/+42
2023-08-31Finish updating SymbolicToPure.mlSon Ho4-115/+212
2023-08-31Start adding support for traitsSon Ho31-776/+1258
2023-08-18Add tests which use const generics as valuesSon Ho2-2/+5
2023-08-18Update following the introduction of ConstantExprSon Ho16-143/+220
2023-08-17Make a minor modificationSon Ho1-11/+0
2023-08-08Update the code following a refactor on Charon's sideSon Ho4-12/+27
2023-08-07Change some fun id names to use "Mut"/"Shared" as a suffixSon Ho5-66/+66
2023-08-04Add an option to not override Hashmap.leanSon Ho3-2/+15
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho2-12/+12
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho5-35/+62
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 Ho10-180/+320
2023-08-03Make a minor formatting modification for LeanSon Ho1-1/+1
2023-08-03Fix issuesSon Ho10-57/+139
2023-08-02Make minor modificationsSon Ho3-16/+29
2023-08-02Add the function signatures in Assumed.mlSon Ho1-0/+143
2023-08-02Make more progressSon Ho2-75/+186
2023-08-02Make progressSon Ho5-53/+80
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 20:42:48 +0000