Zero-terminated repl v2

tools-poly/holrepl.ML

@@ -35,19 +35,6 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
        EOT to the command we were running. *)
     val endOfFile    = ref false;
 
-    (* It seems like the only way to *really* reset a lexer, in particular, to
-       force it back into its INITIAL state, is to create a fresh one. So,
-       this is what bind_cgen() does, and this is what is called in the
-       compile-fail exception handler below. *)
-    val cgenref = ref (fn () => SOME #"\000")
-    fun cgen() = !cgenref()
-    fun bind_cgen () =
-        let
-          val {read, ...} = QFRead.streamToReader true TextIO.stdIn
-        in
-          cgenref := read
-        end
-
     fun reportTiming compileTime runTime =
       (* Print the times if required. *)
       if !timing
@@ -65,16 +52,14 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
             | SOME loc => [ContextLocation loc]
         in
           PolyML.prettyPrint(TextIO.print, !lineLength)
-            (PrettyBlock(0, false, [],
-                        [
-                          PrettyBlock(0, false, exLoc,
-                                      [PrettyString "Exception-"]),
-                          PrettyBreak(1, 3),
-                          prettyRepresentation(exn,
-                                                FixedInt.fromInt
-                                                  (! printDepth)),
-                          PrettyBreak(1, 3),
-                          PrettyString "raised"
+            (PrettyBlock(0, false, [], [
+              PrettyBlock(0, false, exLoc,
+                [PrettyString "Exception-"]),
+              PrettyBreak(1, 3),
+              prettyRepresentation(exn,
+                FixedInt.fromInt (! printDepth)),
+              PrettyBreak(1, 3),
+              PrettyString "raised"
             ]));
           PolyML.Exception.reraise exn
         end
@@ -105,7 +90,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
           open PolyML.Compiler
         in
           polyCompiler (readin, [CPNameSpace nameSpace,
-                                  CPOutStream TextIO.print])
+                                 CPOutStream TextIO.print])
         end
             (* Don't print any times if this raises an exception. *)
             handle exn as Fail s => (
@@ -132,51 +117,86 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
     val readEvalPrint : unit -> unit =
       if zeroTerm then
         let
-          val endOfCommand = ref false;
-
           (* Initial prompt / end of splash message *)
           val () = printOut "\000";
 
-          (* Each character typed is fed into the compiler but a "\0"
-             terminates the input. *)
-          fun readin () =
-            case cgen() of
-              NONE => (endOfFile := true; NONE)
-            | SOME #"\000" => (endOfCommand := true; NONE)
-            | SOME ch => SOME ch;
+          (* The input state is one of:
+             * `Current ""`: initial state, we have no pending input chunk
+             * `Current chunk`: we have a pending input chunk in the
+               current command
+             * `Next chunk`: The input to the current command is exhausted,
+               and `chunk` is pending input for the next command *)
+          datatype state =
+            Current of string
+          | Next of string
+          val state = ref (Current "");
 
-          (* Remove all buffered but unread input. *)
-          fun flushInput () =
-            case cgen () of
-              NONE => endOfFile := true
-            | SOME #"\000" => ()
-            | SOME ch => flushInput ();
+          (* Parse a pending input chunk, splitting on the first zero byte *)
+          fun process chunk =
+            let fun findZero i =
+              if i < String.size chunk then
+                if String.sub(chunk,i) = #"\000" then
+                 (state := Next (String.extract(chunk,i+1,NONE));
+                  String.substring(chunk,0,i))
+                else findZero (i+1)
+              else (state := Current ""; chunk)
+            in findZero 0 end
 
-          fun resetAfterCompileFail () = (
-            if !endOfCommand then () else flushInput();
-            endOfCommand := false;
-            bind_cgen()
-          );
+          (* This is the input function we give to the lexer. It filters `stdIn`
+             to ensure that we do not yield any data to it which is not for
+             this command, and also avoid data loss if it asks for more from
+             the stream. *)
+          fun input _ =
+            case !state of
+              Next _ => ""
+            | Current "" => (case TextIO.input TextIO.stdIn of
+                "" => (endOfFile := true; "")
+              | chunk => process chunk)
+            | Current chunk => process chunk
 
-          fun readEvalPrint compileAcc runAcc =
-            let
-              val () = bind_cgen();
-              val {compileTime, runTime, result} =
-                readEvalPrint1 readin resetAfterCompileFail;
-              val () = reportResult result;
-            in
-              if !endOfCommand orelse !endOfFile then
-                reportTiming compileTime runTime
-              else
-                readEvalPrint (compileAcc + compileTime) (runAcc + runTime)
-            end;
+          (* Returns true and moves to the next state if another statement
+             is ready. *)
+          fun finishCommand () =
+            case !state of
+              Next s => (state := Current s; true)
+            | _ => false
 
-        in fn () => readEvalPrint Time.zeroTime Time.zeroTime end
+        in fn () =>
+          let
+            (* Create a new lexer for each command block. *)
+            val {read, ...} = QFRead.inputToReader true input
+
+            fun readEvalPrint compileAcc runAcc =
+              let
+                val {compileTime, runTime, result} =
+                  readEvalPrint1 read (fn () => ());
+                val () = reportResult result;
+              in
+                if !endOfFile orelse finishCommand () then
+                  reportTiming compileTime runTime
+                else
+                  readEvalPrint (compileAcc + compileTime) (runAcc + runTime)
+              end;
+          in readEvalPrint Time.zeroTime Time.zeroTime end
+        end
       else (* not zeroTerm *)
         let
           val realDataRead = ref false;
           val lastWasEol   = ref true;
 
+          (* It seems like the only way to *really* reset a lexer, in particular, to
+            force it back into its INITIAL state, is to create a fresh one. So,
+            this is what bind_cgen() does, and this is what is called in the
+            compile-fail exception handler below. *)
+          val cgenref = ref (fn () => SOME #"\000")
+          fun cgen() = !cgenref()
+          fun bind_cgen () =
+              let
+                val {read, ...} = QFRead.streamToReader true TextIO.stdIn
+              in
+                cgenref := read
+              end
+
           val () = bind_cgen();
 
           (* Each character typed is fed into the compiler but leading

tools/Holmake/QFRead.sig

@@ -9,6 +9,7 @@ val fromString : bool -> string -> string
 
 val fileToReader : string -> reader
 val stringToReader : bool -> string -> reader
+val inputToReader : bool -> (int -> string) -> reader
 val streamToReader : bool -> 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

tools/Holmake/QFRead.sml

@@ -43,14 +43,17 @@ fun string_to_lexer isscriptp s =
     (#2 o read, (fn () => ()), reset qstate)
   end
 
-fun stream_to_lexer isscriptp strm =
+fun input_to_lexer isscriptp inp =
   let
     val qstate = QuoteFilter.UserDeclarations.newstate (mkstate isscriptp)
-    val read = QuoteFilter.makeLexer (fn n => input strm) qstate
+    val read = QuoteFilter.makeLexer inp qstate
   in
     (#2 o read, (fn () => ()), reset qstate)
   end
 
+fun stream_to_lexer isscriptp strm =
+  input_to_lexer isscriptp (fn n => input strm)
+
 fun inputFile fname = exhaust_lexer (file_to_lexer fname)
 fun fromString b s = exhaust_lexer (string_to_lexer b s)
 
@@ -72,6 +75,7 @@ end
 
 fun fileToReader fname = mkReaderEOF (file_to_lexer fname)
 fun stringToReader b s = mkReaderEOF (string_to_lexer b s)
+fun inputToReader b inp = mkReaderEOF (input_to_lexer b inp)
 fun streamToReader b strm = mkReaderEOF (stream_to_lexer b strm)
 
 end

tools/Holmake/tests/repl/Holmakefile

@@ -0,0 +1,34 @@
+.PHONY: all
+
+INCLUDES = $(HOLDIR)/tools/cmp
+
+HOL = $(protect $(HOLDIR)/bin/hol.bare) --zero
+# CMP = $(protect $(HOLDIR)/tools/cmp/cmp.exe)
+CMP = diff
+
+ifdef POLY
+DEPS = test1.out test2.out test3.out test4.out
+
+# FIXME: % in targets doesn't work
+test1.out: test1.input test1.expected
+	echo $(DEPS)
+	$(HOL) < $< | tail -n +8 > $@
+	$(CMP) $@ $(patsubst %.input,%.expected,$<)
+
+test2.out: test2.input test2.expected
+	$(HOL) < $< | tail -n +8 > $@
+	$(CMP) $@ $(patsubst %.input,%.expected,$<)
+
+test3.out: test3.input test3.expected
+	$(HOL) < $< | tail -n +8 > $@
+	$(CMP) $@ $(patsubst %.input,%.expected,$<)
+
+test4.out: test4.input test4.expected
+	$(HOL) < $< | tail -n +8 > $@
+	$(CMP) $@ $(patsubst %.input,%.expected,$<)
+
+endif
+
+all: $(DEFAULT_TARGETS) $(DEPS)
+
+EXTRA_CLEANS = $(wildcard *.out)

tools/Holmake/tests/repl/test1.input

@@ -0,0 +1 @@
+1

tools/sequences/kernel

@@ -32,4 +32,5 @@ src/proofman
 !src/proofman/tests
 !tools/Holmake/tests/preexec
 !tools/Holmake/tests/parallel_tests
+!tools/Holmake/tests/repl
 !src/1/theory_tests