X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=3a4dac726783e0e6584a8a772efc8d7f1c7aaaa4;hb=0d1ecc789c6d57a3eef47a028634d316905ef317;hp=7203f3647e6eefb642c5fd93be6ff7d465918aa5;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 7203f3647..3a4dac726 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -32,17 +32,19 @@ exception EqCarrOnNonMetaClosed
 let db = ref []
 
 let coerc_carr_of_term t =
-  try
-    Uri (CicUtil.uri_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
+ try
+  match t with
+     Cic.Sort s -> Sort s
+   | Cic.Appl (t::_)
+   | t -> Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+  Term t
 ;;
 
+let uri_of_carr = function
+  | Uri u -> Some u
+  | _ -> None
+
 let rec name_of_carr = function
   | Uri u -> UriManager.name_of_uri u
   | Sort s -> CicPp.ppsort s
@@ -61,39 +63,64 @@ let eq_carr src tgt =
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->
-    if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
-      raise 
-        (EqCarrNotImplemented 
+      if t1 = t2 then true
+      else
+        if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
+          raise 
+          (EqCarrNotImplemented 
           (lazy ("Unsupported carr for coercions: " ^ 
-            CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
-    else raise EqCarrOnNonMetaClosed
+          CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
+      else raise EqCarrOnNonMetaClosed
   | _, _ -> false
 
 let to_list () =
   !db
 
-let add_coercion c =
-  db := c :: !db
-
-let remove_coercion p = 
-  db := List.filter (fun u -> not(p u)) !db
+let rec myfilter p = function
+  | [] -> []
+  | (s,t,l)::tl ->
+      let l = List.filter (fun u -> not (p (s,t,u))) l in
+      if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
+;;
+  
+let remove_coercion p = db := myfilter p !db;;
 
 let find_coercion f =
-  List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+  List.flatten 
+    (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 is_a_coercion u = 
+  List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
+;;
 
 let get_carr uri =
   try
-    let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+    let src, tgt, _ = 
+      List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !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
+;;
   
+let add_coercion (src,tgt,u) =
+  let f s t = eq_carr s src && eq_carr t tgt in
+  let where = List.filter (fun (s,t,_) -> f s t) !db in
+  let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
+  match where with
+  | [] -> db := (src,tgt,[u]) :: !db
+  | (src,tgt,l)::tl ->
+      assert (tl = []); (* not sure, this may be a feature *)
+      db := (src,tgt,u::l)::tl @ rest
+;;
+