/*
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 <vector>
#include "util/flet.h"
#include "util/list_fn.h"
#include "util/lazy_list_fn.h"
#include "util/sstream.h"
#include "util/name_map.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/kernel_exception.h"
#include "kernel/error_msgs.h"
#include "kernel/expr_maps.h"
#include "library/coercion.h"
#include "library/placeholder.h"
#include "library/choice.h"
#include "library/explicit.h"
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/locals.h"
#include "library/let.h"
#include "library/deep_copy.h"
#include "library/metavar_closure.h"
#include "library/typed_expr.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/class.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/no_info.h"
#include "frontends/lean/extra_info.h"
#include "frontends/lean/local_context.h"
#include "frontends/lean/choice_iterator.h"
#include "frontends/lean/placeholder_elaborator.h"
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/proof_qed_elaborator.h"

#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
#define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
#endif

namespace lean {
// ==========================================
// elaborator configuration options
static name * g_elaborator_local_instances = nullptr;

bool get_elaborator_local_instances(options const & opts) {
    return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);
}
// ==========================================

elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
                                       pos_info_provider const * pp, info_manager * info, bool check_unassigned):
    m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
    m_use_local_instances = get_elaborator_local_instances(ios.get_options());
}

/** \brief Mapping from metavariable names to metavariable applications (?M ...) */
typedef name_map<expr> mvar2meta;

/** \brief Helper class for implementing the \c elaborate functions. */
class elaborator : public coercion_info_manager {
    typedef name_map<expr> local_tactic_hints;
    typedef rb_map<expr, pair<expr, constraint_seq>, expr_quick_cmp> cache;

    elaborator_context & m_env;
    name_generator       m_ngen;
    type_checker_ptr     m_tc[2];
    // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
    // representing the context where ?m was created.
    local_context        m_context; // current local context: a list of local constants
    local_context        m_full_context; // superset of m_context, it also contains non-contextual locals.
    mvar2meta            m_mvar2meta;
    cache                m_cache;

    // mapping from metavariable name ?m to tactic expression that should be used to solve it.
    // this mapping is populated by the 'by tactic-expr' expression.
    local_tactic_hints   m_local_tactic_hints;
    // set of metavariables that we already reported unsolved/unassigned
    name_set             m_displayed_errors;
    // if m_relax_main_opaque is true, then treat opaque definitions from the main module as transparent.
    bool                 m_relax_main_opaque;
    // if m_no_info is true, we do not collect information when true,
    // we set is to true whenever we find no_info annotation.
    bool                 m_no_info;
    info_manager         m_pre_info_data;
    unifier_config       m_unifier_config;

    /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
        and a choice constraints <tt>(?m in fn)</tt> where \c fn is a choice function.
        The choice function produces a stream of alternatives. In this case, it produces a stream of
        size \c n, one alternative for each \c e_i.
        This is a helper class for implementing this choice functions.
    */
    struct choice_expr_elaborator : public choice_iterator {
        elaborator &  m_elab;
        local_context m_context;
        local_context m_full_context;
        expr          m_meta;
        expr          m_choice;
        unsigned      m_idx;
        bool          m_relax_main_opaque;
        choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx,
                               expr const & meta, expr const & c, bool relax):
            m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta), m_choice(c),
            m_idx(get_num_choices(m_choice)),
            m_relax_main_opaque(relax) {
        }

        virtual optional<constraints> next() {
            while (m_idx > 0) {
                --m_idx;
                expr const & c = get_choice(m_choice, m_idx);
                expr const & f = get_app_fn(c);
                m_elab.save_identifier_info(f);
                try {
                    flet<local_context> set1(m_elab.m_context,      m_context);
                    flet<local_context> set2(m_elab.m_full_context, m_full_context);
                    pair<expr, constraint_seq> rcs = m_elab.visit(c);
                    expr r = rcs.first;
                    constraint_seq cs = mk_eq_cnstr(m_meta, r, justification(), m_relax_main_opaque) + rcs.second;
                    return optional<constraints>(cs.to_list());
                } catch (exception &) {}
            }
            return optional<constraints>();
        }
    };

public:
    elaborator(elaborator_context & env, name_generator const & ngen):
        m_env(env),
        m_ngen(ngen),
        m_context(),
        m_full_context(),
        m_unifier_config(env.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
        m_relax_main_opaque = false;
        m_no_info = false;
        m_tc[0]  = mk_type_checker(env.m_env, m_ngen.mk_child(), false);
        m_tc[1]  = mk_type_checker(env.m_env, m_ngen.mk_child(), true);
    }

    environment const & env() const { return m_env.m_env; }
    io_state const & ios() const { return m_env.m_ios; }
    local_decls<level> const & lls() const { return m_env.m_lls; }
    bool use_local_instances() const { return m_env.m_use_local_instances; }
    info_manager * infom() const { return m_env.m_info_manager; }
    pos_info_provider const * pip() const { return m_env.m_pos_provider; }
    bool check_unassigned() const { return m_env.m_check_unassigned; }

    expr mk_local(name const & n, expr const & t, binder_info const & bi) {
        return ::lean::mk_local(m_ngen.next(), n, t, bi);
    }

    pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc[m_relax_main_opaque]->infer(e); }
    pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
    expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
    expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
    expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a).set_tag(g); }

    void register_meta(expr const & meta) {
        lean_assert(is_meta(meta));
        m_mvar2meta.insert(mlocal_name(get_app_fn(meta)), meta);
    }

    /** \brief Convert the metavariable to the metavariable application that captures
        the context where it was defined.
    */
    optional<expr> mvar_to_meta(expr const & mvar) {
        lean_assert(is_metavar(mvar));
        name const & m = mlocal_name(mvar);
        if (auto it = m_mvar2meta.find(m))
            return some_expr(*it);
        else
            return none_expr();
    }

    /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
    void save_type_data(expr const & e, expr const & r) {
        if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
            if (auto p = pip()->get_pos_info(e)) {
                expr t = m_tc[m_relax_main_opaque]->infer(r).first;
                m_pre_info_data.add_type_info(p->first, p->second, t);
            }
        }
    }

    /** \brief Store type information at pos(e) for r if \c e is marked as "extra" in the info_manager */
    void save_extra_type_data(expr const & e, expr const & r) {
        if (!m_no_info && infom() && pip()) {
            if (auto p = pip()->get_pos_info(e)) {
                expr t = m_tc[m_relax_main_opaque]->infer(r).first;
                m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
            }
        }
    }

    /** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
    void save_identifier_info(expr const & f) {
        if (!m_no_info && infom() && pip() && is_constant(f)) {
            if (auto p = pip()->get_pos_info(f))
                m_pre_info_data.add_identifier_info(p->first, p->second, const_name(f));
        }
    }

    /** \brief Store actual term that was synthesized for an explicit placeholders */
    void save_synth_data(expr const & e, expr const & r) {
        if (!m_no_info && infom() && pip() && is_placeholder(e)) {
            if (auto p = pip()->get_pos_info(e))
                m_pre_info_data.add_synth_info(p->first, p->second, r);
        }
    }

    void save_placeholder_info(expr const & e, expr const & r) {
        if (is_explicit_placeholder(e)) {
            save_type_data(e, r);
            save_synth_data(e, r);
        }
    }

    /** \brief Auxiliary function for saving information about which coercion was used by the elaborator.
        It marks that coercion c was used on e.
    */
    virtual void save_coercion_info(expr const & e, expr const & c) {
        if (!m_no_info && infom() && pip()) {
            if (auto p = pip()->get_pos_info(e)) {
                expr t = m_tc[m_relax_main_opaque]->infer(c).first;
                m_pre_info_data.add_coercion_info(p->first, p->second, c, t);
            }
        }
    }

    /** \brief Remove coercion information associated with \c e */
    virtual void erase_coercion_info(expr const & e) {
        if (!m_no_info && infom() && pip()) {
            if (auto p = pip()->get_pos_info(e))
                m_pre_info_data.erase_coercion_info(p->first, p->second);
        }
    }

    void copy_info_to_manager(substitution s) {
        if (!infom())
            return;
        m_pre_info_data.instantiate(s);
        bool overwrite = true;
        infom()->merge(m_pre_info_data, overwrite);
        m_pre_info_data.clear();
    }

    /** \brief Create a metavariable, and attach choice constraint for generating
        solutions using class-instances and tactic-hints.
    */
    expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
        auto ec = mk_placeholder_elaborator(env(), ios(), m_context,
                                            m_ngen.next(), m_relax_main_opaque, use_local_instances(),
                                            is_strict, type, g, m_unifier_config);
        register_meta(ec.first);
        cs += ec.second;
        return ec.first;
    }

    expr visit_expecting_type(expr const & e, constraint_seq & cs) {
        if (is_placeholder(e) && !placeholder_type(e)) {
            expr r = m_context.mk_type_meta(m_ngen, e.get_tag());
            save_placeholder_info(e, r);
            return r;
        } else {
            return visit(e, cs);
        }
    }

    expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs) {
        if (is_placeholder(e) && !placeholder_type(e)) {
            expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), cs);
            save_placeholder_info(e, r);
            return r;
        } else if (is_choice(e)) {
            return visit_choice(e, some_expr(t), cs);
        } else if (is_by(e)) {
            return visit_by(e, some_expr(t), cs);
        } else if (is_proof_qed_annotation(e)) {
            return visit_proof_qed(e, some_expr(t), cs);
        } else {
            return visit(e, cs);
        }
    }

    expr visit_choice(expr const & e, optional<expr> const & t, constraint_seq & cs) {
        lean_assert(is_choice(e));
        // Possible optimization: try to lookahead and discard some of the alternatives.
        expr m                 = m_full_context.mk_meta(m_ngen, t, e.get_tag());
        register_meta(m);
        bool relax             = m_relax_main_opaque;
        local_context ctx      = m_context;
        local_context full_ctx = m_full_context;
        auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */,
                      name_generator const & /* ngen */) {
            return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, e, relax));
        };
        justification j = mk_justification("none of the overloads is applicable", some_expr(e));
        cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque);
        return m;
    }

    expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs) {
        lean_assert(is_by(e));
        expr tac = visit(get_by_arg(e), cs);
        expr m   = m_context.mk_meta(m_ngen, t, e.get_tag());
        register_meta(m);
        m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac);
        return m;
    }

    expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
        lean_assert(is_proof_qed_annotation(e));
        pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
        expr m                         = m_full_context.mk_meta(m_ngen, t, e.get_tag());
        register_meta(m);
        constraint c                   = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, m_relax_main_opaque);
        cs += c;
        return m;
    }

    static bool is_implicit_pi(expr const & e) {
        if (!is_pi(e))
            return false;
        binder_info bi = binding_info(e);
        return bi.is_strict_implicit() || bi.is_implicit();
    }

    /** \brief Auxiliary function for adding implicit arguments to coercions to function-class */
    expr add_implict_args(expr e, constraint_seq & cs, bool relax) {
        type_checker & tc = *m_tc[relax];
        constraint_seq new_cs;
        expr type = tc.whnf(tc.infer(e, new_cs), new_cs);
        if (!is_implicit_pi(type))
            return e;
        cs += new_cs;
        while (true) {
            lean_assert(is_pi(type));
            tag g = e.get_tag();
            bool is_strict = false;
            expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, cs);
            e              = mk_app(e, imp_arg, g);
            type           = instantiate(binding_body(type), imp_arg);
            constraint_seq new_cs;
            type           = tc.whnf(type, new_cs);
            if (!is_implicit_pi(type))
                return e;
            cs += new_cs;
        }
    }

    /** \brief Make sure \c f is really a function, if it is not, try to apply coercions.
        The result is a pair <tt>new_f, f_type</tt>, where new_f is the new value for \c f,
        and \c f_type is its type (and a Pi-expression)
    */
    pair<expr, expr> ensure_fun(expr f, constraint_seq & cs) {
        expr f_type = infer_type(f, cs);
        if (!is_pi(f_type))
            f_type = whnf(f_type, cs);
        if (!is_pi(f_type) && has_metavar(f_type)) {
            constraint_seq saved_cs = cs;
            expr new_f_type = whnf(f_type, cs);
            if (!is_pi(new_f_type) && is_meta(new_f_type)) {
                cs = saved_cs;
                // let type checker add constraint
                f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
            } else {
                f_type = new_f_type;
            }
        }
        if (!is_pi(f_type)) {
            // try coercion to function-class
            list<expr> coes  = get_coercions_to_fun(env(), f_type);
            if (is_nil(coes)) {
                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
            } else if (is_nil(tail(coes))) {
                expr old_f = f;
                bool relax = m_relax_main_opaque;
                f = mk_app(head(coes), f, f.get_tag());
                f = add_implict_args(f, cs, relax);
                f_type = infer_type(f, cs);
                save_coercion_info(old_f, f);
                lean_assert(is_pi(f_type));
            } else {
                bool relax             = m_relax_main_opaque;
                local_context ctx      = m_context;
                local_context full_ctx = m_full_context;
                justification j        = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
                        return pp_function_expected(fmt, substitution(subst).instantiate(f));
                    });
                auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator const &) {
                    flet<local_context> save1(m_context,      ctx);
                    flet<local_context> save2(m_full_context, full_ctx);
                    list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
                            expr new_f      = copy_tag(f, ::lean::mk_app(coe, f));
                            constraint_seq cs;
                            new_f = add_implict_args(new_f, cs, relax);
                            cs += mk_eq_cnstr(meta, new_f, j, relax);
                            return cs.to_list();
                        });
                    return choose(std::make_shared<coercion_elaborator>(*this, f, choices, coes, false));
                };
                f   = m_full_context.mk_meta(m_ngen, none_expr(), f.get_tag());
                register_meta(f);
                cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax);
                lean_assert(is_meta(f));
                // let type checker add constraint
                f_type = infer_type(f, cs);
                f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
                lean_assert(is_pi(f_type));
            }
        } else {
            erase_coercion_info(f);
        }
        lean_assert(is_pi(f_type));
        return mk_pair(f, f_type);
    }

    bool has_coercions_from(expr const & a_type) {
        expr const & a_cls = get_app_fn(whnf(a_type).first);
        return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls));
    }

    bool has_coercions_to(expr d_type) {
        d_type = whnf(d_type).first;
        expr const & fn = get_app_fn(d_type);
        if (is_constant(fn))
            return ::lean::has_coercions_to(env(), const_name(fn));
        else if (is_pi(d_type))
            return ::lean::has_coercions_to_fun(env());
        else if (is_sort(d_type))
            return ::lean::has_coercions_to_sort(env());
        else
            return false;
    }

    expr apply_coercion(expr const & a, expr a_type, expr d_type) {
        a_type = whnf(a_type).first;
        d_type = whnf(d_type).first;
        constraint_seq aux_cs;
        list<expr> coes = get_coercions_from_to(*m_tc[m_relax_main_opaque], a_type, d_type, aux_cs);
        if (is_nil(coes)) {
            erase_coercion_info(a);
            return a;
        } else if (is_nil(tail(coes))) {
            expr r = mk_app(head(coes), a, a.get_tag());
            save_coercion_info(a, r);
            return r;
        } else {
            for (expr const & coe : coes) {
                expr r = mk_app(coe, a, a.get_tag());
                expr r_type = infer_type(r).first;
                if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) {
                    save_coercion_info(a, r);
                    return r;
                }
            }
            erase_coercion_info(a);
            return a;
        }
    }

    /** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */
    pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type,
                                                   justification const & j) {
        bool relax = m_relax_main_opaque;
        type_checker & tc = *m_tc[relax];
        expr m       = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag());
        register_meta(m);
        constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax);
        return to_ecs(m, c);
    }

    /** \brief Given a term <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed

        \remark relax == true affects how opaque definitions in the main module are treated.
    */
    pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
                                               justification const & j, bool relax) {
        if (is_meta(expected_type) && has_coercions_from(a_type)) {
            return mk_delayed_coercion(a, a_type, expected_type, j);
        } else if (is_meta(a_type) && has_coercions_to(expected_type)) {
            return mk_delayed_coercion(a, a_type, expected_type, j);
        } else {
            auto dcs = m_tc[relax]->is_def_eq(a_type, expected_type, j);
            if (dcs.first) {
                return to_ecs(a, dcs.second);
            } else {
                expr new_a = apply_coercion(a, a_type, expected_type);
                constraint_seq cs;
                bool coercion_worked = false;
                if (!is_eqp(a, new_a)) {
                    expr new_a_type = infer_type(new_a, cs);
                    coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j, cs);
                }
                if (coercion_worked) {
                    return to_ecs(new_a, cs);
                } else if (has_metavar(a_type) || has_metavar(expected_type)) {
                    // rely on unification hints to solve this constraint
                    return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j, relax));
                } else {
                    throw unifier_exception(j, substitution());
                }
            }
        }
    }

    bool is_choice_app(expr const & e) {
        expr const & f = get_app_fn(e);
        return is_choice(f) || (is_annotation(f) && is_choice(get_nested_annotation_arg(f)));
    }

    /** \brief Process ((choice f_1 ... f_n) a_1 ... a_k) as
        (choice (f_1 a_1 ... a_k) ... (f_n a_1 ... a_k))
    */
    expr visit_choice_app(expr const & e, constraint_seq & cs) {
        buffer<expr> args;
        expr r = get_app_rev_args(e, args);
        expr f = get_nested_annotation_arg(r);
        lean_assert(is_choice(f));
        buffer<expr> new_choices;
        unsigned num = get_num_choices(f);
        for (unsigned i = 0; i < num; i++) {
            expr f_i = get_choice(f, i);
            f_i      = copy_annotations(r, f_i);
            new_choices.push_back(mk_rev_app(f_i, args));
        }
        return visit_choice(copy_tag(e, mk_choice(new_choices.size(), new_choices.data())), none_expr(), cs);
    }

    expr visit_app(expr const & e, constraint_seq & cs) {
        if (is_choice_app(e))
            return visit_choice_app(e, cs);
        constraint_seq f_cs;
        bool expl   = is_nested_explicit(get_app_fn(e));
        expr f      = visit(app_fn(e), f_cs);
        auto f_t    = ensure_fun(f, f_cs);
        f           = f_t.first;
        expr f_type = f_t.second;
        lean_assert(is_pi(f_type));
        if (!expl) {
            bool first = true;
            while (binding_info(f_type).is_strict_implicit() || (!first && binding_info(f_type).is_implicit())) {
                tag g          = f.get_tag();
                bool is_strict = false;
                expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, f_cs);
                f              = mk_app(f, imp_arg, g);
                auto f_t       = ensure_fun(f, f_cs);
                f              = f_t.first;
                f_type         = f_t.second;
                first          = false;
            }
            if (!first) {
                // we save the info data again for application of functions with strict implicit arguments
                save_type_data(get_app_fn(e), f);
            }
        }
        constraint_seq a_cs;
        expr d_type = binding_domain(f_type);
        expr a      = visit_expecting_type_of(app_arg(e), d_type, a_cs);
        expr a_type = infer_type(a, a_cs);
        expr r      = mk_app(f, a, e.get_tag());

        justification j = mk_app_justification(r, a, d_type, a_type);
        auto new_a_cs   = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque);
        expr new_a      = new_a_cs.first;
        cs += f_cs + new_a_cs.second + a_cs;
        return update_app(r, app_fn(r), new_a);
    }

    expr visit_placeholder(expr const & e, constraint_seq & cs) {
        expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), cs);
        save_placeholder_info(e, r);
        return r;
    }

    level replace_univ_placeholder(level const & l) {
        return replace(l, [&](level const & l) {
                if (is_placeholder(l))
                    return some_level(mk_meta_univ(m_ngen.next()));
                else
                    return none_level();
            });
    }

    expr visit_sort(expr const & e) {
        return update_sort(e, replace_univ_placeholder(sort_level(e)));
    }

    expr visit_macro(expr const & e, constraint_seq & cs) {
        if (is_as_is(e)) {
            return get_as_is_arg(e);
        } else {
            // Remark: Macros are not meant to be used in the front end.
            // Perhaps, we should throw error.
            buffer<expr> args;
            for (unsigned i = 0; i < macro_num_args(e); i++)
                args.push_back(visit(macro_arg(e, i), cs));
            return update_macro(e, args.size(), args.data());
        }
    }

    expr visit_constant(expr const & e) {
        declaration d = env().get(const_name(e));
        buffer<level> ls;
        for (level const & l : const_levels(e))
            ls.push_back(replace_univ_placeholder(l));
        unsigned num_univ_params = length(d.get_univ_params());
        if (num_univ_params < ls.size())
            throw_kernel_exception(env(), sstream() << "incorrect number of universe levels parameters for '"
                                   << const_name(e) << "', #" << num_univ_params
                                   << " expected, #" << ls.size() << " provided");
        // "fill" with meta universe parameters
        for (unsigned i = ls.size(); i < num_univ_params; i++)
            ls.push_back(mk_meta_univ(m_ngen.next()));
        lean_assert(num_univ_params == ls.size());
        return update_constant(e, to_list(ls.begin(), ls.end()));
    }

    /** \brief Make sure \c e is a type. If it is not, then try to apply coercions. */
    expr ensure_type(expr const & e, constraint_seq & cs) {
        expr t = infer_type(e, cs);
        erase_coercion_info(e);
        if (is_sort(t))
            return e;
        t = whnf(t, cs);
        if (is_sort(t))
            return e;
        if (has_metavar(t)) {
            t = whnf(t, cs);
            if (is_sort(t))
                return e;
            if (is_meta(t)) {
                // let type checker add constraint
                m_tc[m_relax_main_opaque]->ensure_sort(t, e, cs);
                return e;
            }
        }
        list<expr> coes = get_coercions_to_sort(env(), t);
        if (is_nil(coes)) {
            throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
        } else {
            // Remark: we ignore other coercions to sort
            expr r = mk_app(head(coes), e, e.get_tag());
            save_coercion_info(e, r);
            return r;
        }
    }

    /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants.
        When replacing a variable with a local, we copy the local constant and inherit the tag
        associated with the variable. This is a trick for getter better error messages */
    expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subst) {
        if (closed(a))
            return a;
        return replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
                if (offset >= get_free_var_range(m))
                    return some_expr(m); // expression m does not contain free variables with idx >= offset
                if (is_var(m)) {
                    unsigned vidx = var_idx(m);
                    if (vidx >= offset) {
                        unsigned h = offset + n;
                        if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
                            expr local = subst[n - (vidx - offset) - 1];
                            lean_assert(is_local(local));
                            return some_expr(copy_tag(m, copy(local)));
                        } else {
                            return some_expr(copy_tag(m, mk_var(vidx - n)));
                        }
                    }
                }
                return none_expr();
            });
    }

    expr visit_binding(expr e, expr_kind k, constraint_seq & cs) {
        flet<local_context> save1(m_context, m_context);
        flet<local_context> save2(m_full_context, m_full_context);
        buffer<expr> ds, ls, es;
        while (e.kind() == k) {
            es.push_back(e);
            expr d   = binding_domain(e);
            d = instantiate_rev_locals(d, ls.size(), ls.data());
            d = ensure_type(visit_expecting_type(d, cs), cs);
            ds.push_back(d);
            expr l   = mk_local(binding_name(e), d, binding_info(e));
            if (binding_info(e).is_contextual())
                m_context.add_local(l);
            m_full_context.add_local(l);
            ls.push_back(l);
            e = binding_body(e);
        }
        lean_assert(ls.size() == es.size() && ls.size() == ds.size());
        e = instantiate_rev_locals(e, ls.size(), ls.data());
        e = (k == expr_kind::Pi) ? ensure_type(visit_expecting_type(e, cs), cs) : visit(e, cs);
        e = abstract_locals(e, ls.size(), ls.data());
        unsigned i = ls.size();
        while (i > 0) {
            --i;
            e = update_binding(es[i], abstract_locals(ds[i], i, ls.data()), e);
        }
        return e;
    }
    expr visit_pi(expr const & e, constraint_seq & cs) { return visit_binding(e, expr_kind::Pi, cs); }
    expr visit_lambda(expr const & e, constraint_seq & cs) { return visit_binding(e, expr_kind::Lambda, cs); }

    expr visit_typed_expr(expr const & e, constraint_seq & cs) {
        constraint_seq t_cs;
        expr t      = visit(get_typed_expr_type(e), t_cs);
        constraint_seq v_cs;
        expr v      = visit(get_typed_expr_expr(e), v_cs);
        expr v_type = infer_type(v, v_cs);
        justification j = mk_type_mismatch_jst(v, v_type, t, e);
        auto new_vcs    = ensure_has_type(v, v_type, t, j, m_relax_main_opaque);
        v = new_vcs.first;
        cs += t_cs + new_vcs.second + v_cs;
        return v;
    }

    expr visit_let_value(expr const & e, constraint_seq & cs) {
        if (auto p = m_cache.find(e)) {
            cs += p->second;
            return p->first;
        } else {
            auto ecs = visit(get_let_value_expr(e));
            expr r = copy_tag(ecs.first, mk_let_value(ecs.first));
            m_cache.insert(e, mk_pair(r, ecs.second));
            cs += ecs.second;
            return r;
        }
    }

    expr visit_core(expr const & e, constraint_seq & cs) {
        if (is_placeholder(e)) {
            return visit_placeholder(e, cs);
        } else if (is_choice(e)) {
            return visit_choice(e, none_expr(), cs);
        } else if (is_let_value(e)) {
            return visit_let_value(e, cs);
        } else if (is_by(e)) {
            return visit_by(e, none_expr(), cs);
        } else if (is_proof_qed_annotation(e)) {
            return visit_proof_qed(e, none_expr(), cs);
        } else if (is_no_info(e)) {
            flet<bool> let(m_no_info, true);
            return visit(get_annotation_arg(e), cs);
        } else if (is_typed_expr(e)) {
            return visit_typed_expr(e, cs);
        } else if (is_implicit(e)) {
            return visit_core(get_implicit_arg(e), cs);
        } else {
            switch (e.kind()) {
            case expr_kind::Local:      return e;
            case expr_kind::Meta:       return e;
            case expr_kind::Sort:       return visit_sort(e);
            case expr_kind::Var:        lean_unreachable();  // LCOV_EXCL_LINE
            case expr_kind::Constant:   return visit_constant(e);
            case expr_kind::Macro:      return visit_macro(e, cs);
            case expr_kind::Lambda:     return visit_lambda(e, cs);
            case expr_kind::Pi:         return visit_pi(e, cs);
            case expr_kind::App:        return visit_app(e, cs);
            }
            lean_unreachable(); // LCOV_EXCL_LINE
        }
    }

    pair<expr, constraint_seq> visit(expr const & e) {
        if (is_extra_info(e)) {
            auto ecs = visit(get_annotation_arg(e));
            save_extra_type_data(e, ecs.first);
            return ecs;
        }
        expr r;
        expr b = e;
        constraint_seq cs;
        if (is_explicit(e)) {
            b    = get_explicit_arg(e);
            r    = visit_core(get_explicit_arg(e), cs);
        } else if (is_explicit(get_app_fn(e))) {
            r    = visit_core(e, cs);
        } else {
            if (is_implicit(e)) {
                r = get_implicit_arg(e);
                if (is_explicit(r)) r = get_explicit_arg(r);
                b = r;
                r = visit_core(r, cs);
            } else {
                r = visit_core(e, cs);
            }
            tag  g         = e.get_tag();
            expr r_type    = whnf(infer_type(r, cs), cs);
            expr imp_arg;
            bool is_strict = false;
            while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
                imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs);
                r       = mk_app(r, imp_arg, g);
                r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
            }
        }
        save_type_data(b, r);
        return mk_pair(r, cs);
    }

    expr visit(expr const & e, constraint_seq & cs) {
        auto r = visit(e);
        cs += r.second;
        return r.first;
    }

    unify_result_seq solve(constraint_seq const & cs) {
        buffer<constraint> tmp;
        cs.linearize(tmp);
        return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), m_unifier_config);
    }

    void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) {
        lean_assert(is_metavar(mvar));
        if (!m_displayed_errors.contains(mlocal_name(mvar))) {
            m_displayed_errors.insert(mlocal_name(mvar));
            auto out = regular(env(), ios());
            flycheck_error err(out);
            display_error_pos(out, pip(), mvar);
            out << " unsolved placeholder, " << msg << "\n" << ps << endl;
        }
    }

    // For each occurrence of \c exact_tac in \c pre_tac, display its unassigned metavariables.
    // This is a trick to improve the quality of the error messages.
    void check_exact_tacs(expr const & pre_tac, substitution const & s) {
        for_each(pre_tac, [&](expr const & e, unsigned) {
                expr const & f = get_app_fn(e);
                if (is_constant(f) && const_name(f) == const_name(get_exact_tac_fn())) {
                    display_unassigned_mvars(e, s);
                    return false;
                } else {
                    return true;
                }
            });
    }

    optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
        if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) {
            expr pre_tac = subst.instantiate(*it);
            pre_tac = solve_unassigned_mvars(subst, pre_tac, visited);
            check_exact_tacs(pre_tac, subst);
            return some_expr(pre_tac);
        } else {
            return none_expr();
        }
    }

    optional<tactic> pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) {
        try {
            return optional<tactic>(expr_to_tactic(env(), pre_tac, pip()));
        } catch (expr_to_tactic_exception & ex) {
            auto out = regular(env(), ios());
            display_error_pos(out, pip(), mvar);
            out << " " << ex.what();
            out << pp_indent_expr(out.get_formatter(), pre_tac) << endl << "failed at:"
                << pp_indent_expr(out.get_formatter(), ex.get_expr()) << endl;
            return optional<tactic>();
        }
    }

    optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited) {
        if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
            return pre_tactic_to_tactic(*pre_tac, mvar);
        } else {
            return optional<tactic>();
        }
    }

    /** \brief Try to instantiate meta-variable \c mvar (modulo its state ps) using the given tactic.
        If it succeeds, then update subst with the solution.
        Return true iff the metavariable \c mvar has been assigned.

        If \c show_failure == true, then display reason for failure.
    */
    bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
                   bool show_failure) {
        lean_assert(length(ps.get_goals()) == 1);
        // make sure ps is a really a proof state for mvar.
        lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar));
        try {
            proof_state_seq seq = tac(env(), ios(), ps);
            auto r = seq.pull();
            if (!r) {
                // tactic failed to produce any result
                if (show_failure)
                    display_unsolved_proof_state(mvar, ps, "tactic failed");
                return false;
            } else if (!empty(r->first.get_goals())) {
                // tactic contains unsolved subgoals
                if (show_failure)
                    display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
                return false;
            } else {
                subst = r->first.get_subst();
                expr v = subst.instantiate(mvar);
                subst.assign(mlocal_name(mvar), v);
                return true;
            }
        } catch (tactic_exception & ex) {
            if (show_failure) {
                auto out = regular(env(), ios());
                display_error_pos(out, pip(), ex.get_expr());
                out << " tactic failed: " << ex.what() << "\n";
            }
            return false;
        }
    }

    void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited) {
        if (visited.contains(mlocal_name(mvar)))
            return;
        visited.insert(mlocal_name(mvar));
        auto meta = mvar_to_meta(mvar);
        if (!meta)
            return;
        meta = instantiate_meta(*meta, subst);
        // TODO(Leo): we are discarding constraints here
        expr type = m_tc[m_relax_main_opaque]->infer(*meta).first;
        // first solve unassigned metavariables in type
        type = solve_unassigned_mvars(subst, type, visited);
        proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
        if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) {
            // using user provided tactic
            bool show_failure = true;
            try_using(subst, mvar, ps, *local_hint, show_failure);
        } else {
            // using tactic_hints
            for (tactic_hint_entry const & tentry : get_tactic_hints(env())) {
                bool show_failure = false;
                if (try_using(subst, mvar, ps, tentry.get_tactic(), show_failure))
                    return;
            }
        }
    }

    expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited) {
        e = subst.instantiate(e);
        metavar_closure mvars(e);
        mvars.for_each_expr_mvar([&](expr const & mvar) {
                check_interrupted();
                solve_unassigned_mvar(subst, mvar, visited);
            });
        return subst.instantiate(e);
    }

    expr solve_unassigned_mvars(substitution & subst, expr const & e) {
        name_set visited;
        return solve_unassigned_mvars(subst, e, visited);
    }

    void display_unassigned_mvars(expr const & e, substitution const & s) {
        if (check_unassigned() && has_metavar(e)) {
            substitution tmp_s(s);
            for_each(e, [&](expr const & e, unsigned) {
                    if (!is_metavar(e))
                        return has_metavar(e);
                    if (auto it = mvar_to_meta(e)) {
                        expr meta      = tmp_s.instantiate(*it);
                        expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
                        goal g(meta, meta_type);
                        display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen),
                                                     "don't know how to synthesize it");
                    }
                    return false;
                });
        }
    }

    /** \brief Apply substitution and solve remaining metavariables using tactics. */
    expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params) {
        expr r = s.instantiate(e);
        if (has_univ_metavar(r))
            r = univ_metavars_to_params(env(), lls(), s, univ_params, new_params, r);
        r = solve_unassigned_mvars(s, r);
        display_unassigned_mvars(r, s);
        return r;
    }

    std::tuple<expr, level_param_names> apply(substitution & s, expr const & e) {
        auto ps = collect_univ_params(e);
        buffer<name> new_ps;
        expr r = apply(s, e, ps, new_ps);
        return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
    }

    std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
                                                   bool relax_main_opaque) {
        m_context.set_ctx(ctx);
        m_full_context.set_ctx(ctx);
        flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque);
        constraint_seq cs;
        expr r = visit(e, cs);
        if (_ensure_type)
            r = ensure_type(r, cs);
        auto p  = solve(cs).pull();
        lean_assert(p);
        substitution s = p->first.first;
        auto result = apply(s, r);
        copy_info_to_manager(s);
        return result;
    }

    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
        lean_assert(!has_local(t));
        lean_assert(!has_local(v));
        constraint_seq t_cs;
        expr r_t      = ensure_type(visit(t, t_cs), t_cs);
        // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.
        flet<bool> set_relax(m_relax_main_opaque, is_opaque);
        constraint_seq v_cs;
        expr r_v      = visit(v, v_cs);
        expr r_v_type = infer_type(r_v, v_cs);
        justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) {
                substitution s(subst);
                return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
            });
        pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j, is_opaque);
        r_v = r_v_cs.first;
        constraint_seq cs = t_cs + r_v_cs.second + v_cs;
        auto p  = solve(cs).pull();
        lean_assert(p);
        substitution s = p->first.first;
        name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t));
        buffer<name> new_params;
        expr new_r_t = apply(s, r_t, univ_params, new_params);
        expr new_r_v = apply(s, r_v, univ_params, new_params);
        copy_info_to_manager(s);
        return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
    }
};

static name * g_tmp_prefix = nullptr;

std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
                                              bool relax_main_opaque, bool ensure_type) {
    return elaborator(env, name_generator(*g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque);
}

std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
                                                    bool is_opaque) {
    return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n, is_opaque);
}

void initialize_elaborator() {
    g_elaborator_local_instances = new name{"elaborator", "local_instances"};

    register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
                         "(lean elaborator) use local declarates as class instances");
    g_tmp_prefix = new name(name::mk_internal_unique_name());
}

void finalize_elaborator() {
    delete g_elaborator_local_instances;
    delete g_tmp_prefix;
}
}