blob: e5197db4e2f3300302630acd8efc8edaf1d8fb42 (
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
|
(* $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 = {
evar_concl : typed_type; (* the type of the evar ... *)
evar_hyps : typed_type signature; (* ... under a certain signature *)
evar_body : evar_body; (* its definition *)
evar_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 =
{ evar_concl = typ;
evar_hyps = sign;
evar_body = EVAR_EMPTY;
evar_info = None}
in
Spmap.add sp newinfo evd
let define evd sp body =
let oldinfo = map evd sp in
let newinfo =
{ evar_concl = oldinfo.evar_concl;
evar_hyps = oldinfo.evar_hyps;
evar_body = EVAR_DEFINED body;
evar_info = oldinfo.evar_info}
in
match oldinfo.evar_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.evar_body = EVAR_EMPTY then (d::l) else l)
[] listsp
let is_evar sigma sp = in_dom sigma sp
let is_defined sigma sp =
let info = map sigma sp in not (info.evar_body = EVAR_EMPTY)
|
