From 5d0c54e370ac20e9fbf249c3a7f1851a65e42acf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Aug 2020 14:57:55 +0200
Subject: Moving production_level_eq to extend.ml for separation of concerns.

Add a mli file and uniformize indentation on the way.
---
 parsing/extend.mli | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 parsing/extend.mli

(limited to 'parsing/extend.mli')

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
-- 
cgit v1.2.3