refactor(library/unifier): store the unifier_plugin in the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/elaborator.cpp

@@ -50,7 +50,6 @@ class elaborator {
 
     environment         m_env;
     io_state            m_ios;
-    unifier_plugin      m_plugin;
     name_generator      m_ngen;
     type_checker        m_tc;
     substitution        m_subst;
@@ -195,7 +194,6 @@ public:
     elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp,
                bool check_unassigned):
         m_env(env), m_ios(ios),
-        m_plugin([](constraint const &, name_generator const &) { return lazy_list<list<constraint>>(); }),
         m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, true /* unfold opaque from the main module */)),
         m_pos_provider(pp) {
         m_check_unassigned = check_unassigned;
@@ -742,8 +740,7 @@ public:
         buffer<constraint> cs;
         cs.append(m_constraints);
         m_constraints.clear();
-        return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), m_plugin,
-                     true, m_ios.get_options());
+        return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), true, m_ios.get_options());
     }
 
     void collect_metavars(expr const & e, buffer<expr> & mvars) {

src/library/CMakeLists.txt

@@ -4,7 +4,8 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
   private.cpp placeholder.cpp aliases.cpp level_names.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
-  unifier.cpp explicit.cpp num.cpp string.cpp)
+  unifier.cpp unifier_plugin.cpp
+  explicit.cpp num.cpp string.cpp)
 # hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/tactic/apply_tactic.cpp

@@ -117,7 +117,7 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
         }
     }
     list<expr> meta_lst = to_list(metas.begin(), metas.end());
-    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options());
+    lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
     return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
             name_generator new_ngen(ngen);
             type_checker tc(env, new_ngen.mk_child());

src/library/unifier.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 #include "library/occurs.h"
 #include "library/unifier.h"
+#include "library/unifier_plugin.h"
 #include "library/kernel_bindings.h"
 
 namespace lean {
@@ -328,9 +329,9 @@ struct unifier_fn {
     optional<justification> m_conflict; //!< if different from none, then there is a conflict.
 
     unifier_fn(environment const & env, unsigned num_cs, constraint const * cs,
-               name_generator const & ngen, substitution const & s, unifier_plugin const & p,
+               name_generator const & ngen, substitution const & s,
                bool use_exception, unsigned max_steps, bool unfold_opaque):
-        m_env(env), m_ngen(ngen), m_subst(s), m_plugin(p),
+        m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
         m_tc(env, m_ngen.mk_child(), mk_default_converter(env, unfold_opaque)),
         m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
         m_next_assumption_idx = 0;
@@ -602,7 +603,7 @@ struct unifier_fn {
         }
 
         // We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
-        if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs) || is_meta_intro_app(lhs) || is_meta_intro_app(rhs)) {
+        if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs) || is_meta_intro_app(lhs) || is_meta_intro_app(rhs) || m_plugin->delay_constraint(m_tc, c)) {
             add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::Reduction);
         } else if (is_meta(lhs) && is_meta(rhs)) {
             // flex-flex constraints are delayed the most.
@@ -807,7 +808,7 @@ struct unifier_fn {
 
     bool process_plugin_constraint(constraint const & c) {
         lean_assert(!is_choice_cnstr(c));
-        lazy_list<constraints> alts = m_plugin(c, m_ngen.mk_child());
+        lazy_list<constraints> alts = m_plugin->solve(m_tc, c, m_ngen.mk_child());
         return process_lazy_constraints(alts, c.get_justification());
     }
 
@@ -1253,10 +1254,6 @@ struct unifier_fn {
     }
 };
 
-unifier_plugin get_noop_unifier_plugin() {
-    return [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }; // NOLINT
-}
-
 lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) {
     if (!u->more_solutions()) {
         u->failure(); // make sure exception is thrown if u->m_use_exception is true
@@ -1273,17 +1270,17 @@ lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) {
 }
 
 lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p, bool use_exception, unsigned max_steps, bool unfold_opaque) {
-    return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, substitution(), p, use_exception, max_steps, unfold_opaque));
+                              bool use_exception, unsigned max_steps, bool unfold_opaque) {
+    return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, substitution(), use_exception, max_steps, unfold_opaque));
 }
 
 lazy_list<substitution> unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p, bool use_exception, options const & o) {
-    return unify(env, num_cs, cs, ngen, p, use_exception, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
+                              bool use_exception, options const & o) {
+    return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              unifier_plugin const & p, unsigned max_steps, bool unfold_opaque) {
+                              unsigned max_steps, bool unfold_opaque) {
     name_generator new_ngen(ngen);
     type_checker tc(env, new_ngen.mk_child());
     expr _lhs = s.instantiate(lhs);
@@ -1297,13 +1294,13 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
     if (cs.empty()) {
         return lazy_list<substitution>(s);
     } else {
-        return unify(std::make_shared<unifier_fn>(env, cs.size(), cs.data(), ngen, s, p, false, max_steps, unfold_opaque));
+        return unify(std::make_shared<unifier_fn>(env, cs.size(), cs.data(), ngen, s, false, max_steps, unfold_opaque));
     }
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              substitution const & s, unifier_plugin const & p, options const & o) {
-    return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
+                              substitution const & s, options const & o) {
+    return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o), get_unifier_unfold_opaque(o));
 }
 
 static int unify_simple(lua_State * L) {
@@ -1428,18 +1425,16 @@ static int unify(lua_State * L) {
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
         if (nargs == 6)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(),
-                      to_options(L, 6));
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(),
-                      options());
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), options());
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
         if (nargs == 4)
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, to_options(L, 4));
+            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), false, to_options(L, 4));
         else
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), false, options());
+            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), false, options());
     }
     return push_substitution_seq_it(L, r);
 }

src/library/unifier.h

