From a23118d357d08255652ec64fe90f62b58f5f9fa0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Apr 2015 17:46:13 -0700 Subject: [PATCH] feat(frontends/lean): add tactic_notation command This addresses the first part of issue #461 We still need support for tactic definitions --- hott/init/tactic.hlean | 13 +-- library/init/tactic.lean | 14 +-- src/emacs/lean-syntax.el | 6 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_exprs.cpp | 21 ---- src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/notation_cmd.cpp | 163 +++++++++++++++++---------- src/frontends/lean/parser.cpp | 36 ++---- src/frontends/lean/parser.h | 9 +- src/frontends/lean/parser_config.cpp | 77 +++++++++---- src/frontends/lean/parser_config.h | 15 ++- src/frontends/lean/token_table.cpp | 1 + tests/lean/errors.lean.expected.out | 3 +- tests/lean/run/all_goals2.lean | 5 +- tests/lean/run/by_exact.lean | 5 + tests/lean/run/def_tac.lean | 4 +- tests/lean/run/tac1.lean | 3 + tests/lean/run/tactic14.lean | 2 + tests/lean/run/tactic20.lean | 2 + tests/lean/run/tactic21.lean | 6 +- tests/lean/run/tactic22.lean | 6 +- tests/lean/run/tactic24.lean | 3 + tests/lean/run/tactic25.lean | 9 +- tests/lean/run/tactic26.lean | 3 + tests/lean/run/tactic27.lean | 2 + tests/lean/run/tactic28.lean | 3 + tests/lean/run/tactic4.lean | 5 +- tests/lean/run/tactic5.lean | 4 +- tests/lean/run/tactic7.lean | 2 +- tests/lean/run/tactic9.lean | 2 +- 30 files changed, 255 insertions(+), 174 deletions(-) create mode 100644 tests/lean/run/by_exact.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index d5d903d45..09f5139a9 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -96,15 +96,14 @@ opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin -infixl `;`:15 := and_then -notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r - -definition try (t : tactic) : tactic := (t | id) -definition repeat1 (t : tactic) : tactic := t ; repeat t +definition try (t : tactic) : tactic := or_else t id +definition repeat1 (t : tactic) : tactic := and_then 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 trivial : tactic := or_else (apply eq.refl) assumption definition do (n : num) (t : tactic) : tactic := -nat.rec id (λn t', (t;t')) (nat.of_num n) +nat.rec id (λn t', and_then t t') (nat.of_num n) end tactic +tactic_infixl `;`:15 := tactic.and_then +tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r diff --git a/library/init/tactic.lean b/library/init/tactic.lean index ed7d48e1f..b86f6ca6d 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -96,15 +96,13 @@ opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin -infixl `;`:15 := and_then -notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r - -definition try (t : tactic) : tactic := (t | id) -definition repeat1 (t : tactic) : tactic := t ; repeat t +definition try (t : tactic) : tactic := or_else t id +definition repeat1 (t : tactic) : tactic := and_then 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 trivial : tactic := or_else (or_else (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) - +nat.rec id (λn t', and_then t t') (nat.of_num n) end tactic +tactic_infixl `;`:15 := tactic.and_then +tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index f452933ec..a6dc5178a 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -13,9 +13,11 @@ "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "print" "theorem" "example" "abbreviation" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" - "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix" + "alias" "help" "environment" "options" "precedence" "reserve" "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match" - "infix" "infixl" "infixr" "notation" "eval" "check" "coercion" "end" + "infix" "infixl" "infixr" "notation" "postfix" "prefix" + "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix" + "eval" "check" "coercion" "end" "using" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "metaclasses" "raw" "migrate" "replacing") diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 210fd8f25..678ea90f0 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,7 +7,7 @@ begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp coercion_elaborator.cpp info_tactic.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp -parse_tactic_location.cpp parse_rewrite_tactic.cpp +parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 94718c3aa..a142a18bf 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -32,7 +32,6 @@ Author: Leonardo de Moura #include "frontends/lean/info_tactic.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/structure_cmd.h" -#include "frontends/lean/parse_rewrite_tactic.h" namespace lean { namespace notation { @@ -521,22 +520,6 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const & return parse_calc(p); } -static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { - return p.save_pos(parse_rewrite_tactic(p), pos); -} - -static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { - return p.save_pos(parse_esimp_tactic(p), pos); -} - -static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { - return p.save_pos(parse_unfold_tactic(p), pos); -} - -static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) { - return p.save_pos(parse_fold_tactic(p), pos); -} - static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) { name n = p.check_id_next("invalid '#' local notation, identifier expected"); environment env = overwrite_notation(p.env(), n); @@ -607,10 +590,6 @@ parse_table init_nud_table() { r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0); r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0); r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0); - r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0); - r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0); - r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); - r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0); diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 21c2384a9..98b2d9f2e 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/builtin_cmds.h" #include "frontends/lean/builtin_exprs.h" +#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/inductive_cmd.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/migrate_cmd.h" @@ -37,6 +38,7 @@ void initialize_frontend_lean_module() { initialize_parse_table(); initialize_builtin_cmds(); initialize_builtin_exprs(); + initialize_builtin_tactics(); initialize_elaborator_context(); initialize_elaborator(); initialize_scanner(); @@ -75,6 +77,7 @@ void finalize_frontend_lean_module() { finalize_scanner(); finalize_elaborator(); finalize_elaborator_context(); + finalize_builtin_tactics(); finalize_builtin_exprs(); finalize_builtin_cmds(); finalize_parse_table(); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 2d20b4ffc..978901842 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -96,7 +96,7 @@ void check_not_forbidden(char const * tk) { } } -static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve, bool parse_only) +static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only) -> pair> { std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected"); char const * tks = tk.c_str(); @@ -107,7 +107,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool optional reserved_pt; optional reserved_action; - if (!reserve) { + if (grp != notation_entry_group::Reserve) { if (k == mixfix_kind::prefix) { if (auto at = get_reserved_nud_table(p.env()).find(tks)) { reserved_pt = at->second; @@ -178,7 +178,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool } } - if (reserve) { + if (grp == notation_entry_group::Reserve) { // reserve notation commands do not have a denotation expr dummy = mk_Prop(); if (p.curr_is_token(get_assign_tk())) @@ -186,16 +186,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool switch (k) { case mixfix_kind::infixl: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - dummy, overload, reserve, parse_only), new_token); + dummy, overload, grp, parse_only), new_token); case mixfix_kind::infixr: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - dummy, overload, reserve, parse_only), new_token); + dummy, overload, grp, parse_only), new_token); case mixfix_kind::postfix: return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), - dummy, overload, reserve, parse_only), new_token); + dummy, overload, grp, parse_only), new_token); case mixfix_kind::prefix: return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), - dummy, overload, reserve, parse_only), new_token); + dummy, overload, grp, parse_only), new_token); } } else { p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected"); @@ -207,25 +207,25 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token); + mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token); #endif case mixfix_kind::infixr: return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token); + mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token); case mixfix_kind::postfix: return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())), - mk_app(f, Var(0)), overload, reserve, parse_only), new_token); + mk_app(f, Var(0)), overload, grp, parse_only), new_token); case mixfix_kind::prefix: return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))), - mk_app(f, Var(0)), overload, reserve, parse_only), new_token); + mk_app(f, Var(0)), overload, grp, parse_only), new_token); } } lean_unreachable(); // LCOV_EXCL_LINE } -static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve, +static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, buffer & new_tokens, bool parse_only) { - auto nt = parse_mixfix_notation(p, k, overload, reserve, parse_only); + auto nt = parse_mixfix_notation(p, k, overload, grp, parse_only); if (nt.second) new_tokens.push_back(*nt.second); return nt.first; @@ -416,7 +416,7 @@ static unsigned parse_binders_rbp(parser & p) { } } -static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer & new_tokens, bool parse_only) { +static notation_entry parse_notation_core(parser & p, bool overload, notation_entry_group grp, buffer & new_tokens, bool parse_only) { buffer locals; buffer ts; parser::local_scope scope(p); @@ -436,16 +436,16 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv parse_notation_local(p, locals); is_nud = false; pt = get_led_table(p.env()); - if (!reserve) + if (grp != notation_entry_group::Reserve) reserved_pt = get_reserved_led_table(p.env()); } else { pt = get_nud_table(p.env()); - if (!reserve) + if (grp != notation_entry_group::Reserve) reserved_pt = get_reserved_nud_table(p.env()); } bool used_default = false; - while ((!reserve && !p.curr_is_token(get_assign_tk())) || - (reserve && !p.curr_is_command() && !p.curr_is_eof())) { + while ((grp != notation_entry_group::Reserve && !p.curr_is_token(get_assign_tk())) || + (grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) { name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default); if (auto at = find_next(reserved_pt, tk)) { action const & a = at->first; @@ -521,7 +521,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv new_tokens.back().m_prec = get_max_prec(); } expr n; - if (reserve) { + if (grp == notation_entry_group::Reserve) { // reserve notation commands do not have a denotation lean_assert(p.curr_is_command() || p.curr_is_eof()); expr dummy = mk_Prop(); // any expression without free variables will do @@ -533,7 +533,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos()); n = parse_notation_expr(p, locals); } - return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, parse_only); + return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, grp, parse_only); } bool curr_is_notation_decl(parser & p) { @@ -542,25 +542,25 @@ bool curr_is_notation_decl(parser & p) { p.curr_is_token(get_postfix_tk()) || p.curr_is_token(get_prefix_tk()) || p.curr_is_token(get_notation_tk()); } -static notation_entry parse_notation(parser & p, bool overload, bool reserve, buffer & new_tokens, +static notation_entry parse_notation(parser & p, bool overload, notation_entry_group grp, buffer & new_tokens, bool allow_local) { bool parse_only = false; flet set_allow_local(g_allow_local, allow_local); if (p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::infixl, overload, reserve, new_tokens, parse_only); + return parse_mixfix_notation(p, mixfix_kind::infixl, overload, grp, new_tokens, parse_only); } else if (p.curr_is_token(get_infixr_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::infixr, overload, reserve, new_tokens, parse_only); + return parse_mixfix_notation(p, mixfix_kind::infixr, overload, grp, new_tokens, parse_only); } else if (p.curr_is_token(get_postfix_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::postfix, overload, reserve, new_tokens, parse_only); + return parse_mixfix_notation(p, mixfix_kind::postfix, overload, grp, new_tokens, parse_only); } else if (p.curr_is_token(get_prefix_tk())) { p.next(); - return parse_mixfix_notation(p, mixfix_kind::prefix, overload, reserve, new_tokens, parse_only); + return parse_mixfix_notation(p, mixfix_kind::prefix, overload, grp, new_tokens, parse_only); } else if (p.curr_is_token(get_notation_tk())) { p.next(); - return parse_notation_core(p, overload, reserve, new_tokens, parse_only); + return parse_notation_core(p, overload, grp, new_tokens, parse_only); } else { throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', " "'postfix' or 'notation' expected", p.pos()); @@ -568,8 +568,8 @@ static notation_entry parse_notation(parser & p, bool overload, bool reserve, bu } notation_entry parse_notation(parser & p, bool overload, buffer & new_tokens, bool allow_local) { - bool reserve = false; - return parse_notation(p, overload, reserve, new_tokens, allow_local); + notation_entry_group grp = notation_entry_group::Main; + return parse_notation(p, overload, grp, new_tokens, allow_local); } static char g_reserved_chars[] = {'(', ')', ',', 0}; @@ -624,24 +624,24 @@ struct notation_modifiers { } }; -static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) { +static environment notation_cmd_core(parser & p, bool overload, notation_entry_group grp, bool persistent) { notation_modifiers mods; mods.parse(p); flet set_allow_local(g_allow_local, !persistent); environment env = p.env(); buffer new_tokens; - auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only); + auto ne = parse_notation_core(p, overload, grp, new_tokens, mods.m_parse_only); for (auto const & te : new_tokens) env = add_user_token(env, te, persistent); env = add_notation(env, ne, persistent); return env; } -static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) { +static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool persistent) { notation_modifiers mods; mods.parse(p); flet set_allow_local(g_allow_local, !persistent); - auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only); + auto nt = parse_mixfix_notation(p, k, overload, grp, mods.m_parse_only); environment env = p.env(); if (nt.second) env = add_user_token(env, *nt.second, persistent); @@ -651,59 +651,94 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool res static environment notation_cmd(parser & p) { bool overload = true; - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = true; - return notation_cmd_core(p, overload, reserve, persistent); + return notation_cmd_core(p, overload, grp, persistent); } static environment infixl_cmd(parser & p) { bool overload = true; - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = true; - return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent); } static environment infixr_cmd(parser & p) { bool overload = true; - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = true; - return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent); } static environment postfix_cmd(parser & p) { bool overload = true; - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = true; - return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent); } static environment prefix_cmd(parser & p) { bool overload = true; - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = true; - return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent); +} + +static environment tactic_notation_cmd(parser & p) { + bool overload = false; + notation_entry_group grp = notation_entry_group::Tactic; + bool persistent = true; + return notation_cmd_core(p, overload, grp, persistent); +} + +static environment tactic_infixl_cmd(parser & p) { + bool overload = false; + notation_entry_group grp = notation_entry_group::Tactic; + bool persistent = true; + return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent); +} + +static environment tactic_infixr_cmd(parser & p) { + bool overload = false; + notation_entry_group grp = notation_entry_group::Tactic; + bool persistent = true; + return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent); +} + +static environment tactic_postfix_cmd(parser & p) { + bool overload = false; + notation_entry_group grp = notation_entry_group::Tactic; + bool persistent = true; + return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent); +} + +static environment tactic_prefix_cmd(parser & p) { + bool overload = false; + notation_entry_group grp = notation_entry_group::Tactic; + bool persistent = true; + return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent); } // auxiliary procedure used by local_notation_cmd and reserve_cmd -static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve, bool persistent) { +static environment dispatch_notation_cmd(parser & p, bool overload, notation_entry_group grp, bool persistent) { if (p.curr_is_token(get_notation_tk())) { p.next(); - return notation_cmd_core(p, overload, reserve, persistent); + return notation_cmd_core(p, overload, grp, persistent); } else if (p.curr_is_token(get_infixl_tk())) { p.next(); - return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent); } else if (p.curr_is_token(get_infix_tk())) { p.next(); - return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent); } else if (p.curr_is_token(get_infixr_tk())) { p.next(); - return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent); } else if (p.curr_is_token(get_prefix_tk())) { p.next(); - return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent); } else if (p.curr_is_token(get_postfix_tk())) { p.next(); - return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent); + return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent); } else { throw parser_error("invalid local/reserve notation, 'infix', 'infixl', 'infixr', 'prefix', " "'postfix' or 'notation' expected", p.pos()); @@ -712,16 +747,16 @@ static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve environment local_notation_cmd(parser & p) { bool overload = false; // REMARK: local notation override global one - bool reserve = false; + notation_entry_group grp = notation_entry_group::Main; bool persistent = false; - return dispatch_notation_cmd(p, overload, reserve, persistent); + return dispatch_notation_cmd(p, overload, grp, persistent); } static environment reserve_cmd(parser & p) { bool overload = false; - bool reserve = true; + notation_entry_group grp = notation_entry_group::Reserve; bool persistent = true; - return dispatch_notation_cmd(p, overload, reserve, persistent); + return dispatch_notation_cmd(p, overload, grp, persistent); } static environment precedence_cmd(parser & p) { @@ -732,13 +767,19 @@ static environment precedence_cmd(parser & p) { } void register_notation_cmds(cmd_table & r) { - add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd)); - add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd)); - add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd)); - add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd)); - add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd)); - add_cmd(r, cmd_info("prefix", "declare a new prefix notation", prefix_cmd)); - add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd)); - add_cmd(r, cmd_info("reserve", "reserve notation", reserve_cmd)); + add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd)); + add_cmd(r, cmd_info("infixl", "declare a new infix (left) notation", infixl_cmd)); + add_cmd(r, cmd_info("infix", "declare a new infix (left) notation", infixl_cmd)); + add_cmd(r, cmd_info("infixr", "declare a new infix (right) notation", infixr_cmd)); + add_cmd(r, cmd_info("postfix", "declare a new postfix notation", postfix_cmd)); + add_cmd(r, cmd_info("prefix", "declare a new prefix notation", prefix_cmd)); + add_cmd(r, cmd_info("notation", "declare a new notation", notation_cmd)); + add_cmd(r, cmd_info("tactic_infixl", "declare a new tactic infix (left) notation", tactic_infixl_cmd)); + add_cmd(r, cmd_info("tactic_infix", "declare a new tactic infix (left) notation", tactic_infixl_cmd)); + add_cmd(r, cmd_info("tactic_infixr", "declare a new tactic infix (right) notation", tactic_infixr_cmd)); + add_cmd(r, cmd_info("tactic_postfix", "declare a new tactic postfix notation", tactic_postfix_cmd)); + add_cmd(r, cmd_info("tactic_prefix", "declare a new tactic prefix notation", tactic_prefix_cmd)); + add_cmd(r, cmd_info("tactic_notation", "declare a new tacitc notation", tactic_notation_cmd)); + add_cmd(r, cmd_info("reserve", "reserve notation", reserve_cmd)); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b1fcea993..972566d00 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -925,7 +925,7 @@ bool parser::parse_local_notation_decl(buffer * nentries) { } } -expr parser::parse_notation(parse_table t, expr * left) { +expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { lean_assert(curr() == scanner::token_kind::Keyword); auto p = pos(); if (m_info_manager) @@ -949,17 +949,17 @@ expr parser::parse_notation(parse_table t, expr * left) { break; case notation::action_kind::Expr: next(); - args.push_back(parse_expr(a.rbp())); + args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic)); break; case notation::action_kind::Exprs: { next(); buffer r_args; auto terminator = a.get_terminator(); if (!terminator || !curr_is_token(*terminator)) { - r_args.push_back(parse_expr(a.rbp())); + r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic)); while (curr_is_token(a.get_sep())) { next(); - r_args.push_back(parse_expr(a.rbp())); + r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic)); } } if (terminator) { @@ -1473,34 +1473,18 @@ expr parser::parse_tactic_nud() { } else { return parse_expr(); } - } 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(); - 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_rparen_tk(), "invalid tactic, ')' expected"); - return r; + } else if (curr_is_keyword()) { + return parse_tactic_notation(tactic_nud(), nullptr); } else { - return parse_expr(); + throw parser_error("invalid tactic expression", pos()); } } 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); + if (tactic_led().find(get_token_info().value())) { + return parse_tactic_notation(tactic_led(), &left); } else { - return parse_led(left); + throw parser_error("invalid tactic expression", pos()); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index f87fa3257..a882f4416 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -169,6 +169,8 @@ class parser { parse_table const & nud() const { return get_nud_table(env()); } parse_table const & led() const { return get_led_table(env()); } + parse_table const & tactic_nud() const { return get_tactic_nud_table(env()); } + parse_table const & tactic_led() const { return get_tactic_led_table(env()); } unsigned curr_level_lbp() const; level parse_max_imax(bool is_max); @@ -181,7 +183,12 @@ class parser { void parse_script(bool as_expr = false); bool parse_commands(); unsigned curr_lbp() const; - expr parse_notation(parse_table t, expr * left); + expr parse_notation_core(parse_table t, expr * left, bool as_tactic); + expr parse_expr_or_tactic(unsigned rbp, bool as_tactic) { + return as_tactic ? parse_tactic(rbp) : parse_expr(rbp); + } + expr parse_notation(parse_table t, expr * left) { return parse_notation_core(t, left, false); } + expr parse_tactic_notation(parse_table t, expr * left) { return parse_notation_core(t, left, true); } expr parse_nud_notation(); expr parse_led_notation(expr left); expr parse_nud(); diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 0e2ad05cb..491530372 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "frontends/lean/parser_config.h" #include "frontends/lean/builtin_exprs.h" +#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/builtin_cmds.h" namespace lean { @@ -24,22 +25,23 @@ notation_entry replace(notation_entry const & e, std::function(e.m_transitions); } -notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve, bool parse_only): +notation_entry::notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, + notation_entry_group g, bool parse_only): m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD), - m_expr(e), m_overload(overload), m_reserve(reserve), m_parse_only(parse_only) { + m_expr(e), m_overload(overload), m_group(g), m_parse_only(parse_only) { new (&m_transitions) list(ts); m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); }); } @@ -48,7 +50,7 @@ notation_entry::notation_entry(notation_entry const & e, bool overload): m_overload = overload; } notation_entry::notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only): - m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false), m_parse_only(parse_only) { + m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_group(notation_entry_group::Main), m_parse_only(parse_only) { new (&m_num) mpz(val); } @@ -61,7 +63,7 @@ notation_entry::~notation_entry() { bool operator==(notation_entry const & e1, notation_entry const & e2) { if (e1.kind() != e2.kind() || e1.overload() != e2.overload() || e1.get_expr() != e2.get_expr() || - e1.reserve() != e2.reserve() || e1.parse_only() != e2.parse_only()) + e1.group() != e2.group() || e1.parse_only() != e2.parse_only()) return false; if (e1.is_numeral()) return e1.get_num() == e2.get_num(); @@ -213,11 +215,34 @@ struct notation_state { // The following two tables are used to implement `reserve notation` commands parse_table m_reserved_nud; parse_table m_reserved_led; + // The following two tables are used to implement `notation [tactic]` commands + parse_table m_tactic_nud; + parse_table m_tactic_led; notation_state(): m_nud(get_builtin_nud_table()), m_led(get_builtin_led_table()), m_reserved_nud(true), - m_reserved_led(false) { + m_reserved_led(false), + m_tactic_nud(get_builtin_tactic_nud_table()), + m_tactic_led(get_builtin_tactic_led_table()) { + } + + parse_table & nud(notation_entry_group g) { + switch (g) { + case notation_entry_group::Main: return m_nud; + case notation_entry_group::Reserve: return m_reserved_nud; + case notation_entry_group::Tactic: return m_tactic_nud; + } + lean_unreachable(); + } + + parse_table & led(notation_entry_group g) { + switch (g) { + case notation_entry_group::Main: return m_led; + case notation_entry_group::Reserve: return m_reserved_led; + case notation_entry_group::Tactic: return m_tactic_led; + } + lean_unreachable(); } }; @@ -239,7 +264,7 @@ struct notation_config { to_buffer(e.get_transitions(), ts); if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr())) updt_inv_map(s, *idx, e); - parse_table & nud = e.reserve() ? s.m_reserved_nud : s.m_nud; + parse_table & nud = s.nud(e.group()); nud = nud.add(ts.size(), ts.data(), e.get_expr(), e.overload()); break; } @@ -247,7 +272,7 @@ struct notation_config { to_buffer(e.get_transitions(), ts); if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr())) updt_inv_map(s, *idx, e); - parse_table & led = e.reserve() ? s.m_reserved_led : s.m_led; + parse_table & led = s.led(e.group()); led = led.add(ts.size(), ts.data(), e.get_expr(), e.overload()); break; } @@ -275,7 +300,7 @@ struct notation_config { if (e.is_numeral()) { s << e.get_num(); } else { - s << e.reserve() << length(e.get_transitions()); + s << static_cast(e.group()) << length(e.get_transitions()); for (auto const & t : e.get_transitions()) s << t; } @@ -290,13 +315,13 @@ struct notation_config { return entry(val, e, overload, parse_only); } else { bool is_nud = k == notation_entry_kind::NuD; - bool reserve; - unsigned sz; - d >> reserve >> sz; + unsigned sz; char _g; + d >> _g >> sz; + notation_entry_group g = static_cast(_g); buffer ts; for (unsigned i = 0; i < sz; i++) ts.push_back(read_transition(d)); - return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve, parse_only); + return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, g, parse_only); } } static optional get_fingerprint(entry const &) { @@ -314,25 +339,25 @@ environment add_notation(environment const & env, notation_entry const & e, bool } environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, - expr const & a, bool overload, bool reserve, bool parse_only) { - return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve, parse_only)); + expr const & a, bool overload, notation_entry_group g, bool parse_only) { + return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, g, parse_only)); } environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, - expr const & a, bool overload, bool reserve, bool parse_only) { - return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve, parse_only)); + expr const & a, bool overload, notation_entry_group g, bool parse_only) { + return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, g, parse_only)); } environment add_nud_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload, bool parse_only) { - bool reserve = false; - return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only); + notation_entry_group g = notation_entry_group::Main; + return add_nud_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only); } environment add_led_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload, bool parse_only) { - bool reserve = false; - return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only); + notation_entry_group g = notation_entry_group::Main; + return add_led_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only); } parse_table const & get_nud_table(environment const & env) { @@ -351,6 +376,14 @@ parse_table const & get_reserved_led_table(environment const & env) { return notation_ext::get_state(env).m_reserved_led; } +parse_table const & get_tactic_nud_table(environment const & env) { + return notation_ext::get_state(env).m_tactic_nud; +} + +parse_table const & get_tactic_led_table(environment const & env) { + return notation_ext::get_state(env).m_tactic_led; +} + environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload, bool parse_only) { return add_notation(env, notation_entry(n, e, overload, parse_only)); } diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 8b6df5f60..6c3d43f6e 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -19,7 +19,7 @@ struct token_entry { }; enum class notation_entry_kind { NuD, LeD, Numeral }; - +enum class notation_entry_group { Main, Reserve, Tactic }; class notation_entry { typedef notation::transition transition; notation_entry_kind m_kind; @@ -30,12 +30,12 @@ class notation_entry { expr m_expr; bool m_overload; bool m_safe_ascii; - bool m_reserve; + notation_entry_group m_group; bool m_parse_only; public: notation_entry(); notation_entry(notation_entry const & e); - notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, bool reserve, bool parse_only); + notation_entry(bool is_nud, list const & ts, expr const & e, bool overload, notation_entry_group g, bool parse_only); notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only); notation_entry(notation_entry const & e, bool overload); ~notation_entry(); @@ -47,7 +47,8 @@ public: expr const & get_expr() const { return m_expr; } bool overload() const { return m_overload; } bool is_safe_ascii() const { return m_safe_ascii; } - bool reserve() const { return m_reserve; } + notation_entry_group group() const { return m_group; } + bool reserve() const { return group() == notation_entry_group::Reserve; } bool parse_only() const { return m_parse_only; } }; bool operator==(notation_entry const & e1, notation_entry const & e2); @@ -63,9 +64,9 @@ environment add_notation(environment const & env, notation_entry const & e, bool environment add_token(environment const & env, char const * val, unsigned prec); environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, - bool overload = true, bool reserve = false, bool parse_only = false); + bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false); environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a, - bool overload = true, bool reserve = false, bool parse_only = false); + bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false); environment add_nud_notation(environment const & env, std::initializer_list const & ts, expr const & a, bool overload = true, bool parse_only = false); environment add_led_notation(environment const & env, std::initializer_list const & ts, expr const & a, @@ -75,6 +76,8 @@ parse_table const & get_nud_table(environment const & env); parse_table const & get_led_table(environment const & env); parse_table const & get_reserved_nud_table(environment const & env); parse_table const & get_reserved_led_table(environment const & env); +parse_table const & get_tactic_nud_table(environment const & env); +parse_table const & get_tactic_led_table(environment const & env); cmd_table const & get_cmd_table(environment const & env); /** \brief Force notation from namespace \c n to shadow any existing notation */ environment overwrite_notation(environment const & env, name const & n); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 4eb536903..58e23d180 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -97,6 +97,7 @@ void init_token_table(token_table & t) { "end", "namespace", "section", "prelude", "help", "import", "inductive", "record", "structure", "module", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", + "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out index 92616c448..2cc5b45bd 100644 --- a/tests/lean/errors.lean.expected.out +++ b/tests/lean/errors.lean.expected.out @@ -1,7 +1,6 @@ errors.lean:4:0: error: unknown identifier 'a' tst1 : nat → nat → nat -errors.lean:12:2: error: function expected at - tactic.cases [tactic.expr add] tactic.expr_list.nil +errors.lean:12:12: error: invalid tactic expression errors.lean:22:12: error: unknown identifier 'b' tst3 : A → A → A foo.tst1 : ℕ → ℕ → ℕ diff --git a/tests/lean/run/all_goals2.lean b/tests/lean/run/all_goals2.lean index eca448e6f..3a5aec2c4 100644 --- a/tests/lean/run/all_goals2.lean +++ b/tests/lean/run/all_goals2.lean @@ -4,12 +4,15 @@ open nat attribute nat.add [unfold-c 2] attribute nat.rec_on [unfold-c 2] +infixl `;`:15 := tactic.and_then + namespace tactic definition then_all (t1 t2 : tactic) : tactic := focus (t1 ; all_goals t2) - infixl `;;`:15 := tactic.then_all end tactic +tactic_infixl `;;`:15 := tactic.then_all + open tactic example (a b c : nat) : (a + 0 = 0 + a ∧ b + 0 = 0 + b) ∧ c = c := diff --git a/tests/lean/run/by_exact.lean b/tests/lean/run/by_exact.lean new file mode 100644 index 000000000..7e111ec94 --- /dev/null +++ b/tests/lean/run/by_exact.lean @@ -0,0 +1,5 @@ +import data.nat +open nat + +example (a b c : nat) (h₁ : a + 0 = b) (h₂ : b = c) : a = c := +by esimp at h₁; rewrite h₂ at h₁; exact h₁ diff --git a/tests/lean/run/def_tac.lean b/tests/lean/run/def_tac.lean index 360d31d70..e0ecf8ca1 100644 --- a/tests/lean/run/def_tac.lean +++ b/tests/lean/run/def_tac.lean @@ -1,3 +1,5 @@ +infixl `;`:15 := tactic.and_then + section open tactic definition cases_refl (e : expr) : tactic := @@ -12,7 +14,7 @@ section 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 +tactic_notation `cases_lst` l:(foldr `,` (h t, tactic.expr_list.cons h t) tactic.expr_list.nil) := cases_lst_refl l open prod theorem tst₁ (a : nat × nat) : (pr1 a, pr2 a) = a := diff --git a/tests/lean/run/tac1.lean b/tests/lean/run/tac1.lean index be4747664..38607dee4 100644 --- a/tests/lean/run/tac1.lean +++ b/tests/lean/run/tac1.lean @@ -1,6 +1,9 @@ import logic open tactic +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + definition mytac := apply @and.intro; apply @eq.refl check @mytac diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index 1567b7e84..e0defea4e 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -1,6 +1,8 @@ import logic open tactic +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r + definition basic_tac : tactic := repeat (apply @and.intro | assumption) diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean index 9f7e5ac0a..c509a25d2 100644 --- a/tests/lean/run/tactic20.lean +++ b/tests/lean/run/tactic20.lean @@ -1,6 +1,8 @@ import logic open tactic +infixl `;`:15 := tactic.and_then + definition assump := eassumption theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean index 5a4e7277e..2119b8334 100644 --- a/tests/lean/run/tactic21.lean +++ b/tests/lean/run/tactic21.lean @@ -1,13 +1,11 @@ import logic open tactic -definition assump := eassumption - theorem tst1 {A : Type} {a b c : A} {p : A → A → Prop} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c -:= by apply exists.intro; apply and.intro; assump; assump +:= by apply exists.intro; apply and.intro; eassumption; eassumption theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c -:= by apply exists.intro; apply and.intro; assump; assump +:= by apply exists.intro; apply and.intro; eassumption; eassumption (* print(get_env():find("tst2"):value()) diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean index 9400e0378..51c555546 100644 --- a/tests/lean/run/tactic22.lean +++ b/tests/lean/run/tactic22.lean @@ -1,5 +1,9 @@ import logic open tactic +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + + theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d -:= by fixpoint (λ f, (apply @and.intro; f | assumption; f | id)) +:= by fixpoint (λ f, (apply and.intro; f | assumption; f | id)) diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index e64aca3d5..3c09f9bf1 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -1,6 +1,9 @@ import logic open tactic +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + definition my_tac1 := apply @eq.refl definition my_tac2 := repeat (apply @and.intro; assumption) diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index e6fc9d682..dfbd29bac 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -2,7 +2,7 @@ import logic open tactic definition my_tac1 := apply @eq.refl -definition my_tac2 := repeat (apply @and.intro; assumption) +definition my_tac2 := repeat (and_then (apply and.intro) assumption) tactic_hint my_tac1 tactic_hint my_tac2 @@ -11,8 +11,11 @@ theorem T1 {A : Type.{2}} (a : A) : a = a theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c -definition my_tac3 := fixpoint (λ f, (apply @or.intro_left; f | - apply @or.intro_right; f | +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + +definition my_tac3 := fixpoint (λ f, (apply or.intro_left; f | + apply or.intro_right; f | assumption)) tactic_hint my_tac3 diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean index 7f86e364d..70e229eba 100644 --- a/tests/lean/run/tactic26.lean +++ b/tests/lean/run/tactic26.lean @@ -12,6 +12,9 @@ theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B) := inhabited.destruct H (λ b, inhabited.mk (sum.inr A b)) +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + definition my_tac := fixpoint (λ t, ( apply @inl_inhabited; t | apply @inr_inhabited; t | apply @num.is_inhabited diff --git a/tests/lean/run/tactic27.lean b/tests/lean/run/tactic27.lean index 6eff6ea7f..318f63677 100644 --- a/tests/lean/run/tactic27.lean +++ b/tests/lean/run/tactic27.lean @@ -1,6 +1,8 @@ import logic open tactic +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r + definition my_tac := repeat (apply @and.intro | apply @eq.refl) tactic_hint my_tac diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean index 31663a239..0f1e51c7f 100644 --- a/tests/lean/run/tactic28.lean +++ b/tests/lean/run/tactic28.lean @@ -14,6 +14,9 @@ theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A infixl `..`:10 := append +notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +infixl `;`:15 := tactic.and_then + definition my_tac := repeat (trace "iteration"; state; ( apply @inl_inhabited; trace "used inl" .. apply @inr_inhabited; trace "used inr" diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean index af0d13976..e5a3a39e1 100644 --- a/tests/lean/run/tactic4.lean +++ b/tests/lean/run/tactic4.lean @@ -3,10 +3,7 @@ open tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a -definition simple {A : Prop} : tactic -:= unfold id; assumption - theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A -:= by simple +:= by unfold id; assumption check tst diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean index 268cdc81e..41387388e 100644 --- a/tests/lean/run/tactic5.lean +++ b/tests/lean/run/tactic5.lean @@ -3,7 +3,9 @@ open tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a +infixl `;`:15 := tactic.and_then + theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A -:= by !(unfold id; state); assumption +:= by (unfold id; state); assumption check tst diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index cb7aed129..c0a1fd57c 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -2,7 +2,7 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by apply and.intro; state; assumption; apply and.intro; !assumption +:= by apply and.intro; state; assumption; apply and.intro; assumption check tst theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean index ce73ab2f3..ea0c23790 100644 --- a/tests/lean/run/tactic9.lean +++ b/tests/lean/run/tactic9.lean @@ -2,4 +2,4 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A -:= by apply and.intro; beta; assumption; apply and.intro; !assumption +:= by apply and.intro; beta; assumption; apply and.intro; assumption