summaryrefslogtreecommitdiff
path: root/src/PureToExtract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2022-02-09Add a commentSon Ho1-0/+1
2022-02-09Cleanup a bitSon Ho1-10/+10
2022-02-09Implement the generation of `decreases` clauses in the definitionSon Ho1-0/+4
2022-02-09Start working on the generation of decrease clausesSon Ho1-0/+31
2022-02-09Improve a bit the quality of the generated code by adjusting theSon Ho1-38/+25
2022-02-08Fix some issuesSon Ho1-79/+91
2022-02-08Make progress on implementing support for types and functions likeSon Ho1-1/+9
2022-02-07Implement printing of debugging messages in case of name clashesSon Ho1-22/+116
2022-02-03Implement a micro pass to filter the box functionsSon Ho1-25/+0
2022-02-03Cleanup a bitSon Ho1-4/+2
2022-02-03Implement extraction of switch int and make extract_texpression returnSon Ho1-9/+5
2022-02-03Implement extraction of function callsSon Ho1-68/+122
2022-02-03Implement ExtractToFStar.extract_typed_rvalueSon Ho1-7/+19
2022-02-03Make more progress on implementing function extractionSon Ho1-20/+96
2022-02-03Make progress on function extractionSon Ho1-4/+13
2022-02-02Make minor modifications to extract mutually recursive typesSon Ho1-0/+26
2022-02-02Fix more issues when extracting types to F*Son Ho1-2/+3
2022-02-02Start generating code for type definitionsSon Ho1-0/+13
2022-02-01Implement ExtractToFStar.mk_name_formatterSon Ho1-6/+8
2022-01-29Make a minor modificationSon Ho1-1/+1
2022-01-29Make progress on ExtractToFStar.mk_name_formatterSon Ho1-1/+2
2022-01-29Make the field names optional and make progress on ExtractToFStarSon Ho1-1/+7
2022-01-29Make progress on ExtractToFStarSon Ho1-28/+62
2022-01-29Make progress on ExtractToFstarSon Ho1-1/+24
2022-01-29Start working on extraction to F*Son Ho1-19/+98
2022-01-29Make progress on PureToExtractSon Ho1-95/+93
2022-01-29Make progress on PureToExtractSon Ho1-81/+209
2022-01-27Move some definitions from SymbolicToPure to PureToExtractSon Ho1-0/+103