X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercDb.ml;h=8e2c62f310ca5b14251dcaa0a72dd2f94424688e;hb=6f0e3275c5a100568c8529d6c58150ef4af692d0;hp=437ad65ae202bcddab717c3fa5e5d327f63d6dfc;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git

diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml
index 437ad65ae..8e2c62f31 100644
--- a/helm/ocaml/library/coercDb.ml
+++ b/helm/ocaml/library/coercDb.ml
@@ -23,12 +23,13 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 
 let db = ref []
-let use_coercions = ref true
 
 let coerc_carr_of_term t =
   try
@@ -36,9 +37,21 @@ let coerc_carr_of_term t =
   with Invalid_argument _ ->
     match t with
     | Cic.Sort s -> Sort s
+    | Cic.Appl ((Cic.Const (uri, _))::_) 
+    | Cic.Appl ((Cic.MutInd (uri, _, _))::_) 
+    | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri
     | t -> Term t
 ;;
 
+let name_of_carr = function
+  | Uri u -> UriManager.name_of_uri u
+  | Sort s -> CicPp.ppsort s
+  | Term (Cic.Appl ((Cic.Const (uri, _))::_)) 
+  | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) 
+  | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> 
+        UriManager.name_of_uri uri
+  | Term t -> (* CicPp.ppterm t *) assert false
+
 let eq_carr src tgt =
   match src, tgt with
   | Uri src, Uri tgt -> UriManager.eq src tgt
@@ -53,12 +66,6 @@ let eq_carr src tgt =
     else raise EqCarrOnNonMetaClosed
   | _, _ -> false
 
-let name_of_carr = function
-  | Uri u -> UriManager.name_of_uri u
-  | Sort s -> CicPp.ppsort s
-  | Term t -> CicPp.ppterm t
-  
-
 let to_list () =
   !db
 
@@ -69,7 +76,21 @@ let remove_coercion p =
   db := List.filter (fun u -> not(p u)) !db
 
 let find_coercion f =
-  if !use_coercions then
-    List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
-  else []
+  List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+
+let is_a_coercion u =
+  List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+
+let get_carr uri =
+  try
+    let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+    src, tgt
+  with Not_found -> assert false (* uri must be a coercion *)
+
+let term_of_carr = function
+  | Uri u -> CicUtil.term_of_uri u
+  | Sort s -> Cic.Sort s
+  | Term _ -> assert false
+  
+