1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 'a entry = 'a Grammar.GMake(CLexer).Entry.e
type side = Left | Right
type gram_assoc = NonA | RightA | LeftA
type gram_position =
| First
| Last
| Before of string
| After of string
| Level of string
type production_position =
| BorderProd of side * gram_assoc option
| InternalProd
type production_level =
| NextLevel
| NumLevel of int
type constr_as_binder_kind =
| AsIdent
| AsIdentOrPattern
| AsStrictPattern
(** User-level types used to tell how to parse or interpret of the non-terminal *)
type 'a constr_entry_key_gen =
| ETName
| ETReference
| ETBigint
| ETBinder of bool (* open list of binders if true, closed list of binders otherwise *)
| ETConstr of 'a
| ETConstrAsBinder of constr_as_binder_kind * 'a
| ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
| ETOther of string * string
(** 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 option 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 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 (production_level * production_position) (* Parsed as constr or pattern *)
| ETProdPattern of int (* Parsed as pattern as a binder (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 =
| 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
(** {5 Type-safe grammar extension} *)
type ('self, 'a) symbol =
| Atoken : Tok.t -> ('self, string) symbol
| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
| Aself : ('self, 'self) symbol
| Anext : ('self, 'self) symbol
| Aentry : 'a entry -> ('self, 'a) symbol
| Aentryl : 'a entry * int -> ('self, 'a) symbol
| Arules : 'a rules list -> ('self, 'a) symbol
and ('self, _, 'r) rule =
| Stop : ('self, 'r, 'r) rule
| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule }
and 'a rules =
| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
type 'a production_rule =
| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
type 'a single_extend_statment =
string option *
(** Level *)
gram_assoc option *
(** Associativity *)
'a production_rule list
(** Symbol list with the interpretation function *)
type 'a extend_statment =
gram_position option *
'a single_extend_statment list
|
