generic, term et evd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 64 insertions, 0 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
new file mode 100644
index 0000000000..77351ab9b7
--- /dev/null
+++ b/kernel/evd.ml
@@ -0,0 +1,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