New and improved HOL parser

Manual/Tools/polyscripter.sml

@@ -17,11 +17,11 @@ fun lnumdie linenum extra exn =
 
 val outputPrompt = ref "> "
 
-val quote = QFRead.fromString
+val quote = HolParser.fromString
 val default_linewidth = 77
 
 fun quoteFile lnum fname =
-  QFRead.inputFile fname handle e => lnumdie lnum "" e
+  HolParser.inputFile fname handle e => lnumdie lnum "" e
 
 datatype lbuf =
          LB of {
@@ -319,7 +319,7 @@ fun process_line debugp umap obuf origline lbuf = let
     end
   val assertcmd = "##assert "
   val assertcmdsz = size assertcmd
-  val stringCReader = #read o QFRead.stringToReader true
+  val stringCReader = #read o HolParser.stringToReader true
   fun compile exnhandle input =
       (if debugp then
          TextIO.output(TextIO.stdErr, input)

developers/genUseScript.sml

@@ -39,9 +39,9 @@ in
   (push, read, reset)
 end;
 
-val _ = use "../tools/Holmake/QuoteFilter.sml";
-val _ = use "../tools/Holmake/QFRead.sig";
-val _ = use "../tools/Holmake/QFRead.sml";
+val _ = use "../tools/Holmake/HolLex.sml";
+val _ = use "../tools/Holmake/HolParser.sig";
+val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "../tools/Holmake/Holdep_tokens.sig"
 val _ = use "../tools/Holmake/Holdep_tokens.sml";
 

src/AI/sml_inspection/smlExecute.sml

@@ -29,7 +29,7 @@ val sml_thml_glob = ref []
 
 fun quse_string s =
   let
-    val stream = TextIO.openString (QFRead.fromString false s)
+    val stream = TextIO.openString (HolParser.fromString false s)
     fun infn () = TextIO.input1 stream
   in
     (

src/probability/borelScript.sml

@@ -8120,8 +8120,8 @@ Theorem IN_MEASURABLE_BOREL_POW_EXP:
         (!x. x IN space a ==> h x = (f x) pow (g x)) ==> h IN Borel_measurable a
 Proof
     rw[] >> simp[Once IN_MEASURABLE_BOREL_PLUS_MINUS] >>
-    ‘!P. {x | P (g x)} INTER space a IN subsets a` by (rw[] >>
-        `{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by (
+    ‘!P. {x | P (g x)} INTER space a IN subsets a’ by (rw[] >>
+        ‘{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by (
             rw[Once EXTENSION,IN_BIGUNION] >> eq_tac >> strip_tac >> gvs[] >>
             qexists_tac ‘{y | g y = g x} INTER space a’ >> simp[] >> qexists_tac ‘g x’ >> simp[]) >>
         pop_assum SUBST1_TAC >> irule SIGMA_ALGEBRA_COUNTABLE_UNION >>
@@ -8130,19 +8130,19 @@ Proof
     map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> qexistsl_tac qex >> simp ths) [
         (Pos hd,IN_MEASURABLE_BOREL_ADD',[‘λx. fn_minus f x pow g x * indicator_fn {x | EVEN (g x)} x’,
             ‘λx. fn_plus f x pow g x * indicator_fn {x | $< 0 (g x)} x’],[]),
-        (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}`,`λx. fn_minus f x pow g x’],[]),
+        (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}’,‘λx. fn_minus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | EVEN (g x)} INTER space a’],[]),
-        (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}`,`λx. fn_plus f x pow g x’],[]),
+        (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}’,‘λx. fn_plus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | $< 0 (g x)} INTER space a’],[]),
-        (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}`,`λx. fn_minus f x pow g x’],[]),
+        (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}’,‘λx. fn_minus f x pow g x’],[]),
         (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | ODD (g x)} INTER space a’],[])] >>
     pop_assum kall_tac >>
     ‘!pf. pf IN Borel_measurable a /\ (!x. 0 <= pf x) ==> (λx. pf x pow g x) IN Borel_measurable a’ by (
         rw[] >> irule IN_MEASURABLE_BOREL_SUMINF >> simp[] >>
         qexistsl_tac [‘λn x. pf x pow n * indicator_fn {x | g x = n} x’] >> simp[pow_pos_le,INDICATOR_FN_POS,le_mul] >>
         simp[RIGHT_AND_FORALL_THM] >> strip_tac >>
         map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> simp[] >> qexistsl_tac qex >> simp ths) [
-            (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}`,`λx. pf x pow n’],[]),
+            (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}’,‘λx. pf x pow n’],[]),
             (Pos hd,IN_MEASURABLE_BOREL_POW',[‘n’,‘pf’],[]),
             (Pos hd,IN_MEASURABLE_BOREL_INDICATOR,[‘{x | g x = n} INTER space a’],[indicator_fn_def])] >>
         rw[] >> qspecl_then [‘g x’,‘pf x pow g x’] mp_tac ext_suminf_sing_general >>

src/tactictoe/examples/ttt_demoScript.sml

@@ -31,7 +31,7 @@ open listTheory
 (* ttt ([],``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``); *)
 val ex2 = store_thm("ex2",
   ``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``,
-  asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss)) [LIST_EQ_REWRITE] >>
+  asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss) [LIST_EQ_REWRITE] >>
   metis_tac [EL_MAP, rich_listTheory.EL_REPLICATE]
   );
 

src/tactictoe/src/tttToken.sml

