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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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) *)
(************************************************************************)
open Names
open Libnames
(** {6 Concrete syntax for terms } *)
(** Universes *)
type sort_name_expr =
| CSProp | CProp | CSet
| CType of qualid
| CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *)
type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen
type qvar_expr =
| CQVar of qualid
| CQAnon of Loc.t option
| CRawQVar of Sorts.QVar.t
type quality_expr =
| CQConstant of Sorts.Quality.constant
| CQualVar of qvar_expr
type relevance_expr =
| CRelevant | CIrrelevant
| CRelevanceVar of qvar_expr
type relevance_info_expr = relevance_expr option
type sort_expr = (qvar_expr option * (sort_name_expr * int) list Glob_term.glob_sort_gen)
type instance_expr = quality_expr list * univ_level_expr list
(** Constraints don't have anonymous universes *)
type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr
type universe_decl_expr = (lident list, lident list, univ_constraint_expr list) UState.gen_universe_decl
type cumul_univ_decl_expr =
(lident list, (lident * UVars.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
type ident_decl = lident * universe_decl_expr option
type cumul_ident_decl = lident * cumul_univ_decl_expr option
type name_decl = lname * universe_decl_expr option
type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
type side = Left | Right
type entry_level = int
type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
(* The entry in which a notation is declared *)
type notation_entry = InConstrEntry | InCustomEntry of string
(* A notation entry with the level where the notation lives *)
type notation_entry_level = {
notation_entry : notation_entry;
notation_level : entry_level;
}
(* Notation subentries, to be associated to the variables of the notation *)
type notation_entry_relative_level = {
notation_subentry : notation_entry;
notation_relative_level : entry_relative_level;
notation_position : side option;
}
type notation_key = string
(* A notation associated to a given parsing rule *)
type notation = notation_entry * notation_key
(* A notation associated to a given interpretation *)
type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
type 'a or_by_notation_r =
| AN of 'a
| ByNotation of (string * string option)
type 'a or_by_notation = 'a or_by_notation_r CAst.t
(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
but this formulation avoids a useless dependency. *)
type explicitation =
| ExplByName of Id.t
| ExplByPos of int (* a reference to the n-th non-dependent implicit starting from left *)
type binder_kind =
| Default of Glob_term.binding_kind
| Generalized of Glob_term.binding_kind * bool
(** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type explicit_flag = bool (** true = with "@" *)
type delimiter_depth = DelimOnlyTmpScope | DelimUnboundedScope
(** shallow (%_) vs. deep (%) scope opening *)
type prim_token =
| Number of NumTok.Signed.t
| String of string
(** [constr_expr] is the abstract syntax tree produced by the parser *)
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * lname
| CPatCstr of qualid
* cases_pattern_expr list option * cases_pattern_expr list
(** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
| CPatAtom of qualid option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
| CPatPrim of prim_token
| CPatRecord of (qualid * cases_pattern_expr) list
| CPatDelimiters of delimiter_depth * string * cases_pattern_expr
| CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
and cases_pattern_notation_substitution =
cases_pattern_expr list * (* for cases_pattern subterms parsed as terms *)
cases_pattern_expr list list * (* for recursive notations parsed as terms*)
kinded_cases_pattern_expr list (* for cases_pattern subterms parsed as binders *)
and constr_expr_r =
| CRef of qualid * instance_expr option
| CFix of lident * fix_expr list
| CCoFix of lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of lname * constr_expr * constr_expr option * constr_expr
| CAppExpl of (qualid * instance_expr option) * constr_expr list
| CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
| CProj of explicit_flag * (qualid * instance_expr option)
* (constr_expr * explicitation CAst.t option) list * constr_expr
| CRecord of (qualid * constr_expr) list
(* representation of the "let" and "match" constructs *)
| CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *)
* constr_expr option (* return-clause *)
* case_expr list
* branch_expr list (* branches *)
| CLetTuple of lname list * (lname option * constr_expr option) *
constr_expr * constr_expr
| CIf of constr_expr * (lname option * constr_expr option)
* constr_expr * constr_expr
| CHole of Evar_kinds.glob_evar_kind option
| CGenarg of Genarg.raw_generic_argument
(* because print for genargs wants to print directly the glob without an extern phase (??) *)
| CGenargGlob of Genarg.glob_generic_argument
| CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list
| CSort of sort_expr
| CCast of constr_expr * Constr.cast_kind option * constr_expr
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * constr_expr
| CPrim of prim_token
| CDelimiters of delimiter_depth * string * constr_expr
| CArray of instance_expr option * constr_expr array * constr_expr * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
* lname option (* as-clause *)
* cases_pattern_expr option (* in-clause *)
and branch_expr =
(cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr =
lident * relevance_info_expr
* fixpoint_order_expr option *
local_binder_expr list * constr_expr * constr_expr
and cofix_expr =
lident * relevance_info_expr * local_binder_expr list * constr_expr * constr_expr
and fixpoint_order_expr_r =
| CStructRec of lident
| CWfRec of lident * constr_expr
| CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
and fixpoint_order_expr = fixpoint_order_expr_r CAst.t
(* Anonymous defs allowed ?? *)
and local_binder_expr =
| CLocalAssum of lname list * relevance_info_expr * binder_kind * constr_expr
| CLocalDef of lname * relevance_info_expr * constr_expr * constr_expr option
| CLocalPattern of cases_pattern_expr
and constr_notation_substitution =
constr_expr list * (* for constr subterms *)
constr_expr list list * (* for recursive notations *)
kinded_cases_pattern_expr list * (* for binders *)
local_binder_expr list list (* for binder lists (recursive notations) *)
type constr_pattern_expr = constr_expr
(** Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of Id.t list CAst.t * qualid
| CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
| CMident of qualid
| CMapply of module_ast * qualid
| CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t
|
