X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=1a0fe31d05e77e6ccf3d42138ec1484fc811646c;hb=da3031c3a830df0aaab4f57b63689a1b20d7ab89;hp=82c339ae2b3d13381b6f1fee090eb1721f190fb9;hpb=36842ee77114d2fa896d7ffd2333c07cff22b053;p=helm.git diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 82c339ae2..1a0fe31d0 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -40,30 +40,27 @@ module LO = LibraryObjects module DTI = DoubleTypeInference module HEL = HExtlib -let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = - let _rewrite_tac status = +let rec rewrite ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status= assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in - let curi, metasenv, _subst, 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 match hyps_pat with he::(_::_ as tl) -> - PET.apply_tactic + PET.apply_tactic (T.then_ - (rewrite_tac ~direction - ~pattern:(None,[he],None) equality) - (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) - (S.lift 1 equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,[he],None) equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,tl,concl_pat) (S.lift 1 equality))) ) status | [_] as hyps_pat when concl_pat <> None -> - PET.apply_tactic + PET.apply_tactic (T.then_ - (rewrite_tac ~direction - ~pattern:(None,hyps_pat,None) equality) - (rewrite_tac ~direction ~pattern:(None,[],concl_pat) - (S.lift 1 equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,hyps_pat,None) equality)) + (PET.mk_tactic (rewrite ~direction + ~pattern:(None,[],concl_pat) (S.lift 1 equality))) ) status | _ -> let arg,dir2,tac,concl_pat,gty = @@ -89,13 +86,17 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = Some pat,gty | _::_ -> assert false in + let gsort,_ = + CicTypeChecker.type_of_aux' + metasenv ~subst context gty CicUniv.oblivion_ugraph + in let if_right_to_left do_not_change a b = match direction with | `RightToLeft -> if do_not_change then a else b | `LeftToRight -> if do_not_change then b else a in let ty_eq,ugraph = - CicTypeChecker.type_of_aux' metasenv context equality + CicTypeChecker.type_of_aux' metasenv ~subst context equality CicUniv.oblivion_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = TermUtil.saturate_term @@ -131,7 +132,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = (* now we always do as if direction was `LeftToRight *) let fresh_name = FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv' context C.Anonymous ~typ:ty in + ~subst metasenv' context C.Anonymous ~typ:ty in let lifted_t1 = S.lift 1 t1x in let lifted_gty = S.lift 1 gty in let lifted_conjecture = @@ -147,7 +148,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select - ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture + ~metasenv:metasenv' ~subst ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in let what,with_what = @@ -160,7 +161,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let t1 = CicMetaSubst.apply_subst subst t1 in let t2 = CicMetaSubst.apply_subst subst t2 in let ty = CicMetaSubst.apply_subst subst ty in - let pbo = CicMetaSubst.apply_subst subst pbo in + let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in let equality = CicMetaSubst.apply_subst subst equality in let abstr_gty = @@ -175,6 +176,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let metasenv',arg,newtyp = match arg with None -> + let fresh_meta = CicMkImplicit.new_meta metasenv' subst in let gty' = S.subst t2 abstr_gty in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -189,8 +191,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in try let (proof',goals) = - PET.apply_tactic - (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal) + PET.apply_tactic (tac ~term:exact_proof newtyp) + ((curi,metasenv',subst,pbo,pty, attrs),goal) in let goals = goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv @@ -198,18 +200,18 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = in (proof',goals) with (* FG: this should be PET.Fail _ *) - TC.TypeCheckerFailure _ -> - let msg = lazy "rewrite: nothing to rewrite" in + TC.TypeCheckerFailure m -> + let msg = lazy ("rewrite: "^ Lazy.force m) in raise (PET.Fail msg) - in - PET.mk_tactic _rewrite_tac +;; let rewrite_tac ~direction ~pattern equality names = let _, hyps_pat, _ = pattern in let froms = List.map fst hyps_pat in - let start = rewrite_tac ~direction ~pattern equality in + let start = PET.mk_tactic (rewrite ~direction ~pattern equality) in let continuation = PESR.rename ~froms ~tos:names in if names = [] then start else T.then_ ~start ~continuation +;; let rewrite_simpl_tac ~direction ~pattern equality names = T.then_ @@ -218,12 +220,11 @@ let rewrite_simpl_tac ~direction ~pattern equality names = (ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None)) - 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,_subst,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 = @@ -233,17 +234,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.oblivion_ugraph + ProofEngineHelpers.select ~subst ~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 pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in let pty = CicMetaSubst.apply_subst subst pty in - let status = (uri,metasenv,_subst,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.oblivion_ugraph in + metasenv ~subst context with_what CicUniv.oblivion_ugraph in let whats = match selected_terms_with_context with [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected")) @@ -269,9 +270,9 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = raise (ProofEngineTypes.Fail (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 + CicTypeChecker.type_of_aux' metasenv ~subst context t_in_context CicUniv.oblivion_ugraph in - let b,u = CicReduction.are_convertible ~metasenv context + let b,u = CicReduction.are_convertible ~metasenv ~subst context 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 @@ -301,13 +302,14 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~continuations:[ T.then_ ~start:( - rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) []) + rewrite_tac + ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) []) ~continuation:( T.then_ ~start:( ProofEngineTypes.mk_tactic (function ((proof,goal) as status) -> - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,_,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let hyps = try @@ -336,14 +338,14 @@ let reflexivity_tac = let symmetry_tac = let symmetry_tac (proof, goal) = - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,_,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when LibraryObjects.is_eq_URI uri -> ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac - ~term: (C.Const (LibraryObjects.sym_eq_URI uri, []))) + ~term:(C.Const (LibraryObjects.sym_eq_URI uri, []))) (proof,goal) | _ -> raise (ProofEngineTypes.Fail (lazy "Symmetry failed")) @@ -354,7 +356,7 @@ let symmetry_tac = let transitivity_tac ~term = let transitivity_tac ~term status = let (proof, goal) = status in - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,_,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])