parse open statements

Manual/Tools/polyscripter.sml

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

src/AI/sml_inspection/smlExecute.sml

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

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' = HolParser.fromString false stac;
+val stac' = HolParser.fromString {quietOpen = 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 = HolParser.inputFile file
+    val s1 = HolParser.inputFile {quietOpen = false} file
     val s2 = rm_spaces (rm_comment s1)
     val sl = partial_sml_lexer s2
     val lexdir =  tactictoe_dir ^ "/log/lexer"

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, ...} = HolParser.inputToReader true "" input;
+            val {read, ...} = HolParser.inputToReader {quietOpen = 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, ...} = HolParser.streamToReader true "" TextIO.stdIn
+                val {read, ...} = HolParser.streamToReader {quietOpen = true} "" TextIO.stdIn
               in
                 cgenref := read
               end

tools-poly/poly/quse.sml

@@ -17,12 +17,12 @@ fun use_reader fname (reader as {read = infn0, eof}) =
                            Compiler.CPLineNo (fn () => !lineNo)]) ()
   end
 
-fun use fname = use_reader fname (HolParser.fileToReader fname)
+fun use fname = use_reader fname (HolParser.fileToReader {quietOpen = false} fname)
 
 fun useScript fname =
     let
       val istream = TextIO.openIn fname
-      val reader = HolParser.streamToReader true fname istream
+      val reader = HolParser.streamToReader {quietOpen = false} fname istream
       val _ = use_reader fname reader
               handle e => (TextIO.closeIn istream; PolyML.Exception.reraise e)
     in

tools/Holmake/HolLex

@@ -6,6 +6,7 @@ datatype decl
   = DefinitionDecl of {
       head: int * string, quote: qbody, termination: {tok: int, decls: decls} option,
       end_tok: int option, stop: int}
+  | OpenDecl of {head: int, toks: (int * string) list, stop: int}
   | DatatypeDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
   | QuoteDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
   | QuoteEqnDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int}
@@ -55,6 +56,8 @@ datatype token
   | QuoteEnd of int * string (* from quote, holcomment *)
   | FullQuoteEnd of int * string (* from quote, holcomment *)
   | QDecl of qdecl * token option (* from quote *)
+  | OpenId of int * string (* from opens *)
+  | OpenEnd of int (* from opens *)
   | EOF of int (* from every state *)
 
 type lexresult = token
@@ -180,7 +183,7 @@ fun eof (_:state) = EOF
 
 %%
 %structure HolLex
-%s string stringlbrk comment holcomment quote holstrlit holstrlitlbrk ANTIQ;
+%s string stringlbrk comment holcomment quote holstrlit holstrlitlbrk ANTIQ opens;
 %arg (UserDeclarations.STATE {pardepth, comdepth, comstart, parseError});
 %full
 %posarg
@@ -221,7 +224,8 @@ HOLconjunction = "/\092" | "\226\136\167";
 DefinitionLabelID = {letter}{alphaMLid_tailchar}* | "~"{alphaMLid_tailchar}+ | {HOLconjunction};
 DefinitionLabel = "["{ws}*{DefinitionLabelID}?("["{alphaMLid_list}"]")?{ws}*":"?{ws}*"]";
 Definitionpfx = "Definition"{ws}+{alphaMLid}({ws}*"["{optallws}{defn_attribute_list}"]")?{ws}*":";
-declforms = "val"|"fun"|"structure"|"signature"|"functor"|"abstype"|"datatype"|"exception"|"open"|"infix"[lr]?|"local";
+holstartkeyword = "Datatype"|"Type"|"Overload"|"Definition"|"Theorem"|"Triviality"|"Quote"|("Co")?"Inductive";
+declforms = "val"|"fun"|"structure"|"signature"|"functor"|"type"|"abstype"|"datatype"|"exception"|"open"|"infix"[lr]?|"local"|"in";
 Inductivepfx = ("Co")?"Inductive"{ws}+{alphaMLid}{ws}*":";
 HOLSTRLITstart = "\"" | "\226\128\185" | "\194\171";
 HOLSTRLITend = "\"" | "\226\128\186" | "\194\187";
