Commit 69511635 authored by POTTIER Francois's avatar POTTIER Francois

Added comments to explain that [equal env1 env2] guarantees that

the checkpoints [input_needed env1] and [input_needed env2] are equivalent.
parent 6a3a94b4
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment