Permalink
Browse files

Fix merge conflict in compilationLib

  • Loading branch information...
oskarabrahamsson committed Jul 15, 2018
2 parents e50424d + ec62391 commit 8aafa2110b46528e41a0010d2051f9fd84c4b2ae
Showing with 28,104 additions and 14,531 deletions.
  1. +3 −0 .gitignore
  2. +2 −2 COPYING
  3. +8 −3 README.md
  4. +4 −3 basis/ArrayProofScript.sml
  5. +2 −1 basis/ListProgScript.sml
  6. +50 −0 basis/PrettyPrinterProgScript.sml
  7. +2 −3 basis/StringProgScript.sml
  8. +2 −5 basis/basisProgScript.sml
  9. +1 −1 basis/basis_ffi.c
  10. +10 −11 basis/basis_ffiScript.sml
  11. +1 −0 basis/dependency-order
  12. +0 −1 basis/mlbasicsProgScript.sml
  13. +92 −0 basis/pure/mlprettyprinterScript.sml
  14. +3 −1 build-instructions.sh
  15. +2 −2 candle/set-theory/Holmakefile
  16. +1 −1 candle/set-theory/zfc/setSpecScript.sml
  17. +4 −4 candle/standard/ml_kernel/ml_hol_kernelProgScript.sml
  18. +1 −1 candle/standard/ml_kernel/ppKernelScript.sml
  19. +14 −12 characteristic/cfAppScript.sml
  20. +2 −1 characteristic/cfHeapsBaseLib.sml
  21. +1 −1 characteristic/cfHeapsBaseScript.sml
  22. +4 −18 characteristic/cfMainScript.sml
  23. +2 −1 characteristic/cfScript.sml
  24. +3 −4 characteristic/cfStoreScript.sml
  25. +7 −11 characteristic/cfTacticsLib.sml
  26. +2 −2 compiler/backend/Holmakefile
  27. +1 −1 compiler/backend/arm6/arm6_configScript.sml
  28. +1 −1 compiler/backend/arm8/arm8_configScript.sml
  29. +54 −16 compiler/backend/backendComputeLib.sml
  30. +13 −9 compiler/backend/backendScript.sml
  31. +2 −2 compiler/backend/backend_commonScript.sml
  32. +90 −237 compiler/backend/bvi_tailrecScript.sml
  33. +6 −1 compiler/backend/bvi_to_dataScript.sml
  34. +169 −35 compiler/backend/bvl_constScript.sml
  35. +98 −52 compiler/backend/bvl_inlineScript.sml
  36. +17 −3 compiler/backend/bvl_to_bviScript.sml
  37. +3 −1 compiler/backend/closLangScript.sml
  38. +535 −123 compiler/backend/clos_knownScript.sml
  39. +60 −0 compiler/backend/clos_letopScript.sml
  40. +48 −0 compiler/backend/clos_ticksScript.sml
  41. +5 −2 compiler/backend/clos_to_bvlScript.sml
  42. +5 −3 compiler/backend/data_liveScript.sml
  43. +89 −3 compiler/backend/data_to_wordScript.sml
  44. +3 −3 compiler/backend/exh_to_patScript.sml
  45. +1 −1 compiler/backend/mips/mips_configScript.sml
  46. +1 −0 compiler/backend/patLangScript.sml
  47. +2 −0 compiler/backend/pat_to_closScript.sml
  48. +380 −106 compiler/backend/proofs/backendProofScript.sml
  49. +2 −2 compiler/backend/proofs/bvi_letProofScript.sml
  50. +1,287 −1,267 compiler/backend/proofs/bvi_tailrecProofScript.sml
  51. +126 −100 compiler/backend/proofs/bvi_to_dataProofScript.sml
  52. +87 −29 compiler/backend/proofs/bvl_constProofScript.sml
  53. +1,439 −692 compiler/backend/proofs/bvl_inlineProofScript.sml
  54. +989 −441 compiler/backend/proofs/bvl_to_bviProofScript.sml
  55. +273 −297 compiler/backend/proofs/clos_annotateProofScript.sml
  56. +79 −31 compiler/backend/proofs/clos_callProofScript.sml
  57. +3,023 −856 compiler/backend/proofs/clos_knownProofScript.sml
  58. +27 −15 compiler/backend/proofs/clos_knownPropsScript.sml
  59. +639 −0 compiler/backend/proofs/clos_letopProofScript.sml
  60. +1,253 −684 compiler/backend/proofs/clos_mtiProofScript.sml
  61. +273 −349 compiler/backend/proofs/clos_numberProofScript.sml
  62. +921 −0 compiler/backend/proofs/clos_ticksProofScript.sml
  63. +1,337 −538 compiler/backend/proofs/clos_to_bvlProofScript.sml
  64. +20 −63 compiler/backend/proofs/con_to_decProofScript.sml
  65. +15 −16 compiler/backend/proofs/data_liveProofScript.sml
  66. +29 −9 compiler/backend/proofs/data_spaceProofScript.sml
  67. +267 −156 compiler/backend/proofs/data_to_wordProofScript.sml
  68. +996 −145 compiler/backend/proofs/data_to_word_assignProofScript.sml
  69. +32 −26 compiler/backend/proofs/data_to_word_bignumProofScript.sml
  70. +134 −50 compiler/backend/proofs/data_to_word_gcProofScript.sml
  71. +31 −5 compiler/backend/proofs/data_to_word_memoryProofScript.sml
  72. +18 −76 compiler/backend/proofs/dec_to_exhProofScript.sml
  73. +17 −18 compiler/backend/proofs/exh_reorderProofScript.sml
  74. +508 −119 compiler/backend/proofs/exh_to_patProofScript.sml
  75. +108 −24 compiler/backend/proofs/lab_filterProofScript.sml
  76. +1,043 −254 compiler/backend/proofs/lab_to_targetProofScript.sml
  77. +19 −65 compiler/backend/proofs/mod_to_conProofScript.sml
  78. +134 −120 compiler/backend/proofs/pat_to_closProofScript.sml
  79. +5 −4 compiler/backend/proofs/source_to_modProofScript.sml
  80. +282 −171 compiler/backend/proofs/stack_allocProofScript.sml
  81. +106 −39 compiler/backend/proofs/stack_namesProofScript.sml
  82. +494 −233 compiler/backend/proofs/stack_removeProofScript.sml
  83. +808 −243 compiler/backend/proofs/stack_to_labProofScript.sml
  84. +495 −129 compiler/backend/proofs/word_allocProofScript.sml
  85. +11 −9 compiler/backend/proofs/word_bignumProofScript.sml
  86. +275 −175 compiler/backend/proofs/word_removeProofScript.sml
  87. +42 −27 compiler/backend/proofs/word_simpProofScript.sml
  88. +543 −262 compiler/backend/proofs/word_to_stackProofScript.sml
  89. +294 −226 compiler/backend/proofs/word_to_wordProofScript.sml
  90. +764 −110 compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml
  91. +42 −7 compiler/backend/reg_alloc/reg_allocComputeLib.sml
  92. +644 −146 compiler/backend/reg_alloc/reg_allocScript.sml
  93. +35 −0 compiler/backend/semantics/backendPropsScript.sml
  94. +101 −45 compiler/backend/semantics/bviPropsScript.sml
  95. +53 −14 compiler/backend/semantics/bviSemScript.sml
  96. +194 −57 compiler/backend/semantics/bvlPropsScript.sml
  97. +67 −18 compiler/backend/semantics/bvlSemScript.sml
  98. +1,049 −58 compiler/backend/semantics/closPropsScript.sml
  99. +132 −55 compiler/backend/semantics/closSemScript.sml
  100. +0 −887 compiler/backend/semantics/clos_relationPropsScript.sml
  101. +0 −2,482 compiler/backend/semantics/clos_relationScript.sml
  102. +17 −41 compiler/backend/semantics/conPropsScript.sml
  103. +6 −4 compiler/backend/semantics/conSemScript.sml
  104. +105 −57 compiler/backend/semantics/dataPropsScript.sml
  105. +63 −26 compiler/backend/semantics/dataSemScript.sml
  106. +5 −14 compiler/backend/semantics/decPropsScript.sml
  107. +4 −3 compiler/backend/semantics/decSemScript.sml
  108. +11 −16 compiler/backend/semantics/exhPropsScript.sml
  109. +8 −5 compiler/backend/semantics/exhSemScript.sml
  110. +101 −41 compiler/backend/semantics/labPropsScript.sml
  111. +64 −25 compiler/backend/semantics/labSemScript.sml
  112. +15 −43 compiler/backend/semantics/modPropsScript.sml
  113. +6 −4 compiler/backend/semantics/modSemScript.sml
  114. +37 −15 compiler/backend/semantics/patPropsScript.sml
  115. +66 −8 compiler/backend/semantics/patSemScript.sml
  116. +157 −15 compiler/backend/semantics/stackPropsScript.sml
  117. +79 −25 compiler/backend/semantics/stackSemScript.sml
  118. +27 −32 compiler/backend/semantics/targetPropsScript.sml
  119. +20 −9 compiler/backend/semantics/targetSemScript.sml
  120. +240 −89 compiler/backend/semantics/wordPropsScript.sml
  121. +113 −40 compiler/backend/semantics/wordSemScript.sml
  122. +5 −0 compiler/backend/stackLangScript.sml
  123. +3 −0 compiler/backend/stack_namesScript.sml
  124. +16 −1 compiler/backend/stack_removeScript.sml
  125. +6 −0 compiler/backend/stack_to_labScript.sml
  126. +16 −1 compiler/backend/wordLangScript.sml
  127. +307 −9 compiler/backend/word_allocScript.sml
  128. +2 −0 compiler/backend/word_simpScript.sml
  129. +12 −0 compiler/backend/word_to_stackScript.sml
  130. +2 −2 compiler/backend/word_to_wordScript.sml
  131. +1 −1 compiler/backend/x64/x64_configScript.sml
  132. +45 −0 compiler/benchmarks/cakeml_benchmarks/cakeml/bst_contain.sml
  133. +5 −5 compiler/benchmarks/mlton_benchmarks/cakeml/life.sml
  134. +15 −1 compiler/bootstrap/translation/explorerProgScript.sml
  135. +225 −63 compiler/bootstrap/translation/reg_allocProgScript.sml
  136. +249 −46 compiler/bootstrap/translation/to_dataProgScript.sml
  137. +4 −0 compiler/bootstrap/translation/to_target32ProgScript.sml
  138. +5 −2 compiler/bootstrap/translation/to_target64ProgScript.sml
  139. +69 −8 compiler/bootstrap/translation/to_word32ProgScript.sml
  140. +80 −20 compiler/bootstrap/translation/to_word64ProgScript.sml
  141. +9 −6 compiler/compilationLib.sml
  142. +1 −7 compiler/compilerScript.sml
  143. +24 −25 compiler/inference/proofs/inferPropsScript.sml
  144. +2 −2 compiler/inference/proofs/inferSoundScript.sml
  145. +11 −11 compiler/inference/proofs/infer_eSoundScript.sml
  146. +1 −1 compiler/parsing/cmlPEGScript.sml
  147. +3 −3 compiler/parsing/proofs/pegCompleteScript.sml
  148. +2 −1 compiler/parsing/proofs/pegSoundScript.sml
  149. +33 −7 compiler/parsing/tests/cmlTestsScript.sml
  150. +8 −8 compiler/proofs/compilerProofScript.sml
  151. +1 −1 developers/Holmakefile
  152. +4 −0 developers/README.md
  153. +3 −0 developers/bin/.gitignore
  154. +17 −0 developers/bin/Holmakefile
  155. +2 −0 developers/bin/readmePrefix
  156. +30 −0 developers/bin/set_heap_stack.sml
  157. +7 −4 developers/build-sequence
  158. +3 −3 examples/iocatProgScript.sml
  159. +2 −2 examples/quicksortProgScript.sml
  160. +65 −0 misc/miscScript.sml
  161. +6 −1 readmePrefix
  162. +4 −2 semantics/alt_semantics/proofs/bigClockScript.sml
  163. +7 −5 semantics/alt_semantics/proofs/interpScript.sml
  164. +9 −8 semantics/astScript.sml
  165. +12 −4 semantics/cmlPtreeConversionScript.sml
  166. +18 −17 semantics/ffi/ffi.lem
  167. +22 −19 semantics/ffi/ffiScript.sml
  168. +6 −6 semantics/ffi/simpleIO.lem
  169. +6 −6 semantics/ffi/simpleIOScript.sml
  170. +1 −1 semantics/gramScript.sml
  171. +1 −1 semantics/proofs/cmlPtreeConversionPropsScript.sml
  172. +19 −14 semantics/proofs/evaluatePropsScript.sml
  173. +5 −3 semantics/proofs/semanticPrimitivesPropsScript.sml
  174. +47 −12 semantics/proofs/semanticsPropsScript.sml
  175. +20 −11 semantics/proofs/typeSoundScript.sml
  176. +3 −7 semantics/proofs/typeSysPropsScript.sml
  177. +1 −1 semantics/proofs/weakeningScript.sml
  178. +4 −1 semantics/semanticPrimitives.lem
  179. +5 −2 semantics/semanticPrimitivesScript.sml
  180. +9 −9 semantics/semanticsScript.sml
  181. +10 −3 translator/ml_pmatchScript.sml
  182. +176 −1 translator/ml_pmatch_demoScript.sml
  183. +9 −3 translator/ml_translatorLib.sig
  184. +286 −183 translator/ml_translatorLib.sml
  185. +11 −0 translator/ml_translatorScript.sml
  186. +63 −0 translator/ml_translator_testScript.sml
  187. +217 −11 translator/monadic/examples/floyd_warshallProgScript.sml
  188. +15 −12 translator/monadic/ml_monadBaseLib.sml
  189. +3 −3 translator/monadic/ml_monadStoreLib.sml
  190. +1 −0 translator/monadic/ml_monadStoreScript.sml
  191. +6 −3 translator/monadic/ml_monad_translatorLib.sml
  192. +3 −3 tutorial/wordfreqProofScript.sml
  193. +1,286 −889 unverified/reg_alloc/reg_alloc.sml
  194. +3 −3 unverified/sexpr-bootstrap/x64/32/Holmakefile
  195. +3 −3 unverified/sexpr-bootstrap/x64/64/Holmakefile