@@ -336,6 +340,20 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
 <INITIAL>";"{newline} =>
   (if !pardepth = 0 then Decl (Semi yypos, SOME (Decl (Chunk yyend, NONE))) else continue());
 <INITIAL>";" => (if !pardepth = 0 then Decl (Semi yypos, NONE) else continue());
+<INITIAL>"open" => (
+  if !pardepth = 0 then let
+    val _ = YYBEGIN opens
+    fun finish ls p tok =
+      (YYBEGIN INITIAL; Decl (OpenDecl {head = yypos, toks = rev ls, stop = p}, tok))
+    fun parse ls =
+      case continue() of
+        OpenEnd p => finish ls p NONE
+      | OpenId p => parse (p :: ls)
+      | tk as EOF p => finish ls p (SOME tk)
+      | _ => raise Unreachable
+    in parse [] end
+  else continue()
+);
 <INITIAL>{declforms} => (if !pardepth = 0 then Decl (Chunk yypos, NONE) else continue());
 <INITIAL>{MLid} => (continue());
 <INITIAL>{newline}"End" => (EndTok (yyend-3));
@@ -417,4 +435,22 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
   Antiq (BadAntiq yypos, NONE)
 );
 
+<opens>"(*" => (
+  comdepth := 1; YYBEGIN comment;
+  case continue() of
+    Comment => (YYBEGIN opens; continue())
+  | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p)
+  | _ => raise Unreachable
+);
+<opens>({ws}|{newline})+ => (continue());
+<opens>({holstartkeyword}|{declforms}) => (
+  yybufpos := !yybufpos - (yyend - yypos); (* unread token *)
+  OpenEnd yypos
+);
+<opens>{QUALalphaMLid} => (OpenId (yypos, yytext));
+<opens>. => (
+  yybufpos := !yybufpos - 1; (* unread token *)
+  OpenEnd yypos
+);
+
 .|{newline} => (continue());

tools/Holmake/HolParser.sig

@@ -48,9 +48,14 @@ structure ToSML: sig
     {read: int -> string, readAt: int -> int -> (int * substring -> unit) -> unit}
   val mkDoubleReader: (int -> string) -> int -> double_reader
 
-  val mkPullTranslator:
-    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
-    unit -> string
+  type args = {
+    read: int -> string,
+    filename: string,
+    parseError: int * int -> string -> unit,
+    quietOpen: bool
+  }
+
+  val mkPullTranslator: args -> unit -> string
 
   type strcode = {
     aux: string -> unit,
@@ -63,34 +68,26 @@ structure ToSML: sig
   val mkStrcode: (string -> unit) -> strcode
 
   val mkPushTranslatorCore:
-    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
-    strcode -> {
+    args -> strcode -> {
       doDecl: bool -> int -> Simple.decl -> int,
       feed: unit -> Simple.topdecl,
       finishThmVal: unit -> unit,
       regular: int * int -> unit
     }
 
-  val mkPushTranslator:
-    {read: int -> string, filename: string, parseError: int * int -> string -> unit} ->
-    strcode -> unit -> bool
+  val mkPushTranslator: args -> strcode -> unit -> bool
 
 end
 
 type reader = {read : unit -> char option, eof : unit -> bool}
+type args = {quietOpen: bool}
 
-val inputFile : string -> string
-val fromString : bool -> string -> string
-
-val fileToReader : string -> reader
-val stringToReader : bool -> string -> reader
-val inputToReader : bool -> string -> (int -> string) -> reader
-val streamToReader : bool -> string -> TextIO.instream -> reader
-(* bool is true if the stream corresponds to an interactive session
-   (stdin) or a Script file. In both such situations, the magic >- and
-   Theorem-syntax transformations should be performed *)
+val inputFile : args -> string -> string
+val fromString : args -> string -> string
 
-(* In inputFile and fileToReader, the determination is made on whether or
-   not the filename ends in "Script.sml" *)
+val fileToReader : args -> string -> reader
+val stringToReader : args -> string -> reader
+val inputToReader : args -> string -> (int -> string) -> reader
+val streamToReader : args -> string -> TextIO.instream -> reader
 
 end

tools/Holmake/HolParser.sml

@@ -296,11 +296,18 @@ structure ToSML = struct
   }
 
 
+  type args = {
+    read: int -> string,
+    filename: string,
+    parseError: int * int -> string -> unit,
+    quietOpen: bool
+  }
+
   fun mk_mkloc_string (fname,i) =
       String.concat [
         "(DB_dtype.mkloc (", mlquote fname, ", ", Int.toString (i + 1), ", true))"
       ]
-  fun mkPushTranslatorCore {read, filename, parseError}
+  fun mkPushTranslatorCore ({read, filename, parseError, quietOpen}:args)
       ({regular, aux, strstr, strcode = strcode0}:strcode) = let
     open Simple
     val ss = Substring.string
@@ -387,7 +394,13 @@ structure ToSML = struct
         | _ => doQuoteCore start toks stop (SOME (f false))
       in aux "[QUOTE \"("; locpragma start; doQuote0 start toks; aux ")\"]" end
     and doDecl eager pos d = case d of
-        DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let
+        OpenDecl {head = p, toks, stop} => (
+          regular (pos, p); finishThmVal ();
+          if quietOpen then aux "val _ = HOL_Interactive.toggle_quietdec ();" else ();
+          regular (p, stop);
+          if quietOpen then aux " val _ = HOL_Interactive.toggle_quietdec ();" else ();
+          stop)
+      | DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let
         val {keyword, name, attrs, name_attrs} = parseDefinitionPfx head
         val attrs = destAttrs attrs
         val indThm =
@@ -593,28 +606,32 @@ fun exhaust_parser (read, close) =
     recurse []
   end
 
-fun file_to_parser fname = let
+type args = {quietOpen: bool}
+
+fun file_to_parser ({quietOpen}:args) fname = let
   val instrm = openIn fname
   (* val isscript = String.isSuffix "Script.sml" fname *)
   val read = ToSML.mkPullTranslator
-    {read = fn n => input instrm, filename = fname, parseError = K (K ())}
+    {read = fn n => input instrm, filename = fname, parseError = K (K ()), quietOpen = quietOpen}
   in (read, fn () => closeIn instrm) end
 
-fun string_to_parser isscriptp s = let
+fun string_to_parser ({quietOpen}:args) s = let
   val sr = ref s
   fun str_read _ = (!sr before sr := "")
-  val read = ToSML.mkPullTranslator {read = str_read, filename = "", parseError = K (K ())}
+  val read = ToSML.mkPullTranslator
+    {read = str_read, filename = "", parseError = K (K ()), quietOpen = quietOpen}
   in (read, I) end
 
-fun input_to_parser isscriptp fname inp = let
-  val read = ToSML.mkPullTranslator {read = inp, filename = fname, parseError = K (K ())}
+fun input_to_parser ({quietOpen}:args) fname inp = let
+  val read = ToSML.mkPullTranslator
+    {read = inp, filename = fname, parseError = K (K ()), quietOpen = quietOpen}
   in (read, I) end
 
-fun stream_to_parser isscriptp fname strm =
-  input_to_parser isscriptp fname (fn n => input strm)
+fun stream_to_parser args fname strm =
+  input_to_parser args fname (fn n => input strm)
 
-fun inputFile fname = exhaust_parser (file_to_parser fname)
-fun fromString b s = exhaust_parser (string_to_parser b s)
+fun inputFile args fname = exhaust_parser (file_to_parser args fname)
+fun fromString args s = exhaust_parser (string_to_parser args s)
 
 fun mkReaderEOF (read, close) = let
   val i = ref 0
@@ -630,9 +647,9 @@ fun mkReaderEOF (read, close) = let
   fun eof () = !eofp
   in {read = doit, eof = eof} end
 
-fun fileToReader fname = mkReaderEOF (file_to_parser fname)
-fun stringToReader b s = mkReaderEOF (string_to_parser b s)
-fun inputToReader b fnm inp = mkReaderEOF (input_to_parser b fnm inp)
-fun streamToReader b fnm strm = mkReaderEOF (stream_to_parser b fnm strm)
+fun fileToReader args fname = mkReaderEOF (file_to_parser args fname)
+fun stringToReader args s = mkReaderEOF (string_to_parser args s)
+fun inputToReader args fnm inp = mkReaderEOF (input_to_parser args fnm inp)
+fun streamToReader args fnm strm = mkReaderEOF (stream_to_parser args fnm strm)
 
 end

tools/Holmake/Holdep.sml

@@ -124,7 +124,7 @@ fun encode_for_HOLMKfile {tgt, deps} =
 
 fun uqfname_holdep fname =
   let
-    val reader = HolParser.fileToReader fname
+    val reader = HolParser.fileToReader {quietOpen = false} fname
   in
     Holdep_tokens.reader_deps (fname, #read reader)
   end

tools/Holmake/holdeptool.sml

@@ -23,7 +23,7 @@ fun main() = let
                  handle LEX_ERROR s => diewith("Lexical error: " ^ s)
                       | e => diewith ("Exception: "^General.exnMessage e))
         | ["-h"] => usage ok
-        | [fname] => (reader_deps (fname, #read (HolParser.fileToReader fname))
+        | [fname] => (reader_deps (fname, #read (HolParser.fileToReader {quietOpen = false} fname))
                       handle LEX_ERROR s => diewith("Lexical error: " ^ s)
                            | e => diewith ("Exception: "^General.exnMessage e))
         | _ => usage die

tools/mllex/mllex.sml

@@ -1300,11 +1300,11 @@ fun lexGen infile =
 	 say   "\t\t                  else action(l,NewAcceptingLeaves";
 	 if !UsesTrailingContext then
 	    sayln ",nil))" else sayln "))";
-	 sayln "\t\t  else (if i0=l then yyb := newchars";
-	 sayln "\t\t     else yyb := String.substring(!yyb,i0,l-i0)^newchars;";
-	 sayln "\t\t     yygone := !yygone+i0;";
+	 sayln "\t\t  else (";
+	 sayln "\t\t     yyb := String.substring(!yyb,i0-1,l-i0+1)^newchars;";
+	 sayln "\t\t     yygone := !yygone+i0-1;";
 	 sayln "\t\t     yybl := String.size (!yyb);";
-	 sayln "\t\t     scan (s,AcceptingLeaves,l-i0,0))";
+	 sayln "\t\t     scan (s,AcceptingLeaves,l-i0+1,1))";
 	 sayln "\t    end";
 	 sayln "\t  else let val NewChar = Char.ord (CharVector.sub (!yyb,l))";
          if !CharSetSize=129

tools/quote-filter/poly-unquote.ML

@@ -29,8 +29,8 @@ fun main() = let
      linked executable as Interrupt exceptions *)
   val _ = Signal.signal(2, Signal.SIG_HANDLE
                                (fn _ => Thread.Thread.broadcastInterrupt()))
-  val {instrm, outstrm, interactive, quotefixp, closefn, infilename} =
-      qfilter_util.processArgs(false,false,false) (CommandLine.arguments())
+  val {instrm, outstrm, interactive, quotefixp, quietOpen, closefn, infilename} =
+      qfilter_util.processArgs(false,false,false,false) (CommandLine.arguments())
 
 (* with many thanks to Ken Friis Larsen, Peter Sestoft, Claudio Russo and
    Kenn Heinrich who helped me see the light with respect to this code *)
@@ -46,7 +46,8 @@ fun main() = let
       filename = infilename,
       parseError = fn (start, stop) => fn s =>
         TextIO.output (TextIO.stdErr,
-          "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n")
+          "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n"),
+      quietOpen = quietOpen
     } (mkStrcode write)
 
     fun loop () = if read () then () else loop ()

tools/quote-filter/qfilter_util.sig

@@ -1,13 +1,14 @@
 signature qfilter_util =
 sig
 
-  val processArgs : bool * bool * bool -> string list ->
+  val processArgs : bool * bool * bool * bool -> string list ->
                     {instrm: TextIO.instream,
                      outstrm: TextIO.outstream,
                      interactive: bool,
                      quotefixp: bool,
                      closefn: unit -> unit,
-                     infilename: string
+                     infilename: string,
+                     quietOpen: bool
                     }
 
 end