From 368f9d347e3e911337f31e170a773150e5974a20 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2015 18:07:06 -0800 Subject: [PATCH] refactor(frontends/lean): approach used to parse tactics The previous approach was too fragile TODO: we should add separate parsing tables for tactics --- hott/algebra/precategory/yoneda.hlean | 4 + hott/init/tactic.hlean | 28 ++-- library/init/tactic.lean | 28 ++-- library/logic/axioms/prop_complete.lean | 6 +- src/frontends/lean/builtin_exprs.cpp | 25 +--- src/frontends/lean/parser.cpp | 132 +++++++++++++++++++ src/frontends/lean/parser.h | 8 ++ src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 8 ++ src/frontends/lean/tokens.h | 2 + src/library/constants.cpp | 60 ++++----- src/library/constants.h | 15 +-- src/library/constants.txt | 15 +-- src/library/tactic/change_tactic.cpp | 2 +- src/library/tactic/clear_tactic.cpp | 2 +- src/library/tactic/generalize_tactic.cpp | 2 +- src/library/tactic/intros_tactic.cpp | 2 +- src/library/tactic/inversion_tactic.cpp | 11 +- src/library/tactic/revert_tactic.cpp | 2 +- tests/lean/change_tac_fail.lean | 2 +- tests/lean/change_tac_fail.lean.expected.out | 2 +- tests/lean/empty_thm.lean | 2 +- tests/lean/run/def_tac.lean | 6 +- tests/lean/run/inf_tree3.lean | 2 +- tests/lean/run/rename_tac.lean | 2 +- tests/lean/run/tactic_op_overload_bug.lean | 27 ++++ 26 files changed, 268 insertions(+), 129 deletions(-) create mode 100644 tests/lean/run/tactic_op_overload_bug.lean diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 87e1becb6..94f76e3cf 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -151,6 +151,10 @@ namespace functor -- → F₁ = F₂ := -- functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'1)) + + set_option pp.full_names true + open tactic + print raw id --set_option pp.notation false definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta) diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index dbab32fee..3313e5af2 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -63,37 +63,29 @@ opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin -opaque definition inversion (id : expr) : tactic := builtin - -notation a `↦` b:max := rename a b inductive expr_list : Type := | nil : expr_list | cons : expr → expr_list → expr_list +-- auxiliary type used to mark optional list of arguments +definition opt_expr_list := expr_list + -- rewrite_tac is just a marker for the builtin 'rewrite' notation -- used to create instances of this tactic. opaque definition rewrite_tac (e : expr_list) : tactic := builtin -opaque definition inversion_with (id : expr) (ids : expr_list) : tactic := builtin -notation `cases` a:max := inversion a -notation `cases` a:max `with` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := inversion_with a l +opaque definition cases (id : expr) (ids : opt_expr_list) : tactic := builtin -opaque definition intro_lst (ids : expr_list) : tactic := builtin -notation `intros` := intro_lst expr_list.nil -notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_lst l +opaque definition intros (ids : opt_expr_list) : tactic := builtin -opaque definition generalize_lst (es : expr_list) : tactic := builtin -notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_lst l +opaque definition generalizes (es : expr_list) : tactic := builtin -opaque definition clear_lst (ids : expr_list) : tactic := builtin -notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := clear_lst l +opaque definition clears (ids : expr_list) : tactic := builtin -opaque definition revert_lst (ids : expr_list) : tactic := builtin -notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l +opaque definition reverts (ids : expr_list) : tactic := builtin -opaque definition change_goal (e : expr) : tactic := builtin -notation `change` e := change_goal e +opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin @@ -104,7 +96,7 @@ definition try (t : tactic) : tactic := [t | id] definition repeat1 (t : tactic) : tactic := t ; repeat t definition focus (t : tactic) : tactic := focus_at t 0 definition determ (t : tactic) : tactic := at_most t 1 - +definition trivial : tactic := [ apply eq.refl | assumption ] definition do (n : num) (t : tactic) : tactic := nat.rec id (λn t', (t;t')) (nat.of_num n) diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 4bff9d91b..19e70190b 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -62,37 +62,29 @@ opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin -opaque definition inversion (id : expr) : tactic := builtin - -notation a `↦` b:max := rename a b inductive expr_list : Type := | nil : expr_list | cons : expr → expr_list → expr_list +-- auxiliary type used to mark optional list of arguments +definition opt_expr_list := expr_list + -- rewrite_tac is just a marker for the builtin 'rewrite' notation -- used to create instances of this tactic. opaque definition rewrite_tac (e : expr_list) : tactic := builtin -opaque definition inversion_with (id : expr) (ids : expr_list) : tactic := builtin -notation `cases` a:max := inversion a -notation `cases` a:max `with` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := inversion_with a l +opaque definition cases (id : expr) (ids : opt_expr_list) : tactic := builtin -opaque definition intro_lst (ids : expr_list) : tactic := builtin -notation `intros` := intro_lst expr_list.nil -notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_lst l +opaque definition intros (ids : opt_expr_list) : tactic := builtin -opaque definition generalize_lst (es : expr_list) : tactic := builtin -notation `generalizes` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := generalize_lst l +opaque definition generalizes (es : expr_list) : tactic := builtin -opaque definition clear_lst (ids : expr_list) : tactic := builtin -notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := clear_lst l +opaque definition clears (ids : expr_list) : tactic := builtin -opaque definition revert_lst (ids : expr_list) : tactic := builtin -notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l +opaque definition reverts (ids : expr_list) : tactic := builtin -opaque definition change_goal (e : expr) : tactic := builtin -notation `change` e := change_goal e +opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin @@ -103,7 +95,7 @@ definition try (t : tactic) : tactic := [t | id] definition repeat1 (t : tactic) : tactic := t ; repeat t definition focus (t : tactic) : tactic := focus_at t 0 definition determ (t : tactic) : tactic := at_most t 1 - +definition trivial : tactic := [ apply eq.refl | apply true.intro | assumption ] definition do (n : num) (t : tactic) : tactic := nat.rec id (λn t', (t;t')) (nat.of_num n) diff --git a/library/logic/axioms/prop_complete.lean b/library/logic/axioms/prop_complete.lean index 7c2b9d55e..cce9392c9 100644 --- a/library/logic/axioms/prop_complete.lean +++ b/library/logic/axioms/prop_complete.lean @@ -12,13 +12,13 @@ axiom prop_complete (a : Prop) : a = true ∨ a = false definition eq_true_or_eq_false := prop_complete -theorem cases (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := +theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := or.elim (prop_complete a) (assume Ht : a = true, Ht⁻¹ ▸ H1) (assume Hf : a = false, Hf⁻¹ ▸ H2) theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a := -cases P H1 H2 a +cases_true_false P H1 H2 a -- this supercedes the em in decidable theorem em (a : Prop) : a ∨ ¬a := @@ -37,7 +37,7 @@ by_cases (assume H1 : ¬p, false.rec _ (H H1)) theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true := -cases (λ x, x = false ∨ x = true) +cases_true_false (λ x, x = false ∨ x = true) (or.inr rfl) (or.inl rfl) a diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index b76f8acaa..fec2f7ceb 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -124,34 +124,19 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const return p.save_pos(mk_explicit_expr_placeholder(), pos); } -static environment open_tactic_namespace(parser & p) { - if (!is_tactic_namespace_open(p.env())) { - environment env = using_namespace(p.env(), p.ios(), get_tactic_name()); - env = add_aliases(env, get_tactic_name(), name()); - return env; - } else { - return p.env(); - } -} - static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { - environment env = open_tactic_namespace(p); parser::undef_id_to_local_scope scope(p); - parser::local_scope scope2(p, env); - parser::undef_id_to_local_scope scope1(p); p.next(); - expr t = p.parse_expr(); + expr t = p.parse_tactic(); return p.mk_by(t, pos); } static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & end_token, bool nested = false) { if (!p.has_tactic_decls()) throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos); - environment env = open_tactic_namespace(p); - parser::local_scope scope2(p, env); parser::undef_id_to_local_scope scope1(p); p.next(); - optional pre_tac = get_begin_end_pre_tactic(env); + optional pre_tac = get_begin_end_pre_tactic(p.env()); buffer tacs; bool first = true; @@ -223,7 +208,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & // parse: 'by' tactic auto pos = p.pos(); p.next(); - expr t = p.parse_expr(); + expr t = p.parse_tactic(); add_tac(t, pos); } else { throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos()); @@ -237,7 +222,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & add_tac(t, pos); } else { auto pos = p.pos(); - expr t = p.parse_expr(); + expr t = p.parse_tactic(); add_tac(t, pos); } } @@ -293,7 +278,7 @@ static expr parse_proof(parser & p, expr const & prop) { // parse: 'by' tactic auto pos = p.pos(); p.next(); - expr t = p.parse_expr(); + expr t = p.parse_tactic(); return p.mk_by(t, pos); } else if (p.curr_is_token(get_using_tk())) { // parse: 'using' locals* ',' proof diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 5fc97870c..9281629e5 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" #include "library/parser_nested_exception.h" #include "library/aliases.h" +#include "library/constants.h" #include "library/private.h" #include "library/protected.h" #include "library/choice.h" @@ -44,6 +45,7 @@ Author: Leonardo de Moura #include "frontends/lean/notation_cmd.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/info_annotation.h" +#include "frontends/lean/parse_rewrite_tactic.h" #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true @@ -1284,6 +1286,136 @@ expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environme return parse_expr(rbp); } +static bool is_tactic_type(expr const & e) { + return is_constant(e) && const_name(e) == get_tactic_name(); +} + +static bool is_tactic_expr_list_type(expr const & e) { + return is_constant(e) && const_name(e) == get_tactic_expr_list_name(); +} + +static bool is_tactic_opt_expr_list_type(expr const & e) { + return is_constant(e) && const_name(e) == get_tactic_opt_expr_list_name(); +} + +static bool is_tactic_command_type(expr e) { + while (is_pi(e)) + e = binding_body(e); + return is_tactic_type(e); +} + +optional parser::is_tactic_command(name & id) { + if (id.is_atomic()) + id = get_tactic_name() + id; + auto d = m_env.find(id); + if (!d) + return none_expr(); + expr type = d->get_type(); + if (!is_tactic_command_type(type)) + return none_expr(); + return some_expr(type); +} + +expr parser::parse_tactic_expr_list() { + auto p = pos(); + check_token_next(get_lparen_tk(), "invalid tactic, '(' expected"); + buffer args; + while (!curr_is_token(get_rparen_tk())) { + args.push_back(parse_expr()); + if (!curr_is_token(get_comma_tk())) + break; + next(); + } + check_token_next(get_rparen_tk(), "invalid tactic, ',' or ')' expected"); + unsigned i = args.size(); + expr r = save_pos(mk_constant(get_tactic_expr_list_nil_name()), p); + while (i > 0) { + i--; + r = mk_app({save_pos(mk_constant(get_tactic_expr_list_cons_name()), p), args[i], r}, p); + } + return r; +} + +expr parser::parse_tactic_opt_expr_list() { + if (curr_is_token(get_lparen_tk())) { + return parse_tactic_expr_list(); + } else if (curr_is_token(get_with_tk())) { + next(); + return parse_tactic_expr_list(); + } else { + return save_pos(mk_constant(get_tactic_expr_list_nil_name()), pos()); + } +} + +expr parser::parse_tactic_nud() { + if (curr_is_identifier()) { + auto id_pos = pos(); + name id = get_name_val(); + if (optional tac_type = is_tactic_command(id)) { + next(); + expr type = *tac_type; + expr r = save_pos(mk_constant(id), id_pos); + while (is_pi(type)) { + expr d = binding_domain(type); + if (is_tactic_type(d)) { + r = mk_app(r, parse_tactic(get_max_prec()), id_pos); + } else if (is_tactic_expr_list_type(d)) { + r = mk_app(r, parse_tactic_expr_list(), id_pos); + } else if (is_tactic_opt_expr_list_type(d)) { + r = mk_app(r, parse_tactic_opt_expr_list(), id_pos); + } else { + r = mk_app(r, parse_expr(get_max_prec()), id_pos); + } + type = binding_body(type); + } + return r; + } else { + return parse_expr(); + } + } else if (curr_is_token(get_lbracket_tk())) { + next(); + expr r = parse_tactic(); + while (curr_is_token(get_bar_tk())) { + auto bar_pos = pos(); + next(); + expr n = parse_tactic(); + r = mk_app({save_pos(mk_constant(get_tactic_or_else_name()), bar_pos), r, n}, bar_pos); + } + check_token_next(get_rbracket_tk(), "invalid or-else tactic, ']' expected"); + return r; + } else if (curr_is_token_or_id(get_rewrite_tk())) { + auto p = pos(); + next(); + return save_pos(parse_rewrite_tactic(*this), p); + } else if (curr_is_token(get_lparen_tk())) { + next(); + expr r = parse_tactic(); + check_token_next(get_rparen_tk(), "invalid tactic, ')' expected"); + return r; + } else { + return parse_expr(); + } +} + +expr parser::parse_tactic_led(expr left) { + auto p = pos(); + if (curr_is_token(get_semicolon_tk())) { + next(); + expr right = parse_tactic(); + return mk_app({save_pos(mk_constant(get_tactic_and_then_name()), p), left, right}, p); + } else { + throw parser_error("invalid tactic expression", p); + } +} + +expr parser::parse_tactic(unsigned rbp) { + expr left = parse_tactic_nud(); + while (rbp < curr_lbp()) { + left = parse_tactic_led(left); + } + return left; +} + void parser::parse_command() { lean_assert(curr() == scanner::token_kind::CommandKeyword); m_last_cmd_pos = pos(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 9f9a4a187..e861c0dc8 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -217,6 +217,12 @@ class parser { elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); + optional is_tactic_command(name & id); + expr parse_tactic_led(expr left); + expr parse_tactic_nud(); + expr parse_tactic_expr_list(); + expr parse_tactic_opt_expr_list(); + public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, @@ -380,6 +386,8 @@ public: } expr parse_scoped_expr(buffer const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } + expr parse_tactic(unsigned rbp = 0); + struct local_scope { parser & m_p; environment m_env; local_scope(parser & p, bool save_options = false); local_scope(parser & p, environment const & env); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 26d7c01cc..2f474c839 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -79,7 +79,7 @@ void init_token_table(token_table & t) { {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, - {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, + {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {";", 1}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index e360b8550..1b691239f 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -10,6 +10,7 @@ namespace lean { static name * g_period = nullptr; static name * g_placeholder = nullptr; static name * g_colon = nullptr; +static name * g_semicolon = nullptr; static name * g_dcolon = nullptr; static name * g_lparen = nullptr; static name * g_rparen = nullptr; @@ -81,6 +82,7 @@ static name * g_using = nullptr; static name * g_then = nullptr; static name * g_else = nullptr; static name * g_by = nullptr; +static name * g_rewrite = nullptr; static name * g_proof = nullptr; static name * g_qed = nullptr; static name * g_begin = nullptr; @@ -130,6 +132,7 @@ void initialize_tokens() { g_period = new name("."); g_placeholder = new name("_"); g_colon = new name(":"); + g_semicolon = new name(";"); g_dcolon = new name("::"); g_lparen = new name("("); g_rparen = new name(")"); @@ -201,6 +204,7 @@ void initialize_tokens() { g_then = new name("then"); g_else = new name("else"); g_by = new name("by"); + g_rewrite = new name("rewrite"); g_proof = new name("proof"); g_qed = new name("qed"); g_begin = new name("begin"); @@ -297,6 +301,7 @@ void finalize_tokens() { delete g_then; delete g_else; delete g_by; + delete g_rewrite; delete g_proof; delete g_qed; delete g_begin; @@ -363,6 +368,7 @@ void finalize_tokens() { delete g_rparen; delete g_lparen; delete g_colon; + delete g_semicolon; delete g_dcolon; delete g_placeholder; delete g_period; @@ -372,6 +378,7 @@ name const & get_metaclasses_tk() { return *g_metaclasses; } name const & get_period_tk() { return *g_period; } name const & get_placeholder_tk() { return *g_placeholder; } name const & get_colon_tk() { return *g_colon; } +name const & get_semicolon_tk() { return *g_semicolon; } name const & get_dcolon_tk() { return *g_dcolon; } name const & get_langle_tk() { return *g_langle; } name const & get_rangle_tk() { return *g_rangle; } @@ -443,6 +450,7 @@ name const & get_using_tk() { return *g_using; } name const & get_then_tk() { return *g_then; } name const & get_else_tk() { return *g_else; } name const & get_by_tk() { return *g_by; } +name const & get_rewrite_tk() { return *g_rewrite; } name const & get_proof_tk() { return *g_proof; } name const & get_qed_tk() { return *g_qed; } name const & get_begin_tk() { return *g_begin; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 3005615d8..4fffd620f 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -12,6 +12,7 @@ void finalize_tokens(); name const & get_period_tk(); name const & get_placeholder_tk(); name const & get_colon_tk(); +name const & get_semicolon_tk(); name const & get_dcolon_tk(); name const & get_lparen_tk(); name const & get_rparen_tk(); @@ -83,6 +84,7 @@ name const & get_using_tk(); name const & get_then_tk(); name const & get_else_tk(); name const & get_by_tk(); +name const & get_rewrite_tk(); name const & get_proof_tk(); name const & get_begin_tk(); name const & get_qed_tk(); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 2c413a2c4..d1e4395ca 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -69,16 +69,14 @@ name const * g_tactic_assumption = nullptr; name const * g_tactic_at_most = nullptr; name const * g_tactic_beta = nullptr; name const * g_tactic_builtin = nullptr; -name const * g_tactic_change_goal = nullptr; -name const * g_tactic_change_hypothesis = nullptr; +name const * g_tactic_cases = nullptr; +name const * g_tactic_change = nullptr; name const * g_tactic_clear = nullptr; -name const * g_tactic_clear_lst = nullptr; +name const * g_tactic_clears = nullptr; name const * g_tactic_determ = nullptr; name const * g_tactic_discard = nullptr; name const * g_tactic_intro = nullptr; -name const * g_tactic_intro_lst = nullptr; -name const * g_tactic_inversion = nullptr; -name const * g_tactic_inversion_with = nullptr; +name const * g_tactic_intros = nullptr; name const * g_tactic_exact = nullptr; name const * g_tactic_expr = nullptr; name const * g_tactic_expr_builtin = nullptr; @@ -89,17 +87,18 @@ name const * g_tactic_fail = nullptr; name const * g_tactic_fixpoint = nullptr; name const * g_tactic_focus_at = nullptr; name const * g_tactic_generalize = nullptr; -name const * g_tactic_generalize_lst = nullptr; +name const * g_tactic_generalizes = nullptr; name const * g_tactic_id = nullptr; name const * g_tactic_interleave = nullptr; name const * g_tactic_now = nullptr; +name const * g_tactic_opt_expr_list = nullptr; name const * g_tactic_or_else = nullptr; name const * g_tactic_par = nullptr; name const * g_tactic_state = nullptr; name const * g_tactic_rename = nullptr; name const * g_tactic_repeat = nullptr; name const * g_tactic_revert = nullptr; -name const * g_tactic_revert_lst = nullptr; +name const * g_tactic_reverts = nullptr; name const * g_tactic_rotate_left = nullptr; name const * g_tactic_rotate_right = nullptr; name const * g_tactic_trace = nullptr; @@ -180,16 +179,14 @@ void initialize_constants() { g_tactic_at_most = new name{"tactic", "at_most"}; g_tactic_beta = new name{"tactic", "beta"}; g_tactic_builtin = new name{"tactic", "builtin"}; - g_tactic_change_goal = new name{"tactic", "change_goal"}; - g_tactic_change_hypothesis = new name{"tactic", "change_hypothesis"}; + g_tactic_cases = new name{"tactic", "cases"}; + g_tactic_change = new name{"tactic", "change"}; g_tactic_clear = new name{"tactic", "clear"}; - g_tactic_clear_lst = new name{"tactic", "clear_lst"}; + g_tactic_clears = new name{"tactic", "clears"}; g_tactic_determ = new name{"tactic", "determ"}; g_tactic_discard = new name{"tactic", "discard"}; g_tactic_intro = new name{"tactic", "intro"}; - g_tactic_intro_lst = new name{"tactic", "intro_lst"}; - g_tactic_inversion = new name{"tactic", "inversion"}; - g_tactic_inversion_with = new name{"tactic", "inversion_with"}; + g_tactic_intros = new name{"tactic", "intros"}; g_tactic_exact = new name{"tactic", "exact"}; g_tactic_expr = new name{"tactic", "expr"}; g_tactic_expr_builtin = new name{"tactic", "expr", "builtin"}; @@ -200,17 +197,18 @@ void initialize_constants() { g_tactic_fixpoint = new name{"tactic", "fixpoint"}; g_tactic_focus_at = new name{"tactic", "focus_at"}; g_tactic_generalize = new name{"tactic", "generalize"}; - g_tactic_generalize_lst = new name{"tactic", "generalize_lst"}; + g_tactic_generalizes = new name{"tactic", "generalizes"}; g_tactic_id = new name{"tactic", "id"}; g_tactic_interleave = new name{"tactic", "interleave"}; g_tactic_now = new name{"tactic", "now"}; + g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; g_tactic_or_else = new name{"tactic", "or_else"}; g_tactic_par = new name{"tactic", "par"}; g_tactic_state = new name{"tactic", "state"}; g_tactic_rename = new name{"tactic", "rename"}; g_tactic_repeat = new name{"tactic", "repeat"}; g_tactic_revert = new name{"tactic", "revert"}; - g_tactic_revert_lst = new name{"tactic", "revert_lst"}; + g_tactic_reverts = new name{"tactic", "reverts"}; g_tactic_rotate_left = new name{"tactic", "rotate_left"}; g_tactic_rotate_right = new name{"tactic", "rotate_right"}; g_tactic_trace = new name{"tactic", "trace"}; @@ -292,16 +290,14 @@ void finalize_constants() { delete g_tactic_at_most; delete g_tactic_beta; delete g_tactic_builtin; - delete g_tactic_change_goal; - delete g_tactic_change_hypothesis; + delete g_tactic_cases; + delete g_tactic_change; delete g_tactic_clear; - delete g_tactic_clear_lst; + delete g_tactic_clears; delete g_tactic_determ; delete g_tactic_discard; delete g_tactic_intro; - delete g_tactic_intro_lst; - delete g_tactic_inversion; - delete g_tactic_inversion_with; + delete g_tactic_intros; delete g_tactic_exact; delete g_tactic_expr; delete g_tactic_expr_builtin; @@ -312,17 +308,18 @@ void finalize_constants() { delete g_tactic_fixpoint; delete g_tactic_focus_at; delete g_tactic_generalize; - delete g_tactic_generalize_lst; + delete g_tactic_generalizes; delete g_tactic_id; delete g_tactic_interleave; delete g_tactic_now; + delete g_tactic_opt_expr_list; delete g_tactic_or_else; delete g_tactic_par; delete g_tactic_state; delete g_tactic_rename; delete g_tactic_repeat; delete g_tactic_revert; - delete g_tactic_revert_lst; + delete g_tactic_reverts; delete g_tactic_rotate_left; delete g_tactic_rotate_right; delete g_tactic_trace; @@ -403,16 +400,14 @@ name const & get_tactic_assumption_name() { return *g_tactic_assumption; } name const & get_tactic_at_most_name() { return *g_tactic_at_most; } name const & get_tactic_beta_name() { return *g_tactic_beta; } name const & get_tactic_builtin_name() { return *g_tactic_builtin; } -name const & get_tactic_change_goal_name() { return *g_tactic_change_goal; } -name const & get_tactic_change_hypothesis_name() { return *g_tactic_change_hypothesis; } +name const & get_tactic_cases_name() { return *g_tactic_cases; } +name const & get_tactic_change_name() { return *g_tactic_change; } name const & get_tactic_clear_name() { return *g_tactic_clear; } -name const & get_tactic_clear_lst_name() { return *g_tactic_clear_lst; } +name const & get_tactic_clears_name() { return *g_tactic_clears; } name const & get_tactic_determ_name() { return *g_tactic_determ; } name const & get_tactic_discard_name() { return *g_tactic_discard; } name const & get_tactic_intro_name() { return *g_tactic_intro; } -name const & get_tactic_intro_lst_name() { return *g_tactic_intro_lst; } -name const & get_tactic_inversion_name() { return *g_tactic_inversion; } -name const & get_tactic_inversion_with_name() { return *g_tactic_inversion_with; } +name const & get_tactic_intros_name() { return *g_tactic_intros; } name const & get_tactic_exact_name() { return *g_tactic_exact; } name const & get_tactic_expr_name() { return *g_tactic_expr; } name const & get_tactic_expr_builtin_name() { return *g_tactic_expr_builtin; } @@ -423,17 +418,18 @@ name const & get_tactic_fail_name() { return *g_tactic_fail; } name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; } name const & get_tactic_focus_at_name() { return *g_tactic_focus_at; } name const & get_tactic_generalize_name() { return *g_tactic_generalize; } -name const & get_tactic_generalize_lst_name() { return *g_tactic_generalize_lst; } +name const & get_tactic_generalizes_name() { return *g_tactic_generalizes; } name const & get_tactic_id_name() { return *g_tactic_id; } name const & get_tactic_interleave_name() { return *g_tactic_interleave; } name const & get_tactic_now_name() { return *g_tactic_now; } +name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } name const & get_tactic_or_else_name() { return *g_tactic_or_else; } name const & get_tactic_par_name() { return *g_tactic_par; } name const & get_tactic_state_name() { return *g_tactic_state; } name const & get_tactic_rename_name() { return *g_tactic_rename; } name const & get_tactic_repeat_name() { return *g_tactic_repeat; } name const & get_tactic_revert_name() { return *g_tactic_revert; } -name const & get_tactic_revert_lst_name() { return *g_tactic_revert_lst; } +name const & get_tactic_reverts_name() { return *g_tactic_reverts; } name const & get_tactic_rotate_left_name() { return *g_tactic_rotate_left; } name const & get_tactic_rotate_right_name() { return *g_tactic_rotate_right; } name const & get_tactic_trace_name() { return *g_tactic_trace; } diff --git a/src/library/constants.h b/src/library/constants.h index b1a6df776..6ec469c09 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -71,16 +71,14 @@ name const & get_tactic_assumption_name(); name const & get_tactic_at_most_name(); name const & get_tactic_beta_name(); name const & get_tactic_builtin_name(); -name const & get_tactic_change_goal_name(); -name const & get_tactic_change_hypothesis_name(); +name const & get_tactic_cases_name(); +name const & get_tactic_change_name(); name const & get_tactic_clear_name(); -name const & get_tactic_clear_lst_name(); +name const & get_tactic_clears_name(); name const & get_tactic_determ_name(); name const & get_tactic_discard_name(); name const & get_tactic_intro_name(); -name const & get_tactic_intro_lst_name(); -name const & get_tactic_inversion_name(); -name const & get_tactic_inversion_with_name(); +name const & get_tactic_intros_name(); name const & get_tactic_exact_name(); name const & get_tactic_expr_name(); name const & get_tactic_expr_builtin_name(); @@ -91,17 +89,18 @@ name const & get_tactic_fail_name(); name const & get_tactic_fixpoint_name(); name const & get_tactic_focus_at_name(); name const & get_tactic_generalize_name(); -name const & get_tactic_generalize_lst_name(); +name const & get_tactic_generalizes_name(); name const & get_tactic_id_name(); name const & get_tactic_interleave_name(); name const & get_tactic_now_name(); +name const & get_tactic_opt_expr_list_name(); name const & get_tactic_or_else_name(); name const & get_tactic_par_name(); name const & get_tactic_state_name(); name const & get_tactic_rename_name(); name const & get_tactic_repeat_name(); name const & get_tactic_revert_name(); -name const & get_tactic_revert_lst_name(); +name const & get_tactic_reverts_name(); name const & get_tactic_rotate_left_name(); name const & get_tactic_rotate_right_name(); name const & get_tactic_trace_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index c443389e4..348406140 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -64,16 +64,14 @@ tactic.assumption tactic.at_most tactic.beta tactic.builtin -tactic.change_goal -tactic.change_hypothesis +tactic.cases +tactic.change tactic.clear -tactic.clear_lst +tactic.clears tactic.determ tactic.discard tactic.intro -tactic.intro_lst -tactic.inversion -tactic.inversion_with +tactic.intros tactic.exact tactic.expr tactic.expr.builtin @@ -84,17 +82,18 @@ tactic.fail tactic.fixpoint tactic.focus_at tactic.generalize -tactic.generalize_lst +tactic.generalizes tactic.id tactic.interleave tactic.now +tactic.opt_expr_list tactic.or_else tactic.par tactic.state tactic.rename tactic.repeat tactic.revert -tactic.revert_lst +tactic.reverts tactic.rotate_left tactic.rotate_right tactic.trace diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index e0d1158f6..1a463cfd3 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -45,7 +45,7 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { } void initialize_change_tactic() { - register_tac(get_tactic_change_goal_name(), + register_tac(get_tactic_change_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'change' tactic, invalid argument"); return change_goal_tactic(fn, get_tactic_expr_expr(app_arg(e))); diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index ff37c0528..d0288a57c 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -48,7 +48,7 @@ void initialize_clear_tactic() { name n = tactic_expr_to_id(app_arg(e), "invalid 'clear' tactic, argument must be an identifier"); return clear_tactic(n); }); - register_tac(get_tactic_clear_lst_name(), + register_tac(get_tactic_clears_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected"); diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index cf6414ec6..3dd13f5f1 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -68,7 +68,7 @@ void initialize_generalize_tactic() { return generalize_tactic(fn, get_tactic_expr_expr(app_arg(e)), "x"); }); - register_tac(get_tactic_generalize_lst_name(), + register_tac(get_tactic_generalizes_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { buffer args; get_tactic_expr_list_elements(app_arg(e), args, "invalid 'generalizes' tactic, list of expressions expected"); diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index d5bf3ba45..c62519179 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/src/library/tactic/intros_tactic.cpp @@ -65,7 +65,7 @@ void initialize_intros_tactic() { name const & id = tactic_expr_to_id(app_arg(e), "invalid 'intro' tactic, argument must be an identifier"); return intros_tactic(to_list(id)); }); - register_tac(get_tactic_intro_lst_name(), + register_tac(get_tactic_intros_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers"); diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index a82715468..3067c2503 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -962,16 +962,11 @@ tactic inversion_tactic(name const & n, list const & ids) { } void initialize_inversion_tactic() { - register_tac(get_tactic_inversion_name(), + register_tac(get_tactic_cases_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(e), "invalid 'inversion/cases' tactic, argument must be an identifier"); - return inversion_tactic(n, list()); - }); - register_tac(get_tactic_inversion_with_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases-with' tactic, argument must be an identifier"); + name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an identifier"); buffer ids; - get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases-with' tactic, list of identifiers expected"); + get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases' tactic, list of identifiers expected"); return inversion_tactic(n, to_list(ids.begin(), ids.end())); }); } diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 365d70295..6d22a7acb 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -55,7 +55,7 @@ void initialize_revert_tactic() { return revert_tactic(n); }); - register_tac(get_tactic_revert_lst_name(), + register_tac(get_tactic_reverts_name(), [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { buffer ns; get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected"); diff --git a/tests/lean/change_tac_fail.lean b/tests/lean/change_tac_fail.lean index 1718ee7e3..062132a9b 100644 --- a/tests/lean/change_tac_fail.lean +++ b/tests/lean/change_tac_fail.lean @@ -7,6 +7,6 @@ theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u) | append.assoc nil t u := by esimp | append.assoc (a :: l) t u := begin - change a :: (l ++ t ++ u) = (a :: l) ++ (t ++ a), + change (a :: (l ++ t ++ u) = (a :: l) ++ (t ++ a)), rewrite append.assoc end diff --git a/tests/lean/change_tac_fail.lean.expected.out b/tests/lean/change_tac_fail.lean.expected.out index 4778a96b7..94ca3d0f7 100644 --- a/tests/lean/change_tac_fail.lean.expected.out +++ b/tests/lean/change_tac_fail.lean.expected.out @@ -1,4 +1,4 @@ -change_tac_fail.lean:10:47: error: type mismatch at application +change_tac_fail.lean:10:48: error: type mismatch at application t ++ a term a diff --git a/tests/lean/empty_thm.lean b/tests/lean/empty_thm.lean index 47c975a06..1af981a5c 100644 --- a/tests/lean/empty_thm.lean +++ b/tests/lean/empty_thm.lean @@ -1,7 +1,7 @@ import logic open tactic -definition simple := apply trivial +definition simple := apply _root_.trivial tactic_hint simple diff --git a/tests/lean/run/def_tac.lean b/tests/lean/run/def_tac.lean index d160262ea..2f4f7ec82 100644 --- a/tests/lean/run/def_tac.lean +++ b/tests/lean/run/def_tac.lean @@ -1,15 +1,15 @@ context open tactic definition cases_refl (e : expr) : tactic := - cases e; apply rfl + cases e expr_list.nil; apply rfl definition cases_lst_refl : expr_list → tactic | cases_lst_refl expr_list.nil := apply rfl - | cases_lst_refl (expr_list.cons a l) := cases a; cases_lst_refl l + | cases_lst_refl (expr_list.cons a l) := cases a expr_list.nil; cases_lst_refl l -- Similar to cases_refl, but make sure the argument is not an arbitrary expression. definition eq_rec {A : Type} {a b : A} (e : a = b) : tactic := - cases e; apply rfl + cases e expr_list.nil; apply rfl end notation `cases_lst` l:(foldr `,` (h t, tactic.expr_list.cons h t) tactic.expr_list.nil) := cases_lst_refl l diff --git a/tests/lean/run/inf_tree3.lean b/tests/lean/run/inf_tree3.lean index c6eebb6e1..9daf53db4 100644 --- a/tests/lean/run/inf_tree3.lean +++ b/tests/lean/run/inf_tree3.lean @@ -14,7 +14,7 @@ namespace inftree (t : inftree A) (ht : acc dsub t) : acc dsub (node f t) := acc.intro (node f t) (λ (y : inftree A) (hlt : dsub y (node f t)), begin - inversion hlt, + cases hlt, apply (hf a), apply ht end) diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean index 1c27b8cd0..13bd2d991 100644 --- a/tests/lean/run/rename_tac.lean +++ b/tests/lean/run/rename_tac.lean @@ -12,7 +12,7 @@ end theorem foo2 (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := begin apply eq.trans, - Hab ↦ Foo, + rename Hab Foo, apply Foo, apply Hbc, end diff --git a/tests/lean/run/tactic_op_overload_bug.lean b/tests/lean/run/tactic_op_overload_bug.lean new file mode 100644 index 000000000..2a2e15307 --- /dev/null +++ b/tests/lean/run/tactic_op_overload_bug.lean @@ -0,0 +1,27 @@ +import data.num data.bool + +open bool well_founded + +namespace pos_num + +definition lt_pred (a b : pos_num) : Prop := lt a b = tt + +definition not_lt_one1 (a : pos_num) : ¬ lt_pred a one := +begin + esimp {lt_pred}, + intro H, + apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H) +end + +open tactic well_founded + +print raw intro -- intro is overloaded + +definition not_lt_one2 (a : pos_num) : ¬ lt_pred a one := +begin + esimp {lt_pred}, + intro H, + apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H) +end + +end pos_num