diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index aa5722287..ce9883c9a 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -62,9 +62,6 @@ 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 @@ -72,6 +69,10 @@ inductive expr_list : Type := nil : expr_list, cons : expr → 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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 3163780d2..a5d9088b8 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -63,9 +63,6 @@ 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 @@ -73,6 +70,10 @@ inductive expr_list : Type := nil : expr_list, cons : expr → 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 diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 4dfc96ff5..e52153897 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -10,16 +10,34 @@ Author: Leonardo de Moura #include "frontends/lean/parse_tactic_location.h" namespace lean { -static name parse_rewrite_element_id(parser & p) { - return p.check_id_next("invalid rewrite tactic step, identifier expected"); +static optional parse_pattern(parser & p) { + if (p.curr_is_token(get_lbracket_tk())) { + p.next(); + expr r = p.parse_expr(); + p.check_token_next(get_rbracket_tk(), "invalid rewrite pattern, ']' expected"); + return some_expr(r); + } else { + return none_expr(); + } } -rewrite_element parse_rewrite_element(parser & p) { +static expr parse_rule(parser & p) { + if (p.curr_is_token(get_lparen_tk())) { + p.next(); + expr r = p.parse_expr(); + p.check_token_next(get_rparen_tk(), "invalid rewrite pattern, ']' expected"); + return r; + } else { + return p.parse_id(); + } +} + +expr parse_rewrite_element(parser & p) { if (p.curr_is_token(get_slash_tk())) { p.next(); - name id = p.check_id_next("invalid unfold rewrite step, identifier expected"); + name n = p.check_id_next("invalid unfold rewrite step, identifier expected"); location loc = parse_tactic_location(p); - return rewrite_element::mk_unfold(id, loc); + return mk_rewrite_unfold(n, loc); } bool symm = false; if (p.curr_is_token(get_sub_tk())) { @@ -30,38 +48,44 @@ rewrite_element parse_rewrite_element(parser & p) { unsigned n = p.parse_small_nat(); if (p.curr_is_token(get_question_tk())) { p.next(); - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_at_most_n(id, n, symm, loc); + return mk_rewrite_at_most_n(pat, H, n, symm, loc); } else if (p.curr_is_token(get_bang_tk())) { p.next(); - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_exactly_n(id, n, symm, loc); + return mk_rewrite_exactly_n(pat, H, n, symm, loc); } else { - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_exactly_n(id, n, symm, loc); + return mk_rewrite_exactly_n(pat, H, n, symm, loc); } } else if (p.curr_is_token(get_question_tk())) { p.next(); - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_zero_or_more(id, symm, loc); + return mk_rewrite_zero_or_more(pat, H, symm, loc); } else if (p.curr_is_token(get_bang_tk())) { p.next(); - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_one_or_more(id, symm, loc); + return mk_rewrite_one_or_more(pat, H, symm, loc); } else { - name id = parse_rewrite_element_id(p); + optional pat = parse_pattern(p); + expr H = parse_rule(p); location loc = parse_tactic_location(p); - return rewrite_element::mk_once(id, symm, loc); + return mk_rewrite_once(pat, H, symm, loc); } } expr parse_rewrite_tactic(parser & p) { - buffer elems; + buffer elems; while (true) { bool has_paren = false; if (p.curr_is_token(get_lparen_tk())) { @@ -77,6 +101,7 @@ expr parse_rewrite_tactic(parser & p) { !p.curr_is_token(get_question_tk()) && !p.curr_is_token(get_slash_tk()) && !p.curr_is_identifier() && + !p.curr_is_token(get_lbracket_tk()) && !p.curr_is_token(get_lparen_tk())) break; } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index b5f57553d..b7f49d7a2 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -185,7 +185,6 @@ class parser { expr parse_nud_notation(); expr parse_led_notation(expr left); expr parse_nud(); - expr parse_id(); expr parse_numeral_expr(); expr parse_decimal_expr(); expr parse_string_expr(); @@ -368,6 +367,8 @@ public: */ pair, expr> parse_optional_assignment(unsigned rbp = 0); + expr parse_id(); + expr parse_led(expr left); expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0); expr parse_scoped_expr(buffer const & ps, local_environment const & lenv, unsigned rbp = 0) { diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 9fe08c177..a55d61dfa 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -121,6 +121,16 @@ name const & tactic_expr_to_id(expr e, char const * error_msg) { static expr * g_expr_list_cons = nullptr; static expr * g_expr_list_nil = nullptr; +expr mk_expr_list(unsigned num, expr const * args) { + expr r = *g_expr_list_nil; + unsigned i = num; + while (i > 0) { + --i; + r = mk_app(*g_expr_list_cons, args[i], r); + } + return r; +} + void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg) { while (true) { if (l == *g_expr_list_nil) diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index bf0cd5354..6c5b37cda 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -36,6 +36,8 @@ expr const & get_tactic_expr_expr(expr const & e); void check_tactic_expr(expr const & e, char const * msg); expr const & get_tactic_expr_list_type(); +expr mk_expr_list(unsigned num, expr const * args); + name const & tactic_expr_to_id(expr e, char const * error_msg); void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg); void get_tactic_id_list_elements(expr l, buffer & r, char const * error_msg); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index aaae2c54d..0a0808f79 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -9,137 +9,258 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -rewrite_element::rewrite_element():m_symm(false), m_unfold(true), m_multiplicity(rewrite_multiplicity::Once) {} +class unfold_info { + name m_name; + location m_location; +public: + unfold_info() {} + unfold_info(name const & n, location const & loc):m_name(n), m_location(loc) {} + name const & get_name() const { return m_name; } + location const & get_location() const { return m_location; } + friend serializer & operator<<(serializer & s, unfold_info const & elem); + friend deserializer & operator>>(deserializer & d, unfold_info & e); +}; -rewrite_element::rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, - optional const & n, location const & loc): - m_lemma(l), m_symm(symm), m_unfold(unfold), m_multiplicity(m), m_num(n), m_location(loc) { +serializer & operator<<(serializer & s, unfold_info const & e) { + s << e.m_name << e.m_location; + return s; } -rewrite_element rewrite_element::mk_unfold(name const & l, location const & loc) { - return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional(), loc); +deserializer & operator>>(deserializer & d, unfold_info & e) { + d >> e.m_name >> e.m_location; + return d; } -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); -} +class rewrite_info { + enum multiplicity { Once, AtMostN, ExactlyN, ZeroOrMore, OneOrMore }; + bool m_symm; + multiplicity m_multiplicity; + optional m_num; + location m_location; + rewrite_info(bool symm, multiplicity m, optional const & n, + location const & loc): + m_symm(symm), m_multiplicity(m), m_num(n), m_location(loc) {} +public: + rewrite_info():m_symm(false), m_multiplicity(Once) {} + static rewrite_info mk_once(bool symm, location const & loc) { + return rewrite_info(symm, Once, optional(), loc); + } -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); -} + static rewrite_info mk_at_most_n(unsigned n, bool symm, location const & loc) { + return rewrite_info(symm, AtMostN, optional(n), loc); + } -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); -} + static rewrite_info mk_exactly_n(unsigned n, bool symm, location const & loc) { + return rewrite_info(symm, ExactlyN, optional(n), loc); + } -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); -} + static rewrite_info mk_zero_or_more(bool symm, location const & loc) { + return rewrite_info(symm, ZeroOrMore, optional(), loc); + } -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); -} + static rewrite_info mk_one_or_more(bool symm, location const & loc) { + return rewrite_info(symm, 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) << e.m_location; + bool symm() const { + return m_symm; + } + + multiplicity get_multiplicity() const { + return m_multiplicity; + } + + bool has_num() const { + return multiplicity() == AtMostN || multiplicity() == ExactlyN; + } + + unsigned num() const { + lean_assert(has_num()); + return *m_num; + } + + location get_location() const { return m_location; } + + friend serializer & operator<<(serializer & s, rewrite_info const & elem); + friend deserializer & operator>>(deserializer & d, rewrite_info & e); +}; + +serializer & operator<<(serializer & s, rewrite_info const & e) { + s << e.m_symm << static_cast(e.m_multiplicity) << e.m_location; if (e.has_num()) s << e.num(); return s; } -deserializer & operator>>(deserializer & d, rewrite_element & e) { +deserializer & operator>>(deserializer & d, rewrite_info & e) { char multp; - d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp >> e.m_location; - e.m_multiplicity = static_cast(multp); + d >> e.m_symm >> multp >> e.m_location; + e.m_multiplicity = static_cast(multp); if (e.has_num()) e.m_num = d.read_unsigned(); return d; } -static expr * g_rewrite_tac = nullptr; -static name * g_rewrite_elems_name = nullptr; -static std::string * g_rewrite_elems_opcode = nullptr; +static expr * g_rewrite_tac = nullptr; -[[ noreturn ]] static void throw_re_ex() { throw exception("unexpected occurrence of 'rewrite elements' expression"); } +static name * g_rewrite_elem_name = nullptr; +static std::string * g_rewrite_elem_opcode = nullptr; -class rewrite_elements_macro_cell : public macro_definition_cell { - list m_elems; +static name * g_rewrite_unfold_name = nullptr; +static std::string * g_rewrite_unfold_opcode = nullptr; + +[[ noreturn ]] static void throw_ru_ex() { throw exception("unexpected occurrence of 'rewrite unfold' expression"); } +[[ noreturn ]] static void throw_re_ex() { throw exception("unexpected occurrence of 'rewrite element' expression"); } + +class rewrite_unfold_macro_cell : public macro_definition_cell { + unfold_info m_info; public: - 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(); } + rewrite_unfold_macro_cell(unfold_info const & info):m_info(info) {} + virtual name get_name() const { return *g_rewrite_unfold_name; } + virtual pair get_type(expr const &, extension_context &) const { throw_ru_ex(); } + virtual optional expand(expr const &, extension_context &) const { throw_ru_ex(); } virtual void write(serializer & s) const { - s << *g_rewrite_elems_opcode; - write_list(s, m_elems); - + s << *g_rewrite_unfold_opcode << m_info; } - list const & get_elems() const { return m_elems; } + unfold_info const & get_info() const { return m_info; } }; -/** \brief Create a macro expression to encapsulate a list of rewrite elements */ -expr mk_rewrite_elements(list const & e) { - macro_definition def(new rewrite_elements_macro_cell(e)); +expr mk_rewrite_unfold(name const & n, location const & loc) { + macro_definition def(new rewrite_unfold_macro_cell(unfold_info(n, loc))); return mk_macro(def); } -expr mk_rewrite_elements(buffer const & e) { - return mk_rewrite_elements(to_list(e)); +bool is_rewrite_unfold_step(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == *g_rewrite_unfold_name; } -/** \brief Return true iff \c e is a "macro" that encapsulates a list of rewrite_elements */ -bool is_rewrite_elements(expr const & e) { - return is_macro(e) && macro_def(e).get_name() == *g_rewrite_elems_name; +class rewrite_element_macro_cell : public macro_definition_cell { + rewrite_info m_info; +public: + rewrite_element_macro_cell(rewrite_info const & info):m_info(info) {} + virtual name get_name() const { return *g_rewrite_elem_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_elem_opcode << m_info; + } + rewrite_info const & get_info() const { return m_info; } +}; + +expr mk_rw_macro(macro_definition const & def, optional const & pattern, expr const & H) { + if (pattern) { + expr args[2] = {H, *pattern}; + return mk_macro(def, 2, args); + } else { + return mk_macro(def, 1, &H); + } } -/** \brief Copy the rewrite_elements stored in \c e into result. - \pre is_rewrite_elements(e) -*/ -void get_rewrite_elements(expr const & e, buffer & result) { - lean_assert(is_rewrite_elements(e)); - list const & l = static_cast(macro_def(e).raw())->get_elems(); - to_buffer(l, result); +expr mk_rewrite_once(optional const & pattern, expr const & H, bool symm, location const & loc) { + macro_definition def(new rewrite_element_macro_cell(rewrite_info::mk_once(symm, loc))); + return mk_rw_macro(def, pattern, H); } -expr mk_rewrite_tactic_expr(buffer const & elems) { - return mk_app(*g_rewrite_tac, mk_rewrite_elements(elems)); +expr mk_rewrite_zero_or_more(optional const & pattern, expr const & H, bool symm, location const & loc) { + macro_definition def(new rewrite_element_macro_cell(rewrite_info::mk_zero_or_more(symm, loc))); + return mk_rw_macro(def, pattern, H); } -tactic mk_rewrite_tactic(buffer const & elems) { +expr mk_rewrite_one_or_more(optional const & pattern, expr const & H, bool symm, location const & loc) { + macro_definition def(new rewrite_element_macro_cell(rewrite_info::mk_one_or_more(symm, loc))); + return mk_rw_macro(def, pattern, H); +} + +expr mk_rewrite_at_most_n(optional const & pattern, expr const & H, bool symm, unsigned n, location const & loc) { + macro_definition def(new rewrite_element_macro_cell(rewrite_info::mk_at_most_n(n, symm, loc))); + return mk_rw_macro(def, pattern, H); +} + +expr mk_rewrite_exactly_n(optional const & pattern, expr const & H, bool symm, unsigned n, location const & loc) { + macro_definition def(new rewrite_element_macro_cell(rewrite_info::mk_exactly_n(n, symm, loc))); + return mk_rw_macro(def, pattern, H); +} + +bool is_rewrite_step(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == *g_rewrite_elem_name; +} + +bool has_rewrite_pattern(expr const & e) { + lean_assert(is_rewrite_step(e)); + return macro_num_args(e) == 2; +} + +expr const & get_rewrite_rule(expr const & e) { + lean_assert(is_rewrite_step(e)); + return macro_arg(e, 0); +} + +expr const & get_rewrite_pattern(expr const & e) { + lean_assert(has_rewrite_pattern(e)); + return macro_arg(e, 1); +} + +expr mk_rewrite_tactic_expr(buffer const & elems) { + lean_assert(std::all_of(elems.begin(), elems.end(), [](expr const & e) { + return is_rewrite_step(e) || is_rewrite_unfold_step(e); + })); + return mk_app(*g_rewrite_tac, mk_expr_list(elems.size(), elems.data())); +} + +tactic mk_rewrite_tactic(buffer const & elems) { // TODO(Leo) - for (auto const & e : elems) - std::cout << ">> " << e.get_name() << "\n"; + std::cout << "rewrite_tactic\n"; + for (auto const & e : elems) { + if (is_rewrite_step(e)) + std::cout << ">> " << get_rewrite_rule(e) << "\n"; + else + std::cout << ">> unfold\n"; + } return id_tactic(); } void initialize_rewrite_tactic() { name rewrite_tac_name{"tactic", "rewrite_tac"}; - g_rewrite_tac = new expr(Const(rewrite_tac_name)); - g_rewrite_elems_name = new name("rewrite_elements"); - g_rewrite_elems_opcode = new std::string("RWE"); - register_macro_deserializer(*g_rewrite_elems_opcode, + g_rewrite_tac = new expr(Const(rewrite_tac_name)); + g_rewrite_unfold_name = new name("rewrite_unfold"); + g_rewrite_unfold_opcode = new std::string("RWU"); + g_rewrite_elem_name = new name("rewrite_element"); + g_rewrite_elem_opcode = new std::string("RWE"); + register_macro_deserializer(*g_rewrite_unfold_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) throw corrupted_stream_exception(); - list elems = read_list(d); - return mk_rewrite_elements(elems); + unfold_info info; + d >> info; + macro_definition def(new rewrite_unfold_macro_cell(info)); + return mk_macro(def); + }); + register_macro_deserializer(*g_rewrite_elem_opcode, + [](deserializer & d, unsigned num, expr const * args) { + if (num != 1 && num != 2) + throw corrupted_stream_exception(); + rewrite_info info; + d >> info; + macro_definition def(new rewrite_element_macro_cell(info)); + return mk_macro(def, num, args); }); - register_tac(rewrite_tac_name, [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - 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(arg, elems); - return mk_rewrite_tactic(elems); + buffer args; + get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument"); + for (expr const & arg : args) { + if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg)) + throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); + } + return mk_rewrite_tactic(args); }); } void finalize_rewrite_tactic() { delete g_rewrite_tac; - delete g_rewrite_elems_name; - delete g_rewrite_elems_opcode; + delete g_rewrite_unfold_name; + delete g_rewrite_unfold_opcode; + delete g_rewrite_elem_name; + delete g_rewrite_elem_opcode; } } diff --git a/src/library/tactic/rewrite_tactic.h b/src/library/tactic/rewrite_tactic.h index 01817f915..8d34df631 100644 --- a/src/library/tactic/rewrite_tactic.h +++ b/src/library/tactic/rewrite_tactic.h @@ -9,53 +9,20 @@ Author: Leonardo de Moura #include "library/tactic/location.h" namespace lean { -enum class rewrite_multiplicity { Once, AtMostN, ExactlyN, ZeroOrMore, OneOrMore }; +expr mk_rewrite_unfold(name const & n, location const & loc); +expr mk_rewrite_once(optional const & pattern, expr const & H, bool symm, location const & loc); +expr mk_rewrite_zero_or_more(optional const & pattern, expr const & H, bool symm, location const & loc); +expr mk_rewrite_one_or_more(optional const & pattern, expr const & H, bool symm, location const & loc); +expr mk_rewrite_at_most_n(optional const & pattern, expr const & H, bool symm, unsigned n, location const & loc); +expr mk_rewrite_exactly_n(optional const & pattern, expr const & H, bool symm, unsigned n, location const & loc); +bool is_rewrite_unfold_step(expr const & e); +bool is_rewrite_step(expr const & e); -class rewrite_element { - name m_lemma; - bool m_symm; - bool m_unfold; - rewrite_multiplicity m_multiplicity; - optional m_num; - 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, 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 { - lean_assert(!unfold()); - return m_symm; - } - rewrite_multiplicity multiplicity() const { - lean_assert(!unfold()); - return m_multiplicity; - } - bool has_num() const { - return multiplicity() == rewrite_multiplicity::AtMostN || multiplicity() == rewrite_multiplicity::ExactlyN; - } - unsigned num() const { - 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); +/** \brief Create a rewrite tactic expression, where elems was created using \c mk_rewrite_* procedures. */ +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); +tactic mk_rewrite_tactic(buffer const & elems); void initialize_rewrite_tactic(); void finalize_rewrite_tactic();