Merge pull request #1333 from digama0/holparser

New and improved HOL parser
HOL-Theorem-Prover · Nov 22, 2024 · 468671a · 468671a
2 parents 59560b9 + 568acd0
commit 468671a
Show file tree

Hide file tree

Showing 35 changed files with 1,623 additions and 414 deletions.
diff --git a/Manual/Tools/polyscripter.sml b/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)

diff --git a/developers/genUseScript.sml b/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";
 

diff --git a/src/AI/sml_inspection/smlExecute.sml b/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
     (