diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2ee9d3334..6fc130320 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -354,6 +354,18 @@ bool print_polymorphic(parser & p) { return false; } +static void print_reducible_info(parser & p, reducible_status s1) { + buffer r; + for_each_reducible(p.env(), [&](name const & n, reducible_status s2) { + if (s1 == s2) + r.push_back(n); + }); + io_state_stream out = p.regular_stream(); + std::sort(r.begin(), r.end()); + for (name const & n : r) + out << n << "\n"; +} + environment print_cmd(parser & p) { flycheck_information info(p.regular_stream()); if (info.enabled()) { @@ -370,6 +382,15 @@ environment print_cmd(parser & p) { options opts = out.get_options(); opts = opts.update(get_pp_notation_option_name(), false); out.update_options(opts) << e << endl; + } else if (p.curr_is_token_or_id(get_reducible_tk())) { + p.next(); + print_reducible_info(p, reducible_status::Reducible); + } else if (p.curr_is_token_or_id(get_quasireducible_tk())) { + p.next(); + print_reducible_info(p, reducible_status::Quasireducible); + } else if (p.curr_is_token_or_id(get_irreducible_tk())) { + p.next(); + print_reducible_info(p, reducible_status::Irreducible); } else if (p.curr_is_token_or_id(get_options_tk())) { p.next(); p.regular_stream() << p.ios().get_options() << endl; diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 586757fba..59fe3f6b9 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -21,19 +21,10 @@ struct reducible_entry { reducible_entry(reducible_status s, name const & n):m_status(s), m_name(n) {} }; -class reducible_state { - name_map m_status; -public: - void add(reducible_entry const & e); - reducible_status get_status(name const & n) const; -}; +typedef name_map reducible_state; -void reducible_state::add(reducible_entry const & e) { - m_status.insert(e.m_name, e.m_status); -} - -reducible_status reducible_state::get_status(name const & n) const { - if (auto it = m_status.find(n)) +static reducible_status get_status(reducible_state const & s, name const & n) { + if (auto it = s.find(n)) return *it; else return reducible_status::Semireducible; @@ -46,7 +37,7 @@ struct reducible_config { typedef reducible_state state; typedef reducible_entry entry; static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - s.add(e); + s.insert(e.m_name, e.m_status); } static name const & get_class_name() { return *g_class_name; @@ -87,6 +78,11 @@ void finalize_reducible() { delete g_class_name; } +void for_each_reducible(environment const & env, std::function const & fn) { + reducible_state m_state = reducible_ext::get_state(env); + m_state.for_each(fn); +} + static void check_declaration(environment const & env, name const & n) { declaration const & d = env.get(n); if (!d.is_definition()) @@ -100,7 +96,7 @@ environment set_reducible(environment const & env, name const & n, reducible_sta reducible_status get_reducible_status(environment const & env, name const & n) { reducible_state const & s = reducible_ext::get_state(env); - return s.get_status(n); + return get_status(s, n); } bool is_at_least_quasireducible(environment const & env, name const & n) { @@ -111,14 +107,14 @@ bool is_at_least_quasireducible(environment const & env, name const & n) { name_predicate mk_not_reducible_pred(environment const & env) { reducible_state m_state = reducible_ext::get_state(env); return [=](name const & n) { // NOLINT - return m_state.get_status(n) != reducible_status::Reducible; + return get_status(m_state, n) != reducible_status::Reducible; }; } name_predicate mk_not_quasireducible_pred(environment const & env) { reducible_state m_state = reducible_ext::get_state(env); return [=](name const & n) { // NOLINT - auto r = m_state.get_status(n); + auto r = get_status(m_state, n); return r != reducible_status::Reducible && r != reducible_status::Quasireducible; }; } @@ -126,7 +122,7 @@ name_predicate mk_not_quasireducible_pred(environment const & env) { name_predicate mk_irreducible_pred(environment const & env) { reducible_state m_state = reducible_ext::get_state(env); return [=](name const & n) { // NOLINT - return m_state.get_status(n) == reducible_status::Irreducible; + return get_status(m_state, n) == reducible_status::Irreducible; }; } diff --git a/src/library/reducible.h b/src/library/reducible.h index 83a65be90..b89a0894d 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -28,6 +28,9 @@ reducible_status get_reducible_status(environment const & env, name const & n); bool is_at_least_quasireducible(environment const & env, name const & n); +/* \brief Execute the given function for each declaration explicitly marked with a reducibility annotation */ +void for_each_reducible(environment const & env, std::function const & fn); + /** \brief Create a predicate that returns true for all non reducible constants in \c env */ name_predicate mk_not_reducible_pred(environment const & env); /** \brief Create a predicate that returns true for all non reducible and non quasireducible constants in \c env */ diff --git a/tests/lean/print_reducible.lean b/tests/lean/print_reducible.lean new file mode 100644 index 000000000..4a138c716 --- /dev/null +++ b/tests/lean/print_reducible.lean @@ -0,0 +1,19 @@ +prelude + +definition id₁ [reducible] {A : Type} (a : A) := a +definition id₂ [reducible] {A : Type} (a : A) := a + +definition id₄ [quasireducible] {A : Type} (a : A) := a +definition id₃ [quasireducible] {A : Type} (a : A) := a + +definition id₅ [irreducible] {A : Type} (a : A) := a +definition id₆ [irreducible] {A : Type} (a : A) := a + +definition pr [reducible] {A B : Type} (a : A) (b : B) := a +definition pr2 {A B : Type} (a : A) (b : B) := a + +print [reducible] +print "-----------" +print [quasireducible] +print "-----------" +print [irreducible] diff --git a/tests/lean/print_reducible.lean.expected.out b/tests/lean/print_reducible.lean.expected.out new file mode 100644 index 000000000..8148738a0 --- /dev/null +++ b/tests/lean/print_reducible.lean.expected.out @@ -0,0 +1,9 @@ +id₁ +id₂ +pr +----------- +id₃ +id₄ +----------- +id₅ +id₆