refactoring

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

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 898946ad64f6d89e77c0b18900644c55b0b8462c..6c253df9f73c9274ec1087b122415f9312374962 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -25,7 +25,7 @@
 
 (* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *)
 
-let debug = false
+let debug = false 
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* given the new coercion uri from src to tgt returns the list 
@@ -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)
@@ -202,8 +207,10 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   let spline_len = saturations_for_c1 + saturations_for_c2 in
   let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
+  let old_insert_coercions = !CicRefine.insert_coercions in
   let c, metasenv, univ = 
     try
+      CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context c univ
       in
@@ -246,11 +253,16 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       in
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
       debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+      CicRefine.insert_coercions := old_insert_coercions;
       term, metasenv, ugraph
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
+        CicRefine.insert_coercions := old_insert_coercions;
         raise UnableToCompose
+    | exn ->
+        CicRefine.insert_coercions := old_insert_coercions;
+        raise exn
   in  
   c, metasenv, univ 
 ;;
@@ -316,8 +328,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
@@ -357,8 +369,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