X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=8304d7bb19264738127e76f6409988d69ab14934;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=20dede31e902f3dc94d0a5c7aded2ecfac7f893a;hpb=da3c6e228c3c7ec75c8fd80e8fd7846327eb1b39;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 20dede31e..8304d7bb1 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -22,9 +22,11 @@
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
  *)
+
+(* $Id$ *)
  
-let rewrite_tac ~direction ~pattern equality =
- let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
+let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
+ let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
  =
   let module C = Cic in
   let module U = UriManager in
@@ -33,21 +35,35 @@ let rewrite_tac ~direction ~pattern equality =
   let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   assert (wanted = None);   (* this should be checked syntactically *)
-  (*assert (hyps_pat = []); (*CSC: not implemented yet! *)*)
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
-  let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
+  match hyps_pat with
+     he::(_::_ as tl) ->
+       PET.apply_tactic
+        (Tacticals.then_
+          (rewrite_tac ~direction
+           ~pattern:(None,[he],None) equality)
+          (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
+        ) status
+   | [_] as hyps_pat when concl_pat <> None ->
+       PET.apply_tactic
+        (Tacticals.then_
+          (rewrite_tac ~direction
+           ~pattern:(None,hyps_pat,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
+      [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty
     | [name,pat] ->
-      (*CSC: bug here; I am ignoring the concl_pat *)
       let rec find_hyp n =
        function
           [] -> assert false
         | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
            Cic.Rel n, CicSubstitution.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet!*)
+        | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet! But does this make any sense?*)
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in
@@ -60,20 +76,21 @@ let rewrite_tac ~direction ~pattern equality =
        in
         let dummy = "dummy" in
         Some arg,false,
-         (fun ~term ->
+         (fun ~term typ ->
            Tacticals.seq
             ~tactics:
               [ProofEngineStructuralRules.rename name dummy;
                PT.letin_tac
                 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
                ProofEngineStructuralRules.clearbody name;
-               ReductionTactics.simpl_tac
+               ReductionTactics.change_tac
                 ~pattern:
-                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None);
+                  (None,[name,Cic.Implicit (Some `Hole)], None)
+                (ProofEngineTypes.const_lazy_term typ);
                ProofEngineStructuralRules.clear dummy
               ]),
-         pat,gty
-    | _ -> assert false (*CSC: not implemented yet!*)
+         Some pat,gty
+    | _::_ -> assert false
   in
   let if_right_to_left do_not_change a b = 
     match direction with
@@ -115,7 +132,11 @@ let rewrite_tac ~direction ~pattern equality =
   let lifted_conjecture =
     metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
   let lifted_pattern =
-    Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat
+    let lifted_concl_pat =
+      match concl_pat with
+      | None -> None
+      | Some term -> Some (CicSubstitution.lift 1 term) in
+    Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat
   in
   let subst,metasenv',ugraph,_,selected_terms_with_context =
    ProofEngineHelpers.select
@@ -139,23 +160,24 @@ let rewrite_tac ~direction ~pattern equality =
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   (* The argument is either a meta if we are rewriting in the conclusion
      or the hypothesis if we are rewriting in an hypothesis *)
-  let metasenv',arg =
+  let metasenv',arg,newtyp =
    match arg with
       None ->
        let gty' = CicSubstitution.subst t2 abstr_gty in
        let irl =
         CicMkImplicit.identity_relocation_list_for_metavariable context in
        let metasenv' = (fresh_meta,context,gty')::metasenv' in
-        metasenv', C.Meta (fresh_meta,irl)
+        metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
     | Some arg ->
-       metasenv,arg
+       let gty' = CicSubstitution.subst t1 abstr_gty in
+        metasenv,arg,gty'
   in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]
   in
   let (proof',goals) =
     PET.apply_tactic 
-      (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
+      (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal)
   in
   let goals =
    goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
@@ -163,7 +185,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 =
@@ -179,8 +201,9 @@ let rewrite_simpl_tac ~direction ~pattern equality =
    ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
 ;;
 
-let replace_tac ~pattern ~with_what =
- let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status =
+let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
+ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
+  let _wanted, hyps_pat, concl_pat = pattern in
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -233,7 +256,7 @@ let replace_tac ~pattern ~with_what =
           ty_of_with_what ty_of_t_in_context u in
          if b then
           let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
-          let pattern_for_t = None,[],concl_pat_for_t in
+          let pattern_for_t = None,[],Some concl_pat_for_t in
            t_in_context,pattern_for_t
          else
           raise
@@ -243,7 +266,7 @@ let replace_tac ~pattern ~with_what =
   let rec aux n whats status =
    match whats with
       [] -> ProofEngineTypes.apply_tactic T.id_tac status
-    | (what,pattern)::tl ->
+    | (what,lazy_pattern)::tl ->
        let what = CicSubstitution.lift n what in
        let with_what = CicSubstitution.lift n with_what in
        let ty_of_with_what = CicSubstitution.lift n ty_of_with_what in
@@ -259,7 +282,7 @@ let replace_tac ~pattern ~with_what =
             ~continuations:[            
               T.then_
                 ~start:(
-                  rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+                  rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
                  ~continuation:(
                    T.then_
                     ~start:(