From a8ba78e20a4bdbb21ee257377cb8cbdfbec09717 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 20 Mar 2017 09:19:33 +0100 Subject: [PATCH] refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic --- library/init/meta/async_tactic.lean | 2 +- library/init/meta/interactive.lean | 15 +++------------ library/init/meta/smt/interactive.lean | 3 --- src/frontends/lean/tactic_notation.cpp | 3 --- tests/lean/interactive/focus.lean.expected.out | 4 ++-- 5 files changed, 6 insertions(+), 21 deletions(-) diff --git a/library/init/meta/async_tactic.lean b/library/init/meta/async_tactic.lean index e4bde39410..437db13a07 100644 --- a/library/init/meta/async_tactic.lean +++ b/library/init/meta/async_tactic.lean @@ -50,7 +50,7 @@ namespace interactive open interactive.types /-- Proves the first goal asynchronously as a separate lemma. -/ -meta def async (tac : irtactic) : tactic unit := +meta def async (tac : itactic) : tactic unit := prove_goal_async tac end interactive diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index e23db33b06..e54969d052 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -118,7 +118,7 @@ private meta def parser_desc_aux : expr → tactic (list format) meta def param_desc : expr → tactic format | ```(parse %%p) := join <$> parser_desc_aux p | ```(opt_param %%t ._) := (++ "?") <$> pp t -| e := if is_constant e ∧ (const_name e)^.components^.ilast ∈ [`itactic, `irtactic] +| e := if is_constant e ∧ (const_name e)^.components^.ilast = `itactic then return $ to_fmt "{ tactic }" else paren <$> pp e end interactive @@ -147,15 +147,6 @@ itactic: parse a nested "interactive" tactic. That is, parse meta def itactic : Type := tactic unit -/- -irtactic: parse a nested "interactive" tactic. That is, parse - `{` tactic `}` -It is similar to itactic, but the interactive mode will report errors -when any of the nested tactics fail. This is good for tactics such as async and abstract. --/ -meta def irtactic : Type := -tactic unit - /-- This tactic applies to a goal that is either a Pi/forall or starts with a let binder. @@ -382,7 +373,7 @@ tactic.try meta def solve1 : itactic → tactic unit := tactic.solve1 -meta def abstract (id : parse ident? ) (tac : irtactic) : tactic unit := +meta def abstract (id : parse ident? ) (tac : itactic) : tactic unit := tactic.abstract tac id meta def all_goals : itactic → tactic unit := @@ -391,7 +382,7 @@ tactic.all_goals meta def any_goals : itactic → tactic unit := tactic.any_goals -meta def focus (tac : irtactic) : tactic unit := +meta def focus (tac : itactic) : tactic unit := tactic.focus [tac] /-- diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index a5758edcde..dea726d85e 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -40,9 +40,6 @@ local postfix *:9001 := many meta def itactic : Type := smt_tactic unit -meta def irtactic : Type := -smt_tactic unit - meta def intros : parse ident* → smt_tactic unit | [] := smt_tactic.intros | hs := smt_tactic.intro_lst hs diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index b0519f7460..f7f8fda0c1 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -148,7 +148,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co auto pos = p.pos(); expr type = p.env().get(decl_name).get_type(); name itactic = get_interactive_tactic_full_name(tac_class, "itactic"); - name irtactic = get_interactive_tactic_full_name(tac_class, "irtactic"); buffer args; try { try { @@ -164,8 +163,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2])); } else if (is_constant(arg_type, itactic)) { args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep)); - } else if (is_constant(arg_type, irtactic)) { - args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep)); } else { break; } diff --git a/tests/lean/interactive/focus.lean.expected.out b/tests/lean/interactive/focus.lean.expected.out index 40207f6067..2d984100e9 100644 --- a/tests/lean/interactive/focus.lean.expected.out +++ b/tests/lean/interactive/focus.lean.expected.out @@ -1,4 +1,4 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":5} -{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":7} +{"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5} +{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7} {"record":{"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0\n\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"},"response":"ok","seq_num":9}