Skip to content
Permalink
Browse files

Merge branch 'master' into monadic-trans-cleanup

  • Loading branch information...
hrutvik committed Feb 18, 2019
2 parents bbbb336 + 9feef1e commit 3c21e96e2e4a4d64d5e0c8adc3fcde3a4099fbf6
Showing with 8,948 additions and 5,947 deletions.
  1. +3 −3 README.md
  2. +151 −46 basis/ArrayProgScript.sml
  3. +25 −25 basis/ArrayProofScript.sml
  4. +9 −2 basis/CommandLineProgScript.sml
  5. +18 −22 basis/CommandLineProofScript.sml
  6. +0 −25 basis/CompareProgScript.sml
  7. +34 −20 basis/IntProgScript.sml
  8. +44 −53 basis/ListProgScript.sml
  9. +46 −3 basis/MapProgScript.sml
  10. +0 −61 basis/NumProgScript.sml
  11. +4 −17 basis/OptionProgScript.sml
  12. +1 −0 basis/PrettyPrinterProgScript.sml
  13. +0 −6 basis/README.md
  14. +101 −61 basis/RatProgScript.sml
  15. +7 −11 basis/RuntimeProgScript.sml
  16. +4 −1 basis/RuntimeProofScript.sml
  17. +45 −47 basis/StringProgScript.sml
  18. +74 −28 basis/TextIOProgScript.sml
  19. +242 −161 basis/TextIOProofScript.sml
  20. +42 −57 basis/VectorProgScript.sml
  21. +3 −4 basis/basisFunctionsLib.sml
  22. +5 −9 basis/basisProgScript.sml
  23. +1 −0 basis/basis_ffi.c
  24. +2 −1 basis/basis_ffiLib.sml
  25. +10 −5 basis/basis_ffiScript.sml
  26. +1 −3 basis/dependency-order
  27. +31 −2 basis/mlbasicsProgScript.sml
  28. +1 −1 basis/pure/Holmakefile
  29. +2 −2 basis/pure/README.md
  30. +1 −4 basis/pure/basisComputeLib.sml
  31. +48 −0 basis/pure/mlintScript.sml
  32. +9 −12 basis/pure/mllistScript.sml
  33. +218 −0 basis/pure/mlmapScript.sml
  34. +0 −81 basis/pure/mlnumScript.sml
  35. +5 −1 basis/pure/mloptionScript.sml
  36. +13 −5 basis/pure/mlprettyprinterScript.sml
  37. +3 −3 basis/pure/mlstringScript.sml
  38. +2 −2 basis/pure/mlvectorScript.sml
  39. +1 −2 candle/standard/ml_kernel/ml_hol_kernelProgScript.sml
  40. +1 −1 candle/standard/monadic/holKernelProofScript.sml
  41. +1 −1 candle/standard/opentheory/monadIO/Holmakefile
  42. +13 −13 candle/standard/opentheory/readerProgScript.sml
  43. +0 −1 candle/standard/opentheory/readerScript.sml
  44. +13 −9 candle/standard/syntax/holConservativeScript.sml
  45. +7 −0 characteristic/README.md
  46. +33 −14 characteristic/cfAppScript.sml
  47. +46 −0 characteristic/cfDivLib.sml
  48. +2,390 −0 characteristic/cfDivScript.sml
  49. +2 −0 characteristic/cfHeapsBaseLib.sig
  50. +13 −2 characteristic/cfHeapsBaseLib.sml
  51. +269 −63 characteristic/cfHeapsBaseScript.sml
  52. +117 −9 characteristic/cfHeapsBaseSyntax.sml
  53. +107 −50 characteristic/cfLetAutoLib.sml
  54. +1 −0 characteristic/cfLib.sml
  55. +37 −36 characteristic/cfMainScript.sml
  56. +3 −1 characteristic/cfNormaliseScript.sml
  57. +570 −261 characteristic/cfScript.sml
  58. +1 −0 characteristic/cfTacticsLib.sig
  59. +31 −8 characteristic/cfTacticsLib.sml
  60. +4 −4 characteristic/cfTacticsScript.sml
  61. +9 −9 characteristic/examples/cf_examplesScript.sml
  62. +2 −2 compiler/backend/README.md
  63. +1 −10 compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml
  64. +5 −3 compiler/backend/backend_commonScript.sml
  65. +5 −1 compiler/backend/bvi_tailrecScript.sml
  66. +8 −7 compiler/backend/bvl_to_bviScript.sml
  67. +5 −3 compiler/backend/clos_annotateScript.sml
  68. +1 −1 compiler/backend/displayLangScript.sml
  69. +2 −2 compiler/backend/exportScript.sml
  70. +5 −5 compiler/backend/flatLangScript.sml
  71. +1 −1 compiler/backend/presLangScript.sml
  72. +7 −7 compiler/backend/proofs/backendProofScript.sml
  73. +6 −9 compiler/backend/proofs/bvi_to_dataProofScript.sml
  74. +7 −7 compiler/backend/proofs/bvl_inlineProofScript.sml
  75. +2 −2 compiler/backend/proofs/bvl_to_bviProofScript.sml
  76. +13 −10 compiler/backend/proofs/clos_annotateProofScript.sml
  77. +21 −14 compiler/backend/proofs/clos_callProofScript.sml
  78. +9 −9 compiler/backend/proofs/clos_knownProofScript.sml
  79. +2 −1 compiler/backend/proofs/clos_labelsProofScript.sml
  80. +24 −29 compiler/backend/proofs/clos_letopProofScript.sml
  81. +2 −1 compiler/backend/proofs/clos_ticksProofScript.sml
  82. +83 −79 compiler/backend/proofs/clos_to_bvlProofScript.sml
  83. +1 −1 compiler/backend/proofs/data_to_word_assignProofScript.sml
  84. +7 −27 compiler/backend/proofs/data_to_word_memoryProofScript.sml
  85. +71 −62 compiler/backend/proofs/flat_exh_matchProofScript.sml
  86. +5 −5 compiler/backend/proofs/lab_to_targetProofScript.sml
  87. +1 −1 compiler/backend/proofs/pat_to_closProofScript.sml
  88. +14 −13 compiler/backend/proofs/source_to_flatProofScript.sml
  89. +18 −13 compiler/backend/proofs/stack_allocProofScript.sml
  90. +1 −1 compiler/backend/proofs/stack_namesProofScript.sml
  91. +2 −2 compiler/backend/proofs/stack_removeProofScript.sml
  92. +0 −10 compiler/backend/proofs/stack_to_labProofScript.sml
  93. +1 −1 compiler/backend/proofs/word_allocProofScript.sml
  94. +1 −1 compiler/backend/proofs/word_elimProofScript.sml
  95. +1 −1 compiler/backend/proofs/word_to_wordProofScript.sml
  96. +1 −1 compiler/backend/reg_alloc/parmoveScript.sml
  97. +1 −1 compiler/backend/semantics/bviPropsScript.sml
  98. +1 −1 compiler/backend/semantics/bvlPropsScript.sml
  99. +4 −4 compiler/backend/semantics/closPropsScript.sml
  100. +8 −17 compiler/backend/semantics/labPropsScript.sml
  101. +3 −0 compiler/backend/semantics/stackPropsScript.sml
  102. +9 −2 compiler/backend/semantics/stackSemScript.sml
  103. +7 −3 compiler/backend/stackLangScript.sml
  104. +18 −16 compiler/backend/stack_allocScript.sml
  105. +9 −5 compiler/backend/stack_namesScript.sml
  106. +5 −1 compiler/backend/stack_removeScript.sml
  107. +9 −8 compiler/backend/stack_to_labScript.sml
  108. +92 −0 compiler/benchmarks/Holmakefile
  109. +7 −69 compiler/benchmarks/README.md
  110. +280 −38 compiler/benchmarks/cakeml_benchmarks/benchmark.py
  111. +12 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/Holmakefile
  112. +0 −24 compiler/benchmarks/cakeml_benchmarks/cakeml/Makefile
  113. +1 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/Makefile
  114. +40 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/README.md
  115. +5 −1 compiler/benchmarks/cakeml_benchmarks/cakeml/{array_contain.sml → array_contain.cml}
  116. +1 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/basis_ffi.c
  117. +7 −12 compiler/benchmarks/cakeml_benchmarks/cakeml/{bst_contain.sml → bst_contain.cml}
  118. +4 −1 compiler/benchmarks/cakeml_benchmarks/cakeml/{btree.sml → btree.cml}
  119. +7 −3 compiler/benchmarks/cakeml_benchmarks/cakeml/{dummy_contain.sml → dummy_contain.cml}
  120. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{fib.sml → fib.cml}
  121. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{foldl.sml → foldl.cml}
  122. +46 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/make_all.sh
  123. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{nqueens.sml → nqueens.cml}
  124. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{qsort.sml → qsort.cml}
  125. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{qsortimp.sml → qsortimp.cml}
  126. +6 −3 compiler/benchmarks/cakeml_benchmarks/cakeml/{queue.sml → queue.cml}
  127. +1 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/readmePrefix
  128. +3 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/{reverse.sml → reverse.cml}
  129. +15 −11 compiler/benchmarks/cakeml_benchmarks/cakeml/{sptree_contain.sml → sptree_contain.cml}
  130. +3 −3 compiler/benchmarks/cakeml_benchmarks/ocaml/Makefile
  131. +4 −4 compiler/benchmarks/cakeml_benchmarks/ocaml/bst_contain.ml
  132. +2 −2 compiler/benchmarks/cakeml_benchmarks/ocaml/sptree_contain.ml
  133. +0 −18 compiler/benchmarks/cakeml_benchmarks/ocaml/time_all.sh
  134. +0 −16 compiler/benchmarks/cakeml_benchmarks/plot_benchmarks2.gplot
  135. +11 −11 compiler/benchmarks/cakeml_benchmarks/sml/Makefile
  136. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/array_contain.sml
  137. +8 −4 compiler/benchmarks/cakeml_benchmarks/sml/bst_contain.sml
  138. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/btree.sml
  139. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/dummy_contain.sml
  140. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/fib.sml
  141. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/foldl.sml
  142. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/nqueens.sml
  143. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/qsort.sml
  144. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/qsortimp.sml
  145. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/queue.sml
  146. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/reverse.sml
  147. +4 −0 compiler/benchmarks/cakeml_benchmarks/sml/sptree_contain.sml
  148. +1 −1 compiler/benchmarks/mlton_benchmarks/README.md
  149. +192 −155 compiler/benchmarks/mlton_benchmarks/benchmark.py
  150. +12 −0 compiler/benchmarks/mlton_benchmarks/cakeml/Holmakefile
  151. +0 −35 compiler/benchmarks/mlton_benchmarks/cakeml/Makefile
  152. +1 −0 compiler/benchmarks/mlton_benchmarks/cakeml/Makefile
  153. +52 −0 compiler/benchmarks/mlton_benchmarks/cakeml/README.md
  154. +1 −0 compiler/benchmarks/mlton_benchmarks/cakeml/basis_ffi.c
  155. +8 −4 compiler/benchmarks/mlton_benchmarks/cakeml/{even-odd.sml → even-odd.cml}
  156. +6 −2 compiler/benchmarks/mlton_benchmarks/cakeml/{fib.sml → fib.cml}
  157. +5 −1 compiler/benchmarks/mlton_benchmarks/cakeml/{flat-array.sml → flat-array.cml}
  158. +8 −4 compiler/benchmarks/mlton_benchmarks/cakeml/{imp-for.sml → imp-for.cml}
  159. +20 −22 compiler/benchmarks/mlton_benchmarks/cakeml/{knuth-bendix.sml → knuth-bendix.cml}
  160. +10 −7 compiler/benchmarks/mlton_benchmarks/cakeml/{life.sml → life.cml}
  161. +138 −68 compiler/benchmarks/mlton_benchmarks/cakeml/{logic.sml → logic.cml}
  162. +28 −29 compiler/benchmarks/mlton_benchmarks/cakeml/make_all.sh
  163. +4 −2 compiler/benchmarks/mlton_benchmarks/cakeml/{merge.sml → merge.cml}
  164. +8 −6 compiler/benchmarks/mlton_benchmarks/cakeml/{mpuz.sml → mpuz.cml}
  165. +14 −11 compiler/benchmarks/mlton_benchmarks/cakeml/{pidigits.sml → pidigits.cml}
  166. +31 −31 compiler/benchmarks/mlton_benchmarks/cakeml/{ratio-regions.sml → ratio-regions.cml}
  167. +2 −0 compiler/benchmarks/mlton_benchmarks/cakeml/readmePrefix
  168. +488 −0 compiler/benchmarks/mlton_benchmarks/cakeml/smith-normal-form.cml
  169. +0 −380 compiler/benchmarks/mlton_benchmarks/cakeml/smith-normal-form.sml
  170. +4 −1 compiler/benchmarks/mlton_benchmarks/cakeml/{tailfib.sml → tailfib.cml}
  171. +4 −1 compiler/benchmarks/mlton_benchmarks/cakeml/{tak.sml → tak.cml}
  172. +4 −2 compiler/benchmarks/mlton_benchmarks/cakeml/{vector-concat.sml → vector-concat.cml}
  173. +5 −3 compiler/benchmarks/mlton_benchmarks/cakeml/{vector-rev.sml → vector-rev.cml}
  174. +3 −3 compiler/benchmarks/mlton_benchmarks/sml/Makefile
  175. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/even-odd.sml
  176. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/fib.sml
  177. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/flat-array.sml
  178. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/imp-for.sml
  179. +18 −15 compiler/benchmarks/mlton_benchmarks/sml/knuth-bendix.sml
  180. +14 −11 compiler/benchmarks/mlton_benchmarks/sml/life.sml
  181. +148 −145 compiler/benchmarks/mlton_benchmarks/sml/logic.sml
  182. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/merge.sml
  183. +5 −2 compiler/benchmarks/mlton_benchmarks/sml/mpuz.sml
  184. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/pidigits.sml
  185. +14 −11 compiler/benchmarks/mlton_benchmarks/sml/ratio-regions.sml
  186. +32 −29 compiler/benchmarks/mlton_benchmarks/sml/smith-normal-form.sml
  187. +3 −0 compiler/benchmarks/mlton_benchmarks/sml/tailfib.sml
  188. +4 −1 compiler/benchmarks/mlton_benchmarks/sml/tak.sml
  189. +3 −0 compiler/benchmarks/mlton_benchmarks/sml/vector-concat.sml
  190. +5 −2 compiler/benchmarks/mlton_benchmarks/sml/vector-rev.sml
  191. +1 −0 compiler/benchmarks/readmePrefix
  192. +71 −0 compiler/benchmarks/requirements.txt
  193. +6 −0 compiler/bootstrap/compilation/x64/Makefile
  194. +1 −1 compiler/bootstrap/translation/compiler32ProgScript.sml
  195. +1 −1 compiler/bootstrap/translation/compiler64ProgScript.sml
  196. +5 −4 compiler/bootstrap/translation/reg_allocProgScript.sml
  197. +1 −1 compiler/compilerScript.sml
  198. +8 −7 compiler/inference/inferScript.sml
  199. +16 −0 compiler/inference/inferenceComputeLib.sml
  200. +53 −47 compiler/inference/proofs/inferCompleteScript.sml
  201. +2 −2 compiler/inference/proofs/inferPropsScript.sml
  202. +2 −1 compiler/inference/tests/basisTypeCheckScript.sml
  203. +7 −18 compiler/parsing/cmlPEGScript.sml
  204. +4 −5 compiler/parsing/lexer_implScript.sml
  205. +58 −139 compiler/parsing/proofs/pegCompleteScript.sml
  206. +4 −27 compiler/parsing/proofs/pegSoundScript.sml
  207. +34 −32 compiler/parsing/tests/cmlTestsScript.sml
  208. +3 −0 developers/build-sequence
  209. +1 −1 examples/Holmakefile
  210. +3 −3 examples/README.md
  211. +7 −11 examples/catProgScript.sml
  212. +2 −2 examples/compilation/ag32/proofs/wordcountProofScript.sml
  213. +1 −4 examples/compilation/x64/Holmakefile
  214. +0 −3 examples/compilation/x64/README.md
  215. +0 −11 examples/compilation/x64/iocatCompileScript.sml
  216. +0 −5 examples/compilation/x64/proofs/README.md
  217. +0 −37 examples/compilation/x64/proofs/iocatProofScript.sml
  218. +75 −106 examples/diffScript.sml
  219. +158 −0 examples/divScript.sml
  220. +1 −1 examples/doubleProgScript.sml
  221. +81 −8 examples/grepProgScript.sml
  222. +0 −306 examples/iocatProgScript.sml
  223. +2 −2 examples/patchProgScript.sml
  224. +3 −4 examples/queueProgScript.sml
  225. +21 −17 examples/sortProgScript.sml
  226. +3 −4 examples/stackProgScript.sml
  227. +13 −12 how-to.md
  228. +3 −9 misc/README.md
  229. +0 −52 misc/alist_treeLib.sig
  230. +0 −346 misc/alist_treeLib.sml
  231. +0 −316 misc/alist_treeScript.sml
  232. +8 −15 misc/basicComputeLib.sml
  233. +236 −0 misc/byteScript.sml
  234. +0 −6 misc/lem_lib_stub/README.md
  235. +0 −8 misc/lem_lib_stub/lem_map_extraScript.sml
  236. +0 −8 misc/lem_lib_stub/lem_show_extraScript.sml
  237. +1 −2 misc/lem_lib_stub/lib.lem
  238. +11 −12 misc/lem_lib_stub/libScript.sml
  239. +52 −918 misc/miscScript.sml
  240. +6 −5 misc/preamble.sml
  241. +5 −3 semantics/README.md
  242. +2 −0 semantics/ast.lem
  243. +3 −1 semantics/astScript.sml
  244. +11 −24 semantics/cmlPtreeConversionScript.sml
  245. +2 −2 semantics/evaluateScript.sml
  246. +7 −8 semantics/ffi/ffiScript.sml
  247. +10 −9 semantics/ffi/simpleIOScript.sml
  248. +9 −18 semantics/gramScript.sml
  249. +2 −2 semantics/grammar.txt
  250. +0 −1 semantics/lexer_funScript.sml
  251. +5 −5 semantics/primTypes.lem
  252. +5 −5 semantics/primTypesScript.sml
  253. +11 −14 semantics/proofs/cmlPtreeConversionPropsScript.sml
  254. +64 −23 semantics/proofs/evaluatePropsScript.sml
  255. +3 −3 semantics/proofs/primSemEnvScript.sml
  256. +2 −2 semantics/proofs/semanticPrimitivesPropsScript.sml
  257. +5 −5 semantics/proofs/typeSoundInvariantsScript.sml
  258. +2 −2 semantics/proofs/typeSoundScript.sml
  259. +5 −3 semantics/readmePrefix
  260. +5 −5 semantics/semanticPrimitives.lem
  261. +6 −6 semantics/semanticPrimitivesScript.sml
  262. +1 −1 semantics/tokens.lem
  263. +1 −1 semantics/tokensScript.sml
  264. +15 −0 translator/ml_progLib.sig
  265. +222 −141 translator/ml_progLib.sml
  266. +98 −67 translator/ml_progScript.sml
  267. +3 −3 translator/ml_translatorLib.sig
  268. +85 −77 translator/ml_translatorLib.sml
  269. +29 −4 translator/ml_translatorScript.sml
  270. +51 −0 translator/ml_translator_testScript.sml
  271. +2 −2 translator/monadic/cfMonadLib.sml
  272. +26 −22 translator/monadic/cfMonadScript.sml
  273. +7 −5 translator/monadic/ml_monadStoreLib.sml
  274. +2 −2 translator/monadic/ml_monad_translatorBaseScript.sml
  275. +4 −7 translator/std_preludeScript.sml
  276. +27 −32 tutorial/solutions/wordfreqProgScript.sml
  277. +27 −32 tutorial/wordfreqProgScript.sml
  278. +3 −13 unverified/sexpr-bootstrap/x64/64/extract_code.cml
@@ -68,9 +68,9 @@ Auxiliary files providing glue between a standard HOL installation
and what we want to use for CakeML development.

[semantics](semantics):
The definition of the CakeML language. The definition is (mostly)
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
The definition of the CakeML language. The definition is (mostly) expressed in
[Lem](https://www.cl.cam.ac.uk/~pes20/lem), but the generated HOL is included.
The directory includes definitions of:
- the concrete syntax,
- the abstract syntax,
- big step semantics (both functional and relational),
@@ -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
then False
else (if f (sub arr n)
then true
else exists_aux f arr max (n + 1))
then True
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
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 3c21e96

Please sign in to comment.
You can’t perform that action at this time.