Skip to content
Permalink
Browse files

Use new Overload syntax

  • Loading branch information...
myreen committed Sep 5, 2019
1 parent 7e2dacb commit eaaffc1090438ad6451a91c3479adcd63572c719
Showing with 525 additions and 534 deletions.
  1. +8 −6 basis/TextIOProofScript.sml
  2. +1 −1 basis/Word8ProgScript.sml
  3. +6 −4 basis/basis_ffiScript.sml
  4. +7 −6 basis/fsFFIPropsScript.sml
  5. +1 −1 basis/fsFFIScript.sml
  6. +2 −1 basis/pure/mlintScript.sml
  7. +7 −6 basis/pure/mlstringScript.sml
  8. +23 −23 candle/set-theory/setSpecScript.sml
  9. +36 −36 candle/set-theory/zfc/setSpecScript.sml
  10. +8 −8 candle/standard/monadic/holKernelPmatchScript.sml
  11. +10 −10 candle/standard/monadic/holKernelProofScript.sml
  12. +11 −10 candle/standard/monadic/holKernelScript.sml
  13. +3 −3 candle/standard/opentheory/compilation/ag32/proofs/readerProgProofScript.sml
  14. +8 −7 candle/standard/opentheory/monadIO/readerIOScript.sml
  15. +3 −3 candle/standard/opentheory/prettyScript.sml
  16. +5 −5 candle/standard/opentheory/readerScript.sml
  17. +8 −8 candle/standard/opentheory/reader_initScript.sml
  18. +16 −16 candle/standard/semantics/holAxiomsScript.sml
  19. +21 −21 candle/standard/semantics/holBoolScript.sml
  20. +2 −1 candle/standard/semantics/holExtensionScript.sml
  21. +19 −19 candle/standard/semantics/holSemanticsScript.sml
  22. +19 −19 candle/standard/syntax/holAxiomsSyntaxScript.sml
  23. +21 −20 candle/standard/syntax/holBoolSyntaxScript.sml
  24. +3 −3 candle/standard/syntax/holSyntaxExtraScript.sml
  25. +24 −23 candle/standard/syntax/holSyntaxScript.sml
  26. +12 −12 characteristic/cfHeapsBaseScript.sml
  27. +1 −2 compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml
  28. +1 −2 compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml
  29. +2 −2 compiler/backend/backend_commonScript.sml
  30. +3 −3 compiler/backend/bvl_to_bviScript.sml
  31. +2 −2 compiler/backend/data_to_wordScript.sml
  32. +1 −1 compiler/backend/jsonLangScript.sml
  33. +1 −2 compiler/backend/lab_to_targetScript.sml
  34. +24 −24 compiler/backend/proofs/backendProofScript.sml
  35. +1 −1 compiler/backend/proofs/bvi_tailrecProofScript.sml
  36. +3 −3 compiler/backend/proofs/bvi_to_dataProofScript.sml
  37. +4 −4 compiler/backend/proofs/bvl_to_bviProofScript.sml
  38. +1 −1 compiler/backend/proofs/clos_annotateProofScript.sml
  39. +1 −1 compiler/backend/proofs/clos_knownProofScript.sml
  40. +1 −1 compiler/backend/proofs/clos_knownPropsScript.sml
  41. +2 −2 compiler/backend/proofs/clos_letopProofScript.sml
  42. +1 −1 compiler/backend/proofs/clos_ticksProofScript.sml
  43. +1 −15 compiler/backend/proofs/clos_to_bvlProofScript.sml
  44. +5 −5 compiler/backend/proofs/data_to_wordProofScript.sml
  45. +0 −3 compiler/backend/proofs/data_to_word_assignProofScript.sml
  46. +0 −3 compiler/backend/proofs/data_to_word_bignumProofScript.sml
  47. +0 −2 compiler/backend/proofs/data_to_word_gcProofScript.sml
  48. +1 −1 compiler/backend/proofs/data_to_word_memoryProofScript.sml
  49. +4 −4 compiler/backend/proofs/flat_reorder_matchProofScript.sml
  50. +4 −4 compiler/backend/proofs/lab_to_targetProofScript.sml
  51. +1 −1 compiler/backend/proofs/stack_allocProofScript.sml
  52. +1 −1 compiler/backend/proofs/stack_removeProofScript.sml
  53. +4 −4 compiler/backend/proofs/stack_to_labProofScript.sml
  54. +1 −1 compiler/backend/proofs/word_bignumProofScript.sml
  55. +5 −5 compiler/backend/reg_alloc/linear_scanScript.sml
  56. +6 −6 compiler/backend/reg_alloc/parmoveScript.sml
  57. +4 −4 compiler/backend/reg_alloc/proofs/linear_scanProofScript.sml
  58. +4 −4 compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml
  59. +5 −5 compiler/backend/reg_alloc/reg_allocScript.sml
  60. +1 −1 compiler/backend/semantics/bviSemScript.sml
  61. +1 −1 compiler/backend/semantics/bvlSemScript.sml
  62. +3 −3 compiler/backend/semantics/closPropsScript.sml
  63. +2 −1 compiler/backend/semantics/closSemScript.sml
  64. +9 −8 compiler/backend/semantics/dataSemScript.sml
  65. +1 −2 compiler/backend/semantics/labPropsScript.sml
  66. +2 −1 compiler/backend/semantics/labSemScript.sml
  67. +1 −1 compiler/backend/stack_namesScript.sml
  68. +2 −2 compiler/backend/stack_to_labScript.sml
  69. +1 −1 compiler/backend/wordLangScript.sml
  70. +2 −2 compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml
  71. +4 −4 compiler/bootstrap/translation/reg_allocProgScript.sml
  72. +1 −1 compiler/compilerScript.sml
  73. +2 −2 compiler/encoders/ag32/ag32_targetScript.sml
  74. +1 −1 compiler/encoders/arm7/arm7_targetScript.sml
  75. +2 −2 compiler/encoders/mips/mips_targetScript.sml
  76. +5 −5 compiler/encoders/monadic_enc/monadic_enc32Script.sml
  77. +5 −5 compiler/encoders/monadic_enc/monadic_enc64Script.sml
  78. +1 −1 compiler/encoders/riscv/riscv_targetScript.sml
  79. +1 −1 compiler/encoders/x64/proofs/x64_targetProofScript.sml
  80. +6 −8 compiler/encoders/x64/x64_targetScript.sml
  81. +4 −4 compiler/inference/inferScript.sml
  82. +2 −2 compiler/parsing/cmlPEGScript.sml
  83. +1 −2 compiler/parsing/cmlParseScript.sml
  84. +2 −3 compiler/parsing/fromSexpScript.sml
  85. +14 −16 compiler/parsing/tests/cmlTestsScript.sml
  86. +6 −3 developers/readme_gen.sml
  87. +2 −2 examples/compilation/ag32/proofs/helloProofScript.sml
  88. +2 −2 examples/compilation/ag32/proofs/sortProofScript.sml
  89. +2 −2 examples/compilation/ag32/proofs/wordcountProofScript.sml
  90. +3 −3 examples/diffScript.sml
  91. +1 −1 examples/divScript.sml
  92. +2 −2 examples/grepProgScript.sml
  93. +4 −2 misc/miscScript.sml
  94. +2 −1 semantics/alt_semantics/proofs/interpScript.sml
  95. +4 −2 semantics/cmlPtreeConversionScript.sml
  96. +3 −3 semantics/gramScript.sml
  97. +3 −2 semantics/proofs/cmlPtreeConversionPropsScript.sml
  98. +3 −3 semantics/proofs/semanticPrimitivesPropsScript.sml
  99. +2 −1 semantics/proofs/typeSysPropsScript.sml
  100. +1 −1 translator/ml_translatorScript.sml
  101. +5 −5 translator/monadic/cfMonadLib.sml
  102. +1 −2 translator/monadic/examples/array_global_stateProgScript.sml
  103. +1 −1 translator/monadic/examples/array_local_stateProgScript.sml
  104. +2 −2 translator/monadic/examples/exceptionProgScript.sml
  105. +2 −2 translator/monadic/examples/exception_arity_testProgScript.sml
  106. +1 −1 translator/monadic/examples/test_assumProgScript.sml
  107. +1 −1 translator/monadic/examples/test_precondProgScript.sml
  108. +1 −1 translator/monadic/examples/test_runScript.sml
  109. +6 −7 translator/monadic/ml_monad_translatorScript.sml
  110. +4 −4 translator/monadic/ml_monad_translator_interfaceLib.sml
  111. +4 −4 translator/monadic/monad_base/ml_monadBaseScript.sml
  112. +2 −2 translator/other-examples/auxiliary/regexpMatchScript.sml
@@ -195,8 +195,8 @@ val stdo_def = Define`
(ALOOKUP fs.infds fd = SOME(UStream(strlit name),WriteMode,strlen out) /\
ALOOKUP fs.inode_tbl (UStream(strlit name)) = SOME (explode out))`;

val _ = overload_on("stdout",``stdo 1 "stdout"``);
val _ = overload_on("stderr",``stdo 2 "stderr"``);
Overload stdout = ``stdo 1 "stdout"``
Overload stderr = ``stdo 2 "stderr"``

Theorem stdo_UNICITY_R[xlet_auto_match]:
!fd name fs out out'. stdo fd name fs out ==> (stdo fd name fs out' <=> out = out')
@@ -206,8 +206,9 @@ QED

val up_stdo_def = Define
`up_stdo fd fs out = fsupdate fs fd 0 (strlen out) (explode out)`
val _ = overload_on("up_stdout",``up_stdo 1``);
val _ = overload_on("up_stderr",``up_stdo 2``);

Overload up_stdout = ``up_stdo 1``;
Overload up_stderr = ``up_stdo 2``;

Theorem stdo_numchars:
stdo fd name (fs with numchars := l) out ⇔ stdo fd name fs out
@@ -250,8 +251,9 @@ QED

val add_stdo_def = Define`
add_stdo fd nm fs out = up_stdo fd fs ((@init. stdo fd nm fs init) ^ out)`;
val _ = overload_on("add_stdout",``add_stdo 1 "stdout"``);
val _ = overload_on("add_stderr",``add_stdo 2 "stderr"``);

Overload add_stdout = ``add_stdo 1 "stdout"``
Overload add_stderr = ``add_stdo 2 "stderr"``

Theorem stdo_add_stdo:
stdo fd nm fs init ⇒ stdo fd nm (add_stdo fd nm fs out) (strcat init out)
@@ -146,6 +146,6 @@ Proof
`n1 MOD 256 = n1` by fs[] >> `n2 MOD 256 = n2` by fs[] >> fs[]
QED

val _ = overload_on("WORD8",``WORD:word8 -> v -> bool``);
Overload WORD8 = ``WORD:word8 -> v -> bool``

val _ = export_theory()
@@ -217,8 +217,9 @@ val extract_stdo_def = Define`
MAP (CHR o w2n o FST) (TAKE (w2n(SND(HD(TL bytes)))) (DROP 3 bytes))
++ extract_stdo fd xs
else extract_stdo fd xs)`
val _ = overload_on("extract_stdout",``extract_stdo stdOut``);
val _ = overload_on("extract_stderr",``extract_stdo stdErr``);
Overload extract_stdout = ``extract_stdo stdOut``
Overload extract_stderr = ``extract_stdo stdErr``
Theorem extract_stdo_extract_fs
`∀io_events fs init out ll.
@@ -285,8 +286,9 @@ val _ = export_rewrites["extract_write_def"];
val extract_writes_def = Define
`extract_writes fd io_events =
FLAT (MAP extract_write (FILTER (is_write fd) io_events))`;
val _ = overload_on("extract_stdout",``extract_writes 1w``);
val _ = overload_on("extract_stderr",``extract_writes 2w``);
Overload extract_stdout = ``extract_writes 1w``
Overload extract_stderr = ``extract_writes 2w``;
Theorem extract_writes_thm
`extract_fs init_fs io_events = SOME fs ∧
@@ -18,7 +18,7 @@ QED

(* we can actually open a file if the OS limit has not been reached and we can
* still encode the file descriptor on 8 bits *)
val _ = overload_on("hasFreeFD",``λfs. CARD (set (MAP FST fs.infds)) < MIN fs.maxFD (256**8)``);
Overload hasFreeFD = ``λfs. CARD (set (MAP FST fs.infds)) < MIN fs.maxFD (256**8)``

(* nextFD lemmas *)

