From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 13:06:43 +0000 (+0000) Subject: replace tactic reimplemented. X-Git-Tag: PRE_GETTER_STORAGE~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04cfb486c3fe1609839c6a435bc2db6d6cae581d;p=helm.git replace tactic reimplemented. It is now able to replace several terms at once. NOTE: it is still unable to replace terms in the hypotheses. --- diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index a07a06837..31c9b60b4 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -23,7 +23,6 @@ * http://cs.unibo.it/helm/. *) - let rewrite_tac ~direction ~pattern equality = let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status = @@ -118,7 +117,7 @@ let replace_tac ~pattern ~with_what = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let (_,context,_) as conjecture = CicUtil.lookup_meta goal metasenv in + let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) let context_len = List.length context in let _,selected_terms_with_context = @@ -155,43 +154,56 @@ let replace_tac ~pattern ~with_what = CicUniv.empty_ugraph in let b,u = CicReduction.are_convertible ~metasenv context ty_of_with_what ty_of_t_in_context u in - if b then t_in_context + 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 + t_in_context,pattern_for_t else raise (ProofEngineTypes.Fail "Replace: one of the selected terms and the term to be replaced with have not convertible types") - ) l - in - let rec aux whats status = - match whats with - [] -> ProofEngineTypes.apply_tactic T.id_tac status - | what::tl -> - ProofEngineTypes.apply_tactic - (T.thens - ~start:( - P.cut_tac - (C.Appl [ - (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ; - ty_of_with_what ; - what ; - with_what])) - ~continuations:[ - T.then_ - ~start:( - rewrite_simpl_tac ~direction:`LeftToRight ~pattern (C.Rel 1)) - ~continuation:( - let hyp = - try - match List.hd context with - Some (Cic.Name name,_) -> name - | _ -> assert false - with (Failure "hd") -> assert false - in - ProofEngineStructuralRules.clear ~hyp) ; - aux_tac tl]) - status - and aux_tac tl = ProofEngineTypes.mk_tactic (aux tl) in - aux whats status + ) l in + let rec aux n whats status = + match whats with + [] -> ProofEngineTypes.apply_tactic T.id_tac status + | (what,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 + ProofEngineTypes.apply_tactic + (T.thens + ~start:( + P.cut_tac + (C.Appl [ + (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ; + ty_of_with_what ; + what ; + with_what])) + ~continuations:[ + T.then_ + ~start:( + rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1)) + ~continuation:( + T.then_ + ~start:( + ProofEngineTypes.mk_tactic + (function ((proof,goal) as status) -> + let _,metasenv,_,_ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let hyp = + try + match List.hd context with + Some (Cic.Name name,_) -> name + | _ -> assert false + with (Failure "hd") -> assert false + in + ProofEngineTypes.apply_tactic + (ProofEngineStructuralRules.clear ~hyp) status)) + ~continuation:(aux_tac (n + 1) tl)); + T.id_tac]) + status + and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in + aux 0 whats status in ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what) ;;