From 6951163544188b2211c08f83da6f31f42af4850f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?=
Date: Wed, 5 Apr 2017 15:33:07 +0200
Subject: [PATCH] Added comments to explain that [equal env1 env2] guarantees
that the checkpoints [input_needed env1] and [input_needed env2] are
equivalent.
---
src/Engine.ml | 6 ++++++
src/IncrementalEngine.ml | 12 +++++++-----
2 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/Engine.ml b/src/Engine.ml
index 988ddf7c..e37de2e1 100644
--- a/src/Engine.ml
+++ b/src/Engine.ml
@@ -714,6 +714,12 @@ module Make (T : TABLE) = struct
current states via their numbers (this seems cleaner than using OCaml's
polymorphic equality). *)
+ (* The two fields that are not compared by [equal], namely [error] and
+ [triple], are overwritten by the function [discard], which handles
+ [InputNeeded] checkpoints. Thus, if [equal env1 env2] holds, then the
+ checkpoints [input_needed env1] and [input_needed env2] are
+ equivalent: they lead the parser to behave in the same way. *)
+
let equal env1 env2 =
env1.stack == env2.stack &&
number env1.current = number env2.current
diff --git a/src/IncrementalEngine.ml b/src/IncrementalEngine.ml
index 78700c8c..d21d292a 100644
--- a/src/IncrementalEngine.ml
+++ b/src/IncrementalEngine.ml
@@ -290,11 +290,13 @@ module type INCREMENTAL_ENGINE = sig
val current_state_number: 'a env -> int
(* [equal env1 env2] tells whether the parser configurations [env1] and
- [env2] are equal in the sense that the automaton's current state is
- the same in [env1] and [env2] and the stack is *physically* the same
- in [env1] and [env2]. If [equal env1 env2] is [true], then the list
- of stack elements, as observed via [pop] and [top], must be the same
- in [env1] and [env2]. The function [equal] has time complexity O(1). *)
+ [env2] are equal in the sense that the automaton's current state is the
+ same in [env1] and [env2] and the stack is *physically* the same in
+ [env1] and [env2]. If [equal env1 env2] is [true], then the list of stack
+ elements, as observed via [pop] and [top], must be the same in [env1] and
+ [env2]. Also, if [equal env1 env2], then the checkpoints [input_needed
+ env1] and [input_needed env2] are equivalent. The function [equal] has
+ time complexity O(1). *)
val equal: 'a env -> 'a env -> bool
--
2.22.0