compose tactic restore and added nocomposites keyword

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

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 95b9fd6e04f04a100746d316a95059fe264eae15..7ed3c36e6b86d24d4a46b753a750e11597d919c0 100644 (file)
--- a/components/tactics/closeCoercionGraph.ml
+++ b/components/tactics/closeCoercionGraph.ml
@@ -39,21 +39,33 @@ let get_closure_coercions src tgt uri coercions =
   in
   let uri = enrich uri tgt in
   let eq_carr ?exact s t = 
+    debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t));
     try
-      CoercDb.eq_carr ?exact s t
+            let rc = CoercDb.eq_carr ?exact s t in
+            debug_print(lazy(string_of_bool rc));
+            rc
     with
-    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> 
+        debug_print (lazy("false"));            
+        false
   in
   match src,tgt with
   | CoercDb.Uri _, CoercDb.Uri _ ->
+                  debug_print (lazy ("Uri, Uri4"));
       let c_from_tgt = 
         List.filter 
-          (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
+          (fun (f,t,_) -> 
+                  
+                  debug_print (lazy ("Uri, Uri3"));
+                  eq_carr f tgt (*&& not (eq_carr t src)*)) 
           coercions 
       in
       let c_to_src = 
         List.filter 
-          (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
+          (fun (f,t,_) -> 
+                  
+                  debug_print (lazy ("Uri, Uri2"));
+                  eq_carr t src (*&& not (eq_carr f tgt)*)) 
           coercions 
       in
         (HExtlib.flatten_map 
@@ -70,6 +82,7 @@ let get_closure_coercions src tgt uri coercions =
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
                   (fun u1 ->
+                  debug_print (lazy ("Uri, Uri1"));
                     if  eq_carr ~exact:true s t
                      || eq_carr ~exact:true s tgt
                      || eq_carr ~exact:true src t
@@ -122,8 +135,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       names
   in
   let compose c1 nc1 c2 nc2 =
-   Cic.Appl (CicSubstitution.lift 1 c2 :: mk_implicits (nc2 - sat2 - 1) @
-     Cic.Appl (CicSubstitution.lift 1 c1 :: mk_implicits nc1 ) ::
+   Cic.Appl ((*CicSubstitution.lift 1*) c2 :: mk_implicits (nc2 - sat2 - 1) @
+     Cic.Appl ((*CicSubstitution.lift 1*) c1 :: mk_implicits nc1 ) ::
      mk_implicits sat2)
   in
   let rec create_subst_from_metas_to_rels n = function 
@@ -205,8 +218,14 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
     let meta_to_be_coerced =
      try
       match List.nth l_c1 (c1_pis - sat1 - 1) with
-       | Cic.Meta (i,_) -> i
-       | _ -> assert false
+       | Cic.Meta (i,_) -> Some i
+       | t -> 
+          debug_print 
+            (lazy("meta_to_be_coerced: " ^ CicPp.ppterm t));
+          debug_print 
+            (lazy("c1_pis: " ^ string_of_int c1_pis ^ 
+             " sat1:" ^ string_of_int sat1));
+          None
      with
       Failure _ -> assert false
     in
@@ -230,15 +249,20 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       | (i,_,_)::_ when i = n -> acc
       | _::tl -> position_of n (acc + 1) tl
     in
-    debug_print
-     (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
-    let position_of_meta_to_be_coerced =
-     position_of meta_to_be_coerced 0 sorted in
-     debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
-      string_of_int position_of_meta_to_be_coerced));
-     debug_print (lazy ("SATURATIONS: " ^
-      string_of_int (List.length sorted - position_of_meta_to_be_coerced - 1)));
-     sorted, List.length sorted - position_of_meta_to_be_coerced - 1
+    let saturations_res = 
+      match meta_to_be_coerced with
+      | None -> 0
+      | Some meta_to_be_coerced -> 
+          debug_print
+            (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
+          let position_of_meta_to_be_coerced =
+            position_of meta_to_be_coerced 0 sorted in
+          debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
+            string_of_int position_of_meta_to_be_coerced));
+          List.length sorted - position_of_meta_to_be_coerced - 1
+    in
+    debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res));
+    sorted, saturations_res
   in
   let namer l n = 
     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
@@ -270,6 +294,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
         CicRefine.type_of_aux' metasenv context c univ
       in
       debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+      debug_print(lazy("COMPOSED REFINED (pretty): "^
+        CicMetaSubst.ppterm_in_context [] ~metasenv term context));
 (*       let metasenv = order_metasenv metasenv in *)
 (*       debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *)
       let body_metasenv, lambdas_metasenv = 
@@ -353,7 +379,7 @@ let filter_duplicates l coercions =
           try 
             List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
           with
-          | Invalid_argument "List.for_all2" -> false)
+          | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false)
         coercions))
   l
 
@@ -404,6 +430,7 @@ let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
+  debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
   let todo_list = filter_duplicates todo_list coercions in
   try
     let new_coercions = 
@@ -462,9 +489,9 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;;
 
 (* 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 sat2 =
+let generate_composite c1 c2 context metasenv univ sat1 sat2 =
  let a,b,c,_,_ =
-  generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ
+  generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c
 ;;