@@ -175,7 +175,7 @@ fun inst_term sterm stac =
 (*
 load "tttToken"; open tttToken;
 val stac = "EXISTS_TAC ``1:num``";
-val stac' = QFRead.fromString false stac;
+val stac' = HolParser.fromString false stac;
 val (astac,sterm) = valOf (abstract_term stac');
 val istac = inst_term "2:num" astac;
 *)

src/tactictoe/src/tttUnfold.sml

@@ -973,7 +973,7 @@ fun rm_spaces s =
 
 fun sketch_wrap thy file =
   let
-    val s1 = QFRead.inputFile file
+    val s1 = HolParser.inputFile file
     val s2 = rm_spaces (rm_comment s1)
     val sl = partial_sml_lexer s2
     val lexdir =  tactictoe_dir ^ "/log/lexer"

tools-poly/configure.sml

@@ -425,13 +425,13 @@ val _ = work_in_dir
 val _ = work_in_dir
           "Holmake" (fullPath [HOLDIR, "tools", "Holmake", "poly"])
           (fn () => (OS.FileSys.chDir "..";
-                     systeml [lexer, "QuoteFilter"] ;
+                     systeml [lexer, "HolLex"];
                      OS.FileSys.chDir "poly";
                      polyc_compile (SOME "../mlton/Holmake.mlb")
                                    "poly-Holmake.ML" hmakebin))
 
 (* unquote - the quotation filter *)
-val _ = work_in_dir "unquote." qfdir
+val _ = work_in_dir "unquote" qfdir
                     (fn () => (polyc_compile NONE "poly-unquote.ML" qfbin))
 
 (* holdeptool *)

tools-poly/holrepl.ML

@@ -163,7 +163,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
         in fn () =>
           let
             (* Create a new lexer for each command block. *)
-            val {read, ...} = QFRead.inputToReader true input;
+            val {read, ...} = HolParser.inputToReader true input;
             val endOfBlock = ref false;
             fun read' () = case read () of
                 NONE => (endOfBlock := true; NONE)
@@ -195,7 +195,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
           fun cgen() = !cgenref()
           fun bind_cgen () =
               let
-                val {read, ...} = QFRead.streamToReader true TextIO.stdIn
+                val {read, ...} = HolParser.streamToReader true TextIO.stdIn
               in
                 cgenref := read
               end

tools-poly/poly-build.ML

@@ -17,8 +17,8 @@ val _ = useC "HOLFileSys";
 val _ = useC "Holdep_tokens";
 val _ = useC "HM_SimpleBuffer";
 val _ = useC "AttributeSyntax";
-val _ = use "../tools/Holmake/QuoteFilter.sml";
-val _ = useC "QFRead";
+val _ = use "../tools/Holmake/HolLex.sml";
+val _ = useC "HolParser";
 val _ = useC "Holdep";
 val _ = use "../tools/Holmake/Holmake_tools_dtype.sml";
 val _ = use "../tools/Holmake/terminal_primitives.sig";

tools-poly/poly/poly-init2.ML

@@ -6,7 +6,7 @@ val _ = use "Holmake/Systeml.sml"
 
 val _ = use "../tools/Holmake/AttributeSyntax.sig";
 val _ = use "../tools/Holmake/AttributeSyntax.sml";
-val _ = use "../tools/Holmake/QuoteFilter.sml";
+val _ = use "../tools/Holmake/HolLex.sml";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sig";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sml";
 val _ = use "../tools/Holmake/HOLFS_dtype.sml";
@@ -15,8 +15,8 @@ val _ = use "../tools/Holmake/poly/HFS_NameMunge.sml";
 val _ = use "../tools/Holmake/HOLFS_dtype.sml";
 val _ = use "../tools/Holmake/HOLFileSys.sig";
 val _ = use "../tools/Holmake/HOLFileSys.sml";
-val _ = use "../tools/Holmake/QFRead.sig";
-val _ = use "../tools/Holmake/QFRead.sml";
+val _ = use "../tools/Holmake/HolParser.sig";
+val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "poly/quse.sig";
 val _ = use "poly/quse.sml";
 

tools-poly/poly/quse.sml

@@ -1,7 +1,7 @@
 structure QUse :> QUse =
 struct
 
-fun use_reader fname (reader as {read = infn0, eof, reset}) =
+fun use_reader fname (reader as {read = infn0, eof}) =
   let
     val lineNo = ref 1
     fun infn () =
@@ -17,12 +17,12 @@ fun use_reader fname (reader as {read = infn0, eof, reset}) =
                            Compiler.CPLineNo (fn () => !lineNo)]) ()
   end
 
-fun use fname = use_reader fname (QFRead.fileToReader fname)
+fun use fname = use_reader fname (HolParser.fileToReader fname)
 
 fun useScript fname =
     let
       val istream = TextIO.openIn fname
-      val reader = QFRead.streamToReader true istream
+      val reader = HolParser.streamToReader true istream
       val _ = use_reader fname reader
               handle e => (TextIO.closeIn istream; raise e)
     in

tools/Holmake/.gitignore

@@ -1 +1,2 @@
 QuoteFilter.sml
+HolLex.sml

tools/Holmake/AttributeSyntax.sig

@@ -2,6 +2,7 @@ signature AttributeSyntax =
 sig
 
   val mk_strsafe : string -> string
+  val bslash_escape : char -> string
   val bslash_escape_s : string -> string
   val dest_ml_thm_binding : string -> {keyword: string, name : string,
                                        name_attr_original : string,