"Parallel" rewriting in a list of hypothesis and in the conclusion is now

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 2b2afae67772bc73fd657288691e046ea97bc1dd..e519827f22918328784e7e15a4a6b97a515d6546 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -23,8 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
  
-let rewrite_tac ~direction ~pattern equality =
- let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
+let rec rewrite_tac ~direction ~pattern equality =
+ let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
  =
   let module C = Cic in
   let module U = UriManager in
@@ -37,6 +37,22 @@ let rewrite_tac ~direction ~pattern equality =
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
   let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  match hyps_pat with
+     he::(_::_ as tl) ->
+       PET.apply_tactic
+        (Tacticals.then_
+          (rewrite_tac ~direction
+           ~pattern:(None,[he],Cic.Implicit None) equality)
+          (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
+        ) status
+   | [_] as hyps_pat when concl_pat <> Cic.Implicit None ->
+       PET.apply_tactic
+        (Tacticals.then_
+          (rewrite_tac ~direction
+           ~pattern:(None,hyps_pat,Cic.Implicit None) equality)
+          (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
+        ) status
+   | _ ->
   let arg,dir2,tac,concl_pat,gty =
    match hyps_pat with
       [] -> None,true,PT.exact_tac,concl_pat,gty
@@ -58,30 +74,22 @@ let rewrite_tac ~direction ~pattern equality =
             (Some (Cic.Name s,_))::_ -> s
           | _ -> assert false
        in
+        let dummy = "dummy" in
         Some arg,false,
          (fun ~term ->
            Tacticals.seq
             ~tactics:
-              [PT.letin_tac term;
-               PET.mk_tactic (fun status ->
-                PET.apply_tactic
-                 (ProofEngineStructuralRules.clearbody
-                   (last_hyp_name_of_status status)) status);
-               PET.mk_tactic (fun status ->
-                let hyp = last_hyp_name_of_status status in
-                 PET.apply_tactic
-                  (ReductionTactics.simpl_tac
-                    ~pattern:
-                      (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None))
-                  status);
-               ProofEngineStructuralRules.clear name;
-               PET.mk_tactic (fun status ->
-                let hyp = last_hyp_name_of_status status in
-                 PET.apply_tactic
-                  (ProofEngineStructuralRules.rename hyp name) status)
+              [ProofEngineStructuralRules.rename name dummy;
+               PT.letin_tac
+                ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
+               ProofEngineStructuralRules.clearbody name;
+               ReductionTactics.simpl_tac
+                ~pattern:
+                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None);
+               ProofEngineStructuralRules.clear dummy
               ]),
          pat,gty
-    | _ -> assert false (*CSC: not implemented yet!*)
+    | _::_ -> assert false
   in
   let if_right_to_left do_not_change a b = 
     match direction with
@@ -171,7 +179,7 @@ let rewrite_tac ~direction ~pattern equality =
   in
    (proof',goals)
  in
-  ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
+  ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
   
  
 let rewrite_simpl_tac ~direction ~pattern equality =