From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 12:30:45 +0000 (+0000) Subject: * the auto AST now has the width X-Git-Tag: INDEXING_NO_PROOFS~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=842919f2f8ee71a5301ad962220569450340a9e9;p=helm.git * the auto AST now has the width * a bit of code clean-up * more tactics made available to matita --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 18f89c504..16c3f0a48 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -23,25 +23,36 @@ let tactic_of_ast = function | TacticAst.Absurd (_, term) -> Tactics.absurd term | TacticAst.Apply (_, term) -> Tactics.apply term | TacticAst.Assumption _ -> Tactics.assumption - | TacticAst.Auto (_,depth) -> - AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) () + | TacticAst.Auto (_,depth,width) -> + AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what | TacticAst.Contradiction _ -> Tactics.contradiction | TacticAst.Compare (_, term) -> Tactics.compare term | TacticAst.Constructor (_, n) -> Tactics.constructor n | TacticAst.Cut (_, term) -> Tactics.cut term | TacticAst.DecideEquality _ -> Tactics.decide_equality + | TacticAst.Decompose (_,term) -> Tactics.decompose term | TacticAst.Discriminate (_,term) -> Tactics.discriminate term | TacticAst.Elim (_, term, _) -> Tactics.elim_intros term | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Exists _ -> Tactics.exists + | TacticAst.Fold (_, reduction_kind ,term) -> + let reduction = + match reduction_kind with + | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] + | `Reduce -> ProofEngineReduction.reduce + | `Simpl -> ProofEngineReduction.simpl + | `Whd -> CicReduction.whd ~delta:false ~subst:[] + in + Tactics.fold ~reduction ~also_in_hypotheses:false ~term | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.FwdSimpl (_, term) -> Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat | TacticAst.Goal (_, n) -> Tactics.set_goal n + | TacticAst.Injection (_,term) -> Tactics.injection term | TacticAst.Intros (_, None, names) -> PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Intros (_, Some num, names) -> @@ -370,16 +381,27 @@ let disambiguate_tactic status = function let status, cic = disambiguate_term status term in status, TacticAst.Absurd (loc, cic) | TacticAst.Assumption loc -> status, TacticAst.Assumption loc - | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) + | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width) | TacticAst.Change (loc, what, with_what, pattern) -> let status, cic1 = disambiguate_term status what in let status, cic2 = disambiguate_term status with_what in let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Change (loc, cic1, cic2, pattern) - | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc + | TacticAst.Compare (loc,term) -> + let status, term = disambiguate_term status term in + status, TacticAst.Compare (loc,term) + | TacticAst.Constructor (loc,n) -> + status, TacticAst.Constructor (loc,n) + | TacticAst.Contradiction loc -> + status, TacticAst.Contradiction loc | TacticAst.Cut (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Cut (loc, cic) + | TacticAst.DecideEquality loc -> + status, TacticAst.DecideEquality loc + | TacticAst.Decompose (loc,term) -> + let status,term = disambiguate_term status term in + status, TacticAst.Decompose(loc,term) | TacticAst.Discriminate (loc,term) -> let status,term = disambiguate_term status term in status, TacticAst.Discriminate(loc,term) @@ -397,6 +419,9 @@ let disambiguate_tactic status = function let status, cic = disambiguate_term status term in status, TacticAst.ElimType (loc, cic) | TacticAst.Exists loc -> status, TacticAst.Exists loc + | TacticAst.Fold (loc,reduction_kind, term) -> + let status, term = disambiguate_term status term in + status, TacticAst.Fold (loc,reduction_kind, term) | TacticAst.FwdSimpl (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.FwdSimpl (loc, term) @@ -406,6 +431,9 @@ let disambiguate_tactic status = function let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Generalize(loc,term,pattern) | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) + | TacticAst.Injection (loc,term) -> + let status, term = disambiguate_term status term in + status, TacticAst.Injection (loc,term) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) | TacticAst.LApply (loc, to_what, what) -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 34cf20afa..8eec3244d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -168,7 +168,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,None,None))); MatitaGtkMisc.toggle_widget_visibility ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) ~check:self#main#tacticsBarMenuItem;