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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Context
open Evd
open Environ
(** {5 This modules provides useful functions for unification modulo evars } *)
(** {6 Metas} *)
(** [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> metavariable
val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
val new_evar :
env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> (constr, 'r) Sigma.sigma
val new_pure_evar :
named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> evar_map * evar
val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
(** the same with side-effects *)
val e_new_evar :
env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> types -> constr
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
evar_map * (constr * sorts)
val e_new_type_evar : env -> evar_map ref ->
?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
val restrict_evar : evar_map -> existential_key -> Filter.t ->
constr list option -> evar_map * existential_key
(** Polymorphic constants *)
val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
val e_new_global : evar_map ref -> Globnames.global_reference -> constr
(** Create a fresh evar in a context different from its definition context:
[new_evar_instance sign evd ty inst] creates a new evar of context
[sign] and type [ty], [inst] is a mapping of the evar context to
the context where the evar should occur. This means that the terms
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
named_context_val -> evar_map -> types ->
?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool ->
constr list -> evar_map * constr
val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
(** {6 Evars/Metas switching...} *)
val non_instantiated : evar_map -> evar_info Evar.Map.t
(** {6 Unification utils} *)
(** [head_evar c] returns the head evar of [c] if any *)
exception NoHeadEvar
val head_evar : constr -> existential_key (** 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
(** [check_evars env initial_sigma extended_sigma c] fails if some
new unresolved evar remains in [c] *)
val check_evars : env -> evar_map -> evar_map -> constr -> unit
val define_evar_as_product : evar_map -> existential -> evar_map * types
val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
(** Instantiate an evar by as many lambda's as needed so that its arguments
are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
[?y[vars1:=args1,vars:=args]] with
[vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
evar_map * existential
(** [gather_dependent_evars evm seeds] classifies the evars in [evm]
as dependent_evars and goals (these may overlap). A goal is an
evar in [seeds] or an evar appearing in the (partial) definition
of a goal. A dependent evar is an evar appearing in the type
(hypotheses and conclusion) of a goal, or in the type or (partial)
definition of a dependent evar. The value return is a map
associating to each dependent evar [None] if it has no (partial)
definition or [Some s] if [s] is the list of evars appearing in
its (partial) definition. *)
val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.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 -> named_context -> Evar.Set.t
val undefined_evars_of_evar_info : evar_map -> 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.t -> bool
(** {6 Value/Type constraints} *)
val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
type type_constraint = types option
type val_constraint = constr option
val empty_tycon : type_constraint
val mk_tycon : constr -> type_constraint
val empty_valcon : val_constraint
val mk_valcon : constr -> val_constraint
val split_tycon :
Loc.t -> env -> evar_map -> type_constraint ->
evar_map * (Name.t * type_constraint * type_constraint)
val valcon_of_tycon : type_constraint -> val_constraint
val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
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 -> named_context -> 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 -> evar_info -> evar_info
val nf_evar_map : evar_map -> evar_map
val nf_evar_map_undefined : evar_map -> evar_map
val env_nf_evar : evar_map -> env -> env
val env_nf_betaiotaevar : evar_map -> env -> env
val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment
val jv_nf_betaiotaevar :
evar_map -> unsafe_judgment array -> unsafe_judgment array
(** Presenting terms without solved evars *)
val nf_evars_universes : evar_map -> constr -> constr
val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
(** Normalize the evar map w.r.t. universes, after simplification of constraints.
Return the substitution function for constrs as well. *)
val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
exception Uninstantiated_evar of existential_key
val flush_and_check_evars : evar_map -> constr -> constr
(** {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,types) kind_of_term
(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
[u] up to existential variable instantiation and equalisable
universes. The term [t] is interpreted in [sigma1] while [u] is
interpreted in [sigma2]. The universe constraints in [sigma2] are
assumed to be an extention of those in [sigma1]. *)
val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
(** {6 debug pretty-printer:} *)
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
(** {6 Removing hyps in evars'context}
raise OccurHypInSimpleClause if the removal breaks dependencies *)
type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of existential
exception ClearDependencyError of Id.t * clear_dependency_error
(* spiwack: marks an evar that has been "defined" by clear.
used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
val cleared : bool Store.field
val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
Id.Set.t -> named_context_val * types
val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
Id.Set.t -> named_context_val * types * types
val push_rel_context_to_named_context : Environ.env -> types ->
named_context_val * types * constr list * constr list * (identifier*constr) list
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
(** Evar combinators *)
val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
val meta_counter_summary_name : string
|
