COERCIONS: tentative addition of an equivalence relation over coercion source

carriers (convertibility) for the moment used only in the FunClass case.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 840a955cb8a7218749b74aeed1203ab52485004f..856c9a58622480d6f938cbeb0e8a25c1ce913473 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -454,6 +454,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     in
                     (match boh with
                     | CoercGraph.NoCoercion
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                        enrich localization_tbl t
                         (RefineFailure 
@@ -526,6 +527,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      in
                       match boh with
                       | CoercGraph.NoCoercion
+                      | CoercGraph.SomeCoercionToTgt _
                       |  CoercGraph.NotHandled _ ->
                         enrich localization_tbl s'
                          (RefineFailure 
@@ -1363,6 +1365,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         | CoercGraph.NoCoercion 
         | CoercGraph.NotMetaClosed 
         | CoercGraph.NotHandled _ -> raise exn
+        | CoercGraph.SomeCoercionToTgt candidates
         | CoercGraph.SomeCoercion candidates ->
             match  
             HExtlib.list_findopt 
@@ -1447,6 +1450,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     in
                     (match coer with
                     | CoercGraph.NoCoercion 
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 37ded8ee0675de18ca3600be2cba6ac57ec1e75d..cb33d9e324f0b41851668c37c1f237770b33342a 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/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

diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index ae2bd9233943c3d1993be89f0c05d1fb6a775396..711a1527d940c17fdb66b2c0acabc85c5eb1d967 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -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

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 2e93efa0eb8e09c43bc47b7946e83069491ac14c..aec6dd5795bb9051adf78ce7336cc5f34cef6193 100644 (file)
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -66,9 +66,20 @@ let rec name_of_carr = function
   | Fun i -> "FunClass_" ^ string_of_int i   
 ;;
 
-let eq_carr src tgt =
+let eq_carr ?(exact=false) src tgt =
   match src, tgt with
-  | Uri src, Uri tgt -> UriManager.eq src tgt
+  | Uri src, Uri tgt -> 
+      let coarse_eq = UriManager.eq src tgt in
+      let src_noxpointer = UriManager.strip_xpointer src in
+      if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
+        match 
+          fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
+        with
+        | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
+        | Cic.Constant _ -> true
+        | _ -> false
+      else
+        coarse_eq
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->

diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli
index 5f455c2af97dd6146bddeebd64c0f281ce0b6334..e6d7e46b30042778b6b3889970c56dac329741bd 100644 (file)
--- a/helm/software/components/library/coercDb.mli
+++ b/helm/software/components/library/coercDb.mli
@@ -41,7 +41,7 @@ type coerc_carr =
   
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
 val coerc_carr_of_term: Cic.term -> coerc_carr
 val name_of_carr: coerc_carr -> string
 val uri_of_carr: coerc_carr -> UriManager.uri option

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index d9dc679b32c35c85cafd5b25b68c66f45df554e3..2cff9c608b19816edc3d571beb92431203c1b63c 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -52,15 +52,20 @@ let get_closure_coercions src tgt uri coercions =
           coercions 
       in
         (HExtlib.flatten_map 
-          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+          (fun (_,t,ul) -> 
+             if CoercDb.eq_carr ~exact:true src t then [] else
+             List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
         (HExtlib.flatten_map 
-          (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+          (fun (s,_,ul) -> 
+             if CoercDb.eq_carr ~exact:true s tgt then [] else
+             List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
         (HExtlib.flatten_map 
           (fun (s,_,u1l) ->
             HExtlib.flatten_map 
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
                   (fun u1 ->
+                    if CoercDb.eq_carr ~exact:true s t then [] else
                     List.map 
                       (fun u2 -> (s,[u1;uri;u2],t)) 
                       u2l)