diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 3c4fafe53..4dfc96ff5 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -10,14 +10,16 @@ Author: Leonardo de Moura #include "frontends/lean/parse_tactic_location.h" namespace lean { -name parse_rewrite_element_id(parser & p) { +static 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")); + name id = p.check_id_next("invalid unfold rewrite step, identifier expected"); + location loc = parse_tactic_location(p); + return rewrite_element::mk_unfold(id, loc); } bool symm = false; if (p.curr_is_token(get_sub_tk())) { @@ -28,37 +30,56 @@ rewrite_element parse_rewrite_element(parser & p) { 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); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_at_most_n(id, n, symm, loc); } else if (p.curr_is_token(get_bang_tk())) { p.next(); - return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_exactly_n(id, n, symm, loc); } else { - return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_exactly_n(id, n, symm, loc); } } else if (p.curr_is_token(get_question_tk())) { p.next(); - return rewrite_element::mk_zero_or_more(parse_rewrite_element_id(p), symm); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_zero_or_more(id, symm, loc); } else if (p.curr_is_token(get_bang_tk())) { p.next(); - return rewrite_element::mk_one_or_more(parse_rewrite_element_id(p), symm); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_one_or_more(id, symm, loc); } else { - return rewrite_element::mk_once(parse_rewrite_element_id(p), symm); + name id = parse_rewrite_element_id(p); + location loc = parse_tactic_location(p); + return rewrite_element::mk_once(id, symm, loc); } } expr parse_rewrite_tactic(parser & p) { buffer elems; while (true) { + bool has_paren = false; + if (p.curr_is_token(get_lparen_tk())) { + has_paren = true; + p.next(); + } elems.push_back(parse_rewrite_element(p)); + if (has_paren) + p.check_token_next(get_rparen_tk(), "invalid rewrite tactic element, ')' expected"); 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()) + !p.curr_is_identifier() && + !p.curr_is_token(get_lparen_tk())) break; } - location loc = parse_tactic_location(p); - return mk_rewrite_tactic_expr(elems, loc); + return mk_rewrite_tactic_expr(elems); } } diff --git a/src/frontends/lean/parse_tactic_location.cpp b/src/frontends/lean/parse_tactic_location.cpp index c17cd307f..285d33b21 100644 --- a/src/frontends/lean/parse_tactic_location.cpp +++ b/src/frontends/lean/parse_tactic_location.cpp @@ -61,24 +61,35 @@ location parse_tactic_location(parser & p) { // at * return location::mk_everywhere(); } - } else { + } else if (p.curr_is_token(get_lparen_tk())) { + p.next(); buffer hyps; buffer hyp_occs; - while (p.curr_is_identifier()) { + while (true) { 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 (hyps.empty()) { - occurrence o = parse_occurrence(p); - return location::mk_goal_at(o); - } else if (p.curr_is_token(get_turnstile_tk())) { + p.check_token_next(get_rparen_tk(), "invalid tactic location, ')' expected"); + 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_lcurly_tk())) { + occurrence o = parse_occurrence(p); + return location::mk_goal_at(o); + } else { + buffer hyps; + buffer hyp_occs; + hyps.push_back(p.check_id_next("invalid tactic location, identifier expected")); + hyp_occs.push_back(parse_occurrence(p)); + return location::mk_hypotheses_at(hyps, hyp_occs); } } else { return location::mk_goal_only(); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 43e4f066b..aaae2c54d 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -12,36 +12,36 @@ namespace lean { rewrite_element::rewrite_element():m_symm(false), m_unfold(true), m_multiplicity(rewrite_multiplicity::Once) {} rewrite_element::rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, - optional const & n): - m_lemma(l), m_symm(symm), m_unfold(unfold), m_multiplicity(m), m_num(n) { + optional const & n, location const & loc): + m_lemma(l), m_symm(symm), m_unfold(unfold), m_multiplicity(m), m_num(n), m_location(loc) { } -rewrite_element rewrite_element::mk_unfold(name const & l) { - return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional()); +rewrite_element rewrite_element::mk_unfold(name const & l, location const & loc) { + return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional(), loc); } -rewrite_element rewrite_element::mk_once(name const & l, bool symm) { - return rewrite_element(l, symm, false, rewrite_multiplicity::Once, optional()); +rewrite_element rewrite_element::mk_once(name const & l, bool symm, location const & loc) { + return rewrite_element(l, symm, false, rewrite_multiplicity::Once, optional(), loc); } -rewrite_element rewrite_element::mk_at_most_n(name const & l, unsigned n, bool symm) { - return rewrite_element(l, symm, false, rewrite_multiplicity::AtMostN, optional(n)); +rewrite_element rewrite_element::mk_at_most_n(name const & l, unsigned n, bool symm, location const & loc) { + return rewrite_element(l, symm, false, rewrite_multiplicity::AtMostN, optional(n), loc); } -rewrite_element rewrite_element::mk_exactly_n(name const & l, unsigned n, bool symm) { - return rewrite_element(l, symm, false, rewrite_multiplicity::ExactlyN, optional(n)); +rewrite_element rewrite_element::mk_exactly_n(name const & l, unsigned n, bool symm, location const & loc) { + return rewrite_element(l, symm, false, rewrite_multiplicity::ExactlyN, optional(n), loc); } -rewrite_element rewrite_element::mk_zero_or_more(name const & l, bool symm) { - return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional()); +rewrite_element rewrite_element::mk_zero_or_more(name const & l, bool symm, location const & loc) { + return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional(), loc); } -rewrite_element rewrite_element::mk_one_or_more(name const & l, bool symm) { - return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional()); +rewrite_element rewrite_element::mk_one_or_more(name const & l, bool symm, location const & loc) { + return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional(), loc); } serializer & operator<<(serializer & s, rewrite_element const & e) { - s << e.m_lemma << e.m_symm << e.m_unfold << static_cast(e.m_multiplicity); + s << e.m_lemma << e.m_symm << e.m_unfold << static_cast(e.m_multiplicity) << e.m_location; if (e.has_num()) s << e.num(); return s; @@ -49,7 +49,7 @@ serializer & operator<<(serializer & s, rewrite_element const & e) { deserializer & operator>>(deserializer & d, rewrite_element & e) { char multp; - d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp; + d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp >> e.m_location; e.m_multiplicity = static_cast(multp); if (e.has_num()) e.m_num = d.read_unsigned(); @@ -64,29 +64,27 @@ static std::string * g_rewrite_elems_opcode = nullptr; class rewrite_elements_macro_cell : public macro_definition_cell { list m_elems; - location m_loc; public: - rewrite_elements_macro_cell(list const & elems, location const & loc):m_elems(elems), m_loc(loc) {} + rewrite_elements_macro_cell(list const & elems):m_elems(elems) {} virtual name get_name() const { return *g_rewrite_elems_name; } virtual pair get_type(expr const &, extension_context &) const { throw_re_ex(); } virtual optional expand(expr const &, extension_context &) const { throw_re_ex(); } virtual void write(serializer & s) const { - s << *g_rewrite_elems_opcode << m_loc; + s << *g_rewrite_elems_opcode; write_list(s, m_elems); } list const & get_elems() const { return m_elems; } - location const & get_location() const { return m_loc; } }; /** \brief Create a macro expression to encapsulate a list of rewrite elements */ -expr mk_rewrite_elements(list const & e, location const & loc) { - macro_definition def(new rewrite_elements_macro_cell(e, loc)); +expr mk_rewrite_elements(list const & e) { + macro_definition def(new rewrite_elements_macro_cell(e)); return mk_macro(def); } -expr mk_rewrite_elements(buffer const & e, location const & loc) { - return mk_rewrite_elements(to_list(e), loc); +expr mk_rewrite_elements(buffer const & e) { + return mk_rewrite_elements(to_list(e)); } /** \brief Return true iff \c e is a "macro" that encapsulates a list of rewrite_elements */ @@ -103,20 +101,14 @@ void get_rewrite_elements(expr const & e, buffer & result) { to_buffer(l, result); } -location get_rewrite_location(expr const & e) { - lean_assert(is_rewrite_elements(e)); - return static_cast(macro_def(e).raw())->get_location(); +expr mk_rewrite_tactic_expr(buffer const & elems) { + return mk_app(*g_rewrite_tac, mk_rewrite_elements(elems)); } -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) { +tactic mk_rewrite_tactic(buffer const & elems) { // TODO(Leo) for (auto const & e : elems) std::cout << ">> " << e.get_name() << "\n"; - std::cout << "include goal >> " << static_cast(loc.includes_goal()) << "\n"; return id_tactic(); } @@ -129,10 +121,8 @@ void initialize_rewrite_tactic() { [](deserializer & d, unsigned num, expr const *) { if (num != 0) throw corrupted_stream_exception(); - location loc; - d >> loc; list elems = read_list(d); - return mk_rewrite_elements(elems, loc); + return mk_rewrite_elements(elems); }); register_tac(rewrite_tac_name, @@ -143,8 +133,7 @@ void initialize_rewrite_tactic() { throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); buffer elems; get_rewrite_elements(arg, elems); - location loc = get_rewrite_location(arg); - return mk_rewrite_tactic(elems, loc); + return mk_rewrite_tactic(elems); }); } diff --git a/src/library/tactic/rewrite_tactic.h b/src/library/tactic/rewrite_tactic.h index 308b29725..01817f915 100644 --- a/src/library/tactic/rewrite_tactic.h +++ b/src/library/tactic/rewrite_tactic.h @@ -17,15 +17,17 @@ class rewrite_element { bool m_unfold; rewrite_multiplicity m_multiplicity; optional m_num; - rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, optional const & n); + location m_location; + rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, optional const & n, + location const & loc); public: rewrite_element(); - static rewrite_element mk_unfold(name const & l); - static rewrite_element mk_once(name const & l, bool symm = false); - static rewrite_element mk_at_most_n(name const & l, unsigned n, bool symm = false); - static rewrite_element mk_exactly_n(name const & l, unsigned n, bool symm = false); - static rewrite_element mk_zero_or_more(name const & l, bool symm = false); - static rewrite_element mk_one_or_more(name const & l, bool symm = false); + static rewrite_element mk_unfold(name const & l, location const & loc); + static rewrite_element mk_once(name const & l, bool symm, location const & loc); + static rewrite_element mk_at_most_n(name const & l, unsigned n, bool symm, location const & loc); + static rewrite_element mk_exactly_n(name const & l, unsigned n, bool symm, location const & loc); + static rewrite_element mk_zero_or_more(name const & l, bool symm, location const & loc); + static rewrite_element mk_one_or_more(name const & l, bool symm, location const & loc); name const & get_name() const { return m_lemma; } bool unfold() const { return m_unfold; } bool symm() const { @@ -43,16 +45,17 @@ public: lean_assert(has_num()); return *m_num; } + location get_location() const { return m_location; } friend serializer & operator<<(serializer & s, rewrite_element const & elem); friend deserializer & operator>>(deserializer & d, rewrite_element & e); }; /** \brief Create a rewrite tactic expression, where elems was created using \c mk_rewrite_elements. */ -expr mk_rewrite_tactic_expr(buffer const & elems, location const & loc = location()); +expr mk_rewrite_tactic_expr(buffer const & elems); /** \brief Create rewrite tactic that applies the given rewrite elements */ -tactic mk_rewrite_tactic(buffer const & elems, location const & loc = location()); +tactic mk_rewrite_tactic(buffer const & elems); void initialize_rewrite_tactic(); void finalize_rewrite_tactic();