Merge branch 'master' of gitlab.inria.fr:fpottier/menhir

TODO

@@ -27,6 +27,13 @@
   - Change of LICENSE. Clarify the status of test/.
   - Send CompCert pull request.
 
+* The table back-end should not use Invariant.prodstack,
+  and should produce code for all semantic actions, regardless
+  of whether they are ever reduced.
+
+* The table back-end should not use Invariant at all?
+  And we should be able to save time by not running Invariant.
+
 * Move more of ErrorReports from CompCert to MenhirLib.
   In [show], might want to apply [shorten] to the output of [f].
 

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

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
 

src/tableBackend.ml

@@ -143,7 +143,7 @@ let define_and_measure (x, e) =
 
 (* Code generation for semantic actions. *)
 
-(* The functions [reducecellparams] and [reducebody] are adpated from
+(* The functions [reducecellparams] and [reducebody] are adapted from
    [CodeBackend]. *)
 
 (* Things are slightly more regular here than in the code-based