various updates, removed proofs for now because they are the real bottleneck!!

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 52ea4054de21ae6c0b2d1525f36398c114517e6e..b9db6f705777eb9ae7acb09bace47a5cc6b1857c 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 = ProofEngineHelpers.select ~term:gty' ~pattern:path in
+            let subterms = 
+              List.fold_left (
+                fun acc (i, r) -> 
+                  let wanted = CicSubstitution.lift (List.length 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'
+   ProofEngineReduction.replace_lifting_csc 0
+    ~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,44 +107,45 @@ 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)
 ;;
 
-let replace_tac ~what ~with_what =
- let replace_tac ~what ~with_what status =
+let replace_tac ~pattern ~with_what =
+(*
+ let replace_tac ~pattern ~with_what status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -139,7 +169,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)) ;
@@ -150,6 +180,7 @@ let replace_tac ~what ~with_what =
       raise (ProofEngineTypes.Fail "Replace: empty context")
  in
    ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
+*) assert false
 ;;