Moving production_level_eq to extend.ml for separation of concerns.

Add a mli file and uniformize indentation on the way.

3 files changed, 100 insertions, 21 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index fadfb6c5f4..a6fa6edad5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -21,6 +21,13 @@ type production_level =
   | NumLevel of int
   | DefaultLevel (** Interpreted differently at the border or inside a rule *)
 
+let production_level_eq lev1 lev2 =
+  match lev1, lev2 with
+  | NextLevel, NextLevel -> true
+  | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+  | DefaultLevel, DefaultLevel -> true
+  | (NextLevel | NumLevel _| DefaultLevel), _ -> false
+
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
@@ -59,19 +66,19 @@ type constr_prod_entry_key =
 (** {5 AST for user-provided entries} *)
 
 type 'a user_symbol =
-| Ulist1 of 'a user_symbol
-| Ulist1sep of 'a user_symbol * string
-| Ulist0 of 'a user_symbol
-| Ulist0sep of 'a user_symbol * string
-| Uopt of 'a user_symbol
-| Uentry of 'a
-| Uentryl of 'a * int
+  | Ulist1 of 'a user_symbol
+  | Ulist1sep of 'a user_symbol * string
+  | Ulist0 of 'a user_symbol
+  | Ulist0sep of 'a user_symbol * string
+  | Uopt of 'a user_symbol
+  | Uentry of 'a
+  | Uentryl of 'a * int
 
 type ('a,'b,'c) ty_user_symbol =
-| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
-| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
-| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
-| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
-| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
+  | TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+  | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+  | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
diff --git a/parsing/extend.mli b/parsing/extend.mli
new file mode 100644
index 0000000000..057fdb3841
--- /dev/null
+++ b/parsing/extend.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Entry keys for constr notations *)
+
+type side = Left | Right
+
+type production_position =
+  | BorderProd of side * Gramlib.Gramext.g_assoc option
+  | InternalProd
+
+type production_level =
+  | NextLevel
+  | NumLevel of int
+  | DefaultLevel (** Interpreted differently at the border or inside a rule *)
+
+val production_level_eq : production_level -> production_level -> bool
+
+(** User-level types used to tell how to parse or interpret of the non-terminal *)
+
+type 'a constr_entry_key_gen =
+  | ETIdent
+  | ETGlobal
+  | ETBigint
+  | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
+  | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
+
+(** Entries level (left-hand side of grammar rules) *)
+
+type constr_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 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 string Tok.p list
+
+type binder_target = ForBinder | ForTerm
+
+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 Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
+  | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
+  | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
+  | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
+
+(** {5 AST for user-provided entries} *)
+
+type 'a user_symbol =
+  | Ulist1 of 'a user_symbol
+  | Ulist1sep of 'a user_symbol * string
+  | Ulist0 of 'a user_symbol
+  | Ulist0sep of 'a user_symbol * string
+  | Uopt of 'a user_symbol
+  | Uentry of 'a
+  | Uentryl of 'a * int
+
+type ('a,'b,'c) ty_user_symbol =
+  | TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+  | TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+  | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+  | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+  | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c9a03087e1..0bdcd53c92 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -665,13 +665,6 @@ let expand_list_rule s typ tkl x n p ll =
        aux (i+1) (main :: tks @ hds) ll in
   aux 0 [] ll
 
-let production_level_eq lev1 lev2 =
-  match lev1, lev2 with
-  | NextLevel, NextLevel -> true
-  | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-  | DefaultLevel, DefaultLevel -> true
-  | (NextLevel | NumLevel _| DefaultLevel), _ -> false
-
 let is_constr_typ (s,lev) x etyps =
   match List.assoc x etyps with
   (* TODO: factorize these rules with the ones computing the effective