aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/evd.ml
blob: b482f9453844cb91ecfe403ed8dbe36bb052d6d2 (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

(* $Id$ *)

open Util
open Names
open Term
open Sign
open Environ

(* The type of mappings for existential variables *)

type evar = int

let new_evar =
  let evar_ctr = ref 0 in
  fun () -> incr evar_ctr; !evar_ctr

type evar_body =
  | Evar_empty 
  | Evar_defined of constr

type 'a evar_info = {
  evar_concl : constr;
  evar_env : env;
  evar_body : evar_body;
  evar_info : 'a option }

type 'a evar_map = 'a evar_info Intmap.t

let empty = Intmap.empty

let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc []
let map evc k = Intmap.find k evc
let rmv evc k = Intmap.remove k evc
let remap evc k i = Intmap.add k i evc
let in_dom evc k = Intmap.mem k evc

let add evd ev newinfo =  Intmap.add ev newinfo evd

let define evd ev body = 
  let oldinfo = map evd ev in
  let newinfo =
    { evar_concl = oldinfo.evar_concl;
      evar_env = oldinfo.evar_env;
      evar_body = Evar_defined body;
      evar_info = oldinfo.evar_info } 
  in
  match oldinfo.evar_body with
    | Evar_empty -> Intmap.add ev newinfo evd
    | _ -> anomaly "cannot define an isevar twice"

(* The list of non-instantiated existential declarations *)

let non_instantiated sigma = 
  let listev = to_list sigma in
  List.fold_left 
    (fun l ((ev,evd) as d) -> 
       if evd.evar_body = Evar_empty then (d::l) else l)
    [] listev
    
let is_evar sigma ev = in_dom sigma ev

let is_defined sigma ev =
  let info = map sigma ev in 
  not (info.evar_body = Evar_empty)

let evar_hyps ev = var_context ev.evar_env
let evar_body ev = ev.evar_body

let id_of_existential ev =
  id_of_string ("?" ^ string_of_int ev)