refactor(library,frontends/lean): simplify the creation of custom normalizers

src/frontends/lean/calc_proof_elaborator.cpp

@@ -110,28 +110,10 @@ static optional<pair<expr, expr>> apply_subst(environment const & env, local_con
     return optional<pair<expr, expr>>();
 }
 
-/** \brief Custom converter that does not unfold given relation */
-class calc_converter : public unfold_semireducible_converter {
-    environment m_env;
-    name        m_rel;
-public:
-    calc_converter(environment const & env, name const & r):unfold_semireducible_converter(env, true), m_rel(r) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (m_rel == d.get_name())
-            return true;
-        return unfold_semireducible_converter::is_opaque(d);
-    }
-};
-
-type_checker_ptr mk_calc_type_checker(environment const & env, name_generator && ngen, name const & rel) {
-    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-           std::unique_ptr<converter>(new calc_converter(env, rel))));
-}
-
 // Return true if \c e is convertible to a term of the form (h ...).
 // If the result is true, update \c e and \c cs.
 bool try_normalize_to_head(environment const & env, name_generator && ngen, name const & h, expr & e, constraint_seq & cs) {
-    type_checker_ptr tc = mk_calc_type_checker(env, std::move(ngen), h);
+    type_checker_ptr tc = mk_type_checker(env, std::move(ngen), [=](name const & n) { return n == h; });
     constraint_seq new_cs;
     expr new_e = tc->whnf(e, new_cs);
     expr const & fn = get_app_fn(new_e);

src/frontends/lean/elaborator.cpp

@@ -56,40 +56,18 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_cmds.h"
 
 namespace lean {
-/** \brief Custom converter that does not unfold constants that contains coercions from it.
-    We use this converter for detecting whether we have coercions from a given type. */
-class coercion_from_converter : public unfold_semireducible_converter {
-    environment m_env;
-public:
-    coercion_from_converter(environment const & env):unfold_semireducible_converter(env, true), m_env(env) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (has_coercions_from(m_env, d.get_name()))
-            return true;
-        return unfold_semireducible_converter::is_opaque(d);
-    }
-};
-
-/** \brief Custom converter that does not unfold constants that contains coercions to it.
-    We use this converter for detecting whether we have coercions to a given type. */
-class coercion_to_converter : public unfold_semireducible_converter {
-    environment m_env;
-public:
-    coercion_to_converter(environment const & env):unfold_semireducible_converter(env, true), m_env(env) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (has_coercions_to(m_env, d.get_name()))
-            return true;
-        return unfold_semireducible_converter::is_opaque(d);
-    }
-};
-
 type_checker_ptr mk_coercion_from_type_checker(environment const & env, name_generator && ngen) {
-    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-           std::unique_ptr<converter>(new coercion_from_converter(env))));
+    auto irred_pred = mk_irreducible_pred(env);
+    return mk_type_checker(env, std::move(ngen), [=](name const & n) {
+            return has_coercions_from(env, n) || irred_pred(n);
+        });
 }
 
 type_checker_ptr mk_coercion_to_type_checker(environment const & env, name_generator && ngen) {
-    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-           std::unique_ptr<converter>(new coercion_to_converter(env))));
+    auto irred_pred = mk_irreducible_pred(env);
+    return mk_type_checker(env, std::move(ngen), [=](name const & n) {
+            return has_coercions_to(env, n) || irred_pred(n);
+        });
 }
 
 /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m

src/frontends/lean/migrate_cmd.cpp

@@ -38,28 +38,6 @@ static name * g_migrate_trace  = nullptr;
 
 bool get_migrate_trace(options const & o) { return o.get_bool(*g_migrate_trace, LEAN_DEFAULT_MIGRATE_TRACE); }
 
-/** \brief Converter used by the migrate command. It treat
-    definitions from a given set of namespaces as opaque.
-*/
-class migrate_converter : public unfold_semireducible_converter {
-    list<name> m_namespaces;
-public:
-    migrate_converter(environment const & env, list<name> const & ns):
-        unfold_semireducible_converter(env, true),
-        m_namespaces(ns) {
-    }
-
-    virtual bool is_opaque(declaration const & d) const {
-        name const & n = d.get_name();
-        if (!is_instance(m_env, n) &&
-            std::any_of(m_namespaces.begin(), m_namespaces.end(), [&](name const & ns) {
-                    return is_prefix_of(ns, n);
-                }))
-            return true;
-        return default_converter::is_opaque(d);
-    }
-};
-
 struct migrate_cmd_fn {
     parser &                 m_p;
     environment              m_env;
@@ -416,10 +394,21 @@ struct migrate_cmd_fn {
     environment operator()() {
         m_pos = m_p.pos();
 
-        m_migrate_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
-                       std::unique_ptr<converter>(new migrate_converter(m_env, get_namespaces(m_env)))));
-        m_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
-               std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true))));
+        auto m_namespaces = get_namespaces(m_env);
+        auto irred_pred   = mk_irreducible_pred(m_env);
+        /* auxiliary predicate for custom converter used by the migrate command. It treats
+           definitions from a given set of namespaces as opaque.
+        */
+        auto opaque_pred = [=](name const & n) {
+            if (!is_instance(m_env, n) &&
+                std::any_of(m_namespaces.begin(), m_namespaces.end(), [&](name const & ns) {
+                        return is_prefix_of(ns, n);
+                    }))
+                return true;
+            return irred_pred(n);
+        };
+        m_migrate_tc = mk_type_checker(m_env, m_ngen.mk_child(), opaque_pred);
+        m_tc         = mk_type_checker(m_env, m_ngen.mk_child(), UnfoldSemireducible);
 
         parse_params();
         parse_from_namespace();

