blob: 77351ab9b74081f3c9a8d101ef4ae21c0a57e7ac (
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
|
(* $Id$ *)
open Util
open Names
open Term
open Sign
(* The type of mappings for existential variables *)
type evar_body =
EVAR_EMPTY | EVAR_DEFINED of constr
type 'a evar_info = {
concl : constr; (* the type of the evar ... *)
hyps : context; (* ... under a certain signature *)
body : evar_body; (* its definition *)
info : 'a option (* any other necessary information *)
}
type 'a evar_map = 'a evar_info Spmap.t
let mt_evd = Spmap.empty
let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc []
let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc []
let map evc k = Spmap.find k evc
let rmv evc k = Spmap.remove k evc
let remap evc k i = Spmap.add k i evc
let in_dom evc k = Spmap.mem k evc
let add_with_info evd sp newinfo =
Spmap.add sp newinfo evd
let add_noinfo evd sp sign typ =
let newinfo =
{ concl = typ;
hyps = sign;
body = EVAR_EMPTY;
info = None}
in
Spmap.add sp newinfo evd
let define evd sp body =
let oldinfo = map evd sp in
let newinfo =
{ concl = oldinfo.concl;
hyps = oldinfo.hyps;
body = EVAR_DEFINED body;
info = oldinfo.info}
in
match oldinfo.body with
| EVAR_EMPTY -> Spmap.add sp newinfo evd
| _ -> anomaly "cannot define an isevar twice"
(* The list of non-instantiated existential declarations *)
let non_instantiated sigma =
let listsp = toList sigma in
List.fold_left
(fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l)
[] listsp
let is_evar sigma sp = in_dom sigma sp
|
