-
Notifications
You must be signed in to change notification settings - Fork 632
/
evarutil.mli
266 lines (202 loc) · 9.8 KB
/
evarutil.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
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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 Constr
open Evd
open Environ
open Namegen
open EConstr
(** This module provides useful higher-level functions for evar manipulation. *)
(** {6 Metas} *)
(** [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> metavariable
(** {6 Creating a fresh evar given their type and context} *)
val next_evar_name : evar_map -> intro_pattern_naming_expr -> Id.t option
module VarSet :
sig
type t
val empty : t
val full : t
val variables : Environ.env -> t
end
type naming_mode =
| RenameExistingBut of VarSet.t
| FailIfConflict
| ProgramNaming of VarSet.t
val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?relevance:Sorts.relevance ->
?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
?typeclass_candidate:bool ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
(** Alias of {!Evd.new_pure_evar} *)
val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?relevance:Sorts.relevance ->
?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?name:Id.t ->
?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> rigid ->
evar_map * (constr * ESorts.t)
val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
(** {6 Unification utils} *)
(** [head_evar c] returns the head evar of [c] if any *)
exception NoHeadEvar
val head_evar : evar_map -> constr -> Evar.t (** may raise NoHeadEvar *)
(* Expand head evar if any *)
val whd_head_evar : evar_map -> constr -> constr
(* An over-approximation of [has_undefined (nf_evars evd c)] *)
val has_undefined_evars : evar_map -> constr -> bool
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially)
solved. *)
val advance : evar_map -> Evar.t -> Evar.t option
(** [reachable_from_evars sigma seeds] computes the descendents of
evars in [seeds] by restriction or evar-evar unifications in [sigma]. *)
val reachable_from_evars : evar_map -> Evar.Set.t -> Evar.Set.t
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
[nf_evar]. *)
val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t
type undefined_evars_cache
val create_undefined_evars_cache : unit -> undefined_evars_cache
val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> evar_map -> 'a evar_info -> Evar.Set.t
(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
[c]. It looks up recursively in [sigma] for the value of existential
variables. *)
val occur_evar_upto : evar_map -> Evar.t -> constr -> bool
(** {6 Value/Type constraints} *)
val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
(***********************************************************)
val create_clos_infos : env -> evar_map -> CClosure.RedFlags.reds -> CClosure.clos_infos
(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
val whd_evar : evar_map -> constr -> constr
val nf_evar : evar_map -> constr -> constr
val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment
val jl_nf_evar :
evar_map -> unsafe_judgment list -> unsafe_judgment list
val jv_nf_evar :
evar_map -> unsafe_judgment array -> unsafe_judgment array
val tj_nf_evar :
evar_map -> unsafe_type_judgment -> unsafe_type_judgment
val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context
val nf_rel_context_evar : evar_map -> rel_context -> rel_context
val nf_env_evar : evar_map -> env -> env
val nf_evar_info : evar_map -> 'a evar_info -> 'a evar_info
val nf_evar_map : evar_map -> evar_map
val nf_evar_map_undefined : evar_map -> evar_map
val nf_relevance : evar_map -> Sorts.relevance -> Sorts.relevance
(** Presenting terms without solved evars *)
val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
exception Uninstantiated_evar of Evar.t
val flush_and_check_evars : evar_map -> constr -> Constr.constr
(** [finalize env sigma f] combines universe minimisation,
evar-and-universe normalisation and universe restriction.
It minimizes universes in [sigma], calls [f] a normalisation
function with respect to the updated [sigma] and restricts the
local universes of [sigma] to those encountered while running [f].
Note that the normalizer passed to [f] holds some imperative state
in its closure. *)
val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
((EConstr.t -> Constr.t) -> 'a) ->
evar_map * 'a
(** {6 Term manipulation up to instantiation} *)
(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
value of [e] in [sigma] is (recursively) used. *)
val kind_of_term_upto : evar_map -> Constr.constr ->
(Constr.constr, Constr.types, Sorts.t, UVars.Instance.t) kind_of_term
(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
[t] and [u] up to existential variable instantiation and
equalisable universes. The term [t] is interpreted in [evd] while
[u] is interpreted in [extended_evd]. The universe constraints in
[extended_evd] are assumed to be an extension of those in [evd]. *)
val eq_constr_univs_test :
evd:Evd.evar_map ->
extended_evd:Evd.evar_map ->
constr ->
constr ->
bool
(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
[Inl sigma'] where [sigma'] is [sigma] augmented with universe
constraints such that [u1 cv_pb? u2] according to [variance].
Additionally flexible universes in irrelevant positions are unified
if possible. Returns [Inr p] when the former is impossible. *)
val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array ->
UVars.Instance.t -> UVars.Instance.t -> evar_map ->
(evar_map, UGraph.univ_inconsistency) Util.union
(** We should only compare constructors at convertible types, so this
is only an opportunity to unify universes.
But what about qualities?
*)
val compare_constructor_instances : evar_map ->
UVars.Instance.t -> UVars.Instance.t -> (evar_map, UGraph.univ_inconsistency) Util.union
(** {6 Unification problems} *)
type unification_pb = conv_pb * env * constr * constr
(** [add_unification_pb ?tail pb sigma]
Add a unification problem [pb] to [sigma], if not already present.
Put it at the end of the list if [tail] is true, by default it is false. *)
val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
(** {6 Removing hyps in evars'context}
raise OccurHypInSimpleClause if the removal breaks dependencies *)
type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of Constr.existential
| NoCandidatesLeft of Evar.t
exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
(** Restrict an undefined evar according to a (sub)filter and candidates.
The evar will be defined if there is only one candidate left,
@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates
into an empty list. *)
val restrict_evar : evar_map -> Evar.t -> Filter.t ->
?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types ->
Id.Set.t -> evar_map * named_context_val * types
val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types ->
Id.Set.t -> evar_map * named_context_val * types * types
val check_and_clear_in_constr
: Environ.env
-> Evd.evar_map
-> clear_dependency_error
-> Names.Id.Set.t
-> EConstr.constr
-> Evd.evar_map
type csubst
val empty_csubst : csubst
val csubst_subst : Evd.evar_map -> csubst -> constr -> constr
type ext_named_context =
csubst * Id.Set.t * named_context_val
val default_ext_instance : ext_named_context -> constr SList.t
val push_rel_decl_to_named_context : hypnaming:naming_mode ->
evar_map -> rel_declaration -> ext_named_context -> ext_named_context
val push_rel_context_to_named_context : hypnaming:naming_mode ->
Environ.env -> evar_map -> types ->
named_context_val * types * constr SList.t * csubst
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
val meta_counter_summary_tag : int Summary.Dyn.tag