/
evd.mli
381 lines (289 loc) · 15 KB
/
evd.mli
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
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
(************************************************************************)
(* 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 Sign
open Environ
open Libnames
open Mod_subst
open Termops
(********************************************************************
Meta map *)
module Metamap : Map.S with type key = metavariable
module Metaset : Set.S with type elt = metavariable
val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
type 'a freelisted = {
rebus : 'a;
freemetas : Metaset.t }
val metavars_of : constr -> Metaset.t
val mk_freelisted : constr -> constr freelisted
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
(** Status of an instance found by unification wrt to the meta it solves:
- a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
- a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
- a term that can be eta-expanded n times while still being a solution
(e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
*)
type instance_constraint = IsSuperType | IsSubType | Conv
val eq_instance_constraint :
instance_constraint -> instance_constraint -> bool
(** Status of the unification of the type of an instance against the type of
the meta it instantiates:
- CoerceToType means that the unification of types has not been done
and that a coercion can still be inserted: the meta should not be
substituted freely (this happens for instance given via the
"with" binding clause).
- TypeProcessed means that the information obtainable from the
unification of types has been extracted.
- TypeNotProcessed means that the unification of types has not been
done but it is known that no coercion may be inserted: the meta
can be substituted freely.
*)
type instance_typing_status =
CoerceToType | TypeNotProcessed | TypeProcessed
(** Status of an instance together with the status of its type unification *)
type instance_status = instance_constraint * instance_typing_status
(** Clausal environments *)
type clbinding =
| Cltyp of Name.t * constr freelisted
| Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
val map_clb : (constr -> constr) -> clbinding -> clbinding
(********************************************************************
** Existential variables and unification states ***)
(** A unification state (of type [evar_map]) is primarily a finite mapping
from existential variables to records containing the type of the evar
([evar_concl]), the context under which it was introduced ([evar_hyps])
and its definition ([evar_body]). [evar_extra] is used to add any other
kind of information.
It also contains conversion constraints, debugging information and
information about meta variables. *)
(** Information about existential variables. *)
type evar = existential_key
val string_of_existential : evar -> string
val existential_of_int : int -> evar
type evar_body =
| Evar_empty
| Evar_defined of constr
module Store : Store.S
type evar_info = {
evar_concl : constr;
evar_hyps : named_context_val;
evar_body : evar_body;
evar_filter : bool list;
evar_source : Evar_kinds.t located;
evar_candidates : constr list option;
evar_extra : Store.t }
val eq_evar_info : evar_info -> evar_info -> bool
val make_evar : named_context_val -> types -> evar_info
val evar_concl : evar_info -> constr
val evar_context : evar_info -> named_context
val evar_filtered_context : evar_info -> named_context
val evar_hyps : evar_info -> named_context_val
val evar_filtered_hyps : evar_info -> named_context_val
val evar_body : evar_info -> evar_body
val evar_filter : evar_info -> bool list
val evar_env : evar_info -> env
val evar_filtered_env : evar_info -> env
val map_evar_body : (constr -> constr) -> evar_body -> evar_body
val map_evar_info : (constr -> constr) -> evar_info -> evar_info
(*** Unification state ***)
type evar_map
(** Unification state and existential variables *)
(** Assuming that the second map extends the first one, this says if
some existing evar has been refined *)
val progress_evar_map : evar_map -> evar_map -> bool
val empty : evar_map
val from_env : ?ctx:Univ.universe_context_set -> env -> evar_map
val is_empty : evar_map -> bool
(** [has_undefined sigma] is [true] if and only if
there are uninstantiated evars in [sigma]. *)
val has_undefined : evar_map -> bool
(** [add sigma ev info] adds [ev] with evar info [info] in sigma.
Precondition: ev must not preexist in [sigma]. *)
val add : evar_map -> evar -> evar_info -> evar_map
val find : evar_map -> evar -> evar_info
val find_undefined : evar_map -> evar -> evar_info
val remove : evar_map -> evar -> evar_map
val mem : evar_map -> evar -> bool
val undefined_list : evar_map -> (evar * evar_info) list
val to_list : evar_map -> (evar * evar_info) list
val map : (evar_info -> evar_info) -> evar_map -> evar_map
val map_undefined : (evar_info -> evar_info) -> evar_map -> evar_map
val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
val merge : evar_map -> evar_map -> evar_map
val define : evar -> constr -> evar_map -> evar_map
val cmap : (constr -> constr) -> evar_map -> evar_map
val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
val is_undefined : evar_map -> evar -> bool
val add_constraints : evar_map -> Univ.constraints -> evar_map
val add_universe_constraints : evar_map -> Univ.universe_constraints -> evar_map
(** {6 ... } *)
(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
no body and [Not_found] if it does not exist in [sigma] *)
exception NotInstantiatedEvar
val existential_value : evar_map -> existential -> constr
val existential_type : evar_map -> existential -> types
val existential_opt_value : evar_map -> existential -> constr option
val instantiate_evar : named_context -> constr -> constr list -> constr
(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
val subst_evar_defs_light : substitution -> evar_map -> evar_map
(** spiwack: this function seems to somewhat break the abstraction. *)
val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map
(* spiwack: [is_undefined_evar] should be considered a candidate
for moving to evarutils *)
val is_undefined_evar : evar_map -> constr -> bool
val undefined_evars : evar_map -> evar_map
val defined_evars : evar_map -> evar_map
(* [fold_undefined f m] iterates ("folds") function [f] over the undefined
evars (that is, whose value is [Evar_empty]) of map [m].
It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
val evar_declare :
named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
val evar_source : existential_key -> evar_map -> Evar_kinds.t located
(* spiwack: this function seems to somewhat break the abstraction.
[evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
val evar_merge : evar_map -> evar_map -> evar_map
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
val add_conv_pb : evar_constraint -> evar_map -> evar_map
module ExistentialMap : Map.S with type key = existential_key
module ExistentialSet : Set.S with type elt = existential_key
val extract_changed_conv_pbs : evar_map ->
(ExistentialSet.t -> evar_constraint -> bool) ->
evar_map * evar_constraint list
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
val evar_list : evar_map -> constr -> existential list
val collect_evars : constr -> ExistentialSet.t
(** Metas *)
val find_meta : evar_map -> metavariable -> clbinding
val meta_list : evar_map -> (metavariable * clbinding) list
val meta_defined : evar_map -> metavariable -> bool
(** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
meta has no value *)
val meta_value : evar_map -> metavariable -> constr
val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status
val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
val meta_type : evar_map -> metavariable -> types
val meta_ftype : evar_map -> metavariable -> types freelisted
val meta_name : evar_map -> metavariable -> Name.t
val meta_with_name : evar_map -> Id.t -> metavariable
val meta_declare :
metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map
val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map
(** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
val meta_merge : evar_map -> evar_map -> evar_map
val undefined_metas : evar_map -> metavariable list
val metas_of : evar_map -> meta_type_map
val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
type metabinding = metavariable * constr * instance_status
val retract_coercible_metas : evar_map -> metabinding list * evar_map
val subst_defined_metas : metabinding list -> constr -> constr option
(*********************************************************
Sort/universe variables *)
(** Rigid or flexible universe variables *)
type rigid =
| UnivRigid
| UnivFlexible of bool (** Is substitution by an algebraic ok? *)
val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
(** The universe context associated to an evar map *)
type evar_universe_context
type 'a in_evar_universe_context = 'a * evar_universe_context
val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
val evar_context_universe_context : evar_universe_context -> Univ.universe_context
val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
val empty_evar_universe_context : evar_universe_context
val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
evar_universe_context
val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
val add_constraints_context : evar_universe_context ->
Univ.constraints -> evar_universe_context
val normalize_evar_universe_context_variables : evar_universe_context ->
Univ.universe_subst in_evar_universe_context
val normalize_evar_universe_context : evar_universe_context ->
evar_universe_context
val new_univ_variable : rigid -> evar_map -> evar_map * Univ.universe
val new_sort_variable : rigid -> evar_map -> evar_map * sorts
val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option
(** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is
not a sort variable declared in [evm] *)
val whd_sort_variable : evar_map -> constr -> constr
(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
val normalize_universe : evar_map -> Univ.universe -> Univ.universe
val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
val set_eq_instances : evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
val evar_universe_context : evar_map -> evar_universe_context
val get_universe_context_set : evar_map -> Univ.universe_context_set
val universe_context : evar_map -> Univ.universe_context
val universe_subst : evar_map -> Universes.universe_opt_subst
val merge_universe_context : evar_map -> evar_universe_context -> evar_map
val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
val abstract_undefined_variables : evar_map -> evar_map
val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
val nf_constraints : evar_map -> evar_map
(** Polymorphic universes *)
val fresh_sort_in_family : env -> evar_map -> sorts_family -> evar_map * sorts
val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant
val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
val fresh_global : rigid -> env -> evar_map -> Globnames.global_reference -> evar_map * constr
(********************************************************************
Conversion w.r.t. an evar map: might generate universe unifications
that are kept in the evarmap.
Raises [NotConvertible]. *)
val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
(** This one forgets about the assignemts of universes. *)
val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
val e_test_conversion : env -> evar_map ref -> conv_pb -> constr -> constr -> bool
(********************************************************************
constr with holes *)
type open_constr = evar_map * constr
(********************************************************************
The type constructor ['a sigma] adds an evar map to an object of
type ['a] *)
type 'a sigma = {
it : 'a ;
sigma : evar_map}
val sig_it : 'a sigma -> 'a
val sig_sig : 'a sigma -> evar_map
(*********************************************************
Failure explanation *)
type unsolvability_explanation = SeveralInstancesFound of int
(********************************************************************
debug pretty-printer: *)
val pr_evar_info : evar_info -> Pp.std_ppcmds
val pr_evar_map_constraints : evar_map -> Pp.std_ppcmds
val pr_evar_map : int option -> evar_map -> Pp.std_ppcmds
val pr_metaset : Metaset.t -> Pp.std_ppcmds
val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
(*** /!\Deprecated /!\ **
create an [evar_map] with empty meta map: *)
val create_evar_defs : evar_map -> evar_map
val create_goal_evar_defs : evar_map -> evar_map
val is_defined_evar : evar_map -> existential -> bool
val subst_evar_map : substitution -> evar_map -> evar_map
(*** /Deprecaded ***)