X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=47f422f52dbbd0c3801784314334dc0b83cc9822;hb=3c46776d941312a0faa2e0ae2e112dd76242b6c9;hp=f284a2d1d145dbdb6d2c49c6885098ae19904e9c;hpb=e436c170ce2b9154d3e090c2140e8a0172f4a016;p=helm.git diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index f284a2d1d..47f422f52 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -44,7 +44,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let _rewrite_tac status = assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in - let curi, metasenv, pbo, pty, attrs = proof in + let curi, metasenv, _subst, pbo, pty, attrs = proof in let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in let gsort,_ = CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in @@ -104,7 +104,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in let ty_eq,ugraph = CicTypeChecker.type_of_aux' metasenv context equality - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in @@ -174,6 +174,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let abstr_gty = ProofEngineReduction.replace_lifting_csc 0 ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in + if lifted_gty = abstr_gty then + raise (ProofEngineTypes.Fail (lazy "nothing to do")); let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in let pred = C.Lambda (fresh_name, ty, abstr_gty) in (* The argument is either a meta if we are rewriting in the conclusion @@ -196,7 +198,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = try let (proof',goals) = PET.apply_tactic - (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty, attrs),goal) + (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal) in let goals = goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv @@ -229,7 +231,7 @@ 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 uri,metasenv,pbo,pty, attrs = proof in + let uri,metasenv,_subst,pbo,pty, attrs = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) let eq_URI = @@ -239,17 +241,17 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = in let context_len = List.length context in let subst,metasenv,u,_,selected_terms_with_context = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let with_what, metasenv, u = with_what context metasenv u in let with_what = CicMetaSubst.apply_subst subst with_what in let pbo = CicMetaSubst.apply_subst subst pbo in let pty = CicMetaSubst.apply_subst subst pty in - let status = (uri,metasenv,pbo,pty, attrs),goal in + let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in let ty_of_with_what,u = CicTypeChecker.type_of_aux' - metasenv context with_what CicUniv.empty_ugraph in + metasenv context with_what CicUniv.oblivion_ugraph in let whats = match selected_terms_with_context with [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected")) @@ -276,7 +278,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = (lazy "Replace: one of the selected terms is not closed")) in let ty_of_t_in_context,u = (* TASSI: FIXME *) CicTypeChecker.type_of_aux' metasenv context t_in_context - CicUniv.empty_ugraph in + CicUniv.oblivion_ugraph in let b,u = CicReduction.are_convertible ~metasenv context ty_of_with_what ty_of_t_in_context u in if b then @@ -288,7 +290,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = (ProofEngineTypes.Fail (lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types")) ) l in - let rec aux n whats status = + let rec aux n whats (status : ProofEngineTypes.status) = match whats with [] -> ProofEngineTypes.apply_tactic T.id_tac status | (what,lazy_pattern)::tl -> @@ -313,7 +315,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~start:( ProofEngineTypes.mk_tactic (function ((proof,goal) as status) -> - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let hyps = try @@ -328,7 +330,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = T.id_tac]) status and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in - aux 0 whats status + aux 0 whats (status : ProofEngineTypes.status) in ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what) ;; @@ -342,7 +344,7 @@ let reflexivity_tac = let symmetry_tac = let symmetry_tac (proof, goal) = - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) @@ -360,7 +362,7 @@ let symmetry_tac = let transitivity_tac ~term = let transitivity_tac ~term status = let (proof, goal) = status in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])