blob: 5d03fbfd369fab9a1aede314a2b34e4d07f50832 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Names
open Term
open Sign
open Environ
open Libnames
open Mod_subst
open Termops
(*i*)
(* The type of mappings for existential variables.
The keys are integers and the associated information is a record
containing the type of the evar ([evar_concl]), the context under which
it was introduced ([evar_hyps]) and its definition ([evar_body]).
[evar_info] is used to add any other kind of information. *)
type evar = existential_key
type evar_body =
| Evar_empty
| Evar_defined of constr
type evar_info = {
evar_concl : constr;
evar_hyps : named_context_val;
evar_body : evar_body;
evar_filter : bool list;
evar_extra : Dyn.t option}
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_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
type evar_map
val empty : evar_map
val add : evar_map -> evar -> evar_info -> evar_map
val dom : evar_map -> evar list
val find : evar_map -> evar -> evar_info
val remove : evar_map -> evar -> evar_map
val mem : evar_map -> evar -> bool
val to_list : evar_map -> (evar * evar_info) list
val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
val merge : evar_map -> evar_map -> evar_map
val define : evar_map -> evar -> constr -> evar_map
val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
val string_of_existential : evar -> string
val existential_of_int : int -> evar
(*s [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
(*********************************************************************)
(* 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
(*********************************************************************)
(* Meta map *)
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
(* Possible constraints over the instance of a metavariable:
- 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 | ConvUpToEta of int | UserGiven
type instance_typing_status =
CoerceToType | TypeNotProcessed | TypeProcessed
type instance_status = instance_constraint * instance_typing_status
type clbinding =
| Cltyp of name * constr freelisted
| Clval of name * (constr freelisted * instance_status) * constr freelisted
val map_clb : (constr -> constr) -> clbinding -> clbinding
(*********************************************************************)
(* Unification state *)
type evar_defs
(* Assume empty [evar_map] and [conv_pbs] *)
val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
(* create an [evar_defs] with empty meta map: *)
val create_evar_defs : evar_map -> evar_defs
val create_goal_evar_defs : evar_map -> evar_defs
val evars_of : evar_defs -> evar_map
val evars_reset_evd : evar_map -> evar_defs -> evar_defs
(* Evars *)
type hole_kind =
| ImplicitArg of global_reference * (int * identifier option)
| BinderType of name
| QuestionMark of bool (* Can it be turned into an obligation ? *)
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
| GoalEvar
val is_defined_evar : evar_defs -> existential -> bool
val is_undefined_evar : evar_defs -> constr -> bool
val undefined_evars : evar_defs -> evar_defs
val evar_declare :
named_context_val -> evar -> types -> ?src:loc * hole_kind ->
?filter:bool list -> evar_defs -> evar_defs
val evar_define : evar -> constr -> evar_defs -> evar_defs
val evar_source : existential_key -> evar_defs -> loc * hole_kind
(* [evar_merge evd evars] extends the evars of [evd] with [evars] *)
val evar_merge : evar_defs -> evar_map -> evar_defs
(* Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
val add_conv_pb : evar_constraint -> evar_defs -> evar_defs
val extract_changed_conv_pbs : evar_defs ->
(existential_key list -> evar_constraint -> bool) ->
evar_defs * evar_constraint list
val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list
(* Metas *)
val meta_list : evar_defs -> (metavariable * clbinding) list
val meta_defined : evar_defs -> metavariable -> bool
(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
meta has no value *)
val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status
val meta_ftype : evar_defs -> metavariable -> constr freelisted
val meta_name : evar_defs -> metavariable -> name
val meta_with_name : evar_defs -> identifier -> metavariable
val meta_declare :
metavariable -> types -> ?name:name -> evar_defs -> evar_defs
val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
val meta_merge : evar_defs -> evar_defs -> evar_defs
val metas_of : evar_defs -> metamap
type metabinding = metavariable * constr * instance_status
val retract_coercible_metas : evar_defs -> metabinding list * evar_defs
val subst_defined_metas : metabinding list -> constr -> constr option
(**********************************************************)
(* Sort variables *)
val new_sort_variable : evar_map -> sorts * evar_map
val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
(*********************************************************************)
(* debug pretty-printer: *)
val pr_evar_info : evar_info -> Pp.std_ppcmds
val pr_evar_map : evar_map -> Pp.std_ppcmds
val pr_evar_defs : evar_defs -> Pp.std_ppcmds
val pr_sort_constraints : evar_map -> Pp.std_ppcmds
val pr_metaset : Metaset.t -> Pp.std_ppcmds
|
