Introducing an intermediary type "constr_prod_entry_key" for grammar productions.

This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.

The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.

Also exporting less of extend.mli in API.

4 files changed, 44 insertions, 36 deletions

diff --git a/intf/extend.ml b/intf/extend.ml
index e4d014a09..79bbbd376 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -29,32 +29,41 @@ type production_level =
   | NextLevel
   | NumLevel of int
 
-type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list
+(** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type ('lev,'pos) constr_entry_key_gen =
-  | ETName | ETReference | ETBigint
-  | ETBinder of bool
+  | ETName
+  | ETReference
+  | ETBigint
+  | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
-  | ETConstrList of ('lev * 'pos) * Tok.t list
-  | ETBinderList of binder_entry_kind
 
 (** Entries level (left-hand-side of grammar rules) *)
 
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
 
-(** Entries used in productions (in right-hand-side of grammar rules) *)
-
-type constr_prod_entry_key =
-    (production_level,production_position) constr_entry_key_gen
-
 (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen
 
+(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
+
+type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list
+
+type constr_prod_entry_key =
+  | ETProdName            (* Parsed as a name (ident or _) *)
+  | ETProdReference       (* Parsed as a global reference *)
+  | ETProdBigint          (* Parsed as an (unbounded) integer *)
+  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdPattern                  (* Parsed as pattern (as subpart of a constr) *)
+  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
+  | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
+  | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
+
 (** {5 AST for user-provided entries} *)
 
 type 'a user_symbol =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 16124c26c..3c4f408f8 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -229,7 +229,6 @@ type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -292,23 +291,20 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
-| TTBinder -> Aentry Constr.binder
 | TTOpenBinderList -> Aentry Constr.open_binders
 | TTBigint -> Aentry Prim.bigint
 | TTReference -> Aentry Constr.global
 
 let interp_entry forpat e = match e with
-| ETName -> TTAny TTName
-| ETReference -> TTAny TTReference
-| ETBigint -> TTAny TTBigint
-| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.")
-| ETBinder false  -> TTAny TTBinder
-| ETConstr p -> TTAny (TTConstr (p, forpat))
-| ETPattern -> assert false (** not used *)
-| ETOther _ -> assert false (** not used *)
-| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList
-| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
+| ETProdName -> TTAny TTName
+| ETProdReference -> TTAny TTReference
+| ETProdBigint -> TTAny TTBigint
+| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdPattern -> assert false (** not used *)
+| ETProdOther _ -> assert false (** not used *)
+| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
+| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
 let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
@@ -334,7 +330,6 @@ match e with
   | ForConstr -> push_constr subst (constr_expr_of_name v)
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTBinder -> { subst with binders = (v, true) :: subst.binders }
 | TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders }
 | TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 950246c53..a7e73c91f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -102,7 +102,6 @@ open Decl_kinds
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
-    | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index bb4db1322..09eb0503d 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -574,8 +574,8 @@ let hunks_of_format (from,(vars,typs)) symfmt =
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
 let is_not_small_constr = function
-    ETConstr _ -> true
-  | ETOther("constr","binder_constr") -> true
+    ETProdConstr _ -> true
+  | ETProdOther("constr","binder_constr") -> true
   | _ -> false
 
 let rec define_keywords_aux = function
@@ -607,14 +607,14 @@ let distribute a ll = List.map (fun l -> a @ l) ll
 
 let expand_list_rule typ tkl x n p ll =
   let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in
-  let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in
+  let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in
   let tks = List.map (fun x -> GramConstrTerminal x) tkl in
   let rec aux i hds ll =
   if i < p then aux (i+1) (main :: tks @ hds) ll
   else if Int.equal i (p+n) then
     let hds =
       GramConstrListMark (p+n,true,p) :: hds
-      @	[GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
+      @	[GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in
     distribute hds ll
   else
     distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @
@@ -636,12 +636,21 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
     with Exit -> n,l in
   try_aux 0 l
 
+let prod_entry_type = function
+  | ETName -> ETProdName
+  | ETReference -> ETProdReference
+  | ETBigint -> ETProdBigint
+  | ETBinder _ -> assert false (* See check_binder_type *)
+  | ETConstr p -> ETProdConstr p
+  | ETPattern -> ETProdPattern
+  | ETOther (s,t) -> ETProdOther (s,t)
+
 let make_production etyps symbols =
   let rec aux = function
     | [] -> [[]]
     | NonTerminal m :: l ->
         let typ = List.assoc m etyps in
-        distribute [GramConstrNonTerminal (typ, Some m)] (aux l)
+        distribute [GramConstrNonTerminal (prod_entry_type typ, Some m)] (aux l)
     | Terminal s :: l ->
         distribute [GramConstrTerminal (CLexer.terminal s)] (aux l)
     | Break _ :: l ->
@@ -658,8 +667,8 @@ let make_production etyps symbols =
         | ETBinder o ->
             check_open_binder o sl x;
             let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in
-	    distribute
-              [GramConstrNonTerminal (ETBinderList typ, Some x)] (aux l)
+            distribute
+              [GramConstrNonTerminal (ETProdBinderList typ, Some x)] (aux l)
         | _ ->
            user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in
   let prods = aux symbols in
@@ -909,7 +918,6 @@ let set_entry_type etyps (x,typ) =
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
       | (ETPattern | ETName | ETBigint | ETOther _ |
 	 ETReference | ETBinder _ as t), _ -> t
-      | (ETBinderList _ |ETConstrList _), _ -> assert false
     with Not_found -> ETConstr typ
   in (x,typ)
 
@@ -934,7 +942,6 @@ let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeBinder
   | ETName -> NtnInternTypeIdent
   | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.")
-  | ETBinderList _ | ETConstrList _ -> assert false
 
 let set_internalization_type typs =
   List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -1039,8 +1046,6 @@ let find_precedence lev etyps symbols onlyprint =
 	    if Option.is_empty lev then
 	      user_err Pp.(str "Need an explicit level.")
 	    else [],Option.get lev
-        | ETConstrList _ | ETBinderList _ ->
-	    assert false (* internally used in grammar only *)
       with Not_found ->
 	if Option.is_empty lev then
 	  user_err Pp.(str "A left-recursive notation must have an explicit level.")