compose tactic restore and added nocomposites keyword

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

diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml
index 317030404d12acd322676fd91e56cf05b3fe79c5..6bc3dd0fa2160dac8117a9d64f52f94f4a1870b2 100644 (file)
--- a/components/tactics/compose.ml
+++ b/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 =
@@ -64,22 +85,23 @@ let compose_core t2 t1 (proof, goal) =
         let b, newmenv, sb = unif menv s in
         if b then
           (saturations - cur - 1) :: 
-            (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
+            (positions newmenv (cur + 1) saturations 
+             (CicSubstitution.subst sb t))
         else
           positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
     | _ -> []
   in
-  (* 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 *)
+  (* 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
-    | saturations::tl ->
+    | saturations_t1::tl ->
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph saturations
+            CicUniv.oblivion_ugraph saturations_t2 saturations_t1
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)