From 180cda304eec3d562d3fd2b53c4ca79d07e739af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Feb 2015 16:03:06 -0800 Subject: [PATCH] feat(library/tactic): add rewrite tactic skeleton The tactic has not been implemented yet, but this commit adds all the support for storing arguments, serializing and deserializing them. --- src/library/tactic/CMakeLists.txt | 4 +- src/library/tactic/expr_to_tactic.h | 1 + src/library/tactic/init_module.cpp | 3 + src/library/tactic/rewrite_tactic.cpp | 150 ++++++++++++++++++++++++++ src/library/tactic/rewrite_tactic.h | 59 ++++++++++ 5 files changed, 215 insertions(+), 2 deletions(-) create mode 100644 src/library/tactic/rewrite_tactic.cpp create mode 100644 src/library/tactic/rewrite_tactic.h diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 800d5de8c..c8df8ba15 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -2,7 +2,7 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp -assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp util.cpp -class_instance_synth.cpp init_module.cpp) +assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp +rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 2341eea99..bf0cd5354 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -39,6 +39,7 @@ expr const & get_tactic_expr_list_type(); 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); +expr ids_to_tactic_expr(buffer const & ids); /** \brief Create an expression `by t`, where \c t is an expression of type `tactic`. diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 345b01e97..a31778a47 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "library/tactic/inversion_tactic.h" #include "library/tactic/assert_tactic.h" #include "library/tactic/class_instance_synth.h" +#include "library/tactic/rewrite_tactic.h" namespace lean { void initialize_tactic_module() { @@ -39,9 +40,11 @@ void initialize_tactic_module() { initialize_inversion_tactic(); initialize_assert_tactic(); initialize_class_instance_elaborator(); + initialize_rewrite_tactic(); } void finalize_tactic_module() { + finalize_rewrite_tactic(); finalize_class_instance_elaborator(); finalize_assert_tactic(); finalize_inversion_tactic(); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp new file mode 100644 index 000000000..31df817c4 --- /dev/null +++ b/src/library/tactic/rewrite_tactic.cpp @@ -0,0 +1,150 @@ +/* +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/kernel_serializer.h" +#include "library/tactic/rewrite_tactic.h" +#include "library/tactic/expr_to_tactic.h" + +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) { +} + +rewrite_element rewrite_element::mk_unfold(name const & l) { + return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional()); +} + +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_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_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_zero_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) { + return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional()); +} + +serializer & operator<<(serializer & s, rewrite_element const & e) { + s << e.m_lemma << e.m_symm << e.m_unfold << static_cast(e.m_multiplicity); + if (e.has_num()) + s << e.num(); + return s; +} + +deserializer & operator>>(deserializer & d, rewrite_element & e) { + char multp; + d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp; + 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; + +[[ noreturn ]] static void throw_re_ex() { throw exception("unexpected occurrence of 'rewrite elements' expression"); } + +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) {} + 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; + 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)); + return mk_macro(def); +} + +expr mk_rewrite_elements(buffer const & e, location const & loc) { + return mk_rewrite_elements(to_list(e), loc); +} + +/** \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; +} + +/** \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); +} + +location get_rewrite_location(expr const & e) { + lean_assert(is_rewrite_elements(e)); + return static_cast(macro_def(e).raw())->get_location(); +} + +tactic mk_rewrite_tactic(buffer const & elems, location const & loc) { + // 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(); +} + +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, + [](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); + }); + + 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"); + buffer elems; + get_rewrite_elements(app_arg(e), elems); + location loc = get_rewrite_location(app_arg(e)); + return mk_rewrite_tactic(elems, loc); + }); +} + +void finalize_rewrite_tactic() { + delete g_rewrite_tac; + delete g_rewrite_elems_name; + delete g_rewrite_elems_opcode; +} +} diff --git a/src/library/tactic/rewrite_tactic.h b/src/library/tactic/rewrite_tactic.h new file mode 100644 index 000000000..308b29725 --- /dev/null +++ b/src/library/tactic/rewrite_tactic.h @@ -0,0 +1,59 @@ +/* +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 "library/tactic/tactic.h" +#include "library/tactic/location.h" + +namespace lean { +enum class rewrite_multiplicity { Once, AtMostN, ExactlyN, ZeroOrMore, OneOrMore }; + +class rewrite_element { + name m_lemma; + bool m_symm; + 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); +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); + 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; + } + + 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()); + +/** \brief Create rewrite tactic that applies the given rewrite elements */ +tactic mk_rewrite_tactic(buffer const & elems, location const & loc = location()); + +void initialize_rewrite_tactic(); +void finalize_rewrite_tactic(); +}