blob: 2ac9da119d473fa1ad915797faa7d2da49302884 (
plain)
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
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: topconstr.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
(*i*)
open Pp
open Util
open Names
open Libnames
open Rawterm
open Term
open Mod_subst
(*i*)
(*s This is the subtype of rawconstr allowed in syntactic extensions *)
(* No location since intended to be substituted at any place of a text *)
(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
(* non global expressions such as existential variables also *)
type aconstr =
(* Part common to [rawconstr] and [cases_pattern] *)
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| AList of identifier * identifier * aconstr * aconstr * bool
(* Part only in [rawconstr] *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ARec of fix_kind * identifier array *
(name * aconstr option * aconstr) list array * aconstr array *
aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
(**********************************************************************)
(* Translate a rawconstr into a notation given the list of variables *)
(* bound by the notation; also interpret recursive patterns *)
val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
(* Name of the special identifier used to encode recursive notations *)
val ldots_var : identifier
(* Equality of rawconstr (warning: only partially implemented) *)
val eq_rawconstr : rawconstr -> rawconstr -> bool
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
val rawconstr_of_aconstr_with_binders : loc ->
('a -> identifier -> 'a * identifier) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
(**********************************************************************)
(* [match_aconstr metas] matches a rawconstr against an aconstr with *)
(* metavariables in [metas]; raise [No_match] if the matching fails *)
exception No_match
type scope_name = string
type tmp_scope_name = scope_name
type interpretation =
(identifier * (tmp_scope_name option * scope_name list)) list * aconstr
val match_aconstr : rawconstr -> interpretation ->
(rawconstr * (tmp_scope_name option * scope_name list)) list
(**********************************************************************)
(* Substitution of kernel names in interpretation data *)
val subst_interpretation : substitution -> interpretation -> interpretation
(**********************************************************************)
(*s Concrete syntax for terms *)
type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_expr list
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
and fixpoint_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr
(** Anonymous defs allowed ?? *)
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
(**********************************************************************)
(* Utilities on constr_expr *)
val constr_loc : constr_expr -> loc
val cases_pattern_expr_loc : cases_pattern_expr -> loc
val replace_vars_constr_expr :
(identifier * identifier) list -> constr_expr -> constr_expr
val free_vars_of_constr_expr : constr_expr -> Idset.t
val occur_var_constr_expr : identifier -> constr_expr -> bool
val default_binder_kind : binder_kind
(* Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : constr_expr -> identifier list
val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
val coerce_to_id : constr_expr -> identifier located
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
(* For binders parsing *)
(* Includes let binders *)
val local_binders_length : local_binder list -> int
(* Excludes let binders *)
val local_assums_length : local_binder list -> int
(* Does not take let binders into account *)
val names_of_local_assums : local_binder list -> name located list
(* With let binders *)
val names_of_local_binders : local_binder list -> name located list
(* Used in typeclasses *)
val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
(* Used in correctness and interface; absence of var capture not guaranteed *)
(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
val map_constr_expr_with_binders :
(identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
'a -> constr_expr -> constr_expr
(**********************************************************************)
(* Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
type module_type_ast =
| CMTEident of qualid located
| CMTEapply of module_type_ast * module_ast
| CMTEwith of module_type_ast * with_declaration_ast
type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
|
