Permalink
Browse files

Merge remote-tracking branch 'origin/master' into cheats

  • Loading branch information...
myreen committed Jan 20, 2019
2 parents f645364 + 9e7012b commit 1443c43d08d108d32d1ce7e8b8c8add0ff3d5897
Showing with 1,405 additions and 1,256 deletions.
  1. +148 −43 basis/ArrayProgScript.sml
  2. +21 −21 basis/ArrayProofScript.sml
  3. +9 −2 basis/CommandLineProgScript.sml
  4. +18 −22 basis/CommandLineProofScript.sml
  5. +0 −25 basis/CompareProgScript.sml
  6. +34 −20 basis/IntProgScript.sml
  7. +44 −53 basis/ListProgScript.sml
  8. +46 −3 basis/MapProgScript.sml
  9. +0 −61 basis/NumProgScript.sml
  10. +4 −17 basis/OptionProgScript.sml
  11. +1 −0 basis/PrettyPrinterProgScript.sml
  12. +0 −6 basis/README.md
  13. +101 −61 basis/RatProgScript.sml
  14. +4 −8 basis/RuntimeProgScript.sml
  15. +4 −1 basis/RuntimeProofScript.sml
  16. +45 −47 basis/StringProgScript.sml
  17. +69 −21 basis/TextIOProgScript.sml
  18. +192 −98 basis/TextIOProofScript.sml
  19. +42 −57 basis/VectorProgScript.sml
  20. +1 −3 basis/dependency-order
  21. +27 −0 basis/mlbasicsProgScript.sml
  22. +1 −1 basis/pure/Holmakefile
  23. +2 −2 basis/pure/README.md
  24. +1 −4 basis/pure/basisComputeLib.sml
  25. +48 −0 basis/pure/mlintScript.sml
  26. +9 −12 basis/pure/mllistScript.sml
  27. +218 −0 basis/pure/mlmapScript.sml
  28. +0 −81 basis/pure/mlnumScript.sml
  29. +5 −1 basis/pure/mloptionScript.sml
  30. +13 −5 basis/pure/mlprettyprinterScript.sml
  31. +1 −1 candle/standard/opentheory/monadIO/Holmakefile
  32. +13 −13 candle/standard/opentheory/readerProgScript.sml
  33. +0 −1 candle/standard/opentheory/readerScript.sml
  34. +1 −0 characteristic/cfTacticsLib.sig
  35. +9 −3 characteristic/cfTacticsLib.sml
  36. +1 −1 compiler/backend/displayLangScript.sml
  37. +2 −2 compiler/backend/exportScript.sml
  38. +1 −1 compiler/backend/presLangScript.sml
  39. +1 −1 compiler/backend/proofs/word_elimProofScript.sml
  40. +1 −1 compiler/bootstrap/translation/compiler32ProgScript.sml
  41. +1 −1 compiler/bootstrap/translation/compiler64ProgScript.sml
  42. +3 −0 compiler/bootstrap/translation/reg_allocProgScript.sml
  43. +1 −1 compiler/compilerScript.sml
  44. +16 −0 compiler/inference/inferenceComputeLib.sml
  45. +2 −1 compiler/inference/tests/basisTypeCheckScript.sml
  46. +1 −1 examples/Holmakefile
  47. +0 −3 examples/README.md
  48. +2 −2 examples/catProgScript.sml
  49. +2 −2 examples/compilation/ag32/proofs/wordcountProofScript.sml
  50. +1 −4 examples/compilation/x64/Holmakefile
  51. +0 −3 examples/compilation/x64/README.md
  52. +0 −11 examples/compilation/x64/iocatCompileScript.sml
  53. +0 −5 examples/compilation/x64/proofs/README.md
  54. +0 −37 examples/compilation/x64/proofs/iocatProofScript.sml
  55. +75 −106 examples/diffScript.sml
  56. +79 −4 examples/grepProgScript.sml
  57. +0 −306 examples/iocatProgScript.sml
  58. +2 −2 examples/patchProgScript.sml
  59. +5 −4 examples/sortProgScript.sml
  60. +1 −0 translator/ml_translatorLib.sml
  61. +22 −0 translator/ml_translatorScript.sml
  62. +1 −0 translator/std_preludeScript.sml
  63. +27 −32 tutorial/solutions/wordfreqProgScript.sml
  64. +27 −32 tutorial/wordfreqProgScript.sml
@@ -53,129 +53,208 @@ val _ = append_prog array_tabulate;
(*val array_vector = process_topdecs
`fun vector arr = Vector.tabulate (length arr) (fn i => sub arr i)`*)

val array_copy = process_topdecs
val _ = ml_prog_update open_local_block;

val array_copy_aux = process_topdecs
`fun copy_aux src dst di max n =
if n = max
then ()
else (update dst di (sub src n); copy_aux src dst (di + 1) max (n + 1))
else (update dst di (sub src n); copy_aux src dst (di + 1) max (n + 1))`

val _ = append_prog array_copy_aux;

fun copy src dst di =
val _ = ml_prog_update open_local_in_block;

val array_copy = process_topdecs
`fun copy src dst di =
copy_aux src dst di (length src) 0`

val _ = append_prog array_copy;

val array_copyVec = process_topdecs
val _ = ml_prog_update open_local_block;

val array_copyVec_aux = process_topdecs
`fun copyVec_aux src dst di max n =
if n = max
then ()
else (update dst (di + n) (Vector.sub src n); copyVec_aux src dst di max (n + 1))
else (update dst (di + n) (Vector.sub src n); copyVec_aux src dst di max (n + 1))`

val _ = append_prog array_copyVec_aux;

fun copyVec src dst di =
val _ = ml_prog_update open_local_in_block;

val array_copyVec = process_topdecs
`fun copyVec src dst di =
copyVec_aux src dst di (Vector.length src) 0`

val _ = append_prog array_copyVec;

val array_app = process_topdecs
val _ = ml_prog_update open_local_block;

val array_app_aux = process_topdecs
`fun app_aux f arr max n =
if n = max
then ()
else (f (sub arr n); app_aux f arr max (n + 1))
else (f (sub arr n); app_aux f arr max (n + 1))`

val _ = append_prog array_app_aux;

fun app f arr =
val _ = ml_prog_update open_local_in_block;

val array_app = process_topdecs
`fun app f arr =
app_aux f arr (length arr) 0`

val _ = append_prog array_app;

val array_appi = process_topdecs
val _ = ml_prog_update open_local_block;

val array_appi_aux = process_topdecs
`fun appi_aux f arr max n =
if n = max
then ()
else (f n (sub arr n); app_aux f arr max (n + 1))
else (f n (sub arr n); app_aux f arr max (n + 1))`

val _ = append_prog array_appi_aux;

val _ = ml_prog_update open_local_in_block;

fun appi f arr =
val array_appi = process_topdecs
`fun appi f arr =
appi_aux f arr (length arr) 0`

val _ = append_prog array_appi;

val array_modify = process_topdecs
val _ = ml_prog_update open_local_block;

val array_modify_aux = process_topdecs
`fun modify_aux f arr max n =
if n = max
then ()
else (update arr n (f (sub arr n)); modify_aux f arr max (n + 1))
else (update arr n (f (sub arr n)); modify_aux f arr max (n + 1))`

val _ = append_prog array_modify_aux;

val _ = ml_prog_update open_local_in_block;

fun modify f arr =
val array_modify = process_topdecs
`fun modify f arr =
modify_aux f arr (length arr) 0`

val _ = append_prog array_modify;

val array_modifyi = process_topdecs
val _ = ml_prog_update open_local_block;

val array_modifyi_aux = process_topdecs
`fun modifyi_aux f arr max n =
if n = max
then ()
else (update arr n (f n (sub arr n)); modifyi_aux f arr max (n + 1))
else (update arr n (f n (sub arr n)); modifyi_aux f arr max (n + 1))`

val _ = append_prog array_modifyi_aux;

val _ = ml_prog_update open_local_in_block;

fun modifyi f arr =
val array_modifyi = process_topdecs
`fun modifyi f arr =
modifyi_aux f arr (length arr) 0`

val _ = append_prog array_modifyi;

val array_foldli = process_topdecs
val _ = ml_prog_update open_local_block;

val array_foldli_aux = process_topdecs
`fun foldli_aux f init arr max n =
if n = max
then init
else foldli_aux f (f n (sub arr n) init ) arr max (n + 1)
else foldli_aux f (f n (sub arr n) init ) arr max (n + 1)`

val _ = append_prog array_foldli_aux;

val _ = ml_prog_update open_local_in_block;

fun foldli f init arr =
val array_foldli = process_topdecs
`fun foldli f init arr =
foldli_aux f init arr (length arr) 0`

val _ = append_prog array_foldli;

val array_foldl = process_topdecs
val _ = ml_prog_update open_local_block;

val array_foldl_aux = process_topdecs
`fun foldl_aux f init arr max n =
if n = max
then init
else foldl_aux f (f (sub arr n) init ) arr max (n + 1)
else foldl_aux f (f (sub arr n) init ) arr max (n + 1)`

val _ = append_prog array_foldl_aux;

fun foldl f init arr =
val _ = ml_prog_update open_local_in_block;

