]> matita.cs.unibo.it Git - helm.git/commitdiff
1. composition of coercions with saturations > 0 is now implemented
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Sep 2007 09:39:56 +0000 (09:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Sep 2007 09:39:56 +0000 (09:39 +0000)
2. as a side effect, there is no longer any difference between composition
   of coercions and the compose tactic

TODO: composition of coercions having arity > 0 is not implemented yet

helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/closeCoercionGraph.mli
helm/software/components/tactics/compose.ml

index 0ab937ace0a89b6643034a21936cdc9242d31af4..68e4e7cb2c2b2c176e274e76b6257ea7e09cf2a0 100644 (file)
@@ -29,13 +29,13 @@ 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 eq_carr ?exact s t = 
     try
-      CoercDb.eq_carr s t
+      CoercDb.eq_carr ?exact s t
     with
     | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
   in
@@ -53,11 +53,11 @@ let get_closure_coercions src tgt uri coercions =
       in
         (HExtlib.flatten_map 
           (fun (_,t,ul) -> 
-             if CoercDb.eq_carr ~exact:true src t then [] else
+             if 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) -> 
-             if CoercDb.eq_carr ~exact:true s tgt then [] else
+             if 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) ->
@@ -65,7 +65,10 @@ let get_closure_coercions src tgt uri coercions =
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
                   (fun u1 ->
-                    if CoercDb.eq_carr ~exact:true s t then [] else
+                    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)) 
                       u2l)
@@ -81,12 +84,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,sat1) (c2,sat2) context metasenv univ arity
- last_lam_with_inn_arg
-=
-assert (sat1 = 0);
-assert (sat2 = 0);
-let saturationsres = 0 in
+let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity =
   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
@@ -101,10 +99,9 @@ let saturationsres = 0 in
            (Cic.Implicit None), 
            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
@@ -114,36 +111,18 @@ let saturationsres = 0 in
       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
@@ -156,7 +135,7 @@ let saturationsres = 0 in
     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
@@ -168,27 +147,52 @@ let saturationsres = 0 in
           let metas = CicUtil.metas_of_term t in
           let metas = List.map fst metas 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,_) -> i
+       | _ -> assert false
+     with
+      Failure _ -> assert false
     in
-    (* i should cut off the last elem of l_c2 *)
-    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
-    List.sort 
+    let meta2no = fst (metas_that_saturate (l_c2_b @ l_c1 @ 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
+    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
   in
   let namer l n = 
     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
@@ -206,14 +210,14 @@ let saturationsres = 0 in
   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 spine_len = saturations_for_c1 + saturations_for_c2 in
+  let c1_pis, names_c1 = count_pis c1_ty 0 in 
+  let c2_pis, names_c2 = count_pis c2_ty arity 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 old_insert_coercions = !CicRefine.insert_coercions in
-  let c, metasenv, univ = 
+  let c, metasenv, univ, saturationsres =
     try
       CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
@@ -227,7 +231,9 @@ let saturationsres = 0 in
       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 spine_len body_metasenv in
       debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
@@ -256,10 +262,13 @@ let saturationsres = 0 in
               lambdas_metasenv) 
           metasenv 
       in
+      debug_print (lazy ("####################"));
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
-      debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+      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
+      term, metasenv, ugraph, saturationsres
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
@@ -268,7 +277,7 @@ let saturationsres = 0 in
     | exn ->
         CicRefine.insert_coercions := old_insert_coercions;
         raise exn
-  in  
+  in
   c, metasenv, univ, saturationsres
 ;;
 
@@ -371,8 +380,7 @@ let close_coercion_graph src tgt uri saturations baseuri =
                         let t, menv, univ, saturationsres = 
                           generate_composite' (u,saturations1) 
                             (CoercDb.term_of_carr (CoercDb.Uri coer),
-                             saturations) 
-                            [] [] univ arity true
+                             saturations) [] [] univ arity
                         in
                         if (menv = []) then
                           HLog.warn "MENV non empty after composing coercions";
@@ -407,9 +415,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 arity =
+let generate_composite c1 c2 context metasenv univ arity =
  let a,b,c,_ =
-  generate_composite' (c1,0) (c2,0) context metasenv univ arity b
+  generate_composite' (c1,0) (c2,0) context metasenv univ arity
  in
   a,b,c
 ;;
index 1acea0eebda80bf37a24585ea78933b47dcb6a9f..baf926ff156e37d1d685a7a38c54e6127eeaed03 100644 (file)
@@ -36,5 +36,4 @@ exception UnableToCompose
 val generate_composite:
   Cic.term -> Cic.term -> Cic.context -> 
   Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> 
-    bool (* last lambda goes with innermost arg *) ->
     Cic.term * Cic.metasenv * CicUniv.universe_graph
index 137e919b09fd98e6c5d6da3f5f155cd79b7850c6..cd355dc2785049d44dd78630401ea1884a052087 100644 (file)
@@ -79,7 +79,7 @@ let compose_core t2 t1 (proof, goal) =
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph arity false
+            CicUniv.oblivion_ugraph arity
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)