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 a009944f8c26fe4b14caf41059507e0022e72ddf..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,7 @@ 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
   let rec mk_implicits = function
@@ -105,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])
@@ -177,8 +182,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
     List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
           try List.assoc i meta2no -  List.assoc j meta2no 
-          with Not_found -> 
-            assert false) 
+          with Not_found -> assert false) 
       body_metasenv
   in
   let namer l n = 
@@ -221,6 +225,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
       debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
       let term = CicMetaSubst.apply_subst subst term in
+      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
       debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context term ugraph
@@ -228,7 +233,22 @@ 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 
+          (fun (i,_,_) -> 
+            List.for_all 
+              (fun (j,_,_) ->
+                i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv) 
+              lambdas_metasenv) 
+          metasenv 
+      in
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
       debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       term, metasenv, ugraph
@@ -301,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
@@ -313,7 +333,7 @@ let number_if_already_defined buri name l =
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
-let close_coercion_graph _ src tgt uri baseuri =
+let close_coercion_graph src tgt uri baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt uri coercions in
@@ -341,7 +361,8 @@ let close_coercion_graph _ src tgt uri baseuri =
                             (CoercDb.term_of_carr (CoercDb.Uri coer)) 
                             [] [] univ arity true
                         in
-                        assert (menv = []);
+                        if (menv = []) then
+                          HLog.warn "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl