Switch to more efficient sexp datatype

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\

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\

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 []);
 

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)

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