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
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Loc
open Pp
open Names
open Term
open Libnames
open Globnames
open Glob_term
open Genredexpr
open Pattern
open Constrexpr
open Term
open Evd
open Misctypes
(** FIXME: nothing to do there. *)
val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
in the environment by the effective calls to Intro, Inversion, etc
The [constr_expr] field is [None] in TacDef though *)
type glob_constr_and_expr = glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
type open_glob_constr = unit * glob_constr_and_expr
type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
(** The route of a generic argument, from parsing to evaluation.
In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
{% \begin{%}verbatim{% }%}
parsing in_raw out_raw
char stream ---> raw_object ---> raw_object generic_argument -------+
encapsulation decaps|
|
V
raw_object
|
globalization |
V
glob_object
|
encaps |
in_glob |
V
glob_object generic_argument
|
out in out_glob |
object <--- object generic_argument <--- object <--- glob_object <---+
| decaps encaps interp decaps
|
V
effective use
{% \end{%}verbatim{% }%}
To distinguish between the uninterpreted (raw), globalized and
interpreted worlds, we annotate the type [generic_argument] by a
phantom argument which is either [constr_expr], [glob_constr] or
[constr].
Transformation for each type :
{% \begin{%}verbatim{% }%}
tag raw open type cooked closed type
BoolArgType bool bool
IntArgType int int
IntOrVarArgType int or_var int
StringArgType string (parsed w/ "") string
PreIdentArgType string (parsed w/o "") (vernac only)
IdentArgType true identifier identifier
IdentArgType false identifier (pattern_ident) identifier
IntroPatternArgType intro_pattern_expr intro_pattern_expr
VarArgType identifier located identifier
RefArgType reference global_reference
QuantHypArgType quantified_hypothesis quantified_hypothesis
ConstrArgType constr_expr constr
ConstrMayEvalArgType constr_expr may_eval constr
OpenConstrArgType open_constr_expr open_constr
ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings
BindingsArgType constr_expr bindings constr bindings
List0ArgType of argument_type
List1ArgType of argument_type
OptArgType of argument_type
ExtraArgType of string '_a '_b
{% \end{%}verbatim{% }%}
*)
(** {5 Generic types} *)
type ('raw, 'glob, 'top) genarg_type
(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
one, and ['top] the internalized one. *)
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision when the three types agree. *)
val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
(** Create a new generic type of argument: force to associate
unique ML types at each of the three levels. *)
(** {5 Specialized types} *)
(** All of [rlevel], [glevel] and [tlevel] must be non convertible
to ensure the injectivity of the type inference from type
['co generic_argument] to [('a,'co) abstract_argument_type];
this guarantees that, for 'co fixed, the type of
out_gen is monomorphic over 'a, hence type-safe
*)
type rlevel
type glevel
type tlevel
type ('a, 'co) abstract_argument_type
(** Type at level ['co] represented by an OCaml value of type ['a]. *)
type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
(** Specialized type at raw level. *)
type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type
(** Specialized type at globalized level. *)
type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type
(** Specialized type at internalized level. *)
(** {6 Projections} *)
val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
(** Projection on the raw type constructor. *)
val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
(** Projection on the globalized type constructor. *)
val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
(** Projection on the internalized type constructor. *)
(** {5 Generic arguments} *)
type 'a generic_argument
(** A inhabitant of ['level generic_argument] is a inhabitant of some type at
level ['level], together with the representation of this type. *)
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
(** {6 Constructors} *)
val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument
(** [in_gen t x] embeds an argument of type [t] into a generic argument. *)
val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a
(** [out_gen t x] recovers an argument of type [t] from a generic argument. It
fails if [x] has not the right dynamic type. *)
val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
[out_gen t v] will not raise a dynamic type exception. *)
(** {6 Manipulation of generic arguments}
Those functions fail if they are applied to an argument which has not the right
dynamic type. *)
val fold_list0 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_list1 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_opt :
('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
val fold_pair :
('a generic_argument -> 'a generic_argument -> 'c) ->
'a generic_argument -> 'c
(** [app_list0] fails if applied to an argument not of tag [List0 t]
for some [t]; it's the responsability of the caller to ensure it *)
val app_list0 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_list1 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_opt : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_pair :
('a generic_argument -> 'b generic_argument) ->
('a generic_argument -> 'b generic_argument)
-> 'a generic_argument -> 'b generic_argument
(** {6 Type reification} *)
type argument_type =
(** Basic types *)
| BoolArgType
| IntArgType
| IntOrVarArgType
| StringArgType
| PreIdentArgType
| IntroPatternArgType
| IdentArgType of bool
| VarArgType
| RefArgType
(** Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
| OpenConstrArgType of bool
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
| List0ArgType of argument_type
| List1ArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type
| ExtraArgType of string
val argument_type_eq : argument_type -> argument_type -> bool
val genarg_tag : 'a generic_argument -> argument_type
val unquote : ('a, 'co) abstract_argument_type -> argument_type
(** {5 Basic generic type constructors} *)
(** {6 Ground types} *)
val wit_bool : bool uniform_genarg_type
val wit_int : int uniform_genarg_type
val wit_int_or_var : int or_var uniform_genarg_type
val wit_string : string uniform_genarg_type
val wit_pre_ident : string uniform_genarg_type
val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
val wit_ident : Id.t uniform_genarg_type
val wit_pattern_ident : Id.t uniform_genarg_type
val wit_ident_gen : bool -> Id.t uniform_genarg_type
val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
val wit_constr_may_eval :
((constr_expr,reference or_by_notation,constr_expr) may_eval,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
constr) genarg_type
val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
constr with_bindings sigma) genarg_type
val wit_bindings :
(constr_expr bindings,
glob_constr_and_expr bindings,
constr bindings sigma) genarg_type
val wit_red_expr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
(** {6 Parameterized types} *)
val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
(** {5 Magic used by the parser} *)
(** [in_generic] is used in combination with camlp4 [Gramext.action] magic
[in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
where |a|_l is the interpretation of a at level l
[in_generic] is not typable; we replace the second argument by an absurd
type (with no introduction rule)
*)
type an_arg_of_this_type
val in_generic :
argument_type -> an_arg_of_this_type -> 'co generic_argument
val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
|