summaryrefslogtreecommitdiff
path: root/src/Print.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-10-13Rename Modules to CratesSon Ho1-5/+6
2022-09-22Reformat the project with duneSon Ho1-16/+18
2022-07-18Address much stuff of the PR, throw exceptions at remaining placesSidney Congard1-10/+13
2022-06-29Make minor modificationsSon Ho1-1/+1
2022-06-21concrete & symbolic evaluation work with new LLBC formatSidney Congard1-41/+37
2022-06-13crude generation working - missing unit tests & special constants handlingSidney Congard1-0/+1
2022-06-08read globals from LLBC JSON into functionsSidney Congard1-6/+7
2022-05-15Treat integer casts in a general mannerSon Ho1-1/+9
2022-05-15Add AggregatedOptionSon Ho1-3/+9
2022-05-10Make minor modificationsSon Ho1-7/+1
2022-05-01Perform some renamingsSon Ho1-17/+17
2022-04-26Introduce the Abs expression and continue updating the codeSon Ho1-2/+2
2022-04-26Introduce the App expression, and make progress updating the codeSon Ho1-1/+1
2022-04-21Improve the generation of names for given back valuesSon Ho1-1/+1
2022-04-21Work on pretty namesSon Ho1-1/+1
2022-04-20Introduce mdplace to link meta information about the given back valuesSon Ho1-1/+1
2022-04-20Improve the generation of pretty names by correctly using theSon Ho1-3/+2
2022-03-03In fun_id rename the variant Local to RegularSon Ho1-1/+1
2022-03-03Make good progress on adding support for external and opaqueSon Ho1-29/+44
2022-03-03Rename CFIM to LLBCSon Ho1-5/+5
2022-03-03Add an Opaque variant to type_decl_kind and start updating the codeSon Ho1-1/+2
2022-03-03Update the name definition to use path_elemSon Ho1-6/+8
2022-03-03Move the names from Identifiers to NamesSon Ho1-1/+1
2022-03-03Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...declSon Ho1-79/+82
2022-02-24Update the way function names are handledSon Ho1-4/+10
2022-02-23Improve pretty-printing of environments by filtering and grouping valuesSon Ho1-3/+65
2022-02-22Add support for "fused" match branchesSon Ho1-4/+7
2022-02-08Add an option to allow the presence of bottom values below borrowsSon Ho1-0/+4
2022-02-08Update some code in Print for OptionSon Ho1-0/+10
2022-02-08Implement pre-passes to update the AST before executing the interpreterSon Ho1-1/+1
2022-02-08Fix some issuesSon Ho1-0/+5
2022-02-08Start adding more assumed types and functionsSon Ho1-6/+45
2022-01-29Make the field names optional and make progress on ExtractToFStarSon Ho1-7/+17
2022-01-27Introduce AEndedSharedBorrow so as not to introduce ABottom whenSon Ho1-0/+1
2022-01-27Add some printing facilities to SymbolicToPureSon Ho1-0/+50
2022-01-26Fix various issuesSon Ho1-2/+2
2022-01-26Add a meta-value in SharedBorrow to carry the shared valueSon Ho1-1/+1
2022-01-24Start working on printing for symbolic ASTSon Ho1-2/+2
2022-01-21Update AProjLoans and AEndedProjLoans to take a list of given backSon Ho1-6/+17
2022-01-19Start storing meta-values in the avalues, for synthesis purposesSon Ho1-4/+7
2022-01-18Update type_context to have to have a type info field, use maps insteadSon Ho1-20/+23
2022-01-15Use the new collectionsSon Ho1-5/+5
2022-01-15Start working on Collections.mlSon Ho1-1/+1
2022-01-14Improve printing of symbolic values in abstractionsSon Ho1-18/+16
2022-01-14Implement greedy expansion of symbolic variables and expansion beforeSon Ho1-10/+9
2022-01-14Start working on greedy symbolic value expansion and expansion beforeSon Ho1-9/+9
2022-01-14Update aproj to make AEndedProjLoans take an `aproj option` and add theSon Ho1-2/+6
2022-01-13Introduce "AIgnore" for the avaluesSon Ho1-0/+1
2022-01-13Introduce ended borrow/loan projectors over symbolic valuesSon Ho1-0/+2
2022-01-12Update end_borrow to check if there are loans in borrowed valuesSon Ho1-0/+19