2
(************************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
5
(* \VV/ **************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(************************************************************************)
10
(*i $Id: evd.mli 11865 2009-01-28 17:34:30Z herbelin $ i*)
23
(* The type of mappings for existential variables.
24
The keys are integers and the associated information is a record
25
containing the type of the evar ([evar_concl]), the context under which
26
it was introduced ([evar_hyps]) and its definition ([evar_body]).
27
[evar_info] is used to add any other kind of information. *)
29
type evar = existential_key
33
| Evar_defined of constr
37
evar_hyps : named_context_val;
38
evar_body : evar_body;
39
evar_filter : bool list;
40
evar_extra : Dyn.t option}
42
val eq_evar_info : evar_info -> evar_info -> bool
44
val make_evar : named_context_val -> types -> evar_info
45
val evar_concl : evar_info -> constr
46
val evar_context : evar_info -> named_context
47
val evar_filtered_context : evar_info -> named_context
48
val evar_hyps : evar_info -> named_context_val
49
val evar_body : evar_info -> evar_body
50
val evar_filter : evar_info -> bool list
51
val evar_unfiltered_env : evar_info -> env
52
val evar_env : evar_info -> env
55
val eq_evar_map : evar_map -> evar_map -> bool
59
val add : evar_map -> evar -> evar_info -> evar_map
61
val dom : evar_map -> evar list
62
val find : evar_map -> evar -> evar_info
63
val remove : evar_map -> evar -> evar_map
64
val mem : evar_map -> evar -> bool
65
val to_list : evar_map -> (evar * evar_info) list
66
val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
68
val merge : evar_map -> evar_map -> evar_map
70
val define : evar_map -> evar -> constr -> evar_map
72
val is_evar : evar_map -> evar -> bool
74
val is_defined : evar_map -> evar -> bool
76
val string_of_existential : evar -> string
77
val existential_of_int : int -> evar
79
(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
80
no body and [Not_found] if it does not exist in [sigma] *)
82
exception NotInstantiatedEvar
83
val existential_value : evar_map -> existential -> constr
84
val existential_type : evar_map -> existential -> types
85
val existential_opt_value : evar_map -> existential -> constr option
87
(*********************************************************************)
88
(* constr with holes *)
89
type open_constr = evar_map * constr
91
(*********************************************************************)
92
(* The type constructor ['a sigma] adds an evar map to an object of
98
val sig_it : 'a sigma -> 'a
99
val sig_sig : 'a sigma -> evar_map
101
(*********************************************************************)
104
module Metamap : Map.S with type key = metavariable
106
module Metaset : Set.S with type elt = metavariable
108
val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
110
type 'a freelisted = {
112
freemetas : Metaset.t }
114
val metavars_of : constr -> Metaset.t
115
val mk_freelisted : constr -> constr freelisted
116
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
118
(* Status of an instance found by unification wrt to the meta it solves:
119
- a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
120
- a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
121
- a term that can be eta-expanded n times while still being a solution
122
(e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
125
type instance_constraint =
126
IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
128
(* Status of the unification of the type of an instance against the type of
129
the meta it instantiates:
130
- CoerceToType means that the unification of types has not been done
131
and that a coercion can still be inserted: the meta should not be
132
substituted freely (this happens for instance given via the
133
"with" binding clause).
134
- TypeProcessed means that the information obtainable from the
135
unification of types has been extracted.
136
- TypeNotProcessed means that the unification of types has not been
137
done but it is known that no coercion may be inserted: the meta
138
can be substituted freely.
141
type instance_typing_status =
142
CoerceToType | TypeNotProcessed | TypeProcessed
144
(* Status of an instance together with the status of its type unification *)
146
type instance_status = instance_constraint * instance_typing_status
148
(* Clausal environments *)
151
| Cltyp of name * constr freelisted
152
| Clval of name * (constr freelisted * instance_status) * constr freelisted
154
val map_clb : (constr -> constr) -> clbinding -> clbinding
156
(*********************************************************************)
157
(* Unification state *)
160
(* Assume empty [evar_map] and [conv_pbs] *)
161
val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
163
(* create an [evar_defs] with empty meta map: *)
164
val create_evar_defs : evar_map -> evar_defs
165
val create_goal_evar_defs : evar_map -> evar_defs
166
val empty_evar_defs : evar_defs
167
val evars_of : evar_defs -> evar_map
168
val evars_reset_evd : evar_map -> evar_defs -> evar_defs
170
(* Should the obligation be defined (opaque or transparent (default)) or
171
defined transparent and expanded in the term? *)
173
type obligation_definition_status = Define of bool | Expand
177
| ImplicitArg of global_reference * (int * identifier option)
179
| QuestionMark of obligation_definition_status
182
| TomatchTypeParameter of inductive * int
185
val is_defined_evar : evar_defs -> existential -> bool
186
val is_undefined_evar : evar_defs -> constr -> bool
187
val undefined_evars : evar_defs -> evar_defs
189
named_context_val -> evar -> types -> ?src:loc * hole_kind ->
190
?filter:bool list -> evar_defs -> evar_defs
191
val evar_define : evar -> constr -> evar_defs -> evar_defs
192
val evar_source : existential_key -> evar_defs -> loc * hole_kind
194
(* [evar_merge evd evars] extends the evars of [evd] with [evars] *)
195
val evar_merge : evar_defs -> evar_map -> evar_defs
197
(* Unification constraints *)
198
type conv_pb = Reduction.conv_pb
199
type evar_constraint = conv_pb * env * constr * constr
200
val add_conv_pb : evar_constraint -> evar_defs -> evar_defs
201
val extract_changed_conv_pbs : evar_defs ->
202
(existential_key list -> evar_constraint -> bool) ->
203
evar_defs * evar_constraint list
204
val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list
208
val find_meta : evar_defs -> metavariable -> clbinding
209
val meta_list : evar_defs -> (metavariable * clbinding) list
210
val meta_defined : evar_defs -> metavariable -> bool
211
(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
213
val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status
214
val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option
215
val meta_ftype : evar_defs -> metavariable -> constr freelisted
216
val meta_name : evar_defs -> metavariable -> name
217
val meta_with_name : evar_defs -> identifier -> metavariable
219
metavariable -> types -> ?name:name -> evar_defs -> evar_defs
220
val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
221
val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
223
(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
224
val meta_merge : evar_defs -> evar_defs -> evar_defs
226
val undefined_metas : evar_defs -> metavariable list
227
val metas_of : evar_defs -> metamap
228
val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
230
type metabinding = metavariable * constr * instance_status
232
val retract_coercible_metas : evar_defs -> metabinding list * evar_defs
233
val subst_defined_metas : metabinding list -> constr -> constr option
235
(**********************************************************)
238
val new_sort_variable : evar_map -> sorts * evar_map
239
val is_sort_variable : evar_map -> sorts -> bool
240
val whd_sort_variable : evar_map -> constr -> constr
241
val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
242
val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
244
(**********************************************************)
245
(* Failure explanation *)
247
type unsolvability_explanation = SeveralInstancesFound of int
249
(*********************************************************************)
250
(* debug pretty-printer: *)
252
val pr_evar_info : evar_info -> Pp.std_ppcmds
253
val pr_evar_map : evar_map -> Pp.std_ppcmds
254
val pr_evar_defs : evar_defs -> Pp.std_ppcmds
255
val pr_sort_constraints : evar_map -> Pp.std_ppcmds
256
val pr_metaset : Metaset.t -> Pp.std_ppcmds
added
removed
pretyping/evd.mli
