From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 11:06:46 +0000 (+0000) Subject: * More tactics are now available to matita. X-Git-Tag: INDEXING_NO_PROOFS~53 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0da86404aeb2b8ee460e79be0ba42ff86c97e15e;p=helm.git * More tactics are now available to matita. * Code reordering (match branches are now in alphabetical order) --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 4373b9be7..18f89c504 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -20,50 +20,36 @@ let namer_of names = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ let tactic_of_ast = function - | TacticAst.Intros (_, None, names) -> - (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Intros (_, Some num, names) -> - (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~howmany:num - ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Reflexivity _ -> Tactics.reflexivity + | 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.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.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.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.Intros (_, None, names) -> + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () + | TacticAst.Intros (_, Some num, names) -> + PrimitiveTactics.intros_tac ~howmany:num + ~mk_fresh_name_callback:(namer_of names) () + | TacticAst.LApply (_, to_what, what) -> + Tactics.lapply ?to_what what | TacticAst.Left _ -> Tactics.left - | TacticAst.Right _ -> Tactics.right - | TacticAst.Ring _ -> Tactics.ring - | TacticAst.Split _ -> Tactics.split - | TacticAst.Symmetry _ -> Tactics.symmetry - | TacticAst.Transitivity (_, term) -> Tactics.transitivity term - | TacticAst.Apply (_, term) -> Tactics.apply term - | TacticAst.Absurd (_, term) -> Tactics.absurd term - | TacticAst.Exact (_, term) -> Tactics.exact term - | TacticAst.Cut (_, term) -> Tactics.cut term - | TacticAst.Elim (_, term, _) -> - (* TODO Zack implement "using" argument *) - (* old: Tactics.elim_intros_simpl term *) - Tactics.elim_intros term - | TacticAst.ElimType (_, term) -> Tactics.elim_type term - | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what - | TacticAst.Auto (_,depth) -> -(* AutoTactic.auto_tac ~num (MatitaDb.instance ()) *) - AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) () - | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what -(* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.Replace_pattern of 'term pattern * 'term -*) | TacticAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) | TacticAst.Reduce (_, reduction_kind, pattern) -> @@ -72,15 +58,18 @@ let tactic_of_ast = function | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern | `Whd -> Tactics.whd ~pattern) + | TacticAst.Reflexivity _ -> Tactics.reflexivity + | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what | TacticAst.Rewrite (_, dir, t, pattern) -> if dir = `Left then EqualityTactics.rewrite_tac ~where:pattern ~term:t () else EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () - | TacticAst.FwdSimpl (_, term) -> - Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) - | TacticAst.LApply (_, to_what, what) -> - Tactics.lapply ?to_what what + | TacticAst.Right _ -> Tactics.right + | TacticAst.Ring _ -> Tactics.ring + | TacticAst.Split _ -> Tactics.split + | TacticAst.Symmetry _ -> Tactics.symmetry + | TacticAst.Transitivity (_, term) -> Tactics.transitivity term let eval_tactical status tac = let apply_tactic tactic = @@ -374,21 +363,29 @@ let disambiguate_pattern aliases (hyp_paths ,goal_path) = (hyp_paths ,goal_path) let disambiguate_tactic status = function - | TacticAst.Transitivity (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Transitivity (loc, cic) | TacticAst.Apply (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Apply (loc, cic) | TacticAst.Absurd (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Absurd (loc, cic) - | TacticAst.Exact (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Exact (loc, cic) + | TacticAst.Assumption loc -> status, TacticAst.Assumption loc + | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) + | 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.Cut (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Cut (loc, cic) + | TacticAst.Discriminate (loc,term) -> + let status,term = disambiguate_term status term in + status, TacticAst.Discriminate(loc,term) + | TacticAst.Exact (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Exact (loc, cic) | TacticAst.Elim (loc, term, Some term') -> let status, cic1 = disambiguate_term status term in let status, cic2 = disambiguate_term status term' in @@ -399,65 +396,48 @@ let disambiguate_tactic status = function | TacticAst.ElimType (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.ElimType (loc, cic) - | TacticAst.Replace (loc, what, with_what) -> - let status, cic1 = disambiguate_term status what in - let status, cic2 = disambiguate_term status with_what in - status, TacticAst.Replace (loc, cic1, cic2) - | 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.Exists loc -> status, TacticAst.Exists loc + | TacticAst.FwdSimpl (loc, term) -> + let status, term = disambiguate_term status term in + status, TacticAst.FwdSimpl (loc, term) + | TacticAst.Fourier loc -> status, TacticAst.Fourier loc | TacticAst.Generalize (loc,term,pattern) -> let status,term = disambiguate_term status term in let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Generalize(loc,term,pattern) - | TacticAst.Discriminate (loc,term) -> - let status,term = disambiguate_term status term in - status, TacticAst.Discriminate(loc,term) -(* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.Replace_pattern of 'term pattern * 'term -*) + | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) + | TacticAst.Intros (loc, num, names) -> + status, TacticAst.Intros (loc, num, names) + | TacticAst.LApply (loc, to_what, what) -> + let status, to_what = + match to_what with + None -> status,None + | Some to_what -> status, Some (disambiguate_term status to_what) in + let status, what = disambiguate_term status what in + status, TacticAst.LApply (loc, None, what) + | TacticAst.Left loc -> status, TacticAst.Left loc | TacticAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in status, TacticAst.LetIn (loc,term,name) | TacticAst.Reduce (loc, reduction_kind, pattern) -> let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Reduce(loc, reduction_kind, pattern) + | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc + | TacticAst.Replace (loc, what, with_what) -> + let status, cic1 = disambiguate_term status what in + let status, cic2 = disambiguate_term status with_what in + status, TacticAst.Replace (loc, cic1, cic2) | TacticAst.Rewrite (loc, dir, t, pattern) -> let status, term = disambiguate_term status t in let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Rewrite (loc, dir, term, pattern) - | TacticAst.Intros (loc, num, names) -> - status, TacticAst.Intros (loc, num, names) - | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) - | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc - | TacticAst.Assumption loc -> status, TacticAst.Assumption loc - | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc - | TacticAst.Exists loc -> status, TacticAst.Exists loc - | TacticAst.Fourier loc -> status, TacticAst.Fourier loc - | TacticAst.Left loc -> status, TacticAst.Left loc | TacticAst.Right loc -> status, TacticAst.Right loc | TacticAst.Ring loc -> status, TacticAst.Ring loc | TacticAst.Split loc -> status, TacticAst.Split loc | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc - | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) - | TacticAst.FwdSimpl (loc, term) -> - let status, term = disambiguate_term status term in - status, TacticAst.FwdSimpl (loc, term) - | TacticAst.LApply (loc, Some to_what, what) -> - let status, to_what = disambiguate_term status to_what in - let status, what = disambiguate_term status what in - status, TacticAst.LApply (loc, Some to_what, what) - | TacticAst.LApply (loc, None, what) -> - let status, what = disambiguate_term status what in - status, TacticAst.LApply (loc, None, what) + | TacticAst.Transitivity (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Transitivity (loc, cic) let rec disambiguate_tactical status = function | TacticAst.Tactic (loc, tactic) ->