src/library/reducible.cpp

@@ -21,6 +21,13 @@ struct reducible_entry {
     reducible_entry(reducible_status s, name const & n):m_status(s), m_name(n) {}
 };
 
+class reducible_state {
+    name_map<reducible_status> m_status;
+public:
+    void add(reducible_entry const & e);
+    reducible_status get_status(name const & n) const;
+};
+
 void reducible_state::add(reducible_entry const & e) {
     m_status.insert(e.m_name, e.m_status);
 }
@@ -101,68 +108,46 @@ bool is_at_least_quasireducible(environment const & env, name const & n) {
     return r == reducible_status::Reducible || r == reducible_status::Quasireducible;
 }
 
-unfold_reducible_converter::unfold_reducible_converter(environment const & env, bool memoize):
-    default_converter(env, memoize) {
-    m_state = reducible_ext::get_state(env);
+name_predicate mk_not_reducible_pred(environment const & env) {
+    reducible_state m_state = reducible_ext::get_state(env);
+    return [=](name const & n) {
+        return m_state.get_status(n) != reducible_status::Reducible;
+    };
 }
 
-bool unfold_reducible_converter::is_opaque(declaration const & d) const {
-    auto r = m_state.get_status(d.get_name());
-    if (r != reducible_status::Reducible) return true;
-    return default_converter::is_opaque(d);
+name_predicate mk_not_quasireducible_pred(environment const & env) {
+    reducible_state m_state = reducible_ext::get_state(env);
+    return [=](name const & n) {
+        auto r = m_state.get_status(n);
+        return r != reducible_status::Reducible && r != reducible_status::Quasireducible;
+    };
 }
 
-unfold_quasireducible_converter::unfold_quasireducible_converter(environment const & env, bool memoize):
-    default_converter(env, memoize) {
-    m_state = reducible_ext::get_state(env);
+name_predicate mk_irreducible_pred(environment const & env) {
+    reducible_state m_state = reducible_ext::get_state(env);
+    return [=](name const & n) {
+        return m_state.get_status(n) == reducible_status::Irreducible;
+    };
 }
 
-bool unfold_quasireducible_converter::is_opaque(declaration const & d) const {
-    auto r = m_state.get_status(d.get_name());
-    if (r != reducible_status::Reducible && r != reducible_status::Quasireducible) return true;
-    return default_converter::is_opaque(d);
-}
-
-unfold_semireducible_converter::unfold_semireducible_converter(environment const & env, bool memoize):
-    default_converter(env, memoize) {
-    m_state = reducible_ext::get_state(env);
-}
-
-bool unfold_semireducible_converter::is_opaque(declaration const & d) const {
-    auto r = m_state.get_status(d.get_name());
-    if (r == reducible_status::Irreducible) return true;
-    return default_converter::is_opaque(d);
-}
-
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator && ngen,
-                                              reducible_behavior rb, bool memoize) {
+type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, reducible_behavior rb) {
     switch (rb) {
     case UnfoldReducible:
-        return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-               std::unique_ptr<converter>(new unfold_reducible_converter(env, memoize))));
+        return mk_type_checker(env, std::move(ngen), mk_not_reducible_pred(env));
     case UnfoldQuasireducible:
-        return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-               std::unique_ptr<converter>(new unfold_quasireducible_converter(env, memoize))));
+        return mk_type_checker(env, std::move(ngen), mk_not_quasireducible_pred(env));
     case UnfoldSemireducible:
-        return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-               std::unique_ptr<converter>(new unfold_semireducible_converter(env, memoize))));
+        return mk_type_checker(env, std::move(ngen), mk_irreducible_pred(env));
     }
     lean_unreachable();
 }
 
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior rb) {
+type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb) {
     return mk_type_checker(env, name_generator(*g_tmp_prefix), rb);
 }
 
