2 files changed, 116 insertions, 0 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml
new file mode 100644
index 000000000..48b2a4b57
--- /dev/null
+++ b/kernel/evd.ml
@@ -0,0 +1,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)
diff --git a/kernel/evd.mli b/kernel/evd.mli
new file mode 100644
index 000000000..8063f42b0
--- /dev/null
+++ b/kernel/evd.mli
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+(*i*)
+
+(* The type of mappings for existential variables.
+   The keys are section paths and the associated information is a record
+   containing the type of the evar ([concl]), the signature under which 
+   it was introduced ([hyps]), its definition ([body]) and any other 
+   possible information if necessary ([info]).
+*)
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type 'a evar_info = {
+  evar_concl : typed_type;
+  evar_hyps  : typed_type signature;
+  evar_body  : evar_body;
+  evar_info  : 'a option }
+
+type 'a evar_map
+
+val dom    : 'a evar_map -> section_path list
+val map    : 'a evar_map -> section_path -> 'a evar_info
+val rmv    : 'a evar_map -> section_path -> 'a evar_map
+val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val in_dom : 'a evar_map -> section_path -> bool
+val toList : 'a evar_map -> (section_path * 'a evar_info) list
+
+val mt_evd : 'a evar_map
+val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val add_noinfo : 
+  'a evar_map -> section_path -> typed_type signature -> typed_type 
+    -> 'a evar_map
+
+val define : 'a evar_map -> section_path -> constr -> 'a evar_map
+
+val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
+val is_evar : 'a evar_map -> section_path -> bool
+
+val is_defined : 'a evar_map -> section_path -> bool
+