Renamed [Lr1.entry_nt] to [Lr1.entry_of_nt].

Added [Lr1.nt_of_entry].
Implemented [ReferenceInterpreter.check_error_path].

src/lr1.ml

@@ -1072,10 +1072,28 @@ let fold_entry f accu =
     f prod state nt t accu
   ) entry accu
 
-let entry_nt nt =
+let entry_of_nt nt =
   (* Find the entry state that corresponds to [nt]. *)
   try
     ProductionMap.find (Production.startsymbol2startprod nt) entry
   with Not_found ->
     assert false
 
+exception Found of Nonterminal.t
+
+let nt_of_entry s =
+  (* [s] should be an initial state. *)
+  assert (incoming_symbol s = None);
+  try
+    ProductionMap.iter (fun prod entry ->
+      if Node.compare s entry = 0 then
+        match Production.classify prod with
+        | None ->
+            assert false
+        | Some nt ->
+            raise (Found nt)
+    ) entry;
+    (* This should not happen if [s] is indeed an initial state. *)
+    assert false
+  with Found nt ->
+    nt

src/lr1.mli

@@ -37,10 +37,11 @@ val fold_entry:
   (Production.index -> node -> Nonterminal.t -> Stretch.ocamltype -> 'a -> 'a) ->
   'a -> 'a
 
-(* This maps a (user) non-terminal start symbol to the corresponding
-   start state. *)
+(* [entry_of_nt] maps a (user) non-terminal start symbol to the corresponding
+   start state. [nt_of_entry] does the reverse. *)
 
-val entry_nt: Nonterminal.t -> node
+val entry_of_nt: Nonterminal.t -> node
+val nt_of_entry: node -> Nonterminal.t
 
 (* Nodes are numbered sequentially from [0] to [n-1]. *)
 

src/referenceInterpreter.ml

 open Grammar
 open Cst
 
+(* ------------------------------------------------------------------------ *)
+
 (* Set up all of the information required by the LR engine. Everything is
    read directly from [Grammar] and [Lr1]. *)
 
@@ -204,6 +206,8 @@ module T = struct
 
 end
 
+(* ------------------------------------------------------------------------ *)
+
 (* Define a palatable user entry point. *)
 
 let interpret log nt lexer lexbuf =
@@ -220,15 +224,29 @@ let interpret log nt lexer lexbuf =
   (* Run it. *)
 
   try
-    Some (E.entry (Lr1.entry_nt nt) lexer lexbuf)
+    Some (E.entry (Lr1.entry_of_nt nt) lexer lexbuf)
   with T.Error ->
     None
 
+(* ------------------------------------------------------------------------ *)
+
 (* Another entry point, used internally by [Coverage] to check that the
    sentences that [Coverage] produces do lead to an error in the expected
    state. *)
 
-let _check nt (_path : Terminal.t list) (_z : Terminal.t) =
+open MenhirLib.General (* streams *)
+
+type check_error_path_outcome =
+  (* Bad: the input was read past its end. *)
+| OInputReadPastEnd
+  (* Bad: a syntax error occurred before all of the input was read. *)
+| OInputNotFullyConsumed
+  (* Bad: the parser unexpectedly accepted (part of) this input. *)
+| OUnexpectedAccept
+  (* Good: a syntax error occurred after reading the last input token. *)
+| OK of Lr1.node
+
+let check_error_path nt input =
 
   (* Instantiate the LR engine. *)
 
@@ -239,12 +257,61 @@ let _check nt (_path : Terminal.t list) (_z : Terminal.t) =
     end)
   in
 
-  (* Run it. *)
+  (* Set up a function that delivers tokens one by one. *)
 
-  let _s = Lr1.entry_nt nt in
+  let input = ref input in
+  let next () =
+    match !input with
+    | [] ->
+        None
+    | t :: ts ->
+        input := ts;
+        Some t
+  in
 
-  (* TEMPORARY use the incremental API to drive the engine, step by step,
-     up to the expected error. *)
+  (* Run it. We wish to stop at the first error (without handling the error
+     in any way) and report in which state the error occurred. A clean way
+     of doing this is to use the incremental API, as follows. The main loop
+     resembles the [loop] function in [Engine]. *)
+
+  let entry = Lr1.entry_of_nt nt in
+
+  let rec loop (result : cst E.result) =
+    match result with
+    | E.InputNeeded _ ->
+        begin match next() with
+        | None ->
+            OInputReadPastEnd
+        | Some t ->
+            let dummy = Lexing.dummy_pos in
+            loop (E.offer result (t, dummy, dummy))
+        end
+    | E.Shifting _
+    | E.AboutToReduce _ ->
+        loop (E.resume result)
+    | E.HandlingError env ->
+        (* Check that all of the input has been read. Otherwise, the error
+           has occurred sooner than expected. *)
+        if !input = [] then
+          (* Return the current state. This is done by peeking at the stack.
+             If the stack is empty, then we must be in the initial state. *)
+          OK (
+            match Lazy.force (E.stack env) with
+            | Nil ->
+                entry
+            | Cons (E.Element (s, _, _, _), _) ->
+                s
+          )
+        else
+          OInputNotFullyConsumed
+    | E.Accepted _ ->
+        (* The parser has succeeded. This is unexpected. *)
+        OUnexpectedAccept
+    | E.Rejected ->
+        (* The parser rejects this input. This should not happen; we
+           should observe [HandlingError _] first. *)
+        assert false
+  in
 
-  ()
+  loop (E.start entry)
 

src/referenceInterpreter.mli

@@ -19,3 +19,22 @@ val interpret:
   Lexing.lexbuf ->
   cst option
 
+(* This variant of the reference interpreter is used internally by us. We use
+   it to debug [Coverage]. It checks that a sentence leads to a syntax error
+   in the expected state. *)
+
+type check_error_path_outcome =
+  (* Bad: the input was read past its end. *)
+| OInputReadPastEnd
+  (* Bad: a syntax error occurred before all of the input was read. *)
+| OInputNotFullyConsumed
+  (* Bad: the parser unexpectedly accepted (part of) this input. *)
+| OUnexpectedAccept
+  (* Good: a syntax error occurred after reading the last input token. *)
+| OK of Lr1.node
+
+val check_error_path:
+  Nonterminal.t ->   (* initial non-terminal symbol *)
+  Terminal.t list -> (* input  *)
+  check_error_path_outcome
+