COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / components / cic_unification / coercGraph.ml

diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml
index 37ded8ee0675de18ca3600be2cba6ac57ec1e75d..cb33d9e324f0b41851668c37c1f237770b33342a 100644 (file)
--- a/components/cic_unification/coercGraph.ml
+++ b/components/cic_unification/coercGraph.ml
@@ -32,6 +32,7 @@ type coercion_search_result =
      (* to apply the coercion it is sufficient to unify the last coercion
         argument (that is a Meta) with the term to be coerced *)
   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+  | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
@@ -65,30 +66,38 @@ let saturate_coercion ul metasenv subst context =
           
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion' metasenv subst context src tgt =
+  let pp_l s l =
+   match l with
+   | [] -> 
+       debug_print 
+         (lazy 
+         (sprintf ":-( coercion non trovata[%s] da %s a %s" s
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)));
+   | _::_ -> 
+       debug_print (lazy (
+               sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
+           (List.length l)
+           (CoercDb.name_of_carr src) 
+           (CoercDb.name_of_carr tgt)));
+  in
   try 
     let l = 
       CoercDb.find_coercion 
-        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
-    let uri =
-     match l with
-     | [] -> 
-         debug_print 
-           (lazy 
-             (sprintf ":-( coercion non trovata da %s a %s" 
-               (CoercDb.name_of_carr src) 
-               (CoercDb.name_of_carr tgt)));
-         None
-     | _::_ -> 
-         debug_print (lazy (
-           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
-             (List.length l)
-             (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)));
-         Some l
+        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
     in
-     (match uri with
-         None -> NoCoercion
-       | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
+    pp_l "precise" l;
+     (match l with
+     | [] -> 
+         let l = 
+           CoercDb.find_coercion 
+             (fun (_,t) -> CoercDb.eq_carr t tgt) 
+         in
+         pp_l "approx" l;
+         (match l with
+         | [] -> NoCoercion
+         | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+     | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed