added support for goal patterns

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 52ea4054de21ae6c0b2d1525f36398c114517e6e..e1a4c6849d1c8507043dc466bf1efacb20205992 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -22,11 +22,14 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
+ 
 
-let rewrite ~term:equality ?(direction=`Left) (proof,goal) =
+let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   let module C = Cic in
   let module U = UriManager in
   let module PET = ProofEngineTypes in
+  let module PER = ProofEngineReduction in
+  let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   let module HLO = HelmLibraryObjects in
   let if_left a b = 
@@ -53,10 +56,36 @@ let rewrite ~term:equality ?(direction=`Left) (proof,goal) =
   (* now we always do as if direction was `Left *)
   let gty' = CicSubstitution.lift 1 gty in
   let t1' = CicSubstitution.lift 1 t1 in
+  let eq_kind, what = 
+    match where with
+    | None  
+    | Some ([], None) ->   
+        PER.alpha_equivalence, [t1']
+    | Some (hp_paths, goal_path) -> 
+        assert (hp_paths = []); 
+        match goal_path with
+        | None -> assert false (* (==), [t1'] *)
+        | Some path -> 
+            let roots = CicUtil.select ~term:gty' ~context:path in
+            let subterms = 
+              List.fold_left (
+                fun acc (i, r) -> 
+                  let wanted = CicSubstitution.lift i t1' in
+                  PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc
+            ) [] roots
+            in
+            (==), subterms
+  in
+  let with_what = 
+    let rec aux = function 
+      | 0 -> []
+      | n -> C.Rel 1 :: aux (n-1)
+    in
+    aux (List.length what)
+  in
   let gty'' =
    ProofEngineReduction.replace_lifting
-    ~equality:ProofEngineReduction.alpha_equivalence
-    ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+    ~equality:eq_kind ~what ~with_what ~where:gty'
   in
   let gty_red = CicSubstitution.subst t2 gty'' in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -78,37 +107,37 @@ let rewrite ~term:equality ?(direction=`Left) (proof,goal) =
   (proof',[fresh_meta])
   
  
-let rewrite_tac ~term =
-  let rewrite_tac ~term status =
-    rewrite ~term ~direction:`Right status
+let rewrite_tac ?where ~term () =
+  let rewrite_tac ?where ~term status =
+    rewrite ?where ~term ~direction:`Right status
   in
-  ProofEngineTypes.mk_tactic (rewrite_tac ~term)
+  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
 
-let rewrite_simpl_tac ~term =
- let rewrite_simpl_tac ~term status =
+let rewrite_simpl_tac ?where ~term () =
+ let rewrite_simpl_tac ?where ~term status =
   ProofEngineTypes.apply_tactic
   (Tacticals.then_ 
-   ~start:(rewrite_tac ~term)
+   ~start:(rewrite_tac ?where ~term ())
    ~continuation:
-    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+     (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
    status
  in
    ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
 ;;
 
-let rewrite_back_tac ~term =
-  let rewrite_back_tac ~term status =
-    rewrite ~term ~direction:`Left status
+let rewrite_back_tac ?where ~term () =
+  let rewrite_back_tac ?where ~term status =
+    rewrite ?where ~term ~direction:`Left status
   in
-  ProofEngineTypes.mk_tactic (rewrite_back_tac ~term)
+  ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term)
 
-let rewrite_back_simpl_tac ~term =
- let rewrite_back_simpl_tac ~term status =
+let rewrite_back_simpl_tac ?where ~term () =
+ let rewrite_back_simpl_tac ?where ~term status =
   ProofEngineTypes.apply_tactic
    (Tacticals.then_ 
-    ~start:(rewrite_back_tac ~term)
+    ~start:(rewrite_back_tac ?where ~term ())
     ~continuation:
-     (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+     (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
    status
  in
   ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
@@ -139,7 +168,7 @@ let replace_tac ~what ~with_what =
                          with_what]))
              ~continuations:[            
               
-              T.then_     ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
+              T.then_     ~start:(rewrite_simpl_tac ~term:(C.Rel 1) ())
                           ~continuation:(
                                 ProofEngineStructuralRules.clear
                                                ~hyp:(List.hd context)) ;