From 80851231197a76340b99fefae814f01be767db8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jul 2015 10:39:30 -0700 Subject: [PATCH] refactor(library/simplifier): rename 'rewrite_rule' to 'simp_rule' --- src/frontends/lean/builtin_cmds.cpp | 16 ++-- src/frontends/lean/decl_attributes.cpp | 4 +- src/frontends/lean/parse_simp_tactic.cpp | 7 +- src/library/simplifier/CMakeLists.txt | 2 +- src/library/simplifier/init_module.cpp | 6 +- src/library/simplifier/rewrite_rule_set.h | 80 ------------------- ...rewrite_rule_set.cpp => simp_rule_set.cpp} | 72 ++++++++--------- src/library/simplifier/simp_rule_set.h | 80 +++++++++++++++++++ tests/lean/rw_set2.lean.expected.out | 4 +- tests/lean/rw_set3.lean.expected.out | 4 +- 10 files changed, 138 insertions(+), 137 deletions(-) delete mode 100644 src/library/simplifier/rewrite_rule_set.h rename src/library/simplifier/{rewrite_rule_set.cpp => simp_rule_set.cpp} (64%) create mode 100644 src/library/simplifier/simp_rule_set.h diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6d350fb16..8610fbc6d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -32,7 +32,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/composition_manager.h" #include "library/definitional/projection.h" -#include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_rule_set.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" #include "frontends/lean/calc.h" @@ -190,8 +190,8 @@ void print_attributes(parser & p, name const & n) { out << " [class]"; if (is_instance(env, n)) out << " [instance]"; - if (is_rewrite_rule(env, n)) - out << " [rewrite]"; + if (is_simp_rule(env, n)) + out << " [simp]"; switch (get_reducible_status(env, n)) { case reducible_status::Reducible: out << " [reducible]"; break; case reducible_status::Irreducible: out << " [irreducible]"; break; @@ -379,13 +379,13 @@ static void print_reducible_info(parser & p, reducible_status s1) { out << n << "\n"; } -static void print_rewrite_sets(parser & p) { +static void print_simp_sets(parser & p) { io_state_stream out = p.regular_stream(); - rewrite_rule_sets s = get_rewrite_rule_sets(p.env()); + simp_rule_sets s = get_simp_rule_sets(p.env()); name prev_eqv; - s.for_each([&](name const & eqv, rewrite_rule const & rw) { + s.for_each([&](name const & eqv, simp_rule const & rw) { if (prev_eqv != eqv) { - out << "rewrite rules for " << eqv << "\n"; + out << "simplification rules for " << eqv << "\n"; prev_eqv = eqv; } out << rw.pp(out.get_formatter()) << "\n"; @@ -496,7 +496,7 @@ environment print_cmd(parser & p) { print_recursor_info(p); } else if (p.curr_is_token(get_simp_attr_tk())) { p.next(); - print_rewrite_sets(p); + print_simp_sets(p); } else if (print_polymorphic(p)) { } else { throw parser_error("invalid print command", p.pos()); diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 63eabb545..8752e342b 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/relation_manager.h" #include "library/user_recursors.h" #include "library/coercion.h" -#include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_rule_set.h" #include "frontends/lean/decl_attributes.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" @@ -218,7 +218,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c if (m_is_class) env = add_class(env, d, m_persistent); if (m_simp) - env = add_rewrite_rule(env, d, m_persistent); + env = add_simp_rule(env, d, m_persistent); if (m_has_multiple_instances) env = mark_multiple_instances(env, d, m_persistent); return env; diff --git a/src/frontends/lean/parse_simp_tactic.cpp b/src/frontends/lean/parse_simp_tactic.cpp index 6a10df64b..8a860d2b2 100644 --- a/src/frontends/lean/parse_simp_tactic.cpp +++ b/src/frontends/lean/parse_simp_tactic.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/tactic/exact_tactic.h" #include "library/tactic/expr_to_tactic.h" -#include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_rule_set.h" #include "library/simplifier/simp_tactic.h" #include "frontends/lean/parser.h" #include "frontends/lean/parse_tactic_location.h" @@ -53,8 +53,9 @@ expr parse_simp_tactic(parser & p) { while (true) { auto id_pos = p.pos(); name id = p.check_constant_next("invalid 'simp' tactic, constant expected"); - if (!is_rewrite_rule(p.env(), id)) - throw parser_error(sstream() << "invalid 'simp' tactic, '" << id << "' is not an active rewriting rule", id_pos); + if (!is_simp_rule(p.env(), id)) + throw parser_error(sstream() << "invalid 'simp' tactic, '" << id + << "' is not an active simplification rule", id_pos); hiding.push_back(id); if (!p.curr_is_token(get_comma_tk())) break; diff --git a/src/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt index c9a1ac96c..aeaa1df5f 100644 --- a/src/library/simplifier/CMakeLists.txt +++ b/src/library/simplifier/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(simplifier ceqv.cpp rewrite_rule_set.cpp init_module.cpp simp_tactic.cpp) +add_library(simplifier ceqv.cpp simp_rule_set.cpp init_module.cpp simp_tactic.cpp) target_link_libraries(simplifier ${LEAN_LIBS}) diff --git a/src/library/simplifier/init_module.cpp b/src/library/simplifier/init_module.cpp index d4e530c00..f521c8079 100644 --- a/src/library/simplifier/init_module.cpp +++ b/src/library/simplifier/init_module.cpp @@ -4,16 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_rule_set.h" #include "library/simplifier/simp_tactic.h" namespace lean { void initialize_simplifier_module() { - initialize_rewrite_rule_set(); + initialize_simp_rule_set(); initialize_simp_tactic(); } void finalize_simplifier_module() { finalize_simp_tactic(); - finalize_rewrite_rule_set(); + finalize_simp_rule_set(); } } diff --git a/src/library/simplifier/rewrite_rule_set.h b/src/library/simplifier/rewrite_rule_set.h deleted file mode 100644 index 88eb47e5b..000000000 --- a/src/library/simplifier/rewrite_rule_set.h +++ /dev/null @@ -1,80 +0,0 @@ -/* -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/type_checker.h" -#include "library/head_map.h" - -namespace lean { -class rewrite_rule_sets; - -class rewrite_rule { - name m_id; - levels m_univ_metas; - list m_metas; - expr m_lhs; - expr m_rhs; - expr m_proof; - bool m_is_permutation; - rewrite_rule(name const & id, levels const & univ_metas, list const & metas, - expr const & lhs, expr const & rhs, expr const & proof, bool is_perm); - friend rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s, name const & id, - levels const & univ_metas, expr const & e, expr const & h); -public: - name const & get_id() const { return m_id; } - levels const & get_univ_metas() const { return m_univ_metas; } - list const & get_metas() const { return m_metas; } - expr const & get_lhs() const { return m_lhs; } - expr const & get_rhs() const { return m_rhs; } - expr const & get_proof() const { return m_proof; } - bool is_perm() const { return m_is_permutation; } - friend bool operator==(rewrite_rule const & r1, rewrite_rule const & r2); - format pp(formatter const & fmt) const; -}; - -bool operator==(rewrite_rule const & r1, rewrite_rule const & r2); -inline bool operator!=(rewrite_rule const & r1, rewrite_rule const & r2) { return !operator==(r1, r2); } - -class rewrite_rule_set { - typedef head_map rule_set; - name m_eqv; - rule_set m_set; -public: - rewrite_rule_set() {} - /** \brief Return the equivalence relation associated with this set */ - rewrite_rule_set(name const & eqv); - bool empty() const { return m_set.empty(); } - name const & get_eqv() const { return m_eqv; } - void insert(rewrite_rule const & r); - void erase(rewrite_rule const & r); - list const * find(head_index const & h) const; - void for_each(std::function const & fn) const; -}; - -class rewrite_rule_sets { - name_map m_sets; // mapping from relation name to rewrite_rule_set -public: - void insert(name const & eqv, rewrite_rule const & r); - void erase(name const & eqv, rewrite_rule const & r); - void get_relations(buffer & rs) const; - rewrite_rule_set const * find(name const & eqv) const; - list const * find(name const & eqv, head_index const & h) const; - void for_each(std::function const & fn) const; -}; - -rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const & id, expr const & e, expr const & h); -rewrite_rule_sets join(rewrite_rule_sets const & s1, rewrite_rule_sets const & s2); - -environment add_rewrite_rule(environment const & env, name const & n, bool persistent = true); -/** \brief Return true if \c n is an active rewrite rule in \c env */ -bool is_rewrite_rule(environment const & env, name const & n); -/** \brief Get current rewrite rule sets */ -rewrite_rule_sets get_rewrite_rule_sets(environment const & env); -/** \brief Get rewrite rule sets in the given namespace. */ -rewrite_rule_sets get_rewrite_rule_set(environment const & env, name const & ns); -void initialize_rewrite_rule_set(); -void finalize_rewrite_rule_set(); -} diff --git a/src/library/simplifier/rewrite_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp similarity index 64% rename from src/library/simplifier/rewrite_rule_set.cpp rename to src/library/simplifier/simp_rule_set.cpp index a4565c43e..403ab773f 100644 --- a/src/library/simplifier/rewrite_rule_set.cpp +++ b/src/library/simplifier/simp_rule_set.cpp @@ -11,19 +11,19 @@ Author: Leonardo de Moura #include "library/expr_pair.h" #include "library/relation_manager.h" #include "library/simplifier/ceqv.h" -#include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simp_rule_set.h" namespace lean { -bool operator==(rewrite_rule const & r1, rewrite_rule const & r2) { +bool operator==(simp_rule const & r1, simp_rule const & r2) { return r1.m_lhs == r2.m_lhs && r1.m_rhs == r2.m_rhs; } -rewrite_rule::rewrite_rule(name const & id, levels const & univ_metas, list const & metas, - expr const & lhs, expr const & rhs, expr const & proof, bool is_perm): +simp_rule::simp_rule(name const & id, levels const & univ_metas, list const & metas, + expr const & lhs, expr const & rhs, expr const & proof, bool is_perm): m_id(id), m_univ_metas(univ_metas), m_metas(metas), m_lhs(lhs), m_rhs(rhs), m_proof(proof), m_is_permutation(is_perm) {} -format rewrite_rule::pp(formatter const & fmt) const { +format simp_rule::pp(formatter const & fmt) const { format r; r += format("#") + format(length(m_metas)); if (m_is_permutation) @@ -34,27 +34,27 @@ format rewrite_rule::pp(formatter const & fmt) const { return r; } -rewrite_rule_set::rewrite_rule_set(name const & eqv): +simp_rule_set::simp_rule_set(name const & eqv): m_eqv(eqv) {} -void rewrite_rule_set::insert(rewrite_rule const & r) { +void simp_rule_set::insert(simp_rule const & r) { m_set.insert(r.get_lhs(), r); } -list const * rewrite_rule_set::find(head_index const & h) const { +list const * simp_rule_set::find(head_index const & h) const { return m_set.find(h); } -void rewrite_rule_set::for_each(std::function const & fn) const { - m_set.for_each_entry([&](head_index const &, rewrite_rule const & r) { fn(r); }); +void simp_rule_set::for_each(std::function const & fn) const { + m_set.for_each_entry([&](head_index const &, simp_rule const & r) { fn(r); }); } -void rewrite_rule_set::erase(rewrite_rule const & r) { +void simp_rule_set::erase(simp_rule const & r) { m_set.erase(r.get_lhs(), r); } -void rewrite_rule_sets::insert(name const & eqv, rewrite_rule const & r) { - rewrite_rule_set s(eqv); +void simp_rule_sets::insert(name const & eqv, simp_rule const & r) { + simp_rule_set s(eqv); if (auto const * curr = m_sets.find(eqv)) { s = *curr; } @@ -62,9 +62,9 @@ void rewrite_rule_sets::insert(name const & eqv, rewrite_rule const & r) { m_sets.insert(eqv, s); } -void rewrite_rule_sets::erase(name const & eqv, rewrite_rule const & r) { +void simp_rule_sets::erase(name const & eqv, simp_rule const & r) { if (auto const * curr = m_sets.find(eqv)) { - rewrite_rule_set s = *curr; + simp_rule_set s = *curr; s.erase(r); if (s.empty()) m_sets.erase(eqv); @@ -73,25 +73,25 @@ void rewrite_rule_sets::erase(name const & eqv, rewrite_rule const & r) { } } -void rewrite_rule_sets::get_relations(buffer & rs) const { - m_sets.for_each([&](name const & r, rewrite_rule_set const &) { +void simp_rule_sets::get_relations(buffer & rs) const { + m_sets.for_each([&](name const & r, simp_rule_set const &) { rs.push_back(r); }); } -rewrite_rule_set const * rewrite_rule_sets::find(name const & eqv) const { +simp_rule_set const * simp_rule_sets::find(name const & eqv) const { return m_sets.find(eqv); } -list const * rewrite_rule_sets::find(name const & eqv, head_index const & h) const { +list const * simp_rule_sets::find(name const & eqv, head_index const & h) const { if (auto const * s = m_sets.find(eqv)) return s->find(h); return nullptr; } -void rewrite_rule_sets::for_each(std::function const & fn) const { - m_sets.for_each([&](name const & eqv, rewrite_rule_set const & s) { - s.for_each([&](rewrite_rule const & r) { +void simp_rule_sets::for_each(std::function const & fn) const { + m_sets.for_each([&](name const & eqv, simp_rule_set const & s) { + s.for_each([&](simp_rule const & r) { fn(eqv, r); }); }); @@ -99,11 +99,11 @@ void rewrite_rule_sets::for_each(std::function ceqvs = to_ceqvs(tc, e, h); environment const & env = tc.env(); - rewrite_rule_sets new_s = s; + simp_rule_sets new_s = s; for (expr_pair const & p : ceqvs) { expr new_e = p.first; expr new_h = p.second; @@ -118,19 +118,19 @@ rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s, } expr rel, lhs, rhs; if (is_transitive(env, new_e, rel, lhs, rhs) && is_constant(rel)) { - new_s.insert(const_name(rel), rewrite_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm)); + new_s.insert(const_name(rel), simp_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm)); } } return new_s; } -rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const & id, expr const & e, expr const & h) { +simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h) { return add_core(tc, s, id, list(), e, h); } -rewrite_rule_sets join(rewrite_rule_sets const & s1, rewrite_rule_sets const & s2) { - rewrite_rule_sets new_s1 = s1; - s2.for_each([&](name const & eqv, rewrite_rule const & r) { +simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2) { + simp_rule_sets new_s1 = s1; + s2.for_each([&](name const & eqv, simp_rule const & r) { new_s1.insert(eqv, r); }); return new_s1; @@ -140,9 +140,9 @@ static name * g_class_name = nullptr; static std::string * g_key = nullptr; struct rrs_state { - rewrite_rule_sets m_sets; + simp_rule_sets m_sets; name_set m_rnames; - name_map m_namespace_cache; + name_map m_namespace_cache; void add(environment const & env, name const & cname) { type_checker tc(env); @@ -187,26 +187,26 @@ struct rrs_config { template class scoped_ext; typedef scoped_ext rrs_ext; -environment add_rewrite_rule(environment const & env, name const & n, bool persistent) { +environment add_simp_rule(environment const & env, name const & n, bool persistent) { return rrs_ext::add_entry(env, get_dummy_ios(), n, persistent); } -bool is_rewrite_rule(environment const & env, name const & n) { +bool is_simp_rule(environment const & env, name const & n) { return rrs_ext::get_state(env).m_rnames.contains(n); } -rewrite_rule_sets get_rewrite_rule_sets(environment const & env) { +simp_rule_sets get_simp_rule_sets(environment const & env) { return rrs_ext::get_state(env).m_sets; } -void initialize_rewrite_rule_set() { +void initialize_simp_rule_set() { g_prefix = new name(name::mk_internal_unique_name()); g_class_name = new name("rrs"); g_key = new std::string("rrs"); rrs_ext::initialize(); } -void finalize_rewrite_rule_set() { +void finalize_simp_rule_set() { rrs_ext::finalize(); delete g_key; delete g_class_name; diff --git a/src/library/simplifier/simp_rule_set.h b/src/library/simplifier/simp_rule_set.h new file mode 100644 index 000000000..d2899d338 --- /dev/null +++ b/src/library/simplifier/simp_rule_set.h @@ -0,0 +1,80 @@ +/* +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/type_checker.h" +#include "library/head_map.h" + +namespace lean { +class simp_rule_sets; + +class simp_rule { + name m_id; + levels m_univ_metas; + list m_metas; + expr m_lhs; + expr m_rhs; + expr m_proof; + bool m_is_permutation; + simp_rule(name const & id, levels const & univ_metas, list const & metas, + expr const & lhs, expr const & rhs, expr const & proof, bool is_perm); + friend simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s, name const & id, + levels const & univ_metas, expr const & e, expr const & h); +public: + name const & get_id() const { return m_id; } + levels const & get_univ_metas() const { return m_univ_metas; } + list const & get_metas() const { return m_metas; } + expr const & get_lhs() const { return m_lhs; } + expr const & get_rhs() const { return m_rhs; } + expr const & get_proof() const { return m_proof; } + bool is_perm() const { return m_is_permutation; } + friend bool operator==(simp_rule const & r1, simp_rule const & r2); + format pp(formatter const & fmt) const; +}; + +bool operator==(simp_rule const & r1, simp_rule const & r2); +inline bool operator!=(simp_rule const & r1, simp_rule const & r2) { return !operator==(r1, r2); } + +class simp_rule_set { + typedef head_map rule_set; + name m_eqv; + rule_set m_set; +public: + simp_rule_set() {} + /** \brief Return the equivalence relation associated with this set */ + simp_rule_set(name const & eqv); + bool empty() const { return m_set.empty(); } + name const & get_eqv() const { return m_eqv; } + void insert(simp_rule const & r); + void erase(simp_rule const & r); + list const * find(head_index const & h) const; + void for_each(std::function const & fn) const; +}; + +class simp_rule_sets { + name_map m_sets; // mapping from relation name to simp_rule_set +public: + void insert(name const & eqv, simp_rule const & r); + void erase(name const & eqv, simp_rule const & r); + void get_relations(buffer & rs) const; + simp_rule_set const * find(name const & eqv) const; + list const * find(name const & eqv, head_index const & h) const; + void for_each(std::function const & fn) const; +}; + +simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h); +simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2); + +environment add_simp_rule(environment const & env, name const & n, bool persistent = true); +/** \brief Return true if \c n is an active rewrite rule in \c env */ +bool is_simp_rule(environment const & env, name const & n); +/** \brief Get current rewrite rule sets */ +simp_rule_sets get_simp_rule_sets(environment const & env); +/** \brief Get rewrite rule sets in the given namespace. */ +simp_rule_sets get_simp_rule_set(environment const & env, name const & ns); +void initialize_simp_rule_set(); +void finalize_simp_rule_set(); +} diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out index 8844695bc..c06137f93 100644 --- a/tests/lean/rw_set2.lean.expected.out +++ b/tests/lean/rw_set2.lean.expected.out @@ -1,4 +1,4 @@ -rewrite rules for iff +simplification rules for iff #2, ?M_1 - ?M_2 < succ ?M_1 ↦ true #1, ?M_1 < 0 ↦ false #1, ?M_1 < succ ?M_1 ↦ true @@ -9,7 +9,7 @@ rewrite rules for iff #1, succ ?M_1 ≤ ?M_1 ↦ false #1, pred ?M_1 ≤ ?M_1 ↦ true #1, ?M_1 ≤ succ ?M_1 ↦ true -rewrite rules for eq +simplification rules for eq #1, g ?M_1 ↦ f ?M_1 + 1 #2, g ?M_1 ↦ 1 #2, f ?M_1 ↦ 0 diff --git a/tests/lean/rw_set3.lean.expected.out b/tests/lean/rw_set3.lean.expected.out index 2748bba11..df6fc53e3 100644 --- a/tests/lean/rw_set3.lean.expected.out +++ b/tests/lean/rw_set3.lean.expected.out @@ -1,4 +1,4 @@ -rewrite rules for iff +simplification rules for iff #1, ?M_1 ↔ ?M_1 ↦ true #1, false ↔ ?M_1 ↦ ¬?M_1 #1, ?M_1 ↔ false ↦ ¬?M_1 @@ -15,7 +15,7 @@ rewrite rules for iff #1, ?M_1 ∨ true ↦ true #0, ¬false ↦ true #0, ¬true ↦ false -rewrite rules for eq +simplification rules for eq #2 perm, nat.add ?M_1 ?M_2 ↦ nat.add ?M_2 ?M_1 #3, ite false ?M_2 ?M_3 ↦ ?M_3 #3, ite true ?M_2 ?M_3 ↦ ?M_2