From 630f26504893f06eac0faafac53b87fb39af7aba Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 30 Sep 2024 17:27:17 +0200
Subject: [PATCH] zero-repl: ensure all commands in block are processed

---
 tools-poly/holrepl.ML                   |  19 +++++++++++--------
 tools/Holmake/tests/repl/Holmakefile    |   7 +++++--
 tools/Holmake/tests/repl/test5.expected | Bin 0 -> 129 bytes
 tools/Holmake/tests/repl/test5.input    | Bin 0 -> 4 bytes
 4 files changed, 16 insertions(+), 10 deletions(-)
 create mode 100644 tools/Holmake/tests/repl/test5.expected
 create mode 100644 tools/Holmake/tests/repl/test5.input

diff --git a/tools-poly/holrepl.ML b/tools-poly/holrepl.ML
index c2e4f531b9..28269c247c 100644
--- a/tools-poly/holrepl.ML
+++ b/tools-poly/holrepl.ML
@@ -154,26 +154,29 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
               | chunk => process chunk)
             | Current chunk => process chunk
 
-          (* Returns true and moves to the next state if another statement
-             is ready. *)
+          (* Moves to the next state if another statement is ready. *)
           fun finishCommand () =
             case !state of
-              Next s => (state := Current s; true)
-            | _ => false
+              Next s => state := Current s
+            | _ => () (* this can only happen if endOfFile is true *)
 
         in fn () =>
           let
             (* Create a new lexer for each command block. *)
-            val {read, ...} = QFRead.inputToReader true input
+            val {read, ...} = QFRead.inputToReader true input;
+            val endOfBlock = ref false;
+            fun read' () = case read () of
+                NONE => (endOfBlock := true; NONE)
+              | ch => ch;
 
             fun readEvalPrint compileAcc runAcc =
               let
                 val {compileTime, runTime, result} =
-                  readEvalPrint1 read (fn () => ());
+                  readEvalPrint1 read' (fn () => ());
                 val () = reportResult result;
               in
-                if !endOfFile orelse finishCommand () then
-                  reportTiming compileTime runTime
+                if !endOfBlock then
+                  (finishCommand (); reportTiming compileTime runTime)
                 else
                   readEvalPrint (compileAcc + compileTime) (runAcc + runTime)
               end;
diff --git a/tools/Holmake/tests/repl/Holmakefile b/tools/Holmake/tests/repl/Holmakefile
index cb6625edf8..7e22dadf2a 100644
--- a/tools/Holmake/tests/repl/Holmakefile
+++ b/tools/Holmake/tests/repl/Holmakefile
@@ -7,11 +7,10 @@ HOL = $(protect $(HOLDIR)/bin/hol.bare) --zero
 CMP = diff
 
 ifdef POLY
-DEPS = test1.out test2.out test3.out test4.out
+DEPS = test1.out test2.out test3.out test4.out test5.out
 
 # FIXME: % in targets doesn't work
 test1.out: test1.input test1.expected
-	echo $(DEPS)
 	$(HOL) < $< | tail -n +8 > $@
 	$(CMP) $@ $(patsubst %.input,%.expected,$<)
 
@@ -27,6 +26,10 @@ test4.out: test4.input test4.expected
 	$(HOL) < $< | tail -n +8 > $@
 	$(CMP) $@ $(patsubst %.input,%.expected,$<)
 
+test5.out: test5.input test5.expected
+	$(HOL) < $< | tail -n +8 > $@
+	$(CMP) $@ $(patsubst %.input,%.expected,$<)
+
 endif
 
 all: $(DEFAULT_TARGETS) $(DEPS)
diff --git a/tools/Holmake/tests/repl/test5.expected b/tools/Holmake/tests/repl/test5.expected
new file mode 100644
index 0000000000000000000000000000000000000000..2bb5812a8bf976b28cec8e9e1479eafc45aed934
GIT binary patch
literal 129
zcmX}iF%E+;3`XJ1ImJKHY-L31-hqKDxYV>(T?ZwGUcVqD#!v61gg(;~Gx-}$Wrl7X
zcCA!|9?BP3{$b4KBv#Ra&5Ll2DS;;EvbVaZi@k8q`lSy~qT3L|N(yn@aP1)G@pOAQ
Fgg*|fDZ2mw

literal 0
HcmV?d00001

diff --git a/tools/Holmake/tests/repl/test5.input b/tools/Holmake/tests/repl/test5.input
new file mode 100644
index 0000000000000000000000000000000000000000..a606bcbbeed76d861977e30e7c8af4a6c5a8103b
GIT binary patch
literal 4
LcmXrCHevt(0o?$f

literal 0
HcmV?d00001