View
@@ -9,6 +9,9 @@
.HOLMK
.hollogs
# TacticToe
*Script_ttt.sml
# Generated assembly
*.S
View
@@ -1,7 +1,7 @@
CakeML Copyright Notice, License, and Disclaimer.
Copyright 2013, 2014, 2015, 2016, 2017 by
Anthony Fox, Ramana Kumar, Magnus Myreen,
Copyright 2013, 2014, 2015, 2016, 2017, 2018 by
Anthony Fox, Google LLC, Ramana Kumar, Magnus Myreen,
Michael Norrish, Scott Owens, Yong Kiam Tan, and
other contributors listed at https://cakeml.org
View
@@ -5,12 +5,17 @@ CakeML is a verified implementation of a significant subset of
Standard ML.
The source and proofs for CakeML are developed in the [HOL4 theorem
prover](http://hol-theorem-prover.org). We use the latest development
prover](http://hol-theorem-prover.org). We use the latest development
version of [HOL4](https://github.com/HOL-Theorem-Prover/HOL), which we
build on [PolyML 5.7](http://www.polyml.org).
Example build instructions can be found in
[build-instructions.sh](build-instructions.sh).
Building all of CakeML (including the bootstrapped compiler and its proofs)
requires significant resources. [Built copies](https://cakeml.org/download) of
the compiler and resource usage for our
[regression tests](https://cakeml.org/regression.cgi) are online.
The [master](../../tree/master) branch contains the latest development
version of CakeML. See the [version2](../../tree/version2) or
[version1](../../tree/version1) branch for previous versions.
@@ -44,8 +49,8 @@ A verified compiler for CakeML, including:
- targets: code generation to x86, ARM, and more
[developers](developers):
This directory contains scripts for automating routine tasks, e.g. for
running regression tests.
This directory contains scripts for automating routine tasks, e.g., for
generating README.md files.
[documentation](documentation):
Work-in-progress documentation regarding the CakeML language.
@@ -171,12 +171,13 @@ val array_tabulate_spec = Q.store_thm ("array_tabulate_spec",
>- (xapp \\ xsimpl \\ instantiate)
\\ xlet `POSTv u. ARRAY av (LUPDATE val (LENGTH l_pre) (l_pre ++ rest))`
>- (xapp \\ xsimpl \\ instantiate \\ `LENGTH l_pre + LENGTH rest <> LENGTH l_pre` by metis_tac[num_eq_thm] \\ fs[])
\\ xlet `POSTv vp. & NUM ((LENGTH l_pre) + 1) vp * ARRAY av (LUPDATE val (LENGTH l_pre) (l_pre ++ rest))`
>- (xapp \\ xsimpl \\ fs [NUM_def] \\ instantiate \\ rw[integerTheory.INT_ADD])
\\ xlet_auto
\\ fs [plus_def]
THEN1 xsimpl
\\ xapp \\ xsimpl \\ cases_on `rest`
>- (`xv = nv` by fs [NUM_def, INT_def])
\\ qexists_tac `t` \\ qexists_tac `l_pre ++ [val]`
\\ fs [LENGTH, ADD1, GSYM CONS_APPEND, lupdate_append2] \\ rw[GENLIST_CONS, GSYM ADD1, o_DEF] \\ fs [ADD1]) >>
\\ fs [LENGTH, ADD1, GSYM CONS_APPEND, lupdate_append2] \\ rw[GENLIST_CONS, GSYM ADD1, o_DEF] \\ fs [ADD1,NUM_def,GSYM integerTheory.INT_ADD]) >>
Cases_on `n` >>
fs [NUM_def, INT_def] >>
rfs []
View
@@ -103,7 +103,8 @@ val result = translate EVERY_DEF;
val result = translate SNOC;
val result = translate GENLIST_AUX;
val result = translate GENLIST_GENLIST_AUX;
val result = translate tabulate_aux_def;
val res = translate tabulate_aux_def;
val result = translate tabulate_def;
val result = translate collate_def;
@@ -0,0 +1,50 @@
open
preamble
ml_translatorLib
ml_progLib
TextIOProgTheory
mlprettyprinterTheory
val _ = (
new_theory "PrettyPrinterProg";
translation_extends "TextIOProg";
generate_sigs := true;
register_type ``:'a app_list``;
ml_prog_update (open_module "PrettyPrinter")
)
fun tr name def = (
next_ml_names := [name];
translate def
)
val _ = tr "fromString" fromString_def
val _ = tr "fromChar" fromChar_def
val _ = tr "fromBool" fromBool_def
val _ = tr "fromInt" fromInt_def
val _ = tr "fromNum" fromNum_def
val _ = tr "fromWord8" fromWord8_def
val _ = tr "fromWord64" fromWord64_def
val _ = tr "fromRat" fromRat_def
val _ = tr "fromOption" fromOption_def
val _ = tr "fromList" fromList_def
val _ = tr "fromArray" fromArray_def
val _ = tr "fromVector" fromVector_def
val sigs = module_signatures [
"fromString",
"fromChar",
"fromBool",
"fromInt",
"fromNum",
"fromWord8",
"fromWord64",
"fromRat",
"fromOption",
"fromList",
"fromArray",
"fromVector"
]
val _ = ml_prog_update (close_module (SOME sigs))
val _ = export_theory ()
@@ -36,8 +36,7 @@ val extract_side_thm = Q.prove(
`!s i opt. extract_side s i opt`,
rw [extract_side_def, MIN_DEF] ) |> update_precondition
val result = translate concatWith_aux_def;
val res = translate concatWith_aux_def;
val _ = next_ml_names := ["concatWith"];
val result = translate concatWith_def;
@@ -62,7 +61,7 @@ val translate_side_thm = Q.prove (
val r = translate splitl_aux_def;
val r = translate splitl_def;
val result = translate tokens_aux_def;
val res = translate tokens_aux_def;
val tokens_aux_side_def = theorem"tokens_aux_side_def";
val result = translate tokens_def;
val tokens_side_def = definition"tokens_side_def";
@@ -1,16 +1,13 @@
open preamble ml_translatorLib ml_progLib cfLib basisFunctionsLib
CommandLineProofTheory TextIOProofTheory
CommandLineProofTheory TextIOProofTheory PrettyPrinterProgTheory
val _ = new_theory "basisProg"
val _ = translation_extends"TextIOProg";
val _ = translation_extends"PrettyPrinterProg";
val print_eval_thm = derive_eval_thm true "print" ``Var(Long"TextIO"(Short"print"))``
val () = ml_prog_update (add_Dlet print_eval_thm "print" [])
val res = register_type``:'a app_list``;
val MISC_APP_LIST_TYPE_def = theorem"MISC_APP_LIST_TYPE_def";
val print_app_list = process_topdecs
`fun print_app_list ls =
(case ls of
View
@@ -129,7 +129,7 @@ int hasT = 0;
void cml_exit(int arg) {
#ifdef DEBUG_FFI
{
printf("GCNum: %d, GCTime(us): %ld\n",numGC,microsecs);
fprintf(stderr,"GCNum: %d, GCTime(us): %ld\n",numGC,microsecs);
}
#endif
exit(arg);
View
@@ -14,43 +14,42 @@ val basis_ffi_oracle_def = Define `
if name = "write" then
case ffi_write conf bytes fs of
| SOME (bytes,fs) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "read" then
case ffi_read conf bytes fs of
| SOME (bytes,fs) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "get_arg_count" then
case ffi_get_arg_count conf bytes cls of
| SOME (bytes,cls) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "get_arg_length" then
case ffi_get_arg_length conf bytes cls of
| SOME (bytes,cls) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "get_arg" then
case ffi_get_arg conf bytes cls of
| SOME (bytes,cls) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "open_in" then
case ffi_open_in conf bytes fs of
| SOME (bytes,fs) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "open_out" then
case ffi_open_out conf bytes fs of
| SOME (bytes,fs) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
| _ => Oracle_final FFI_failed else
if name = "close" then
case ffi_close conf bytes fs of
| SOME (bytes,fs) => Oracle_return (cls,fs) bytes
| _ => Oracle_fail else
Oracle_fail`
| _ => Oracle_final FFI_failed else
Oracle_final FFI_failed`
(* standard streams are initialized *)
val basis_ffi_def = Define `
basis_ffi cl fs =
<| oracle := basis_ffi_oracle
; ffi_state := (cl, fs)
; final_event := NONE
; io_events := [] |>`;
val basis_proj1_def = Define `
@@ -250,7 +249,7 @@ val RTC_call_FFI_rel_IMP_basis_events = Q.store_thm ("RTC_call_FFI_rel_IMP_basis
\\ HO_MATCH_MP_TAC RTC_INDUCT \\ rw [] \\ fs []
\\ fs [evaluatePropsTheory.call_FFI_rel_def]
\\ fs [ffiTheory.call_FFI_def]
\\ Cases_on `st.final_event = NONE` \\ fs [] \\ rw []
(* \\ Cases_on `st.final_event = NONE` \\ fs [] \\ rw []*)
\\ Cases_on `n = ""` \\ fs [] THEN1 (rveq \\ fs [])
\\ FULL_CASE_TAC \\ fs [] \\ rw [] \\ fs []
\\ FULL_CASE_TAC \\ fs [] \\ rw [] \\ fs []
View
@@ -28,4 +28,5 @@ Compare
Map
CommandLine
TextIO
PrettyPrinter
basis
@@ -78,5 +78,4 @@ val assign_spec = Q.store_thm ("assign_spec",
(rv ~~> xv) (POSTv v. cond (UNIT_TYPE () v) * rv ~~> yv)`,
prove_ref_spec "op :=");
val _ = export_theory ()
@@ -0,0 +1,92 @@
open
preamble
mlstringTheory
mlintTheory
mlnumTheory
wordsTheory
val _ = new_theory "mlprettyprinter"
val fromString_def = Define`
fromString s = List [strlit "\""; s; strlit "\""]
`
val fromChar_def = Define`
fromChar c = List [strlit "#\""; str c; strlit "\""]
`
val fromBool_def = Define`
fromBool b =
List [if b then (strlit "true") else (strlit "false")]
`
val fromInt_def = Define`
fromInt i = List [(mlint$toString i)]
`
val fromNum_def = Define`
fromNum n = List [(mlnum$toString n)]
`
val fromWord8_def = Define`
fromWord8 (w : 8 word) =
List [strlit "0wx"; mlnum$toString (words$w2n w)]
`
val fromWord64_def = Define`
fromWord64 (w : 64 word) =
List [strlit "0wx", mlnum$toString (words$w2n w)]
`
val fromRat_def = Define`
fromRat (n:int, d:num) =
if d = 1 then List [mlint$toString n]
else List [mlint$toString n; strlit "/"; mlnum$toString d]
`
val fromOption_def = Define`
fromOption f opt =
case opt of
NONE => List [strlit "NONE"]
| SOME el => Append (List [strlit "SOME "]) (f el)
`
val fromList_def = Define`
fromList f l =
case l of
[] => List [strlit "[]"]
| h::t =>
Append
(Append
(List [strlit "["])
( FOLDL (λ acc el .
Append (Append acc (List [strlit ", "])) (f el)
) (f h) t
)
)
(List [strlit "]"])
`
val fromArray_def = Define`
fromArray f a =
Append
( foldli (λ i acc el .
if i = 0 then f el
else Append (Append acc (List [strlit ", "])) (f el)
) (List [strlit "fromList["]) a
)
(List [strlit "]"])
`
val fromVector_def = Define`
fromVector f v =
Append
( foldli (λ i acc el .
if i = 0 then f el
else Append (Append acc (List [strlit ", "])) (f el)
) (List [strlit "fromList["]) v
)
(List [strlit "]"])
`
val _ = export_theory ()
View
@@ -26,14 +26,16 @@ cd HOL
# git checkout kananaskis-11
## note: currently, we only aim to ensure that
## CakeML branch master builds on HOL branch master
poly < tools/smart-configure.sml
poly --script tools/smart-configure.sml
bin/build
## optionally set HOLDIR to point to the HOL installation
# export HOLDIR=$HOME/HOL
## optionally put $HOLDIR/bin in your PATH
# export PATH=$HOLDIR/bin:$PATH
## build CakeML
## note: a full build (including the bootstrapped compiler)
## takes a long time (~20 hours) and requires much RAM (~16 GB)
cd
git clone https://github.com/CakeML/cakeml
cd cakeml
@@ -1,4 +1,4 @@
INCLUDES = ../../misc $(HOLDIR)/examples/set-theory/hol_sets
INCLUDES = ../../misc $(HOLDIR)/src/pred_set/src/more_theories
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
@@ -12,7 +12,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = $(HOLDIR)/examples/set-theory/hol_sets/cardinalTheory ../../misc/miscTheory
BARE_THYS = $(HOLDIR)/src/pred_set/src/more_theories/cardinalTheory ../../misc/miscTheory
DEPS = $(patsubst %,%.uo,$(BARE_THYS))
@@ -9,7 +9,7 @@ fun remove_tyabbrev s =
let
val _ = Parse.temp_set_grammars(type_grammar.remove_abbreviation(Parse.type_grammar())s,Parse.term_grammar())
val q = String.concat["val ",ct,"_grammars = (type_grammar.remove_abbreviation(#1 ",ct,"_grammars)\"",s,"\",#2 ",ct,"_grammars);"]
val _ = adjoin_to_theory{sig_ps=NONE, struct_ps=SOME(fn pp => PP.add_string pp q)}
val _ = adjoin_to_theory{sig_ps=NONE, struct_ps=SOME(fn _ => PP.add_string q)}
in () end
end
val _ = remove_tyabbrev"reln"
Oops, something went wrong.

0 comments on commit 8aafa21

Please sign in to comment.