blob: e1fc425befc71abb616cd6bf6964b892d2f41106 (
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
|
(************************************************************************)
(* 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: evd.mli 9573 2007-01-31 20:18:18Z notin $ i*)
(*i*)
open Util
open Names
open Term
open Sign
open Libnames
open Mod_subst
(*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 : Environ.named_context_val;
evar_body : evar_body;
evar_extra : Dyn.t option}
val eq_evar_info : evar_info -> evar_info -> bool
val evar_context : evar_info -> named_context
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 define : evar_map -> evar -> constr -> evar_map
val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
val evar_concl : evar_info -> constr
val evar_hyps : evar_info -> Environ.named_context_val
val evar_body : evar_info -> evar_body
val evar_env : evar_info -> Environ.env
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
type clbinding =
| Cltyp of name * constr freelisted
| Clval of name * constr freelisted * constr freelisted
val map_clb : (constr -> constr) -> clbinding -> clbinding
(*********************************************************************)
(* Unification state *)
type evar_defs
(* Substitution is not applied to the [evar_map] *)
val subst_evar_defs : substitution -> evar_defs -> evar_defs
(* create an [evar_defs] with empty meta map: *)
val create_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
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
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 :
Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind ->
evar_defs -> evar_defs
val evar_define : evar -> constr -> evar_defs -> evar_defs
val evar_source : existential_key -> evar_defs -> loc * hole_kind
(* Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * constr * constr
val add_conv_pb : evar_constraint -> evar_defs -> evar_defs
val get_conv_pbs : evar_defs -> (evar_constraint -> bool) ->
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
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 -> 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
(**********************************************************)
(* 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
|
