X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=e4520292df8b9a9e7c489c1cf1876d77caaefb0a;hb=e9e3089b886e88a07267743cae79d6a9cabdd3c3;hp=a07a06837afed5c07f52c86e3b67035addc5f5e0;hpb=0d0b78958d6198e157171b3590516666d568c85f;p=helm.git diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index a07a06837..e4520292d 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 = @@ -33,7 +32,6 @@ let rewrite_tac ~direction ~pattern equality = let module PER = ProofEngineReduction in 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 @@ -44,18 +42,19 @@ let rewrite_tac ~direction ~pattern equality = in let curi, metasenv, pbo, pty = proof 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 CicUniv.empty_ugraph in let eq_ind, ty, t1, t2 = 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_right_to_left HLO.Logic.eq_ind_URI HLO.Logic.eq_ind_r_URI,[]) + | C.Appl [C.MutInd (uri, 0, []); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> + let ind_uri = + if_right_to_left LibraryObjects.eq_ind_URI LibraryObjects.eq_ind_r_URI in - if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2) + let eq_ind = C.Const (ind_uri uri,[]) 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 = @@ -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 (LibraryObjects.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) ;; @@ -212,10 +224,10 @@ let symmetry_tac = let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) - when (U.eq uri HelmLibraryObjects.Logic.eq_URI) -> + when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac - ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))) + ~term: (C.Const (LibraryObjects.sym_eq_URI uri, []))) (proof,goal) | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") @@ -234,11 +246,11 @@ let transitivity_tac ~term = let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) - when (uri = HelmLibraryObjects.Logic.eq_URI) -> + when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (T.thens ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, []))) + ~term: (C.Const (LibraryObjects.trans_eq_URI uri, []))) ~continuations: [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]) status