From: Andrea Asperti Date: Thu, 15 Jun 2006 09:38:08 +0000 (+0000) Subject: added applyS X-Git-Tag: 0.4.95@7852~1314 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb64f05e45f500e0929b8d89acfa590ddaa82e2b;p=helm.git added applyS --- diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index a9505d739..9f54c6cec 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -354,3 +354,115 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation in ProofEngineTypes.mk_tactic (auto_tac dbd) ;; + +(********************** applyS *******************) + +let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = + let (consthead,newmetasenv,arguments,_) = + ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in + let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in + let proof',metasenv = + let (puri,metasenv,pbo,pty) = proof in + (puri,newmetasenv,pbo,pty),metasenv + in + let proof'',goals = + match LibraryObjects.eq_URI () with + | Some uri -> + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) + ~continuation: + (PrimitiveTactics.cut_tac + (CicSubstitution.lift 1 + (Cic.Appl + [Cic.MutInd (uri,0,[]); + Cic.Sort Cic.Prop; + consthead; + ty])))) (proof',goal) + | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) + in + match goals with + [g1;g2] -> + let proof'',goals = + ProofEngineTypes.apply_tactic + (auto_tac ~paramodulation:"qualsiasi" ~dbd ()) (proof'',g2) + in + let proof'',goals = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) + ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) + ) (proof'',g1) + in + proof'', + (*CSC: Brrrr.... *) + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:(let _,m,_,_ = proof'' in m) + | _ -> assert false + +let rec count_prods context ty = + match CicReduction.whd context ty with + Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + +let applyS_tac ~dbd ~term (proof, goal) = + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic in + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in + let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = + match term with + C.Var (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Var (uri,exp_named_subst') + | C.Const (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | _ -> [],newmeta,[],term + in + let metasenv' = metasenv@newmetasenvfragment in + let termty,_ = + CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph + in + let termty = + CicSubstitution.subst_vars exp_named_subst_diff termty in + let goal_arity = count_prods context ty in + let res = + new_metasenv_and_unify_and_t dbd proof goal + newmeta' metasenv' context term' ty termty goal_arity + in + res + +let applyS_tac ~dbd ~term = + ProofEngineTypes.mk_tactic + (fun status -> + try applyS_tac ~dbd ~term status + with + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (ProofEngineTypes.Fail msg)) diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli index fe72629f0..207011648 100644 --- a/components/tactics/autoTactic.mli +++ b/components/tactics/autoTactic.mli @@ -29,3 +29,4 @@ val auto_tac: dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic +val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 4d5272589..327256b3d 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -27,6 +27,7 @@ let absurd = NegationTactics.absurd_tac let apply = PrimitiveTactics.apply_tac +let applyS = AutoTactic.applyS_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac let change = ReductionTactics.change_tac diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 67127e640..06b62911c 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,6 +1,7 @@ (* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic +val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : ?depth:int ->