COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / components / tactics / closeCoercionGraph.ml

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 3e64110987cef40500d3339e833f007204525f55..2cff9c608b19816edc3d571beb92431203c1b63c 100644 (file)
--- a/components/tactics/closeCoercionGraph.ml
+++ b/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)
@@ -77,7 +82,6 @@ exception UnableToCompose
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * both living in the same context and metasenv *)
 let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
-  let module RT = RefinementTool in
   let original_metasenv = metasenv in 
   let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
@@ -106,7 +110,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   in
   let compose c1 nc1 c2 nc2 =
     Cic.Lambda 
-      (Cic.Name "x", (Cic.Implicit None),
+      (Cic.Name "x", (Cic.Implicit (Some `Type)),
           (Cic.Appl (  CicSubstitution.lift 1 c2 :: mk_implicits nc2 @ 
             [ Cic.Appl (  CicSubstitution.lift 1 c1 :: mk_implicits nc1 @ 
              [if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
@@ -229,6 +233,12 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       let body_metasenv, lambdas_metasenv = 
         split_metasenv metasenv (spline_len + List.length context)
       in
+      let lambdas_metasenv = 
+        List.filter 
+          (fun (i,_,_) -> 
+            List.for_all (fun (j,_,_) -> i <> j) original_metasenv)
+          lambdas_metasenv
+      in
       let term = purge_unused_lambdas lambdas_metasenv term in
       let metasenv = 
         List.filter 
@@ -311,8 +321,8 @@ let number_if_already_defined buri name l =
     if List.exists (UriManager.eq uri) l then retry ()
     else
       try
-        let _  = Http_getter.resolve' ~writable:true uri in
-        if Http_getter.exists' uri then retry () else uri
+        let _  = Http_getter.resolve' ~local:true ~writable:true uri in
+        if Http_getter.exists' ~local:true uri then retry () else uri
       with 
       | Http_getter_types.Key_not_found _ -> uri
       | Http_getter_types.Unresolvable_URI _ -> assert false
@@ -352,8 +362,7 @@ let close_coercion_graph src tgt uri baseuri =
                             [] [] univ arity true
                         in
                         if (menv = []) then
-                          prerr_endline 
-                            "MENV non empty after composing coercions";
+                          HLog.warn "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl