From a151eb936bada5ffaad4dc07b4d3f508c67c8cc2 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Fri, 20 Feb 2026 01:08:58 +0800 Subject: [PATCH 01/14] Replace simpleSexp with mlsexp in fromSexpScript Rewrite compiler/parsing/fromSexpScript.sml to use mlsexp (Atom/Expr) from basis/pure instead of simpleSexp from HOL4's context-free examples. This is Phase 1 of eliminating simpleSexp from CakeML. Key changes: - Ancestor: mlsexp replaces simpleSexpParse - Holmakefile: INCLUDES basis/pure instead of HOL4 context-free - Encoding: SX_SYM/SX_NUM/SX_STR/SX_CONS replaced by Atom/Expr - listsexp xs = Expr xs (trivial, lists are native) - dstrip_sexp extracts tag + args from Expr (Atom tag :: args) - All roundtrip proofs (encoder/decoder bijection) updated - dstrip_sexp_SOME uses strlit nm form for efficient gvs resolution Co-Authored-By: Claude Opus 4.6 --- compiler/parsing/Holmakefile | 2 +- compiler/parsing/fromSexpScript.sml | 1923 ++++++++++++--------------- 2 files changed, 835 insertions(+), 1090 deletions(-) diff --git a/compiler/parsing/Holmakefile b/compiler/parsing/Holmakefile index 28e93b3ca5..a0239f72f3 100644 --- a/compiler/parsing/Holmakefile +++ b/compiler/parsing/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\ +INCLUDES = $(CAKEMLDIR)/basis/pure \ $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics \ $(CAKEMLDIR)/semantics/proofs diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml index b01cea3072..844dc86df7 100644 --- a/compiler/parsing/fromSexpScript.sml +++ b/compiler/parsing/fromSexpScript.sml @@ -2,13 +2,13 @@ Definitions of functions for conversion between an S-expression encoding of the CakeML abstract syntax and the abstract syntax type itself. - The S-expressions are parsed as *per* the PEG in HOL’s - `examples/formal-language/context-free/simpleSexpPEGScript.sml`. + The S-expressions use the mlsexp type (Atom mlstring | Expr (sexp list)) + from basis/pure/mlsexpScript.sml. *) Theory fromSexp Ancestors - simpleSexp ast location[qualified] fpSem - quantHeuristics ASCIInumbers numposrep mlstring + mlsexp mlint mlstring ast location[qualified] fpSem + quantHeuristics ASCIInumbers numposrep Libs preamble match_goal @@ -43,63 +43,6 @@ Proof \\ Cases_on`y`\\fs[] \\ Cases_on`z`\\fs[] QED -Theorem FOLDR_SX_CONS_INJ: - ∀l1 l2. FOLDR SX_CONS nil l1 = FOLDR SX_CONS nil l2 ⇔ l1 = l2 -Proof - Induct \\ simp[] - >- ( Induct \\ simp[] ) - \\ gen_tac \\ Induct \\ simp[] -QED - -Theorem strip_sxcons_11: - ∀s1 s2 x. strip_sxcons s1 = SOME x ∧ strip_sxcons s2 = SOME x ⇒ s1 = s2 -Proof - ho_match_mp_tac simpleSexpTheory.strip_sxcons_ind - \\ ntac 4 strip_tac - \\ simp[Once simpleSexpTheory.strip_sxcons_def] - \\ CASE_TAC \\ fs[] \\ strip_tac \\ rveq \\ fs[] - \\ pop_assum mp_tac - \\ simp[Once simpleSexpTheory.strip_sxcons_def] - \\ CASE_TAC \\ fs[] \\ strip_tac \\ rveq \\ fs[] -QED - -Theorem dstrip_sexp_size: - ∀s sym args. dstrip_sexp s = SOME (sym, args) ⇒ - ∀e. MEM e args ⇒ sexp_size e < sexp_size s -Proof - Induct >> simp[dstrip_sexp_def, sexp_size_def] >> - rename1 `sexp_CASE sxp` >> Cases_on `sxp` >> simp[] >> rpt strip_tac >> - rename1 `MEM sxp0 sxpargs` >> rename1 `strip_sxcons sxp'` >> - `sxMEM sxp0 sxp'` by metis_tac[sxMEM_def] >> imp_res_tac sxMEM_sizelt >> - simp[] -QED - -Theorem dstrip_sexp_SOME: - dstrip_sexp s = SOME x ⇔ - ∃sym sa args. s = - SX_CONS (SX_SYM sym) sa ∧ - strip_sxcons sa = SOME args ∧ - (x = (sym,args)) -Proof - Cases_on`s`>>simp[dstrip_sexp_def]>> - every_case_tac>>simp[] -QED - -Theorem strip_sxcons_SOME_NIL[simp]: - strip_sxcons s = SOME [] ⇔ s = nil -Proof - rw[Once strip_sxcons_def] >> - every_case_tac >> simp[] -QED - -Theorem strip_sxcons_EQ_CONS[simp]: - strip_sxcons s = SOME (h::t) ⇔ - ∃s0. s = SX_CONS h s0 ∧ strip_sxcons s0 = SOME t -Proof - simp[Once strip_sxcons_def] >> every_case_tac >> simp[] >> - metis_tac[] -QED - val type_ind = (TypeBase.induction_of``:ast_t``) |> Q.SPECL[`P`,`EVERY P`] @@ -272,126 +215,205 @@ Proof metis_tac[isLower_isAlpha, isAlpha_isUpper_isLower] QED +Theorem encode_control_remove: + ∀s. EVERY isPrint s ∧ #"\\" ∉ set s ⇒ encode_control s = s +Proof + Induct \\ simp[encode_control_def] +QED + +(* --- mlsexp-based encoding/decoding helpers --- *) + +(* Encode a string with control char escaping *) Definition SEXSTR_def: - SEXSTR s = SX_STR (encode_control s) + SEXSTR s = Atom (implode (encode_control s)) End Theorem SEXSTR_11[simp]: SEXSTR s1 = SEXSTR s2 ⇔ s1 = s2 Proof rw[SEXSTR_def] - \\ metis_tac[decode_encode_control,SOME_11] + \\ metis_tac[decode_encode_control,SOME_11,explode_implode] QED -Theorem SEXSTR_distinct[simp]: - (SEXSTR s ≠ SX_SYM sym) ∧ - (SEXSTR s ≠ SX_NUM num) ∧ - (SEXSTR s ≠ SX_CONS a d) ∧ - ((SEXSTR s = SX_STR s') ⇔ s' = encode_control s) +(* Encode a natural number *) +Definition SXNUM_def: + SXNUM (n:num) = Atom (toString (&n)) +End + +Theorem SXNUM_11[simp]: + SXNUM n1 = SXNUM n2 ⇔ n1 = n2 Proof - rw[SEXSTR_def,EQ_IMP_THM] + simp[SXNUM_def, mlintTheory.num_to_str_11] QED +(* Decode a string with control char unescaping *) Definition odestSEXSTR_def[simp]: - (odestSEXSTR (SX_STR s) = OPTION_MAP implode (decode_control s)) ∧ - (odestSEXSTR _ = NONE) + (odestSEXSTR (Atom s) = OPTION_MAP implode (decode_control (explode s))) ∧ + (odestSEXSTR (Expr _) = NONE) End -Theorem encode_control_remove: - ∀s. EVERY isPrint s ∧ #"\\" ∉ set s ⇒ encode_control s = s +(* Decode a symbol/tag (raw mlstring) *) +Definition odestSXSYM_def[simp]: + (odestSXSYM (Atom s) = SOME s) ∧ + (odestSXSYM (Expr _) = NONE) +End + +(* Decode a natural number *) +Definition odestSXNUM_def[simp]: + (odestSXNUM (Atom s) = + (case fromString s of + | SOME i => if 0 ≤ i ∧ toString i = s then SOME (Num i) else NONE + | NONE => NONE)) ∧ + (odestSXNUM (Expr _) = NONE) +End + +(* Decode an integer *) +Definition odestSXINT_def[simp]: + (odestSXINT (Atom s) = + (case fromString s of + | SOME i => if toString i = s then SOME i else NONE + | NONE => NONE)) ∧ + (odestSXINT (Expr _) = NONE) +End + +Theorem odestSXNUM_SXNUM[simp]: + odestSXNUM (SXNUM n) = SOME n Proof - Induct \\ simp[encode_control_def] + simp[SXNUM_def,odestSXNUM_def,num_to_str_def,fromString_toString] QED -Theorem SEXSTR_remove: - EVERY isPrint s ∧ #"\\" ∉ set s ⇒ SEXSTR s = SX_STR s +Theorem odestSXINT_SXINT[simp]: + odestSXINT (Atom (toString i)) = SOME i Proof - rw[SEXSTR_def,encode_control_remove] + simp[odestSXINT_def, fromString_toString] QED -Definition odestSXSTR_def[simp]: - (odestSXSTR (SX_STR s) = SOME (implode s)) ∧ - (odestSXSTR _ = NONE) -End +Theorem odestSEXSTR_SEXSTR[simp]: + odestSEXSTR (SEXSTR s) = SOME (implode s) +Proof + simp[SEXSTR_def,odestSEXSTR_def] +QED -Definition odestSXSYM_def[simp]: - (odestSXSYM (SX_SYM s) = SOME (implode s)) ∧ - (odestSXSYM _ = NONE) +(* Lists: Expr wraps a list directly *) +Definition listsexp_def: + listsexp xs = Expr xs End -Definition odestSXNUM_def[simp]: - (odestSXNUM (SX_NUM n) = SOME n) ∧ - (odestSXNUM _ = NONE) -End +Theorem listsexp_thm[simp]: + listsexp [] = Expr [] ∧ listsexp (h::t) = Expr (h :: t) +Proof + simp[listsexp_def] +QED -Theorem odestSXNUM_SEXSTR[simp]: - odestSXNUM (SEXSTR strng) = NONE +Theorem listsexp_11[simp]: + ∀ l1 l2. listsexp l1 = listsexp l2 ⇔ l1 = l2 Proof - simp[SEXSTR_def] + simp[listsexp_def] QED -Definition sexpopt_def: - sexpopt p s = - do - nm <- odestSXSYM s ; - assert(nm = «NONE»); - return NONE - od ++ - do - (nm,args) <- dstrip_sexp s; - assert(nm = "SOME" ∧ LENGTH args = 1); - lift SOME (p (HD args)) - od +(* Extract tag + args from (Tag arg1 arg2 ...) *) +Definition dstrip_sexp_def[simp]: + dstrip_sexp (Expr (Atom tag :: args)) = SOME (explode tag, args) ∧ + dstrip_sexp _ = NONE End +Theorem dstrip_sexp_size: + ∀s sym args. dstrip_sexp s = SOME (sym, args) ⇒ + ∀e. MEM e args ⇒ sexp_size e < sexp_size s +Proof + Cases >> simp[dstrip_sexp_def] >> + rename1 `Expr l` >> + Cases_on `l` >> simp[dstrip_sexp_def] >> + rename1 `h :: t` >> Cases_on `h` >> simp[dstrip_sexp_def] >> + rw[] >> gvs[sexp_size_def] >> + `sexp_size e <= list_size sexp_size t` by metis_tac[MEM_list_size] >> + simp[] +QED + +Theorem explode_eq: + (explode tag = s ⇔ tag = strlit s) ∧ + (s = explode tag ⇔ strlit s = tag) +Proof + simp[mlstringTheory.implode_def, EQ_IMP_THM] >> + metis_tac[mlstringTheory.implode_explode, mlstringTheory.explode_implode, + mlstringTheory.implode_def] +QED + +Theorem dstrip_sexp_SOME: + dstrip_sexp s = SOME x ⇔ + ∃nm args. s = Expr (Atom (strlit nm) :: args) ∧ x = (nm, args) +Proof + Cases_on `s` >> simp[dstrip_sexp_def] >> + Cases_on `l` >> simp[dstrip_sexp_def] >> + Cases_on `h` >> simp[dstrip_sexp_def] >> + rw[EQ_IMP_THM] >> gvs[explode_eq] >> + metis_tac[mlstringTheory.implode_explode, mlstringTheory.implode_def] +QED + +Theorem dstrip_sexp_listsexp[simp]: + (dstrip_sexp (listsexp ls) = + case ls of (Atom x :: xs) => SOME (explode x, xs) | _ => NONE) +Proof + Cases_on `ls` >> simp[dstrip_sexp_def,listsexp_def] >> + Cases_on `h` >> simp[dstrip_sexp_def] +QED + +Theorem dstrip_sexp_SEXSTR[simp]: + dstrip_sexp (SEXSTR s) = NONE +Proof + simp[SEXSTR_def,dstrip_sexp_def] +QED + +Theorem dstrip_sexp_SXNUM[simp]: + dstrip_sexp (SXNUM n) = NONE +Proof + simp[SXNUM_def,dstrip_sexp_def] +QED + +(* Decode list *) Definition sexplist_def: - sexplist p s = - case s of - SX_CONS h t => - do - ph <- p h; - pt <- sexplist p t; - return (ph::pt) - od - | SX_SYM s => if s = "nil" then return [] else fail - | _ => fail + sexplist p (Atom _) = NONE ∧ + sexplist p (Expr []) = SOME [] ∧ + sexplist p (Expr (h::t)) = + do + ph <- p h; + pt <- sexplist p (Expr t); + return (ph::pt) + od +Termination + wf_rel_tac `measure (sexp_size o SND)` >> + simp[sexp_size_def] End Theorem sexplist_thm[simp]: - sexplist p (SX_CONS h t) = - do ph <- p h ; pt <- sexplist p t; return (ph::pt) od ∧ - (sexplist p (SX_SYM s) = if s = "nil" then return [] else fail) ∧ - sexplist p (&n) = fail ∧ - sexplist p (SX_STR strng) = fail + sexplist p (Atom a) = NONE ∧ + sexplist p (Expr []) = SOME [] ∧ + sexplist p (Expr (h::t)) = + do ph <- p h ; pt <- sexplist p (Expr t); return (ph::pt) od Proof rpt strip_tac >> simp[Once sexplist_def] QED +(* Decode pair from 2-element Expr *) Definition sexppair_def: sexppair p1 p2 s = case s of - SX_CONS s1 s2 => lift2 (,) (p1 s1) (p2 s2) + Expr [s1; s2] => lift2 (,) (p1 s1) (p2 s2) | _ => fail End Theorem sexppair_CONG[defncong]: ∀s1 s2 p1 p1' p2 p2'. s1 = s2 ∧ - (∀s. (∃s'. s2 = SX_CONS s s') ⇒ p1 s = p1' s) ∧ - (∀s. (∃s'. s2 = SX_CONS s' s) ⇒ p2 s = p2' s) + (∀s. (∃s'. s2 = Expr [s; s']) ⇒ p1 s = p1' s) ∧ + (∀s. (∃s'. s2 = Expr [s'; s]) ⇒ p2 s = p2' s) ⇒ sexppair p1 p2 s1 = sexppair p1' p2' s2 Proof - simp[] >> Cases >> simp[sexppair_def] + rw[sexppair_def] >> every_case_tac >> gvs[] QED - -Theorem strip_sxcons_FAIL_sexplist_FAIL: - ∀s. (strip_sxcons s = NONE) ⇒ (sexplist p s = NONE) -Proof - Induct >> simp[Once sexplist_def] >> - metis_tac[TypeBase.nchotomy_of ``:α option``] -QED +Overload guard[local] = ``λb m. monad_unitbind (assert b) m`` Theorem monad_bind_FAIL: monad_bind m1 (λx. fail) = fail @@ -408,28 +430,60 @@ Proof Cases_on `m12` >> simp[] QED -Theorem strip_sxcons_thm[simp]: - strip_sxcons ⟪ h • t ⟫ = lift (CONS h) (strip_sxcons t) ∧ - strip_sxcons (&n) = NONE ∧ - strip_sxcons (SX_STR strng) = NONE ∧ - strip_sxcons (SX_SYM s) = if s = "nil" then SOME [] else NONE -Proof - rpt strip_tac >> simp[] -QED - Theorem sexplist_CONG[defncong]: ∀s1 s2 p1 p2. - s1 = s2 ∧ (∀e. sxMEM e s2 ⇒ p1 e = p2 e) ⇒ + s1 = s2 ∧ (∀e xs. s2 = Expr xs ∧ MEM e xs ⇒ p1 e = p2 e) ⇒ sexplist p1 s1 = sexplist p2 s2 Proof - simp[sxMEM_def, PULL_EXISTS] >> Induct >> simp[PULL_EXISTS] >> dsimp[] >> - rename [‘strip_sxcons s2 = SOME _’] >> Cases_on ‘strip_sxcons s2’ >> gvs[] - >- simp[monad_bind_FAIL, strip_sxcons_FAIL_sexplist_FAIL] >> - rpt strip_tac >> simp[] >> first_x_assum dxrule >> simp[] + simp[] >> Induct_on `s2` >> simp[] >> + Induct_on `l` >> rw[] >> simp[Once sexplist_def] >> + `p1 h = p2 h` by gvs[] >> + `sexplist p1 (Expr l) = sexplist p2 (Expr l)` + by (first_x_assum irule >> rw[]) >> + simp[] QED -Overload guard[local] = ``λb m. monad_unitbind (assert b) m`` +Theorem sexpMEM_sizelt: + ∀s xs e. s = Expr xs ∧ MEM e xs ⇒ sexp_size e < sexp_size s +Proof + rw[sexp_size_def] >> + Induct_on `xs` >> simp[sexp_size_def] >> rw[] >> res_tac >> simp[] +QED +Theorem sexpMEM_sizelt': + ∀xs a. MEM a xs ⇒ sexp_size a < sexp_size (Expr xs) +Proof + Induct >> rw[sexp_size_def] >> res_tac >> fs[sexp_size_def] +QED + +Theorem dstrip_sexp_sexpMEM_size: + ∀s nm args i xs a. dstrip_sexp s = SOME (nm, args) ∧ + i < LENGTH args ∧ EL i args = Expr xs ∧ MEM a xs ⇒ + sexp_size a < sexp_size s +Proof + rw[] >> + `sexp_size a < sexp_size (Expr xs)` by metis_tac[sexpMEM_sizelt'] >> + `sexp_size (EL i args) < sexp_size s` + by (irule dstrip_sexp_size >> metis_tac[MEM_EL]) >> + gvs[] +QED + +(* Decode optional *) +Definition sexpopt_def: + sexpopt p s = + do + nm <- odestSXSYM s ; + assert(nm = «NONE»); + return NONE + od ++ + do + (nm,args) <- dstrip_sexp s; + assert(nm = "SOME" ∧ LENGTH args = 1); + lift SOME (p (HD args)) + od +End + +(* Decode identifiers *) Definition sexpid_def: sexpid p s = do @@ -441,9 +495,12 @@ Definition sexpid_def: od Termination wf_rel_tac `measure (sexp_size o SND)` >> - simp[dstrip_sexp_SOME, LENGTH_EQ_NUM_compute, PULL_EXISTS, sexp_size_def] + rw[] >> imp_res_tac dstrip_sexp_size >> + gvs[LENGTH_EQ_NUM_compute] End +(* --- Decoder functions --- *) + Definition sexptype_def: sexptype s = do @@ -460,8 +517,9 @@ Definition sexptype_def: od Termination wf_rel_tac `measure sexp_size` >> - simp[LENGTH_EQ_NUM_compute, dstrip_sexp_SOME, PULL_EXISTS, sexp_size_def] >> - rpt strip_tac >> drule sxMEM_sizelt >> simp[] + rw[] >> imp_res_tac dstrip_sexp_size >> + imp_res_tac sexpMEM_sizelt' >> + gvs[LENGTH_EQ_NUM_compute, sexp_size_def, SF DNF_ss] End (* translator friendly version for bootstrapping *) @@ -481,38 +539,29 @@ Definition sexptype_alt_def: else NONE) ∧ (sexptype_list s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexptype_alt a of | NONE => NONE | SOME h => - case sexptype_list d of + case sexptype_list (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) + | SOME t => SOME (h::t))) Termination - wf_rel_tac‘inv_image (measure sexp_size) - (λx. case x of INL y => y | INR y => y)’ \\ rw[] \\ + wf_rel_tac`inv_image (measure sexp_size) + (λx. case x of INL y => y | INR y => y)` \\ rw[] \\ imp_res_tac dstrip_sexp_size \\ - fs[LENGTH_EQ_NUM_compute] + gvs[LENGTH_EQ_NUM_compute, sexp_size_def] End Theorem sexptype_alt_intro: (∀s. sexptype s = sexptype_alt s) ∧ ∀s. sexptype_list s = sexplist sexptype s Proof - ho_match_mp_tac sexptype_alt_ind \\ rw[] - >- ( - rw[Once sexptype_alt_def,Once sexptype_def] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - simp[monad_unitbind_assert] \\ - srw_tac[ETA_ss][] ) - >- ( - rw[Once sexplist_def,Once (CONJUNCT2 sexptype_alt_def)] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) + ho_match_mp_tac sexptype_alt_ind >> rw[] >> + simp[Once sexptype_def, Once sexptype_alt_def, Once sexplist_def] >> + every_case_tac >> gvs[ETA_THM] QED Theorem sexptype_alt_intro1: @@ -523,14 +572,12 @@ QED Definition sexplit_def: sexplit s = - lift (IntLit o (&)) (odestSXNUM s) ++ lift StrLit (odestSEXSTR s) ++ do (nm,args) <- dstrip_sexp s; assert(LENGTH args = 1); - guard (nm = "-") - (OPTION_BIND (odestSXNUM (HD args)) - (λn. if n = 0 then NONE else SOME (IntLit (-&n)))) ++ + guard (nm = "IntLit") + (lift IntLit (odestSXINT (HD args))) ++ guard (nm = "char") do cs <- odestSEXSTR (HD args); @@ -580,17 +627,11 @@ Definition sexppat_def: (lift2 Ptannot (sexppat (EL 0 args)) (sexptype (EL 1 args))) od Termination - WF_REL_TAC `measure sexp_size` >> simp[] >> rpt strip_tac - >- metis_tac[arithmeticTheory.LESS_TRANS, rich_listTheory.EL_MEM, - DECIDE ``1n < 2``, sxMEM_sizelt, dstrip_sexp_size] - >- metis_tac[arithmeticTheory.LESS_TRANS, rich_listTheory.EL_MEM, - DECIDE ``0n < 2``, sxMEM_sizelt, dstrip_sexp_size, - EL ] - >- metis_tac[arithmeticTheory.LESS_TRANS, rich_listTheory.EL_MEM, - DECIDE ``0n < 2``, sxMEM_sizelt, dstrip_sexp_size, - EL ] - >- metis_tac[rich_listTheory.EL_MEM, DECIDE ``0n < 1``, listTheory.EL, - dstrip_sexp_size] + WF_REL_TAC `measure sexp_size` >> + rw[] >> + imp_res_tac dstrip_sexp_size >> + imp_res_tac sexpMEM_sizelt' >> + gvs[LENGTH_EQ_NUM_compute, sexp_size_def, SF DNF_ss] End (* translator friendly version for bootstrapping *) @@ -617,19 +658,19 @@ Definition sexppat_alt_def: else NONE) ∧ (sexppat_list s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexppat_alt a of | NONE => NONE | SOME h => - case sexppat_list d of + case sexppat_list (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) + | SOME t => SOME (h::t))) Termination wf_rel_tac`inv_image (measure sexp_size) (λx. case x of INL y => y | INR y => y)` \\ rw[] \\ imp_res_tac dstrip_sexp_size \\ - fs[LENGTH_EQ_NUM_compute] + gvs[LENGTH_EQ_NUM_compute, sexp_size_def] End val sexppat_alt_ind = theorem"sexppat_alt_ind"; @@ -637,18 +678,9 @@ val sexppat_alt_ind = theorem"sexppat_alt_ind"; Theorem sexppat_alt_intro: (∀s. sexppat s = sexppat_alt s) ∧ (∀s. sexppat_list s = sexplist sexppat s) Proof - ho_match_mp_tac sexppat_alt_ind \\ rw[] - >- ( - rw[Once sexppat_alt_def,Once sexppat_def] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - simp[monad_unitbind_assert] \\ - srw_tac[ETA_ss][sexptype_alt_intro1] ) - >- ( - rw[Once sexplist_def,Once (CONJUNCT2 sexppat_alt_def)] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) + ho_match_mp_tac sexppat_alt_ind >> rw[] >> + simp[Once sexppat_def, Once sexppat_alt_def, Once sexplist_def] >> + every_case_tac >> gvs[ETA_THM, sexptype_alt_intro] QED Theorem sexppat_alt_intro1: @@ -670,155 +702,159 @@ Definition encode_thunk_mode_def: End Definition decode_test_def: - decode_test (SX_SYM s) = - (if s = "Equal" then SOME Equal else - if s = "Less" then SOME (Compare Lt) else - if s = "LessEq" then SOME (Compare Leq) else - if s = "Greater" then SOME (Compare Gt) else - if s = "GreaterEq" then SOME (Compare Geq) else - if s = "AltLess" then SOME (AltCompare Lt) else - if s = "AltLessEq" then SOME (AltCompare Leq) else - if s = "AltGreater" then SOME (AltCompare Gt) else - if s = "AltGreaterEq" then SOME (AltCompare Geq) else NONE) ∧ + decode_test (Atom s) = + (if s = «Equal» then SOME Equal else + if s = «Less» then SOME (Compare Lt) else + if s = «LessEq» then SOME (Compare Leq) else + if s = «Greater» then SOME (Compare Gt) else + if s = «GreaterEq» then SOME (Compare Geq) else + if s = «AltLess» then SOME (AltCompare Lt) else + if s = «AltLessEq» then SOME (AltCompare Leq) else + if s = «AltGreater» then SOME (AltCompare Gt) else + if s = «AltGreaterEq» then SOME (AltCompare Geq) else NONE) ∧ decode_test _ = NONE End Definition decode_prim_type_def: - decode_prim_type (SX_SYM s) = - (if s = "BoolT" then SOME BoolT else - if s = "IntT" then SOME IntT else - if s = "CharT" then SOME CharT else - if s = "StrT" then SOME StrT else - if s = "Word8T" then SOME $ WordT W8 else - if s = "Word64T" then SOME $ WordT W64 else - if s = "Float64T" then SOME Float64T else NONE) ∧ + decode_prim_type (Atom s) = + (if s = «BoolT» then SOME BoolT else + if s = «IntT» then SOME IntT else + if s = «CharT» then SOME CharT else + if s = «StrT» then SOME StrT else + if s = «Word8T» then SOME $ WordT W8 else + if s = «Word64T» then SOME $ WordT W64 else + if s = «Float64T» then SOME Float64T else NONE) ∧ decode_prim_type _ = NONE End Definition sexparith_def: - sexparith (SX_SYM s) = - (if s = "Add" then SOME Add else - if s = "Sub" then SOME Sub else - if s = "Mul" then SOME Mul else - if s = "Div" then SOME Div else - if s = "Mod" then SOME Mod else - if s = "Neg" then SOME Neg else - if s = "Abs" then SOME Abs else - if s = "And" then SOME And else - if s = "Xor" then SOME Xor else - if s = "Or" then SOME Or else - if s = "Not" then SOME Not else - if s = "Sqrt" then SOME Sqrt else - if s = "FMA" then SOME FMA else NONE) ∧ + sexparith (Atom s) = + (if s = «Add» then SOME Add else + if s = «Sub» then SOME Sub else + if s = «Mul» then SOME Mul else + if s = «Div» then SOME Div else + if s = «Mod» then SOME Mod else + if s = «Neg» then SOME Neg else + if s = «Abs» then SOME Abs else + if s = «And» then SOME And else + if s = «Xor» then SOME Xor else + if s = «Or» then SOME Or else + if s = «Not» then SOME Not else + if s = «Sqrt» then SOME Sqrt else + if s = «FMA» then SOME FMA else NONE) ∧ sexparith _ = NONE End Definition sexplog_def: - sexplog (SX_SYM s) = - (if s = "Andalso" then SOME Andalso else - if s = "Orelse" then SOME Orelse else NONE) ∧ + sexplog (Atom s) = + (if s = «Andalso» then SOME Andalso else + if s = «Orelse» then SOME Orelse else NONE) ∧ sexplog _ = NONE End Definition sexpop_def: - (sexpop (SX_SYM s) = - if s = "Equality" then SOME Equality else - if s = "Opapp" then SOME Opapp else - if s = "Opassign" then SOME Opassign else - if s = "Opref" then SOME Opref else - if s = "Opderef" then SOME Opderef else - if s = "Aw8alloc" then SOME Aw8alloc else - if s = "Aw8sub" then SOME Aw8sub else - if s = "Aw8length" then SOME Aw8length else - if s = "Aw8update" then SOME Aw8update else - if s = "Aw8subunsafe" then SOME Aw8sub_unsafe else - if s = "Aw8updateunsafe" then SOME Aw8update_unsafe else - if s = "CopyStrStr" then SOME CopyStrStr else - if s = "CopyStrAw8" then SOME CopyStrAw8 else - if s = "CopyAw8Str" then SOME CopyAw8Str else - if s = "CopyAw8Aw8" then SOME CopyAw8Aw8 else - if s = "XorAw8Strunsafe" then SOME XorAw8Str_unsafe else - if s = "Implode" then SOME Implode else - if s = "Explode" then SOME Explode else - if s = "Strsub" then SOME Strsub else - if s = "Strlen" then SOME Strlen else - if s = "Strcat" then SOME Strcat else - if s = "VfromList" then SOME VfromList else - if s = "Vsub" then SOME Vsub else - if s = "Vsub_unsafe" then SOME Vsub_unsafe else - if s = "Vlength" then SOME Vlength else - if s = "ListAppend" then SOME ListAppend else - if s = "Aalloc" then SOME Aalloc else - if s = "AallocEmpty" then SOME AallocEmpty else - if s = "AallocFixed" then SOME AallocFixed else - if s = "Asub" then SOME Asub else - if s = "Alength" then SOME Alength else - if s = "Aupdate" then SOME Aupdate else - if s = "Asubunsafe" then SOME Asub_unsafe else - if s = "Aupdateunsafe" then SOME Aupdate_unsafe else - if s = "ForceThunk" then SOME (ThunkOp ForceThunk) else - if s = "ConfigGC" then SOME ConfigGC else - if s = "Eval" then SOME Eval else - if s = "Envid" then SOME Env_id else NONE) ∧ - (sexpop (SX_CONS (SX_SYM s) (SX_STR s')) = - if s = "FFI" then OPTION_MAP (FFI ∘ implode) (decode_control s') else NONE - ) ∧ - (sexpop (SX_CONS (SX_SYM s) (SX_SYM t)) = - case decode_thunk_mode t of - | NONE => NONE - | SOME m => - if s = "AllocThunk" then SOME (ThunkOp (AllocThunk m)) else - if s = "UpdateThunk" then SOME (ThunkOp (UpdateThunk m)) else NONE - ) ∧ - (sexpop (SX_CONS (SX_SYM s) (SX_NUM n)) = - if s = "Shift8Lsl" then SOME (Shift W8 Lsl n) else - if s = "Shift8Lsr" then SOME (Shift W8 Lsr n) else - if s = "Shift8Asr" then SOME (Shift W8 Asr n) else - if s = "Shift8Ror" then SOME (Shift W8 Ror n) else - if s = "Shift64Lsl" then SOME (Shift W64 Lsl n) else - if s = "Shift64Lsr" then SOME (Shift W64 Lsr n) else - if s = "Shift64Asr" then SOME (Shift W64 Asr n) else - if s = "Shift64Ror" then SOME (Shift W64 Ror n) else NONE) ∧ - (sexpop (SX_CONS (SX_SYM s) (SX_CONS x y)) = - if s = "Arith" then - (case (sexparith x, decode_prim_type y) of - | (SOME a, SOME prim_type) => SOME (Arith a prim_type) - | _ => NONE) - else if s = "FromTo" then - (case (decode_prim_type x, decode_prim_type y) of - | (SOME ty1, SOME ty2) => SOME (FromTo ty1 ty2) - | _ => NONE) - else if s = "Test" then - (case (decode_test x, decode_prim_type y) of - | (SOME test, SOME prim_type) => SOME (Test test prim_type) - | _ => NONE) - else NONE) ∧ - (sexpop _ = NONE) + sexpop s = + case s of + | Atom a => + (if a = «Equality» then SOME Equality else + if a = «Opapp» then SOME Opapp else + if a = «Opassign» then SOME Opassign else + if a = «Opref» then SOME Opref else + if a = «Opderef» then SOME Opderef else + if a = «Aw8alloc» then SOME Aw8alloc else + if a = «Aw8sub» then SOME Aw8sub else + if a = «Aw8length» then SOME Aw8length else + if a = «Aw8update» then SOME Aw8update else + if a = «Aw8subunsafe» then SOME Aw8sub_unsafe else + if a = «Aw8updateunsafe» then SOME Aw8update_unsafe else + if a = «CopyStrStr» then SOME CopyStrStr else + if a = «CopyStrAw8» then SOME CopyStrAw8 else + if a = «CopyAw8Str» then SOME CopyAw8Str else + if a = «CopyAw8Aw8» then SOME CopyAw8Aw8 else + if a = «XorAw8Strunsafe» then SOME XorAw8Str_unsafe else + if a = «Implode» then SOME Implode else + if a = «Explode» then SOME Explode else + if a = «Strsub» then SOME Strsub else + if a = «Strlen» then SOME Strlen else + if a = «Strcat» then SOME Strcat else + if a = «VfromList» then SOME VfromList else + if a = «Vsub» then SOME Vsub else + if a = «Vsub_unsafe» then SOME Vsub_unsafe else + if a = «Vlength» then SOME Vlength else + if a = «ListAppend» then SOME ListAppend else + if a = «Aalloc» then SOME Aalloc else + if a = «AallocEmpty» then SOME AallocEmpty else + if a = «AallocFixed» then SOME AallocFixed else + if a = «Asub» then SOME Asub else + if a = «Alength» then SOME Alength else + if a = «Aupdate» then SOME Aupdate else + if a = «Asubunsafe» then SOME Asub_unsafe else + if a = «Aupdateunsafe» then SOME Aupdate_unsafe else + if a = «ForceThunk» then SOME (ThunkOp ForceThunk) else + if a = «ConfigGC» then SOME ConfigGC else + if a = «Eval» then SOME Eval else + if a = «Envid» then SOME Env_id else NONE) + | Expr [Atom tag; arg] => + (if tag = «FFI» then lift FFI (odestSEXSTR arg) else + if tag = «Shift8Lsl» then lift (Shift W8 Lsl) (odestSXNUM arg) else + if tag = «Shift8Lsr» then lift (Shift W8 Lsr) (odestSXNUM arg) else + if tag = «Shift8Asr» then lift (Shift W8 Asr) (odestSXNUM arg) else + if tag = «Shift8Ror» then lift (Shift W8 Ror) (odestSXNUM arg) else + if tag = «Shift64Lsl» then lift (Shift W64 Lsl) (odestSXNUM arg) else + if tag = «Shift64Lsr» then lift (Shift W64 Lsr) (odestSXNUM arg) else + if tag = «Shift64Asr» then lift (Shift W64 Asr) (odestSXNUM arg) else + if tag = «Shift64Ror» then lift (Shift W64 Ror) (odestSXNUM arg) else + if tag = «AllocThunk» then + (case arg of + | Atom a => + (case decode_thunk_mode (explode a) of + | SOME m => SOME (ThunkOp (AllocThunk m)) + | NONE => NONE) + | _ => NONE) else + if tag = «UpdateThunk» then + (case arg of + | Atom a => + (case decode_thunk_mode (explode a) of + | SOME m => SOME (ThunkOp (UpdateThunk m)) + | NONE => NONE) + | _ => NONE) else + NONE) + | Expr [Atom tag; arg1; arg2] => + (if tag = «Arith» then + (case (sexparith arg1, decode_prim_type arg2) of + | (SOME a, SOME prim_type) => SOME (Arith a prim_type) + | _ => NONE) else + if tag = «FromTo» then + (case (decode_prim_type arg1, decode_prim_type arg2) of + | (SOME ty1, SOME ty2) => SOME (FromTo ty1 ty2) + | _ => NONE) else + if tag = «Test» then + (case (decode_test arg1, decode_prim_type arg2) of + | (SOME test, SOME prim_type) => SOME (Test test prim_type) + | _ => NONE) else + NONE) + | _ => NONE End Definition sexplocpt_def: - (sexplocpt (SX_SYM s) = - if s = "unk" then SOME UNKNOWNpt - else if s = "eof" then SOME EOFpt - else NONE) ∧ - (sexplocpt s = - do - ls <- strip_sxcons s ; - guard (LENGTH ls = 2) (lift2 POSN - (odestSXNUM (EL 0 ls)) - (odestSXNUM (EL 1 ls))) - od) + sexplocpt (Atom s) = + (if s = «unk» then SOME UNKNOWNpt + else if s = «eof» then SOME EOFpt + else NONE) ∧ + sexplocpt (Expr ls) = + if LENGTH ls = 2 then + lift2 POSN (odestSXNUM (EL 0 ls)) (odestSXNUM (EL 1 ls)) + else NONE End Definition sexplocn_def: sexplocn s = - do - ls <- strip_sxcons s; - guard (LENGTH ls = 2) - (lift2 Locs - (sexplocpt (EL 0 ls)) - (sexplocpt (EL 1 ls))) - od + case s of + | Expr ls => + if LENGTH ls = 2 then + lift2 Locs (sexplocpt (EL 0 ls)) (sexplocpt (EL 1 ls)) + else NONE + | _ => NONE End Definition sexpexp_def: @@ -874,10 +910,10 @@ Definition sexpexp_def: od Termination WF_REL_TAC `measure sexp_size` >> - rw[]>> + rw[] >> imp_res_tac dstrip_sexp_size >> - imp_res_tac sxMEM_sizelt >> - gvs[sexp_size_def,DB.fetch "quantHeuristics" "LIST_LENGTH_3",SF DNF_ss] + imp_res_tac sexpMEM_sizelt' >> + gvs[LENGTH_EQ_NUM_compute, sexp_size_def, SF DNF_ss] End (* translator friendly version for bootstrapping *) @@ -940,50 +976,50 @@ Definition sexpexp_alt_def: else NONE) ∧ (sexpexp_list s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexpexp_alt a of | NONE => NONE | SOME h => - case sexpexp_list d of + case sexpexp_list (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) ∧ + | SOME t => SOME (h::t))) ∧ (sexppes s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexppatexp a of | NONE => NONE | SOME h => - case sexppes d of + case sexppes (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) ∧ + | SOME t => SOME (h::t))) ∧ (sexpfuns s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexpfun a of | NONE => NONE | SOME h => - case sexpfuns d of + case sexpfuns (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) ∧ + | SOME t => SOME (h::t))) ∧ (sexppatexp s = case s of - | SX_CONS a d => + | Expr [a; d] => (case (sexppat_alt a, sexpexp_alt d) of | (SOME p, SOME e) => SOME (p,e) | _ => NONE) | _ => NONE) ∧ (sexpfun s = case s of - | SX_CONS a d => + | Expr [a; d] => (case d of - | SX_CONS b d => - (case (odestSEXSTR a, odestSEXSTR b, sexpexp_alt d) of + | Expr [b; e] => + (case (odestSEXSTR a, odestSEXSTR b, sexpexp_alt e) of | (SOME x, SOME y, SOME z) => SOME (x,y,z) | _ => NONE) | _ => NONE) @@ -998,7 +1034,7 @@ Termination | INR (INR (INR (INR (INL y)))) => y | INR (INR (INR (INR (INR y)))) => y)` \\ rw[] \\ imp_res_tac dstrip_sexp_size \\ - fs[LENGTH_EQ_NUM_compute] + gvs[LENGTH_EQ_NUM_compute, sexp_size_def] End Theorem sexpexp_alt_intro: @@ -1009,49 +1045,27 @@ Theorem sexpexp_alt_intro: (∀s. sexppair sexppat sexpexp s = sexppatexp s) ∧ (∀s. sexppair odestSEXSTR (sexppair odestSEXSTR sexpexp) s = sexpfun s) Proof - ho_match_mp_tac sexpexp_alt_ind \\ rw[] - >- ( - rw[Once sexpexp_alt_def,Once sexpexp_def] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - simp[monad_unitbind_assert] \\ - rpt ( - IF_CASES_TAC >- ( - pop_assum strip_assume_tac \\ rveq \\ - full_simp_tac std_ss [] - \\ fsrw_tac[ETA_ss][sexptype_alt_intro1] ) \\ - simp[] ) ) - >- ( - rw[Once sexplist_def,Once (CONJUNCT2 sexpexp_alt_def)] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) - >- ( - rw[Once sexplist_def,Once (CONJUNCT1 (CONJUNCT2 (CONJUNCT2 sexpexp_alt_def)))] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) - >- ( - rw[Once sexplist_def,Once (CONJUNCT1 (funpow 3 CONJUNCT2 sexpexp_alt_def))] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) - >- ( - rw[Once sexplist_def, - sexppair_def, - Once (CONJUNCT1 (funpow 4 CONJUNCT2 sexpexp_alt_def))] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[sexppat_alt_intro1] \\ - TOP_CASE_TAC \\ fs[] ) - >- ( - rw[Once sexplist_def, - sexppair_def, - Once (funpow 5 CONJUNCT2 sexpexp_alt_def)] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[sexppat_alt_intro1] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[]) + ho_match_mp_tac sexpexp_alt_ind >> rw[] >- + (simp[Once sexpexp_def, Once sexpexp_alt_def] >> + Cases_on `dstrip_sexp s` >> simp[] >> + PairCases_on `x` >> rw[] >> + gvs[ETA_THM, sexptype_alt_intro, sexppat_alt_intro]) >- + (Cases_on `s` >> simp[Once sexplist_def, Once (cj 2 sexpexp_alt_def)] >> + rename1 `Expr l` >> Cases_on `l` >> simp[Once sexplist_def] >> + gvs[] >> Cases_on `sexpexp_alt h` >> gvs[] >> + Cases_on `sexpexp_list (Expr t)` >> simp[]) >- + (Cases_on `s` >> simp[Once sexplist_def, Once (cj 3 sexpexp_alt_def)] >> + rename1 `Expr l` >> Cases_on `l` >> simp[Once sexplist_def] >> + gvs[] >> Cases_on `sexppatexp h` >> gvs[] >> + Cases_on `sexppes (Expr t)` >> simp[]) >- + (Cases_on `s` >> simp[Once sexplist_def, Once (cj 4 sexpexp_alt_def)] >> + rename1 `Expr l` >> Cases_on `l` >> simp[Once sexplist_def] >> + gvs[] >> Cases_on `sexpfun h` >> gvs[] >> + Cases_on `sexpfuns (Expr t)` >> simp[]) >- + (simp[sexppair_def, Once (cj 5 sexpexp_alt_def), sexppat_alt_intro] >> + every_case_tac >> gvs[]) >> + simp[sexppair_def, Once (cj 6 sexpexp_alt_def)] >> + every_case_tac >> gvs[] QED Theorem sexpexp_alt_intro1: @@ -1103,8 +1117,9 @@ Definition sexpdec_def: od Termination wf_rel_tac`measure sexp_size` - \\ rw[LENGTH_EQ_NUM_compute] \\ fs[] - \\ metis_tac[sxMEM_sizelt,dstrip_sexp_size,MEM,LESS_TRANS] + \\ rw[] \\ imp_res_tac dstrip_sexp_size + \\ imp_res_tac sexpMEM_sizelt' + \\ gvs[LENGTH_EQ_NUM_compute, sexp_size_def, SF DNF_ss] End (* translator friendly version for bootstrapping *) @@ -1141,22 +1156,22 @@ Definition sexpdec_alt_def: (sexpdec_list (EL 1 args))) else NONE) ∧ (sexpdec_list s = case s of - | SX_SYM nm => if nm = "nil" then SOME [] else NONE - | SX_CONS a d => + | Atom _ => NONE + | Expr [] => SOME [] + | Expr (a::d) => (case sexpdec_alt a of | NONE => NONE | SOME h => - case sexpdec_list d of + case sexpdec_list (Expr d) of | NONE => NONE - | SOME t => SOME (h::t)) - | _ => NONE) + | SOME t => SOME (h::t))) Termination wf_rel_tac`inv_image (measure sexp_size) (λx. case x of | INL y => y | INR y => y)` \\ rw[] \\ imp_res_tac dstrip_sexp_size \\ - fs[LENGTH_EQ_NUM_compute] + gvs[LENGTH_EQ_NUM_compute, sexp_size_def] End val sexpdec_alt_ind = theorem"sexpdec_alt_ind"; @@ -1165,17 +1180,15 @@ Theorem sexpdec_alt_intro: (∀s. sexpdec s = sexpdec_alt s) ∧ (∀s. sexplist sexpdec s = sexpdec_list s) Proof - ho_match_mp_tac sexpdec_alt_ind \\ rw[] - >- ( - rw[Once sexpdec_def,Once sexpdec_alt_def,sexppat_alt_intro1,sexpexp_alt_intro1,sexptype_alt_intro1] - \\ TOP_CASE_TAC \\ fs[] - \\ TOP_CASE_TAC \\ fs[] - \\ rw[] \\ rfs[] \\ fsrw_tac[ETA_ss][]) - >- ( - rw[Once sexplist_def,Once (CONJUNCT2 sexpdec_alt_def)] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] \\ - TOP_CASE_TAC \\ fs[] ) + ho_match_mp_tac sexpdec_alt_ind >> rw[] >- + (simp[Once sexpdec_def, Once sexpdec_alt_def] >> + Cases_on `dstrip_sexp s` >> simp[] >> + PairCases_on `x` >> rw[] >> + gvs[ETA_THM, sexptype_alt_intro, sexppat_alt_intro, sexpexp_alt_intro]) >> + Cases_on `s` >> simp[Once sexplist_def, Once (cj 2 sexpdec_alt_def)] >> + rename1 `Expr l` >> Cases_on `l` >> simp[Once sexplist_def] >> + gvs[] >> Cases_on `sexpdec_alt h` >> gvs[] >> + Cases_on `sexpdec_list (Expr t)` >> simp[] QED Theorem sexpdec_alt_intro1: @@ -1185,38 +1198,22 @@ Proof rw[FUN_EQ_THM,sexpdec_alt_intro] QED -(* now the reverse: toSexp *) - -Definition listsexp_def: - listsexp = FOLDR SX_CONS nil -End - -Theorem listsexp_thm[simp]: - listsexp [] = nil ∧ listsexp (h::t) = SX_CONS h (listsexp t) -Proof - simp[listsexp_def] -QED - -Theorem listsexp_11[simp]: - ∀ l1 l2. listsexp l1 = listsexp l2 ⇔ l1 = l2 -Proof - Induct >> gen_tac >> cases_on `l2` >> fs[] -QED +(* --- Encoder functions (toSexp) --- *) Definition optsexp_def: - (optsexp NONE = SX_SYM "NONE") ∧ - (optsexp (SOME x) = listsexp [SX_SYM "SOME"; x]) + (optsexp NONE = Atom «NONE») ∧ + (optsexp (SOME x) = Expr [Atom «SOME»; x]) End Theorem optsexp_11[simp]: optsexp o1 = optsexp o2 ⇔ o1 = o2 Proof - cases_on `o1` >> cases_on `o2` >> fs[optsexp_def, listsexp_def] + cases_on `o1` >> cases_on `o2` >> fs[optsexp_def] QED Definition idsexp_def: - (idsexp (Short n) = listsexp [SX_SYM"Short"; SEXSTR (explode n)]) ∧ - (idsexp (Long ns n) = listsexp [SX_SYM"Long"; SEXSTR (explode ns); idsexp n]) + (idsexp (Short n) = Expr [Atom «Short»; SEXSTR (explode n)]) ∧ + (idsexp (Long ns n) = Expr [Atom «Long»; SEXSTR (explode ns); idsexp n]) End Theorem idsexp_11[simp]: @@ -1226,54 +1223,33 @@ Proof QED Definition typesexp_def: - (typesexp (Atvar s) = listsexp [SX_SYM "Atvar"; SEXSTR (explode s)]) ∧ - (typesexp (Atfun t1 t2) = listsexp [SX_SYM "Atfun"; typesexp t1; typesexp t2]) ∧ - (typesexp (Attup ts) = listsexp [SX_SYM "Attup"; listsexp (MAP typesexp ts)]) ∧ - (typesexp (Atapp ts tc) = listsexp [SX_SYM "Atapp"; listsexp (MAP typesexp ts); idsexp tc]) + (typesexp (Atvar s) = Expr [Atom «Atvar»; SEXSTR (explode s)]) ∧ + (typesexp (Atfun t1 t2) = Expr [Atom «Atfun»; typesexp t1; typesexp t2]) ∧ + (typesexp (Attup ts) = Expr [Atom «Attup»; Expr (MAP typesexp ts)]) ∧ + (typesexp (Atapp ts tc) = Expr [Atom «Atapp»; Expr (MAP typesexp ts); idsexp tc]) Termination WF_REL_TAC`measure ast_t_size` >> rw[] \\ Induct_on`ts` >> simp[ast_t_size_def] >> rw[] >> res_tac >> simp[] End -Theorem typesexp_11[simp]: - ∀t1 t2. typesexp t1 = typesexp t2 ⇔ t1 = t2 -Proof - ho_match_mp_tac (theorem"typesexp_ind") - \\ simp[typesexp_def] - \\ rpt conj_tac \\ simp[PULL_FORALL] - \\ CONV_TAC(RESORT_FORALL_CONV List.rev) - \\ Cases \\ simp[typesexp_def] - \\ srw_tac[ETA_ss][EQ_IMP_THM] - \\ metis_tac[MAP_EQ_MAP_IMP] -QED - Definition litsexp_def: - (litsexp (IntLit i) = - if i < 0 then listsexp [SX_SYM "-"; SX_NUM (Num(-i))] - else SX_NUM (Num i)) ∧ - (litsexp (Char c) = listsexp [SX_SYM "char"; SEXSTR [c]]) ∧ + (litsexp (IntLit i) = Expr [Atom «IntLit»; Atom (toString i)]) ∧ + (litsexp (Char c) = Expr [Atom «char»; SEXSTR [c]]) ∧ (litsexp (StrLit s) = SEXSTR (explode s)) ∧ - (litsexp (Word8 w) = listsexp [SX_SYM "word8"; SX_NUM (w2n w)]) ∧ - (litsexp (Word64 w) = listsexp [SX_SYM "word64"; SX_NUM (w2n w)]) ∧ - (litsexp (Float64 w) = listsexp [SX_SYM "float64"; SX_NUM (w2n w)]) + (litsexp (Word8 w) = Expr [Atom «word8»; SXNUM (w2n w)]) ∧ + (litsexp (Word64 w) = Expr [Atom «word64»; SXNUM (w2n w)]) ∧ + (litsexp (Float64 w) = Expr [Atom «float64»; SXNUM (w2n w)]) End -Theorem litsexp_11[simp]: - ∀l1 l2. litsexp l1 = litsexp l2 ⇔ l1 = l2 -Proof - Cases \\ Cases \\ rw[litsexp_def,EQ_IMP_THM,listsexp_def] - \\ intLib.COOPER_TAC -QED - Definition patsexp_def: - (patsexp Pany = listsexp [SX_SYM "Pany"]) ∧ + (patsexp Pany = Expr [Atom «Pany»]) ∧ (patsexp (Pvar s) = SEXSTR (explode s)) ∧ - (patsexp (Plit l) = listsexp [SX_SYM "Plit"; litsexp l]) ∧ - (patsexp (Pcon cn ps) = listsexp [SX_SYM "Pcon"; optsexp (OPTION_MAP idsexp cn); listsexp (MAP patsexp ps)]) ∧ - (patsexp (Pas p i) = listsexp [SX_SYM "Pas"; patsexp p; SEXSTR (explode i)]) ∧ - (patsexp (Pref p) = listsexp [SX_SYM "Pref"; patsexp p]) ∧ - (patsexp (Ptannot p t) = listsexp [SX_SYM "Ptannot" ; patsexp p; typesexp t]) + (patsexp (Plit l) = Expr [Atom «Plit»; litsexp l]) ∧ + (patsexp (Pcon cn ps) = Expr [Atom «Pcon»; optsexp (OPTION_MAP idsexp cn); Expr (MAP patsexp ps)]) ∧ + (patsexp (Pas p i) = Expr [Atom «Pas»; patsexp p; SEXSTR (explode i)]) ∧ + (patsexp (Pref p) = Expr [Atom «Pref»; patsexp p]) ∧ + (patsexp (Ptannot p t) = Expr [Atom «Ptannot» ; patsexp p; typesexp t]) Termination WF_REL_TAC`measure pat_size` >> simp [] >> @@ -1283,31 +1259,16 @@ Termination decide_tac End -Theorem patsexp_11[simp]: - ∀p1 p2. patsexp p1 = patsexp p2 ⇔ p1 = p2 -Proof - ho_match_mp_tac (theorem"patsexp_ind") - \\ rpt conj_tac \\ simp[PULL_FORALL] - \\ CONV_TAC(RESORT_FORALL_CONV List.rev) - \\ Cases \\ rw[patsexp_def,listsexp_def] - \\ rw[EQ_IMP_THM] - >- ( metis_tac[OPTION_MAP_INJ,idsexp_11] ) - \\ imp_res_tac FOLDR_SX_CONS_INJ - \\ imp_res_tac (REWRITE_RULE[AND_IMP_INTRO] MAP_EQ_MAP_IMP) - \\ first_x_assum match_mp_tac - \\ simp[] \\ metis_tac[] -QED - Definition testsexp_def: - testsexp Equal = SX_SYM "Equal" ∧ - testsexp (Compare Lt) = SX_SYM "Less" ∧ - testsexp (Compare Leq) = SX_SYM "LessEq" ∧ - testsexp (Compare Gt) = SX_SYM "Greater" ∧ - testsexp (Compare Geq) = SX_SYM "GreaterEq" ∧ - testsexp (AltCompare Lt) = SX_SYM "AltLess" ∧ - testsexp (AltCompare Leq) = SX_SYM "AltLessEq" ∧ - testsexp (AltCompare Gt) = SX_SYM "AltGreater" ∧ - testsexp (AltCompare Geq) = SX_SYM "AltGreaterEq" + testsexp Equal = Atom «Equal» ∧ + testsexp (Compare Lt) = Atom «Less» ∧ + testsexp (Compare Leq) = Atom «LessEq» ∧ + testsexp (Compare Gt) = Atom «Greater» ∧ + testsexp (Compare Geq) = Atom «GreaterEq» ∧ + testsexp (AltCompare Lt) = Atom «AltLess» ∧ + testsexp (AltCompare Leq) = Atom «AltLessEq» ∧ + testsexp (AltCompare Gt) = Atom «AltGreater» ∧ + testsexp (AltCompare Geq) = Atom «AltGreaterEq» End Theorem testsexp_11[simp]: @@ -1322,25 +1283,25 @@ Theorem sexptest_testsexp[simp]: ∀x. decode_test (testsexp x) = SOME x Proof Cases - \\ TRY (rename [‘Compare oo’] \\ Cases_on ‘oo’) - \\ TRY (rename [‘AltCompare oo’] \\ Cases_on ‘oo’) + \\ TRY (rename [`Compare oo`] \\ Cases_on `oo`) + \\ TRY (rename [`AltCompare oo`] \\ Cases_on `oo`) \\ fs [decode_test_def,testsexp_def] QED Definition arithsexp_def: - arithsexp Add = SX_SYM "Add" ∧ - arithsexp Sub = SX_SYM "Sub" ∧ - arithsexp Mul = SX_SYM "Mul" ∧ - arithsexp Div = SX_SYM "Div" ∧ - arithsexp Mod = SX_SYM "Mod" ∧ - arithsexp And = SX_SYM "And" ∧ - arithsexp Xor = SX_SYM "Xor" ∧ - arithsexp Or = SX_SYM "Or" ∧ - arithsexp Not = SX_SYM "Not" ∧ - arithsexp Neg = SX_SYM "Neg" ∧ - arithsexp Abs = SX_SYM "Abs" ∧ - arithsexp Sqrt = SX_SYM "Sqrt" ∧ - arithsexp FMA = SX_SYM "FMA" + arithsexp Add = Atom «Add» ∧ + arithsexp Sub = Atom «Sub» ∧ + arithsexp Mul = Atom «Mul» ∧ + arithsexp Div = Atom «Div» ∧ + arithsexp Mod = Atom «Mod» ∧ + arithsexp And = Atom «And» ∧ + arithsexp Xor = Atom «Xor» ∧ + arithsexp Or = Atom «Or» ∧ + arithsexp Not = Atom «Not» ∧ + arithsexp Neg = Atom «Neg» ∧ + arithsexp Abs = Atom «Abs» ∧ + arithsexp Sqrt = Atom «Sqrt» ∧ + arithsexp FMA = Atom «FMA» End Theorem arithsexp_11[simp]: @@ -1358,276 +1319,114 @@ Proof QED Definition prim_typesexp_def: - prim_typesexp BoolT = SX_SYM "BoolT" ∧ - prim_typesexp IntT = SX_SYM "IntT" ∧ - prim_typesexp CharT = SX_SYM "CharT" ∧ - prim_typesexp StrT = SX_SYM "StrT" ∧ - prim_typesexp (WordT W8) = SX_SYM "Word8T" ∧ - prim_typesexp (WordT W64) = SX_SYM "Word64T" ∧ - prim_typesexp Float64T = SX_SYM "Float64T" + prim_typesexp BoolT = Atom «BoolT» ∧ + prim_typesexp IntT = Atom «IntT» ∧ + prim_typesexp CharT = Atom «CharT» ∧ + prim_typesexp StrT = Atom «StrT» ∧ + prim_typesexp (WordT W8) = Atom «Word8T» ∧ + prim_typesexp (WordT W64) = Atom «Word64T» ∧ + prim_typesexp Float64T = Atom «Float64T» End -Theorem sexplist_listsexp_matchable: - ∀g gl. (∀x. MEM x l ⇒ f (g x) = SOME x) ∧ (gl = MAP g l) ⇒ - sexplist f (listsexp gl) = SOME l -Proof - Induct_on`l` >> simp[listsexp_def,Once sexplist_def] >> - simp[GSYM listsexp_def] >> metis_tac[] -QED - -Theorem dstrip_sexp_SX_STR[simp]: - dstrip_sexp (SX_STR s) = NONE -Proof - EVAL_TAC -QED - -Theorem dstrip_sexp_SEXSTR[simp]: - dstrip_sexp (SEXSTR s) = NONE -Proof - EVAL_TAC -QED - -Theorem odestSXSTR_SOME[simp]: - (odestSXSTR s = SOME y ⇔ s = SX_STR (explode y)) ∧ - (SOME y = odestSXSTR s ⇔ s = SX_STR (explode y)) -Proof - Cases_on`s`>>simp[odestSXSTR_def] >> simp[EQ_SYM_EQ] >> - iff_tac >> strip_tac >> simp [] -QED - -Theorem odestSEXSTR_SOME[simp]: - (odestSEXSTR s = SOME y ⇔ s = SEXSTR (explode y)) ∧ - (SOME y = odestSEXSTR s ⇔ s = SEXSTR (explode y)) -Proof - Cases_on`s`\\simp[odestSEXSTR_def,SEXSTR_def] - \\ metis_tac[decode_encode_control,encode_decode_control, - explode_implode,implode_explode] -QED - -Theorem odestSXNUM_SOME[simp]: - (odestSXNUM s = SOME n ⇔ s = &n) ∧ - (SOME n = odestSXNUM s ⇔ s = &n) -Proof - Cases_on ‘s’ >> simp[] -QED - -Theorem odestSXSTR_SX_STR[simp]: - (odestSXSTR (SX_STR s) = SOME (implode s)) -Proof - simp[] -QED - -Theorem odestSEXSTR_SEXSTR[simp]: - odestSEXSTR (SEXSTR s) = SOME (implode s) -Proof simp[] -QED - -Theorem odestSXNUM_SX_NUM[simp]: - odestSXNUM (SX_NUM n) = SOME n -Proof simp[] -QED - -Theorem odestSXSYM_SX_SYM[simp]: - odestSXSYM (SX_SYM s) = SOME (implode s) -Proof - simp[] -QED - -Theorem odestSXSTR_listsexp[simp]: - odestSXSTR (listsexp l) = NONE -Proof - Cases_on`l`>>EVAL_TAC -QED - -Theorem odestSEXSTR_listsexp[simp]: - odestSEXSTR (listsexp l) = NONE -Proof - Cases_on`l`>>EVAL_TAC -QED - -Theorem odestSXNUM_listsexp[simp]: - odestSXNUM (listsexp l) = NONE -Proof - Cases_on`l`>>EVAL_TAC -QED - -Theorem strip_sxcons_listsexp[simp]: - strip_sxcons (listsexp ls) = SOME ls -Proof - Induct_on`ls`>>rw[listsexp_def] >> simp[GSYM listsexp_def] -QED - -Theorem dstrip_sexp_listsexp[simp]: - (dstrip_sexp (listsexp ls) = - case ls of (SX_SYM x::xs) => SOME (x,xs) | _ => NONE) -Proof - BasicProvers.CASE_TAC >> rw[dstrip_sexp_def,listsexp_def] >> - BasicProvers.CASE_TAC >> rw[GSYM listsexp_def] -QED - -Theorem sexplist_listsexp_rwt[simp]: - (∀x. MEM x l ⇒ f (g x) = SOME x) ⇒ - (sexplist f (listsexp (MAP g l)) = SOME l) -Proof - metis_tac[sexplist_listsexp_matchable] -QED - -Theorem sexplist_listsexp_imp: - sexplist f (listsexp l1) = SOME l2 ⇒ - ∀n. n < LENGTH l1 ⇒ f (EL n l1) = SOME (EL n l2) -Proof - qid_spec_tac`l2`>> Induct_on`l1`>> simp[PULL_EXISTS, LT_SUC, DISJ_IMP_THM] -QED - -Theorem sexpopt_optsexp[simp]: - (∀y. (x = SOME y) ⇒ (f (g y) = x)) ⇒ - (sexpopt f (optsexp (OPTION_MAP g x)) = SOME x) -Proof - Cases_on`x`>>EVAL_TAC >> simp[] -QED - -Theorem sexpid_odestSEXSTR_idsexp[simp]: - sexpid odestSEXSTR (idsexp i) = SOME i -Proof - Induct_on `i` >> simp[idsexp_def, dstrip_sexp_def] >> - rw [Once sexpid_def, dstrip_sexp_def, EXISTS_PROD, strip_sxcons_def] -QED - -Theorem dstrip_sexp_thm[simp]: - dstrip_sexp ⟪SX_SYM s • args⟫ = lift (λt. (s,t)) (strip_sxcons args) ∧ - dstrip_sexp ⟪ &n • args⟫ = NONE ∧ - dstrip_sexp ⟪SX_STR strng • args⟫ = NONE ∧ - dstrip_sexp ⟪ ⟪s1 • s2⟫ • args⟫ = NONE ∧ - dstrip_sexp (&n) = NONE ∧ - dstrip_sexp (SX_SYM s) = NONE ∧ - dstrip_sexp (SX_STR strng) = NONE -Proof - simp[dstrip_sexp_def] -QED - -Theorem sexptype_typesexp[simp]: - sexptype (typesexp t) = SOME t -Proof - qid_spec_tac`t` >> - ho_match_mp_tac type_ind >> - conj_tac >- rw[Once sexptype_def,typesexp_def] >> - conj_tac >- (rw[] \\ rw[Once sexptype_def,typesexp_def]) >> - conj_tac \\ ( - Induct>>rw[typesexp_def] >- ( - rw[Once sexptype_def,sexplist_listsexp_matchable] ) >> fs[] >> - rw[Once sexptype_def] >> - fsrw_tac[boolSimps.ETA_ss][] >> - match_mp_tac sexplist_listsexp_matchable >> - fs[typesexp_def] >> rw[] >> rw[] >> - fs[listTheory.EVERY_MEM] >> - metis_tac[]) -QED - Theorem sexpprim_type_testsexp[simp]: ∀x. decode_prim_type (prim_typesexp x) = SOME x Proof Cases \\ fs [decode_prim_type_def,prim_typesexp_def] - \\ Cases_on ‘w’ \\ fs [decode_prim_type_def,prim_typesexp_def] + \\ Cases_on `w` \\ fs [decode_prim_type_def,prim_typesexp_def] QED Theorem prim_typesexp_11[simp]: ∀l1 l2. prim_typesexp l1 = prim_typesexp l2 ⇔ l1 = l2 Proof Cases \\ Cases \\ simp[prim_typesexp_def] - \\ Cases_on ‘w’ \\ simp[prim_typesexp_def] - \\ Cases_on ‘w'’ \\ simp[prim_typesexp_def] + \\ Cases_on `w` \\ simp[prim_typesexp_def] + \\ Cases_on `w'` \\ simp[prim_typesexp_def] QED Definition opsexp_def: - (opsexp (Shift W8 Lsl n) = SX_CONS (SX_SYM "Shift8Lsl") (SX_NUM n)) ∧ - (opsexp (Shift W8 Lsr n) = SX_CONS (SX_SYM "Shift8Lsr") (SX_NUM n)) ∧ - (opsexp (Shift W8 Asr n) = SX_CONS (SX_SYM "Shift8Asr") (SX_NUM n)) ∧ - (opsexp (Shift W8 Ror n) = SX_CONS (SX_SYM "Shift8Ror") (SX_NUM n)) ∧ - (opsexp (Shift W64 Lsl n) = SX_CONS (SX_SYM "Shift64Lsl") (SX_NUM n)) ∧ - (opsexp (Shift W64 Lsr n) = SX_CONS (SX_SYM "Shift64Lsr") (SX_NUM n)) ∧ - (opsexp (Shift W64 Asr n) = SX_CONS (SX_SYM "Shift64Asr") (SX_NUM n)) ∧ - (opsexp (Shift W64 Ror n) = SX_CONS (SX_SYM "Shift64Ror") (SX_NUM n)) ∧ - (opsexp Equality = SX_SYM "Equality") ∧ - (opsexp Opapp = SX_SYM "Opapp") ∧ - (opsexp Opassign = SX_SYM "Opassign") ∧ - (opsexp Opref = SX_SYM "Opref") ∧ - (opsexp Opderef = SX_SYM "Opderef") ∧ - (opsexp Aw8alloc = SX_SYM "Aw8alloc") ∧ - (opsexp Aw8sub = SX_SYM "Aw8sub") ∧ - (opsexp Aw8length = SX_SYM "Aw8length") ∧ - (opsexp Aw8update = SX_SYM "Aw8update") ∧ - (opsexp Aw8sub_unsafe = SX_SYM "Aw8subunsafe") ∧ - (opsexp Aw8update_unsafe = SX_SYM "Aw8updateunsafe") ∧ - (opsexp CopyStrStr = SX_SYM "CopyStrStr") ∧ - (opsexp CopyStrAw8 = SX_SYM "CopyStrAw8") ∧ - (opsexp CopyAw8Str = SX_SYM "CopyAw8Str") ∧ - (opsexp CopyAw8Aw8 = SX_SYM "CopyAw8Aw8") ∧ - (opsexp XorAw8Str_unsafe = SX_SYM "XorAw8Strunsafe") ∧ - (opsexp Implode = SX_SYM "Implode") ∧ - (opsexp Explode = SX_SYM "Explode") ∧ - (opsexp Strsub = SX_SYM "Strsub") ∧ - (opsexp Strlen = SX_SYM "Strlen") ∧ - (opsexp Strcat = SX_SYM "Strcat") ∧ - (opsexp VfromList = SX_SYM "VfromList") ∧ - (opsexp Vsub = SX_SYM "Vsub") ∧ - (opsexp Vsub_unsafe = SX_SYM "Vsub_unsafe") ∧ - (opsexp Vlength = SX_SYM "Vlength") ∧ - (opsexp ListAppend = SX_SYM "ListAppend") ∧ - (opsexp Aalloc = SX_SYM "Aalloc") ∧ - (opsexp AallocEmpty = SX_SYM "AallocEmpty") ∧ - (opsexp AallocFixed = SX_SYM "AallocFixed") ∧ - (opsexp Asub = SX_SYM "Asub") ∧ - (opsexp Alength = SX_SYM "Alength") ∧ - (opsexp Aupdate = SX_SYM "Aupdate") ∧ - (opsexp Asub_unsafe = SX_SYM "Asubunsafe") ∧ - (opsexp Aupdate_unsafe = SX_SYM "Aupdateunsafe") ∧ - (opsexp ConfigGC = SX_SYM "ConfigGC") ∧ - (opsexp Eval = SX_SYM "Eval") ∧ - (opsexp Env_id = SX_SYM "Envid") ∧ - (opsexp (FFI s) = SX_CONS (SX_SYM "FFI") (SEXSTR (explode s))) ∧ - (opsexp (ThunkOp ForceThunk) = SX_SYM "ForceThunk") ∧ + (opsexp (Shift W8 Lsl n) = Expr [Atom «Shift8Lsl»; SXNUM n]) ∧ + (opsexp (Shift W8 Lsr n) = Expr [Atom «Shift8Lsr»; SXNUM n]) ∧ + (opsexp (Shift W8 Asr n) = Expr [Atom «Shift8Asr»; SXNUM n]) ∧ + (opsexp (Shift W8 Ror n) = Expr [Atom «Shift8Ror»; SXNUM n]) ∧ + (opsexp (Shift W64 Lsl n) = Expr [Atom «Shift64Lsl»; SXNUM n]) ∧ + (opsexp (Shift W64 Lsr n) = Expr [Atom «Shift64Lsr»; SXNUM n]) ∧ + (opsexp (Shift W64 Asr n) = Expr [Atom «Shift64Asr»; SXNUM n]) ∧ + (opsexp (Shift W64 Ror n) = Expr [Atom «Shift64Ror»; SXNUM n]) ∧ + (opsexp Equality = Atom «Equality») ∧ + (opsexp Opapp = Atom «Opapp») ∧ + (opsexp Opassign = Atom «Opassign») ∧ + (opsexp Opref = Atom «Opref») ∧ + (opsexp Opderef = Atom «Opderef») ∧ + (opsexp Aw8alloc = Atom «Aw8alloc») ∧ + (opsexp Aw8sub = Atom «Aw8sub») ∧ + (opsexp Aw8length = Atom «Aw8length») ∧ + (opsexp Aw8update = Atom «Aw8update») ∧ + (opsexp Aw8sub_unsafe = Atom «Aw8subunsafe») ∧ + (opsexp Aw8update_unsafe = Atom «Aw8updateunsafe») ∧ + (opsexp CopyStrStr = Atom «CopyStrStr») ∧ + (opsexp CopyStrAw8 = Atom «CopyStrAw8») ∧ + (opsexp CopyAw8Str = Atom «CopyAw8Str») ∧ + (opsexp CopyAw8Aw8 = Atom «CopyAw8Aw8») ∧ + (opsexp XorAw8Str_unsafe = Atom «XorAw8Strunsafe») ∧ + (opsexp Implode = Atom «Implode») ∧ + (opsexp Explode = Atom «Explode») ∧ + (opsexp Strsub = Atom «Strsub») ∧ + (opsexp Strlen = Atom «Strlen») ∧ + (opsexp Strcat = Atom «Strcat») ∧ + (opsexp VfromList = Atom «VfromList») ∧ + (opsexp Vsub = Atom «Vsub») ∧ + (opsexp Vsub_unsafe = Atom «Vsub_unsafe») ∧ + (opsexp Vlength = Atom «Vlength») ∧ + (opsexp ListAppend = Atom «ListAppend») ∧ + (opsexp Aalloc = Atom «Aalloc») ∧ + (opsexp AallocEmpty = Atom «AallocEmpty») ∧ + (opsexp AallocFixed = Atom «AallocFixed») ∧ + (opsexp Asub = Atom «Asub») ∧ + (opsexp Alength = Atom «Alength») ∧ + (opsexp Aupdate = Atom «Aupdate») ∧ + (opsexp Asub_unsafe = Atom «Asubunsafe») ∧ + (opsexp Aupdate_unsafe = Atom «Aupdateunsafe») ∧ + (opsexp ConfigGC = Atom «ConfigGC») ∧ + (opsexp Eval = Atom «Eval») ∧ + (opsexp Env_id = Atom «Envid») ∧ + (opsexp (FFI s) = Expr [Atom «FFI»; SEXSTR (explode s)]) ∧ + (opsexp (ThunkOp ForceThunk) = Atom «ForceThunk») ∧ (opsexp (ThunkOp (AllocThunk m)) = - SX_CONS (SX_SYM "AllocThunk") (SX_SYM (encode_thunk_mode m))) ∧ + Expr [Atom «AllocThunk»; Atom (implode (encode_thunk_mode m))]) ∧ (opsexp (ThunkOp (UpdateThunk m)) = - SX_CONS (SX_SYM "UpdateThunk") (SX_SYM (encode_thunk_mode m))) ∧ + Expr [Atom «UpdateThunk»; Atom (implode (encode_thunk_mode m))]) ∧ (opsexp (Arith a prim_type) = - SX_CONS (SX_SYM "Arith") $ - SX_CONS (arithsexp a) - (prim_typesexp prim_type)) ∧ + Expr [Atom «Arith»; arithsexp a; prim_typesexp prim_type]) ∧ (opsexp (FromTo ty1 ty2) = - SX_CONS (SX_SYM "FromTo") $ - SX_CONS (prim_typesexp ty1) - (prim_typesexp ty2)) ∧ + Expr [Atom «FromTo»; prim_typesexp ty1; prim_typesexp ty2]) ∧ (opsexp (Test test prim_type) = - SX_CONS (SX_SYM "Test") $ - SX_CONS (testsexp test) - (prim_typesexp prim_type)) + Expr [Atom «Test»; testsexp test; prim_typesexp prim_type]) End Theorem sexpop_opsexp[simp]: sexpop (opsexp op) = SOME op Proof - Cases_on ‘∃t. op = ThunkOp t’ - >- (gvs [] \\ Cases_on ‘t’ - \\ gvs [sexpop_def,opsexp_def] - \\ rw [] \\ gvs [AllCaseEqs()] - \\ Cases_on ‘t'’ \\ gvs [encode_thunk_mode_def,decode_thunk_mode_def]) >> - Cases_on`op`>>fs []>>rw[sexpop_def,opsexp_def] >> + Cases_on `∃t. op = ThunkOp t` + >- (gvs [] >> Cases_on `t` + >> gvs [sexpop_def,opsexp_def] + >> rw [] >> gvs [AllCaseEqs()] + >> Cases_on `t'` >> gvs [encode_thunk_mode_def,decode_thunk_mode_def]) >> + Cases_on `op` >> fs [] >> rw[sexpop_def,opsexp_def] >> rw[sexpop_def,opsexp_def,SEXSTR_def] >> rename [‘Shift c1 c2 _’] >> - Cases_on`c1` >> rw[sexpop_def,opsexp_def] >> - Cases_on`c2` >> rw[sexpop_def,opsexp_def] + Cases_on `c1` >> rw[sexpop_def,opsexp_def] >> + Cases_on `c2` >> rw[sexpop_def,opsexp_def] QED Theorem opsexp_11[simp]: ∀o1 o2. opsexp o1 = opsexp o2 ⇔ o1 = o2 Proof - rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM “sexpop”) >> simp[] + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexpop``) >> simp[] QED Definition logsexp_def: - logsexp Andalso = SX_SYM "Andalso" ∧ - logsexp Orelse = SX_SYM "Orelse" + logsexp Andalso = Atom «Andalso» ∧ + logsexp Orelse = Atom «Orelse» End Theorem logsexp_11[simp]: @@ -1637,19 +1436,19 @@ Proof QED Definition locnsexp_def: - locnsexp (POSN n1 n2) = listsexp (MAP SX_NUM [n1;n2]) ∧ - locnsexp UNKNOWNpt = SX_SYM "unk" ∧ - locnsexp EOFpt = SX_SYM "eof" + locnsexp (POSN n1 n2) = Expr [SXNUM n1; SXNUM n2] ∧ + locnsexp UNKNOWNpt = Atom «unk» ∧ + locnsexp EOFpt = Atom «eof» End Theorem locnsexp_11[simp]: locnsexp p1 = locnsexp p2 ⇔ p1 = p2 Proof - map_every Cases_on [‘p1’, ‘p2’] >> simp[locnsexp_def, listsexp_def] + map_every Cases_on [`p1`, `p2`] >> simp[locnsexp_def, SXNUM_def, mlintTheory.num_to_str_11] QED Definition locssexp_def: - locssexp (Locs p1 p2) = listsexp (MAP locnsexp [p1;p2]) + locssexp (Locs p1 p2) = Expr [locnsexp p1; locnsexp p2] End Theorem locssexp_11[simp]: @@ -1659,81 +1458,42 @@ Proof QED Definition expsexp_def: - expsexp (Raise e) = ⟪SX_SYM "Raise"; expsexp e⟫ ∧ + expsexp (Raise e) = Expr [Atom «Raise»; expsexp e] ∧ expsexp (Handle e pes) = - ⟪SX_SYM "Handle"; expsexp e; - listsexp (MAP (λ(p,e). SX_CONS (patsexp p) (expsexp e)) pes)⟫ ∧ - expsexp (Lit l) = listsexp [SX_SYM "Lit"; litsexp l] ∧ + Expr [Atom «Handle»; expsexp e; + Expr (MAP (λ(p,e). Expr [patsexp p; expsexp e]) pes)] ∧ + expsexp (Lit l) = Expr [Atom «Lit»; litsexp l] ∧ expsexp (Con cn es) = - listsexp [SX_SYM "Con"; optsexp (OPTION_MAP idsexp cn); - listsexp (MAP expsexp es)] ∧ - expsexp (Var id) = listsexp [SX_SYM "Var"; idsexp id] ∧ - expsexp (Fun x e) = listsexp [SX_SYM "Fun"; SEXSTR (explode x); expsexp e] ∧ + Expr [Atom «Con»; optsexp (OPTION_MAP idsexp cn); + Expr (MAP expsexp es)] ∧ + expsexp (Var id) = Expr [Atom «Var»; idsexp id] ∧ + expsexp (Fun x e) = Expr [Atom «Fun»; SEXSTR (explode x); expsexp e] ∧ expsexp (App op es) = - listsexp [SX_SYM "App"; opsexp op; listsexp (MAP expsexp es)] ∧ - expsexp (Log lop e1 e2) = ⟪SX_SYM "Log"; logsexp lop; expsexp e1; expsexp e2⟫ ∧ - expsexp (If e1 e2 e3) = ⟪SX_SYM "If"; expsexp e1; expsexp e2; expsexp e3⟫ ∧ + Expr [Atom «App»; opsexp op; Expr (MAP expsexp es)] ∧ + expsexp (Log lop e1 e2) = Expr [Atom «Log»; logsexp lop; expsexp e1; expsexp e2] ∧ + expsexp (If e1 e2 e3) = Expr [Atom «If»; expsexp e1; expsexp e2; expsexp e3] ∧ expsexp (Mat e pes) = - ⟪SX_SYM "Mat"; expsexp e; - listsexp (MAP (λ(p,e). SX_CONS (patsexp p) (expsexp e)) pes)⟫ ∧ + Expr [Atom «Mat»; expsexp e; + Expr (MAP (λ(p,e). Expr [patsexp p; expsexp e]) pes)] ∧ expsexp (Let so e1 e2) = - ⟪SX_SYM "Let"; optsexp (OPTION_MAP (SEXSTR ∘ explode) so); expsexp e1; expsexp e2⟫ ∧ + Expr [Atom «Let»; optsexp (OPTION_MAP (SEXSTR ∘ explode) so); expsexp e1; expsexp e2] ∧ expsexp (Letrec funs e) = - ⟪SX_SYM "Letrec"; - listsexp (MAP (λ(x,y,z). SX_CONS (SEXSTR (explode x)) - (SX_CONS (SEXSTR (explode y)) (expsexp z))) funs); - expsexp e⟫ ∧ - expsexp (Tannot e t) = ⟪SX_SYM "Tannot"; expsexp e; typesexp t⟫ ∧ - expsexp (Lannot e loc) = ⟪SX_SYM "Lannot"; expsexp e; locssexp loc⟫ + Expr [Atom «Letrec»; + Expr (MAP (λ(x,y,z). Expr [SEXSTR (explode x); + Expr [SEXSTR (explode y); expsexp z]]) funs); + expsexp e] ∧ + expsexp (Tannot e t) = Expr [Atom «Tannot»; expsexp e; typesexp t] ∧ + expsexp (Lannot e loc) = Expr [Atom «Lannot»; expsexp e; locssexp loc] End -Theorem SEXSTR_explode_11[local]: - (SEXSTR ∘ explode) s1 = (SEXSTR ∘ explode) s2 ⇒ s1 = s2 -Proof - simp [] -QED - -Theorem expsexp_11[simp]: - ∀e1 e2. expsexp e1 = expsexp e2 ⇒ e1 = e2 -Proof - ho_match_mp_tac (theorem"expsexp_ind") - \\ rpt conj_tac \\ simp[PULL_FORALL] - \\ CONV_TAC(RESORT_FORALL_CONV List.rev) - \\ Cases \\ rw[expsexp_def] - \\ imp_res_tac (REWRITE_RULE[AND_IMP_INTRO] MAP_EQ_MAP_IMP) - \\ TRY(first_x_assum match_mp_tac \\ rw[FORALL_PROD]) - \\ rpt(pairarg_tac \\ fs[]) - \\ metis_tac[OPTION_MAP_INJ,idsexp_11,simpleSexpTheory.sexp_11,SEXSTR_11,SEXSTR_explode_11] -QED - Definition type_defsexp_def: - type_defsexp = listsexp o + type_defsexp = Expr o MAP (λ(xs,x,ls). - SX_CONS (listsexp (MAP (SEXSTR ∘ explode) xs)) - (SX_CONS (SEXSTR (explode x)) - (listsexp (MAP (λ(y,ts). SX_CONS (SEXSTR (explode y)) (listsexp (MAP typesexp ts))) ls)))) + Expr [Expr (MAP (SEXSTR ∘ explode) xs); + Expr [SEXSTR (explode x); + Expr (MAP (λ(y,ts). Expr [SEXSTR (explode y); Expr (MAP typesexp ts)]) ls)]]) End -Theorem type_defsexp_11[simp]: - ∀t1 t2. type_defsexp t1 = type_defsexp t2 ⇔ t1 = t2 -Proof - rw[type_defsexp_def,EQ_IMP_THM] - \\ imp_res_tac (REWRITE_RULE[AND_IMP_INTRO] MAP_EQ_MAP_IMP) - \\ first_x_assum match_mp_tac - \\ rw[FORALL_PROD] - \\ rpt (pairarg_tac \\ fs[]) \\ rveq - \\ conj_tac - >- ( - Q.ISPEC_THEN`SEXSTR ∘ explode`match_mp_tac INJ_MAP_EQ - \\ simp[INJ_DEF] ) - \\ imp_res_tac (REWRITE_RULE[AND_IMP_INTRO] MAP_EQ_MAP_IMP) - \\ first_x_assum match_mp_tac - \\ rw[FORALL_PROD] - \\ rpt (pairarg_tac \\ fs[]) \\ rveq - \\ Q.ISPEC_THEN`typesexp`match_mp_tac INJ_MAP_EQ - \\ simp[INJ_DEF] -QED - Theorem dec1_size_eq: dec1_size xs = list_size dec_size xs Proof @@ -1748,69 +1508,127 @@ QED Definition decsexp_def: decsexp (Dlet locs p e) = - ⟪SX_SYM "Dlet"; locssexp locs; patsexp p; expsexp e⟫ ∧ + Expr [Atom «Dlet»; locssexp locs; patsexp p; expsexp e] ∧ decsexp (Dletrec locs funs) = - listsexp [ - SX_SYM "Dletrec"; + Expr [ + Atom «Dletrec»; locssexp locs; - listsexp - (MAP (λ(f,x,e). SX_CONS (SEXSTR (explode f)) (SX_CONS (SEXSTR (explode x)) (expsexp e))) + Expr + (MAP (λ(f,x,e). Expr [SEXSTR (explode f); + Expr [SEXSTR (explode x); expsexp e]]) funs)] ∧ - decsexp (Dtype locs td) = ⟪SX_SYM "Dtype"; locssexp locs; type_defsexp td⟫ ∧ - decsexp (Dtabbrev locs ns x t) = ⟪SX_SYM "Dtabbrev"; locssexp locs; listsexp (MAP (SEXSTR ∘ explode) ns); SEXSTR (explode x); typesexp t⟫ ∧ - decsexp (Denv name) = ⟪SX_SYM "Denv"; SEXSTR (explode name)⟫ ∧ + decsexp (Dtype locs td) = Expr [Atom «Dtype»; locssexp locs; type_defsexp td] ∧ + decsexp (Dtabbrev locs ns x t) = Expr [Atom «Dtabbrev»; locssexp locs; Expr (MAP (SEXSTR ∘ explode) ns); SEXSTR (explode x); typesexp t] ∧ + decsexp (Denv name) = Expr [Atom «Denv»; SEXSTR (explode name)] ∧ decsexp (Dexn locs x ts) = - ⟪SX_SYM "Dexn"; locssexp locs; SEXSTR (explode x); listsexp (MAP typesexp ts)⟫ ∧ + Expr [Atom «Dexn»; locssexp locs; SEXSTR (explode x); Expr (MAP typesexp ts)] ∧ decsexp (Dmod name decs) = - ⟪SX_SYM "Dmod"; SEXSTR (explode name); listsexp (MAP decsexp decs)⟫ ∧ + Expr [Atom «Dmod»; SEXSTR (explode name); Expr (MAP decsexp decs)] ∧ decsexp (Dlocal ldecs decs) = - listsexp [SX_SYM "Dlocal"; listsexp (MAP decsexp ldecs); - listsexp (MAP decsexp decs)] + Expr [Atom «Dlocal»; Expr (MAP decsexp ldecs); + Expr (MAP decsexp decs)] End -Theorem decsexp_11[simp]: - ∀d1 d2. decsexp d1 = decsexp d2 ⇔ d1 = d2 +(* --- Roundtrip proofs --- *) + +Theorem sexplist_listsexp_matchable: + ∀g gl. (∀x. MEM x l ⇒ f (g x) = SOME x) ∧ (gl = MAP g l) ⇒ + sexplist f (Expr gl) = SOME l Proof - ho_match_mp_tac(theorem"decsexp_ind") - \\ rw[decsexp_def,EQ_IMP_THM] \\ fs[decsexp_def] - \\ Cases_on`d2` \\ fs[decsexp_def] \\ rw[] - \\ imp_res_tac (REWRITE_RULE[AND_IMP_INTRO] MAP_EQ_MAP_IMP) - \\ TRY (first_x_assum match_mp_tac \\ rw[]) - \\ rpt(pairarg_tac \\ fs[]) + Induct_on`l` >> simp[Once sexplist_def] >> + simp[] >> metis_tac[] QED -(* round trip *) +Theorem sexplist_listsexp_rwt[simp]: + (∀x. MEM x l ⇒ f (g x) = SOME x) ⇒ + (sexplist f (Expr (MAP g l)) = SOME l) +Proof + metis_tac[sexplist_listsexp_matchable] +QED -val exists_g_tac = - (fn (g as (asl,w)) => - let - val (x,b) = dest_exists w - val tm = find_term (fn y => type_of x = type_of y andalso not (is_var y)) b - in EXISTS_TAC tm end g) +Theorem odestSEXSTR_SOME[simp]: + (odestSEXSTR s = SOME y ⇔ s = SEXSTR (explode y)) ∧ + (SOME y = odestSEXSTR s ⇔ s = SEXSTR (explode y)) +Proof + Cases_on`s`\\simp[odestSEXSTR_def,SEXSTR_def] + \\ metis_tac[decode_encode_control,encode_decode_control, + explode_implode,implode_explode] +QED -Theorem sexptype_def_type_defsexp[simp]: - sexptype_def (type_defsexp l) = SOME l +Theorem odestSXNUM_SOME[simp]: + (odestSXNUM s = SOME n ⇔ s = SXNUM n) ∧ + (SOME n = odestSXNUM s ⇔ s = SXNUM n) Proof - rw[type_defsexp_def, sexptype_def_def] >> - irule sexplist_listsexp_matchable >> - irule_at Any EQ_REFL >> simp[FORALL_PROD, sexppair_def] + `!s n. odestSXNUM s = SOME n ==> s = SXNUM n` suffices_by + (rw[EQ_IMP_THM] >> gvs[SXNUM_def, odestSXNUM_def, fromString_toString, num_to_str_def]) >> + Cases >> simp[odestSXNUM_def, SXNUM_def] >> every_case_tac >> gvs[] >> + rw[num_to_str_def] >> AP_TERM_TAC >> simp[Once (GSYM integerTheory.INT_OF_NUM)] +QED + +Theorem odestSXSYM_EQ_SOME[simp]: + (odestSXSYM s = SOME strng ⇔ s = Atom strng) ∧ + (SOME strng = odestSXSYM s ⇔ s = Atom strng) +Proof + Cases_on`s` >> simp[odestSXSYM_def] >> metis_tac[] +QED + +Theorem odestSEXSTR_listsexp[simp]: + odestSEXSTR (listsexp l) = NONE +Proof + simp[listsexp_def] +QED + +Theorem odestSXNUM_listsexp[simp]: + odestSXNUM (listsexp l) = NONE +Proof + simp[listsexp_def] +QED + +Theorem sexpopt_optsexp[simp]: + (∀y. (x = SOME y) ⇒ (f (g y) = x)) ⇒ + (sexpopt f (optsexp (OPTION_MAP g x)) = SOME x) +Proof + Cases_on`x`>>simp[sexpopt_def,optsexp_def,dstrip_sexp_def] +QED + +Theorem sexpid_odestSEXSTR_idsexp[simp]: + sexpid odestSEXSTR (idsexp i) = SOME i +Proof + Induct_on `i` >> simp[idsexp_def, dstrip_sexp_def] >> + rw [Once sexpid_def, dstrip_sexp_def, EXISTS_PROD] +QED + +Theorem sexptype_typesexp[simp]: + sexptype (typesexp t) = SOME t +Proof + qid_spec_tac `t` >> + ho_match_mp_tac type_ind >> + conj_tac >- rw[Once sexptype_def,typesexp_def] >> + conj_tac >- (rw[] >> rw[Once sexptype_def,typesexp_def]) >> + conj_tac >> ( + Induct >> rw[typesexp_def] >- ( + rw[Once sexptype_def,sexplist_listsexp_matchable] ) >> fs[] >> + rw[Once sexptype_def] >> + fsrw_tac[boolSimps.ETA_ss][] >> + match_mp_tac sexplist_listsexp_matchable >> + fs[typesexp_def] >> rw[] >> rw[] >> + fs[listTheory.EVERY_MEM] >> + metis_tac[]) QED Theorem sexplit_litsexp[simp]: sexplit (litsexp l) = SOME l Proof - Cases_on`l`>>simp[sexplit_def,litsexp_def] - >- (rw[] >> intLib.ARITH_TAC ) - >- EVAL_TAC >> + Cases_on `l` >> simp[sexplit_def,litsexp_def,mlstringTheory.implode_def] >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_8] >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_64] >> - ONCE_REWRITE_TAC[wordsTheory.w2n_lt] + simp[wordsTheory.w2n_lt] QED Theorem sexppat_patsexp[simp]: sexppat (patsexp p) = SOME p Proof - qid_spec_tac`p` >> + qid_spec_tac `p` >> ho_match_mp_tac pat_ind >> conj_tac >- simp[patsexp_def,Once sexppat_def] >> conj_tac >- simp[patsexp_def,Once sexppat_def] >> @@ -1821,7 +1639,7 @@ Proof simp[patsexp_def,Once sexppat_def] >> match_mp_tac sexplist_listsexp_matchable >> srw_tac[boolSimps.ETA_ss][] >> - qexists_tac`patsexp`>>simp[] >> + qexists_tac `patsexp` >> simp[] >> fs[listTheory.EVERY_MEM] >> metis_tac[]) >> rw[] >> simp[patsexp_def,Once sexppat_def] QED @@ -1829,8 +1647,7 @@ QED Theorem sexplocpt_locnsexp[simp]: sexplocpt (locnsexp p) = SOME p Proof - Cases_on ‘p’ >> simp[sexplocpt_def, locnsexp_def, listsexp_def] >> - simp[strip_sxcons_def] + Cases_on `p` >> simp[sexplocpt_def, locnsexp_def, odestSXNUM_SXNUM] QED Theorem sexplocn_locnsexp[simp]: @@ -1845,82 +1662,123 @@ Proof Cases_on `l` >> rw[sexplog_def,logsexp_def] QED +val exists_g_tac = + (fn (g as (asl,w)) => + let + val (x,b) = dest_exists w + val tm = find_term (fn y => type_of x = type_of y andalso not (is_var y)) b + in EXISTS_TAC tm end g) + Theorem sexpexp_expsexp[simp]: sexpexp (expsexp e) = SOME e Proof - qid_spec_tac`e` >> + qid_spec_tac `e` >> ho_match_mp_tac exp_ind >> rw[] >> rw[expsexp_def] >> rw[Once sexpexp_def] >> match_mp_tac sexplist_listsexp_matchable >> exists_g_tac >> simp[] >> fs[listTheory.EVERY_MEM] >> - qx_gen_tac`p`>>PairCases_on`p` >> simp[] >> + qx_gen_tac `p` >> PairCases_on `p` >> simp[] >> simp[sexppair_def] >> rw[] >> res_tac >> fs[] QED +Theorem sexptype_def_type_defsexp[simp]: + sexptype_def (type_defsexp l) = SOME l +Proof + rw[type_defsexp_def, sexptype_def_def] >> + irule sexplist_listsexp_matchable >> + irule_at Any EQ_REFL >> simp[FORALL_PROD, sexppair_def] +QED + Theorem sexpdec_decsexp[simp]: ∀d. sexpdec (decsexp d) = SOME d Proof ho_match_mp_tac dec_ind - \\ rw[decsexp_def] - \\ rw[Once sexpdec_def] - \\ match_mp_tac sexplist_listsexp_matchable - \\ exists_g_tac >> simp[] \\ fs[EVERY_MEM] - \\ qx_gen_tac`p`>>PairCases_on`p`>>rw[] - \\ simp[sexppair_def] + >> rw[decsexp_def] + >> rw[Once sexpdec_def] + >> match_mp_tac sexplist_listsexp_matchable + >> exists_g_tac >> simp[] >> fs[EVERY_MEM] + >> qx_gen_tac `p` >> PairCases_on `p` >> rw[] + >> simp[sexppair_def] QED -Theorem odestSXSYM_EQ_SOME[simp]: - (odestSXSYM s = SOME strng ⇔ s = SX_SYM (explode strng)) ∧ - (SOME strng = odestSXSYM s ⇔ s = SX_SYM (explode strng)) + +(* --- Injectivity proofs (via forward roundtrips) --- *) + +Theorem typesexp_11[simp]: + ∀t1 t2. typesexp t1 = typesexp t2 ⇔ t1 = t2 Proof - Cases_on‘s’ >> simp[odestSXSYM_def] >> - metis_tac[implode_explode,explode_implode] + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexptype``) >> simp[] QED -Theorem sexpopt_SOME: - sexpopt f s = SOME opt ⇔ - opt = NONE ∧ s = SX_SYM "NONE" ∨ - ∃x s0. opt = SOME x ∧ f s0 = SOME x ∧ s = listsexp [SX_SYM "SOME"; s0] +Theorem litsexp_11[simp]: + ∀l1 l2. litsexp l1 = litsexp l2 ⇔ l1 = l2 Proof - simp[sexpopt_def, OPTION_CHOICE_EQUALS_OPTION, EXISTS_PROD, - LENGTH_EQ_NUM_compute, PULL_EXISTS, dstrip_sexp_SOME, SF CONJ_ss, - odestSXSYM_def, listsexp_def] >> metis_tac[] + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexplit``) >> simp[] QED -Theorem listsexp_MAP_EQ_f: - (∀x. MEM x ls ⇒ f1 x = f2 x) ⇒ - listsexp (MAP f1 ls) = listsexp (MAP f2 ls) +Theorem patsexp_11[simp]: + ∀p1 p2. patsexp p1 = patsexp p2 ⇔ p1 = p2 Proof - simp[MAP_CONG] + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexppat``) >> simp[] +QED + +Theorem expsexp_11[simp]: + ∀e1 e2. expsexp e1 = expsexp e2 ⇒ e1 = e2 +Proof + rw[] >> pop_assum (mp_tac o AP_TERM ``sexpexp``) >> simp[] +QED + +Theorem type_defsexp_11[simp]: + ∀t1 t2. type_defsexp t1 = type_defsexp t2 ⇔ t1 = t2 +Proof + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexptype_def``) >> simp[] +QED + +Theorem decsexp_11[simp]: + ∀d1 d2. decsexp d1 = decsexp d2 ⇔ d1 = d2 +Proof + rw[EQ_IMP_THM] >> pop_assum (mp_tac o AP_TERM ``sexpdec``) >> simp[] +QED + +(* --- Reverse roundtrip proofs --- *) + +Theorem sexpopt_SOME: + sexpopt f s = SOME opt ⇔ + opt = NONE ∧ s = Atom «NONE» ∨ + ∃x s0. opt = SOME x ∧ f s0 = SOME x ∧ s = Expr [Atom «SOME»; s0] +Proof + Cases_on `s` >> simp[sexpopt_def, odestSXSYM_def, dstrip_sexp_def] >- metis_tac[] >> + simp[dstrip_sexp_SOME, PULL_EXISTS, LENGTH_EQ_NUM_compute] >> + rw[EQ_IMP_THM] >> gvs[] >> + `tag = implode (explode tag)` by simp[mlstringTheory.implode_explode] >> + pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] >> simp[mlstringTheory.implode_def] QED Theorem sexplist_SOME: - sexplist f s = SOME ls ⇔ ∃l. s = listsexp l ∧ MAP f l = MAP SOME ls + sexplist f s = SOME ls ⇔ ∃l. s = Expr l ∧ MAP f l = MAP SOME ls Proof - map_every qid_spec_tac[`s`,`ls`] >> + map_every qid_spec_tac [`s`,`ls`] >> Induct >> rw[] - >- simp[Once sexplist_def, AllCaseEqs(), listsexp_def] >> - simp[Once sexplist_def, AllCaseEqs(), PULL_EXISTS, MAP_EQ_CONS, - listsexp_def] >> metis_tac[] + >- (Cases_on `s` >> simp[Once sexplist_def] >> + Cases_on `l` >> simp[Once sexplist_def, AllCaseEqs()]) >> + Cases_on `s` >> simp[Once sexplist_def, AllCaseEqs(), PULL_EXISTS, MAP_EQ_CONS] >> + Cases_on `l` >> simp[Once sexplist_def, AllCaseEqs(), PULL_EXISTS] >> metis_tac[] QED Theorem sexppair_SOME: sexppair f1 f2 s = SOME p ⇔ - ∃x y a b. f1 x = SOME a ∧ f2 y = SOME b ∧ s = SX_CONS x y ∧ p = (a,b) + ∃x y a b. f1 x = SOME a ∧ f2 y = SOME b ∧ s = Expr [x; y] ∧ p = (a,b) Proof simp[sexppair_def, AllCaseEqs(), PULL_EXISTS] >> metis_tac[] QED Theorem OPTION_CHOICE_EQ_SOME = OPTION_CHOICE_EQUALS_OPTION -Theorem odestSXNUM_EQ_SOME[simp]: - (odestSXNUM s = SOME n ⇔ s = &n) ∧ - (SOME n = odestSXNUM s ⇔ s = &n) -Proof - Cases_on ‘s’ >> simp[odestSXNUM_def] -QED +val tag_tac = + `tag = implode (explode tag)` by simp[mlstringTheory.implode_explode] >> + pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] >> simp[mlstringTheory.implode_def] Theorem litsexp_sexplit: (sexplit s = SOME l ⇔ litsexp l = s) ∧ @@ -1928,23 +1786,24 @@ Theorem litsexp_sexplit: Proof simp[EQ_SYM_EQ] >> simp[sexplit_def, OPTION_CHOICE_EQUALS_OPTION, dstrip_sexp_SOME, PULL_EXISTS, - OPTION_CHOICE_EQ_NONE, LENGTH_EQ_NUM_compute, SF CONJ_ss, odestSXNUM_def, - odestSEXSTR_def] >> - rpt gen_tac >> eq_tac >> rpt strip_tac >> gvs[litsexp_def, listsexp_def] - >- ( - simp[SF CONJ_ss, litsexp_def] >> - Cases_on‘l’ >> - simp[litsexp_def, listsexp_def, PULL_EXISTS, AllCaseEqs(), SF CONJ_ss] >~ - [‘i < 0i’] >- (Cases_on ‘i’ >> simp[]) >~ - [‘STRING c ""’] >- ( - qexists_tac ‘str c’ >> simp []>> - EVAL_TAC) >~ - [‘w2n (c : word8)’] - >- (Cases_on ‘c’ using ranged_word_nchotomy >> gs[dimword_def]) >>~- - ([‘w2n (w : word64)’], - Cases_on ‘w’ using ranged_word_nchotomy >> gs[dimword_def])) >> - Cases_on`cs`>> - Cases_on`s`>>fs[] + OPTION_CHOICE_EQ_NONE, LENGTH_EQ_NUM_compute, SF CONJ_ss, + odestSXNUM_SOME, odestSEXSTR_SOME, odestSXINT_def, AllCaseEqs()] >> + rpt gen_tac >> eq_tac >> rpt strip_tac >> gvs[litsexp_def] + (* backward direction *) + >- (Cases_on `l` >> simp[litsexp_def] >- + (qexists_tac `str c` >> simp[] >> EVAL_TAC) >> + ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_8] >> + ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_64] >> + simp[wordsTheory.w2n_lt]) + (* IntLit forward *) + >- (tag_tac >> Cases_on `h` >> gvs[odestSXINT_def, AllCaseEqs()]) + (* Char forward *) + >- (tag_tac >> + `LENGTH (explode cs) = 1` by simp[mlstringTheory.strlen_implode] >> + Cases_on `explode cs` >> gvs[] >> + Cases_on `cs` >> gvs[mlstringTheory.strsub_def, mlstringTheory.explode_def]) + (* word8, word64, float64 forward - just tag *) + >> tag_tac QED Theorem idsexp_sexpid_odestSEXSTR: @@ -1952,7 +1811,7 @@ Theorem idsexp_sexpid_odestSEXSTR: Proof Induct >> simp[Once sexpid_def, EXISTS_PROD, dstrip_sexp_SOME, PULL_EXISTS, idsexp_def, - OPTION_CHOICE_EQUALS_OPTION, LENGTH_EQ_NUM_compute] + OPTION_CHOICE_EQUALS_OPTION, LENGTH_EQ_NUM_compute, explode_eq] QED Theorem idsexp_sexpid_odestSEXSTR'[simp]: @@ -1967,16 +1826,15 @@ Theorem typesexp_sexptype: (SOME t = sexptype s ⇔ typesexp t = s) Proof simp[EQ_SYM_EQ] >> - ho_match_mp_tac(theorem"sexptype_ind") - \\ simp[dstrip_sexp_SOME, LENGTH_EQ_NUM_compute, PULL_EXISTS] - \\ rw[] - \\ Cases_on ‘t’ - \\ simp[Once sexptype_def, EXISTS_PROD, dstrip_sexp_SOME, + ho_match_mp_tac (theorem"sexptype_ind") + >> simp[dstrip_sexp_SOME, LENGTH_EQ_NUM_compute, PULL_EXISTS] + >> rw[] + >> Cases_on `t` + >> simp[Once sexptype_def, EXISTS_PROD, dstrip_sexp_SOME, LENGTH_EQ_NUM_compute, PULL_EXISTS, OPTION_CHOICE_EQUALS_OPTION, OPTION_CHOICE_EQ_NONE, typesexp_def] - \\ eq_tac >> strip_tac >> gvs[] >> - gvs[sexplist_SOME] >> - gvs[sexplist_SOME, LIST_EQ_REWRITE,EL_MAP, sxMEM_def, PULL_EXISTS, MEM_EL] + >> eq_tac >> strip_tac >> gvs[explode_eq] >> + gvs[sexplist_SOME, LIST_EQ_REWRITE, EL_MAP, PULL_EXISTS, MEM_EL] QED Theorem patsexp_sexppat0: @@ -1988,10 +1846,10 @@ Proof Cases >> simp[OPTION_CHOICE_EQUALS_OPTION, OPTION_CHOICE_EQ_NONE, EXISTS_PROD, dstrip_sexp_SOME, patsexp_def, PULL_EXISTS, LENGTH_EQ_NUM_compute, - litsexp_sexplit, sexpopt_SOME, typesexp_sexptype] >> + litsexp_sexplit, sexpopt_SOME, typesexp_sexptype, explode_eq] >> rpt (gen_tac ORELSE disch_then strip_assume_tac) >> rw[] >> rw[optsexp_def] >> - gvs[sxMEM_def, PULL_EXISTS, sexplist_SOME, LIST_EQ_REWRITE, EL_MAP, MEM_EL] + gvs[PULL_EXISTS, sexplist_SOME, LIST_EQ_REWRITE, EL_MAP, MEM_EL] QED Theorem patsexp_sexppat: @@ -2020,28 +1878,25 @@ Theorem decode_prim_type_prim_typesexp: prim_typesexp prim_type = s0 Proof rw [oneline decode_prim_type_def, AllCaseEqs()] - \\ simp [prim_typesexp_def] \\ gvs [typesexp_sexptype] + \\ simp [prim_typesexp_def] QED Theorem opsexp_sexpop: sexpop s = SOME p ⇒ opsexp p = s Proof - Cases_on`s` \\ rw[sexpop_def] \\ rw[opsexp_def] - \\ rename [‘sexpop ⟪s1 • s2⟫ = SOME p’] - \\ Cases_on ‘s1’ \\ gvs[sexpop_def] - \\ Cases_on ‘s2’ - \\ gvs[sexpop_def, AllCaseEqs(), opsexp_def, encode_decode_control] - \\ gvs [encode_thunk_mode_def,decode_thunk_mode_def,AllCaseEqs(), + Cases_on `s` >> rw[sexpop_def] >> rw[opsexp_def] + >> gvs[sexpop_def, AllCaseEqs(), opsexp_def, encode_decode_control] + >> gvs [encode_thunk_mode_def,decode_thunk_mode_def,AllCaseEqs(), decode_test_testsexp,decode_prim_type_prim_typesexp, - sexparith_arithsexp] + sexparith_arithsexp, explode_eq, mlstringTheory.implode_def] QED Theorem locnsexp_sexplocpt0: sexplocpt s = SOME z ⇒ locnsexp z = s Proof - Cases_on ‘z’ >> Cases_on ‘s’ >> - simp[locnsexp_def,sexplocpt_def, AllCaseEqs(), PULL_EXISTS, - LENGTH_EQ_NUM_compute, listsexp_def] + Cases_on `z` >> Cases_on `s` >> + simp[locnsexp_def, sexplocpt_def, AllCaseEqs(), PULL_EXISTS, + LENGTH_EQ_NUM_compute] >> rw[] >> gvs[] QED Theorem locnsexp_sexplocpt[simp]: @@ -2051,13 +1906,20 @@ Proof metis_tac[locnsexp_sexplocpt0, sexplocpt_locnsexp] QED +Theorem locnsexp_sexplocn0: + sexplocn s = SOME z ⇒ locssexp z = s +Proof + Cases_on `z` >> Cases_on `s` >> + simp[sexplocn_def, locssexp_def, AllCaseEqs(), PULL_EXISTS, + LENGTH_EQ_NUM_compute] >> + rw[] >> gvs[] +QED + Theorem locnsexp_sexplocn: (sexplocn s = SOME z ⇔ locssexp z = s) ∧ (SOME z = sexplocn s ⇔ locssexp z = s) Proof - Cases_on`z` >> - simp[sexplocn_def, locssexp_def, listsexp_def, LENGTH_EQ_NUM_compute, - PULL_EXISTS] >> metis_tac[] + metis_tac[locnsexp_sexplocn0, sexplocn_locnsexp] QED Theorem logsexp_sexplog: @@ -2065,7 +1927,7 @@ Theorem logsexp_sexplog: (SOME z = sexplog s ⇔ logsexp z = s) Proof Cases_on`z` >> - simp[oneline sexplog_def, logsexp_def, listsexp_def, LENGTH_EQ_NUM_compute, + simp[oneline sexplog_def, logsexp_def, LENGTH_EQ_NUM_compute, PULL_EXISTS, AllCaseEqs()] QED @@ -2073,27 +1935,27 @@ Theorem expsexp_sexpexp: (sexpexp s = SOME e ⇔ expsexp e = s) ∧ (SOME e = sexpexp s ⇔ expsexp e = s) Proof - ‘∀s e. sexpexp s = SOME e ⇒ expsexp e = s’ + `∀s e. sexpexp s = SOME e ⇒ expsexp e = s` suffices_by metis_tac[sexpexp_expsexp] >> - ho_match_mp_tac (theorem"sexpexp_ind") >> + ho_match_mp_tac (theorem "sexpexp_ind") >> simp[OPTION_GUARD_EQ_THM, LENGTH_EQ_NUM_compute, PULL_EXISTS, dstrip_sexp_SOME] - \\ rpt gen_tac \\ strip_tac \\ gen_tac - \\ simp[Once sexpexp_def, EXISTS_PROD, dstrip_sexp_SOME, PULL_EXISTS] - \\ rpt gen_tac - \\ rename1 `guard (nm = "Raise" ∧ _) _` - \\ reverse (Cases_on `nm ∈ {"Raise"; "Handle"; "Lit"; "Con"; "Var"; "Fun"; + >> rpt gen_tac >> strip_tac >> gen_tac + >> simp[Once sexpexp_def, EXISTS_PROD, dstrip_sexp_SOME, PULL_EXISTS] + >> rpt gen_tac + >> rename1 `guard (nm = "Raise" ∧ _) _` + >> reverse (Cases_on `nm ∈ {"Raise"; "Handle"; "Lit"; "Con"; "Var"; "Fun"; "App"; "Log"; "If"; "Mat"; "Let"; "Letrec"; "Lannot"; "Tannot"}`) - \\ pop_assum mp_tac - \\ simp[] - \\ rw[] - \\ simp[expsexp_def] - \\ gvs[LENGTH_EQ_NUM_compute, listsexp_thm, litsexp_sexplit, opsexp_sexpop, + >> pop_assum mp_tac + >> simp[] + >> rw[] + >> simp[expsexp_def] + >> gvs[LENGTH_EQ_NUM_compute, litsexp_sexplit, opsexp_sexpop, idsexp_sexpid_odestSEXSTR, typesexp_sexptype, locnsexp_sexplocn, - OPTION_APPLY_MAP3, expsexp_def, arithsexp_sexparith, sexpopt_SOME, - optsexp_def,sexparith_arithsexp, logsexp_sexplog] >> - gvs[sexplist_SOME, sxMEM_def, EL_MAP, LIST_EQ_REWRITE, MEM_EL, PULL_EXISTS] >> + OPTION_APPLY_MAP3, expsexp_def, sexpopt_SOME, + optsexp_def, logsexp_sexplog] >> + gvs[sexplist_SOME, EL_MAP, LIST_EQ_REWRITE, MEM_EL, PULL_EXISTS] >> rw[] >> pairarg_tac >> first_x_assum drule >> simp[sexppair_SOME, PULL_EXISTS, patsexp_sexppat] >> metis_tac[] QED @@ -2103,7 +1965,7 @@ Theorem type_defsexp_sexptype_def: (SOME x = sexptype_def s ⇔ type_defsexp x = s) Proof simp[EQ_SYM_EQ] >> simp[EQ_IMP_THM] >> - rw[sexptype_def_def,type_defsexp_def] >> + rw[sexptype_def_def, type_defsexp_def] >> gvs[sexplist_SOME, LIST_EQ_REWRITE, EL_MAP, sexppair_SOME, PULL_EXISTS, EL_MAP, SF CONJ_ss, typesexp_sexptype] >> rpt strip_tac >> pairarg_tac >> simp[] >> @@ -2117,160 +1979,43 @@ Theorem decsexp_sexpdec: (sexpdec s = SOME d ⇔ decsexp d = s) ∧ (SOME d = sexpdec s ⇔ decsexp d = s) Proof - ‘∀s d. sexpdec s = SOME d ⇒ decsexp d = s’ - suffices_by metis_tac[sexpdec_decsexp]>> - ho_match_mp_tac(theorem"sexpdec_ind") - \\ ntac 3 strip_tac - \\ rw[Once sexpdec_def] - \\ pairarg_tac \\ gvs[dstrip_sexp_SOME] - \\ rename1 `guard (nm = _ ∧ _) _` - \\ Cases_on `nm ∈ {"Dlet"; "Dletrec"; "Dtype"; "Dtabbrev"; "Denv"; "Dexn"; "Dmod"}` - \\ fs[] - \\ fs[decsexp_def, LENGTH_EQ_NUM_compute] - \\ gvs[OPTION_APPLY_MAP3,OPTION_APPLY_MAP4,decsexp_def,expsexp_sexpexp, - locnsexp_sexplocn,patsexp_sexppat, type_defsexp_sexptype_def, - typesexp_sexptype] >> + `!s d. sexpdec s = SOME d ==> decsexp d = s` + suffices_by metis_tac[sexpdec_decsexp] >> + ho_match_mp_tac (theorem "sexpdec_ind") >> + ntac 3 strip_tac >> + rw[Once sexpdec_def] >> + pairarg_tac >> gvs[dstrip_sexp_SOME] >> + rename1 `guard (nm = _ ∧ _) _` >> + Cases_on `nm ∈ {"Dlet"; "Dletrec"; "Dtype"; "Dtabbrev"; "Denv"; "Dexn"; "Dmod"}` >> + fs[] >> + fs[decsexp_def, LENGTH_EQ_NUM_compute] >> + gvs[OPTION_APPLY_MAP3, OPTION_APPLY_MAP4, decsexp_def, expsexp_sexpexp, + locnsexp_sexplocn, patsexp_sexppat, type_defsexp_sexptype_def, + typesexp_sexptype] >> gvs[sexplist_SOME, LIST_EQ_REWRITE, EL_MAP, sexppair_SOME, PULL_EXISTS, - typesexp_sexptype, sxMEM_def, MEM_EL] >> + typesexp_sexptype, MEM_EL] >> rw[] >> pairarg_tac >> first_x_assum $ drule_then strip_assume_tac >> gvs[expsexp_sexpexp] QED -(* valid sexps *) - -Theorem SEXSTR_valid[simp]: - valid_sexp (SEXSTR s) -Proof - rw[SEXSTR_def,EVERY_isPrint_encode_control] -QED - -Theorem listsexp_valid: - ∀ls. EVERY valid_sexp ls ⇒ valid_sexp (listsexp ls) -Proof - Induct \\ simp[listsexp_def] \\ simp[GSYM listsexp_def] - \\ EVAL_TAC -QED - -Theorem idsexp_valid[simp]: - ∀i. valid_sexp (idsexp i) -Proof - Induct \\ REWRITE_TAC[idsexp_def] >> gen_tac >> - match_mp_tac listsexp_valid >> - simp[] \\ EVAL_TAC -QED - -Theorem typesexp_valid[simp]: - ∀t. valid_sexp (typesexp t) -Proof - ho_match_mp_tac(theorem"typesexp_ind") - \\ REWRITE_TAC[typesexp_def] >> rpt strip_tac - \\ match_mp_tac listsexp_valid - \\ simp[] - \\ rpt conj_tac - \\ TRY (match_mp_tac listsexp_valid) - \\ simp[EVERY_MAP,EVERY_MEM] - \\ EVAL_TAC -QED - -Theorem litsexp_valid[simp]: - ∀l. valid_sexp (litsexp l) -Proof - Cases \\ rw[litsexp_def] \\ EVAL_TAC -QED - -Theorem optsexp_valid: - ∀x. (∀y. x = SOME y ⇒ valid_sexp y) ⇒ valid_sexp (optsexp x) -Proof - Cases \\ rw[optsexp_def] \\ EVAL_TAC -QED - -Theorem patsexp_valid[simp]: - ∀p. valid_sexp (patsexp p) -Proof - ho_match_mp_tac(theorem"patsexp_ind") - \\ rw[patsexp_def] \\ simp[] \\ TRY (EVAL_TAC >> NO_TAC) - \\ (irule optsexp_valid ORELSE irule listsexp_valid) - \\ simp[PULL_EXISTS, EVERY_MEM, MEM_MAP] -QED - -Theorem type_defsexp_valid[simp]: - ∀t. valid_sexp (type_defsexp t) -Proof - rw[type_defsexp_def] - \\ match_mp_tac listsexp_valid - \\ rw[EVERY_MEM,EVERY_MAP] - \\ pairarg_tac \\ rw[] - \\ match_mp_tac listsexp_valid - \\ rw[EVERY_MEM,EVERY_MAP] - \\ pairarg_tac \\ rw[] - \\ match_mp_tac listsexp_valid - \\ rw[EVERY_MEM,EVERY_MAP] -QED - -Theorem valid_sexp_prim_typesexp[simp]: - ∀t. valid_sexp (prim_typesexp t) -Proof - Cases \\ EVAL_TAC \\ fs [] - \\ Cases_on ‘w’ \\ fs [] \\ EVAL_TAC -QED - -Theorem valid_sexp_arithsexp[local,simp]: - valid_sexp (arithsexp a) -Proof - Cases_on ‘a’ \\ EVAL_TAC -QED - -Theorem valid_sexp_logsexp[local,simp]: - valid_sexp (logsexp a) -Proof - Cases_on ‘a’ \\ EVAL_TAC -QED - -Theorem opsexp_valid[simp]: - ∀op. valid_sexp (opsexp op) -Proof - Cases \\ simp[opsexp_def] - \\ TRY (EVAL_TAC \\ NO_TAC) - \\ TRY(Cases_on`o'`) \\ simp[opsexp_def] - \\ TRY(Cases_on`w`) \\ simp[opsexp_def] - \\ TRY(Cases_on`s`) \\ simp[opsexp_def] - \\ TRY(Cases_on`f`) \\ simp[opsexp_def] - \\ TRY(Cases_on`r`) \\ simp[opsexp_def] - \\ TRY(Cases_on`t`) \\ simp[opsexp_def] - \\ TRY(Cases_on`t'`) \\ simp[encode_thunk_mode_def] - \\ TRY(Cases_on`b`) \\ simp[opsexp_def] - \\ EVAL_TAC - \\ TRY (rename [‘Compare oo’] \\ Cases_on ‘oo’ \\ EVAL_TAC) - \\ TRY (rename [‘AltCompare oo’] \\ Cases_on ‘oo’ \\ EVAL_TAC) -QED - -Theorem locnsexp_valid[simp]: - ∀p. valid_sexp (locnsexp p) +Theorem listsexp_MAP_EQ_f: + (∀x. MEM x ls ⇒ f1 x = f2 x) ⇒ + listsexp (MAP f1 ls) = listsexp (MAP f2 ls) Proof - Cases >> simp[locnsexp_def] >> EVAL_TAC + simp[MAP_CONG] QED -Theorem locssexp_valid[simp]: - ∀l. valid_sexp (locssexp l) +Theorem sexplist_listsexp_imp: + sexplist f (Expr l1) = SOME l2 ⇒ + ∀n. n < LENGTH l1 ⇒ f (EL n l1) = SOME (EL n l2) Proof - Cases \\ simp[locssexp_def, listsexp_valid] \\ EVAL_TAC + qid_spec_tac`l2`>> Induct_on`l1`>> simp[PULL_EXISTS, LT_SUC, DISJ_IMP_THM] QED -Theorem expsexp_valid[simp]: - ∀e. valid_sexp (expsexp e) +Theorem odestSXNUM_EQ_SOME[simp]: + (odestSXNUM s = SOME n ⇔ s = SXNUM n) ∧ + (SOME n = odestSXNUM s ⇔ s = SXNUM n) Proof - ho_match_mp_tac(theorem"expsexp_ind") - \\ rw[expsexp_def] \\ TRY (EVAL_TAC \\ NO_TAC) - \\ (irule listsexp_valid ORELSE irule optsexp_valid) - \\ simp[EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD] - \\ first_x_assum MATCH_ACCEPT_TAC + simp[odestSXNUM_SOME] QED -Theorem decsexp_valid[simp]: - ∀d. valid_sexp (decsexp d) -Proof - ho_match_mp_tac dec_ind \\ rw[decsexp_def] \\ TRY (EVAL_TAC \\ NO_TAC) - \\ match_mp_tac listsexp_valid - \\ rw[] - \\ simp[EVERY_MAP,EVERY_MEM, FORALL_PROD] -QED From 41e62c1905c250676e51028b664ccccbc0636ac0 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Fri, 20 Feb 2026 12:36:49 +0800 Subject: [PATCH 02/14] Replace simpleSexpParse with mlsexp in compiler integration Use mlsexp$fromString instead of parse_sexp for sexp input parsing, and sexp_to_string instead of print_sexp for sexp output. Remove simpleSexpParse ancestor and formal-languages/context-free includes from compiler, scheme, and dafny Holmakefiles. Co-Authored-By: Claude Opus 4.6 --- compiler/Holmakefile | 3 +-- compiler/compilerScript.sml | 11 ++++------- compiler/dafny/dafny_compilerScript.sml | 10 +++------- compiler/scheme/Holmakefile | 3 +-- compiler/scheme/proofs/Holmakefile | 1 - compiler/scheme/scheme_compilerScript.sml | 6 +++--- 6 files changed, 12 insertions(+), 22 deletions(-) diff --git a/compiler/Holmakefile b/compiler/Holmakefile index b5dbefd497..50d9f81908 100644 --- a/compiler/Holmakefile +++ b/compiler/Holmakefile @@ -1,5 +1,4 @@ -INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\ - $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\ +INCLUDES = $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\ $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis $(CAKEMLDIR)/characteristic\ $(CAKEMLDIR)/pancake\ $(CAKEMLDIR)/pancake/parser\ diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index 9dc66689a7..f45f41bb80 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -7,7 +7,7 @@ Theory compiler Ancestors lexer_fun lexer_impl cmlParse infer backend backend_passes - mlint mlstring basisProg fromSexp simpleSexpParse x64_config + mlint mlstring basisProg fromSexp x64_config export_x64 arm8_config export_arm8 riscv_config export_riscv mips_config export_mips arm7_config export_arm7 ag32_config export_ag32 panPtreeConversion pan_to_target panStatic @@ -221,13 +221,10 @@ Definition locs_to_string_def: | _ => implode "unknown location") End -(* this is a rather annoying feature of peg_exec requiring locs... *) -Overload add_locs = ``MAP (λc. (c,unknown_loc))`` - Definition parse_sexp_input_def: parse_sexp_input input = let err = strlit "Parsing of sexp syntax failed" in - case parse_sexp (add_locs input) of + case mlsexp$fromString (implode input) of | NONE => INL err | SOME x => case sexplist sexpdec x of | NONE => INL err @@ -268,8 +265,8 @@ Definition compile_def: inf_env_to_types_string ic ++ [strlit "\n"]))), Nil) else if c.only_print_sexp then - (Failure (TypeError (implode - ("\n" ++ print_sexp (listsexp (MAP decsexp full_prog))))),Nil) + (Failure (TypeError (concat [strlit "\n"; + sexp_to_string (listsexp (MAP decsexp full_prog))])),Nil) else case backend_passes$compile_tap c.asm_config c.backend_config full_prog of | (NONE, td) => (Failure AssembleError, td) diff --git a/compiler/dafny/dafny_compilerScript.sml b/compiler/dafny/dafny_compilerScript.sml index aa146e2f8e..46e408b0e8 100644 --- a/compiler/dafny/dafny_compilerScript.sml +++ b/compiler/dafny/dafny_compilerScript.sml @@ -4,7 +4,7 @@ Theory dafny_compiler Ancestors result_monad sexp_to_dafny dafny_to_cakeml - dafny_freshen dafny_remove_assert fromSexp simpleSexpParse + dafny_freshen dafny_remove_assert fromSexp Libs preamble @@ -39,14 +39,10 @@ Definition cmlm_to_str_def: cml = unpack cmlm; cml_sexp = listsexp (MAP decsexp cml); in - print_sexp cml_sexp + sexp_to_string cml_sexp End Definition main_function_def: main_function (sexp: mlsexp$sexp): mlstring = - let - cmlm = dfy_to_cml sexp; - cml_str = cmlm_to_str cmlm; - in - implode cml_str + cmlm_to_str (dfy_to_cml sexp) End diff --git a/compiler/scheme/Holmakefile b/compiler/scheme/Holmakefile index 4f9d1adf09..10494e3bf1 100644 --- a/compiler/scheme/Holmakefile +++ b/compiler/scheme/Holmakefile @@ -3,8 +3,7 @@ INCLUDES = $(CAKEMLDIR)/translator \ $(CAKEMLDIR)/basis/pure \ $(CAKEMLDIR)/compiler/parsing \ $(CAKEMLDIR)/semantics \ - $(CAKEMLDIR)/misc \ - $(HOLDIR)/examples/formal-languages/context-free + $(CAKEMLDIR)/misc all: $(DEFAULT_TARGETS) README.md .PHONY: all diff --git a/compiler/scheme/proofs/Holmakefile b/compiler/scheme/proofs/Holmakefile index 520fa3404a..8f85579cfb 100644 --- a/compiler/scheme/proofs/Holmakefile +++ b/compiler/scheme/proofs/Holmakefile @@ -6,7 +6,6 @@ INCLUDES = $(CAKEMLDIR)/translator \ $(CAKEMLDIR)/semantics \ $(CAKEMLDIR)/semantics/proofs \ $(CAKEMLDIR)/misc \ - $(HOLDIR)/examples/formal-languages/context-free \ $(CAKEMLDIR)/compiler/scheme all: $(DEFAULT_TARGETS) README.md diff --git a/compiler/scheme/scheme_compilerScript.sml b/compiler/scheme/scheme_compilerScript.sml index edc1026dcc..45ac0cef73 100644 --- a/compiler/scheme/scheme_compilerScript.sml +++ b/compiler/scheme/scheme_compilerScript.sml @@ -3,14 +3,14 @@ *) Theory scheme_compiler Ancestors - fromSexp simpleSexpParse scheme_ast scheme_parsing + fromSexp scheme_ast scheme_parsing scheme_to_cake Libs preamble Definition cake_prog_to_string_def: cake_prog_to_string ast = - print_sexp (listsexp (MAP decsexp ast)) + sexp_to_string (listsexp (MAP decsexp ast)) End Definition cake_for_err_def: @@ -37,5 +37,5 @@ EVAL “compile "(print hi)"” *) Definition main_function_def: - main_function s = implode (compile (explode s)) + main_function s = compile (explode s) End From 822c744fdfa3d3336b3946f0b28719eb3b332113 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Fri, 20 Feb 2026 13:23:14 +0800 Subject: [PATCH 03/14] Remove simpleSexp translations from bootstrap/dafny/scheme translation files SexpProg (in basis/) already translates the mlsexp parser/printer to CakeML, so the translation files no longer need to translate simpleSexp's PEG parser, printer, or destructor functions. Remove ~300 lines of now-unnecessary code. Co-Authored-By: Claude Opus 4.6 --- compiler/bootstrap/translation/Holmakefile | 3 +- .../translation/sexp_parserProgScript.sml | 168 +----------------- .../translation/dafny_compilerProgScript.sml | 140 +-------------- .../scheme/translation/to_sexpProgScript.sml | 7 +- 4 files changed, 15 insertions(+), 303 deletions(-) diff --git a/compiler/bootstrap/translation/Holmakefile b/compiler/bootstrap/translation/Holmakefile index afb45abb53..6bbefb5ea0 100644 --- a/compiler/bootstrap/translation/Holmakefile +++ b/compiler/bootstrap/translation/Holmakefile @@ -1,5 +1,4 @@ -INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\ - $(CAKEMLDIR)/misc\ +INCLUDES = $(CAKEMLDIR)/misc\ $(CAKEMLDIR)/basis\ $(CAKEMLDIR)/characteristic\ $(CAKEMLDIR)/pancake/parser\ diff --git a/compiler/bootstrap/translation/sexp_parserProgScript.sml b/compiler/bootstrap/translation/sexp_parserProgScript.sml index 2388ccfb4a..066bca898e 100644 --- a/compiler/bootstrap/translation/sexp_parserProgScript.sml +++ b/compiler/bootstrap/translation/sexp_parserProgScript.sml @@ -1,16 +1,15 @@ (* - Translate the alternative s-expression parser. + Translate the s-expression parser and fromSexp functions. *) Theory sexp_parserProg Ancestors - decodeProg ml_translator peg simpleSexp simpleSexpPEG - simpleSexpParse fromSexp + decodeProg ml_translator fromSexp Libs preamble ml_translatorLib open preamble decodeProgTheory ml_translatorLib ml_translatorTheory - pegTheory simpleSexpTheory simpleSexpPEGTheory simpleSexpParseTheory fromSexpTheory; + fromSexpTheory; val _ = temp_delsimps ["NORMEQ_CONV"] @@ -28,67 +27,11 @@ Proof QED (* -- *) -val r = translate simpleSexpPEGTheory.pnt_def -val r = translate pegTheory.ignoreR_def -val r = translate pegTheory.ignoreL_def -val r = translate simpleSexpTheory.arb_sexp_def -val r = translate simpleSexpPEGTheory.sumID_def -val r = translate simpleSexpPEGTheory.choicel_def - -val r = translate simpleSexpPEGTheory.tokeq_def -val r = translate simpleSexpPEGTheory.pegf_def -val r = translate simpleSexpPEGTheory.grabWS_def -val r = translate simpleSexpPEGTheory.replace_nil_def -val r = translate simpleSexpTheory.destSXNUM_def -val r = translate simpleSexpTheory.destSXCONS_def -val r = translate simpleSexpTheory.destSXSYM_def -val r = translate stringTheory.isPrint_def -val r = translate stringTheory.isGraph_def -val r = translate (simpleSexpTheory.valid_first_symchar_def - |> SIMP_RULE std_ss [IN_INSERT,NOT_IN_EMPTY]) -val r = translate (simpleSexpTheory.valid_symchar_def - |> SIMP_RULE std_ss [IN_INSERT,NOT_IN_EMPTY]) -val r = translate pairTheory.PAIR_MAP_THM; (* TODO: isn't this done earlier? *) -val r = translate simpleSexpPEGTheory.sexpPEG_def -val () = next_ml_names := ["destResult"]; -val r = translate pegexecTheory.destResult_def - -val r = - simpleSexpParseTheory.parse_sexp_def - |> SIMP_RULE std_ss[monad_unitbind_assert,OPTION_BIND_THM, - pegexecTheory.pegparse_def, - simpleSexpPEGTheory.wfG_sexpPEG,UNCURRY,GSYM NULL_EQ] - |> translate; - -val parse_sexp_side = Q.prove( - `∀x. parse_sexp_side x = T`, - simp[definition"parse_sexp_side_def", - parserProgTheory.peg_exec_side_def, - parserProgTheory.coreloop_side_def] \\ - qx_gen_tac`i` \\ - (MATCH_MP pegexecTheory.peg_exec_total simpleSexpPEGTheory.wfG_sexpPEG |> strip_assume_tac) - \\ fs[definition"destresult_1_side_def"] \\ - (MATCH_MP pegexecTheory.coreloop_total simpleSexpPEGTheory.wfG_sexpPEG |> strip_assume_tac) - \\ fs[pegexecTheory.coreloop_def] - \\ qmatch_abbrev_tac`IS_SOME (OWHILE a b c)` - \\ qmatch_assum_abbrev_tac`OWHILE a b' c = _` - \\ qsuff_tac `b = b'` THEN1 fs [] - \\ simp[Abbr`b`,Abbr`b'`,FUN_EQ_THM] - \\ rpt gen_tac - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[] - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[] - \\ Cases_on ‘k’ \\ TRY (fs [] \\ NO_TAC) - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[] - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[] - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[] - \\ TOP_CASE_TAC \\ simp[FLOOKUP_DEF] \\ rw[]) |> update_precondition; - val r = fromSexpTheory.sexplist_def |> SIMP_RULE std_ss [OPTION_BIND_THM] |> translate; -val r = translate simpleSexpTheory.strip_sxcons_def -val r = translate simpleSexpTheory.dstrip_sexp_def +val r = translate fromSexpTheory.dstrip_sexp_def (* TODO: move (used?) *) @@ -122,8 +65,7 @@ Theorem isHexDigit_UNHEX_LESS: isHexDigit c ⇒ UNHEX c < 16 Proof rw[isHexDigit_cases] \\ EVAL_TAC \\ - rw[GSYM simpleSexpParseTheory.isDigit_UNHEX_alt] \\ - fs[isDigit_def] + fs[isDigit_def, ASCIInumbersTheory.UNHEX_def] QED Theorem num_from_hex_string_alt_length_2: @@ -240,17 +182,6 @@ val r = fromSexpTheory.sexptype_def_def val r = translate optionTheory.OPTION_APPLY_def; -(* -val r = fromSexpTheory.sexpspec_def - |> SIMP_RULE std_ss [OPTION_BIND_THM,monad_unitbind_assert,sexptype_alt_intro1] - |> translate; - -val sexpspec_side = Q.prove( - `∀x. sexpspec_side x = T`, - EVAL_TAC \\ rw[] \\ strip_tac \\ fs[]) - |> update_precondition; -*) - val r = fromSexpTheory.sexpopt_def |> SIMP_RULE std_ss [OPTION_BIND_THM,monad_unitbind_assert] |> translate; @@ -299,94 +230,7 @@ val sexpdec_alt_side = Q.prove( \\ fs[LENGTH_EQ_NUM_compute]) |> update_precondition; -Theorem strip_dot_alt = - simpleSexpParseTheory.strip_dot_def |> PURE_ONCE_REWRITE_RULE [CONS_APPEND]; -val _ = translate strip_dot_alt - -val _ = translate simpleSexpParseTheory.print_space_separated_def; - -val _ = translate simpleSexpParseTheory.escape_string_def; - - -(* TODO: translator failed for some reason if I just prove these as equations on print_sexp *) -Definition print_sexp_alt_def: - (print_sexp_alt (SX_SYM s) = s) ∧ - (print_sexp_alt (SX_NUM n) = explode (toString n)) ∧ - (print_sexp_alt (SX_STR s) = "\"" ++ IMPLODE(escape_string s) ++ "\"") ∧ - (print_sexp_alt s = - let (ls,n) = strip_dot s in - case n of - | NONE => - if LENGTH ls = 2 ∧ HD ls = SX_SYM "quote" - then "'" ++ print_sexp_alt (EL 1 ls) - else "(" ++ print_space_separated (MAP print_sexp_alt ls) ++ ")" - | SOME lst => - "(" ++ print_space_separated (MAP print_sexp_alt ls) ++ " . " ++ print_sexp_alt lst ++ ")") -Termination - WF_REL_TAC`measure sexp_size` >> rw[] >> simp[simpleSexpTheory.sexp_size_def] >> - fs[Once simpleSexpParseTheory.strip_dot_def] >> - pairarg_tac \\ fs[] \\ rw[simpleSexpTheory.sexp_size_def] \\ fs[] - \\ imp_res_tac simpleSexpParseTheory.strip_dot_MEM_sizelt - \\ imp_res_tac simpleSexpParseTheory.strip_dot_last_sizeleq - \\ fsrw_tac[boolSimps.DNF_ss][] \\ simp[] - \\ fs[LENGTH_EQ_NUM_compute] \\ rw[] \\ fs[] - \\ res_tac \\ simp[] -End - -Theorem strip_dot_EQ_NILSOME: - strip_dot s = ([], SOME x) ⇒ s = x -Proof - Cases_on ‘s’ >> simp[AllCaseEqs()] >> pairarg_tac >> simp[] -QED - -Theorem toString_toString_explode: - toString n = explode (toString (n:num)) -Proof - simp[mlintTheory.num_to_str_thm] -QED - -Theorem print_sexp_alt_thm: - print_sexp s = print_sexp_alt s -Proof - `?n. n = sexp_size s` by rw[] >> - pop_assum mp_tac >> - qid_spec_tac `s` >> qid_spec_tac `n` >> - ho_match_mp_tac COMPLETE_INDUCTION >> - rpt strip_tac >> Cases_on `s` >> - fs[simpleSexpParseTheory.print_sexp_def,print_sexp_alt_def,IMPLODE_EXPLODE_I, - sexp_size_def, PULL_FORALL,toString_toString_explode] >> - pairarg_tac >> fs[] >> every_case_tac >> - gvs[STRCAT_11, LENGTH_EQ_NUM_compute, PULL_EXISTS] >> - pairarg_tac >> gvs[] - >- (first_x_assum irule >> dxrule strip_dot_MEM_sizelt >> simp[]) - >- (drule strip_dot_last_sizelt >> dxrule strip_dot_MEM_sizelt >> simp[]) - >- (dxrule strip_dot_MEM_sizelt >> - disch_then (C (resolve_then Any assume_tac) - (DECIDE “x < y ⇒ x < a + (y + 1n)”)) >> - pop_assum (first_assum o resolve_then Any assume_tac) >> - simp[Cong MAP_CONG] >> simp[SF ETA_ss]) - >- (drule strip_dot_last_sizelt >> drule strip_dot_MEM_sizelt >> simp[] >> - rename [‘strip_dot s0 = (els, SOME _)’] >> - Cases_on ‘NULL els’ >> gs[] >> - disch_then (C (resolve_then Any assume_tac) - (DECIDE “x < y ⇒ x < a + (y + 1n)”)) >> - pop_assum (first_assum o resolve_then Any assume_tac) >> - simp[Cong MAP_CONG] >> simp[SF ETA_ss] >> - Cases_on ‘els’ >> gs[] >> - dxrule strip_dot_EQ_NILSOME >> simp[]) -QED - -val _ = translate print_sexp_alt_def; - -val _ = translate print_sexp_alt_thm; - -Theorem listsexp_alt[local]: - listsexp = FOLDR (λs1 s2. SX_CONS s1 s2) nil -Proof - rpt(CHANGED_TAC(CONV_TAC (DEPTH_CONV ETA_CONV))) >> simp[listsexp_def] -QED - -val _ = translate listsexp_alt +val _ = translate fromSexpTheory.listsexp_def; val _ = translate (locnsexp_def |> SIMP_RULE list_ss []); diff --git a/compiler/dafny/translation/dafny_compilerProgScript.sml b/compiler/dafny/translation/dafny_compilerProgScript.sml index ebbbf703b4..e3229fe389 100644 --- a/compiler/dafny/translation/dafny_compilerProgScript.sml +++ b/compiler/dafny/translation/dafny_compilerProgScript.sml @@ -4,143 +4,24 @@ Theory dafny_compilerProg Ancestors dafny_remove_assertProg dafny_compiler - fromSexp (* listsexp *) - string numposrep simpleSexp ml_translator simpleSexpParse + fromSexp Libs preamble ml_translatorLib basisFunctionsLib val _ = translation_extends "dafny_remove_assertProg"; -(* First, we translate the functions for converting the output of the compiler - (CakeML AST) into an S-expression string, namely decsexp, listsexp, and - print_sexp *) - -(* Adapted from compiler/bootstrap/translation/sexp_parserProgScript.sml *) - -(* Note that we keep turning on and off use_string_type. This appears to be - necessary to avoid weird translation problems, especially starting with the - translation of litsexp_def for some reason, which is also where the on/offs - start to differ from sexp_parserProg. The downside is, that this seems to - introduce *a lot* of automatic additions of IMPLODE sometimes; see TODOs. *) - -val _ = ml_translatorLib.use_string_type true; val _ = ml_translatorLib.use_sub_check true; val _ = add_preferred_thy "-"; -val r = translate stringTheory.isPrint_def; - -Theorem strip_dot_alt = - simpleSexpParseTheory.strip_dot_def |> PURE_ONCE_REWRITE_RULE [CONS_APPEND]; - -val r = translate strip_dot_alt; - -val r = translate simpleSexpParseTheory.print_space_separated_def; - -val _ = use_string_type false; -val r = translate simpleSexpParseTheory.escape_string_def; -val _ = use_string_type true; - -Theorem num_to_dec_string_v_thm: - (NUM --> HOL_STRING_TYPE) toString ^(IntProgTheory.tostring_v_thm |> concl |> rand) -Proof - assume_tac IntProgTheory.tostring_v_thm >> - fs[NUM_def,Arrow_def,HOL_STRING_TYPE_def,INT_def,AppReturns_def, - GSYM mlintTheory.num_to_str_thm,mlintTheory.num_to_str_def] -QED +(* fromSexp encoder translations *) -val _ = add_user_proved_v_thm num_to_dec_string_v_thm; - -(* The following TODO was copied over from sexp_parserProgScript.sml *) -(* TODO: translator failed for some reason if I just prove these as equations on print_sexp *) -Definition print_sexp_alt_def: - (print_sexp_alt (SX_SYM s) = s) ∧ - (print_sexp_alt (SX_NUM n) = toString n) ∧ - (print_sexp_alt (SX_STR s) = "\"" ++ IMPLODE(escape_string s) ++ "\"") ∧ - (print_sexp_alt s = - let (ls,n) = strip_dot s in - case n of - | NONE => - if LENGTH ls = 2 ∧ HD ls = SX_SYM "quote" - then "'" ++ print_sexp_alt (EL 1 ls) - else "(" ++ print_space_separated (MAP print_sexp_alt ls) ++ ")" - | SOME lst => - "(" ++ print_space_separated (MAP print_sexp_alt ls) ++ " . " ++ print_sexp_alt lst ++ ")") -Termination - WF_REL_TAC‘measure sexp_size’ >> rw[] >> simp[simpleSexpTheory.sexp_size_def] >> - fs[Once simpleSexpParseTheory.strip_dot_def] >> - pairarg_tac \\ fs[] \\ rw[simpleSexpTheory.sexp_size_def] \\ fs[] - \\ imp_res_tac simpleSexpParseTheory.strip_dot_MEM_sizelt - \\ imp_res_tac simpleSexpParseTheory.strip_dot_last_sizeleq - \\ fsrw_tac[boolSimps.DNF_ss][] \\ simp[] - \\ fs[LENGTH_EQ_NUM_compute] \\ rw[] \\ fs[] - \\ res_tac \\ simp[] -End - -Theorem strip_dot_EQ_NILSOME: - strip_dot s = ([], SOME x) ⇒ s = x -Proof - Cases_on ‘s’ >> simp[AllCaseEqs()] >> pairarg_tac >> simp[] -QED - -Theorem print_sexp_alt_thm: - print_sexp s = print_sexp_alt s -Proof - ‘∃n. n = sexp_size s’ by rw[] >> - pop_assum mp_tac >> - qid_spec_tac ‘s’ >> qid_spec_tac ‘n’ >> - ho_match_mp_tac COMPLETE_INDUCTION >> - rpt strip_tac >> Cases_on ‘s’ >> - fs[simpleSexpParseTheory.print_sexp_def,print_sexp_alt_def,IMPLODE_EXPLODE_I, - sexp_size_def, PULL_FORALL] >> - pairarg_tac >> fs[] >> every_case_tac >> - gvs[STRCAT_11, LENGTH_EQ_NUM_compute, PULL_EXISTS] >> - pairarg_tac >> gvs[] - >- (first_x_assum irule >> dxrule strip_dot_MEM_sizelt >> simp[]) - >- (drule strip_dot_last_sizelt >> dxrule strip_dot_MEM_sizelt >> simp[]) - >- (dxrule strip_dot_MEM_sizelt >> - disch_then (C (resolve_then Any assume_tac) - (DECIDE “x < y ⇒ x < a + (y + 1n)”)) >> - pop_assum (first_assum o resolve_then Any assume_tac) >> - simp[Cong MAP_CONG] >> simp[SF ETA_ss]) - >- (drule strip_dot_last_sizelt >> drule strip_dot_MEM_sizelt >> simp[] >> - rename [‘strip_dot s0 = (els, SOME _)’] >> - Cases_on ‘NULL els’ >> gs[] >> - disch_then (C (resolve_then Any assume_tac) - (DECIDE “x < y ⇒ x < a + (y + 1n)”)) >> - pop_assum (first_assum o resolve_then Any assume_tac) >> - simp[Cong MAP_CONG] >> simp[SF ETA_ss] >> - Cases_on ‘els’ >> gs[] >> - dxrule strip_dot_EQ_NILSOME >> simp[]) -QED - -val r = translate EL; - -Theorem el_side_thm[local]: - ∀n xs. el_side n xs = (n < LENGTH xs) -Proof - Induct THEN Cases_on ‘xs’ THEN ONCE_REWRITE_TAC [fetch "-" "el_side_def"] - THEN fs[] -QED - -val _ = el_side_thm |> update_precondition; - -val r = translate print_sexp_alt_def; - -val r = translate print_sexp_alt_thm; - -val _ = use_string_type false; - -Theorem listsexp_alt[local]: - listsexp = FOLDR (λs1 s2. SX_CONS s1 s2) nil -Proof - rpt(CHANGED_TAC(CONV_TAC (DEPTH_CONV ETA_CONV))) >> simp[listsexp_def] -QED - -val r = translate listsexp_alt; +val r = translate fromSexpTheory.listsexp_def; val r = translate (fromSexpTheory.locnsexp_def |> SIMP_RULE list_ss []); val r = translate fromSexpTheory.locssexp_def; +val r = translate stringTheory.isPrint_def; + val r = translate ASCIInumbersTheory.HEX_def; Definition hex_alt_def: @@ -209,8 +90,6 @@ val r = translate fromSexpTheory.encode_control_def; val r = translate fromSexpTheory.SEXSTR_def; -val _ = ml_translatorLib.use_string_type false; - val r = translate fromSexpTheory.litsexp_def; Theorem litsexp_side_thm[local]: @@ -227,16 +106,13 @@ val r = translate fromSexpTheory.idsexp_def; val r = translate fromSexpTheory.typesexp_def; val r = translate fromSexpTheory.patsexp_def; val r = translate fromSexpTheory.encode_thunk_mode_def; -(* TODO 101 automatically added string IMPLODEs *) val r = translate fromSexpTheory.prim_typesexp_def; val r = translate fromSexpTheory.testsexp_def; val r = translate fromSexpTheory.arithsexp_def; val r = translate fromSexpTheory.opsexp_def; val r = translate fromSexpTheory.logsexp_def; -(* TODO 24 automatically added string IMPLODEs *) val r = translate fromSexpTheory.expsexp_def; val r = translate fromSexpTheory.type_defsexp_def; -(* TODO 14 automatically added string IMPLODEs *) val r = translate fromSexpTheory.decsexp_def; (* Translating dafny_compilerTheory *) @@ -246,13 +122,11 @@ val r = translate dafny_compilerTheory.dfy_to_cml_def; val r = translate dafny_compilerTheory.unpack_def; val r = translate dafny_compilerTheory.cmlm_to_str_def; -val _ = ml_translatorLib.use_string_type true; - val r = translate dafny_compilerTheory.main_function_def; (* Sanity checks + Finalizing *) -val _ = type_of “main_function” = “:mlsexp$sexp -> mlstring” +val _ = type_of "main_function" = ":mlsexp$sexp -> mlstring" orelse failwith "The main_function has the wrong type."; val _ = r |> hyp |> null orelse @@ -270,7 +144,7 @@ val prog = |> ml_progLib.get_thm |> REWRITE_RULE [ml_progTheory.ML_code_def] |> concl |> rator |> rator |> rand - |> (fn tm => “^tm ++ ^main”) + |> (fn tm => "^tm ++ ^main") |> EVAL |> concl |> rand; Definition dafny_compiler_prog_def: diff --git a/compiler/scheme/translation/to_sexpProgScript.sml b/compiler/scheme/translation/to_sexpProgScript.sml index ac142c2481..084513b693 100644 --- a/compiler/scheme/translation/to_sexpProgScript.sml +++ b/compiler/scheme/translation/to_sexpProgScript.sml @@ -3,7 +3,7 @@ *) Theory to_sexpProg Ancestors - ast fromSexp simpleSexpParse + ast fromSexp Libs preamble basis @@ -17,11 +17,6 @@ val r = translate numposrepTheory.n2l_def; val r = translate ASCIInumbersTheory.n2s_def; val r = translate ASCIInumbersTheory.HEX_def; val r = translate ASCIInumbersTheory.num_to_dec_string_def; -val r = translate simpleSexpParseTheory.print_space_separated_def; -val r = translate simpleSexpParseTheory.strip_dot_def; -val r = translate simpleSexpParseTheory.escape_string_def; -val r = translate listTheory.EL; -val r = translate simpleSexpParseTheory.print_sexp_def; val r = translate fromSexpTheory.listsexp_def; val r = translate fromSexpTheory.locnsexp_def; val r = translate fromSexpTheory.locssexp_def; From 5276b34f55aaa6ebadee122d7e378d18ab237bc7 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Fri, 5 Jun 2026 18:44:55 +0800 Subject: [PATCH 04/14] Fix fromSexpTheory after simpleSexp -> mlsexp switch The rewritten proofs referenced mlstringTheory.implode_def, which no longer exists now that mlstring's constructor is `implode` (with `strlit` an inferior overload of it). Those references caused static errors that aborted the theory. Since `strlit = implode` is definitional, the implode_def rewrite was a no-op; the affected proofs close with the existing implode_explode/explode_implode lemmas. Also fixes the Char witness in litsexp_sexplit: `str c` (a string) -> `implode [c]` (the correct mlstring). fromSexpTheory now builds with all proofs complete. Co-Authored-By: Claude Opus 4.8 (1M context) --- compiler/parsing/fromSexpScript.sml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml index 5a327a7f46..f2b0c91b8b 100644 --- a/compiler/parsing/fromSexpScript.sml +++ b/compiler/parsing/fromSexpScript.sml @@ -334,9 +334,8 @@ Theorem explode_eq: (explode tag = s ⇔ tag = strlit s) ∧ (s = explode tag ⇔ strlit s = tag) Proof - simp[mlstringTheory.implode_def, EQ_IMP_THM] >> - metis_tac[mlstringTheory.implode_explode, mlstringTheory.explode_implode, - mlstringTheory.implode_def] + simp[EQ_IMP_THM] >> + metis_tac[mlstringTheory.implode_explode, mlstringTheory.explode_implode] QED Theorem dstrip_sexp_SOME: @@ -347,7 +346,7 @@ Proof Cases_on `l` >> simp[dstrip_sexp_def] >> Cases_on `h` >> simp[dstrip_sexp_def] >> rw[EQ_IMP_THM] >> gvs[explode_eq] >> - metis_tac[mlstringTheory.implode_explode, mlstringTheory.implode_def] + metis_tac[mlstringTheory.implode_explode] QED Theorem dstrip_sexp_listsexp[simp]: @@ -1619,7 +1618,7 @@ QED Theorem sexplit_litsexp[simp]: sexplit (litsexp l) = SOME l Proof - Cases_on `l` >> simp[sexplit_def,litsexp_def,mlstringTheory.implode_def] >> + Cases_on `l` >> simp[sexplit_def,litsexp_def] >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_8] >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_64] >> simp[wordsTheory.w2n_lt] @@ -1753,7 +1752,7 @@ Proof simp[dstrip_sexp_SOME, PULL_EXISTS, LENGTH_EQ_NUM_compute] >> rw[EQ_IMP_THM] >> gvs[] >> `tag = implode (explode tag)` by simp[mlstringTheory.implode_explode] >> - pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] >> simp[mlstringTheory.implode_def] + pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] QED Theorem sexplist_SOME: @@ -1778,7 +1777,7 @@ Theorem OPTION_CHOICE_EQ_SOME = OPTION_CHOICE_EQUALS_OPTION val tag_tac = `tag = implode (explode tag)` by simp[mlstringTheory.implode_explode] >> - pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] >> simp[mlstringTheory.implode_def] + pop_assum SUBST1_TAC >> ASM_REWRITE_TAC[] Theorem litsexp_sexplit: (sexplit s = SOME l ⇔ litsexp l = s) ∧ @@ -1791,7 +1790,7 @@ Proof rpt gen_tac >> eq_tac >> rpt strip_tac >> gvs[litsexp_def] (* backward direction *) >- (Cases_on `l` >> simp[litsexp_def] >- - (qexists_tac `str c` >> simp[] >> EVAL_TAC) >> + (qexists_tac `implode [c]` >> simp[]) >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_8] >> ONCE_REWRITE_TAC[GSYM wordsTheory.dimword_64] >> simp[wordsTheory.w2n_lt]) @@ -1888,7 +1887,7 @@ Proof >> gvs[sexpop_def, AllCaseEqs(), opsexp_def, encode_decode_control] >> gvs [encode_thunk_mode_def,decode_thunk_mode_def,AllCaseEqs(), decode_test_testsexp,decode_prim_type_prim_typesexp, - sexparith_arithsexp, explode_eq, mlstringTheory.implode_def] + sexparith_arithsexp, explode_eq] QED Theorem locnsexp_sexplocpt0: From 47675dbfa7f6b1d06d01229fb18fc6c60a4da678 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 14:25:35 +0800 Subject: [PATCH 05/14] Fix to_sexpProg after simpleSexp -> mlsexp switch SXNUM is now an ordinary smart-constructor definition (SXNUM n = Atom (toString (&n))) rather than a simpleSexp datatype constructor, so the translator no longer handles it automatically. Translate fromSexpTheory.SXNUM_def before locnsexp_def (its first use) so the encoder translations close. to_sexpProgTheory now builds. Co-Authored-By: Claude Opus 4.8 (1M context) --- compiler/scheme/translation/to_sexpProgScript.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/compiler/scheme/translation/to_sexpProgScript.sml b/compiler/scheme/translation/to_sexpProgScript.sml index 084513b693..91c4a864b2 100644 --- a/compiler/scheme/translation/to_sexpProgScript.sml +++ b/compiler/scheme/translation/to_sexpProgScript.sml @@ -18,6 +18,7 @@ val r = translate ASCIInumbersTheory.n2s_def; val r = translate ASCIInumbersTheory.HEX_def; val r = translate ASCIInumbersTheory.num_to_dec_string_def; val r = translate fromSexpTheory.listsexp_def; +val r = translate fromSexpTheory.SXNUM_def; val r = translate fromSexpTheory.locnsexp_def; val r = translate fromSexpTheory.locssexp_def; val r = translate stringTheory.isPrint_def; From 8780fbe21aa314d5c12748c0214d533b49f8583e Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 14:25:35 +0800 Subject: [PATCH 06/14] Fix dafny_compilerProg after simpleSexp -> mlsexp switch - Translate fromSexpTheory.SXNUM_def before locnsexp_def: SXNUM is now a smart-constructor function, not a datatype constructor, so the translator no longer handles it automatically. - Remove the obsolete litsexp_side_thm: litsexp now translates without a precondition, so litsexp_side no longer exists. - Restore HOL term/type quotation marks on the main_function sanity check and the program-assembly antiquotation, which an earlier commit had turned into ASCII string literals. dafny_compilerProgTheory now builds. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../translation/dafny_compilerProgScript.sml | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/compiler/dafny/translation/dafny_compilerProgScript.sml b/compiler/dafny/translation/dafny_compilerProgScript.sml index e3229fe389..503546e8ab 100644 --- a/compiler/dafny/translation/dafny_compilerProgScript.sml +++ b/compiler/dafny/translation/dafny_compilerProgScript.sml @@ -17,6 +17,8 @@ val _ = add_preferred_thy "-"; val r = translate fromSexpTheory.listsexp_def; +val r = translate fromSexpTheory.SXNUM_def; + val r = translate (fromSexpTheory.locnsexp_def |> SIMP_RULE list_ss []); val r = translate fromSexpTheory.locssexp_def; @@ -92,15 +94,6 @@ val r = translate fromSexpTheory.SEXSTR_def; val r = translate fromSexpTheory.litsexp_def; -Theorem litsexp_side_thm[local]: - ∀v. litsexp_side v ⇔ T -Proof - PURE_ONCE_REWRITE_TAC[fetch "-" "litsexp_side_def"] >> rw[] - >> intLib.COOPER_TAC -QED - -val _ = litsexp_side_thm |> update_precondition; - val r = translate fromSexpTheory.optsexp_def; val r = translate fromSexpTheory.idsexp_def; val r = translate fromSexpTheory.typesexp_def; @@ -126,7 +119,7 @@ val r = translate dafny_compilerTheory.main_function_def; (* Sanity checks + Finalizing *) -val _ = type_of "main_function" = ":mlsexp$sexp -> mlstring" +val _ = type_of “main_function” = “:mlsexp$sexp -> mlstring” orelse failwith "The main_function has the wrong type."; val _ = r |> hyp |> null orelse @@ -144,7 +137,7 @@ val prog = |> ml_progLib.get_thm |> REWRITE_RULE [ml_progTheory.ML_code_def] |> concl |> rator |> rator |> rand - |> (fn tm => "^tm ++ ^main") + |> (fn tm => “^tm ++ ^main”) |> EVAL |> concl |> rand; Definition dafny_compiler_prog_def: From 0207a34126cf614db193f68e54bc7962c4b3bd80 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 15:06:38 +0800 Subject: [PATCH 07/14] Update README.md --- compiler/bootstrap/translation/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/bootstrap/translation/README.md b/compiler/bootstrap/translation/README.md index 5931b4606f..1b744c7072 100644 --- a/compiler/bootstrap/translation/README.md +++ b/compiler/bootstrap/translation/README.md @@ -74,7 +74,7 @@ Translate the compiler's register allocator. Translate the RISC-V instruction encoder and RISC-V-specific config. [sexp_parserProgScript.sml](sexp_parserProgScript.sml): -Translate the alternative s-expression parser. +Translate the s-expression parser and fromSexp functions. [to_bviProgScript.sml](to_bviProgScript.sml): Translate the backend phase from BVL to BVI. From 878c20577b926cada551f000be3a8f596fbb194b Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 15:06:54 +0800 Subject: [PATCH 08/14] Fix sexp_parserProg Assisted-by: Claude:claude-opus-4-8[1m] --- .../translation/sexp_parserProgScript.sml | 44 +++---------------- 1 file changed, 5 insertions(+), 39 deletions(-) diff --git a/compiler/bootstrap/translation/sexp_parserProgScript.sml b/compiler/bootstrap/translation/sexp_parserProgScript.sml index 066bca898e..cc8c4bae7a 100644 --- a/compiler/bootstrap/translation/sexp_parserProgScript.sml +++ b/compiler/bootstrap/translation/sexp_parserProgScript.sml @@ -33,41 +33,6 @@ val r = fromSexpTheory.sexplist_def val r = translate fromSexpTheory.dstrip_sexp_def - -(* TODO: move (used?) *) -Theorem isHexDigit_cases: - isHexDigit c ⇔ - isDigit c ∨ - c ∈ {#"a";#"b";#"c";#"d";#"e";#"f"} ∨ - c ∈ {#"A";#"B";#"C";#"D";#"E";#"F"} -Proof - rw[isHexDigit_def,isDigit_def] - \\ EQ_TAC \\ strip_tac \\ simp[] - >- ( - `ORD c = 97 ∨ - ORD c = 98 ∨ - ORD c = 99 ∨ - ORD c = 100 ∨ - ORD c = 101 ∨ - ORD c = 102` by decide_tac \\ - pop_assum(assume_tac o Q.AP_TERM`CHR`) \\ fs[CHR_ORD] ) - >- ( - `ORD c = 65 ∨ - ORD c = 66 ∨ - ORD c = 67 ∨ - ORD c = 68 ∨ - ORD c = 69 ∨ - ORD c = 70` by decide_tac \\ - pop_assum(assume_tac o Q.AP_TERM`CHR`) \\ fs[CHR_ORD] ) -QED - -Theorem isHexDigit_UNHEX_LESS: - isHexDigit c ⇒ UNHEX c < 16 -Proof - rw[isHexDigit_cases] \\ EVAL_TAC \\ - fs[isDigit_def, ASCIInumbersTheory.UNHEX_def] -QED - Theorem num_from_hex_string_alt_length_2: num_from_hex_string_alt [d1;d2] < 256 Proof @@ -111,6 +76,8 @@ Proof rw[num_from_hex_string_alt_intro] QED +val r = translate stringTheory.isPrint_def; + val _ = add_preferred_thy "-"; val r = fromSexpTheory.decode_control_def @@ -167,6 +134,7 @@ val r = translate (fromSexpTheory.odestSEXSTR_def |> REWRITE_RULE [decode_control_eq]); val r = translate fromSexpTheory.odestSXSYM_def; val r = translate fromSexpTheory.odestSXNUM_def; +val r = translate fromSexpTheory.odestSXINT_def; val r = fromSexpTheory.sexpid_def |> SIMP_RULE std_ss [OPTION_BIND_THM,monad_unitbind_assert] @@ -232,6 +200,8 @@ val sexpdec_alt_side = Q.prove( val _ = translate fromSexpTheory.listsexp_def; +val _ = translate fromSexpTheory.SXNUM_def; + val _ = translate (locnsexp_def |> SIMP_RULE list_ss []); val _ = translate HEX_def @@ -303,10 +273,6 @@ val _ = translate SEXSTR_def; val _ = translate litsexp_def; -val litsexp_side_thm = Q.prove(`!v. litsexp_side v <=> T`, - PURE_ONCE_REWRITE_TAC[fetch "-" "litsexp_side_def"] >> rw[] >> - intLib.COOPER_TAC) |> update_precondition - val _ = translate optsexp_def; val _ = translate idsexp_def; val _ = translate typesexp_def; From e966b70bab28319be6af03742c76488f52b79e55 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 18:41:44 +0800 Subject: [PATCH 09/14] Fix bad merge --- compiler/compilerScript.sml | 203 +++++++++++++++++++----------------- 1 file changed, 108 insertions(+), 95 deletions(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index f45f41bb80..159e2f339b 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -53,6 +53,8 @@ OPTIONS: genN - a generational Cheney garbage collector is used; the size of the nursery generation is N machine words (example: --gc=gen5000) + This option has no effect under --pancake; the Pancake + compiler always uses gc=none. --target=T specifies that compilation should produce code for target T, where T can be one of x64, arm8, mips, riscv for @@ -107,6 +109,8 @@ Optimisations can be configured using the following advanced options. --len_size=N size of length field in heap object header cells --emit_empty_ffi=B true emits debugging FFI calls for use with DEBUG_FFI --hash_size=N size of the memoization table used by instruction encoder + --perf_callgraph=B unverified: emit C-stack shadowing so `perf record + --call-graph fp` produces correct call graphs (x64 only) ’ (* end of --help string *) @@ -123,18 +127,18 @@ val date_tm = Term `strlit^(stringSyntax.fromMLstring date_str)` Definition print_option_def: print_option h x = case x of - NONE => strlit"" - | SOME y => h ^ strlit" " ^ y ^ strlit"\n" + NONE => «» + | SOME y => h ^ « » ^ y ^ «\n» End val current_build_info_str_tm = EVAL `` - let commit = print_option (strlit"CakeML:") ^current_version_tm in - let hol = print_option (strlit"HOL4: ") ^hol_version_tm in - let poly = print_option (strlit"PolyML:") ^poly_version_tm in + let commit = print_option «CakeML:» ^current_version_tm in + let hol = print_option «HOL4: » ^hol_version_tm in + let poly = print_option «PolyML:» ^poly_version_tm in concat - [ strlit"The CakeML compiler\n\n" - ; strlit"Version details:\n" - ; ^date_tm; strlit"\n" + [ «The CakeML compiler\n\n» + ; «Version details:\n» + ; ^date_tm; «\n» ; commit; hol; poly ]`` |> concl |> rhs @@ -189,7 +193,7 @@ End Definition safe_substring_def: safe_substring s n l = let k = strlen s in - if k ≤ n then strlit "" else + if k ≤ n then «» else if n + l ≤ k then substring s n l else substring s n (k - n) @@ -214,17 +218,17 @@ Definition locs_to_string_def: let stop = (case endl of POSN r1 c1 => (if r1 = r then c1 else len) | _ => len) in let underline = - concat (REPLICATE c (strlit " ") ++ REPLICATE ((stop - c) + 1) (strlit [CHR 94])) in - concat [strlit "line "; toString (r+1); strlit "\n\n"; - line; strlit "\n"; - underline; strlit "\n"]) + concat (REPLICATE c « » ++ REPLICATE ((stop - c) + 1) (strlit [CHR 94])) in + concat [«line »; toString (r+1); «\n\n»; + line; «\n»; + underline; «\n»]) | _ => implode "unknown location") End Definition parse_sexp_input_def: parse_sexp_input input = - let err = strlit "Parsing of sexp syntax failed" in case mlsexp$fromString (implode input) of + let err = «Parsing of sexp syntax failed» in | NONE => INL err | SOME x => case sexplist sexpdec x of | NONE => INL err @@ -234,13 +238,13 @@ End Definition parse_cml_input_def: parse_cml_input input = case parse_prog (lexer_fun input) of - | Failure l _ => INL (strlit "Parsing failed at " ^ locs_to_string (implode input) (SOME l)) + | Failure l _ => INL («Parsing failed at » ^ locs_to_string (implode input) (SOME l)) | Success _ x _ => INR x End Definition compile_def: compile c prelude input = - let _ = empty_ffi (strlit "finished: start up") in + let _ = empty_ffi «finished: start up» in case if c.input_is_sexp then parse_sexp_input input @@ -248,7 +252,7 @@ Definition compile_def: of | INL msg => (Failure (ParseError msg), Nil) | INR prog => - let _ = empty_ffi (strlit "finished: lexing and parsing") in + let _ = empty_ffi «finished: lexing and parsing» in let full_prog = if c.exclude_prelude then prog else prelude ++ prog in case if c.skip_type_inference @@ -256,17 +260,17 @@ Definition compile_def: else infertype_prog c.inferencer_config full_prog of | Failure (locs, msg) => - (Failure (TypeError (concat [msg; strlit " at "; + (Failure (TypeError (concat [msg; « at »; locs_to_string (implode input) locs])), Nil) | Success ic => - let _ = empty_ffi (strlit "finished: type inference") in + let _ = empty_ffi «finished: type inference» in if c.only_print_types then - (Failure (TypeError (concat ([strlit "\n"] ++ + (Failure (TypeError (concat ([«\n»] ++ inf_env_to_types_string ic ++ - [strlit "\n"]))), Nil) + [«\n»]))), Nil) else if c.only_print_sexp then - (Failure (TypeError (concat [strlit "\n"; - sexp_to_string (listsexp (MAP decsexp full_prog))])),Nil) + (Failure (TypeError (implode + ("\n" ++ print_sexp (listsexp (MAP decsexp full_prog))))),Nil) else case backend_passes$compile_tap c.asm_config c.backend_config full_prog of | (NONE, td) => (Failure AssembleError, td) @@ -275,18 +279,18 @@ End Definition compile_pancake_def: compile_pancake asm_conf c input = - let _ = empty_ffi (strlit "finished: start up") in + let _ = empty_ffi «finished: start up» in case panPtreeConversion$parse_topdecs_to_ast input of | INR errs => ((Failure $ ParseError $ concat $ - MAP (λ(msg,loc). concat [msg; strlit " at "; - locs_to_string (implode input) (SOME loc); strlit "\n"]) + MAP (λ(msg,loc). concat [msg; « at »; + locs_to_string (implode input) (SOME loc); «\n»]) errs), Nil, []) | INL funs => case static_check funs of | (error e, warns) => (Failure $ StaticError e, Nil, MAP StaticError warns) | (return (), warns) => - let _ = empty_ffi (strlit "finished: lexing and parsing") in + let _ = empty_ffi «finished: lexing and parsing» in case pan_passes$pan_compile_tap asm_conf c funs of | (NONE,td) => (Failure AssembleError, td, MAP StaticError warns) | (SOME (bytes,data,c),td) => (Success (bytes,data,c), td, MAP StaticError warns) @@ -295,25 +299,25 @@ End (* The top-level compiler *) Definition error_to_str_def: (error_to_str (ParseError s) = - concat [strlit "### ERROR: parse error\n"; s; strlit "\n"]) /\ + concat [«### ERROR: parse error\n»; s; «\n»]) /\ (error_to_str (TypeError s) = (* if the first char in the message is a newline char then it isn't an error *) if (if strlen s = 0 then T else if strsub s 0 = #"\n" then F else T) then - concat [strlit "### ERROR: type error\n"; s; strlit "\n"] + concat [«### ERROR: type error\n»; s; «\n»] else s) /\ - (error_to_str (ConfigError s) = concat [strlit "### ERROR: config error\n"; s; strlit "\n"]) /\ - (error_to_str AssembleError = strlit "### ERROR: assembly error\n") /\ + (error_to_str (ConfigError s) = concat [«### ERROR: config error\n»; s; «\n»]) /\ + (error_to_str AssembleError = «### ERROR: assembly error\n») /\ (error_to_str (StaticError e) = case e of - ScopeErr s => concat [strlit "### ERROR: scope error\n"; s; strlit "\n"] - | WarningErr s => concat [strlit "# WARNING:\n"; s; strlit "\n"] - | GenErr s => concat [strlit "### ERROR: static error\n"; s; strlit "\n"] - | ShapeErr s => concat [strlit "### ERROR: shape error\n"; s; strlit "\n"]) + ScopeErr s => concat [«### ERROR: scope error\n»; s; «\n»] + | WarningErr s => concat [«# WARNING:\n»; s; «\n»] + | GenErr s => concat [«### ERROR: static error\n»; s; «\n»] + | ShapeErr s => concat [«### ERROR: shape error\n»; s; «\n»]) End Definition is_error_msg_def: - is_error_msg x = mlstring$isPrefix (strlit "###") x + is_error_msg x = mlstring$isPrefix «###» x End (* TODO: translator fails inside mlstringLib.mlstring_case_conv @@ -329,8 +333,8 @@ End Definition parse_bool_def: parse_bool str = - if str = strlit "true" then SOME T - else if str = strlit "false" then SOME F + if str = «true» then SOME T + else if str = «false» then SOME F else NONE End @@ -365,7 +369,7 @@ Definition find_bool_def: | SOME rest => case parse_bool rest of SOME b => INL b - | NONE => INR (concat [strlit"Unable to parse as bool: ";rest;strlit " for flag: ";flag]) + | NONE => INR (concat [«Unable to parse as bool: »;rest;« for flag: »;flag]) End (* If flag is not present then INL default, else if it is present then @@ -377,12 +381,12 @@ Definition find_num_def: | SOME rest => case parse_num rest of SOME n => INL n - | NONE => INR (concat [strlit"Unable to parse as num: ";rest;strlit " for flag: ";flag]) + | NONE => INR (concat [«Unable to parse as num: »;rest;« for flag: »;flag]) End Definition get_err_str_def: - (get_err_str (INL n) = strlit"") ∧ - (get_err_str (INR n) = concat[n;strlit"\n"]) + (get_err_str (INL n) = «») ∧ + (get_err_str (INR n) = concat[n;«\n»]) End (* All the numbers must parse *) @@ -390,7 +394,7 @@ Definition parse_num_list_def: (parse_num_list [] = INL []) /\ (parse_num_list (x::xs) = case parse_num x of - NONE => INR (concat [strlit"Unable to parse as num: ";x]) + NONE => INR (concat [«Unable to parse as num: »;x]) | SOME n => case parse_num_list xs of INR s => INR s @@ -412,9 +416,9 @@ Definition parse_nums_def: End (* - EVAL``find_bool (strlit "--mul=") [strlit "asf";strlit"--mul=fse"] F`` - EVAL``find_bool (strlit "--nomul") [strlit "asf";strlit"--nomul=fdsa"] T`` - EVAL``find_num (strlit "--fl") [strlit "asf";strlit"--f1234"] 5n`` + EVAL``find_bool «--mul=» [«asf»;«--mul=fse»] F`` + EVAL``find_bool «--nomul» [«asf»;«--nomul=fdsa»] T`` + EVAL``find_num «--fl» [«asf»;«--f1234»] 5n`` *) (* @@ -426,15 +430,15 @@ End (* clos_conf *) Definition parse_clos_conf_def: parse_clos_conf ls clos = - let multi = find_bool (strlit"--multi=") ls clos.do_mti in - let known = find_bool (strlit"--known=") ls (IS_SOME clos.known_conf) in - let inline_factor = find_num (strlit"--inline_factor=") ls default_inline_factor in - let call = find_bool (strlit"--call=") ls clos.do_call in - let maxapp = find_num (strlit "--max_app=") ls clos.max_app in + let multi = find_bool «--multi=» ls clos.do_mti in + let known = find_bool «--known=» ls (IS_SOME clos.known_conf) in + let inline_factor = find_num «--inline_factor=» ls default_inline_factor in + let call = find_bool «--call=» ls clos.do_call in + let maxapp = find_num «--max_app=» ls clos.max_app in case (multi,known,inline_factor,call,maxapp) of (INL m,INL k,INL i,INL c,INL n) => if k then - (let max_body_size = find_num (strlit"--max_body_size=") ls (default_max_body_size n i) in + (let max_body_size = find_num «--max_body_size=» ls (default_max_body_size n i) in case max_body_size of (INL x) => INL @@ -464,9 +468,9 @@ End (* bvl *) Definition parse_bvl_conf_def: parse_bvl_conf ls bvl = - let inlinesz = find_num (strlit "--inline_size=") ls bvl.inline_size_limit in - let expcut = find_num (strlit "--exp_cut=") ls bvl.exp_cut in - let splitmain = find_bool (strlit"--split=") ls bvl.split_main_at_seq in + let inlinesz = find_num «--inline_size=» ls bvl.inline_size_limit in + let expcut = find_num «--exp_cut=» ls bvl.exp_cut in + let splitmain = find_bool «--split=» ls bvl.split_main_at_seq in case (inlinesz,expcut,splitmain) of (INL i,INL e,INL m) => INL @@ -484,7 +488,7 @@ End (* wtw *) Definition parse_wtw_conf_def: parse_wtw_conf ls wtw = - let regalg = find_num (strlit "--reg_alg=") ls wtw.reg_alg in + let regalg = find_num «--reg_alg=» ls wtw.reg_alg in case regalg of INL r => INL (wtw with <|reg_alg:= r |>) | INR s => INR (get_err_str regalg) @@ -492,21 +496,21 @@ End Definition parse_gc_def: parse_gc ls default = - case find_str (strlit"--gc=") ls of + case find_str «--gc=» ls of NONE => INL default | SOME rest => - if rest = strlit"none" then INL None - else if rest = strlit"simple" then INL Simple - else if isPrefix (strlit "gen") rest then - case parse_nums (extract rest (strlen (strlit"gen")) NONE) of + if rest = «none» then INL None + else if rest = «simple» then INL Simple + else if isPrefix «gen» rest then + case parse_nums (extract rest (strlen «gen») NONE) of INL ls => INL (Generational ls) | INR s => - INR (concat [strlit"Error parsing GenGC argument: ";s]) - else INR (concat [strlit"Unrecognized GC option: ";rest]) + INR (concat [«Error parsing GenGC argument: »;s]) + else INR (concat [«Unrecognized GC option: »;rest]) End (* -EVAL ``parse_gc [strlit "--gc=gen1234,1234,1234"] def`` +EVAL ``parse_gc [«--gc=gen1234,1234,1234»] def`` *) (* Copy of conf_ok from data_to_word *) @@ -520,11 +524,11 @@ End (* data *) Definition parse_data_conf_def: parse_data_conf ls data = - let tag_bits = find_num (strlit "--tag_bits=") ls data.tag_bits in - let len_bits = find_num (strlit "--len_bits=") ls data.len_bits in - let pad_bits = find_num (strlit "--pad_bits=") ls data.pad_bits in - let len_size = find_num (strlit "--len_size=") ls data.len_size in - let empty_FFI= find_bool (strlit"--emit_empty_ffi=") ls data.call_empty_ffi in + let tag_bits = find_num «--tag_bits=» ls data.tag_bits in + let len_bits = find_num «--len_bits=» ls data.len_bits in + let pad_bits = find_num «--pad_bits=» ls data.pad_bits in + let len_size = find_num «--len_size=» ls data.len_size in + let empty_FFI= find_bool «--emit_empty_ffi=» ls data.call_empty_ffi in let gc = parse_gc ls data.gc_kind in case (tag_bits,len_bits,pad_bits,len_size,gc,empty_FFI) of (INL tb,INL lb,INL pb,INL ls,INL gc, INL empty_FFI) => @@ -548,22 +552,24 @@ End (* stack *) Definition parse_stack_conf_def: parse_stack_conf ls stack = - let jump = find_bool (strlit"--jump=") ls stack.jump in - case jump of - INL j => INL (stack with jump:=j) - | INR s => INR s + let jump = find_bool «--jump=» ls stack.jump in + let perf = find_bool «--perf_callgraph=» ls stack.perf_calls in + case (jump, perf) of + (INL j, INL p) => INL (stack with <| jump := j; perf_calls := p |>) + | (INR s, _) => INR s + | (_, INR s) => INR s End (* tap *) Definition parse_tap_conf_def: parse_tap_conf ls stack = - INL (<| explore_flag := MEMBER (strlit"--explore") ls |>) + INL (<| explore_flag := MEMBER «--explore» ls |>) End (* lab *) Definition parse_lab_conf_def: parse_lab_conf ls lab = - let hs = find_num (strlit "--hash_size=") ls lab.hash_size in + let hs = find_num «--hash_size=» ls lab.hash_size in case hs of INL r => INL (lab with <|hash_size := r |>) | INR s => INR s @@ -601,36 +607,36 @@ End (* Defaults to x64 if no target given *) Definition parse_target_64_def: parse_target_64 ls = - case find_str (strlit"--target=") ls of + case find_str «--target=» ls of NONE => INL (x64_backend_config,x64_export,x64_config) | SOME rest => - if rest = strlit"x64" then INL (x64_backend_config,x64_export,x64_config) - else if rest = strlit"arm8" then INL (arm8_backend_config,arm8_export,arm8_config) - else if rest = strlit"mips" then INL (mips_backend_config,mips_export,mips_config) - else if rest = strlit"riscv" then INL (riscv_backend_config,riscv_export,riscv_config) - else INR (concat [strlit"Unrecognized 64-bit target option: ";rest]) + if rest = «x64» then INL (x64_backend_config,x64_export,x64_config) + else if rest = «arm8» then INL (arm8_backend_config,arm8_export,arm8_config) + else if rest = «mips» then INL (mips_backend_config,mips_export,mips_config) + else if rest = «riscv» then INL (riscv_backend_config,riscv_export,riscv_config) + else INR (concat [«Unrecognized 64-bit target option: »;rest]) End (* Defaults to arm7 if no target given *) Definition parse_target_32_def: parse_target_32 ls = - case find_str (strlit"--target=") ls of + case find_str «--target=» ls of NONE => INL (arm7_backend_config,arm7_export,arm7_config) | SOME rest => - if rest = strlit"arm7" then INL (arm7_backend_config,arm7_export,arm7_config) - else if rest = strlit"ag32" then INL (ag32_backend_config,ag32_export,ag32_config) - else INR (concat [strlit"Unrecognized 32-bit target option: ";rest]) + if rest = «arm7» then INL (arm7_backend_config,arm7_export,arm7_config) + else if rest = «ag32» then INL (ag32_backend_config,ag32_export,ag32_config) + else INR (concat [«Unrecognized 32-bit target option: »;rest]) End Definition parse_top_config_def: parse_top_config ls = - let sexp = find_bool (strlit"--sexp=") ls F in - let prelude = find_bool (strlit"--exclude_prelude=") ls F in - let typeinference = find_bool (strlit"--skip_type_inference=") ls F in - let sexpprint = MEMBER (strlit"--print_sexp") ls in - let onlyprinttypes = MEMBER (strlit"--types") ls in - let nowarnings = MEMBER (strlit"--no_warn") ls in - let mainreturn = find_bool (strlit"--main_return=") ls F in + let sexp = find_bool «--sexp=» ls F in + let prelude = find_bool «--exclude_prelude=» ls F in + let typeinference = find_bool «--skip_type_inference=» ls F in + let sexpprint = MEMBER «--print_sexp» ls in + let onlyprinttypes = MEMBER «--types» ls in + let nowarnings = MEMBER «--no_warn» ls in + let mainreturn = find_bool «--main_return=» ls F in case (sexp,prelude,typeinference,mainreturn) of (INL sexp,INL prelude,INL typeinference,INL mainreturn) => INL (sexp,prelude,typeinference,onlyprinttypes,sexpprint,mainreturn,nowarnings) @@ -643,17 +649,17 @@ End (* Check for version flag *) Definition has_version_flag_def: - has_version_flag ls = MEM (strlit"--version") ls + has_version_flag ls = MEM «--version» ls End (* Check for version help *) Definition has_help_flag_def: - has_help_flag ls = MEM (strlit"--help") ls + has_help_flag ls = MEM «--help» ls End (* Check for pancake flag *) Definition has_pancake_flag_def: - has_pancake_flag ls = MEM (strlit"--pancake") ls + has_pancake_flag ls = MEM «--pancake» ls End Definition format_compiler_result_def: @@ -707,6 +713,11 @@ Definition compile_64_def: (List[], error_to_str (ConfigError (concat [get_err_str confexp;get_err_str topconf]))) End +Definition pancake_backend_conf_def: + pancake_backend_conf c = + c with data_conf := (c.data_conf with gc_kind := None) +End + Definition compile_pancake_64_def: compile_pancake_64 cl input = let confexp = parse_target_64 cl in @@ -722,6 +733,7 @@ Definition compile_pancake_64_def: | INR err => (List[], error_to_str (ConfigError (get_err_str ext_conf))) | INL ext_conf => + let ext_conf = pancake_backend_conf ext_conf in case compiler$compile_pancake aconf ext_conf input of | (Failure err, td, warns) => (List[], concat (MAP error_to_str (err::(if nowarn then [] else warns)))) @@ -797,6 +809,7 @@ Definition compile_pancake_32_def: | INR err => (List[], error_to_str (ConfigError (get_err_str ext_conf))) | INL ext_conf => + let ext_conf = pancake_backend_conf ext_conf in case compiler$compile_pancake aconf ext_conf input of | (Failure err, td, warns) => (List[], concat (MAP error_to_str (err::(if nowarn then [] else warns)))) From e301442365e2a4d4ee85b218b55177b7c4020544 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 21:45:01 +0800 Subject: [PATCH 10/14] Actually fix bad merge --- compiler/compilerScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index 159e2f339b..e772124416 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -227,8 +227,8 @@ End Definition parse_sexp_input_def: parse_sexp_input input = - case mlsexp$fromString (implode input) of let err = «Parsing of sexp syntax failed» in + case mlsexp$fromString (implode input) of | NONE => INL err | SOME x => case sexplist sexpdec x of | NONE => INL err From eae30ec4b0ef49ff8423adef4bb4fde88a0c0f1e Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sat, 6 Jun 2026 23:48:18 +0800 Subject: [PATCH 11/14] Replace removed print_sexp with mlsexp$sexp_to_string The switch from simpleSexpParse to mlsexp dropped simpleSexpParse from the Ancestors, removing print_sexp. The --print_sexp path in compile_def still referenced it. Use mlsexp$sexp_to_string (flat output) instead; it returns an mlstring directly, so the old implode/"++" wrapping is no longer needed. Co-Authored-By: Claude Opus 4.8 (1M context) --- compiler/compilerScript.sml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index e772124416..e9e310b3b7 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -269,8 +269,8 @@ Definition compile_def: inf_env_to_types_string ic ++ [«\n»]))), Nil) else if c.only_print_sexp then - (Failure (TypeError (implode - ("\n" ++ print_sexp (listsexp (MAP decsexp full_prog))))),Nil) + (Failure (TypeError («\n» ^ + mlsexp$sexp_to_string (listsexp (MAP decsexp full_prog)))),Nil) else case backend_passes$compile_tap c.asm_config c.backend_config full_prog of | (NONE, td) => (Failure AssembleError, td) From 8d012555bf553bb085caae952f296488cde16a21 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sun, 7 Jun 2026 12:45:41 +0800 Subject: [PATCH 12/14] Update changes-since-release.md --- developers/changes-since-release.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/developers/changes-since-release.md b/developers/changes-since-release.md index bf20af8e3f..148b2788f2 100644 --- a/developers/changes-since-release.md +++ b/developers/changes-since-release.md @@ -2,6 +2,11 @@ Changes since release v3304: ## Source language and front‑end +## Parser + +The S-expression parser has been changed to use the simpler and more efficient mlsexp parser +instead of the PEG-based parser from HOL (simpleSexp) (#1365). + ## Basis library `TextIO.inputAllFrom` has been added to the basis library. The CF theorem for `TextIO.inputAll` has been corrected (#1375, #1366). From 52f2db05d7f714d18143a76b93d11251501b59a8 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Sun, 7 Jun 2026 14:02:41 +0800 Subject: [PATCH 13/14] Rewrite astToSexprLib for the mlsexp representation astToSexprLib is a hand-written SML mirror of the fromSexpScript.sml encoders that serialises a CakeML AST term to s-expression text. It still produced the old simpleSexp format, which no longer matches the migrated mlsexp-based encoders/decoders, so its output would not re-parse. Rewrite it to emit exactly what mlsexp$sexp_to_string would print for the encoder results (decsexp/expsexp/...), keeping the public API (write_ast, write_ast_to_file) unchanged so all consumers are unaffected. Notable format changes (mlsexp sexp = Atom | Expr): - no dotted pairs/tuples; pairs become 2-element lists, empty list "()" - atoms quoted only when unsafe (faithful encode_control + make_str_safe + escape_str ports), using an ordinal isPrint (32..126) test - IntLit now tagged with a "~" sign; Char via SEXSTR; StrLit bare; words/Float64 via decimal SXNUM - locations as nested s-expressions, incl. EOFpt - ThunkOp operators handled; explicit op->tag table that keeps Vsub_unsafe's underscore while stripping the other unsafe ops Verified in HOL: byte-exact match against sexp_to_string (decsexp d) for every literal/op/pattern/type/declaration form (incl. tricky strings), and a full write_ast -> fromString -> sexplist sexpdec round-trip recovering the original program. Co-Authored-By: Claude Opus 4.8 (1M context) --- unverified/sexpr-bootstrap/astToSexprLib.sml | 422 ++++++++++--------- 1 file changed, 229 insertions(+), 193 deletions(-) diff --git a/unverified/sexpr-bootstrap/astToSexprLib.sml b/unverified/sexpr-bootstrap/astToSexprLib.sml index bc0f06fb5a..7368053938 100644 --- a/unverified/sexpr-bootstrap/astToSexprLib.sml +++ b/unverified/sexpr-bootstrap/astToSexprLib.sml @@ -1,225 +1,261 @@ structure astToSexprLib = struct -open preamble mlstringSyntax fromSexpTheory +open preamble mlstringSyntax -datatype exp = exp_tuple of exp list | exp_list of exp list | exp_str of string; +(* This library is a fast SML reimplementation of the HOL encoders in + compiler/parsing/fromSexpScript.sml (decsexp/expsexp/patsexp/...). It walks + a HOL term representing a CakeML AST and writes the corresponding + s-expression text, exactly as mlsexp$sexp_to_string would print the encoder + result. Working directly on terms avoids EVALuating the (slow) HOL + definitions on large bootstrap programs. -fun escape_wrap c = "\"" ^ c ^ "\"" -fun escape_char c = + The textual format must match the mlsexp representation + (basis/pure/mlsexpScript.sml): sexp = Atom mlstring | Expr (sexp list). + There are no cons-pairs, no dotted notation and no nil; lists are Expr [...] + and the empty list prints as "()". The tag strings below mirror the + encoder definitions and must be kept in sync with them. *) + +datatype sexp = Atom of string | Expr of sexp list; + +(*--------------------------------------------------------------* + Printing: faithful port of mlsexp$sexp_to_string + *--------------------------------------------------------------*) + +(* HOL isPrint c <=> 32 <= ORD c < 127. Do NOT use Char.isPrint, whose + behaviour for ORD c >= 127 is implementation-defined. *) +fun isPrintH c = let val n = Char.ord c in 32 <= n andalso n < 127 end +(* HOL isSpace c <=> ORD c = 32 \/ 9 <= ORD c <= 13 *) +fun isSpaceH c = let val n = Char.ord c in n = 32 orelse (9 <= n andalso n <= 13) end + +(* mlsexp$is_safe_char *) +fun is_safe_char c = not (Char.contains "()\"\000" c) andalso not (isSpaceH c) + +(* mlstring$char_escaped *) +fun char_escaped c = + case c of + #"\t" => "\\t" + | #"\n" => "\\n" + | #"\\" => "\\\\" + | #"\"" => "\\\"" + | _ => String.str c + +(* mlstring$escape_str *) +fun escape_str s = "\"" ^ String.concat (map char_escaped (String.explode s)) ^ "\"" + +(* mlsexp$make_str_safe *) +fun make_str_safe s = + if s = "" then "\"\"" + else if List.all is_safe_char (String.explode s) then s + else escape_str s + +(* mlsexp$sexp_to_string: atoms via make_str_safe, lists space-separated in + parentheses ("()" when empty). *) +fun sexp_to_string (Atom s) = make_str_safe s + | sexp_to_string (Expr l) = + "(" ^ String.concatWith " " (map sexp_to_string l) ^ ")" + +(*--------------------------------------------------------------* + Atom builders mirroring SEXSTR / SXNUM and integer formatting + *--------------------------------------------------------------*) + +(* fromSexp$encode_control: double backslashes; keep printable chars; escape + non-printable chars as a single backslash followed by two uppercase hex + digits (with a leading "0" when ORD c < 16). *) +fun encode_control_char c = + if c = #"\\" then "\\\\" + else if isPrintH c then String.str c + else "\\" ^ (if Char.ord c < 16 then "0" else "") ^ Int.fmt StringCvt.HEX (Char.ord c) +fun encode_control s = String.concat (map encode_control_char (String.explode s)) + +(* SEXSTR (string) and SEXSTR (mlstring term) *) +fun sexstr_str s = Atom (encode_control s) +fun sexstr t = sexstr_str (mlstringSyntax.dest_mlstring t) + +(* SXNUM applied to a num term and to a word literal *) +fun sxnum_num n = Atom (Arbnum.toString (numSyntax.dest_numeral n)) +fun sxnum_word w = Atom (Arbnum.toString (wordsSyntax.dest_word_literal w)) + +(* mlint$toString of an integer literal: "~" sign for negatives, decimal + magnitude. *) +fun int_to_string t = let - val to_hex = (StringCvt.padLeft #"0" 2) o (Int.fmt StringCvt.HEX) o Char.ord + val i = intSyntax.int_of_term t + val mag = Arbnum.toString (Arbint.toNat (Arbint.abs i)) in - if c = #"\\" then "\\\\\\\\" - else if c = #"\"" then "\\\"" - else if Char.isPrint c then Char.toString c - else "\\\\" ^ (to_hex c) + if Arbint.<(i, Arbint.zero) then "~" ^ mag else mag end -val fromHOLchar = - escape_wrap o escape_char o stringSyntax.fromHOLchar; -val fromHOLstring = - escape_wrap o (String.translate escape_char) o mlstringSyntax.dest_mlstring; -val fromHOLnum = Arbnumcore.toString o numSyntax.dest_numeral; +(*--------------------------------------------------------------* + Leaf encoders (explicit tables mirroring the HOL definitions) + *--------------------------------------------------------------*) -fun char_to_exp c = exp_list [exp_str "char", exp_str (fromHOLchar c)] -val string_to_exp = exp_str o fromHOLstring; -val num_to_exp = exp_str o fromHOLnum; +val const_name = #1 o dest_const -fun word_to_exp lit_name w = - let - val str = Arbnumcore.toString (wordsSyntax.dest_word_literal w) - in - exp_list [exp_str lit_name, exp_str str] +(* fromSexp$opsexp: most nullary ops use their constructor name verbatim (note + Vsub_unsafe keeps its underscore), but these few are renamed. *) +fun op_tag nm = + case nm of + "Aw8sub_unsafe" => "Aw8subunsafe" + | "Aw8update_unsafe" => "Aw8updateunsafe" + | "XorAw8Str_unsafe" => "XorAw8Strunsafe" + | "Asub_unsafe" => "Asubunsafe" + | "Aupdate_unsafe" => "Aupdateunsafe" + | "Env_id" => "Envid" + | _ => nm + +fun width_digits w = + case const_name w of + "W8" => "8" + | "W64" => "64" + | s => failwith ("astToSexprLib: unknown word_size " ^ s) + +(* fromSexp$prim_typesexp *) +fun prim_typesexp pt = + let val (h, args) = strip_comb pt in + case const_name h of + "WordT" => Atom ("Word" ^ width_digits (hd args) ^ "T") + | s => Atom s (* BoolT, IntT, CharT, StrT, Float64T *) end -fun int_to_exp i = - let - fun via_num i = (num_to_exp o rhs o concl o EVAL) ``Num (^i)`` - in - if intSyntax.is_negated i - then exp_list [exp_str "-", via_num (intSyntax.mk_negated i)] - else via_num i +(* fromSexp$arithsexp: constructor names match the tags verbatim *) +fun arithsexp a = Atom (const_name a) + +(* fromSexp$testsexp *) +fun cmp_word nm = + case nm of + "Lt" => "Less" + | "Leq" => "LessEq" + | "Gt" => "Greater" + | "Geq" => "GreaterEq" + | s => failwith ("astToSexprLib: unknown opb " ^ s) +fun testsexp t = + let val (h, args) = strip_comb t in + case const_name h of + "Equal" => Atom "Equal" + | "Compare" => Atom (cmp_word (const_name (hd args))) + | "AltCompare" => Atom ("Alt" ^ cmp_word (const_name (hd args))) + | s => failwith ("astToSexprLib: unknown test " ^ s) end -fun loc_to_exp xs = - let - fun loc_to_str tm = - if aconv tm “UNKNOWNpt” then "unk" else - if aconv (repeat rator tm) “POSN” then - "(" ^ (numSyntax.dest_numeral (rand (rator tm)) |> Arbnum.toString) ^ - " " ^ (numSyntax.dest_numeral (rand tm) |> Arbnum.toString) ^ ")" - else "0 0 0" - fun join [] = "" - | join [x] = x - | join (x::xs) = x ^ " " ^ join xs - in - exp_list [exp_str (join (map loc_to_str xs))] +(* fromSexp$opsexp for the ThunkOp cases; modes use encode_thunk_mode, whose + output equals the constructor name. *) +fun thunkop t = + let val (h, args) = strip_comb t in + case const_name h of + "ForceThunk" => Atom "ForceThunk" + | "AllocThunk" => Expr [Atom "AllocThunk", Atom (const_name (hd args))] + | "UpdateThunk" => Expr [Atom "UpdateThunk", Atom (const_name (hd args))] + | s => failwith ("astToSexprLib: unknown thunk_op " ^ s) end -val int_lit = astSyntax.IntLit_tm; -val char_lit = astSyntax.Char_tm; -val word8_lit = astSyntax.Word8_tm; -val word64_lit = astSyntax.Word64_tm; -val float64_lit = prim_mk_const{Thy = "ast", Name = "Float64"}; -fun lit_to_exp t = - let - val (x, xs) = strip_comb t - val h = hd xs - in - if same_const x int_lit then int_to_exp h - else if same_const x char_lit then char_to_exp h - else if same_const x word8_lit then word_to_exp "word8" h - else if same_const x word64_lit then word_to_exp "word64" h - else if same_const x float64_lit then word_to_exp "float64" h - else string_to_exp h +(* fromSexp$opsexp. Operators only ever appear as the first argument of App, + so they are routed here rather than through the generic dispatcher. *) +fun opsexp t = + let val (h, args) = strip_comb t in + case const_name h of + "Shift" => Expr [Atom ("Shift" ^ width_digits (List.nth (args, 0)) + ^ const_name (List.nth (args, 1))), + sxnum_num (List.nth (args, 2))] + | "FFI" => Expr [Atom "FFI", sexstr (hd args)] + | "Arith" => Expr [Atom "Arith", arithsexp (List.nth (args, 0)), + prim_typesexp (List.nth (args, 1))] + | "FromTo" => Expr [Atom "FromTo", prim_typesexp (List.nth (args, 0)), + prim_typesexp (List.nth (args, 1))] + | "Test" => Expr [Atom "Test", testsexp (List.nth (args, 0)), + prim_typesexp (List.nth (args, 1))] + | "ThunkOp" => thunkop (hd args) + | nm => Atom (op_tag nm) end -val shift_op = astSyntax.Shift_tm; -val test_op = prim_mk_const{Thy="ast",Name="Test"}; -val arith_op = prim_mk_const{Thy="ast",Name="Arith"}; -val from_to_op = prim_mk_const{Thy="ast",Name="FromTo"}; -val ffi_op = astSyntax.FFI_tm; -val Compare_tm = prim_mk_const{Thy="ast",Name="Compare"}; -val AltCompare_tm = prim_mk_const{Thy="ast",Name="AltCompare"}; -val WordT_tm = prim_mk_const{Thy="ast",Name="WordT"}; -val wordT_W8 = mk_comb(WordT_tm, astSyntax.W8); -val wordT_W64 = mk_comb(WordT_tm, astSyntax.W64); -val test_eq = prim_mk_const{Thy="ast",Name="Equal"}; -val test_lt = mk_comb(Compare_tm, astSyntax.Lt) -val test_leq = mk_comb(Compare_tm, astSyntax.Leq) -val test_gt = mk_comb(Compare_tm, astSyntax.Gt) -val test_geq = mk_comb(Compare_tm, astSyntax.Geq) -val test_alt_lt = mk_comb(AltCompare_tm, astSyntax.Lt) -val test_alt_leq = mk_comb(AltCompare_tm, astSyntax.Leq) -val test_alt_gt = mk_comb(AltCompare_tm, astSyntax.Gt) -val test_alt_geq = mk_comb(AltCompare_tm, astSyntax.Geq) -fun op_to_exp arg = - let - val underscore_filter = - String.implode o filter (fn n => n <> #"_") o String.explode - val to_string = #1 o dest_const - fun filtered_string t = - case to_string t of "W8" => "8" - | "W64" => "64" - | s => underscore_filter s - fun wordInt xs s = exp_str ((hd (map to_string xs)) ^ s) - fun ffi xs = exp_tuple [exp_str "FFI", string_to_exp (hd xs)] - fun test_ty x = - if aconv x wordT_W8 then exp_str "Word8T" else - if aconv x wordT_W64 then exp_str "Word64T" else - exp_str (to_string x) - fun test_name x = - if aconv x test_eq then exp_str "Equal" else - if aconv x test_lt then exp_str "Less" else - if aconv x test_leq then exp_str "LessEq" else - if aconv x test_gt then exp_str "Greater" else - if aconv x test_geq then exp_str "GreaterEq" else - if aconv x test_alt_lt then exp_str "AltLess" else - if aconv x test_alt_leq then exp_str "AltLessEq" else - if aconv x test_alt_gt then exp_str "AltGreater" else - if aconv x test_alt_geq then exp_str "AltGreaterEq" else - failwith ("test_name failed for: " ^ term_to_string x) - fun test xs = exp_tuple [exp_str "Test", - test_name (hd xs), - test_ty (hd (tl xs))] - fun from_to xs = exp_tuple [exp_str "FromTo", - test_ty (hd xs), - test_ty (hd (tl xs))] - fun arith xs = exp_tuple [exp_str "Arith", - exp_str (hd xs |> dest_const |> fst), - test_ty (hd (tl xs))] - fun shift xs = - let - val consts = List.take (xs, 2) - val str = "Shift" ^ String.concat (map filtered_string consts) - in - exp_tuple [exp_str str, num_to_exp (last xs)] - end - val (x, xs) = strip_comb arg - in - if same_const x shift_op then shift xs - else if same_const x ffi_op then ffi xs - else if same_const x test_op then test xs - else if same_const x arith_op then arith xs - else if same_const x from_to_op then from_to xs - else exp_str (String.concat (map filtered_string (x::xs))) +(* fromSexp$litsexp *) +fun lit_to_sexp t = + let val (h, args) = strip_comb t val a = hd args in + case const_name h of + "IntLit" => Expr [Atom "IntLit", Atom (int_to_string a)] + | "Char" => Expr [Atom "char", sexstr_str (String.str (stringSyntax.fromHOLchar a))] + | "StrLit" => sexstr a + | "Word8" => Expr [Atom "word8", sxnum_word a] + | "Word64" => Expr [Atom "word64", sxnum_word a] + | "Float64" => Expr [Atom "float64", sxnum_word a] + | s => failwith ("astToSexprLib: unknown lit " ^ s) end -val cons = listSyntax.cons_tm; -val comma = pairSyntax.comma_tm; -val pvar = astSyntax.Pvar_tm; -val pany = astSyntax.Pany; -val locs = prim_mk_const{Thy="location",Name="Locs"}; -val nil_l = listSyntax.nil_tm; -val app = astSyntax.App_tm; -val lit = astSyntax.Lit_tm; -val plit = astSyntax.Plit_tm; -fun ast_to_exp term = - let - val list_to_exp = map ast_to_exp - fun app_to_exp const args = - let - val exp = (exp_str o #1 o dest_const) const - val op_exp = op_to_exp (hd args) - val args_exp = list_to_exp (tl args) - in - exp_list (exp::op_exp::args_exp) - end - fun generic_to_exp const args = - let - val exp = (exp_str o #1 o dest_const) const - val args_exp = list_to_exp args - in - case args of [] => exp - | _ => exp_list (exp::args_exp) - end - fun cons_to_exp term = - (exp_list o list_to_exp o #1 o listSyntax.dest_list) term - val tuple_to_exp = - exp_tuple o list_to_exp o pairSyntax.spine_pair - val (x, xs) = strip_comb term - in - if same_const x pvar then ast_to_exp (hd xs) - else if same_const x pany then exp_list [exp_str "Pany"] - else if same_const x lit then - exp_list [exp_str "Lit", lit_to_exp (hd xs)] - else if same_const x plit then - exp_list [exp_str "Plit", lit_to_exp (hd xs)] - else if same_const x locs then loc_to_exp xs - else if same_const x nil_l then exp_list [] - else if same_const x cons then cons_to_exp term - else if same_const x comma then tuple_to_exp term - else if same_const x app then app_to_exp x xs - else if mlstringSyntax.is_mlstring_literal term then string_to_exp term - else generic_to_exp x xs +(* fromSexp$locnsexp *) +fun locnsexp p = + let val (h, args) = strip_comb p in + case const_name h of + "UNKNOWNpt" => Atom "unk" + | "EOFpt" => Atom "eof" + | "POSN" => Expr [sxnum_num (List.nth (args, 0)), sxnum_num (List.nth (args, 1))] + | s => failwith ("astToSexprLib: unknown locn " ^ s) end +(* fromSexp$locssexp; args are the two arguments of Locs *) +fun locssexp args = Expr [locnsexp (List.nth (args, 0)), locnsexp (List.nth (args, 1))] -fun exp_to_string e = +(*--------------------------------------------------------------* + Generic recursive dispatcher + *--------------------------------------------------------------*) + +val pvar_tm = astSyntax.Pvar_tm +val pany_tm = astSyntax.Pany +val lit_tm = astSyntax.Lit_tm +val plit_tm = astSyntax.Plit_tm +val app_tm = astSyntax.App_tm +val cons_tm = listSyntax.cons_tm +val nil_tm = listSyntax.nil_tm +val comma_tm = pairSyntax.comma_tm +val locs_tm = prim_mk_const{Thy="location",Name="Locs"} + +fun ast_to_sexp term = let - val list_to_string = - (String.concatWith " ") o (map exp_to_string) - fun tuple_to_string t = - case t of [] => "" - | [x, exp_list l] => (exp_to_string x) ^ " " ^ (list_to_string l) - | [x, y] => (exp_to_string x) ^ " . " ^ (exp_to_string y) - | x::xs => (exp_to_string x) ^ " " ^ (tuple_to_string xs) + val (x, xs) = strip_comb term in - case e of exp_str s => s - | exp_tuple l => "(" ^ (tuple_to_string l) ^ ")" - | exp_list [] => "nil" - | exp_list l => "(" ^ (list_to_string l) ^ ")" + (* a list: nil -> Expr []; cons -> Expr of the converted elements *) + if same_const x nil_tm then Expr [] + else if same_const x cons_tm then + Expr (map ast_to_sexp (#1 (listSyntax.dest_list term))) + (* a pair (a, b) -> 2-element Expr; the right-nested tuple structure makes + triples like (f, x, e) nest as Expr [.; Expr [.; .]] to match the + encoder lambdas. *) + else if same_const x comma_tm then + Expr [ast_to_sexp (List.nth (xs, 0)), ast_to_sexp (List.nth (xs, 1))] + (* Pvar s is a bare SEXSTR (no tag); Pany is a one-element Expr *) + else if same_const x pvar_tm then sexstr (hd xs) + else if same_const x pany_tm then Expr [Atom "Pany"] + (* literals are encoded by litsexp *) + else if same_const x lit_tm then Expr [Atom "Lit", lit_to_sexp (hd xs)] + else if same_const x plit_tm then Expr [Atom "Plit", lit_to_sexp (hd xs)] + (* App routes its operator through opsexp *) + else if same_const x app_tm then + Expr [Atom "App", opsexp (List.nth (xs, 0)), ast_to_sexp (List.nth (xs, 1))] + else if same_const x locs_tm then locssexp xs + (* a raw mlstring (identifier names etc.) is a SEXSTR *) + else if mlstringSyntax.is_mlstring_literal term then sexstr term + (* generic: nullary constructor -> bare atom; applied -> tagged Expr. This + handles NONE/SOME, Short/Long, Andalso/Orelse, ast_t, and every other + constructor whose tag equals its name. *) + else + case xs of + [] => Atom (const_name x) + | _ => Expr (Atom (const_name x) :: map ast_to_sexp xs) end +(*--------------------------------------------------------------* + Top-level output + *--------------------------------------------------------------*) + +(* Writes the program as a single s-expression: an Expr of the top-level + declarations, with newlines between them for readability (newlines are + whitespace and parse identically to spaces). *) fun write_ast write prog = let - val out = write o exp_to_string o ast_to_exp - val (funcs, _) = listSyntax.dest_list prog - fun step l = - case l of [] => () - | [x] => out x - | x::xs => (out x; write " \n"; step xs) + val out = write o sexp_to_string o ast_to_sexp + val (decs, _) = listSyntax.dest_list prog + fun step [] = () + | step [x] = out x + | step (x::xs) = (out x; write " \n"; step xs) in - write "(\n"; step funcs; write "\n)" + write "(\n"; step decs; write "\n)" end fun write_ast_to_file filename prog = From ccb7f39aa5ea0ad2238f140fe75b3d29cc572c47 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Tue, 9 Jun 2026 20:30:58 +0800 Subject: [PATCH 14/14] Add underscores to make encoding consistent with constructor name --- compiler/parsing/fromSexpScript.sml | 24 ++++++++++---------- unverified/sexpr-bootstrap/astToSexprLib.sml | 14 +----------- 2 files changed, 13 insertions(+), 25 deletions(-) diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml index f2b0c91b8b..89abcb63ae 100644 --- a/compiler/parsing/fromSexpScript.sml +++ b/compiler/parsing/fromSexpScript.sml @@ -764,13 +764,13 @@ Definition sexpop_def: if a = «Aw8sub» then SOME Aw8sub else if a = «Aw8length» then SOME Aw8length else if a = «Aw8update» then SOME Aw8update else - if a = «Aw8subunsafe» then SOME Aw8sub_unsafe else - if a = «Aw8updateunsafe» then SOME Aw8update_unsafe else + if a = «Aw8sub_unsafe» then SOME Aw8sub_unsafe else + if a = «Aw8update_unsafe» then SOME Aw8update_unsafe else if a = «CopyStrStr» then SOME CopyStrStr else if a = «CopyStrAw8» then SOME CopyStrAw8 else if a = «CopyAw8Str» then SOME CopyAw8Str else if a = «CopyAw8Aw8» then SOME CopyAw8Aw8 else - if a = «XorAw8Strunsafe» then SOME XorAw8Str_unsafe else + if a = «XorAw8Str_unsafe» then SOME XorAw8Str_unsafe else if a = «Implode» then SOME Implode else if a = «Explode» then SOME Explode else if a = «Strsub» then SOME Strsub else @@ -787,12 +787,12 @@ Definition sexpop_def: if a = «Asub» then SOME Asub else if a = «Alength» then SOME Alength else if a = «Aupdate» then SOME Aupdate else - if a = «Asubunsafe» then SOME Asub_unsafe else - if a = «Aupdateunsafe» then SOME Aupdate_unsafe else + if a = «Asub_unsafe» then SOME Asub_unsafe else + if a = «Aupdate_unsafe» then SOME Aupdate_unsafe else if a = «ForceThunk» then SOME (ThunkOp ForceThunk) else if a = «ConfigGC» then SOME ConfigGC else if a = «Eval» then SOME Eval else - if a = «Envid» then SOME Env_id else NONE) + if a = «Env_id» then SOME Env_id else NONE) | Expr [Atom tag; arg] => (if tag = «FFI» then lift FFI (odestSEXSTR arg) else if tag = «Shift8Lsl» then lift (Shift W8 Lsl) (odestSXNUM arg) else @@ -1360,13 +1360,13 @@ Definition opsexp_def: (opsexp Aw8sub = Atom «Aw8sub») ∧ (opsexp Aw8length = Atom «Aw8length») ∧ (opsexp Aw8update = Atom «Aw8update») ∧ - (opsexp Aw8sub_unsafe = Atom «Aw8subunsafe») ∧ - (opsexp Aw8update_unsafe = Atom «Aw8updateunsafe») ∧ + (opsexp Aw8sub_unsafe = Atom «Aw8sub_unsafe») ∧ + (opsexp Aw8update_unsafe = Atom «Aw8update_unsafe») ∧ (opsexp CopyStrStr = Atom «CopyStrStr») ∧ (opsexp CopyStrAw8 = Atom «CopyStrAw8») ∧ (opsexp CopyAw8Str = Atom «CopyAw8Str») ∧ (opsexp CopyAw8Aw8 = Atom «CopyAw8Aw8») ∧ - (opsexp XorAw8Str_unsafe = Atom «XorAw8Strunsafe») ∧ + (opsexp XorAw8Str_unsafe = Atom «XorAw8Str_unsafe») ∧ (opsexp Implode = Atom «Implode») ∧ (opsexp Explode = Atom «Explode») ∧ (opsexp Strsub = Atom «Strsub») ∧ @@ -1383,11 +1383,11 @@ Definition opsexp_def: (opsexp Asub = Atom «Asub») ∧ (opsexp Alength = Atom «Alength») ∧ (opsexp Aupdate = Atom «Aupdate») ∧ - (opsexp Asub_unsafe = Atom «Asubunsafe») ∧ - (opsexp Aupdate_unsafe = Atom «Aupdateunsafe») ∧ + (opsexp Asub_unsafe = Atom «Asub_unsafe») ∧ + (opsexp Aupdate_unsafe = Atom «Aupdate_unsafe») ∧ (opsexp ConfigGC = Atom «ConfigGC») ∧ (opsexp Eval = Atom «Eval») ∧ - (opsexp Env_id = Atom «Envid») ∧ + (opsexp Env_id = Atom «Env_id») ∧ (opsexp (FFI s) = Expr [Atom «FFI»; SEXSTR (explode s)]) ∧ (opsexp (ThunkOp ForceThunk) = Atom «ForceThunk») ∧ (opsexp (ThunkOp (AllocThunk m)) = diff --git a/unverified/sexpr-bootstrap/astToSexprLib.sml b/unverified/sexpr-bootstrap/astToSexprLib.sml index 7368053938..da305591a6 100644 --- a/unverified/sexpr-bootstrap/astToSexprLib.sml +++ b/unverified/sexpr-bootstrap/astToSexprLib.sml @@ -91,18 +91,6 @@ fun int_to_string t = val const_name = #1 o dest_const -(* fromSexp$opsexp: most nullary ops use their constructor name verbatim (note - Vsub_unsafe keeps its underscore), but these few are renamed. *) -fun op_tag nm = - case nm of - "Aw8sub_unsafe" => "Aw8subunsafe" - | "Aw8update_unsafe" => "Aw8updateunsafe" - | "XorAw8Str_unsafe" => "XorAw8Strunsafe" - | "Asub_unsafe" => "Asubunsafe" - | "Aupdate_unsafe" => "Aupdateunsafe" - | "Env_id" => "Envid" - | _ => nm - fun width_digits w = case const_name w of "W8" => "8" @@ -164,7 +152,7 @@ fun opsexp t = | "Test" => Expr [Atom "Test", testsexp (List.nth (args, 0)), prim_typesexp (List.nth (args, 1))] | "ThunkOp" => thunkop (hd args) - | nm => Atom (op_tag nm) + | nm => Atom nm end (* fromSexp$litsexp *)