From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 17:00:44 +0000 (+0000) Subject: A few other tactics made available to matita. X-Git-Tag: INDEXING_NO_PROOFS~38 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=72f63f8d930b8b7fe41b47a5cfd3b4c701be34c7;p=helm.git A few other tactics made available to matita. A few tactics (change, fold, replace) generalized to patterns. The argument of clear and clearbody is now an identifier. --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 89d168af3..37c96ce4e 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -26,6 +26,8 @@ let tactic_of_ast = function | TacticAst.Auto (_,depth,width) -> AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what + | TacticAst.Clear (_,id) -> Tactics.clear id + | TacticAst.ClearBody (_,id) -> Tactics.clearbody id | TacticAst.Contradiction _ -> Tactics.contradiction | TacticAst.Compare (_, term) -> Tactics.compare term | TacticAst.Constructor (_, n) -> Tactics.constructor n @@ -40,7 +42,8 @@ let tactic_of_ast = function | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Exists _ -> Tactics.exists - | TacticAst.Fold (_, reduction_kind ,term) -> + | TacticAst.Fail _ -> Tactics.fail + | TacticAst.Fold (_, reduction_kind ,term, pattern) -> let reduction = match reduction_kind with | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] @@ -48,7 +51,7 @@ let tactic_of_ast = function | `Simpl -> ProofEngineReduction.simpl | `Whd -> CicReduction.whd ~delta:false ~subst:[] in - Tactics.fold ~reduction ~also_in_hypotheses:false ~term + Tactics.fold ~reduction ~pattern ~term | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.FwdSimpl (_, term) -> Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) @@ -56,6 +59,7 @@ let tactic_of_ast = function let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~term ~mk_fresh_name_callback:(namer_of names) pat | TacticAst.Goal (_, n) -> Tactics.set_goal n + | TacticAst.IdTac _ -> Tactics.id | TacticAst.Injection (_,term) -> Tactics.injection term | TacticAst.Intros (_, None, names) -> PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () @@ -74,7 +78,8 @@ let tactic_of_ast = function | `Simpl -> Tactics.simpl ~pattern | `Whd -> Tactics.whd ~pattern) | TacticAst.Reflexivity _ -> Tactics.reflexivity - | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what + | TacticAst.Replace (_, pattern, with_what) -> + Tactics.replace ~pattern ~with_what | TacticAst.Rewrite (_, dir, t, pattern) -> if dir = `Left then EqualityTactics.rewrite_tac ~where:pattern ~term:t () @@ -104,10 +109,8 @@ let eval_tactical status tac = in let rec tactical_of_ast = function | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic - | TacticAst.Fail loc -> Tacticals.fail | TacticAst.Do (loc, num, tactical) -> Tacticals.do_tactic num (tactical_of_ast tactical) - | TacticAst.IdTac loc -> Tacticals.id_tac | TacticAst.Repeat (loc, tactical) -> Tacticals.repeat_tactic (tactical_of_ast tactical) | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) @@ -391,6 +394,8 @@ let disambiguate_tactic status = function 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.Clear (loc,id) -> status,TacticAst.Clear (loc,id) + | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id) | TacticAst.Compare (loc,term) -> let status, term = disambiguate_term status term in status, TacticAst.Compare (loc,term) @@ -423,9 +428,11 @@ 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) -> + | TacticAst.Fail loc -> status,TacticAst.Fail loc + | TacticAst.Fold (loc,reduction_kind, term, pattern) -> let status, term = disambiguate_term status term in - status, TacticAst.Fold (loc,reduction_kind, term) + let pattern = disambiguate_pattern status.aliases pattern in + status, TacticAst.Fold (loc,reduction_kind, term, pattern) | TacticAst.FwdSimpl (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.FwdSimpl (loc, term) @@ -435,6 +442,7 @@ let disambiguate_tactic status = function let pattern = disambiguate_pattern status.aliases pattern in status, TacticAst.Generalize(loc,term,ident,pattern) | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) + | TacticAst.IdTac loc -> status,TacticAst.IdTac loc | TacticAst.Injection (loc,term) -> let status, term = disambiguate_term status term in status, TacticAst.Injection (loc,term) @@ -458,10 +466,10 @@ let disambiguate_tactic status = function 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.Replace (loc, pattern, with_what) -> + let pattern = disambiguate_pattern status.aliases pattern in + let status, with_what = disambiguate_term status with_what in + status, TacticAst.Replace (loc, pattern, with_what) | TacticAst.Rewrite (loc, dir, t, pattern) -> let status, term = disambiguate_term status t in let pattern = disambiguate_pattern status.aliases pattern in @@ -498,8 +506,6 @@ let rec disambiguate_tactical status = function | TacticAst.Try (loc, tactical) -> let status, tactical = disambiguate_tactical status tactical in status, TacticAst.Try (loc, tactical) - | (TacticAst.IdTac _ | TacticAst.Fail _) as tac -> - status, tac and disambiguate_tacticals status tacticals = let status, tacticals =