]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/closeCoercionGraph.ml
compose tactic restore and added nocomposites keyword
[helm.git] / components / tactics / closeCoercionGraph.ml
index 898946ad64f6d89e77c0b18900644c55b0b8462c..7ed3c36e6b86d24d4a46b753a750e11597d919c0 100644 (file)
 
 (* $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 
- * of new coercions to create. hte list elements are
+ * of new coercions to create. the list elements are
  * (source, list of coercions to follow, target)
  *)
 let get_closure_coercions src tgt uri coercions =
-  let eq_carr s t = 
+  let enrich (uri,sat) tgt =
+   let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+    uri,sat,arity
+  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 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 
-          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+          (fun (_,t,ul) -> 
+             if eq_carr ~exact:true src t then [] else
+             List.map (fun u -> src,[uri; enrich u t],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,t,ul) -> 
+             if eq_carr ~exact:true s tgt then [] else
+             List.map (fun u -> s,[enrich u t; uri],tgt) ul) c_to_src) @
         (HExtlib.flatten_map 
-          (fun (s,_,u1l) ->
+          (fun (s,t1,u1l) ->
             HExtlib.flatten_map 
               (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
+                    then [] else
                     List.map 
-                      (fun u2 -> (s,[u1;uri;u2],t)) 
+                      (fun u2 -> (s,[enrich u1 t1;uri;enrich u2 t],t)) 
                       u2l)
                   u1l) 
               c_from_tgt) 
@@ -75,26 +101,31 @@ let obj_attrs n = [`Class (`Coercion n); `Generated]
 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 =
+   both living in the same context and metasenv
+
+    c2 ?p2 (c1 ?p1 ?x ?s1) ?s2
+
+    where:
+     ?pn + 1 + ?sn = count_pi n - arity n
+*)
+let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
   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
     | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
   in
-  let rec mk_lambda_spline c namer = function
+  let rec mk_lambda_spine c namer = function
     | 0 -> c
     | n -> 
         Cic.Lambda 
           (namer n,
            (Cic.Implicit None), 
-           mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1))
+           mk_lambda_spine (CicSubstitution.lift 1 c) namer (n-1))
   in 
-  let count_saturations_needed t arity = 
+  let count_pis t arity = 
     let rec aux acc n = function
-      | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> 
-          aux (acc@[name]) (n+1) t
+      | Cic.Prod (name,src,tgt) -> aux (acc@[name]) (n+1) tgt
       | _ -> n,acc
     in
     let len,names = aux [] 0 t in
@@ -104,36 +135,18 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       names
   in
   let compose c1 nc1 c2 nc2 =
-    Cic.Lambda 
-      (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])
-            ])))
+   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 order_metasenv metasenv = 
-    let module OT = struct type t = int let compare = Pervasives.compare end in
-    let module S = HTopoSort.Make (OT) in
-    let dep i = 
-      let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
-      let metas = List.map fst (CicUtil.metas_of_term ty) in
-      HExtlib.list_uniq (List.sort Pervasives.compare metas)
-    in
-    let om =  
-      S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep 
-    in
-    List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
-  in 
-*)
   let rec create_subst_from_metas_to_rels n = function 
     | [] -> []
     | (metano, ctx, ty)::tl -> 
-        (metano,(ctx,Cic.Rel (n+1),ty)) ::
+        (metano,(ctx,Cic.Rel n,ty)) ::
           create_subst_from_metas_to_rels (n-1) tl
   in
   let split_metasenv metasenv n =
-    List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
+    List.partition (fun (_,ctx,_) -> List.length ctx >= n) metasenv
   in
   let purge_unused_lambdas metasenv t =
     let rec aux = function
@@ -146,39 +159,110 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
     in
     aux t
   in
-  let order_body_menv term body_metasenv =
+  let order_body_menv term body_metasenv c1_pis c2_pis =
     let rec purge_lambdas = function
       | Cic.Lambda (_,_,t) -> purge_lambdas t
       | t -> t
     in
     let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+    let rec metas_of_term_and_types t =
+      let metas = CicUtil.metas_of_term t in
+      let types = 
+       List.flatten       
+        (List.map 
+          (fun (i,_) -> try 
+            let _,_,ty = CicUtil.lookup_meta i body_metasenv in metas_of_term_and_types ty
+            with CicUtil.Meta_not_found _ -> []) 
+          metas)
+      in
+      metas @ types
+    in
+    let sorted_metas_of_term world t = 
+      let metas = metas_of_term_and_types t in
+      (* this check should be useless *)
+      let metas = List.filter (fun (i,_)->List.exists (fun (j,_,_) -> j=i) world) metas in
+      let order_metas metasenv metas = 
+        let module OT = struct type t = int let compare = Pervasives.compare end in
+        let module S = HTopoSort.Make (OT) in
+        let dep i = 
+          try 
+            let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+            let metas = List.map fst (CicUtil.metas_of_term ty) in
+            HExtlib.list_uniq (List.sort Pervasives.compare metas)
+          with Not_found -> []
+        in
+          S.topological_sort (List.map (fun (i,_) -> i) metas) dep 
+      in 
+      order_metas world metas
+    in
     let metas_that_saturate l =
       List.fold_left 
         (fun (acc,n) t ->
-          let metas = CicUtil.metas_of_term t in
-          let metas = List.map fst metas in
+          let metas = sorted_metas_of_term body_metasenv t in
           let metas = 
-            List.filter 
-              (fun i -> List.for_all (fun (j,_) -> j<>i) acc) 
-              metas 
-          in
+            List.filter (fun i -> List.for_all (fun (j,_) -> j<>i) acc) metas in
           let metas = List.map (fun i -> i,n) metas in
           metas @ acc, n+1)
         ([],0) l
     in
     let l_c2 = skip_appl (purge_lambdas term) in
-    let l_c1 = 
-      match HExtlib.list_last l_c2 with
-      | Cic.Appl l -> List.tl l
-      | _ -> assert false
+    let l_c2_b,l_c2_a =
+     try
+      HExtlib.split_nth (c2_pis - sat2 - 1) l_c2
+     with
+      Failure _ -> assert false in
+    let l_c1,l_c2_a =
+     match l_c2_a with
+        Cic.Appl (_::l_c1)::tl -> l_c1,tl
+      | _ -> assert false in
+    let meta_to_be_coerced =
+     try
+      match List.nth l_c1 (c1_pis - sat1 - 1) with
+       | 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
-    (* i should cut off the laet elem of l_c2 *)
-    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
-    List.sort 
+    (* BIG HACK ORRIBLE:
+     * it should be (l_c2_b @ l_c1 @ l_c2_a), but in this case sym (eq_f) gets
+     *  \A,B,f,x,y,Exy and not \B,A,f,x,y,Exy
+     * as an orrible side effect, the other composites get a type lyke
+     *  \A,x,y,Exy,B,f with 2 saturations
+     *)
+    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2_b @ l_c2_a)) in
+    let sorted =
+     List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
           try List.assoc i meta2no -  List.assoc j meta2no 
           with Not_found -> assert false) 
       body_metasenv
+    in
+    let rec position_of n acc =
+     function
+        [] -> assert false
+      | (i,_,_)::_ when i = n -> acc
+      | _::tl -> position_of n (acc + 1) tl
+    in
+    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
@@ -196,28 +280,34 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   debug_print (lazy ("\nCOMPOSING"));
   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
-  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
-  let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
-  let spline_len = saturations_for_c1 + saturations_for_c2 in
-  let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
+  let c1_pis, names_c1 = count_pis c1_ty arity1 in 
+  let c2_pis, names_c2 = count_pis c2_ty arity2 in
+  let c = compose c1 c1_pis c2 c2_pis in
+  let spine_len = c1_pis + c2_pis in
+  let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
-  let c, metasenv, univ = 
+  let old_insert_coercions = !CicRefine.insert_coercions in
+  let c, metasenv, univ, saturationsres =
     try
+      CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
         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 = 
-        split_metasenv metasenv (spline_len + List.length context)
+        split_metasenv metasenv (spine_len + List.length context)
       in
       debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
       debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
-      let body_metasenv = order_body_menv term body_metasenv in
+      let body_metasenv, saturationsres =
+       order_body_menv term body_metasenv c1_pis c2_pis
+      in
       debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
-      let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+      let subst = create_subst_from_metas_to_rels spine_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
@@ -226,7 +316,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
         CicRefine.type_of_aux' metasenv context term ugraph
       in
       let body_metasenv, lambdas_metasenv = 
-        split_metasenv metasenv (spline_len + List.length context)
+        split_metasenv metasenv (spine_len + List.length context)
       in
       let lambdas_metasenv = 
         List.filter 
@@ -244,15 +334,23 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
               lambdas_metasenv) 
           metasenv 
       in
+      debug_print (lazy ("####################"));
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
-      debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
-      term, metasenv, ugraph
+      debug_print (lazy ("SATURATIONS: " ^ string_of_int saturationsres));
+      debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+      debug_print (lazy ("####################"));
+      CicRefine.insert_coercions := old_insert_coercions;
+      term, metasenv, ugraph, saturationsres
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
+        CicRefine.insert_coercions := old_insert_coercions;
         raise UnableToCompose
-  in  
-  c, metasenv, univ 
+    | exn ->
+        CicRefine.insert_coercions := old_insert_coercions;
+        raise exn
+  in
+  c, metasenv, univ, saturationsres, arity2
 ;;
 
 let build_obj c univ arity =
@@ -279,9 +377,9 @@ let filter_duplicates l coercions =
           CoercDb.eq_carr s src && 
           CoercDb.eq_carr t tgt &&
           try 
-            List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+            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
 
@@ -316,8 +414,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
@@ -328,10 +426,11 @@ 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 saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
-  let todo_list = get_closure_coercions src tgt uri coercions 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 = 
@@ -340,44 +439,45 @@ let close_coercion_graph src tgt uri baseuri =
           try 
             (match l with
             | [] -> assert false 
-            | he :: tl ->
-                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+            | (he,saturations1,arity1) :: tl ->
                 let first_step = 
                   Cic.Constant ("", 
-                    Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                    Cic.Sort Cic.Prop, [], obj_attrs arity)
+                   Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                    Cic.Sort Cic.Prop, [], obj_attrs arity1),
+                  saturations1,
+                  arity1
                 in
                 let o,_ = 
-                  List.fold_left (fun (o,univ) coer ->
+                  List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
                     match o with 
-                    | Cic.Constant (_,Some c,_,[],_) ->
-                        let t, menv, univ = 
-                          generate_composite c 
-                            (CoercDb.term_of_carr (CoercDb.Uri coer)
-                            [] [] univ arity true
+                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 ->
+                        let t, menv, univ, saturationsres, arityres = 
+                          generate_composite' (u,saturations1,arity1) 
+                            (CoercDb.term_of_carr (CoercDb.Uri coer),
+                             saturations2, arity2) [] [] univ
                         in
                         if (menv = []) then
-                          prerr_endline 
-                            "MENV non empty after composing coercions";
-                        build_obj t univ arity
+                          HLog.warn "MENV non empty after composing coercions";
+                        let o,univ = build_obj t univ arityres in
+                         (o,saturationsres,arityres),univ
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl
                 in
                 let name_src = CoercDb.name_of_carr src in
                 let name_tgt = CoercDb.name_of_carr tgt in
-                let by = List.map UriManager.name_of_uri l in
+                let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in
                 let name = mangle name_tgt name_src by in
                 let c_uri = 
                   number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_) -> u) acc) 
+                    (List.map (fun (_,_,u,_,_,_) -> u) acc) 
                 in
-                let named_obj = 
+                let named_obj,saturations,arity = 
                   match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs) ->
-                      Cic.Constant (name,bo,ty,vl,attrs)
+                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity ->
+                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity
                   | _ -> assert false 
                 in
-                  (src,tgt,c_uri,named_obj))::acc
+                  (src,tgt,c_uri,saturations,named_obj,arity))::acc
           with UnableToCompose -> acc
       ) [] todo_list
     in
@@ -386,3 +486,12 @@ let close_coercion_graph src tgt uri baseuri =
 ;;
 
 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 sat1 sat2 =
+ let a,b,c,_,_ =
+  generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
+ in
+  a,b,c
+;;