diff options
Diffstat (limited to 'parsing/extend.mli')
| -rw-r--r-- | parsing/extend.mli | 79 |
1 files changed, 79 insertions, 0 deletions
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 |