val array_foldl = process_topdecs
`fun foldl f init arr =
foldl_aux f init arr (length arr) 0`

val _ = append_prog array_foldl;

val array_foldri = process_topdecs
val _ = ml_prog_update open_local_block;

val array_foldri_aux = process_topdecs
`fun foldri_aux f init arr n =
if n = 0
then init
else foldri_aux f (f (n - 1) (sub arr (n - 1)) init) arr (n - 1)
else foldri_aux f (f (n - 1) (sub arr (n - 1)) init) arr (n - 1)`

val _ = append_prog array_foldri_aux;

fun foldri f init arr =
val _ = ml_prog_update open_local_in_block;

val array_foldri = process_topdecs
`fun foldri f init arr =
foldri_aux f init arr (length arr)`

val _ = append_prog array_foldri;

val array_foldr = process_topdecs
val _ = ml_prog_update open_local_block;

val array_foldr_aux = process_topdecs
`fun foldr_aux f init arr n =
if n = 0
then init
else foldr_aux f (f (sub arr (n - 1)) init) arr (n - 1)
else foldr_aux f (f (sub arr (n - 1)) init) arr (n - 1)`

val _ = append_prog array_foldr_aux;

fun foldr f init arr =
val _ = ml_prog_update open_local_in_block;

val array_foldr = process_topdecs
`fun foldr f init arr =
foldr_aux f init arr (length arr)`

val _ = append_prog array_foldr;

val array_find = process_topdecs
val _ = ml_prog_update open_local_block;

val array_find_aux = process_topdecs
`fun find_aux f arr max n =
if n = max
then None
else (if f (sub arr n)
then Some(sub arr n)
else find_aux f arr max (n + 1))
else find_aux f arr max (n + 1))`

val _ = append_prog array_find_aux;

fun find f arr =
val _ = ml_prog_update open_local_in_block;

val array_find = process_topdecs
`fun find f arr =
find_aux f arr (length arr) 0`

val _ = append_prog array_find;

val _ = ml_prog_update open_local_block;

(* Parser bug, see Issue #25 *)
val array_findi_aux =
``[(Dletrec unknown_loc
@@ -224,48 +303,72 @@ val array_findi_aux =
Var (Short "max")];
Var (Short "e")]))))))))))])]``

val _ = append_prog array_findi_aux;

val _ = ml_prog_update open_local_in_block;

val array_findi = process_topdecs
`fun findi f arr =
findi_aux f arr (length arr) 0`

val _ = append_prog array_findi_aux;
val _ = append_prog array_findi;

val array_exists = process_topdecs
val _ = ml_prog_update open_local_block;

val array_exists_aux = process_topdecs
`fun exists_aux f arr max n =
if n = max
then False
else (if f (sub arr n)
then True
else exists_aux f arr max (n + 1))
else exists_aux f arr max (n + 1))`

fun exists f arr =
val _ = append_prog array_exists_aux;

val _ = ml_prog_update open_local_in_block;

val array_exists = process_topdecs
`fun exists f arr =
exists_aux f arr (length arr) 0`

val _ = append_prog array_exists;

val array_all = process_topdecs
val _ = ml_prog_update open_local_block;

val array_all_aux = process_topdecs
`fun all_aux f arr max n =
if n = max
then True
else (if f (sub arr n)
then all_aux f arr max (n + 1)
else False)
else False)`

fun all f arr =
val _ = append_prog array_all_aux;

val _ = ml_prog_update open_local_in_block;

val array_all = process_topdecs
`fun all f arr =
all_aux f arr (length arr) 0`

val _ = append_prog array_all;

val array_collate = process_topdecs
val _ = ml_prog_update open_local_block;

val array_collate_aux = process_topdecs
`fun collate_aux f a1 a2 max ord n =
if n = max
then ord
else (if f (sub a1 n) (sub a2 n) = Equal
then collate_aux f a1 a2 max ord (n + 1)
else f (sub a1 n) (sub a2 n))
else f (sub a1 n) (sub a2 n))`

fun collate f a1 a2 =
val _ = append_prog array_collate_aux;

val _ = ml_prog_update open_local_in_block;

val array_collate = process_topdecs
`fun collate f a1 a2 =
if (length a1) < (length a2)
then collate_aux f a1 a2 (length a1) Less 0
else if (length a2) < (length a1)
@@ -274,6 +377,8 @@ val array_collate = process_topdecs

val _ = append_prog array_collate;

val _ = ml_prog_update close_local_blocks;

val _ = ml_prog_update (close_module NONE);

val _ = export_theory ()
Oops, something went wrong.

0 comments on commit 1443c43

Please sign in to comment.