/*
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 <utility>
#include <memory>
#include <vector>
#include <limits>
#include <algorithm>
#include "util/interrupt.h"
#include "util/luaref.h"
#include "util/lazy_list_fn.h"
#include "util/sstream.h"
#include "util/lbool.h"
#include "util/flet.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/for_each_fn.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/kernel_exception.h"
#include "kernel/error_msgs.h"
#include "library/normalize.h"
#include "library/occurs.h"
#include "library/locals.h"
#include "library/module.h"
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/unifier_plugin.h"
#include "library/kernel_bindings.h"
#include "library/print.h"
#include "library/expr_lt.h"

#ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS
#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000
#endif

#ifndef LEAN_DEFAULT_UNIFIER_COMPUTATION
#define LEAN_DEFAULT_UNIFIER_COMPUTATION false
#endif

#ifndef LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES
#define LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES false
#endif

#ifndef LEAN_DEFAULT_UNIFIER_CONSERVATIVE
#define LEAN_DEFAULT_UNIFIER_CONSERVATIVE false
#endif

#ifndef LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL
#define LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL true
#endif

namespace lean {
static name * g_unifier_max_steps               = nullptr;
static name * g_unifier_computation             = nullptr;
static name * g_unifier_expensive_classes       = nullptr;
static name * g_unifier_conservative            = nullptr;
static name * g_unifier_nonchronological        = nullptr;

unsigned get_unifier_max_steps(options const & opts) {
    return opts.get_unsigned(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS);
}

bool get_unifier_computation(options const & opts) {
    return opts.get_bool(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION);
}

bool get_unifier_expensive_classes(options const & opts) {
    return opts.get_bool(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES);
}

bool get_unifier_conservative(options const & opts) {
    return opts.get_bool(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE);
}

bool get_unifier_nonchronological(options const & opts) {
    return opts.get_bool(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL);
}

unifier_config::unifier_config(bool use_exceptions, bool discard):
    m_use_exceptions(use_exceptions),
    m_max_steps(LEAN_DEFAULT_UNIFIER_MAX_STEPS),
    m_computation(LEAN_DEFAULT_UNIFIER_COMPUTATION),
    m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES),
    m_discard(discard),
    m_nonchronological(LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL) {
    m_kind    = unifier_kind::Liberal;
    m_pattern = false;
    m_ignore_context_check = false;
}

unifier_config::unifier_config(options const & o, bool use_exceptions, bool discard):
    m_use_exceptions(use_exceptions),
    m_max_steps(get_unifier_max_steps(o)),
    m_computation(get_unifier_computation(o)),
    m_expensive_classes(get_unifier_expensive_classes(o)),
    m_discard(discard),
    m_nonchronological(get_unifier_nonchronological(o)) {
    if (get_unifier_conservative(o))
        m_kind = unifier_kind::Conservative;
    else
        m_kind = unifier_kind::Liberal;
    m_pattern = false;
    m_ignore_context_check = false;
}

// If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where
// l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args.
// Otherwise return none.
optional<expr> is_simple_meta(expr const & e, buffer<expr> & args) {
    expr const & m = get_app_args(e, args);
    if (!is_metavar(m))
        return none_expr();
    for (auto it = args.begin(); it != args.end(); it++) {
        if (!is_local(*it) || contains_local(*it, args.begin(), it))
            return none_expr();
    }
    return some_expr(m);
}

bool is_simple_meta(expr const & e) {
    buffer<expr> args;
    return (bool)is_simple_meta(e, args); // NOLINT
}

// Return true if all local constants in \c e are in locals
bool context_check(expr const & e, buffer<expr> const & locals) {
    bool failed = false;
    for_each(e, [&](expr const & e, unsigned) {
            if (failed)
                return false;
            if (is_local(e)) {
                if (!contains_local(e, locals))
                    failed = true;
                return false; // do not visit type
            }
            if (is_metavar(e))
                return false; // do not visit type
            return has_local(e);
        });
    return !failed;
}

enum class occurs_check_status { Ok, Maybe, FailCircular, FailLocal };

// Return
//   - l_undef if \c e contains a metavariable application that contains
//     a local constant not in locals
//   - l_true if \c e does not contain the metavariable \c m, and all local
//     constants are in \c e are in \c locals.
//   - l_false if \c e contains \c m or it contains a local constant \c l
//     not in locals that is not in a metavariable application.
occurs_check_status occurs_context_check(substitution & s, expr const & e, expr const & m, buffer<expr> const & locals, expr & bad_local) {
    expr root = e;
    occurs_check_status r = occurs_check_status::Ok;
    for_each(e, [&](expr const & e, unsigned) {
            if (r == occurs_check_status::FailLocal || r == occurs_check_status::FailCircular) {
                return false;
            } else if (is_local(e)) {
                if (!contains_local(e, locals)) {
                    // right-hand-side contains variable that is not in the scope
                    // of metavariable.
                    bad_local = e;
                    r = occurs_check_status::FailLocal;
                }
                return false; // do not visit type
            } else if (is_meta(e)) {
                if (r == occurs_check_status::Ok) {
                    if (!context_check(e, locals))
                        r = occurs_check_status::Maybe;
                    if (s.occurs(m, e))
                        r = occurs_check_status::Maybe;
                }
                if (mlocal_name(get_app_fn(e)) == mlocal_name(m))
                    r = occurs_check_status::FailCircular;
                return false; // do not visit children
            } else {
                // we only need to continue exploring e if it contains
                // metavariables and/or local constants.
                return has_expr_metavar(e) || has_local(e);
            }
        });
    if (r != occurs_check_status::Ok)
        return r;
    for (expr const & local : locals) {
        if (s.occurs(m, mlocal_type(local)))
            return occurs_check_status::Maybe;
    }
    return r;
}

occurs_check_status occurs_context_check(substitution & s, expr const & e, expr const & m, buffer<expr> const & locals) {
    expr bad_local;
    return occurs_context_check(s, e, m, locals, bad_local);
}

unify_status unify_simple_core(substitution & s, expr const & lhs, expr const & rhs, justification const & j) {
    lean_assert(is_meta(lhs));
    buffer<expr> args;
    auto m = is_simple_meta(lhs, args);
    if (!m || is_meta(rhs)) {
        return unify_status::Unsupported;
    } else {
        switch (occurs_context_check(s, rhs, *m, args)) {
        case occurs_check_status::FailLocal:
        case occurs_check_status::FailCircular:
            return unify_status::Failed;
        case occurs_check_status::Maybe:
            return unify_status::Unsupported;
        case occurs_check_status::Ok: {
            s.assign(*m, args, rhs, j);
            return unify_status::Solved;
        }}
    }
    lean_unreachable(); // LCOV_EXCL_LINE
}

unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs, justification const & j) {
    if (lhs == rhs)
        return unify_status::Solved;
    else if (!has_metavar(lhs) && !has_metavar(rhs))
        return unify_status::Failed;
    else if (is_meta(lhs))
        return unify_simple_core(s, lhs, rhs, j);
    else if (is_meta(rhs))
        return unify_simple_core(s, rhs, lhs, j);
    else
        return unify_status::Unsupported;
}

// Return true if m occurs in e
bool occurs_meta(level const & m, level const & e) {
    lean_assert(is_meta(m));
    bool contains = false;
    for_each(e, [&](level const & l) {
            if (contains)
                return false;
            if (l == m) {
                contains = true;
                return false;
            }
            return has_meta(l);
        });
    return contains;
}

unify_status unify_simple_core(substitution & s, level const & lhs, level const & rhs, justification const & j) {
    lean_assert(is_meta(lhs));
    bool contains = occurs_meta(lhs, rhs);
    if (contains) {
        if (is_succ(rhs))
            return unify_status::Failed;
        else
            return unify_status::Unsupported;
    }
    s.assign(meta_id(lhs), rhs, j);
    return unify_status::Solved;
}

unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j) {
    if (lhs == rhs)
        return unify_status::Solved;
    else if (!has_meta(lhs) && !has_meta(rhs))
        return unify_status::Failed;
    else if (is_meta(lhs))
        return unify_simple_core(s, lhs, rhs, j);
    else if (is_meta(rhs))
        return unify_simple_core(s, rhs, lhs, j);
    else if (is_succ(lhs) && is_succ(rhs))
        return unify_simple(s, succ_of(lhs), succ_of(rhs), j);
    else
        return unify_status::Unsupported;
}

unify_status unify_simple(substitution & s, constraint const & c) {
    if (is_eq_cnstr(c))
        return unify_simple(s, cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());
    else if (is_level_eq_cnstr(c))
        return unify_simple(s, cnstr_lhs_level(c), cnstr_rhs_level(c), c.get_justification());
    else
        return unify_status::Unsupported;
}

static constraint * g_dont_care_cnstr = nullptr;
static unsigned g_group_size = 1u << 28;
constexpr unsigned g_num_groups = 8;
static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size};
static unsigned get_group_first_index(cnstr_group g) {
    return g_cnstr_group_first_index[static_cast<unsigned>(g)];
}
static cnstr_group to_cnstr_group(unsigned d) {
    if (d >= g_num_groups)
        d = g_num_groups-1;
    return static_cast<cnstr_group>(d);
}

/** \brief Convert choice constraint delay factor to cnstr_group */
cnstr_group get_choice_cnstr_group(constraint const & c) {
    lean_assert(is_choice_cnstr(c));
    unsigned f = cnstr_delay_factor(c);
    if (f > static_cast<unsigned>(cnstr_group::MaxDelayed)) {
        return cnstr_group::MaxDelayed;
    } else {
        return static_cast<cnstr_group>(f);
    }
}