@@ -39,26 +39,16 @@ std::pair<unify_status, substitution> unify_simple(substitution const & s, expr
 std::pair<unify_status, substitution> unify_simple(substitution const & s, level const & lhs, level const & rhs, justification const & j);
 std::pair<unify_status, substitution> unify_simple(substitution const & s, constraint const & c);
 
-/**
-   \brief A unifier_plugin provides a simple way to extend the \c unify procedures.
-   Whenever, the default implementation does not know how to solve a constraint, it invokes the plugin.
-   The plugin return a lazy_list (stream) of possible solutions. Each "solution" is represented as
-   a new list of constraints.
-*/
-typedef std::function<lazy_list<constraints>(constraint const &, name_generator const &)> unifier_plugin;
-
-unifier_plugin get_noop_unifier_plugin();
-
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true,
-                              unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
+                              bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS,
+                              bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
-                              unifier_plugin const & p, bool use_exception, options const & o);
+                              bool use_exception, options const & o);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              substitution const & s = substitution(), unifier_plugin const & p = get_noop_unifier_plugin(),
-                              unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
+                              substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS,
+                              bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
-                              unifier_plugin const & p, options const & o);
+                              options const & o);
 
 class unifier_exception : public exception {
     justification m_jst;

src/library/unifier_plugin.cpp

@@ -0,0 +1,86 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/lazy_list_fn.h"
+#include "library/unifier_plugin.h"
+
+namespace lean {
+class binary_unifier_plugin_cell : public unifier_plugin_cell {
+protected:
+    unifier_plugin m_p1;
+    unifier_plugin m_p2;
+public:
+    binary_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):m_p1(p1), m_p2(p2) {}
+    virtual bool delay_constraint(type_checker & tc, constraint const & c) const {
+        return m_p1->delay_constraint(tc, c) || m_p2->delay_constraint(tc, c);
+    }
+};
+
+class append_unifier_plugin_cell : public binary_unifier_plugin_cell {
+public:
+    append_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
+    virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator const & ngen) const {
+        return append(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen));
+    }
+};
+
+class orelse_unifier_plugin_cell : public binary_unifier_plugin_cell {
+public:
+    orelse_unifier_plugin_cell(unifier_plugin const & p1, unifier_plugin const & p2):binary_unifier_plugin_cell(p1, p2) {}
+    virtual lazy_list<constraints> solve(type_checker & tc, constraint const & c, name_generator const & ngen) const {
+        return orelse(m_p1->solve(tc, c, ngen), m_p2->solve(tc, c, ngen));
+    }
+};
+
+unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2) {
+    return std::make_shared<append_unifier_plugin_cell>(p1, p2);
+}
+
+unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2) {
+    return std::make_shared<orelse_unifier_plugin_cell>(p1, p2);
+}
+
+static unifier_plugin noop_unifier_plugin() {
+    class noop_unifier_plugin_cell : public unifier_plugin_cell {
+    public:
+        virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator const &) const {
+            return lazy_list<constraints>();
+        }
+        virtual bool delay_constraint(type_checker &, constraint const &) const { return false; }
+    };
+    return std::make_shared<noop_unifier_plugin_cell>();
+}
+
+struct unifier_plugin_ext : public environment_extension {
+    unifier_plugin m_plugin;
+    unifier_plugin_ext() {
+        m_plugin = noop_unifier_plugin();
+    }
+};
+
+struct unifier_plugin_ext_reg {
+    unsigned m_ext_id;
+    unifier_plugin_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<unifier_plugin_ext>()); }
+};
+
+static unifier_plugin_ext_reg g_ext;
+static unifier_plugin_ext const & get_extension(environment const & env) {
+    return static_cast<unifier_plugin_ext const &>(env.get_extension(g_ext.m_ext_id));
+}
+static environment update(environment const & env, unifier_plugin_ext const & ext) {
+    return env.update(g_ext.m_ext_id, std::make_shared<unifier_plugin_ext>(ext));
+}
+
+environment set_unifier_plugin(environment const & env, unifier_plugin const & p) {
+    unifier_plugin_ext ext = get_extension(env);
+    ext.m_plugin = p;
+    return update(env, ext);
+}
+
+unifier_plugin const & get_unifier_plugin(environment const & env) {
+    return get_extension(env).m_plugin;
+}
+}

src/library/unifier_plugin.h

@@ -0,0 +1,38 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/lazy_list.h"
+#include "kernel/environment.h"
+#include "kernel/constraint.h"
+#include "kernel/type_checker.h"
+
+namespace lean {
+/**
+   \brief A unifier_plugin provides a simple way to extend the \c unify procedures.
+   Whenever, the default implementation does not know how to solve a constraint, it invokes the plugin.
+   The plugin return a lazy_list (stream) of possible solutions. Each "solution" is represented as
+   a new list of constraints.
+
+   The method \c delay_constraint is invoked to decide whether the particular constraint should
+   be delayed. This is useful when implementing unification plugins
+*/
+class unifier_plugin_cell {
+public:
+    virtual ~unifier_plugin_cell() {}
+    virtual lazy_list<constraints> solve(type_checker &, constraint const &, name_generator const &) const = 0;
+    virtual bool delay_constraint(type_checker &, constraint const &) const = 0;
+};
+
+typedef std::shared_ptr<unifier_plugin_cell> unifier_plugin;
+/** \brief Combine two plugins by appending their solutions. */
+unifier_plugin append(unifier_plugin const & p1, unifier_plugin const & p2);
+/** \brief Combine two plugins by taking the solutions of p1, if it is empty, then return solutions of p2 */
+unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2);
+
+environment set_unifier_plugin(environment const & env, unifier_plugin const & p);
+unifier_plugin const & get_unifier_plugin(environment const & env);
+}