The rewrite_* set of tactics is now working again. However, as before,

they do not work yet when the user asks to rewrite somethign also in the
hypotheses.

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 5bbfa33a6f3d27fb04ee3f39401bf5c165e933f5..93606201c501dd332d6eec06d4207e9d0ae75ec7 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -25,8 +25,8 @@
  
 
 let rewrite_tac ~direction ~pattern equality =
- let rewrite_tac ~direction ~pattern equality status =
-(*
+ let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
+ =
   let module C = Cic in
   let module U = UriManager in
   let module PET = ProofEngineTypes in
@@ -34,14 +34,16 @@ let rewrite_tac ~direction ~pattern equality =
   let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   let module HLO = HelmLibraryObjects in
+  assert (wanted = None);   (* this should be checked syntactically *)
+  assert (hyps_pat = []); (*CSC: not implemented yet! *)
   let proof,goal = status in
-  let if_left a b = 
+  let if_right_to_left a b = 
     match direction with
-    | `Right -> b
-    | `Left -> a
+    | `RightToLeft -> a
+    | `LeftToRight -> b
   in
   let curi, metasenv, pbo, pty = proof in
-  let metano, context, gty = CicUtil.lookup_meta goal metasenv in
+  let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let eq_uri = HLO.Logic.eq_URI in
   let ty_eq,_ = 
     CicTypeChecker.type_of_aux' metasenv context equality 
@@ -51,54 +53,37 @@ let rewrite_tac ~direction ~pattern equality =
     match ty_eq with
     | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] when U.eq uri eq_uri ->
         let eq_ind = 
-          C.Const (if_left HLO.Logic.eq_ind_URI HLO.Logic.eq_ind_r_URI,[])
+          C.Const (if_right_to_left HLO.Logic.eq_ind_URI HLO.Logic.eq_ind_r_URI,[])
         in
-        if_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2)
-    | _ -> raise (PET.Fail "Rewrite: argument is not a proof of an equality")
-  in
-  (* 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_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
-  let irl =CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let metasenv' = (fresh_meta,context,gty_red)::metasenv in
+        if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2)
+    | _ -> raise (PET.Fail "Rewrite: argument is not a proof of an equality") in
+  (* now we always do as if direction was `LeftToRight *)
   let fresh_name = 
     FreshNamesGenerator.mk_fresh_name 
-    ~subst:[] metasenv context C.Anonymous ~typ:ty
-  in
-  let pred = C.Lambda (fresh_name, ty, gty'') in
+    ~subst:[] metasenv context C.Anonymous ~typ:ty in
+  let lifted_t1 = CicSubstitution.lift 1 t1 in
+  let lifted_gty = CicSubstitution.lift 1 gty in
+  let lifted_conjecture =
+    metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
+  let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in
+  let _,selected_terms_with_context =
+   ProofEngineHelpers.select
+    ~metasenv ~conjecture:lifted_conjecture ~pattern:lifted_pattern in
+  let what,with_what = 
+   (* Note: Rel 1 does not live in the context context_of_t           *)
+   (* The replace_lifting_csc_0 function will take care of lifting it *)
+   (* to context_of_t                                                 *)
+   List.fold_right
+    (fun (context_of_t,t) (l1,l2) -> t::l1, Cic.Rel 1::l2)
+    selected_terms_with_context ([],[]) in
+  let abstr_gty =
+   ProofEngineReduction.replace_lifting_csc 0
+    ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+  let gty' = CicSubstitution.subst t2 abstr_gty in
+  let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let metasenv' = (fresh_meta,context,gty')::metasenv in
+  let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]
   in
@@ -108,16 +93,15 @@ let rewrite_tac ~direction ~pattern equality =
   in
   assert (List.length goals = 0) ;
   (proof',[fresh_meta])
-  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
-*) assert false in
- ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
+ in
+  ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
   
  
 let rewrite_simpl_tac ~direction ~pattern equality =
  let rewrite_simpl_tac ~direction ~pattern equality status =
   ProofEngineTypes.apply_tactic
   (Tacticals.then_ 
-   ~start:(rewrite_tac ~direction:`LeftToRight ~pattern equality)
+   ~start:(rewrite_tac ~direction ~pattern equality)
    ~continuation:
      (ReductionTactics.simpl_tac
        ~pattern:(ProofEngineTypes.conclusion_pattern None)))