Module Extend
Entry keys for constr notations
type 'a entry= 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.etype side=|Left|Righttype production_position=|BorderProd of side * Gramlib.Gramext.g_assoc option|InternalProdtype production_level=|NextLevel|NumLevel of int
type 'a constr_entry_key_gen=|ETIdent|ETGlobal|ETBigint|ETBinder of bool|ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a|ETPattern of bool * int option
type constr_entry_key= (production_level * production_position) constr_entry_key_gen
type simple_constr_prod_entry_key= production_level option constr_entry_key_gen
type binder_entry_kind=|ETBinderOpen|ETBinderClosed of string Tok.p listtype binder_target=|ForBinder|ForTermtype constr_prod_entry_key=|ETProdName|ETProdReference|ETProdBigint|ETProdConstr of Constrexpr.notation_entry * production_level * production_position|ETProdPattern of int|ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * string Tok.p list|ETProdBinderList of binder_entry_kind
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 * inttype ('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
Type-safe grammar extension
type norec= Gramlib.Grammar.ty_norectype mayrec= Gramlib.Grammar.ty_mayrectype ('self, 'trec, 'a) symbol=|Atoken : 'c Tok.p -> ('self, norec, 'c) symbol|Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol|Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol -> ('self, 'trec, 'a list) symbol|Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol|Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol -> ('self, 'trec, 'a list) symbol|Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol|Aself : ('self, mayrec, 'self) symbol|Anext : ('self, mayrec, 'self) symbol|Aentry : 'a entry -> ('self, norec, 'a) symbol|Aentryl : 'a entry * string -> ('self, norec, 'a) symbol|Arules : 'a rules list -> ('self, norec, 'a) symboland ('self, 'trec, _, 'r) rule=|Stop : ('self, norec, 'r, 'r) rule|Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule|NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) ruleand 'a rules=|Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rulestype 'a production_rule=|Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule