From 95a1c22b9a2638b3800426f462cce2723a93801c Mon Sep 17 00:00:00 2001
From: =?UTF8?q?Fran=C3=A7ois=20Pottier?=
Date: Wed, 3 Dec 2014 14:32:16 +0100
Subject: [PATCH] Change the reference interpreter's [semantic_action] function
so that it does not write [env.current]. This was easy, as the write to
[env.current] was in fact unobservable and could be replaced with a write to
a local reference [current]. At the same time, changed the local recursive
function [pop] to a loop, for greater readability.

src/referenceInterpreter.ml  85 +++++++++++++++++++
1 file changed, 43 insertions(+), 42 deletions()
diff git a/src/referenceInterpreter.ml b/src/referenceInterpreter.ml
index 510eb878..b5c1b6e0 100644
 a/src/referenceInterpreter.ml
+++ b/src/referenceInterpreter.ml
@@ 108,64 +108,65 @@ module T = struct
 None >
let n = Production.length prod in
+
let values : semantic_value array =
Array.make n CstError (* dummy *)
 and startp : Lexing.position ref =
+ and startp =
ref Lexing.dummy_pos
 and endp : Lexing.position ref =
+ and endp=
ref Lexing.dummy_pos
+ and current =
+ ref env.current
+ and stack =
+ ref env.stack
in
 (* The auxiliary function [pop k stack] pops [k] stack cells
 and returns a truncated stack. It also updates the automaton's
 current state, and fills in [values], [startp], and [endp]. *)

 let rec pop k stack =
+ (* We now enter a loop to pop [k] stack cells and (after that) push
+ a new cell onto the stack. *)
 if k = 0 then
+ (* This loop does not update [env.current]. Instead, the state in
+ the newly pushed stack cell will be used (by our caller) as a
+ basis for a goto transition, and [env.current] will be updated
+ (if necessary) then. *)
 (* There are no more stack cells to pop. *)
+ for k = n downto 1 do
 stack
+ (* Fetch a semantic value. *)
 else begin
+ values.(k  1) < !stack.semv;
 (* Fetch a semantic value. *)
+ (* Pop one cell. The stack must be nonempty. As we pop a cell,
+ change the automaton's current state to the one stored within
+ the cell. (It is sufficient to do this only when [k] is 1,
+ since the last write overwrites any and all previous writes.)
+ If this is the first (last) cell that we pop, update [endp]
+ ([startp]). *)
 values.(k  1) < stack.semv;
+ let next = !stack.next in
+ assert (!stack != next);
+ if k = n then begin
+ endp := !stack.endp
+ end;
+ if k = 1 then begin
+ current := !stack.state;
+ startp := !stack.startp
+ end;
+ stack := next
 (* Pop one cell. The stack must be nonempty. As we pop a cell,
 change the automaton's current state to the one stored within
 the cell. (It is sufficient to do this only when [k] is 1.)
 If this is the first (last) cell that we pop, update [endp]
 ([startp]). *)
+ done;
 let next = stack.next in
 assert (stack != next);
 if k = n then begin
 endp := stack.endp
 end;
 if k = 1 then begin
 env.current < stack.state;
 startp := stack.startp
 end;
 pop (k  1) next
+ (* Done popping. *)
 end
+ (* Construct and push a new stack cell. The associated semantic
+ value is a new concrete syntax tree. *)
 in
 let stack = pop n env.stack in

 (* Construct and push a new stack cell. The associated semantic
 value is a new concrete syntax tree. *)

 {
 state = env.current;
 semv = CstNonTerminal (prod, values);
 startp = !startp;
 endp = !endp;
 next = stack
 }
+ {
+ state = !current;
+ semv = CstNonTerminal (prod, values);
+ startp = !startp;
+ endp = !endp;
+ next = !stack
+ }
module Log = struct

GitLab