X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;hp=2b2afae67772bc73fd657288691e046ea97bc1dd;hpb=dfbf84276e3183c190a6c7a59689324dccbaa6dc;p=helm.git diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 2b2afae67..b3dc1bb9e 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,55 +35,55 @@ 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 - let last_hyp_name_of_status (proof,goal) = - let curi, metasenv, pbo, pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - match context with - (Some (Cic.Name s,_))::_ -> s - | _ -> assert false - in + let dummy = "dummy" in Some arg,false, - (fun ~term -> + (fun ~term typ -> Tacticals.seq ~tactics: - [PT.letin_tac term; - PET.mk_tactic (fun status -> - PET.apply_tactic - (ProofEngineStructuralRules.clearbody - (last_hyp_name_of_status status)) status); - PET.mk_tactic (fun status -> - let hyp = last_hyp_name_of_status status in - PET.apply_tactic - (ReductionTactics.simpl_tac - ~pattern: - (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None)) - status); - ProofEngineStructuralRules.clear name; - PET.mk_tactic (fun status -> - let hyp = last_hyp_name_of_status status in - PET.apply_tactic - (ProofEngineStructuralRules.rename hyp name) status) + [ProofEngineStructuralRules.rename name dummy; + PT.letin_tac + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term; + ProofEngineStructuralRules.clearbody name; + ReductionTactics.change_tac + ~pattern: + (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 @@ -123,7 +125,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 @@ -147,23 +153,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 @@ -171,7 +178,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 = @@ -187,8 +194,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 @@ -241,7 +249,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 @@ -251,7 +259,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 @@ -267,7 +275,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:(