From c845e44777e4bc3ea27cd5a2bb246de58c1302a5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Feb 2015 17:02:14 -0800 Subject: [PATCH] feat(frontends/lean): parse rewrite tactic --- hott/init/reserved_notation.hlean | 1 + hott/init/tactic.hlean | 3 + library/init/reserved_notation.lean | 1 + library/init/tactic.lean | 3 + src/emacs/lean-syntax.el | 4 +- src/frontends/lean/CMakeLists.txt | 1 + src/frontends/lean/builtin_exprs.cpp | 6 ++ src/frontends/lean/parse_rewrite_tactic.cpp | 64 ++++++++++++++++++++ src/frontends/lean/parse_rewrite_tactic.h | 13 ++++ src/frontends/lean/parse_tactic_location.cpp | 27 ++++----- src/frontends/lean/token_table.cpp | 8 +-- src/frontends/lean/tokens.cpp | 28 +++++++++ src/frontends/lean/tokens.h | 7 +++ src/library/tactic/rewrite_tactic.cpp | 14 +++-- 14 files changed, 156 insertions(+), 24 deletions(-) create mode 100644 src/frontends/lean/parse_rewrite_tactic.cpp create mode 100644 src/frontends/lean/parse_rewrite_tactic.h diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index cf86c21f05..a4cddb53e8 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -56,6 +56,7 @@ reserve infixl `-`:65 reserve infixl `*`:70 reserve infixl `div`:70 reserve infixl `mod`:70 +reserve infixl `/`:70 reserve prefix `-`:100 reserve infix `<=`:50 diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 27be915884..aa5722287f 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -62,6 +62,9 @@ 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 +-- rewrite_tac is just a marker for the builtin 'rewrite' notation +-- used to create instances of this tactic. +opaque definition rewrite_tac (e : expr) : tactic := builtin notation a `↦` b:max := rename a b diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 019fb5a565..859e4e3593 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -65,6 +65,7 @@ reserve infixl `-`:65 reserve infixl `*`:70 reserve infixl `div`:70 reserve infixl `mod`:70 +reserve infixl `/`:70 reserve prefix `-`:100 reserve infix `<=`:50 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 739731e0e7..3163780d2b 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -63,6 +63,9 @@ 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 +-- rewrite_tac is just a marker for the builtin 'rewrite' notation +-- used to create instances of this tactic. +opaque definition rewrite_tac (e : expr) : tactic := builtin notation a `↦` b:max := rename a b diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 331bb62e8e..51c245fcbc 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -96,7 +96,7 @@ (defconst lean-font-lock-defaults `((;; Keywords - (,(rx word-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun" + (,(rx word-start (or "calc" "have" "obtains" "show" "by" "in" "at" "let" "forall" "fun" "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from") word-end) . font-lock-keyword-face) ;; String @@ -126,7 +126,7 @@ (,(rx (not (any "\.")) word-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros" "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" - "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert") + "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert" "rewrite") word-end) . 'font-lock-constant-face) ;; Types diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index db3487f79d..990c2b0b9d 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,6 +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 proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp +parse_tactic_location.cpp parse_rewrite_tactic.cpp type_util.cpp elaborator_exception.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 ce8bbe87ef..71b03e327a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -31,6 +31,7 @@ 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 { @@ -419,6 +420,10 @@ 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_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); @@ -488,6 +493,7 @@ 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("#", 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/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp new file mode 100644 index 0000000000..3c4fafe53f --- /dev/null +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -0,0 +1,64 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/tactic/rewrite_tactic.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/tokens.h" +#include "frontends/lean/parse_tactic_location.h" + +namespace lean { +name parse_rewrite_element_id(parser & p) { + return p.check_id_next("invalid rewrite tactic step, identifier expected"); +} + +rewrite_element parse_rewrite_element(parser & p) { + if (p.curr_is_token(get_slash_tk())) { + p.next(); + return rewrite_element::mk_unfold(p.check_id_next("invalid unfold rewrite step, identifier expected")); + } + bool symm = false; + if (p.curr_is_token(get_sub_tk())) { + p.next(); + symm = true; + } + if (p.curr_is_numeral()) { + unsigned n = p.parse_small_nat(); + if (p.curr_is_token(get_question_tk())) { + p.next(); + return rewrite_element::mk_at_most_n(parse_rewrite_element_id(p), n, symm); + } else if (p.curr_is_token(get_bang_tk())) { + p.next(); + return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm); + } else { + return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm); + } + } else if (p.curr_is_token(get_question_tk())) { + p.next(); + return rewrite_element::mk_zero_or_more(parse_rewrite_element_id(p), symm); + } else if (p.curr_is_token(get_bang_tk())) { + p.next(); + return rewrite_element::mk_one_or_more(parse_rewrite_element_id(p), symm); + } else { + return rewrite_element::mk_once(parse_rewrite_element_id(p), symm); + } +} + +expr parse_rewrite_tactic(parser & p) { + buffer elems; + while (true) { + elems.push_back(parse_rewrite_element(p)); + if (!p.curr_is_token(get_sub_tk()) && + !p.curr_is_numeral() && + !p.curr_is_token(get_bang_tk()) && + !p.curr_is_token(get_question_tk()) && + !p.curr_is_token(get_slash_tk()) && + !p.curr_is_identifier()) + break; + } + location loc = parse_tactic_location(p); + return mk_rewrite_tactic_expr(elems, loc); +} +} diff --git a/src/frontends/lean/parse_rewrite_tactic.h b/src/frontends/lean/parse_rewrite_tactic.h new file mode 100644 index 0000000000..ab81f494a7 --- /dev/null +++ b/src/frontends/lean/parse_rewrite_tactic.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" + +namespace lean { +class parser; +expr parse_rewrite_tactic(parser & p); +} diff --git a/src/frontends/lean/parse_tactic_location.cpp b/src/frontends/lean/parse_tactic_location.cpp index dcacb2ff02..c17cd307f1 100644 --- a/src/frontends/lean/parse_tactic_location.cpp +++ b/src/frontends/lean/parse_tactic_location.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { static occurrence parse_occurrence(parser & p) { - if (p.curr_is_token(get_at_tk())) { + if (p.curr_is_token(get_lcurly_tk())) { p.next(); bool has_pos = false; bool has_neg = false; @@ -30,9 +30,10 @@ static occurrence parse_occurrence(parser & p) { throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos); has_pos = true; } - if (!p.curr_is_token(get_sub_tk()) && !p.curr_is_numeral()) + if (p.curr_is_token(get_rcurly_tk())) break; } + p.next(); if (has_pos) return occurrence::mk_occurrences(occs); else @@ -43,44 +44,42 @@ static occurrence parse_occurrence(parser & p) { } location parse_tactic_location(parser & p) { - if (p.curr_is_token(get_in_tk())) { + if (p.curr_is_token(get_at_tk())) { p.next(); if (p.curr_is_token(get_star_tk())) { p.next(); if (p.curr_is_token(get_turnstile_tk())) { p.next(); if (p.curr_is_token(get_star_tk())) { - // in * |- * + // at * |- * return location::mk_everywhere(); } else { - // in * |- + // at * |- return location::mk_all_hypotheses(); } } else { - // in * + // at * return location::mk_everywhere(); } } else { buffer hyps; buffer hyp_occs; - while (true) { + while (p.curr_is_identifier()) { hyps.push_back(p.get_name_val()); p.next(); hyp_occs.push_back(parse_occurrence(p)); - if (!p.curr_is_token(get_comma_tk())) - break; - p.next(); } - if (p.curr_is_token(get_turnstile_tk())) { + if (hyps.empty()) { + occurrence o = parse_occurrence(p); + return location::mk_goal_at(o); + } else if (p.curr_is_token(get_turnstile_tk())) { + p.next(); occurrence goal_occ = parse_occurrence(p); return location::mk_at(goal_occ, hyps, hyp_occs); } else { return location::mk_hypotheses_at(hyps, hyp_occs); } } - } else if (p.curr_is_token(get_at_tk())) { - occurrence o = parse_occurrence(p); - return location::mk_goal_at(o); } else { return location::mk_goal_only(); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 6cb3b738b2..1fdd872882 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -74,13 +74,13 @@ static char const * g_decreasing_unicode = "↓"; void init_token_table(token_table & t) { pair builtin[] = - {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, + {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"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}, - {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0}, - {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, + {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, + {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, + {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 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}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 5bc7a35ba5..459bcbf74a 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -25,6 +25,12 @@ static name * g_rbracket = nullptr; static name * g_bar = nullptr; static name * g_comma = nullptr; static name * g_add = nullptr; +static name * g_sub = nullptr; +static name * g_question = nullptr; +static name * g_bang = nullptr; +static name * g_slash = nullptr; +static name * g_star = nullptr; +static name * g_turnstile = nullptr; static name * g_max = nullptr; static name * g_imax = nullptr; static name * g_cup = nullptr; @@ -58,6 +64,7 @@ static name * g_whnf = nullptr; static name * g_wf = nullptr; static name * g_strict = nullptr; static name * g_in = nullptr; +static name * g_at = nullptr; static name * g_assign = nullptr; static name * g_visible = nullptr; static name * g_from = nullptr; @@ -124,6 +131,12 @@ void initialize_tokens() { g_bar = new name("|"); g_comma = new name(","); g_add = new name("+"); + g_sub = new name("-"); + g_question = new name("?"); + g_bang = new name("!"); + g_slash = new name("/"); + g_star = new name("*"); + g_turnstile = new name("⊢"); g_max = new name("max"); g_imax = new name("imax"); g_cup = new name("\u2294"); @@ -157,6 +170,7 @@ void initialize_tokens() { g_wf = new name("[wf]"); g_strict = new name("[strict]"); g_in = new name("in"); + g_at = new name("at"); g_assign = new name(":="); g_visible = new name("[visible]"); g_from = new name("from"); @@ -242,6 +256,7 @@ void finalize_tokens() { delete g_attribute; delete g_parsing_only; delete g_in; + delete g_at; delete g_assign; delete g_visible; delete g_from; @@ -286,6 +301,12 @@ void finalize_tokens() { delete g_imax; delete g_max; delete g_add; + delete g_sub; + delete g_question; + delete g_bang; + delete g_slash; + delete g_star; + delete g_turnstile; delete g_comma; delete g_bar; delete g_rbracket; @@ -323,6 +344,12 @@ name const & get_rbracket_tk() { return *g_rbracket; } name const & get_bar_tk() { return *g_bar; } name const & get_comma_tk() { return *g_comma; } name const & get_add_tk() { return *g_add; } +name const & get_sub_tk() { return *g_sub; } +name const & get_question_tk() { return *g_question; } +name const & get_bang_tk() { return *g_bang; } +name const & get_slash_tk() { return *g_slash; } +name const & get_star_tk() { return *g_star; } +name const & get_turnstile_tk() { return *g_turnstile; } name const & get_max_tk() { return *g_max; } name const & get_imax_tk() { return *g_imax; } name const & get_cup_tk() { return *g_cup; } @@ -356,6 +383,7 @@ name const & get_whnf_tk() { return *g_whnf; } name const & get_wf_tk() { return *g_wf; } name const & get_strict_tk() { return *g_strict; } name const & get_in_tk() { return *g_in; } +name const & get_at_tk() { return *g_at; } name const & get_assign_tk() { return *g_assign; } name const & get_visible_tk() { return *g_visible; } name const & get_from_tk() { return *g_from; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 2134e3e2ae..f28d4006fb 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -27,6 +27,12 @@ name const & get_rbracket_tk(); name const & get_bar_tk(); name const & get_comma_tk(); name const & get_add_tk(); +name const & get_sub_tk(); +name const & get_question_tk(); +name const & get_bang_tk(); +name const & get_slash_tk(); +name const & get_star_tk(); +name const & get_turnstile_tk(); name const & get_max_tk(); name const & get_imax_tk(); name const & get_cup_tk(); @@ -60,6 +66,7 @@ name const & get_whnf_tk(); name const & get_wf_tk(); name const & get_strict_tk(); name const & get_in_tk(); +name const & get_at_tk(); name const & get_assign_tk(); name const & get_visible_tk(); name const & get_from_tk(); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 31df817c46..43e4f066b1 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -108,6 +108,10 @@ location get_rewrite_location(expr const & e) { return static_cast(macro_def(e).raw())->get_location(); } +expr mk_rewrite_tactic_expr(buffer const & elems, location const & loc) { + return mk_app(*g_rewrite_tac, mk_rewrite_elements(elems, loc)); +} + tactic mk_rewrite_tactic(buffer const & elems, location const & loc) { // TODO(Leo) for (auto const & e : elems) @@ -133,11 +137,13 @@ void initialize_rewrite_tactic() { register_tac(rewrite_tac_name, [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - if (!is_rewrite_elements(app_arg(e))) - throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, argument is ill-formed"); + check_tactic_expr(app_arg(e), "invalid 'rewrite' tactic, invalid argument"); + expr arg = get_tactic_expr_expr(app_arg(e)); + if (!is_rewrite_elements(arg)) + throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); buffer elems; - get_rewrite_elements(app_arg(e), elems); - location loc = get_rewrite_location(app_arg(e)); + get_rewrite_elements(arg, elems); + location loc = get_rewrite_location(arg); return mk_rewrite_tactic(elems, loc); }); }