X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcompose.ml;h=e009010a7648980a9d979df0bd65b7edc781adc4;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=cd355dc2785049d44dd78630401ea1884a052087;hpb=1f6aab137983a515b3ba4bb1d1efe0c9e22e889e;p=helm.git

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index cd355dc27..e009010a7 100644
--- a/helm/software/components/tactics/compose.ml
+++ b/helm/software/components/tactics/compose.ml
@@ -23,6 +23,11 @@
  * http://helm.cs.unibo.it/
  *)
 
+let debug = false;;
+let debug_print = 
+  if not debug then (fun _ -> ()) else (fun s -> prerr_endline (Lazy.force s))
+;;
+
 let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
 
 let compose_core t2 t1 (proof, goal) =
@@ -34,11 +39,27 @@ let compose_core t2 t1 (proof, goal) =
   let ty2,_ = 
     CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph 
   in
-  let saturated_ty2, menv_for_saturated_ty2 = 
+  let saturated_ty2, menv_for_saturated_ty2, args_t2 = 
     let maxm = CicMkImplicit.new_meta metasenv [] in
-    let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
-    ty2, menv
+    let ty2, menv, args, _ = 
+      TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in
+    ty2, menv, args
+  in
+  let saturations_t2 = 
+    let rec aux n = function 
+      | Cic.Meta (i,_)::tl -> 
+          let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in
+          if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop)
+            CicUniv.oblivion_ugraph) 
+          then n else aux (n+1) tl
+      | _::tl -> aux (n+1) tl
+      | [] -> n+1
+    in
+      List.length args_t2 - aux 0 args_t2 +1
   in
+  debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context
+    [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^
+    " saturations_t2:" ^ string_of_int saturations_t2));
   (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
   let unif menv t = 
     let m, menv2 =
@@ -59,27 +80,28 @@ let compose_core t2 t1 (proof, goal) =
     | CicUnification.Uncertain _ -> false, menv2, m
   in
   (* check which "positions" in the input arrow unifies with saturated_ty2 *)
-  let rec positions menv cur arity = function 
+  let rec positions menv cur saturations = function 
     | Cic.Prod (n,s,t) -> 
         let b, newmenv, sb = unif menv s in
         if b then
-          (arity - cur - 1) :: 
-            (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
+          (saturations - cur - 1) :: 
+            (positions newmenv (cur + 1) saturations 
+             (CicSubstitution.subst sb t))
         else
-          positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
+          positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
     | _ -> []
   in
-  (* position is a list of arities, that is if t1 : a -> b -> c and arity is
-   * 0 then the computed term will be (t1 ? t2) of type a -> c
-   * if arity is 1 then (t1 t2 ?) of type b -> c *)
+  (* position is a list of arities, that is if t1 : a -> b -> c and saturations
+   * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations
+   * is 1 then (t1 t2 ?) of type b -> c *)
   let rec generate positions menv acc =
     match positions with
     | [] -> acc, menv
-    | arity::tl ->
+    | saturations_t1::tl ->
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph arity
+            CicUniv.oblivion_ugraph saturations_t2 saturations_t1
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)
@@ -103,7 +125,7 @@ let compose_core t2 t1 (proof, goal) =
         in
         let proof, gl = 
           ProofEngineTypes.apply_tactic
-            (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
+            (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None))
             (proof,goal)
         in
         assert(List.length gl = 1);