new more flexible compose, see matita/tests/compose.ma for a sample

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

diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml
index f090c3dbfeb6504f15c7136ef505f414cc61df62..137e919b09fd98e6c5d6da3f5f155cd79b7850c6 100644 (file)
--- a/components/tactics/compose.ml
+++ b/components/tactics/compose.ml
@@ -23,30 +23,78 @@
  * http://helm.cs.unibo.it/
  *)
 
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) =
+let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
+
+let compose_core t2 t1 (proof, goal) =
   let _,metasenv,_subst,_,_,_ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let ty1,_ = 
     CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph 
   in
-  let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 in
-  let rec generate arity menv acc =
-    if arity < 0 then acc, menv
-    else
+  let ty2,_ = 
+    CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph 
+  in
+  let saturated_ty2, menv_for_saturated_ty2 = 
+    let maxm = CicMkImplicit.new_meta metasenv [] in
+    let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
+    ty2, menv
+  in
+  (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
+  let unif menv t = 
+    let m, menv2 =
+      let n = CicMkImplicit.new_meta menv [] in
+      let irl = 
+        CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+      Cic.Meta (n,irl), ((n,context,t)::menv)
+    in
+    try 
+      let _ = 
+        CicUnification.fo_unif menv context t saturated_ty2
+          CicUniv.oblivion_ugraph
+      in 
+        true, menv2, m
+    with
+    | CicUnification.UnificationFailure _
+    | CicUnification.Uncertain _ -> false, menv2, m
+  in
+  (* check which "positions" in the input arrow unifies with saturated_ty2 *)
+  let rec positions menv cur arity = 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))
+        else
+          positions newmenv (cur + 1) arity (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 *)
+  let rec generate positions menv acc =
+    match positions with
+    | [] -> acc, menv
+    | arity::tl ->
       try
-        let t, menv, _ =
-          CloseCoercionGraph.generate_composite t1 t2 context menv
+        let t, menv1, _ =
+          CloseCoercionGraph.generate_composite t2 t1 context menv
             CicUniv.oblivion_ugraph arity false
         in
-        generate (arity - 1) menv (t::acc)
+        assert (List.length menv1 = List.length menv);
+        generate tl menv (t::acc)
       with 
-      | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc
+      | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
+  in
+  let terms, metasenv =
+    generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
   in
-  let terms, metasenv = generate (count_pi ty1) metasenv [] in
+  (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
   let proof = 
     let uri, _, _subst, bo, ty, attrs = proof in
     uri, metasenv, _subst, bo, ty, attrs
   in
+  (* now we have the terms, we generalize them and intros them *)
   let proof, goal =
     List.fold_left 
       (fun (proof,goal) t ->
@@ -62,12 +110,64 @@ let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) =
         proof,List.hd gl)
       (proof,goal) terms
   in
-  ProofEngineTypes.apply_tactic 
-    (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
-    (proof,goal)
+  (proof, goal), List.length terms
+;;
+
+let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
+  let ((proof, goal), k), n = 
+    match t2 with
+    | Some t2 -> compose_core t1 t2 proofstatus, n-1
+    | None -> 
+        let k = 
+          let proof, goal = proofstatus in
+          let _,metasenv,subst,_,_,_ = proof in
+          let _,_,ty = CicUtil.lookup_meta goal metasenv in
+          count_pi (CicMetaSubst.apply_subst subst ty)
+        in
+        (proofstatus, k), n
+  in
+  let (proof, goal), k = 
+    (* fix iterates n times the composition *)
+    let rec fix proofstatus k t = function
+      | 0 -> proofstatus, k
+      | n ->
+          let t = CicSubstitution.lift k t in
+          let proof, gl =  
+            ProofEngineTypes.apply_tactic 
+              (PrimitiveTactics.intros_tac 
+                ~howmany:k ?mk_fresh_name_callback ()) proofstatus
+          in
+          assert (List.length gl = 1);
+          let goal = List.hd gl in
+          let k, proofstatus =
+            (* aux compose t with every previous result *)
+            let rec aux k proofstatus = function
+              | 0 -> k, proofstatus
+              | n -> 
+                 let (proof, goal), k1 = 
+                   compose_core t (Cic.Rel n) proofstatus 
+                 in
+                 aux (k+k1) (proof, goal) (n-1)
+            in
+              aux 0 (proof, goal) k
+          in
+          fix proofstatus k t (n-1)
+    in
+      fix (proof, goal) k t1 n
+  in
+  let howmany = 
+    match howmany with
+    | None -> None
+    | Some i ->
+        if i - k < 0 then (* we should generalize back and clear *) Some 0
+        else Some (i - k)
+  in
+     ProofEngineTypes.apply_tactic 
+      (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
+      (proof,goal)
 ;;
 
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 =
+let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
   ProofEngineTypes.mk_tactic 
-    (compose_tac ?howmany ?mk_fresh_name_callback t1 t2)
+    (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)
 ;;