Implement higher-order unification

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

src/frontends/lean/elaborator.cpp

@@ -211,7 +211,7 @@ class elaborator::imp {
                 }
             } else if (has_assigned_metavar(e)) {
                 return check_pi(instantiate(e), ctx, s, s_ctx);
-            } else if (is_metavar(e) && !has_context(e)) {
+            } else if (is_metavar(e) && !has_meta_context(e)) {
                 // e is a unassigned metavariable that must be a Pi,
                 // then we can assign it to (Pi x : A, B x), where
                 // A and B are fresh metavariables
@@ -551,7 +551,7 @@ class elaborator::imp {
     }
 
     void solve_mvar(expr const & m, expr const & t, constraint const & c) {
-        lean_assert(is_metavar(m) && !has_context(m));
+        lean_assert(is_metavar(m) && !has_meta_context(m));
         unsigned midx = metavar_idx(m);
         if (m_metavars[midx].m_assignment) {
             m_constraints.push_back(constraint(m_metavars[midx].m_assignment, t, c));
@@ -577,7 +577,7 @@ class elaborator::imp {
        \brief Temporary hack until we build the new elaborator.
     */
     bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) {
-        if (!is_metavar(e) || !has_context(e))
+        if (!is_metavar(e) || !has_meta_context(e))
             return false;
         meta_ctx const & ctx = metavar_ctx(e);
         meta_entry const & entry = head(ctx);
@@ -596,7 +596,7 @@ class elaborator::imp {
        \brief Temporary hack until we build the new elaborator.
     */
     bool is_inst(expr const & e, expr & c, unsigned & s, expr & v) {
-        if (!is_metavar(e) || !has_context(e))
+        if (!is_metavar(e) || !has_meta_context(e))
             return false;
         meta_ctx const & ctx = metavar_ctx(e);
         meta_entry const & entry = head(ctx);
@@ -612,7 +612,7 @@ class elaborator::imp {
     }
 
     bool solve_meta(expr const & e, expr const & t, constraint const & c) {
-        lean_assert(has_context(e));
+        lean_assert(has_meta_context(e));
         expr const & m = e;
         unsigned midx  = metavar_idx(m);
         unsigned i, s, n;
@@ -667,10 +667,10 @@ class elaborator::imp {
             if (lhs == rhs || (!has_metavar(lhs) && !has_metavar(rhs))) {
                 // do nothing
                 delayed = 0;
-            } else if (is_metavar(lhs) && !has_context(lhs)) {
+            } else if (is_metavar(lhs) && !has_meta_context(lhs)) {
                 delayed = 0;
                 solve_mvar(lhs, rhs, c);
-            } else if (is_metavar(rhs) && !has_context(rhs)) {
+            } else if (is_metavar(rhs) && !has_meta_context(rhs)) {
                 delayed = 0;
                 solve_mvar(rhs, lhs, c);
             } else if (is_metavar(lhs) || is_metavar(rhs)) {

src/kernel/metavar.cpp

@@ -24,13 +24,17 @@ void metavar_env::inc_timestamp() {
 
 metavar_env::metavar_env():m_timestamp(0) {}
 
-expr metavar_env::mk_metavar(context const & ctx) {
+expr metavar_env::mk_metavar(expr const & type, context const & ctx) {
     inc_timestamp();
     unsigned midx = m_env.size();
-    m_env.push_back(data(ctx));
+    m_env.push_back(data(type, ctx));
     return ::lean::mk_metavar(midx);
 }
 
+expr metavar_env::mk_metavar(context const & ctx) {
+    return mk_metavar(expr(), ctx);
+}
+
 bool metavar_env::contains(unsigned midx) const {
     return midx < m_env.size();
 }
@@ -39,10 +43,23 @@ bool metavar_env::is_assigned(unsigned midx) const {
     return m_env[midx].m_subst;
 }
 
-expr metavar_env::get_subst(unsigned midx) const {
+expr metavar_env::get_subst_core(unsigned midx) const {
     return m_env[midx].m_subst;
 }
 
+expr metavar_env::get_subst(unsigned midx) const {
+    expr r = m_env[midx].m_subst;
+    if (r && has_assigned_metavar(r, *this)) {
+        r = instantiate_metavars(r, *this);
+        expr t      = m_env[midx].m_type;
+        context ctx = m_env[midx].m_ctx;
+        const_cast<metavar_env*>(this)->m_env[midx] = data(r, t, ctx);
+        return r;
+    } else {
+        return r;
+    }
+}
+
 expr metavar_env::get_type(unsigned midx, unification_problems & up) {
     auto p = m_env[midx];
     expr t = p->m_type;
@@ -60,6 +77,10 @@ expr metavar_env::get_type(unsigned midx, unification_problems & up) {
     }
 }
 
+expr metavar_env::get_type(unsigned midx) const {
+    return m_env[midx].m_type;
+}
+
 void metavar_env::assign(unsigned midx, expr const & v) {
     inc_timestamp();
     lean_assert(!is_assigned(midx));
@@ -96,13 +117,7 @@ expr metavar_env::get_subst(expr const & m) const {
 
 expr metavar_env::get_type(expr const & m, unification_problems & up) {
     expr s = get_type(metavar_idx(m), up);
-    lean_assert(is_metavar(s));
+    return instantiate(s, metavar_ctx(m), *this);
-    lean_assert(!metavar_ctx(s));
-    meta_ctx const & ctx = metavar_ctx(m);
-    if (ctx)
-        return ::lean::mk_metavar(metavar_idx(s), ctx);
-    else
-        return s;
 }
 
 void metavar_env::assign(expr const & m, expr const & t) {
@@ -166,15 +181,34 @@ expr add_inst(expr const & m, unsigned s, expr const & v) {
     return mk_metavar(metavar_idx(m), add_inst(metavar_ctx(m), s, v));
 }
 
-bool has_context(expr const & m) {
+bool has_meta_context(expr const & m) {
     return metavar_ctx(m);
 }
 
-expr pop_context(expr const & m) {
+expr pop_meta_context(expr const & m) {
-    lean_assert(has_context(m));
+    lean_assert(has_meta_context(m));
     return mk_metavar(metavar_idx(m), tail(metavar_ctx(m)));
 }
 
+struct found_assigned {};
+bool has_assigned_metavar(expr const & e, metavar_env const & menv) {
+    if (!has_metavar(e)) {
+        return false;
+    } else {
+        auto proc = [&](expr const & n, unsigned offset) {
+            if (is_metavar(n) && menv.contains(n) && menv.is_assigned(n))
+                throw found_assigned();
+        };
+        for_each_fn<decltype(proc)> visitor(proc);
+        try {
+            visitor(e);
+            return false;
+        } catch (found_assigned&) {
+            return true;
+        }
+    }
+}
+
 /**
    \brief Auxiliary exception used to sign that a metavariable was
    found in an expression.

src/kernel/metavar.h

@@ -46,7 +46,7 @@ class metavar_env {
         expr    m_subst;
         expr    m_type;
         context m_ctx;
-        data(context const & ctx):m_ctx(ctx) {}
+        data(expr const & t, context const & ctx):m_type(t), m_ctx(ctx) {}
         data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {}
     };
     pvector<data> m_env;
@@ -61,11 +61,21 @@ public:
     */
     unsigned get_timestamp() const { return m_timestamp; }
 
+    /**
+       \brief Return the number of metavariables in this metavar_env.
+    */
+    unsigned size() const { return m_env.size(); }
+
     /**
        \brief Create new metavariable in this environment.
     */
     expr mk_metavar(context const & ctx = context());
 
+    /**
+       \brief Create a new metavariable with the given type and context.
+    */
+    expr mk_metavar(expr const & type, context const & ctx = context());
+
     /**
        \brief Return true if this environment contains a metavariable
        with id \c midx. That is, it has an entry of the form
@@ -91,6 +101,8 @@ public:
     */
     expr get_subst(unsigned midx) const;
 
+    expr get_subst_core(unsigned midx) const;
+
     /**
        \brief Return the type of the metavariable with id \c midx in this environment.
 
@@ -103,6 +115,12 @@ public:
     */
     expr get_type(unsigned midx, unification_problems & up);
 
+    /**
+       \brief Return type of the metavariable with id \c midx in this environment.
+       If the metavariable is not associated with any type, then return the null expression.
+    */
+    expr get_type(unsigned midx) const;
+
     /**
        \brief Assign the metavariable with id \c midx to the term \c t.
 
@@ -192,19 +210,27 @@ meta_ctx add_inst(meta_ctx const & ctx, unsigned s, expr const & v);
 
    \pre is_metavar(m)
 */
-bool has_context(expr const & m);
+bool has_meta_context(expr const & m);
 
 /**
    \brief Return the same metavariable, but the head of the context is removed.
 
    \pre is_metavar(m)
-   \pre has_context(m)
+   \pre has_meta_context(m)
 */
-expr pop_context(expr const & m);
+expr pop_meta_context(expr const & m);
+
+/**
+   \brief Return true iff \c e has a metavariable that is assigned in menv.
+*/
+bool has_assigned_metavar(expr const & e, metavar_env const & menv);
 
 /**
    \brief Return true iff \c e contains the metavariable with index \c midx.
    The substitutions in \c menv are taken into account.
 */
 bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv = metavar_env());
+inline bool has_metavar(expr const & e, expr const & m, metavar_env const & menv = metavar_env()) {
+    return has_metavar(e, metavar_idx(m), menv);
+}
 }

src/kernel/type_checker.cpp

@@ -50,7 +50,7 @@ class type_checker::imp {
             expr A = m_menv->mk_metavar(ctx);
             expr B = m_menv->mk_metavar(ctx);
             expr p = mk_pi(g_x_name, A, B(Var(0)));
-            if (has_context(r)) {
+            if (has_meta_context(r)) {
                 // r contains lift/inst operations, so we put the constraint in m_up
                 m_up->add_eq(ctx, r, p);
             } else {
@@ -75,7 +75,7 @@ class type_checker::imp {
             // A better solution is consists in creating a fresh universe level k and
             // associate the constraint that u == Type k.
             // Later the constraint must be solved in the elaborator.
-            if (has_context(u))
+            if (has_meta_context(u))
                 m_up->add_eq(ctx, u, Type());
             else
                 m_menv->assign(u, Type());
@@ -252,6 +252,8 @@ public:
     void clear() {
         m_cache.clear();
         m_normalizer.clear();
+        m_menv           = nullptr;
+        m_menv_timestamp = 0;
     }
 
     normalizer & get_normalizer() {

src/library/ho_unifier.cpp

@@ -4,39 +4,462 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
+#include "util/pvector.h"
+#include "util/pdeque.h"
+#include "util/exception.h"
 #include "kernel/environment.h"
+#include "kernel/free_vars.h"
+#include "kernel/instantiate.h"
+#include "kernel/normalizer.h"
+#include "library/light_checker.h"
+#include "library/reduce.h"
+#include "library/update_expr.h"
 #include "library/ho_unifier.h"
+#include "library/printer.h"
 
 namespace lean {
+static name g_x_name("x");
 class ho_unifier::imp {
+    typedef std::tuple<context, expr, expr> constraint;
+    typedef pdeque<constraint>              cqueue; // constraint queue
+    struct state {
+        unsigned    m_id;
+        metavar_env m_subst;
+        cqueue      m_queue;
+        state(unsigned id, metavar_env const & menv, cqueue const & q):
+            m_id(id), m_subst(menv), m_queue(q) {}
+    };
+    typedef std::vector<state>              state_stack;
+
     environment    m_env;
+    normalizer     m_normalizer;
+    light_checker  m_type_infer;
+    state_stack    m_state_stack;
+    unsigned       m_delayed;
+    unsigned       m_next_state_id;
+    bool           m_ho; // true if used higher-order
     volatile bool  m_interrupted;
 
+    static metavar_env & subst_of(state & s) { return s.m_subst; }
+    static cqueue & queue_of(state & s) { return s.m_queue; }
+
+    state mk_state(metavar_env const & s, cqueue const & q) {
+        unsigned id = m_next_state_id;
+        m_next_state_id++;
+        return state(id, s, q);
+    }
+
+    void reset_delayed() {
+        m_delayed = 0;
+    }
+
+    /**
+       \brief Add a constraint to the state in the top of the state_stack
+    */
+    void add_constraint(context const & ctx, expr const & l, expr const & r) {
+        lean_assert(!m_state_stack.empty());
+        state & s = m_state_stack.back();
+        queue_of(s).push_front(constraint(ctx, l, r));
+        reset_delayed();
+    }
+
+    /**
+       \brief Add a constraint to the state in the top of the state_stack,
+       but put the constraint in the end of the queue, and increase the m_delayed counter.
+    */
+    void postpone_constraint(context const & ctx, expr const & l, expr const & r) {
+        lean_assert(!m_state_stack.empty());
+        state & s = m_state_stack.back();
+        queue_of(s).push_back(constraint(ctx, l, r));
+        m_delayed++;
+    }
+
+    void init(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) {
+        m_next_state_id = 0;
+        m_ho = false;
+        m_state_stack.clear();
+        m_state_stack.push_back(mk_state(menv, cqueue()));
+        add_constraint(ctx, l, r);
+    }
+
+    metavar_env cleanup_subst(metavar_env const & s, unsigned num_input_metavars) {
+        // eliminate auxiliary metavariables
+        if (!m_ho) {
+            return s;
+        } else {
+            metavar_env new_s;
+            for (unsigned i = 0; i < num_input_metavars; i++) {
+                new_s.mk_metavar(s.get_type(i), s.get_context(i));
+                expr subst = s.get_subst(i);
+                if (subst)
+                    new_s.assign(i, subst);
+            }
+            return new_s;
+        }
+    }
+
+    list<result> save_result(list<result> const & r, metavar_env const & s, residue const & rs, unsigned num_input_metavars) {
+        return cons(result(cleanup_subst(s, num_input_metavars), rs), r);
+    }
+
+    /**
+       Process <tt>a == b</tt> when:
+       1- \c a is an assigned metavariable
+       2- \c a is a unassigned metavariable without a metavariable context.
+       3- \c a is a unassigned metavariable of the form <tt>?m[lift:s:n, ...]</tt>, and \c b does not have
+          a free variable in the range <tt>[s, s+n)</tt>.
+       4- \c a is an application of the form <tt>(?m ...)</tt> where ?m is an assigned metavariable.
+    */
+    enum status { Solved, Failed, Continue };
+    status process_metavar(expr & a, expr & b, metavar_env & s) {
+        if (is_metavar(a)) {
+            if (s.is_assigned(a)) {
+                // Case 1
+                a = s.get_subst(a);
+            } else if (!has_meta_context(a)) {
+                // Case 2
+                if (has_metavar(b, a, s)) {
+                    return Failed;
+                } else {
+                    s.assign(a, b);
+                    reset_delayed();
+                    return Solved;
+                }
+            } else {
+                meta_entry const & me = head(metavar_ctx(a));
+                if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) {
+                    // Case 3
+                    b = lower_free_vars(b, me.s() + me.n(), me.n());
+                    a = pop_meta_context(a);
+                }
+            }
+        }
+
+        if (is_app(a) && is_metavar(arg(a, 0)) && s.is_assigned(arg(a, 0))) {
+            // Case 4
+            a = update_app(a, 0, s.get_subst(arg(a, 0)));
+        }
+        return Continue;
+    }
+
+    /** \brief Unfold let-expression */
+    void process_let(expr & a) {
+        if (is_let(a))
+            a = instantiate(let_body(a), let_value(a));
+    }
+
+    /** \brief Unfold constants */
+    void process_constant(expr & a) {
+        if (is_constant(a)) {
+            object const & obj = m_env.find_object(const_name(a));
+            if (obj && obj.is_definition() && !obj.is_opaque())
+                a = obj.get_value();
+        }
+    }
+
+    /** \brief Replace variables by their definition if the context contains it. */
+    void process_var(context const & ctx, expr & a) {
+        if (is_var(a)) {
+            try {
+                context_entry const & e = lookup(ctx, var_idx(a));
+                if (e.get_body())
+                    a = e.get_body();
+            } catch (exception&) {
+            }
+        }
+    }
+
+    /** \brief Applies simple unfolding steps */
+    void process_simple(context const & ctx, expr & a) {
+        process_let(a);
+        process_constant(a);
+        process_var(ctx, a);
+    }
+
+    /** \brief Process the application's function using \c process_simple */
+    void process_app_function(context const & ctx, expr & a) {
+        if (is_app(a)) {
+            expr f = arg(a, 0);
+            process_simple(ctx, f);
+            a = update_app(a, 0, f);
+        }
+    }
+
+    /** \brief Creates a subproblem based on the application arguments */
+    bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) {
+        lean_assert(is_app(a) && is_app(b));
+        if (num_args(a) != num_args(b)) {
+            return false;
+        } else {
+            for (unsigned i = 1; i < num_args(a); i++) {
+                add_constraint(ctx, arg(a, i), arg(b, i));
+            }
+            return true;
+        }
+    }
+
+    /**
+       Process a constraint <tt>ctx |- a = b</tt>, where \c a and \c b
+       are applications and the function is the same.
+       That is, <tt>arg(a, 0) == arg(b, 0)</tt>
+
+       \pre is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0)
+    */
+    bool process_easy_app(context const & ctx, expr const & a, expr const & b) {
+        lean_assert(is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0));
+        return process_app_args(ctx, a, b, 1);
+    }
+
+    /** \brief Return true if \c a is of the form <tt>(?m ...)</tt> */
+    bool is_meta_app(expr const & a) {
+        return is_app(a) && is_metavar(arg(a, 0));
+    }
+
+    /**
+       Auxiliary class for invoking m_type_infer.
+       If it creates a new unfication problem we mark m_failed to true.
+       add_eq can be easily supported, but we need to extend ho_unifier API to be able
+       to support add_type_of_eq and add_is_convertible.
+       The m_type_infer only invokes add_type_of_eq when it needs to ask for the type
+       of a metavariable that does not have a type yet.
+       One possible workaround it o make sure that every metavariable has an associated type
+       before invoking ho_unifier.
+    */
+    class unification_problems_wrapper : public unification_problems {
+        bool m_failed;
+    public:
+        unification_problems_wrapper():m_failed(false) {}
+        virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_failed = true; }
+        virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_failed = true; }
+        virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_failed = true; }
+        bool failed() const { return m_failed; }
+    };
+
+    /**
+       \brief Process a constraint <tt>ctx |- a = b</tt> where \c a is of the form <tt>(?m ...)</tt>.
+       We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching
+       for further details.
+    */
+    bool process_meta_app(context const & ctx, expr const & a, expr const & b) {
+        lean_assert(is_meta_app(a));
+        lean_assert(!is_meta_app(b));
+        m_ho = true; // using higher-order matching
+        expr f_a          = arg(a, 0);
+        lean_assert(is_metavar(f_a));
+        state top_state   = m_state_stack.back();
+        cqueue q          = queue_of(top_state);
+        metavar_env s     = subst_of(top_state);
+        unsigned midx     = metavar_idx(f_a);
+        unsigned num_a    = num_args(a);
+        unification_problems_wrapper upw;
+        buffer<expr> arg_types;
+        for (unsigned i = 1; i < num_a; i++) {
+            arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &upw));
+        }
+        // clear the cache since we don't want a reference to s inside of m_type_infer
+        m_type_infer.clear();
+        if (upw.failed())
+            return false;
+        m_state_stack.pop_back();
+        // add projections
+        for (unsigned i = 1; i < num_a; i++) {
+            expr proj = mk_var(i - 1);
+            for (unsigned j = 1; j < num_a; j++)
+                proj = mk_lambda(name(g_x_name, j), arg_types[j - 1], proj);
+            cqueue new_q = q;
+            new_q.push_front(constraint(ctx, arg(a, i), b));
+            metavar_env new_s = s;
+            new_s.assign(midx, proj);
+            m_state_stack.push_back(mk_state(new_s, new_q));
+        }
+        // add imitation
+        metavar_env new_s = s;
+        cqueue  new_q     = q;
+        if (is_app(b)) {
+            expr f_b          = arg(b, 0);
+            unsigned num_b    = num_args(b);
+            buffer<expr> imitation_args; // arguments for the imitation
+            imitation_args.push_back(f_b);
+            for (unsigned i = 1; i < num_b; i++) {
+                expr h_i = new_s.mk_metavar(ctx);
+                buffer<expr> h_app_var_args;
+                buffer<expr> h_app_subst_args;
+                h_app_var_args.push_back(h_i);
+                h_app_subst_args.push_back(h_i);
+                for (unsigned j = 1; j < num_a; j++) {
+                    h_app_var_args.push_back(mk_var(num_a - j - 1));
+                    h_app_subst_args.push_back(arg(a, j));
+                }
+                imitation_args.push_back(mk_app(h_app_var_args.size(), h_app_var_args.data()));
+                new_q.push_front(constraint(ctx, mk_app(h_app_subst_args.size(), h_app_subst_args.data()), arg(b, i)));
+            }
+            expr imitation = mk_app(imitation_args.size(), imitation_args.data());
+            for (unsigned j = 1; j < num_a; j++)
+                imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation);
+            new_s.assign(midx, imitation);
+            m_state_stack.push_back(mk_state(new_s, new_q));
+        } else {
+            // TODO(Leo) handle eq like we handle applications
+            // make f_a the constant function
+            expr imitation = lift_free_vars(b, 0, num_a - 1);
+            for (unsigned j = 1; j < num_a; j++)
+                imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation);
+            new_s.assign(midx, imitation);
+            m_state_stack.push_back(mk_state(new_s, new_q));
+        }
+        reset_delayed();
+        return true;
+    }
+
+    /**
+       \brief Process the constraint \c c. Return true if the constraint was processed or postponed, and false
+       if it failed to solve the constraint.
+    */
+    bool process(constraint const & c, metavar_env & s) {
+        context ctx = std::get<0>(c);
+        expr const & old_a = std::get<1>(c);
+        expr const & old_b = std::get<2>(c);
+        expr a = old_a;
+        expr b = old_b;
+        if (a == b) {
+            reset_delayed();
+            return true;
+        }
+        if (is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0))
+            return process_easy_app(ctx, a, b);
+        status r;
+        r = process_metavar(a, b, s);
+        if (r != Continue) { return r == Solved; }
+        r = process_metavar(b, a, s);
+        if (r != Continue) { return r == Solved; }
+        process_simple(ctx, a);
+        process_simple(ctx, b);
+        process_app_function(ctx, a);
+        process_app_function(ctx, b);
+        if ((is_app(a) && !is_eqp(a, old_a)) || (is_app(b) && !is_eqp(b, old_b))) {
+            // some progress was made
+            add_constraint(ctx, a, b);
+            return true;
+        }
+        a = head_beta_reduce(a);
+        b = head_beta_reduce(b);
+        if ((is_metavar(a) && has_meta_context(a)) ||
+            (is_metavar(b) && has_meta_context(b))) {
+            // a or b is a metavariable that has a metavariable context associated with it.
+            // postpone
+            postpone_constraint(ctx, a, b);
+            return true;
+        }
+        if (!is_app(a) && !is_app(b)) {
+            if (a.kind() != b.kind())
+                return false;
+            switch (a.kind()) {
+            case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: case expr_kind::Type:
+                return false;
+            case expr_kind::Eq:
+                add_constraint(ctx, eq_lhs(a), eq_lhs(b));
+                add_constraint(ctx, eq_rhs(a), eq_rhs(b));
+                return true;
+            case expr_kind::Lambda: case expr_kind::Pi:
+                add_constraint(ctx, abst_domain(a), abst_domain(b));
+                add_constraint(extend(ctx, abst_name(a), abst_domain(a)), abst_body(a), abst_body(b));
+                return true;
+            case expr_kind::Let: case expr_kind::MetaVar: case expr_kind::App:
+                lean_unreachable();
+                return false;
+            }
+        }
+
+        if (is_meta_app(a)) {
+            if (is_meta_app(b)) {
+                postpone_constraint(ctx, a, b);
+                return true;
+            } else {
+                return process_meta_app(ctx, a, b);
+                return true;
+            }
+        } else if (is_meta_app(b)) {
+            lean_assert(!is_meta_app(b));
+            return process_meta_app(ctx, b, a);
+        }
+
+        if (!is_eqp(a, old_a) || !is_eqp(b, old_b)) {
+            // some progress was made
+            add_constraint(ctx, a, b);
+            return true;
+        }
+
+        expr norm_a = m_normalizer(a, ctx, &s);
+        expr norm_b = m_normalizer(b, ctx, &s);
+        if (norm_a.kind() != norm_b.kind())
+            return false;
+        if (is_app(norm_a)) {
+            return process_app_args(ctx, norm_a, norm_b, 0);
+        } else if (a == norm_a && b == norm_b) {
+            return false;
+        } else {
+            // some progress was made
+            add_constraint(ctx, norm_a, norm_b);
+            return true;
+        }
+    }
+
 public:
-    imp(environment const & env):m_env(env) {
+    imp(environment const & env):m_env(env), m_normalizer(env), m_type_infer(env) {
         m_interrupted = false;
-        // TODO(Leo)
+        m_delayed     = 0;
     }
 
-    bool unify(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up) {
+    list<result> unify(context const & ctx, expr const & a, expr const & b, metavar_env const & menv) {
-        // TODO(Leo)
+        unsigned num_metavars = menv.size();
-        return false;
+        init(ctx, a, b, menv);
-    }
+        list<result> r;
-
+        while (!m_state_stack.empty()) {
-    void clear() {
+            check_interrupted(m_interrupted);
-        // TODO(Leo)
+            state & top_state = m_state_stack.back();
+            cqueue & cq       = queue_of(top_state);
+            unsigned cq_size  = cq.size();
+            if (cq.empty()) {
+                // no constraints left to be solved
+                r = save_result(r, subst_of(top_state), residue(), num_metavars);
+                m_state_stack.pop_back();
+            } else {
+                // try cq_sz times to find a constraint that can be processed
+                constraint c = cq.front();
+                // std::cout << "solving (" << top_state.m_id << ") " << std::get<1>(c) << " === " << std::get<2>(c) << "\n";
+                cq.pop_front();
+                if (!process(c, subst_of(top_state))) {
+                    // state can't be solved
+                    reset_delayed();
+                    m_state_stack.pop_back();
+                }
+                if (m_delayed > cq_size) {
+                    // None of the constraints could be processed.
+                    // So, we save the remaining constraints as a residue
+                    residue rs;
+                    for (auto c : cq)
+                        rs = cons(c, rs);
+                    r = save_result(r, subst_of(top_state), rs, num_metavars);
+                    reset_delayed();
+                    m_state_stack.pop_back();
+                }
+            }
+        }
+        return r;
     }
 
     void set_interrupt(bool flag) {
         m_interrupted = flag;
+        m_normalizer.set_interrupt(flag);
+        m_type_infer.set_interrupt(flag);
     }
 };
 
 ho_unifier::ho_unifier(environment const & env):m_ptr(new imp(env)) {}
 ho_unifier::~ho_unifier() {}
-void ho_unifier::clear() { m_ptr->clear(); }
 void ho_unifier::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
-bool ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up) {
+list<ho_unifier::result> ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv) {
-    return m_ptr->unify(ctx, l, r, menv, up);
+    return m_ptr->unify(ctx, l, r, menv);
 }
 }

src/library/ho_unifier.h

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
+#include <utility>
+#include "util/list.h"
 #include "kernel/metavar.h"
 
 namespace lean {
@@ -17,24 +19,21 @@ public:
     ho_unifier(environment const & env);
     ~ho_unifier();
 
+    typedef list<std::tuple<context, expr, expr>> residue;
+    typedef std::pair<metavar_env, residue> result;
+
     /**
-        \brief Try to unify \c l and \c r in the context \c ctx using the substitution \c menv.
+        \brief Try to unify \c l and \c r in the context \c ctx using the input substitution \c menv.
         By unification, we mean we have to find an assignment for the unassigned metavariables in
         \c l and \c r s.t. \c l and \c r become definitionally equal.
-        The unifier may produce a residue: a set of unification problems that could not be solved,
+        The unifier may produce a residue: a set of unification problems
-        and were postponed. This set of problems is stored in \c up. The caller should try to instantiate
+        that could not be solved, and were postponed. The unifier postpones unification problems of the form
-        the metavariables in the residue using other constraints, and then try to continue the unification.
+        <tt>(?M1 ...) == (?M2 ...)</tt> where \c M1 and \c M2 are unassigned metavariables.
-        Return true if the unification succeeded (modulo residue), and false if the terms can't be unified.
+        The result is a list of pairs: substitution (in the form of \c metavar_env) and residue.
-
+        Each pair is a possible solution. The resultant \c metavar_env may contain new metavariables.
-        @param[in] ctx The context for \c l and \c r
+        The empty list represents failure.
-        @param[in] l   Expression to be unified with \c r
-        @param[in] r   Expression to be unified with \c l
-        @param[in,out] menv  Metavariable substitution. \c menv may already contain some instantiated variables when this method is invoked.
-        @param[out]    up Delayed unification problems (aka residue), that could not be solved by the unifier.
     */
-    bool operator()(context const & ctx, expr const & l, expr const & r, metavar_env & menv, unification_problems & up);
+    list<result> operator()(context const & ctx, expr const & l, expr const & r, metavar_env const & menv);
-
-    void clear();
 
     void set_interrupt(bool flag);
     void interrupt() { set_interrupt(true); }

src/library/light_checker.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/flet.h"
 #include "util/scoped_map.h"
 #include "kernel/environment.h"
 #include "kernel/normalizer.h"
@@ -11,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
+#include "kernel/metavar.h"
 #include "library/reduce.h"
 #include "library/light_checker.h"
 
@@ -18,10 +20,13 @@ namespace lean {
 class light_checker::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
 
-    environment    m_env;
+    environment            m_env;
-    cache          m_cache;
+    metavar_env *          m_menv;
-    normalizer     m_normalizer;
+    unsigned               m_menv_timestamp;
-    volatile bool  m_interrupted;
+    unification_problems * m_up;
+    normalizer             m_normalizer;
+    cache                  m_cache;
+    volatile bool          m_interrupted;
 
     level infer_universe(expr const & t, context const & ctx) {
         expr u = m_normalizer(infer_type(t, ctx), ctx);
@@ -53,21 +58,29 @@ class light_checker::imp {
             return instantiate(t, num_args(e)-1, &arg(e, 1));
     }
 
-public:
+    void set_menv(metavar_env * menv) {
-    imp(environment const & env):
+        if (m_menv == menv) {
-        m_env(env),
+            // Check whether m_menv has been updated since the last time the normalizer has been invoked
-        m_normalizer(env) {
+            if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
-        m_interrupted = false;
+                m_menv_timestamp = m_menv->get_timestamp();
+                m_cache.clear();
+            }
+        } else {
+            m_menv = menv;
+            m_cache.clear();
+            m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
+        }
     }
 
     expr infer_type(expr const & e, context const & ctx) {
         // cheap cases, we do not cache results
         switch (e.kind()) {
         case expr_kind::MetaVar:
-            // TODO(Leo) The following code should be unreachable in the current implementation.
+            if (m_menv && m_up) {
-            // It will be needed when we implement the new elaborator.
+                return m_menv->get_type(e, *m_up);
-            lean_unreachable();
+            } else {
-            return e;
+                throw kernel_exception(m_env, "unexpected metavariable occurrence");
+            }
         case expr_kind::Constant: {
             object const & obj = m_env.get_object(const_name(e));
             if (obj.has_type())
@@ -152,6 +165,22 @@ public:
         return r;
     }
 
+public:
+    imp(environment const & env):
+        m_env(env),
+        m_normalizer(env) {
+        m_interrupted = false;
+        m_menv           = nullptr;
+        m_menv_timestamp = 0;
+        m_up             = nullptr;
+    }
+
+    expr operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
+        set_menv(menv);
+        flet<unification_problems*> set(m_up, up);
+        return infer_type(e, ctx);
+    }
+
     void set_interrupt(bool flag) {
         m_interrupted = flag;
         m_normalizer.set_interrupt(flag);
@@ -160,11 +189,15 @@ public:
     void clear() {
         m_cache.clear();
         m_normalizer.clear();
+        m_menv = nullptr;
+        m_menv_timestamp = 0;
     }
 };
 light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {}
 light_checker::~light_checker() {}
-expr light_checker::operator()(expr const & e, context const & ctx) { return m_ptr->infer_type(e, ctx); }
+expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, unification_problems * up) {
+    return m_ptr->operator()(e, ctx, menv, up);
+}
 void light_checker::clear() { m_ptr->clear(); }
 void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 }

src/library/light_checker.h

@@ -11,6 +11,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 class environment;
+class metavar_env;
+class unification_problems;
 /**
    \brief Functional object for "quickly" inferring the type of expressions.
    It does not check whether the input expression is type correct or not.
@@ -28,7 +30,7 @@ public:
     light_checker(environment const & env);
     ~light_checker();
 
-    expr operator()(expr const & e, context const & ctx = context());
+    expr operator()(expr const & e, context const & ctx = context(), metavar_env * menv = nullptr, unification_problems * up = nullptr);
 
     void clear();
 

src/library/reduce.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/environment.h"
 #include "kernel/free_vars.h"
+#include "kernel/replace.h"
 #include "library/update_expr.h"
 
 namespace lean {
@@ -43,6 +44,22 @@ expr head_beta_reduce(expr const & t) {
     }
 }
 
+expr beta_reduce(expr t) {
+    auto f = [=](expr const & m, unsigned offset) -> expr {
+        if (is_head_beta(m))
+            return head_beta_reduce(m);
+        else
+            return m;
+    };
+    while (true) {
+        expr new_t = replace_fn<decltype(f)>(f)(t);
+        if (new_t == t)
+            return new_t;
+        else
+            t = new_t;
+    }
+}
+
 expr head_reduce(expr const & t, environment const & e, context const & c, name_set const * defs) {
     if (is_head_beta(t)) {
         return head_beta_reduce(t);

src/library/reduce.h

@@ -12,5 +12,6 @@ Author: Leonardo de Moura
 namespace lean {
 bool is_head_beta(expr const & t);
 expr head_beta_reduce(expr const & t);
+expr beta_reduce(expr t);
 expr head_reduce(expr const & t, environment const & e, context const & c = context(), name_set const * defs = nullptr);
 }

src/tests/kernel/metavar.cpp

@@ -497,6 +497,18 @@ static void tst23() {
     std::cout << up << "\n";
 }
 
+static void tst24() {
+    metavar_env menv;
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar();
+    expr f  = Const("f");
+    expr a  = Const("a");
+    menv.assign(m1, f(m2));
+    menv.assign(m2, a);
+    lean_assert(instantiate_metavars(f(m1), menv) == f(f(a)));
+    std::cout << instantiate_metavars(f(m1), menv) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -521,5 +533,6 @@ int main() {
     tst21();
     tst22();
     tst23();
+    tst24();
     return has_violations() ? 1 : 0;
 }

src/tests/library/CMakeLists.txt

@@ -1,3 +1,6 @@
 add_executable(light_checker light_checker.cpp)
 target_link_libraries(light_checker ${EXTRA_LIBS})
 add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker)
+add_executable(ho_unifier ho_unifier.cpp)
+target_link_libraries(ho_unifier ${EXTRA_LIBS})
+add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier)

src/tests/library/ho_unifier.cpp

@@ -0,0 +1,40 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/environment.h"
+#include "library/ho_unifier.h"
+#include "library/printer.h"
+#include "library/reduce.h"
+using namespace lean;
+
+void tst1() {
+    environment env;
+    metavar_env menv;
+    ho_unifier  unify(env);
+    expr N  = Const("N");
+    env.add_var("N", Type());
+    env.add_var("f", N >> (N >> N));
+    env.add_var("a", N);
+    env.add_var("b", N);
+    expr f  = Const("f");
+    expr x  = Const("x");
+    expr a  = Const("a");
+    expr b  = Const("b");
+    expr m1 = menv.mk_metavar();
+    expr m2 = menv.mk_metavar();
+    expr l = m1(b);
+    expr r = f(b, f(a, b));
+    for (auto sol : unify(context(), l, r, menv)) {
+        std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n";
+        std::cout << "--------------\n";
+    }
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}