summaryrefslogtreecommitdiff
path: root/src/PureToExtract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 01:56:42 +0000