/** \brief Auxiliary functional object for implementing simultaneous higher-order unification */
struct unifier_fn {
    typedef pair<constraint, unsigned> cnstr; // constraint + idx
    struct cnstr_cmp {
        int operator()(cnstr const & c1, cnstr const & c2) const {
            return c1.second < c2.second ? -1 : (c1.second == c2.second ? 0 : 1);
        }
    };
    typedef rb_tree<cnstr, cnstr_cmp> cnstr_set;
    typedef rb_tree<unsigned, unsigned_cmp> cnstr_idx_set;
    typedef name_map<cnstr_idx_set> name_to_cnstrs;
    typedef name_map<unsigned> owned_map;
    typedef rb_map<expr, pair<expr, justification>, expr_quick_cmp> expr_map;
    typedef std::shared_ptr<type_checker> type_checker_ptr;
    environment      m_env;
    name_generator   m_ngen;
    substitution     m_subst;
    constraints      m_postponed; // constraints that will not be solved
    owned_map        m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m
    expr_map         m_type_map;  // auxiliary map for storing the type of the expr in choice constraints
    unifier_plugin   m_plugin;
    type_checker_ptr m_tc[2];
    type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
                                      // only the definitions from the main module are treated as transparent.
    unifier_config   m_config;
    unsigned         m_num_steps;
    bool             m_first; //!< True if we still have to generate the first solution.
    unsigned         m_next_assumption_idx; //!< Next assumption index.
    unsigned         m_next_cidx; //!< Next constraint index.
    /**
       \brief "Queue" of constraints to be solved.

       We implement it using a red-black-tree because:
       1- Our red-black-trees support a O(1) copy operation. So, it is cheap to create a snapshot
       whenever we create a backtracking point.

       2- We can easily remove any constraint from the queue in O(n log n). We do that when
       a metavariable \c m is assigned, and we want to instantiate it in all constraints that
       contains it.
    */
    cnstr_set        m_cnstrs;
    /**
        \brief The following map is an index. The map a metavariable name \c m to the set of constraint indices that contain \c m.
        We use these indices whenever a metavariable \c m is assigned.
        When the metavariable is assigned, we used this index to remove constraints that contains \c m from \c m_cnstrs,
        instantiate \c m, and reprocess them.

        \remark \c m_mvar_occs is for regular metavariables.
    */
    name_to_cnstrs   m_mvar_occs;

    /**
        \brief Base class for the case-splits created by the unifier.

        We have three different kinds of case splits:
        1- unifier plugin
        2- choice constraints
        3- higher-order unification
    */
    struct case_split {
        unsigned         m_assumption_idx; // idx of the current assumption
        justification    m_jst;
        justification    m_failed_justifications; // justifications for failed branches
        // snapshot of unifier's state
        substitution     m_subst;
        constraints      m_postponed;
        cnstr_set        m_cnstrs;
        expr_map         m_type_map;
        name_to_cnstrs   m_mvar_occs;
        owned_map        m_owned_map;

        /** \brief Save unifier's state */
        case_split(unifier_fn & u, justification const & j):
            m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst),
            m_postponed(u.m_postponed), m_cnstrs(u.m_cnstrs), m_type_map(u.m_type_map),
            m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map) {
            u.m_next_assumption_idx++;
        }

        /** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */
        void restore_state(unifier_fn & u) {
            lean_assert(u.in_conflict());
            u.m_subst     = m_subst;
            u.m_postponed = m_postponed;
            u.m_cnstrs    = m_cnstrs;
            u.m_mvar_occs = m_mvar_occs;
            u.m_owned_map = m_owned_map;
            u.m_type_map  = m_type_map;
            m_assumption_idx = u.m_next_assumption_idx;
            m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict);
            u.m_next_assumption_idx++;
            u.m_conflict  = optional<justification>();
        }
        justification get_jst() const { return m_jst; }
        virtual ~case_split() {}
        virtual bool next(unifier_fn & u) = 0;
    };
    typedef std::vector<std::unique_ptr<case_split>> case_split_stack;

    struct lazy_constraints_case_split : public case_split {
        lazy_list<constraints> m_tail;
        lazy_constraints_case_split(unifier_fn & u, justification const & j, lazy_list<constraints> const & tail):
            case_split(u, j), m_tail(tail) {}
        virtual bool next(unifier_fn & u) { return u.next_lazy_constraints_case_split(*this); }
    };

    struct simple_case_split : public case_split {
        list<constraints> m_tail;
        simple_case_split(unifier_fn & u, justification const & j, list<constraints> const & tail):case_split(u, j), m_tail(tail) {}
        virtual bool next(unifier_fn & u) { return u.next_simple_case_split(*this); }
    };

    struct delta_unfold_case_split : public case_split {
        bool       m_done;
        constraint m_cnstr;
        delta_unfold_case_split(unifier_fn & u, justification const & j, constraint const & c):
            case_split(u, j), m_done(false), m_cnstr(c) {}
        virtual bool next(unifier_fn & u) { return u.next_delta_unfold_case_split(*this); }
    };

    case_split_stack        m_case_splits;
    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_config const & cfg):
        m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
        m_config(cfg), m_num_steps(0) {
        switch (m_config.m_kind) {
        case unifier_kind::Cheap:
            m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child());
            m_tc[1] = m_tc[0];
            m_flex_rigid_tc = m_tc[0];
            m_config.m_computation = false;
            break;
        case unifier_kind::VeryConservative:
            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldReducible);
            m_tc[1] = m_tc[0];
            m_flex_rigid_tc = m_tc[0];
            m_config.m_computation = false;
            break;
        case unifier_kind::Conservative:
            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
            m_tc[1] = m_tc[0];
            m_flex_rigid_tc = m_tc[0];
            m_config.m_computation = false;
            break;
        case unifier_kind::Liberal:
            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false);
            m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true);
            if (!cfg.m_computation)
                m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
            break;
        default:
            lean_unreachable();
        }
        m_next_assumption_idx = 0;
        m_next_cidx = 0;
        m_first     = true;
        process_input_constraints(num_cs, cs);
    }

    void process_input_constraints(unsigned num_cs, constraint const * cs) {
        // Input choice constraints may have ownership over a metavariable.
        // So, we must first process them, to make sure the ownership table is initialized before
        // we solve the remaining constraints
        for (unsigned i = 0; i < num_cs; i++) {
            if (cs[i].kind() == constraint_kind::Choice)
                preprocess_choice_constraint(cs[i]);
        }
        for (unsigned i = 0; i < num_cs; i++) {
            if (cs[i].kind() != constraint_kind::Choice)
                process_constraint(cs[i]);
        }
    }

    void check_system() {
        check_interrupted();
        if (m_num_steps > m_config.m_max_steps)
            throw exception(sstream() << "unifier maximum number of steps (" << m_config.m_max_steps << ") exceeded, " <<
                            "the maximum number of steps can be increased by setting the option unifier.max_steps " <<
                            "(remark: the unifier uses higher order unification and unification-hints, " <<
                            "which may trigger non-termination");
        m_num_steps++;
    }

    bool in_conflict() const { return (bool)m_conflict; } // NOLINT
    void set_conflict(justification const & j) { m_conflict = j; }
    void update_conflict(justification const & j) { m_conflict = j; }
    void reset_conflict() { m_conflict = optional<justification>(); lean_assert(!in_conflict()); }

    expr mk_local_for(expr const & b) {
        return mk_local(m_ngen.next(), binding_name(b), binding_domain(b), binding_info(b));
    }

    /**
        \brief Update occurrence index with entry <tt>m -> cidx</tt>, where \c m is the name of a metavariable,
        and \c cidx is the index of a constraint that contains \c m.
    */
    void add_mvar_occ(name const & m, unsigned cidx) {
        cnstr_idx_set s;
        auto it = m_mvar_occs.find(m);
        if (it)
            s = *it;
        if (!s.contains(cidx)) {
            s.insert(cidx);
            m_mvar_occs.insert(m, s);
        }
    }

    void add_meta_occ(expr const & m, unsigned cidx) {
        lean_assert(is_meta(m));
        add_mvar_occ(mlocal_name(get_app_fn(m)), cidx);
    }

    /** \brief For each metavariable m in e add an entry m -> cidx at m_mvar_occs.
        Return true if at least one entry was added.
    */
    bool add_meta_occs(expr const & e, unsigned cidx) {
        bool added = false;
        if (has_expr_metavar(e)) {
            for_each(e, [&](expr const & e, unsigned) {
                    if (is_meta(e)) {
                        add_meta_occ(e, cidx);
                        added = true;
                        return false;
                    }
                    if (is_local(e))
                        return false;
                    return has_expr_metavar(e);
                });
        }
        return added;
    }

    /** \brief Add constraint to the constraint queue */
    unsigned add_cnstr(constraint const & c, cnstr_group g) {
        unsigned cidx = m_next_cidx + get_group_first_index(g);
        m_cnstrs.insert(cnstr(c, cidx));
        m_next_cidx++;
        return cidx;
    }

    /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j

        \remark If relax is true then opaque definitions from the main module are treated as transparent.
    */
    bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
        try {
            auto dcs = m_tc[relax]->is_def_eq(t1, t2, j);
            if (!dcs.first) {
                // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n";
                set_conflict(j);
                return false;
            } else {
                return process_constraints(dcs.second);
            }
        } catch (exception&) {
            set_conflict(j);
            return false;
        }
    }

    /** \brief Process the given constraints. Return true iff no conflict was detected. */
    bool process_constraints(constraint_seq const & cs) {
        return cs.all_of([&](constraint const & c) { return process_constraint(c); });
    }

    bool process_constraints(buffer<constraint> const & cs) {
        for (auto const & c : cs) {
            if (!process_constraint(c))
                return false;
        }
        return true;
    }


    /** \brief Process constraints in \c cs, and append justification \c j to them. */
    bool process_constraints(constraint_seq const & cs, justification const & j) {
        return cs.all_of([&](constraint const & c) {
                return process_constraint(update_justification(c, mk_composite1(c.get_justification(), j)));
            });
    }

    template<typename Constraints>
    bool process_constraints(Constraints const & cs, justification const & j) {
        for (auto const & c : cs) {
            if (!process_constraint(update_justification(c, mk_composite1(c.get_justification(), j))))
                return false;
        }
        return true;
    }

    /** \brief Put \c e in weak head normal form.

        \remark If relax is true then opaque definitions from the main module are treated as transparent.
        \remark Constraints generated in the process are stored in \c cs.
    */
    expr whnf(expr const & e, bool relax, constraint_seq & cs) {
        return m_tc[relax]->whnf(e, cs);
    }

    /** \brief Infer \c e type.

        \remark Return none if an exception was throw when inferring the type.
        \remark If relax is true then opaque definitions from the main module are treated as transparent.
        \remark Constraints generated in the process are stored in \c cs.
    */
    optional<expr> infer(expr const & e, bool relax, constraint_seq & cs) {
        try {
            return some_expr(m_tc[relax]->infer(e, cs));
        } catch (exception &) {
            return none_expr();
        }
    }

    expr whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
        constraint_seq _cs;
        expr r = whnf(e, relax, _cs);
        to_buffer(_cs, j, cs);
        return r;
    }

    expr flex_rigid_whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
        if (m_config.m_computation) {
            return whnf(e, j, relax, cs);
        } else {
            constraint_seq _cs;
            expr r = m_flex_rigid_tc->whnf(e, _cs);
            to_buffer(_cs, j, cs);
            return r;
        }
    }

    justification mk_assign_justification(expr const & m, expr const & m_type, expr const & v_type, justification const & j) {
        auto r = j.get_main_expr();
        if (!r) r = m;
        justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst) {
                substitution s(subst);
                format r;
                expr _m = s.instantiate(m);
                if (is_meta(_m)) {
                    r = format("type error in placeholder assignment");
                } else {
                    r  = format("type error in placeholder assigned to");
                    r += pp_indent_expr(fmt, _m);
                }
                format expected_fmt, given_fmt;
                std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, m_type, v_type);
                r += compose(line(), format("placeholder has type"));
                r += given_fmt;
                r += compose(line(), format("but is expected to have type"));
                r += expected_fmt;
                r += compose(line(), format("the assignment was attempted when trying to solve"));
                r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst)));
                return r;
            });
        return mk_composite1(new_j, j);
    }

    /**
       \brief Given lhs of the form (m args), assign (m args) := rhs with justification j.
       The type of lhs and rhs are inferred, and is_def_eq is invoked.

       Any other constraint that contains \c m is revisited

       \remark If relax is true then opaque definitions from the main module are treated as transparent.
    */
    bool assign(expr const & lhs, expr const & m, buffer<expr> const & args, expr const & rhs, justification const & j, bool relax) {
        lean_assert(is_metavar(m));
        lean_assert(!in_conflict());
        m_subst.assign(m, args, rhs, j);
        constraint_seq cs;
        auto lhs_type = infer(lhs, relax, cs);
        auto rhs_type = infer(rhs, relax, cs);
        if (lhs_type && rhs_type) {
            if (!process_constraints(cs, j))
                return false;
            justification new_j = mk_assign_justification(m, *lhs_type, *rhs_type, j);
            if (!is_def_eq(*lhs_type, *rhs_type, new_j, relax))
                return false;
        } else {
            set_conflict(j);
            return false;
        }
        auto it = m_mvar_occs.find(mlocal_name(m));
        if (it) {
            cnstr_idx_set s = *it;
            m_mvar_occs.erase(mlocal_name(m));
            s.for_each([&](unsigned cidx) {
                    process_constraint_cidx(cidx);
                });
            return !in_conflict();
        } else {
            return true;
        }
    }

    /**
       \brief Assign \c v to universe metavariable \c m with justification \c j.
       Any constraint that contains \c m is revisted.
    */
    bool assign(level const & m, level const & v, justification const & j) {
        lean_assert(is_meta(m));
        m_subst.assign(m, v, j);
        return true;
    }

    justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j,
                                                     expr const & bad_local) {
        justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst) {
                format r = format("invalid local context when tried to assign");
                r += pp_indent_expr(fmt, rhs);
                buffer<expr> locals;
                auto m = get_app_args(lhs, locals);
                r += line() + format("containing '") + fmt(bad_local) + format("', to placeholder '") + fmt(m) + format("'");
                if (locals.empty()) {
                    r += format(", in the empty local context");
                } else {
                    r += format(", in the local context");
                    format aux;
                    bool first = true;
                    for (expr const l : locals) {
                        if (first) first = false; else aux += space();
                        aux += fmt(l);
                    }
                    r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux));
                }
                r += compose(line(), format("the assignment was attempted when trying to solve"));
                r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst)));
                return r;
            });
        return mk_composite1(new_j, j);
    }

    enum status { Solved, Failed, Continue };
    /**
       \brief Process constraints of the form <tt>lhs =?= rhs</tt> where lhs is of the form <tt>?m</tt> or <tt>(?m l_1 .... l_n)</tt>,
       where all \c l_i are distinct local variables. In this case, the method returns Solved, if the method assign succeeds.
       The method returns \c Failed if \c rhs contains <tt>?m</tt>, or it contains a local constant not in <tt>{l_1, ..., l_n}</tt>.
       Otherwise, it returns \c Continue.
    */
    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
        if (!is_meta(lhs))
            return Continue;
        buffer<expr> locals;
        auto m = is_simple_meta(lhs, locals);
        if (!m || is_meta(rhs))
            return Continue;
        expr bad_local;
        occurs_check_status status;
        if (m_config.m_ignore_context_check)
            status = occurs_check_status::Ok;
        else
            status = occurs_context_check(m_subst, rhs, *m, locals, bad_local);
        if (status == occurs_check_status::FailLocal || status == occurs_check_status::FailCircular) {
            // Try to normalize rhs
            // Example:  ?M := f (pr1 (pair 0 ?M))
            constraint_seq cs;
            auto is_target_fn = [&](expr const & e) {
                if (status == occurs_check_status::FailLocal && occurs(bad_local, e))
                    return true;
                else if (status == occurs_check_status::FailCircular && occurs(*m, e))
                    return true;
                return false;
            };
            expr rhs_n = normalize(*m_tc[relax], rhs, is_target_fn, cs);
            if (rhs != rhs_n && process_constraints(cs))
                return process_metavar_eq(lhs, rhs_n, j, relax);
        }
        switch (status) {
        case occurs_check_status::FailLocal:
            set_conflict(mk_invalid_local_ctx_justification(lhs, rhs, j, bad_local));
            return Failed;
        case occurs_check_status::FailCircular:
            set_conflict(j);
            return Failed;
        case occurs_check_status::Maybe:
            return Continue;
        case occurs_check_status::Ok:
            lean_assert(!m_subst.is_assigned(*m));
            if (assign(lhs, *m, locals, rhs, j, relax)) {
                return Solved;
            } else {
                return Failed;
            }
        }
        lean_unreachable(); // LCOV_EXCL_LINE
    }

    optional<declaration> is_delta(expr const & e) {
        bool relax_opaque = true;
        return m_tc[relax_opaque]->is_delta(e);
    }

    /** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */
    bool is_eq_deltas(expr const & lhs, expr const & rhs) {
        auto lhs_d = is_delta(lhs);
        auto rhs_d = is_delta(rhs);
        return lhs_d && rhs_d && is_eqp(*lhs_d, *rhs_d);
    }

    /** \brief Return true if the constraint is of the form (f ...) =?= (f ...), where f can be expanded. */
    bool is_delta_cnstr(constraint const & c) {
        return is_eq_cnstr(c) && is_eq_deltas(cnstr_lhs_expr(c), cnstr_rhs_expr(c));
    }

    pair<constraint, bool> instantiate_metavars(constraint const & c) {
        if (is_eq_cnstr(c)) {
            auto lhs_jst = m_subst.instantiate_metavars(cnstr_lhs_expr(c));
            auto rhs_jst = m_subst.instantiate_metavars(cnstr_rhs_expr(c));
            expr lhs = lhs_jst.first;
            expr rhs = rhs_jst.first;
            if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
                return mk_pair(mk_eq_cnstr(lhs, rhs,
                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
                                           relax_main_opaque(c)),
                               true);
            }
        } else if (is_level_eq_cnstr(c)) {
            auto lhs_jst = m_subst.instantiate_metavars(cnstr_lhs_level(c));
            auto rhs_jst = m_subst.instantiate_metavars(cnstr_rhs_level(c));
            level lhs = lhs_jst.first;
            level rhs = rhs_jst.first;
            if (lhs != cnstr_lhs_level(c) || rhs != cnstr_rhs_level(c)) {
                return mk_pair(mk_level_eq_cnstr(lhs, rhs,
                                                 mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)),
                               true);
            }
        }
        return mk_pair(c, false);
    }

    status process_eq_constraint_core(constraint const & c) {
        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        justification const & jst = c.get_justification();
        bool relax = relax_main_opaque(c);

        if (lhs == rhs)
            return Solved; // trivial constraint

        // Update justification using the justification of the instantiated metavariables
        if (!has_metavar(lhs) && !has_metavar(rhs)) {
            return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
        }

        // Handle higher-order pattern matching.
        status st = process_metavar_eq(lhs, rhs, jst, relax);
        if (st != Continue) return st;
        st = process_metavar_eq(rhs, lhs, jst, relax);
        if (st != Continue) return st;

        return Continue;
    }

    expr instantiate_meta(expr e, justification & j) {
        while (true) {
            if (auto p = m_subst.expand_metavar_app(e)) {
                e = p->first;
                j = mk_composite1(j, p->second);
            } else {
                return e;
            }
        }
    }

    expr instantiate_meta_args(expr const & e, justification & j) {
        if (!is_app(e))
            return e;
        buffer<expr> args;
        bool modified = false;
        expr const & f = get_app_rev_args(e, args);
        unsigned i = args.size();
        while (i > 0) {
            --i;
            expr new_arg = instantiate_meta(args[i], j);
            if (new_arg != args[i]) {
                modified = true;
                args[i]  = new_arg;
            }
        }
        if (!modified)
            return e;
        return mk_rev_app(f, args.size(), args.data());
    }

    status instantiate_eq_cnstr(constraint const & c) {
        justification j = c.get_justification();
        expr lhs = instantiate_meta(cnstr_lhs_expr(c), j);
        expr rhs = instantiate_meta(cnstr_rhs_expr(c), j);
        if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
        lhs = instantiate_meta_args(lhs, j);
        rhs = instantiate_meta_args(rhs, j);
        if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
        return Continue;
    }

    /** \brief Return a delay factor if e is of the form (?m ...) and ?m is a metavariable owned by
        a choice constraint. The delay factor is the delay of the choice constraint.
        Return none otherwise. */
    optional<unsigned> is_owned(expr const & e) {
        expr const & m = get_app_fn(e);
        if (!is_metavar(m))
            return optional<unsigned>();
        if (auto it = m_owned_map.find(mlocal_name(m)))
            return optional<unsigned>(*it);
        else
            return optional<unsigned>();
    }

    /** \brief Applies previous method to the left and right hand sides of the equality constraint */
    optional<unsigned> is_owned(constraint const & c) {
        if (auto d = is_owned(cnstr_lhs_expr(c)))
            return d;
        else
            return is_owned(cnstr_rhs_expr(c));
    }

    /** \brief Process an equality constraints. */
    bool process_eq_constraint(constraint const & c) {
        lean_assert(is_eq_cnstr(c));
        // instantiate assigned metavariables
        status st = instantiate_eq_cnstr(c);
        if (st != Continue) return st == Solved;

        if (auto d = is_owned(c)) {
            // Metavariable in the constraint is owned by choice constraint.
            // So, we postpone this constraint.
            add_cnstr(c, to_cnstr_group(*d+1));
            return true;
        }

        st = process_eq_constraint_core(c);
        if (st != Continue) return st == Solved;

        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        bool relax = relax_main_opaque(c);

        if (is_eq_deltas(lhs, rhs)) {
            // we need to create a backtracking point for this one
            add_cnstr(c, cnstr_group::Basic);
        } else if (is_meta(lhs) && is_meta(rhs)) {
            // flex-flex constraints are delayed the most.
            unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
            add_meta_occ(lhs, cidx);
            add_meta_occ(rhs, cidx);
        } else if (m_tc[relax]->may_reduce_later(lhs) ||
                   m_tc[relax]->may_reduce_later(rhs) ||
                   m_plugin->delay_constraint(*m_tc[relax], c)) {
            unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
            add_meta_occs(lhs, cidx);
            add_meta_occs(rhs, cidx);
        } else if (is_meta(lhs)) {
            // flex-rigid constraints are delayed.
            unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid);
            add_meta_occ(lhs, cidx);
        } else if (is_meta(rhs)) {
            // flex-rigid constraints are delayed.
            unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid);
            add_meta_occ(rhs, cidx);
        } else {
            // this constraints require the unifier plugin to be solved
            add_cnstr(c, cnstr_group::Basic);
        }
        return true;
    }

    /**
       \brief Process a universe level constraints of the form <tt>?m =?= rhs</tt>. It fails if rhs contains \c ?m and
       is definitely bigger than \c ?m.

       TODO(Leo): we should improve this method in the future. It is doing only very basic things.
    */
    status process_metavar_eq(level const & lhs, level const & rhs, justification const & j) {
        if (!is_meta(lhs))
            return Continue;
        bool contains = occurs_meta(lhs, rhs);
        if (contains) {
            if (is_succ(rhs)) {
                set_conflict(j);
                return Failed;
            } else {
                return Continue;
            }
        }
        lean_assert(!m_subst.is_assigned(lhs));
        if (assign(lhs, rhs, j)) {
            return Solved;
        } else {
            set_conflict(j);
            return Failed;
        }
    }

    /** \brief Process a universe level contraints. */
    bool process_level_eq_constraint(constraint const & c) {
        lean_assert(is_level_eq_cnstr(c));
        // instantiate assigned metavariables
        constraint new_c = instantiate_metavars(c).first;
        level lhs = cnstr_lhs_level(new_c);
        level rhs = cnstr_rhs_level(new_c);
        justification jst = new_c.get_justification();

        // normalize lhs and rhs
        lhs = normalize(lhs);
        rhs = normalize(rhs);
        // eliminate outermost succs
        while (is_succ(lhs) && is_succ(rhs)) {
            lhs = succ_of(lhs);
            rhs = succ_of(rhs);
        }

        if (lhs == rhs)
            return true; // trivial constraint

        if (!has_meta(lhs) && !has_meta(rhs)) {
            set_conflict(jst);
            return false; // trivial failure
        }

        status st = process_metavar_eq(lhs, rhs, jst);
        if (st != Continue) return st == Solved;
        st = process_metavar_eq(rhs, lhs, jst);
        if (st != Continue) return st == Solved;

        if (lhs != cnstr_lhs_level(new_c) || rhs != cnstr_rhs_level(new_c))
            new_c = mk_level_eq_cnstr(lhs, rhs, new_c.get_justification());

        add_cnstr(new_c, cnstr_group::FlexRigid);
        return true;
    }

    bool preprocess_choice_constraint(constraint c) {
        if (!cnstr_on_demand(c)) {
            if (cnstr_is_owner(c)) {
                expr m = get_app_fn(cnstr_expr(c));
                lean_assert(is_metavar(m));
                m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c));
            }
            add_cnstr(c, get_choice_cnstr_group(c));
            return true;
        } else {
            expr m = cnstr_expr(c);
            // choice constraints that are marked as "on demand"
            // are only processed when all metavariables in the
            // type of m have been instantiated.
            expr type;
            justification jst;
            if (auto it = m_type_map.find(m)) {
                // Type of m is already cached in m_type_map
                type = it->first;
                jst  = it->second;
            } else {
                // Type of m is not cached yet, we
                // should infer it, process generated
                // constraints and save the result in
                // m_type_map.
                bool relax = relax_main_opaque(c);
                constraint_seq cs;
                optional<expr> t = infer(m, relax, cs);
                if (!t) {
                    set_conflict(c.get_justification());
                    return false;
                }
                if (!process_constraints(cs, c.get_justification()))
                    return false;
                type = *t;
                m_type_map.insert(m, mk_pair(type, justification()));
            }
            // Try to instantiate metavariables in type
            pair<expr, justification> type_jst = m_subst.instantiate_metavars(type);
            if (type_jst.first != type) {
                // Type was modified by instantiation,
                // we update the constraint justification,
                // and store the new type in m_type_map
                jst  = mk_composite1(jst, type_jst.second);
                type = type_jst.first;
                c    = update_justification(c, mk_composite1(c.get_justification(), jst));
                m_type_map.insert(m, mk_pair(type, jst));
            }
            unsigned cidx = add_cnstr(c, cnstr_group::ClassInstance);
            if (!add_meta_occs(type, cidx)) {
                // type does not contain metavariables...
                // so this "on demand" constraint is ready to be solved
                m_cnstrs.erase(cnstr(c, cidx));
                add_cnstr(c, cnstr_group::Basic);
                m_type_map.erase(m);
            }
            return true;
        }
    }

    /**
        \brief Process the given constraint \c c. "Easy" constraints are solved, and the remaining ones
        are added to the constraint queue m_cnstrs. By "easy", see the methods
        #process_eq_constraint and #process_level_eq_constraint.
    */
    bool process_constraint(constraint const & c) {
        if (in_conflict())
            return false;
        check_system();
        // std::cout << "process: " << c << "\n";
        switch (c.kind()) {
        case constraint_kind::Choice:
            return preprocess_choice_constraint(c);
        case constraint_kind::Eq:
            return process_eq_constraint(c);
        case constraint_kind::LevelEq:
            return process_level_eq_constraint(c);
        }
        lean_unreachable(); // LCOV_EXCL_LINE
    }

    /**
       \brief Process constraint with index \c cidx. The constraint is removed
       from the constraint queue, and the method #process_constraint is invoked.
    */
    bool process_constraint_cidx(unsigned cidx) {
        if (in_conflict())
            return false;
        cnstr c(*g_dont_care_cnstr, cidx);
        if (auto it = m_cnstrs.find(c)) {
            constraint c2 = it->first;
            m_cnstrs.erase(c);
            return process_constraint(c2);
        }
        return true;
    }

    void add_case_split(std::unique_ptr<case_split> && cs) {
        m_case_splits.push_back(std::move(cs));
    }

    // This method is used only for debugging purposes.
    void display(std::ostream & out, justification const & j, unsigned indent = 0) {
        for (unsigned i = 0; i < indent; i++)
            out << " ";
        out << j.pp(mk_print_formatter_factory()(m_env, options()), nullptr, m_subst) << "\n";
        if (j.is_composite()) {
            display(out, composite_child1(j), indent+2);
            display(out, composite_child2(j), indent+2);
        }
    }

    void pop_case_split() {
        m_case_splits.pop_back();
    }

    bool resolve_conflict() {
        lean_assert(in_conflict());
        while (!m_case_splits.empty()) {
            justification conflict = *m_conflict;
            std::unique_ptr<case_split> & d = m_case_splits.back();
            if (!m_config.m_nonchronological || depends_on(conflict, d->m_assumption_idx)) {
                d->m_failed_justifications = mk_composite1(d->m_failed_justifications, conflict);
                if (d->next(*this)) {
                    reset_conflict();
                    return true;
                }
            } else {
                pop_case_split();
            }
        }
        return false;
    }

    bool next_lazy_constraints_case_split(lazy_constraints_case_split & cs) {
        auto r = cs.m_tail.pull();
        if (r) {
            cs.restore_state(*this);
            lean_assert(!in_conflict());
            cs.m_tail = r->second;
            return process_constraints(r->first, mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx)));
        } else {
            // update conflict
            update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
            pop_case_split();
            return false;
        }
    }

    bool process_lazy_constraints(lazy_list<constraints> const & l, justification const & j) {
        auto r = l.pull();
        if (r) {
            if (r->second.is_nil()) {
                // there is only one alternative
                return process_constraints(r->first, j);
            } else {
                justification a = mk_assumption_justification(m_next_assumption_idx);
                add_case_split(std::unique_ptr<case_split>(new lazy_constraints_case_split(*this, j, r->second)));
                return process_constraints(r->first, mk_composite1(j, a));
            }
        } else {
            set_conflict(j);
            return false;
        }
    }

    /** \brief Given a constraint of the form
            f a_1 ... a_n =?= f b_1 ... b_n
        Return singleton stream with the possible solution
             a_i =?= b_i
        If c is not of the expected form, then return the empty stream.
    */
    lazy_list<constraints> process_const_const_cnstr(constraint const & c) {
        if (!is_eq_cnstr(c))
            return lazy_list<constraints>();
        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        expr const & f_lhs = get_app_fn(lhs);
        expr const & f_rhs = get_app_fn(rhs);
        if (!is_constant(f_lhs) || !is_constant(f_rhs) || const_name(f_lhs) != const_name(f_rhs))
            return lazy_list<constraints>();
        justification const & j = c.get_justification();
        constraint_seq cs;
        bool relax = relax_main_opaque(c);
        auto fcs = m_tc[relax]->is_def_eq(f_lhs, f_rhs, j);
        if (!fcs.first)
            return lazy_list<constraints>();
        cs = fcs.second;
        buffer<expr> args_lhs, args_rhs;
        get_app_args(lhs, args_lhs);
        get_app_args(rhs, args_rhs);
        if (args_lhs.size() != args_rhs.size())
            return lazy_list<constraints>();
        for (unsigned i = 0; i < args_lhs.size(); i++) {
            auto acs = m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j);
            if (!acs.first)
                return lazy_list<constraints>();
            cs = acs.second + cs;
        }
        return lazy_list<constraints>(cs.to_list());
    }

    bool process_plugin_constraint(constraint const & c) {
        bool relax = relax_main_opaque(c);
        lean_assert(!is_choice_cnstr(c));
        lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
        alts = append(alts, process_const_const_cnstr(c));
        return process_lazy_constraints(alts, c.get_justification());
    }

    bool process_choice_constraint(constraint const & c) {
        lean_assert(is_choice_cnstr(c));
        expr const &   m            = cnstr_expr(c);
        choice_fn const & fn        = cnstr_choice_fn(c);
        if (cnstr_is_owner(c)) {
            // choice will have a chance to assign m, so
            // we remove the "barrier" that was preventing m from being assigned.
            m_owned_map.erase(mlocal_name(get_app_fn(m)));
        }
        expr m_type;
        bool relax = relax_main_opaque(c);

        constraint_seq cs;
        if (auto type = infer(m, relax, cs)) {
            m_type = *type;
            if (!process_constraints(cs))
                return false;
        } else {
            set_conflict(c.get_justification());
            return false;
        }
        auto m_type_jst             = m_subst.instantiate_metavars(m_type);
        lazy_list<constraints> alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child());
        return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second));
    }

    bool next_simple_case_split(simple_case_split & cs) {
        if (!is_nil(cs.m_tail)) {
            cs.restore_state(*this);
            lean_assert(!in_conflict());
            constraints c = head(cs.m_tail);
            cs.m_tail     = tail(cs.m_tail);
            return process_constraints(c, mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx)));
        } else {
            // update conflict
            update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
            pop_case_split();
            return false;
        }
    }

    bool unfold_delta(constraint const & c, justification const & extra_j) {
        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        buffer<expr> lhs_args, rhs_args;
        justification j = c.get_justification();
        expr lhs_fn     = get_app_rev_args(lhs, lhs_args);
        expr rhs_fn     = get_app_rev_args(rhs, rhs_args);
        declaration d   = *m_env.find(const_name(lhs_fn));
        levels lhs_lvls = const_levels(lhs_fn);
        levels rhs_lvls = const_levels(lhs_fn);
        bool relax = relax_main_opaque(c);
        expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn));
        expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn));
        expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
        expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
        auto dcs = m_tc[relax]->is_def_eq(t, s, j);
        if (dcs.first) {
            constraints cnstrs = dcs.second.to_list();
            return process_constraints(cnstrs, extra_j);
        } else {
            set_conflict(j);
            return false;
        }
    }

    bool next_delta_unfold_case_split(delta_unfold_case_split & cs) {
        if (!cs.m_done) {
            cs.restore_state(*this);
            cs.m_done = true;
            constraint const & c = cs.m_cnstr;
            justification j      = mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx));
            return unfold_delta(c, j);
        } else {
            // update conflict
            update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications));
            pop_case_split();
            return false;
        }
    }

    /**
        \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded.
        We consider two possible solutions:
        1)   a_1 =?= b_1, ..., a_n =?= b_n
        2)   t =?= s, where t and s are the terms we get after expanding f
    */
    bool process_delta(constraint const & c) {
        lean_assert(is_delta_cnstr(c));
        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        buffer<expr> lhs_args, rhs_args;
        justification j = c.get_justification();
        expr lhs_fn     = get_app_rev_args(lhs, lhs_args);
        expr rhs_fn     = get_app_rev_args(rhs, rhs_args);
        declaration d   = *m_env.find(const_name(lhs_fn));
        levels lhs_lvls = const_levels(lhs_fn);
        levels rhs_lvls = const_levels(lhs_fn);
        if (length(lhs_lvls) != length(rhs_lvls) ||
            d.get_num_univ_params() != length(lhs_lvls)) {
            // the constraint is not well-formed, this can happen when users are abusing the API
            set_conflict(j);
            return false;
        }

        if (lhs_args.size() != rhs_args.size())
            return unfold_delta(c, justification());

        justification a;
        bool relax = relax_main_opaque(c);
        if (m_config.m_kind == unifier_kind::Liberal &&
            (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))) {
            // add case_split for t =?= s
            a = mk_assumption_justification(m_next_assumption_idx);
            add_case_split(std::unique_ptr<case_split>(new delta_unfold_case_split(*this, j, c)));
        }

        // process first case
        justification new_j = mk_composite1(j, a);
        while (!is_nil(lhs_lvls)) {
            level lhs = head(lhs_lvls);
            level rhs = head(rhs_lvls);
            if (!process_constraint(mk_level_eq_cnstr(lhs, rhs, new_j)))
                return false;
            lhs_lvls = tail(lhs_lvls);
            rhs_lvls = tail(rhs_lvls);
        }

        unsigned i = lhs_args.size();
        while (i > 0) {
            --i;
            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
                return false;
        }
        return true;
    }

    /** \brief Return true iff \c c is a flex-rigid constraint. */
    static bool is_flex_rigid(constraint const & c) {
        if (!is_eq_cnstr(c))
            return false;
        bool is_lhs_meta = is_meta(cnstr_lhs_expr(c));
        bool is_rhs_meta = is_meta(cnstr_rhs_expr(c));
        return is_lhs_meta != is_rhs_meta;
    }

    /** \brief Return true iff \c c is a flex-flex constraint */
    static bool is_flex_flex(constraint const & c) {
        return is_eq_cnstr(c) && is_meta(cnstr_lhs_expr(c)) && is_meta(cnstr_rhs_expr(c));
    }

    /** \brief Append the auxiliary constraints \c aux to each alternative in \c alts */
    void append_auxiliary_constraints(buffer<constraints> & alts, list<constraint> const & aux) {
        if (is_nil(aux))
            return;
        for (constraints & cs : alts)
            cs = append(aux, cs);
    }

    /** \brief Auxiliary functional object for implementing process_flex_rigid_core */
    class flex_rigid_core_fn {
        unifier_fn &          u;
        expr const &          lhs;
        buffer<expr>          margs;
        expr const &          m;
        expr const &          rhs;
        justification         j;
        bool                  relax;
        buffer<constraints> & alts; // result: alternatives
        bool                  imitation_only; // if true, then only imitation step is used

        optional<bool>        _has_meta_args;

        bool cheap() const { return u.m_config.m_kind == unifier_kind::Cheap; }
        bool pattern() const { return u.m_config.m_pattern; }

        type_checker & tc() {
            return *u.m_tc[relax];
        }

        type_checker & restricted_tc() {
            if (u.m_config.m_computation)
                return *u.m_tc[relax];
            else
                return *u.m_flex_rigid_tc;
        }

        /** \brief Return true if margs contains an expression \c e s.t. is_meta(e) */
        bool has_meta_args() {
            if (!_has_meta_args) {
                _has_meta_args = std::any_of(margs.begin(), margs.end(),
                                              [](expr const & e) { return is_meta(e); });
            }
            return *_has_meta_args;
        }

        /**
           \brief Given t
           <tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
           return
           <tt>fun (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), v[x_1, ... x_n]</tt>

           \remark v has free variables.
        */
        expr mk_lambda_for(unsigned i, expr const & t, expr const & v) {
            if (i < margs.size()) {
                return mk_lambda(binding_name(t), binding_domain(t), mk_lambda_for(i+1, binding_body(t), v), binding_info(t));
            } else {
                return v;
            }
        }

        expr mk_lambda_for(expr const & t, expr const & v) {
            return mk_lambda_for(0, t, v);
        }

        /** \brief Return true if \c local occurs once in the buffer \c es. */
        bool local_occurs_once(expr const & local, buffer<expr> const & es) {
            bool found = false;
            for (expr const & e : es) {
                if (is_local(e) && mlocal_name(e) == mlocal_name(local)) {
                    if (found)
                        return false;
                    found = true;
                }
            }
            return true;
        }

        /** \see ensure_sufficient_args */
        expr ensure_sufficient_args_core(expr mtype, unsigned i, constraint_seq & cs) {
            if (i == margs.size())
                return mtype;
            mtype = tc().ensure_pi(mtype, cs);
            expr local = u.mk_local_for(mtype);
            expr body  = instantiate(binding_body(mtype), local);
            return Pi(local, ensure_sufficient_args_core(body, i+1, cs));
        }

        /** \brief Make sure mtype is a Pi of size at least margs.size().
            If it is not, we use ensure_pi and (potentially) add new constaints to enforce it.
        */
        expr ensure_sufficient_args(expr const & mtype, constraint_seq & cs) {
            expr t = mtype;
            unsigned num = 0;
            while (is_pi(t)) {
                num++;
                t = binding_body(t);
            }
            if (num >= margs.size())
                return mtype;
            return ensure_sufficient_args_core(mtype, 0, cs);
        }

        /**
           \brief Given
                 m      := a metavariable ?m
                 rhs    := sort, constant
           Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint
                 ?m  =?= fun (x1 ... x_k), rhs
        */
        void mk_simple_imitation() {
            lean_assert(is_metavar(m));
            lean_assert(is_sort(rhs) || is_constant(rhs));
            expr const & mtype = mlocal_type(m);
            constraint_seq cs;
            expr new_mtype = ensure_sufficient_args(mtype, cs);
            cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j, relax);
            alts.push_back(cs.to_list());
        }

        bool restricted_is_def_eq(expr const & marg, expr const & rhs, justification const & j, constraint_seq & cs) {
            try {
                if (restricted_tc().is_def_eq(marg, rhs, j, cs)) {
                    return true;
                } else {
                    return false;
                }
            } catch (exception & ex) {
                return false;
            }
        }

        /**
           Given,
               m      := a metavariable ?m
               margs  := [a_1 ... a_k]
           We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple nonlocal i-th projection" when

           1) rhs is not a local constant
           2) is_def_eq(a_i, rhs) does not fail

           In this case, we add
                a_i =?= rhs
                ?m  =?= fun x_1 ... x_k, x_i
           to alts as a possible solution.
        */
        void mk_simple_nonlocal_projection(unsigned i) {
            expr const & mtype = mlocal_type(m);
            unsigned vidx = margs.size() - i - 1;
            expr const & marg = margs[i];
            constraint_seq cs;
            auto new_mtype = ensure_sufficient_args(mtype, cs);
            // Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
            // The unifier assumes the eq constraints are reduced.
            if (tc().is_def_eq_types(marg, rhs, j, cs) &&
                restricted_is_def_eq(marg, rhs, j, cs)) {
                expr v = mk_lambda_for(new_mtype, mk_var(vidx));
                cs = cs + mk_eq_cnstr(m, v, j, relax);
                alts.push_back(cs.to_list());
            }
        }

        /**
           Given,
              m      := a metavariable ?m
              margs  := [a_1 ... a_k]
           We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple projections" when

           If (rhs and a_i are *not* local constants) OR (rhs is a local constant and a_i is a metavariable application),
           then we add the constraints
                a_i =?= rhs
                ?m  =?= fun x_1 ... x_k, x_i
                to alts as a possible solution.

           If rhs is a local constant and a_i == rhs, then we add the constraint
                ?m =?= fun x_1 ... x_k, x_i
           to alts as a possible solution when a_i is the same local constant or a metavariable application
        */
        void mk_simple_projections() {
            lean_assert(is_metavar(m));
            lean_assert(!is_meta(rhs));
            expr const & mtype = mlocal_type(m);
            unsigned i = margs.size();
            while (i > 0) {
                unsigned vidx = margs.size() - i;
                --i;
                expr const & marg = margs[i];
                if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) {
                    // if rhs is not local, then we only add projections for the nonlocal arguments of lhs
                    mk_simple_nonlocal_projection(i);
                    if (cheap())
                        return;
                } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
                    // if the argument is local, and rhs is equal to it, then we also add a projection
                    constraint_seq cs;
                    auto new_mtype = ensure_sufficient_args(mtype, cs);
                    expr v = mk_lambda_for(new_mtype, mk_var(vidx));
                    cs = cs + mk_eq_cnstr(m, v, j, relax);
                    alts.push_back(cs.to_list());
                    if (cheap())
                        return;
                }
            }
        }

        void mk_app_projections() {
            lean_assert(is_metavar(m));
            lean_assert(is_app(rhs));
            if (!pattern() && !cheap()) {
                expr const & f = get_app_fn(rhs);
                lean_assert(is_constant(f) || is_local(f));
                if (is_local(f)) {
                    unsigned i = margs.size();
                    while (i > 0) {
                        --i;
                        if (!(is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f)))
                            mk_simple_nonlocal_projection(i);
                    }
                } else {
                    mk_simple_projections();
                }
            }
        }

        /** \brief Create the local context \c locals for the imitation step.
         */
        void mk_local_context(buffer<expr> & locals, constraint_seq & cs) {
            expr mtype     = mlocal_type(m);
            unsigned nargs = margs.size();
            mtype = ensure_sufficient_args(mtype, cs);
            expr it = mtype;
            for (unsigned i = 0; i < nargs; i++) {
                expr d     = instantiate_rev(binding_domain(it), locals.size(), locals.data());
                auto d_jst = u.m_subst.instantiate_metavars(d);
                d = d_jst.first;
                j = mk_composite1(j, d_jst.second);
                name n;
                if (is_local(margs[i]) && local_occurs_once(margs[i], margs)) {
                    n = mlocal_name(margs[i]);
                } else {
                    n = u.m_ngen.next();
                }
                expr local = mk_local(n, binding_name(it), d, binding_info(it));
                locals.push_back(local);
                it = binding_body(it);
            }
        }

        expr mk_imitation_arg(expr const & arg, expr const & type, buffer<expr> const & locals,
                               constraint_seq & cs) {
            // The following optimization is broken. It does not really work when we have dependent
            // types. The problem is that the type of arg may depend on other arguments,
            // and constraints are not generated to enforce it.
            //
            //  Here is a minimal counterexample
            //     ?M A B a b H B b  =?=  heq.type_eq A B a b H
            //  with this optimization the imitation is
            //
            //    ?M := fun (A B a b H B' b'), heq.type_eq A (?M1 A B a b H B' b') a (?M2 A B a b H B' b') H
            //
            //  This imitation is only correct if
            //     typeof(H) is (heq A a (?M1 A B a b H B' b') (?M2 A B a b H B' b'))
            //
            //  Adding an extra constraint is problematic since typeof(H) may contain local constants,
            //  and these local constants may have been "renamed" by mk_local_context above
            //
            //  For now, we simply comment the optimization.
            //

            // Broken optimization
            // if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) {
            //    return arg;
            // }

            // The following code is not affected by the problem above because we
            // attach the type \c type to the new metavariables being created.

            // std::cout << "type: " << type << "\n";
            if (context_check(type, locals)) {
                expr maux    = mk_metavar(u.m_ngen.next(), Pi(locals, type));
                // std::cout << "  >> " << maux << " : " << mlocal_type(maux) << "\n";
                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
                return mk_app(maux, locals);
            } else {
                expr maux_type   = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
                expr maux        = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
                return mk_app(maux, locals);
            }
        }

        void mk_app_imitation_core(expr const & f, buffer<expr> const & locals, constraint_seq & cs) {
            buffer<expr> rargs;
            get_app_args(rhs, rargs);
            buffer<expr> sargs;
            try {
                expr f_type = tc().infer(f, cs);
                for (expr const & rarg : rargs) {
                    f_type      = tc().ensure_pi(f_type, cs);
                    expr d_type = binding_domain(f_type);
                    expr sarg   = mk_imitation_arg(rarg, d_type, locals, cs);
                    sargs.push_back(sarg);
                    f_type      = instantiate(binding_body(f_type), sarg);
                }
            } catch (exception&) {}
            expr v = Fun(locals, mk_app(f, sargs));
            cs += mk_eq_cnstr(m, v, j, relax);
            alts.push_back(cs.to_list());
        }

        /**
           \brief Given
               m      := a metavariable ?m
               margs  := [a_1 ... a_k]
               rhs    := (f b_1 ... b_n)
           Then create the constraints
               (?m_1 a_1 ... a_k) =?= b_1
               ...
               (?m_n a_1 ... a_k) =?= b_n
               ?m  =?= fun (x_1 ... x_k), g (?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k)

           If f is a constant, then g is f.
           If f is a local constant, then we consider each a_i that is equal to f.

           Remark: we try to minimize the number of constraints (?m_i a_1 ... a_k) =?= b_i by detecting "easy" cases
           that can be solved immediately. See \c mk_imitation_arg
        */
        void mk_app_imitation() {
            lean_assert(is_metavar(m));
            lean_assert(is_app(rhs));
            buffer<expr> locals;
            constraint_seq cs;
            flet<justification> let(j, j); // save j value
            mk_local_context(locals, cs);
            lean_assert(margs.size() == locals.size());
            expr const & f = get_app_fn(rhs);
            lean_assert(is_constant(f) || is_local(f));
            if (is_local(f)) {
                unsigned i = margs.size();
                while (i > 0) {
                    --i;
                    if (is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f)) {
                        constraint_seq new_cs = cs;
                        mk_app_imitation_core(locals[i], locals, new_cs);
                    }
                }
            } else {
                mk_app_imitation_core(f, locals, cs);
            }
        }

        /**
           \brief Given
               m      := a metavariable ?m
               margs  := [a_1 ... a_k]
               rhs    := (fun/Pi (y : A), B y)
           Then create the constraints
              (?m_1 a_1 ... a_k)   =?= A
              (?m_2 a_1 ... a_k l) =?= B l
              ?m   =?= fun (x_1 ... x_k), fun/Pi (y : ?m_1 x_1 ... x_k), ?m_2 x_1 ... x_k y
           where l is a fresh local constant.
        */
        void mk_bindings_imitation() {
            lean_assert(is_metavar(m));
            lean_assert(is_binding(rhs));
            constraint_seq cs;
            buffer<expr> locals;
            flet<justification> let(j, j); // save j value
            mk_local_context(locals, cs);
            lean_assert(margs.size() == locals.size());
            try {
                // create a scope to make sure no constraints "leak" into the current state
                expr rhs_A     = binding_domain(rhs);
                expr A_type    = tc().infer(rhs_A, cs);
                expr A         = mk_imitation_arg(rhs_A, A_type, locals, cs);
                expr local     = mk_local(u.m_ngen.next(), binding_name(rhs), A, binding_info(rhs));
                locals.push_back(local);
                margs.push_back(local);
                expr rhs_B     = instantiate(binding_body(rhs), local);
                expr B_type    = tc().infer(rhs_B, cs);
                expr B         = mk_imitation_arg(rhs_B, B_type, locals, cs);
                expr binding   = is_pi(rhs) ? Pi(local, B) : Fun(local, B);
                locals.pop_back();
                expr v         = Fun(locals, binding);
                cs += mk_eq_cnstr(m, v, j, relax);
                alts.push_back(cs.to_list());
            } catch (exception&) {}
            margs.pop_back();
        }

    public:
        flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs,
                           justification const & _j, bool _relax, buffer<constraints> & _alts,
                           bool _imitation_only):
            u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), relax(_relax), alts(_alts),
            imitation_only(_imitation_only) {}

        void operator()() {
            switch (rhs.kind()) {
            case expr_kind::Var: case expr_kind::Meta:
                lean_unreachable(); // LCOV_EXCL_LINE
            case expr_kind::Local:
                mk_simple_projections();
                break;
            case expr_kind::Sort: case expr_kind::Constant:
                if (!pattern() && !cheap() && !imitation_only)
                    mk_simple_projections();
                mk_simple_imitation();
                break;
            case expr_kind::Pi: case expr_kind::Lambda:
                if (!pattern() && !cheap() && !imitation_only)
                    mk_simple_projections();
                mk_bindings_imitation();
                break;
            case expr_kind::Macro:
                lean_unreachable(); // LCOV_EXCL_LINE
            case expr_kind::App:
                if (!imitation_only)
                    mk_app_projections();
                mk_app_imitation();
                break;
            }
        }
    };

    void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j, bool relax,
                                 buffer<constraints> & alts, bool imitation_only) {
        flex_rigid_core_fn(*this, lhs, rhs, j, relax, alts, imitation_only)();
    }

    /** \brief When lhs is an application (f ...), make sure that if any argument that is reducible to a
        local constant is replaced with a local constant.

        \remark We store auxiliary constraints created in the reductions in \c aux. We return the new
        "reduce" application.
    */
    expr expose_local_args(expr const & lhs, justification const & j, bool relax, buffer<constraint> & aux) {
        buffer<expr> margs;
        expr m        = get_app_args(lhs, margs);
        bool modified = false;
        for (expr & marg : margs) {
            // Make sure that if marg is reducible to a local constant, then it is replaced with it.
            if (!is_local(marg)) {
                expr new_marg = whnf(marg, j, relax, aux);
                if (is_local(new_marg)) {
                    marg     = new_marg;
                    modified = true;
                }
            }
        }
        return modified ? mk_app(m, margs) : lhs;
    }

    optional<expr> expand_rhs(expr const & rhs, bool relax) {
        buffer<expr> args;
        expr const & f = get_app_rev_args(rhs, args);
        lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f));
        if (is_lambda(f)) {
            return some_expr(apply_beta(f, args.size(), args.data()));
        } else if (is_macro(f)) {
            if (optional<expr> new_f = m_tc[relax]->expand_macro(f))
                return some_expr(mk_rev_app(*new_f, args.size(), args.data()));
        }
        return none_expr();
    }

    /** \brief When solving flex-rigid constraints lhs =?= rhs (lhs is of the form ?M a_1 ... a_n),
        we consider an additional case-split where rhs is put in weak-head-normal-form when

        1- Option unifier.computation is true
        2- At least one a_i is not a local constant
        3- rhs contains a local constant that is not equal to any a_i.
    */
    bool use_flex_rigid_whnf_split(expr const & lhs, expr const & rhs) {
        lean_assert(is_meta(lhs));
        if (m_config.m_kind != unifier_kind::Liberal)
            return false;
        if (m_config.m_computation)
            return true; // if unifier.computation is true, we always consider the additional whnf split
        buffer<expr> locals;
        expr const * it = &lhs;
        while (is_app(*it)) {
            expr const & arg = app_arg(*it);
            if (!is_local(arg))
                return true; // lhs contains non-local constant
            locals.push_back(arg);
            it = &(app_fn(*it));
        }
        if (!context_check(rhs, locals))
            return true; // rhs contains local constant that is not in locals
        return false;
    }

    /** \brief Process a flex rigid constraint */
    bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) {
        lean_assert(is_meta(lhs));
        lean_assert(!is_meta(rhs));
        if (is_app(rhs)) {
            expr const & f = get_app_fn(rhs);
            if (!is_local(f) && !is_constant(f)) {
                if (auto new_rhs = expand_rhs(rhs, relax)) {
                    lean_assert(*new_rhs != rhs);
                    return is_def_eq(lhs, *new_rhs, j, relax);
                } else {
                    return false;
                }
            }
        } else if (is_macro(rhs)) {
            if (auto new_rhs = expand_rhs(rhs, relax)) {
                lean_assert(*new_rhs != rhs);
                return is_def_eq(lhs, *new_rhs, j, relax);
            } else {
                return false;
            }
        }

        buffer<constraint> aux;
        lhs = expose_local_args(lhs, j, relax, aux);
        buffer<constraints> alts;
        process_flex_rigid_core(lhs, rhs, j, relax, alts, false);
        append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end()));
        if (use_flex_rigid_whnf_split(lhs, rhs)) {
            expr rhs_whnf = flex_rigid_whnf(rhs, j, relax, aux);
            if (rhs_whnf != rhs) {
                if (is_meta(rhs_whnf)) {
                    // it become a flex-flex constraint
                    alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j, relax)));
                } else {
                    buffer<constraints> alts2;
                    process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2, true);
                    append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end()));
                    alts.append(alts2);
                }
            }
        }

        // std::cout << "FlexRigid\n";
        // for (auto cs : alts) {
        //     std::cout << " alternative\n";
        //     for (auto c : cs) {
        //         std::cout << "   >> " << c << "\n";
        //     }
        // }

        if (alts.empty()) {
            set_conflict(j);
            return false;
        } else if (alts.size() == 1) {
            // we don't need to create a backtracking point
            return process_constraints(alts[0], justification());
        } else {
            justification a = mk_assumption_justification(m_next_assumption_idx);
            add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(alts.begin() + 1, alts.end()))));
            return process_constraints(alts[0], a);
        }
    }

    /** \brief Process a flex rigid constraint */
    bool process_flex_rigid(constraint const & c) {
        lean_assert(is_flex_rigid(c));
        expr lhs   = cnstr_lhs_expr(c);
        expr rhs   = cnstr_rhs_expr(c);
        bool relax = relax_main_opaque(c);
        if (is_meta(lhs))
            return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
        else
            return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
    }

    void postpone(constraint const & c) {
        m_postponed = cons(c, m_postponed);
    }

    void discard(constraint const & c) {
        if (!m_config.m_discard)
            postpone(c);
    }

    bool process_flex_flex(constraint const & c) {
        expr const & lhs = cnstr_lhs_expr(c);
        expr const & rhs = cnstr_rhs_expr(c);
        // We ignore almost all flex-flex constraints.
        // We just handle flex_flex "first-order" case
        //   ?M_1 l_1 ... l_k =?= ?M_2 l_1 ... l_k
        //   ?M_1 l_1 ... l_k =?= ?M_2 l_1 ... l_k ... l_n
        //   ?M_1 l_1 ... l_k ... l_n =?= ?M_2 l_1 ... l_k
        if (!is_simple_meta(lhs) || !is_simple_meta(rhs)) {
            discard(c);
            return true;
        }
        buffer<expr> lhs_args, rhs_args;
        expr ml = get_app_args(lhs, lhs_args);
        expr mr = get_app_args(rhs, rhs_args);
        if (mlocal_name(ml) == mlocal_name(mr)) {
            discard(c);
            return true;
        }
        unsigned min_sz = std::min(lhs_args.size(), rhs_args.size());
        lean_assert(!m_subst.is_assigned(ml));
        lean_assert(!m_subst.is_assigned(mr));
        unsigned i = 0;
        for (; i < min_sz; i++)
            if (mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i]))
                break;
        if (i == min_sz) {
            if (lhs_args.size() >= rhs_args.size()) {
                return assign(lhs, ml, lhs_args, rhs, c.get_justification(), relax_main_opaque(c));
            } else {
                return assign(rhs, mr, rhs_args, lhs, c.get_justification(), relax_main_opaque(c));
            }
        } else {
            discard(c);
            return true;
        }
    }

    /** \brief Return true iff \c rhs is of the form <tt> max(l_1 ... lhs ... l_k) </tt>,
        such that l_i's do not contain lhs.

        If the result is true, then all l_i's are stored in rest.
    */
    static bool generalized_check_meta(level const & m, level const & rhs, bool & found_m, buffer<level> & rest) {
        lean_assert(is_meta(m));
        if (is_max(rhs)) {
            return
                generalized_check_meta(m, max_lhs(rhs), found_m, rest) &&
                generalized_check_meta(m, max_rhs(rhs), found_m, rest);
        } else if (m == rhs) {
            found_m = true;
            return true;
        } else if (occurs_meta(m, rhs)) {
            return false;
        } else {
            rest.push_back(rhs);
            return true;
        }
    }

    status process_l_eq_max_core(level const & lhs, level const & rhs, justification const & jst) {
        lean_assert(is_meta(lhs));
        buffer<level> rest;
        bool found_lhs = false;
        if (generalized_check_meta(lhs, rhs, found_lhs, rest)) {
            level r;
            if (found_lhs) {
                // rhs is of the form max(rest, lhs)
                // Solution is lhs := max(rest, ?u) where ?u is fresh metavariable
                r = mk_meta_univ(m_ngen.next());
                rest.push_back(r);
                unsigned i = rest.size();
                while (i > 0) {
                    --i;
                    r = mk_max(rest[i], r);
                }
                r = normalize(r);
            } else {
                // lhs does not occur in rhs
                r = rhs;
            }

            if (assign(lhs, r, jst)) {
                return Solved;
            } else {
                set_conflict(jst);
                return Failed;
            }
        } else {
            return Continue;
        }
    }

    /** \brief Return solved iff \c c is a constraint of the form
                   lhs =?= max(rest, lhs)
               and is successfully solved.
    */
    status process_l_eq_max(constraint const & c) {
        lean_assert(is_level_eq_cnstr(c));
        level lhs = cnstr_lhs_level(c);
        level rhs = cnstr_rhs_level(c);
        justification jst = c.get_justification();
        if (is_meta(lhs))
            return process_l_eq_max_core(lhs, rhs, jst);
        else if (is_meta(rhs))
            return process_l_eq_max_core(rhs, lhs, jst);
        else
            return Continue;
    }

    /** Auxiliary method for process_succ_eq_max */
    status process_succ_eq_max_core(level const & lhs, level const & rhs, justification const & jst) {
        if (!is_succ(lhs) || !is_max(rhs))
            return Continue;
        level m = rhs;
        while (is_max(m)) {
            level m1 = max_lhs(m);
            level m2 = max_rhs(m);
            if (is_geq(lhs, m1)) {
                m = m2;
            } else if (is_geq(lhs, m2)) {
                m = m1;
            } else {
                return Continue;
            }
        }
        if (!is_meta(m))
            return Continue;
        if (assign(m, lhs, jst)) {
            return Solved;
        } else {
            set_conflict(jst);
            return Failed;
        }
    }

    /** \brief Return Solved iff \c c is a constraint of the form
                  succ^k_1 a =?= max(succ^k_2 b, ?m)
               where k_1 >= k_2 and a == b or b == zero

              and is successfully solved by assigning ?m := succ^k_1 a
    */
    status process_succ_eq_max(constraint const & c) {
        lean_assert(is_level_eq_cnstr(c));
        level lhs = cnstr_lhs_level(c);
        level rhs = cnstr_rhs_level(c);
        justification jst = c.get_justification();
        status st = process_succ_eq_max_core(lhs, rhs, jst);
        if (st != Continue) return st;
        return process_succ_eq_max_core(rhs, lhs, jst);
    }

    /**
       \brief Process the following constraints
          1. (max l1 l2) =?= 0    OR
                 solution:  l1 =?= 0, l2 =?= 0
          2. (imax l1 l2) =?= 0
                 solution:  l2 =?= 0
    */
    status try_level_eq_zero(level const & lhs, level const & rhs, justification const & j) {
        if (!is_zero(rhs))
            return Continue;
        if (is_max(lhs)) {
            if (process_constraint(mk_level_eq_cnstr(max_lhs(lhs), rhs, j)) &&
                process_constraint(mk_level_eq_cnstr(max_rhs(lhs), rhs, j)))
                return Solved;
            else
                return Failed;
        } else if (is_imax(lhs)) {
            return process_constraint(mk_level_eq_cnstr(imax_rhs(lhs), rhs, j)) ? Solved : Failed;
        } else {
            return Continue;
        }
    }

    status try_level_eq_zero(constraint const & c) {
        lean_assert(is_level_eq_cnstr(c));
        level const & lhs = cnstr_lhs_level(c);
        level const & rhs = cnstr_rhs_level(c);
        justification const & j = c.get_justification();
        status st = try_level_eq_zero(lhs, rhs, j);
        if (st != Continue) return st;
        return try_level_eq_zero(rhs, lhs, j);
    }

    /** \brief Try to solve constraints of the form
              (?m1 =?= max ?m2 ?m3)
              (?m1 =?= max ?m2 ?m3)
        by assigning ?m1 =?= ?m2 and ?m1 =?= ?m3

        \remark we may miss solutions.
    */
    status try_merge_max_core(level const & lhs, level const & rhs, justification const & j) {
        level m1 = lhs;
        level m2, m3;
        if (is_max(rhs)) {
            m2 = max_lhs(rhs);
            m3 = max_rhs(rhs);
        } else if (is_imax(rhs)) {
            m2 = imax_lhs(rhs);
            m3 = imax_rhs(rhs);
        } else {
            return Continue;
        }
        if (process_constraint(mk_level_eq_cnstr(m1, m2, j)) &&
            process_constraint(mk_level_eq_cnstr(m1, m3, j)))
            return Solved;
        else
            return Failed;
    }

    /** \see try_merge_max_core */
    status try_merge_max(constraint const & c) {
        lean_assert(is_level_eq_cnstr(c));
        level const & lhs = cnstr_lhs_level(c);
        level const & rhs = cnstr_rhs_level(c);
        justification const & j = c.get_justification();
        status st = try_merge_max_core(lhs, rhs, j);
        if (st != Continue) return st;
        return try_merge_max_core(rhs, lhs, j);
    }

    /** \brief Process the next constraint in the constraint queue m_cnstrs */
    bool process_next() {
        lean_assert(!m_cnstrs.empty());
        auto const * p = m_cnstrs.min();
        constraint c   = p->first;
        unsigned cidx  = p->second;
        if (cidx >= get_group_first_index(cnstr_group::ClassInstance) &&
            !m_config.m_discard && is_choice_cnstr(c) && cnstr_on_demand(c)) {
            // we postpone class-instance constraints whose type still contains metavariables
            m_cnstrs.erase_min();
            postpone(c);
            return true;
        }
        // std::cout << "process_next: " << c << "\n";
        m_cnstrs.erase_min();
        if (is_choice_cnstr(c)) {
            return process_choice_constraint(c);
        } else {
            auto r = instantiate_metavars(c);
            c = r.first;
            bool modified = r.second;
            if (is_level_eq_cnstr(c)) {
                if (modified) {
                    return process_constraint(c);
                }
                status st = process_l_eq_max(c);
                if (st != Continue) return st == Solved;
                st = process_succ_eq_max(c);
                if (st != Continue) return st == Solved;
                if (m_config.m_discard) {
                    // we only try try_level_eq_zero and try_merge_max when we are discarding
                    // constraints that canno be solved.
                    st = try_level_eq_zero(c);
                    if (st != Continue) return st == Solved;
                    if (cidx < get_group_first_index(cnstr_group::FlexFlex)) {
                        add_cnstr(c, cnstr_group::FlexFlex);
                        return true;
                    }
                    st = try_merge_max(c);
                    if (st != Continue) return st == Solved;
                    return process_plugin_constraint(c);
                } else {
                    discard(c);
                    return true;
                }
            } else {
                lean_assert(is_eq_cnstr(c));
                if (is_delta_cnstr(c)) {
                    return process_delta(c);
                } else if (modified) {
                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
                } else if (auto d = is_owned(c)) {
                    // Metavariable in the constraint is owned by choice constraint.
                    // choice constraint was postponed... since c was not modifed
                    // So, we should postpone this one too.
                    add_cnstr(c, to_cnstr_group(*d+1));
                    return true;
                } else if (is_flex_rigid(c)) {
                    return process_flex_rigid(c);
                } else if (is_flex_flex(c)) {
                    return process_flex_flex(c);
                } else {
                    return process_plugin_constraint(c);
                }
            }
        }
    }

    /** \brief Return true if unifier may be able to produce more solutions */
    bool more_solutions() const {
        return !in_conflict() || !m_case_splits.empty();
    }

    typedef optional<pair<substitution, constraints>> next_result;

    next_result failure() {
        lean_assert(in_conflict());
        if (m_config.m_use_exceptions)
            throw unifier_exception(*m_conflict, m_subst);
        else
            return next_result();
    }

    /** \brief Produce the next solution */
    next_result next() {
        if (!more_solutions())
            return failure();
        if (!m_first && !m_case_splits.empty()) {
            justification all_assumptions;
            for (auto const & cs : m_case_splits)
                all_assumptions = mk_composite1(all_assumptions, mk_assumption_justification(cs->m_assumption_idx));
            set_conflict(all_assumptions);
            if (!resolve_conflict())
                return failure();
        } else if (m_first) {
            m_first = false;
        } else {
            // This is not the first run, and there are no case-splits.
            // We don't throw an exception since there are no more solutions.
            return next_result();
        }

        while (true) {
            if (!in_conflict()) {
                if (m_cnstrs.empty())
                    break;
                process_next();
            }
            if (in_conflict() && !resolve_conflict())
                return failure();
        }
        lean_assert(!in_conflict());
        lean_assert(m_cnstrs.empty());
        substitution s = m_subst;
        s.forget_justifications();
        return next_result(mk_pair(s, m_postponed));
    }
};

unify_result_seq 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
        return unify_result_seq();
    } else {
        return mk_lazy_list<pair<substitution, constraints>>([=]() {
                auto s = u->next();
                if (s)
                    return some(mk_pair(*s, unify(u)));
                else
                    return unify_result_seq::maybe_pair();
            });
    }
}

unify_result_seq unify(environment const & env,  unsigned num_cs, constraint const * cs, name_generator const & ngen,
                       substitution const & s, unifier_config const & cfg) {
    return unify(std::make_shared<unifier_fn>(env, num_cs, cs, ngen, s, cfg));
}

unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
                       bool relax, substitution const & s, unifier_config const & cfg) {
    substitution new_s = s;
    expr _lhs = new_s.instantiate(lhs);
    expr _rhs = new_s.instantiate(rhs);
    auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, cfg);
    constraint_seq cs;
    if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
        return unify_result_seq();
    } else {
        return unify(u);
    }
}

static int unify_simple(lua_State * L) {
    int nargs = lua_gettop(L);
    unify_status r;
    if (nargs == 2)
        r = unify_simple(to_substitution(L, 1), to_constraint(L, 2));
    else if (nargs == 3 && is_expr(L, 2))
        r = unify_simple(to_substitution(L, 1), to_expr(L, 2), to_expr(L, 3), justification());
    else if (nargs == 3 && is_level(L, 2))
        r = unify_simple(to_substitution(L, 1), to_level(L, 2), to_level(L, 3), justification());
    else if (is_expr(L, 2))
        r = unify_simple(to_substitution(L, 1), to_expr(L, 2), to_expr(L, 3), to_justification(L, 4));
    else
        r = unify_simple(to_substitution(L, 1), to_level(L, 2), to_level(L, 3), to_justification(L, 4));
    return push_integer(L, static_cast<unsigned>(r));
}

DECL_UDATA(unify_result_seq)

static const struct luaL_Reg unify_result_seq_m[] = {
    {"__gc", unify_result_seq_gc},
    {0, 0}
};

static int unify_result_seq_next(lua_State * L) {
    unify_result_seq seq = to_unify_result_seq(L, lua_upvalueindex(1));
    unify_result_seq::maybe_pair p;
    p = seq.pull();
    if (p) {
        push_unify_result_seq(L, p->second);
        lua_replace(L, lua_upvalueindex(1));
        push_substitution(L, p->first.first);
        // TODO(Leo): return postponed constraints
    } else {
        lua_pushnil(L);
    }
    return 1;
}

static int push_unify_result_seq_it(lua_State * L, unify_result_seq const & seq) {
    push_unify_result_seq(L, seq);
    lua_pushcclosure(L, &safe_function<unify_result_seq_next>, 1); // create closure with 1 upvalue
    return 1;
}

static void to_constraint_buffer(lua_State * L, int idx, buffer<constraint> & cs) {
    luaL_checktype(L, idx, LUA_TTABLE);
    lua_pushvalue(L, idx); // put table on top of the stack
    int n = objlen(L, idx);
    for (int i = 1; i <= n; i++) {
        lua_rawgeti(L, -1, i);
        cs.push_back(to_constraint(L, -1));
        lua_pop(L, 1);
    }
    lua_pop(L, 1);
}

#if 0
static constraints to_constraints(lua_State * L, int idx) {
    buffer<constraint> cs;
    to_constraint_buffer(L, idx, cs);
    return to_list(cs.begin(), cs.end());
}

static unifier_plugin to_unifier_plugin(lua_State * L, int idx) {
    luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
    luaref f(L, idx);
    return unifier_plugin([=](constraint const & c, name_generator const & ngen) {
            lua_State * L = f.get_state();
            f.push();
            push_constraint(L, c);
            push_name_generator(L, ngen);
            pcall(L, 2, 1, 0);
            lazy_list<constraints> r;
            if (is_constraint(L, -1)) {
                // single constraint
                r = lazy_list<constraints>(constraints(to_constraint(L, -1)));
            } else if (lua_istable(L, -1)) {
                int num = objlen(L, -1);
                if (num == 0) {
                    // empty table
                    r = lazy_list<constraints>();
                } else {
                    lua_rawgeti(L, -1, 1);
                    if (is_constraint(L, -1)) {
                        // array of constraints case
                        lua_pop(L, 1);
                        r = lazy_list<constraints>(to_constraints(L, -1));
                    } else {
                        lua_pop(L, 1);
                        buffer<constraints> css;
                        // array of array of constraints
                        for (int i = 1; i <= num; i++) {
                            lua_rawgeti(L, -1, i);
                            css.push_back(to_constraints(L, -1));
                            lua_pop(L, 1);
                        }
                        r = to_lazy(to_list(css.begin(), css.end()));
                    }
                }
            } else if (lua_isnil(L, -1)) {
                // nil case
                r = lazy_list<constraints>();
            } else {
                throw exception("invalid unifier plugin, the result value must be a constrant, "
                                "nil, an array of constraints, or an array of arrays of constraints");
            }
            lua_pop(L, 1);
            return r;
        });
}
#endif

static name * g_tmp_prefix = nullptr;

static int unify(lua_State * L) {
    int nargs = lua_gettop(L);
    unify_result_seq r;
    environment const & env = to_environment(L, 1);
    if (is_expr(L, 2)) {
        if (nargs == 7)
            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6),
                      unifier_config(to_options(L, 7)));
        else if (nargs == 6)
            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6));
        else
            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
    } else {
        buffer<constraint> cs;
        to_constraint_buffer(L, 2, cs);
        if (nargs == 5)
            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4), unifier_config(to_options(L, 5)));
        else if (nargs == 4)
            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4));
        else
            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3));
    }
    return push_unify_result_seq_it(L, r);
}

void open_unifier(lua_State * L) {
    luaL_newmetatable(L, unify_result_seq_mt);
    lua_pushvalue(L, -1);
    lua_setfield(L, -2, "__index");
    setfuncs(L, unify_result_seq_m, 0);
    SET_GLOBAL_FUN(unify_result_seq_pred, "is_unify_result_seq");

    SET_GLOBAL_FUN(unify_simple,  "unify_simple");
    SET_GLOBAL_FUN(unify,         "unify");

    lua_newtable(L);
    SET_ENUM("Solved",       unify_status::Solved);
    SET_ENUM("Failed",       unify_status::Failed);
    SET_ENUM("Unsupported",  unify_status::Unsupported);
    lua_setglobal(L, "unify_status");
}

void initialize_unifier() {
    g_unifier_max_steps         = new name{"unifier", "max_steps"};
    g_unifier_computation       = new name{"unifier", "computation"};
    g_unifier_expensive_classes = new name{"unifier", "expensive_classes"};
    g_unifier_conservative      = new name{"unifier", "conservative"};
    g_unifier_nonchronological  = new name{"unifier", "nonchronological"};

    register_unsigned_option(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps");
    register_bool_option(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION,
                         "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints");
    register_bool_option(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES,
                         "(unifier) use \"full\" higher-order unification when solving class instances");
    register_bool_option(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE,
                         "(unifier) unfolds only constants marked as reducible, avoid expensive case-splits (it is faster but less complete)");
    register_bool_option(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL,
                         "(unifier) enable/disable nonchronological backtracking in the unifier (this option is only available for debugging and benchmarking purposes, and running experiments)");

    g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification(), false));
    g_tmp_prefix      = new name(name::mk_internal_unique_name());
}

void finalize_unifier() {
    delete g_tmp_prefix;
    delete g_dont_care_cnstr;
    delete g_unifier_max_steps;
    delete g_unifier_computation;
    delete g_unifier_expensive_classes;
    delete g_unifier_conservative;
    delete g_unifier_nonchronological;
}
}