@@ -1006,8 +1006,8 @@ val lines_of_def = Define `

(* all_lines_inode: get all the lines based on an inode *)

val _ = overload_on("all_lines_inode",
``λfs ino. lines_of (implode (THE (ALOOKUP fs.inode_tbl ino)))``)
Overload all_lines_inode =
``λfs ino. lines_of (implode (THE (ALOOKUP fs.inode_tbl ino)))``

(* all_lines: get all the lines based on filename *)

@@ -1409,9 +1409,10 @@ Proof
\\ metis_tac[]
QED

val _ = overload_on("hard_link",
``λfs fn1 fn2. ∃ino. ALOOKUP fs.files fn1 = SOME ino ∧
ALOOKUP fs.files fn2 = SOME ino``);
Overload hard_link =
``λfs fn1 fn2. ∃ino. ALOOKUP fs.files fn1 = SOME ino ∧
ALOOKUP fs.files fn2 = SOME ino``

val pipe_def = Define`
pipe fs (fdin, fdout) c =
(∃ ino ipos. ALOOKUP fs.infds fdin = SOME (UStream ino, ReadMode, ipos) ∧
@@ -13,7 +13,7 @@ val _ = option_monadsyntax.temp_add_option_monadsyntax();
(* regular files and unnamed streams *)
val _ = Datatype` inode = UStream mlstring | File mlstring`

val _ = overload_on("isFile",``λinode. ∃fnm. inode = File fnm``);
Overload isFile = ``λinode. ∃fnm. inode = File fnm``

val _ = Datatype` mode = ReadMode | WriteMode`;

@@ -127,7 +127,8 @@ Proof
QED

val num_to_str_def = Define `num_to_str (n:num) = toString (&n)`;
val _ = overload_on("toString",``num_to_str``);

Overload toString = ``num_to_str``

Theorem num_to_str_thm:
num_to_str n = implode (num_to_dec_string n)
@@ -169,7 +169,7 @@ QED

val strcat_def = Define`strcat s1 s2 = concat [s1; s2]`
val _ = Parse.add_infix("^",480,Parse.LEFT)
val _ = Parse.overload_on("^",``λx y. strcat x y``)
Overload "^" = ``λx y. strcat x y``

Theorem concat_cons:
concat (h::t) = strcat h (concat t)
@@ -641,24 +641,25 @@ val compare_def = Define`

val mlstring_lt_def = Define `
mlstring_lt s1 s2 ⇔ (compare s1 s2 = LESS)`;
val _ = Parse.overload_on("<",``λx y. mlstring_lt x y``);

val mlstring_le_def = Define `
mlstring_le s1 s2 ⇔ (compare s1 s2 ≠ GREATER)`;
val _ = Parse.overload_on("<=",``λx y. mlstring_le x y``);

val mlstring_gt_def = Define `
mlstring_gt s1 s2 ⇔ (compare s1 s2 = GREATER)`;
val _ = Parse.overload_on(">",``λx y. mlstring_gt x y``);

val mlstring_ge_def = Define `
mlstring_ge s1 s2 ⇔ (compare s1 s2 <> LESS)`;
val _ = Parse.overload_on(">=",``λx y. mlstring_ge x y``);

Overload "<" = ``λx y. mlstring_lt x y``
Overload "<=" = ``λx y. mlstring_le x y``
Overload ">" = ``λx y. mlstring_gt x y``
Overload ">=" = ``λx y. mlstring_ge x y``

(* Properties of string orderings *)

val flip_ord_def = ternaryComparisonsTheory.invert_comparison_def
val _ = overload_on ("flip_ord", ``invert_comparison``);
Overload flip_ord = ``invert_comparison``

val compare_aux_spec = Q.prove (
`!s1 s2 ord_in start len.
@@ -18,7 +18,7 @@ val _ = Parse.hide "mem";
val mem = ``mem:'U->'U->bool``

val _ = Parse.add_infix("<:",425,Parse.NONASSOC)
val _ = Parse.overload_on("<:",mem)
Overload "<:" = ``mem:'U->'U->bool``

val extensional_def = Define`
extensional ^mem ⇔ ∀x y. x = y ⇔ ∀a. mem a x ⇔ mem a y`
@@ -114,9 +114,9 @@ Proof
QED

val _ = Parse.add_infix("suchthat",9,Parse.LEFT)
val _ = Parse.overload_on("suchthat",``sub ^mem``)
val _ = Parse.overload_on("Pow",``power ^mem``)
val _ = Parse.overload_on("+",``upair ^mem``)
Overload suchthat = ``sub ^mem``
Overload Pow = ``power ^mem``
Overload "+" = ``upair ^mem``

Theorem mem_sub:
is_set_theory ^mem ⇒ ∀x s P. x <: (s suchthat P) ⇔ x <: s ∧ P x
@@ -147,7 +147,7 @@ QED
val empty_def = Define`
empty ^mem = sub mem ARB (K F)`

val _ = Parse.overload_on("",``empty ^mem``)
Overload "" = ``empty ^mem``

Theorem mem_empty:
is_set_theory ^mem ⇒ ∀x. ¬(x <: ∅)
@@ -159,7 +159,7 @@ QED
val unit_def = Define`
unit ^mem x = x + x`

val _ = Parse.overload_on("Unit",``unit ^mem``)
Overload Unit = ``unit ^mem``

Theorem mem_unit:
is_set_theory ^mem ⇒
@@ -182,7 +182,7 @@ QED
val one_def = Define`
one ^mem = Unit ∅`

val _ = Parse.overload_on("One",``one ^mem``)
Overload One = ``one ^mem``

Theorem mem_one:
is_set_theory ^mem ⇒
@@ -194,7 +194,7 @@ QED
val two_def = Define`
two ^mem = ∅ + One`

val _ = Parse.overload_on("Two",``two ^mem``)
Overload Two = ``two ^mem``

Theorem mem_two:
is_set_theory ^mem ⇒
@@ -206,7 +206,7 @@ QED
val pair_def = Define`
pair ^mem x y = (Unit x) + (x + y)`

val _ = Parse.overload_on(",",``pair ^mem``)
Overload "," = ``pair ^mem``

Theorem upair_inj:
is_set_theory ^mem ⇒
@@ -240,7 +240,7 @@ QED
val binary_union_def = Define`
binary_union ^mem x y = union mem (upair mem x y)`

val _ = Parse.overload_on("UNION",``binary_union ^mem``)
Overload UNION = ``binary_union ^mem``

Theorem mem_binary_union:
is_set_theory ^mem ⇒
@@ -255,7 +255,7 @@ val product_def = Define`
(Pow (Pow (x ∪ y)) suchthat
λa. ∃b c. b <: x ∧ c <: y ∧ a = (b,c))`

val _ = Parse.overload_on("CROSS",``product ^mem``)
Overload CROSS = ``product ^mem``

Theorem mem_product:
is_set_theory ^mem ⇒
@@ -271,30 +271,30 @@ QED
val relspace_def = Define`
relspace ^mem x y = Pow (x × y)`

val _ = Parse.overload_on("Relspace",``relspace ^mem``)
Overload Relspace = ``relspace ^mem``

val funspace_def = Define`
funspace ^mem x y =
(Relspace x y suchthat
λf. ∀a. a <: x ⇒ ∃!b. (a,b) <: f)`

val _ = Parse.overload_on("Funspace",``funspace ^mem``)
Overload Funspace = ``funspace ^mem``

val apply_def = Define`
apply ^mem x y = @a. (y,a) <: x`

val _ = Parse.overload_on("'",``apply ^mem``)
Overload "'" = ``apply ^mem``

val _ = Parse.overload_on("boolset",``Two``)
Overload boolset = ``Two``

val true_def = Define`
true ^mem = ∅`

val false_def = Define`
false ^mem = One`

val _ = Parse.overload_on("True",``true ^mem``)
val _ = Parse.overload_on("False",``false ^mem``)
Overload True = ``true ^mem``
Overload False = ``false ^mem``

Theorem true_neq_false:
is_set_theory ^mem ⇒ True ≠ False
@@ -316,7 +316,7 @@ QED
val boolean_def = Define`
boolean ^mem b = if b then True else False`

val _ = Parse.overload_on("Boolean",``boolean ^mem``)
Overload Boolean = ``boolean ^mem``

Theorem boolean_in_boolset:
is_set_theory ^mem ⇒
@@ -335,12 +335,12 @@ QED
val holds_def = Define`
holds ^mem s x ⇔ s ' x = True`

val _ = Parse.overload_on("Holds",``holds ^mem``)
Overload Holds = ``holds ^mem``

val abstract_def = Define`
abstract ^mem dom rng f = (dom × rng suchthat λx. ∃a. x = (a,f a))`

val _ = Parse.overload_on("Abstract",``abstract ^mem``)
Overload Abstract = ``abstract ^mem``

Theorem apply_abstract:
is_set_theory ^mem ⇒
@@ -441,7 +441,7 @@ val indset = ``indset:'U``
val ch = ``ch:'U->'U``
val s = ``(^mem,^indset,^ch)``

val _ = Parse.overload_on("M",s)
Overload M = ``(^mem,^indset,^ch)``

val is_choice_def = Define`
is_choice ^mem ch = ∀x. (∃a. a <: x) ⇒ ch x <: x`
@@ -479,7 +479,7 @@ QED
val tuple_def = Define`
(tuple0 ^mem [] = ∅) ∧
(tuple0 ^mem (a::as) = (a, tuple0 ^mem as))`
val _ = Parse.overload_on("tuple",``tuple0 ^mem``)
Overload tuple = ``tuple0 ^mem``

Theorem pair_not_empty:
is_set_theory ^mem ⇒ (x,y) ≠ ∅
@@ -512,7 +512,7 @@ QED
val bigcross_def = Define`
(bigcross0 ^mem [] = One) ∧
(bigcross0 ^mem (a::as) = a × (bigcross0 ^mem as))`
val _ = Parse.overload_on("bigcross",``bigcross0 ^mem``)
Overload bigcross = ``bigcross0 ^mem``

Theorem mem_bigcross:
is_set_theory ^mem ⇒

0 comments on commit eaaffc1

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