From 966e0109ffa0709f0cd8da23cdf87dbf13d45ca7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jul 2015 12:57:28 -0700 Subject: [PATCH] feat(library/simplifier): initialize simplification set. --- src/frontends/lean/builtin_cmds.cpp | 24 ++----- src/frontends/lean/parse_simp_tactic.cpp | 4 -- src/library/simplifier/simp_rule_set.cpp | 82 ++++++++++++++++++++++++ src/library/simplifier/simp_rule_set.h | 13 ++++ src/library/simplifier/simp_tactic.cpp | 21 +++++- 5 files changed, 120 insertions(+), 24 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index fdfb768b4..c24c8eda2 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -392,30 +392,16 @@ static void print_simp_rules(parser & p) { } else { s = get_simp_rule_sets(p.env()); } - name prev_eqv; - s.for_each_simp([&](name const & eqv, simp_rule const & rw) { - if (prev_eqv != eqv) { - out << "simplification rules for " << eqv; - if (!ns.is_anonymous()) - out << " at namespace '" << ns << "'"; - out << "\n"; - prev_eqv = eqv; - } - out << rw.pp(out.get_formatter()) << "\n"; - }); + format header; + if (!ns.is_anonymous()) + header = format(" at namespace '") + format(ns) + format("'"); + out << s.pp_simp(out.get_formatter(), header); } static void print_congr_rules(parser & p) { io_state_stream out = p.regular_stream(); simp_rule_sets s = get_simp_rule_sets(p.env()); - name prev_eqv; - s.for_each_congr([&](name const & eqv, congr_rule const & cr) { - if (prev_eqv != eqv) { - out << "congruencec rules for " << eqv << "\n"; - prev_eqv = eqv; - } - out << cr.pp(out.get_formatter()) << "\n"; - }); + out << s.pp_congr(out.get_formatter()); } environment print_cmd(parser & p) { diff --git a/src/frontends/lean/parse_simp_tactic.cpp b/src/frontends/lean/parse_simp_tactic.cpp index 8a860d2b2..f25e0cfb3 100644 --- a/src/frontends/lean/parse_simp_tactic.cpp +++ b/src/frontends/lean/parse_simp_tactic.cpp @@ -51,11 +51,7 @@ expr parse_simp_tactic(parser & p) { p.next(); p.check_token_next(get_lbracket_tk(), "invalid 'simp' tactic, '[' expected"); while (true) { - auto id_pos = p.pos(); name id = p.check_constant_next("invalid 'simp' tactic, constant expected"); - 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/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp index 14c39f7d6..4509b3449 100644 --- a/src/library/simplifier/simp_rule_set.cpp +++ b/src/library/simplifier/simp_rule_set.cpp @@ -99,6 +99,24 @@ void simp_rule_set::for_each_congr(std::function const m_congr_set.for_each_entry([&](head_index const &, congr_rule const & r) { fn(r); }); } +void simp_rule_set::erase_simp(name_set const & ids) { + // This method is not very smart and doesn't use any indexing or caching. + // So, it may be a bottleneck in the future + buffer to_delete; + for_each_simp([&](simp_rule const & r) { + if (ids.contains(r.get_id())) { + to_delete.push_back(r); + } + }); + for (simp_rule const & r : to_delete) { + erase(r); + } +} + +void simp_rule_set::erase_simp(buffer const & ids) { + erase_simp(to_name_set(ids)); +} + template void simp_rule_sets::insert_core(name const & eqv, R const & r) { simp_rule_set s(eqv); @@ -143,6 +161,20 @@ void simp_rule_sets::get_relations(buffer & rs) const { }); } +void simp_rule_sets::erase_simp(name_set const & ids) { + name_map new_sets; + m_sets.for_each([&](name const & n, simp_rule_set const & s) { + simp_rule_set new_s = s; + new_s.erase_simp(ids); + new_sets.insert(n, new_s); + }); + m_sets = new_sets; +} + +void simp_rule_sets::erase_simp(buffer const & ids) { + erase_simp(to_name_set(ids)); +} + simp_rule_set const * simp_rule_sets::find(name const & eqv) const { return m_sets.find(eqv); } @@ -175,6 +207,50 @@ void simp_rule_sets::for_each_congr(std::function const & ids); list const * find_simp(head_index const & h) const; void for_each_simp(std::function const & fn) const; list const * find_congr(head_index const & h) const; @@ -90,12 +93,19 @@ public: void erase(name const & eqv, simp_rule const & r); void insert(name const & eqv, congr_rule const & r); void erase(name const & eqv, congr_rule const & r); + void erase_simp(name_set const & ids); + void erase_simp(buffer const & ids); void get_relations(buffer & rs) const; simp_rule_set const * find(name const & eqv) const; list const * find_simp(name const & eqv, head_index const & h) const; list const * find_congr(name const & eqv, head_index const & h) const; void for_each_simp(std::function const & fn) const; void for_each_congr(std::function const & fn) const; + format pp(formatter const & fmt, format const & header, bool simp, bool congr) const; + format pp_simp(formatter const & fmt, format const & header) const; + format pp_simp(formatter const & fmt) const; + format pp_congr(formatter const & fmt) const; + format pp(formatter const & fmt) const; }; simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h); @@ -112,6 +122,9 @@ bool is_congr_rule(environment const & env, name const & n); simp_rule_sets get_simp_rule_sets(environment const & env); /** \brief Get simplification rule sets in the given namespace. */ simp_rule_sets get_simp_rule_sets(environment const & env, name const & ns); + +io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s); + void initialize_simp_rule_set(); void finalize_simp_rule_set(); } diff --git a/src/library/simplifier/simp_tactic.cpp b/src/library/simplifier/simp_tactic.cpp index a7d5a7a40..8ef0c6224 100644 --- a/src/library/simplifier/simp_tactic.cpp +++ b/src/library/simplifier/simp_tactic.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/tactic/expr_to_tactic.h" #include "library/simplifier/simp_tactic.h" +#include "library/simplifier/simp_rule_set.h" #ifndef LEAN_DEFAULT_SIMP_SINGLE_PASS #define LEAN_DEFAULT_SIMP_SINGLE_PASS false @@ -135,6 +136,8 @@ private: goal m_g; substitution m_subst; + simp_rule_sets m_simp_set; + // configuration options bool m_single_pass; bool m_bottom_up; @@ -148,6 +151,8 @@ private: bool m_propext; bool m_standard; + io_state_stream out() const { return regular(m_env, m_ios); } + void set_options(environment const & env, options const & o) { m_single_pass = get_simp_single_pass(o); m_bottom_up = get_simp_bottom_up(o); @@ -179,11 +184,25 @@ private: return false; } + // Initialize m_simp_set with information that is context independent + void init_simp_set(buffer const & ns, buffer const & ex) { + m_simp_set = get_simp_rule_sets(m_env); + for (name const & n : ns) { + simp_rule_sets tmp_simp_set = get_simp_rule_sets(m_env, n); + m_simp_set = join(m_simp_set, tmp_simp_set); + } + m_simp_set.erase_simp(ex); + if (m_trace) { + out() << m_simp_set; + } + } + public: simp_tactic_fn(environment const & env, io_state const & ios, name_generator && ngen, - buffer const & /* ls */, buffer const & /* ns */, buffer const & /* ex */, + buffer const & /* ls */, buffer const & ns, buffer const & ex, optional const & tac):m_env(env), m_ios(ios), m_ngen(ngen), m_tactic(tac) { set_options(env, m_ios.get_options()); + init_simp_set(ns, ex); } std::tuple operator()(goal const & g, location const & loc, substitution const & s) {