-class opaque_converter : public default_converter {
-public:
-    opaque_converter(environment const & env): default_converter(env) {}
-    virtual bool is_opaque(declaration const &) const { return true; }
-};
-
-std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator && ngen) {
-    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
-                                                          std::unique_ptr<converter>(new opaque_converter(env))));
+type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen) {
+    return mk_type_checker(env, std::move(ngen), [](name const &) { return true; });
 }
 
 static int mk_opaque_type_checker(lua_State * L) {

src/library/reducible.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include "kernel/type_checker.h"
 #include "kernel/default_converter.h"
+#include "library/util.h"
 
 namespace lean {
 enum class reducible_status { Reducible, Quasireducible, Semireducible, Irreducible };
@@ -27,49 +28,22 @@ reducible_status get_reducible_status(environment const & env, name const & n);
 
 bool is_at_least_quasireducible(environment const & env, name const & n);
 
-struct reducible_entry;
-
-class reducible_state {
-    name_map<reducible_status> m_status;
-public:
-    void add(reducible_entry const & e);
-    reducible_status get_status(name const & n) const;
-};
-
-/** \brief Unfold only constants marked as reducible */
-class unfold_reducible_converter : public default_converter {
-    reducible_state m_state;
-public:
-    unfold_reducible_converter(environment const & env, bool memoize);
-    virtual bool is_opaque(declaration const & d) const;
-};
-
-/** \brief Unfold only constants marked as reducible or quasireducible */
-class unfold_quasireducible_converter : public default_converter {
-    reducible_state m_state;
-public:
-    unfold_quasireducible_converter(environment const & env, bool memoize);
-    virtual bool is_opaque(declaration const & d) const;
-};
-
-/** \brief Unfold only constants marked as reducible, quasireducible, or semireducible */
-class unfold_semireducible_converter : public default_converter {
-    reducible_state m_state;
-public:
-    unfold_semireducible_converter(environment const & env, bool memoize);
-    virtual bool is_opaque(declaration const & d) const;
-};
+/** \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 */
+name_predicate mk_not_quasireducible_pred(environment const & env);
+/** \brief Create a predicate that returns true for irreducible constants  in \c env */
+name_predicate mk_irreducible_pred(environment const & env);
 
 enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible };
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator && ngen,
-                                              reducible_behavior r = UnfoldSemireducible,
-                                              bool memoize = true);
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
+type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen,
+                                 reducible_behavior r = UnfoldSemireducible);
+type_checker_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
 
 /** \brief Create a type checker that treats all definitions as opaque. */
-std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator && ngen);
+type_checker_ptr mk_opaque_type_checker(environment const & env, name_generator && ngen);
 
 void initialize_reducible();
 void finalize_reducible();

src/library/tactic/rewrite_tactic.cpp

@@ -1424,24 +1424,15 @@ class rewrite_fn {
         }
     }
 
-    class match_converter : public unfold_reducible_converter {
-    public:
-        match_converter(environment const & env):
-            unfold_reducible_converter(env, true) {}
-        virtual bool is_opaque(declaration const & d) const {
-            if (is_projection(m_env, d.get_name()))
-                return true;
-            return unfold_reducible_converter::is_opaque(d);
-        }
-    };
-
     type_checker_ptr mk_matcher_tc() {
         if (get_rewriter_syntactic(m_ios.get_options())) {
             // use an everything opaque converter
             return mk_opaque_type_checker(m_env, m_ngen.mk_child());
         } else {
-            return std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
-                   std::unique_ptr<converter>(new match_converter(m_env))));
+            auto aux_pred = mk_not_reducible_pred(m_env);
+            return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) {
+                    return is_projection(m_env, n) || aux_pred(n);
+                });
         }
     }
 

src/library/util.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
+#include "kernel/default_converter.h"
 #include "kernel/metavar.h"
 #include "kernel/inductive/inductive.h"
 #include "library/locals.h"
@@ -713,4 +714,21 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
             return pp_type_mismatch(fmt, s.instantiate(v), s.instantiate(v_type), s.instantiate(t));
         });
 }
+
+class extra_opaque_converter : public default_converter {
+    name_predicate m_pred;
+public:
+    extra_opaque_converter(environment const & env, name_predicate const & p):default_converter(env, true), m_pred(p) {}
+    virtual bool is_opaque(declaration const & d) const {
+        if (m_pred(d.get_name()))
+            return true;
+        return default_converter::is_opaque(d);
+    }
+};
+
+type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) {
+    return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
+                                         std::unique_ptr<converter>(new extra_opaque_converter(env, pred))));
+
+}
 }

src/library/util.h

@@ -225,6 +225,9 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
     return mk_type_mismatch_jst(v, v_type, t, v);
 }
 
+/** \brief Create a type checker and normalizer that treats any constant named \c n as opaque when pred(n) is true */
+type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred);
+
 void initialize_library_util();
 void finalize_library_util();
 }

src/util/name.h

@@ -186,6 +186,8 @@ struct name_pair_quick_cmp {
     }
 };
 
+typedef std::function<bool(name const &)> name_predicate;
+
 serializer & operator<<(serializer & s, name const & n);
 name read_name(deserializer & d);
 inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }