diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 87b20e93ce..28de75c5d0 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -19,6 +19,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp - old_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp + old_type_checker.cpp old_converter.cpp old_default_converter.cpp old_util.cpp ) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 5b8e5c92d9..0b65d9360b 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -372,7 +372,6 @@ public: if (mask[i]) { --j; expr const & m = head(it); - // TODO(Leo): old_type_context used relaxed_assign if (!m_ctx.is_def_eq(m, args[j])) { trace_unify_failure(c, j, m, args[j]); throw app_builder_exception(); diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 328ea8cbd1..fce1d09918 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -49,14 +49,10 @@ Author: Leonardo de Moura #include "library/rfl_lemmas.h" #include "library/pattern_attribute.h" -// #include "library/congr_lemma_manager.h" -// #include "library/light_lt_manager.h" - #include "library/old_converter.h" #include "library/old_default_converter.h" #include "library/old_type_checker.h" -#include "library/old_type_context.h" namespace lean { @@ -112,10 +108,7 @@ void initialize_library_module() { initialize_user_recursors(); initialize_noncomputable(); initialize_aux_recursors(); - initialize_old_type_context(); initialize_app_builder(); - // initialize_light_rule_set(); - // initialize_congr_lemma_manager(); initialize_fun_info(); initialize_unification_hint(); initialize_rfl_lemmas(); @@ -137,10 +130,7 @@ void finalize_library_module() { finalize_rfl_lemmas(); finalize_unification_hint(); finalize_fun_info(); - // finalize_congr_lemma_manager(); - // finalize_light_rule_set(); finalize_app_builder(); - finalize_old_type_context(); finalize_aux_recursors(); finalize_noncomputable(); finalize_user_recursors(); diff --git a/src/library/old_type_context.cpp b/src/library/old_type_context.cpp deleted file mode 100644 index bb59397e70..0000000000 --- a/src/library/old_type_context.cpp +++ /dev/null @@ -1,2025 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/interrupt.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/for_each_fn.h" -#include "kernel/replace_fn.h" -#include "kernel/inductive/inductive.h" -#include "library/trace.h" -#include "library/util.h" -#include "library/projection.h" -#include "library/normalize.h" -#include "library/replace_visitor.h" -#include "library/old_type_context.h" -#include "library/pp_options.h" -#include "library/reducible.h" -#include "library/exception.h" -#include "library/class.h" -#include "library/constants.h" -#include "library/unification_hint.h" - -#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH -#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 -#endif - -#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES -#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true -#endif - -namespace lean { -static name * g_tmp_prefix = nullptr; -static name * g_internal_prefix = nullptr; -static name * g_class_instance_max_depth = nullptr; -static name * g_class_trans_instances = nullptr; - -unsigned get_class_instance_max_depth(options const & o); -bool get_class_trans_instances(options const &) { return false; } - -old_type_context::old_type_context(environment const & env, options const & o, bool multiple_instances): - m_env(env), - m_proj_info(get_projection_info_map(env)) { - m_pip = nullptr; - m_ci_multiple_instances = multiple_instances; - m_ignore_external_mvars = false; - m_check_types = true; - m_relax_is_opaque = false; - // TODO(Leo): use compilation options for setting config - m_ci_max_depth = 32; - m_ci_trans_instances = true; - update_options(o); -} - -old_type_context::~old_type_context() { -} - -void old_type_context::push() { - m_infer_cache.push(); - push_core(); -} - -void old_type_context::pop() { - pop_core(); - m_infer_cache.pop(); -} - -expr old_type_context::mk_tmp_local(expr const & type, binder_info const & bi) { - name n = mk_tagged_fresh_name(*g_tmp_prefix); - return lean::mk_local(n, n, type, bi); -} - -expr old_type_context::mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi) { - name n = mk_tagged_fresh_name(*g_tmp_prefix); - return lean::mk_local(n, pp_name, type, bi); -} - -bool old_type_context::is_tmp_local(expr const & e) const { - if (!is_local(e)) - return false; - name const & n = mlocal_name(e); - return is_tagged_by(n, *g_tmp_prefix); -} - -expr old_type_context::mk_internal_local(name const & n, expr const & type, binder_info const & bi) { - return mk_local(mk_tagged_fresh_name(*g_internal_prefix), n, type, bi); -} - -expr old_type_context::mk_internal_local(expr const & type, binder_info const & bi) { - name n = mk_tagged_fresh_name(*g_internal_prefix); - return mk_local(n, n, type, bi); -} - -bool old_type_context::is_internal_local(expr const & e) const { - if (!is_local(e)) - return false; - name const & n = mlocal_name(e); - return is_tagged_by(n, *g_internal_prefix); -} - -void old_type_context::set_local_instances(list const & insts) { - clear_cache(); - m_ci_local_instances.clear(); - for (expr const & e : insts) { - if (auto cname = is_class(infer(e))) { - m_ci_local_instances.push_back(mk_pair(*cname, e)); - } - } -} - -bool old_type_context::is_opaque(declaration const & d) const { - if (d.is_theorem()) - return true; - name const & n = d.get_name(); - if (m_proj_info.contains(n)) - return true; - if (m_relax_is_opaque) - return false; - return is_extra_opaque(n); -} - -optional old_type_context::is_transparent(name const & n) { - auto it = m_is_transparent_cache[m_relax_is_opaque].find(n); - if (it != m_is_transparent_cache[m_relax_is_opaque].end()) { - return it->second; - } - optional r; - if (auto d = m_env.find(n)) { - if (d->is_definition() && !is_opaque(*d)) - r = d; - } - m_is_transparent_cache[m_relax_is_opaque].insert(mk_pair(n, r)); - return r; -} - -optional old_type_context::expand_macro(expr const & m) { - lean_assert(is_macro(m)); - if (m_in_is_def_eq || should_unfold_macro(m)) - return macro_def(m).expand(m, *this); - else - return none_expr(); -} - -optional old_type_context::reduce_projection(expr const & e) { - expr const & f = get_app_fn(e); - if (!is_constant(f)) - return none_expr(); - projection_info const * info = m_proj_info.find(const_name(f)); - if (!info) - return none_expr(); - buffer args; - get_app_args(e, args); - if (args.size() <= info->m_nparams) - return none_expr(); - unsigned mkidx = info->m_nparams; - expr const & mk = args[mkidx]; - expr new_mk = whnf(mk); - expr const & new_mk_fn = get_app_fn(new_mk); - if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor) - return none_expr(); - buffer mk_args; - get_app_args(new_mk, mk_args); - unsigned i = info->m_nparams + info->m_i; - if (i >= mk_args.size()) - none_expr(); - expr r = mk_args[i]; - r = mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1); - return some_expr(r); -} - -optional old_type_context::norm_ext(expr const & e) { - if (auto r = reduce_projection(e)) { - return r; - } else { - return m_env.norm_ext()(e, *this); - } -} - -expr old_type_context::whnf_core(expr const & e) { - check_system("whnf"); - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: - return e; - case expr_kind::Let: - return whnf_core(instantiate(let_body(e), let_value(e))); - case expr_kind::Macro: - if (auto m = expand_macro(e)) - return whnf_core(*m); - else - return e; - break; - case expr_kind::App: { - buffer args; - expr f0 = get_app_rev_args(e, args); - expr f = whnf_core(f0); - if (is_lambda(f)) { - unsigned m = 1; - unsigned num_args = args.size(); - while (is_lambda(binding_body(f)) && m < num_args) { - f = binding_body(f); - m++; - } - lean_assert(m <= num_args); - return whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), - num_args - m, args.data())); - } else { - return f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data())); - } - }} - lean_unreachable(); -} - -/** \brief Expand \c e if it is non-opaque constant with height >= h */ -expr old_type_context::unfold_name_core(expr e, unsigned h) { - if (is_constant(e)) { - if (auto d = is_transparent(const_name(e))) { - if (d->get_hints().get_height() >= h && length(const_levels(e)) == d->get_num_univ_params()) - return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h); - } - } - return e; -} - -/** \brief Expand constants and application where the function is a constant. - The unfolding is only performend if the constant corresponds to - a non-opaque definition with height >= h */ -expr old_type_context::unfold_names(expr const & e, unsigned h) { - if (is_app(e)) { - expr f0 = get_app_fn(e); - expr f = unfold_name_core(f0, h); - if (is_eqp(f, f0)) { - return e; - } else { - buffer args; - get_app_rev_args(e, args); - return mk_rev_app(f, args); - } - } else { - return unfold_name_core(e, h); - } -} - -/** \brief Return some definition \c d iff \c e is a target for delta-reduction, - and the given definition is the one to be expanded. */ -optional old_type_context::is_delta(expr const & e) { - expr const & f = get_app_fn(e); - if (is_constant(f)) { - return is_transparent(const_name(f)); - } else { - return none_declaration(); - } -} - -/** \brief Weak head normal form core procedure that performs delta reduction - for non-opaque constants with definitional height greater than or equal to \c h. - - This method is based on whnf_core(expr const &) and \c unfold_names. - \remark This method does not use normalization extensions attached in the environment. -*/ -expr old_type_context::whnf_core(expr e, unsigned h) { - while (true) { - expr new_e = unfold_names(whnf_core(e), h); - if (is_eqp(e, new_e)) - return e; - e = new_e; - } -} - -/** \brief Put expression \c t in weak head normal form */ -expr old_type_context::whnf(expr const & e) { - // Do not cache easy cases - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: - return e; - case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: - case expr_kind::Let: - break; - } - - expr t = e; - while (true) { - expr t1 = whnf_core(t, 0); - if (auto new_t = norm_ext(t1)) { - t = *new_t; - } else { - return t1; - } - } -} - -expr old_type_context::try_to_pi(expr const & e) { - expr new_e = whnf(e); - if (is_pi(new_e)) - return new_e; - else - return e; -} - -expr old_type_context::relaxed_whnf(expr const & e) { - flet relax(m_relax_is_opaque, true); - return whnf(e); -} - -expr old_type_context::relaxed_try_to_pi(expr const & e) { - flet relax(m_relax_is_opaque, true); - return try_to_pi(e); -} - -bool old_type_context::relaxed_assign(expr const & ma, expr const & v) { - flet relax(m_relax_is_opaque, true); - return assign(ma, v); -} - -bool old_type_context::relaxed_force_assign(expr const & ma, expr const & v) { - flet relax(m_relax_is_opaque, true); - return force_assign(ma, v); -} - -bool old_type_context::relaxed_is_def_eq(expr const & e1, expr const & e2) { - flet relax(m_relax_is_opaque, true); - return is_def_eq(e1, e2); -} - -static bool is_max_like(level const & l) { - return is_max(l) || is_imax(l); -} - -lbool old_type_context::quick_is_def_eq(level const & l1, level const & l2) { - if (is_equivalent(l1, l2)) { - return l_true; - } - - if (is_uvar(l1)) { - if (auto v = get_assignment(l1)) { - return quick_is_def_eq(*v, l2); - } else { - update_assignment(l1, l2); - return l_true; - } - } - - if (is_uvar(l2)) { - if (auto v = get_assignment(l2)) { - return quick_is_def_eq(l1, *v); - } else { - update_assignment(l2, l1); - return l_true; - } - } - - // postpone constraint if l1 or l2 is max, imax or meta. - if (is_max_like(l1) || is_max_like(l2) || is_meta(l1) || is_meta(l2)) - return l_undef; - - if (l1.kind() == l2.kind()) { - switch (l1.kind()) { - case level_kind::Succ: - return quick_is_def_eq(succ_of(l1), succ_of(l2)); - case level_kind::Param: case level_kind::Global: - return l_false; - case level_kind::Max: case level_kind::IMax: - case level_kind::Zero: case level_kind::Meta: - lean_unreachable(); - } - lean_unreachable(); - } else { - return l_false; - } -} - -bool old_type_context::full_is_def_eq(level const & l1, level const & l2) { - if (is_equivalent(l1, l2)) { - return true; - } - - if (is_uvar(l1)) { - if (auto v = get_assignment(l1)) { - return full_is_def_eq(*v, l2); - } else { - update_assignment(l1, l2); - return true; - } - } - - if (is_uvar(l2)) { - if (auto v = get_assignment(l2)) { - return full_is_def_eq(l1, *v); - } else { - update_assignment(l2, l1); - return true; - } - } - - level new_l1 = normalize(instantiate_uvars(l1)); - level new_l2 = normalize(instantiate_uvars(l2)); - - if (ignore_universe_def_eq(new_l1, new_l2)) - return true; - - if (l1 != new_l1 || l2 != new_l2) - return full_is_def_eq(new_l1, new_l2); - - if (l1.kind() != l2.kind()) - return false; - - switch (l1.kind()) { - case level_kind::Max: - return - full_is_def_eq(max_lhs(l1), max_lhs(l2)) && - full_is_def_eq(max_rhs(l1), max_rhs(l2)); - case level_kind::IMax: - return - full_is_def_eq(imax_lhs(l1), imax_lhs(l2)) && - full_is_def_eq(imax_rhs(l1), imax_rhs(l2)); - case level_kind::Succ: - return full_is_def_eq(succ_of(l1), succ_of(l2)); - case level_kind::Param: - case level_kind::Global: - return false; - case level_kind::Zero: - case level_kind::Meta: - lean_unreachable(); - } - lean_unreachable(); -} - -bool old_type_context::is_def_eq(level const & l1, level const & l2) { - auto r = quick_is_def_eq(l1, l2); - if (r == l_undef) { - m_postponed.emplace_back(l1, l2); - return true; - } else { - return r == l_true; - } -} - -bool old_type_context::is_def_eq(levels const & ls1, levels const & ls2) { - if (is_nil(ls1) && is_nil(ls2)) { - return true; - } else if (!is_nil(ls1) && !is_nil(ls2)) { - return - is_def_eq(head(ls1), head(ls2)) && - is_def_eq(tail(ls1), tail(ls2)); - } else { - return false; - } -} - -/** \brief Given \c e of the form ?m t_1 ... t_n, where - ?m is an assigned mvar, substitute \c ?m with its assignment. */ -expr old_type_context::subst_mvar(expr const & e) { - buffer args; - expr const & m = get_app_rev_args(e, args); - lean_assert(is_mvar(m)); - optional v = get_assignment(m); - lean_assert(v); - return apply_beta(*v, args.size(), args.data()); -} - -bool old_type_context::has_assigned_uvar(level const & l) const { - if (!has_meta(l)) - return false; - bool found = false; - for_each(l, [&](level const & l) { - if (!has_meta(l)) - return false; // stop search - if (found) - return false; // stop search - if (is_uvar(l) && is_assigned(l)) { - found = true; - return false; // stop search - } - return true; // continue search - }); - return found; -} - -bool old_type_context::has_assigned_uvar(levels const & ls) const { - for (level const & l : ls) { - if (has_assigned_uvar(l)) - return true; - } - return false; -} - -bool old_type_context::has_assigned_uvar_mvar(expr const & e) const { - if (!has_expr_metavar(e) && !has_univ_metavar(e)) - return false; - bool found = false; - for_each(e, [&](expr const & e, unsigned) { - if (!has_expr_metavar(e) && !has_univ_metavar(e)) - return false; // stop search - if (found) - return false; // stop search - if ((is_mvar(e) && is_assigned(e)) || - (is_constant(e) && has_assigned_uvar(const_levels(e))) || - (is_sort(e) && has_assigned_uvar(sort_level(e)))) { - found = true; - return false; // stop search - } - return true; // continue search - }); - return found; -} - -level old_type_context::instantiate_uvars(level const & l) { - if (!has_assigned_uvar(l)) - return l; - return replace(l, [&](level const & l) { - if (!has_meta(l)) { - return some_level(l); - } else if (is_uvar(l)) { - if (auto v1 = get_assignment(l)) { - level v2 = instantiate_uvars(*v1); - if (*v1 != v2) { - update_assignment(l, v2); - return some_level(v2); - } else { - return some_level(*v1); - } - } - } - return none_level(); - }); -} - -struct instantiate_uvars_mvars_fn : public replace_visitor { - old_type_context & m_owner; - - level visit_level(level const & l) { - return m_owner.instantiate_uvars(l); - } - - levels visit_levels(levels const & ls) { - return map_reuse(ls, - [&](level const & l) { return visit_level(l); }, - [](level const & l1, level const & l2) { return is_eqp(l1, l2); }); - } - - virtual expr visit_sort(expr const & s) override { - return update_sort(s, visit_level(sort_level(s))); - } - - virtual expr visit_constant(expr const & c) override { - return update_constant(c, visit_levels(const_levels(c))); - } - - virtual expr visit_local(expr const & e) override { - return update_mlocal(e, visit(mlocal_type(e))); - } - - virtual expr visit_meta(expr const & m) override { - if (m_owner.is_mvar(m)) { - if (auto v1 = m_owner.get_assignment(m)) { - if (!has_expr_metavar(*v1)) { - return *v1; - } else { - expr v2 = m_owner.instantiate_uvars_mvars(*v1); - if (v2 != *v1) - m_owner.update_assignment(m, v2); - return v2; - } - } else { - return m; - } - } else { - return m; - } - } - - virtual expr visit_app(expr const & e) override { - buffer args; - expr const & f = get_app_rev_args(e, args); - if (m_owner.is_mvar(f)) { - if (auto v = m_owner.get_assignment(f)) { - expr new_app = apply_beta(*v, args.size(), args.data()); - if (has_expr_metavar(new_app)) - return visit(new_app); - else - return new_app; - } - } - expr new_f = visit(f); - buffer new_args; - bool modified = !is_eqp(new_f, f); - for (expr const & arg : args) { - expr new_arg = visit(arg); - if (!is_eqp(arg, new_arg)) - modified = true; - new_args.push_back(new_arg); - } - if (!modified) - return e; - else - return mk_rev_app(new_f, new_args, e.get_tag()); - } - - virtual expr visit_macro(expr const & e) override { - lean_assert(is_macro(e)); - buffer new_args; - for (unsigned i = 0; i < macro_num_args(e); i++) - new_args.push_back(visit(macro_arg(e, i))); - return update_macro(e, new_args.size(), new_args.data()); - } - - virtual expr visit(expr const & e) override { - if (!has_expr_metavar(e) && !has_univ_metavar(e)) - return e; - else - return replace_visitor::visit(e); - } - -public: - instantiate_uvars_mvars_fn(old_type_context & o):m_owner(o) {} - - expr operator()(expr const & e) { return visit(e); } -}; - -expr old_type_context::instantiate_uvars_mvars(expr const & e) { - if (!has_assigned_uvar_mvar(e)) - return e; - else - return instantiate_uvars_mvars_fn(*this)(e); -} - -bool old_type_context::is_prop(expr const & e) { - if (m_env.impredicative()) { - expr t = whnf(infer(e)); - return t == mk_Prop(); - } else { - return false; - } -} - -bool old_type_context::is_def_eq_binding(expr e1, expr e2) { - lean_assert(e1.kind() == e2.kind()); - lean_assert(is_binding(e1)); - expr_kind k = e1.kind(); - buffer subst; - do { - optional var_e1_type; - if (binding_domain(e1) != binding_domain(e2)) { - var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); - expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data()); - if (!is_def_eq_core(var_e2_type, *var_e1_type)) - return false; - } - if (!closed(binding_body(e1)) || !closed(binding_body(e2))) { - // local is used inside t or s - if (!var_e1_type) - var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); - subst.push_back(mk_internal_local(binding_name(e1), *var_e1_type)); - } else { - expr const & dont_care = mk_Prop(); - subst.push_back(dont_care); - } - e1 = binding_body(e1); - e2 = binding_body(e2); - } while (e1.kind() == k && e2.kind() == k); - return is_def_eq_core(instantiate_rev(e1, subst.size(), subst.data()), - instantiate_rev(e2, subst.size(), subst.data())); -} - -bool old_type_context::is_def_eq_args(expr const & e1, expr const & e2) { - lean_assert(is_app(e1) && is_app(e2)); - buffer args1, args2; - get_app_args(e1, args1); - get_app_args(e2, args2); - if (args1.size() != args2.size()) - return false; - for (unsigned i = 0; i < args1.size(); i++) { - if (!is_def_eq_core(args1[i], args2[i])) - return false; - } - return true; -} - -/** \brief Try to solve e1 := (lambda x : A, t) =?= e2 by eta-expanding e2. - - \remark eta-reduction is not a good alternative (even in a system without cumulativity like Lean). - Example: - (lambda x : A, f ?M) =?= f - The lhs cannot be eta-reduced because ?M is a meta-variable. */ -bool old_type_context::is_def_eq_eta(expr const & e1, expr const & e2) { - if (is_lambda(e1) && !is_lambda(e2)) { - expr e2_type = relaxed_whnf(infer(e2)); - if (is_pi(e2_type)) { - // e2_type may not be a Pi because it is a stuck term. - // We are ignoring this case and just failing. - expr new_e2 = mk_lambda(binding_name(e2_type), binding_domain(e2_type), - mk_app(e2, Var(0)), binding_info(e2_type)); - scope s(*this); - if (is_def_eq_core(e1, new_e2)) { - s.commit(); - return true; - } - } - } - return false; -} - -bool old_type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) { - if (!m_env.prop_proof_irrel()) - return false; - expr e1_type = infer(e1); - if (is_prop(e1_type)) { - expr e2_type = infer(e2); - scope s(*this); - if (is_def_eq_core(e1_type, e2_type)) { - s.commit(); - return true; - } - } - return false; -} - -bool old_type_context::validate_assignment_types(expr const & m, expr const & v) { - return is_def_eq_core(infer_metavar(m), infer(v)); -} - -/** \brief Given \c ma of the form ?m t_1 ... t_n, (try to) assign - ?m to (an abstraction of) v. Return true if success and false otherwise. */ -bool old_type_context::process_assignment_core(expr const & ma, expr const & v) { - buffer args; - expr const & m = get_app_args(ma, args); - buffer locals; - for (expr & arg : args) { - expr new_arg = arg; - // try to instantiate - if (is_meta(new_arg)) - new_arg = instantiate_uvars_mvars(arg); - if (!is_local(new_arg)) - break; // it is not local - arg = new_arg; - lean_assert(is_local(arg)); - if (std::any_of(locals.begin(), locals.end(), [&](expr const & local) { - return mlocal_name(local) == mlocal_name(arg); })) - break; // duplicate local - locals.push_back(arg); - } - lean_assert(is_mvar(m)); - expr new_v = instantiate_uvars_mvars(v); - - if (!validate_assignment(m, locals, v)) - return false; - - if (m_check_types) { - try { - scope s(*this); - expr t1 = infer(ma); - expr t2 = infer(v); - flet ignore_ext_mvar(m_ignore_external_mvars, true); - if (!is_def_eq_core(t1, t2)) - return false; - s.commit(); - } catch (exception &) { - // We may fail to infer the type of ma or v because the type may contain meta-variables. - // Example: ma may be of the form (?m a), and the type of ?m may be ?M where ?M is a - // (external) metavariable created by the unifier. - // We believe this only happens when we are interacting with the elaborator. - } - } - - if (args.empty()) { - // easy case - } else if (args.size() == locals.size()) { - new_v = Fun(locals, new_v); - } else { - // This case is imprecise since it is not a higher order pattern. - // That the term \c ma is of the form (?m t_1 ... t_n) and the t_i's are not pairwise - // distinct local constants. - expr m_type = infer_metavar(m); - for (unsigned i = 0; i < args.size(); i++) { - m_type = whnf(m_type); - if (!is_pi(m_type)) - return false; - lean_assert(i <= locals.size()); - if (i == locals.size()) - locals.push_back(mk_internal_local_from_binding(m_type)); - lean_assert(i < locals.size()); - m_type = instantiate(binding_body(m_type), locals[i]); - } - lean_assert(locals.size() == args.size()); - new_v = Fun(locals, new_v); - } - update_assignment(m, new_v); - return validate_assignment_types(m, new_v); -} - -bool old_type_context::process_assignment(expr const & ma, expr const & v) { - scope s(*this); - unsigned psz = m_postponed.size(); - if (!process_assignment_core(ma, v)) { - return false; - } - if (process_postponed(psz)) { - m_postponed.resize(psz); - s.commit(); - return true; - } - return false; -} - -bool old_type_context::assign(expr const & ma, expr const & v) { - expr const & f = get_app_fn(ma); - if (is_assigned(f)) { - return is_def_eq(ma, v); - } else { - return process_assignment(ma, v); - } -} - -bool old_type_context::force_assign(expr const & ma, expr const & v) { - return process_assignment(ma, v); -} - -/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */ -lbool old_type_context::quick_is_def_eq(expr const & e1, expr const & e2) { - if (e1 == e2) - return l_true; - - expr const & f1 = get_app_fn(e1); - if (is_mvar(f1)) { - if (is_assigned(f1)) { - return to_lbool(is_def_eq_core(subst_mvar(e1), e2)); - } else { - return to_lbool(process_assignment_core(e1, e2)); - } - } - - expr const & f2 = get_app_fn(e2); - if (is_mvar(f2)) { - if (is_assigned(f2)) { - return to_lbool(is_def_eq_core(e1, subst_mvar(e2))); - } else { - return to_lbool(process_assignment_core(e2, e1)); - } - } - - if (m_ignore_external_mvars && (is_meta(e1) || is_meta(e2))) - return l_true; - - if (e1.kind() == e2.kind()) { - switch (e1.kind()) { - case expr_kind::Lambda: case expr_kind::Pi: - return to_lbool(is_def_eq_binding(e1, e2)); - case expr_kind::Sort: - return to_lbool(is_def_eq(sort_level(e1), sort_level(e2))); - case expr_kind::Meta: case expr_kind::Var: - case expr_kind::Local: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Macro: - case expr_kind::Let: - // We do not handle these cases in this method. - break; - } - } - return l_undef; // This is not an "easy case" -} - -auto old_type_context::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status { - auto d_t = is_delta(t_n); - auto d_s = is_delta(s_n); - if (!d_t && !d_s) { - return reduction_status::DefUnknown; - } else if (d_t && !d_s) { - t_n = whnf_core(unfold_names(t_n, 0)); - } else if (!d_t && d_s) { - s_n = whnf_core(unfold_names(s_n, 0)); - } else { - int c = compare(d_t->get_hints(), d_s->get_hints()); - if (c < 0) { - t_n = whnf_core(unfold_names(t_n, d_t->get_hints().get_height())); - } else if (c > 0) { - s_n = whnf_core(unfold_names(s_n, d_s->get_hints().get_height())); - } else { - if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { - if (!is_opaque(*d_t)) { - scope s(*this); - if (is_def_eq_args(t_n, s_n) && - is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)))) { - s.commit(); - return reduction_status::DefEqual; - } - } - } - t_n = whnf_core(unfold_names(t_n, d_t->get_hints().get_height() - 1)); - s_n = whnf_core(unfold_names(s_n, d_s->get_hints().get_height() - 1)); - } - } - switch (quick_is_def_eq(t_n, s_n)) { - case l_true: return reduction_status::DefEqual; - case l_false: return reduction_status::DefDiff; - case l_undef: return reduction_status::Continue; - } - lean_unreachable(); -} - -lbool old_type_context::lazy_delta_reduction(expr & t_n, expr & s_n) { - while (true) { - switch (lazy_delta_reduction_step(t_n, s_n)) { - case reduction_status::Continue: break; - case reduction_status::DefUnknown: return l_undef; - case reduction_status::DefEqual: return l_true; - case reduction_status::DefDiff: return l_false; - } - } -} - -auto old_type_context::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status { - auto new_t_n = norm_ext(t_n); - auto new_s_n = norm_ext(s_n); - if (!new_t_n && !new_s_n) - return reduction_status::DefUnknown; - if (new_t_n) - t_n = whnf_core(*new_t_n); - if (new_s_n) - s_n = whnf_core(*new_s_n); - switch (quick_is_def_eq(t_n, s_n)) { - case l_true: return reduction_status::DefEqual; - case l_false: return reduction_status::DefDiff; - case l_undef: return reduction_status::Continue; - } - lean_unreachable(); -} - -// Apply lazy delta-reduction and then normalizer extensions -lbool old_type_context::reduce_def_eq(expr & t_n, expr & s_n) { - while (true) { - // first, keep applying lazy delta-reduction while applicable - lbool r = lazy_delta_reduction(t_n, s_n); - if (r != l_undef) return r; - - // try normalizer extensions - switch (ext_reduction_step(t_n, s_n)) { - case reduction_status::Continue: break; - case reduction_status::DefUnknown: return l_undef; - case reduction_status::DefEqual: return l_true; - case reduction_status::DefDiff: return l_false; - } - } -} - -bool old_type_context::is_def_eq_core(expr const & t, expr const & s) { - check_system("is_definitionally_equal"); - lbool r = quick_is_def_eq(t, s); - if (r != l_undef) return r == l_true; - - expr t_n = whnf_core(t); - expr s_n = whnf_core(s); - - if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { - r = quick_is_def_eq(t_n, s_n); - if (r != l_undef) return r == l_true; - } - - r = reduce_def_eq(t_n, s_n); - if (r != l_undef) return r == l_true; - - if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n)) { - scope s(*this); - if (is_def_eq(const_levels(t_n), const_levels(s_n))) { - s.commit(); - return true; - } - } - - if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n)) - return true; - - if (is_app(t_n) && is_app(s_n)) { - scope s(*this); - if (is_def_eq_args(t_n, s_n) && - is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n))) { - s.commit(); - return true; - } - } - - if (is_def_eq_eta(t_n, s_n)) - return true; - if (is_def_eq_eta(s_n, t_n)) - return true; - - if (is_def_eq_proof_irrel(t_n, s_n)) - return true; - - return on_is_def_eq_failure(t_n, s_n); -} - -bool old_type_context::process_postponed(unsigned old_sz) { - if (m_postponed.size() == old_sz) - return true; // no new universe constraints. - lean_assert(m_postponed.size() > old_sz); - buffer> b1, b2; - b1.append(m_postponed.size() - old_sz, m_postponed.data() + old_sz); - buffer> * curr, * next; - curr = &b1; - next = &b2; - while (true) { - for (auto p : *curr) { - auto r = quick_is_def_eq(p.first, p.second); - if (r == l_undef) { - next->push_back(p); - } else if (r == l_false) { - return false; - } - } - if (next->empty()) { - return true; // all constraints have been processed - } else if (next->size() < curr->size()) { - // easy constraints have been processed in this iteration - curr->clear(); - std::swap(next, curr); - lean_assert(next->empty()); - } else { - // use full (and approximate) is_def_eq to process the first constraint - // in next. - auto p = (*next)[0]; - if (!full_is_def_eq(p.first, p.second)) - return false; - if (next->size() == 1) - return true; // the last constraint has been solved. - curr->clear(); - curr->append(next->size() - 1, next->data() + 1); - next->clear(); - } - } -} - -bool old_type_context::is_def_eq(expr const & e1, expr const & e2) { - scope s(*this); - flet in_is_def_eq(m_in_is_def_eq, true); - unsigned psz = m_postponed.size(); - if (!is_def_eq_core(e1, e2)) { - return false; - } - if (process_postponed(psz)) { - m_postponed.resize(psz); - s.commit(); - return true; - } - return false; -} - -expr old_type_context::infer_constant(expr const & e) { - declaration d = m_env.get(const_name(e)); - auto const & ps = d.get_univ_params(); - auto const & ls = const_levels(e); - if (length(ps) != length(ls)) - throw exception("infer type failed, incorrect number of universe levels"); - return instantiate_type_univ_params(d, ls); -} - -expr old_type_context::infer_macro(expr const & e) { - auto def = macro_def(e); - bool infer_only = true; - return def.check_type(e, *this, infer_only); -} - -expr old_type_context::infer_lambda(expr e) { - buffer es, ds, ls; - while (is_lambda(e)) { - es.push_back(e); - ds.push_back(binding_domain(e)); - expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); - expr l = mk_internal_local(binding_name(e), d, binding_info(e)); - ls.push_back(l); - e = binding_body(e); - } - check_system("infer_type"); - expr t = infer(instantiate_rev(e, ls.size(), ls.data())); - expr r = abstract_locals(t, ls.size(), ls.data()); - unsigned i = es.size(); - while (i > 0) { - --i; - r = mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i])); - } - return r; -} - -optional old_type_context::get_level_core(expr const & A) { - expr A_type = relaxed_whnf(infer(A)); - while (true) { - if (is_sort(A_type)) { - return some_level(sort_level(A_type)); - } else if (is_mvar(A_type)) { - if (auto v = get_assignment(A_type)) { - A_type = *v; - } else { - level r = mk_uvar(); - update_assignment(A_type, mk_sort(r)); - return some_level(r); - } - } else { - return none_level(); - } - } -} - -level old_type_context::get_level(expr const & A) { - if (auto r = get_level_core(A)) { - return *r; - } else { - throw exception("infer type failed, sort expected"); - } -} - -expr old_type_context::infer_pi(expr const & e0) { - buffer ls; - buffer us; - expr e = e0; - while (is_pi(e)) { - expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); - us.push_back(get_level(d)); - expr l = mk_internal_local(d, binding_info(e)); - ls.push_back(l); - e = binding_body(e); - } - e = instantiate_rev(e, ls.size(), ls.data()); - level r = get_level(e); - unsigned i = ls.size(); - bool imp = m_env.impredicative(); - while (i > 0) { - --i; - r = imp ? mk_imax(us[i], r) : mk_max(us[i], r); - } - return mk_sort(r); -} - -/** \brief Make sure \c e is a Pi-expression, if it is not throw an exception using \c ref as a reference */ -void old_type_context::ensure_pi(expr const & e, expr const & /* ref */) { - // Remark: for simplicity reasons, we just fail if \c e is not a Pi. - if (!is_pi(e)) - throw exception("infer type failed, Pi expected"); - // Potential problem: e is of the form (f ...) where f is a constant that is not marked as reducible. - // So, whnf does not reduce it, and we fail to detect that e is can be reduced to a Pi-expression. -} - -expr old_type_context::infer_app(expr const & e) { - check_system("infer_type"); - buffer args; - expr const & f = get_app_args(e, args); - expr f_type = infer(f); - unsigned j = 0; - unsigned nargs = args.size(); - for (unsigned i = 0; i < nargs; i++) { - if (is_pi(f_type)) { - f_type = binding_body(f_type); - } else { - f_type = relaxed_whnf(instantiate_rev(f_type, i-j, args.data()+j)); - ensure_pi(f_type, e); - f_type = binding_body(f_type); - j = i; - } - } - return instantiate_rev(f_type, nargs-j, args.data()+j); -} - -expr old_type_context::infer(expr const & e) { - lean_assert(!is_var(e)); - lean_assert(closed(e)); - auto it = m_infer_cache.find(e); - if (it != m_infer_cache.end()) - return it->second; - expr r; - switch (e.kind()) { - case expr_kind::Local: - r = infer_local(e); - break; - case expr_kind::Meta: - r = infer_metavar(e); - break; - case expr_kind::Var: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Sort: - r = mk_sort(mk_succ(sort_level(e))); - break; - case expr_kind::Constant: - r = infer_constant(e); - break; - case expr_kind::Macro: - r = infer_macro(e); - break; - case expr_kind::Lambda: - r = infer_lambda(e); - break; - case expr_kind::Pi: - r = infer_pi(e); - break; - case expr_kind::App: - r = infer_app(e); - break; - case expr_kind::Let: - r = infer(instantiate(let_body(e), let_value(e))); - break; - } - m_infer_cache.insert(mk_pair(e, r)); - return r; -} - -void old_type_context::clear_cache() { - m_ci_cache.clear(); - m_ss_cache.clear(); - m_is_transparent_cache[0].clear(); - m_is_transparent_cache[1].clear(); - clear_infer_cache(); -} - -void old_type_context::clear_infer_cache() { - m_infer_cache.clear(); -} - -/** \brief If the constant \c e is a class, return its name */ -optional old_type_context::constant_is_class(expr const & e) { - name const & cls_name = const_name(e); - if (lean::is_class(m_env, cls_name)) { - return optional(cls_name); - } else { - return optional(); - } -} - -optional old_type_context::is_full_class(expr type) { - type = whnf(type); - if (is_pi(type)) { - return is_full_class(instantiate(binding_body(type), mk_internal_local_from_binding(type))); - } else { - expr f = get_app_fn(type); - if (!is_constant(f)) - return optional(); - return constant_is_class(f); - } -} - -/** \brief Partial/Quick test for is_class. Result - l_true: \c type is a class, and the name of the class is stored in \c result. - l_false: \c type is not a class. - l_undef: procedure did not establish whether \c type is a class or not. -*/ -lbool old_type_context::is_quick_class(expr const & type, name & result) { - expr const * it = &type; - while (true) { - switch (it->kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Lambda: case expr_kind::Let: - return l_false; - case expr_kind::Macro: - return l_undef; - case expr_kind::Constant: - if (auto r = constant_is_class(*it)) { - result = *r; - return l_true; - } else if (is_extra_opaque(const_name(*it))) { - return l_false; - } else { - return l_undef; - } - case expr_kind::App: { - expr const & f = get_app_fn(*it); - if (is_constant(f)) { - if (auto r = constant_is_class(f)) { - result = *r; - return l_true; - } else if (is_extra_opaque(const_name(f))) { - return l_false; - } else { - return l_undef; - } - } else if (is_lambda(f) || is_macro(f)) { - return l_undef; - } else { - return l_false; - } - } - case expr_kind::Pi: - it = &binding_body(*it); - break; - } - } -} - -/** \brief Return true iff \c type is a class or Pi that produces a class. */ -optional old_type_context::is_class(expr const & type) { - name result; - switch (is_quick_class(type, result)) { - case l_true: return optional(result); - case l_false: return optional(); - case l_undef: break; - } - return is_full_class(type); -} - -bool old_type_context::compatible_local_instances(list const & ctx) { - unsigned i = 0; - for (expr const & e : ctx) { - // Remark: we use infer_type(e) instead of mlocal_type because we want to allow - // customers (e.g., blast) of this class to store the type of local constants - // in a different place. - if (auto cname = is_class(infer(e))) { - if (i == m_ci_local_instances.size()) - return false; // ctx has more local instances than m_ci_local_instances - if (e != m_ci_local_instances[i].second) - return false; // local instance in ctx is not compatible with one at m_ci_local_instances - i++; - } - } - return i == m_ci_local_instances.size(); -} - -// Helper function for find_unsynth_metavar -static bool has_meta_arg(expr e) { - if (!has_expr_metavar(e)) - return false; - while (is_app(e)) { - if (is_meta(app_arg(e))) - return true; - e = app_fn(e); - } - return false; -} - -/** IF \c e is of the form (f ... (?m t_1 ... t_n) ...) where ?m is an unassigned - metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized - by type class resolution, then we return ?m. - Otherwise, we return none */ -optional> old_type_context::find_unsynth_metavar_at_args(expr const & e) { - if (!has_meta_arg(e)) - return optional>(); - buffer args; - expr const & fn = get_app_args(e, args); - expr type = infer(fn); - unsigned i = 0; - while (i < args.size()) { - type = whnf(type); - if (!is_pi(type)) - return optional>(); - expr const & arg = args[i]; - if (binding_info(type).is_inst_implicit() && is_meta(arg)) { - expr const & m = get_app_fn(arg); - if (is_mvar(m)) { - expr m_type = instantiate_uvars_mvars(infer(m)); - if (!has_expr_metavar_relaxed(m_type)) { - return some(mk_pair(m, m_type)); - } - } - } - type = instantiate(binding_body(type), arg); - i++; - } - return optional>(); -} - -/** Search in \c e for an expression of the form (f ... (?m t_1 ... t_n) ...) where ?m is an unassigned - metavariable whose type is a type class, and (?m t_1 ... t_n) must be synthesized - by type class resolution, then we return ?m. - Otherwise, we return none. - This procedure goes inside lambdas. */ -optional> old_type_context::find_unsynth_metavar(expr const & e) { - if (!has_expr_metavar(e)) - return optional>(); - if (is_app(e)) { - if (auto r = find_unsynth_metavar_at_args(e)) - return r; - expr it = e; - while (is_app(it)) { - if (auto r = find_unsynth_metavar(app_arg(it))) - return r; - it = app_fn(it); - } - return optional>(); - } else if (is_lambda(e)) { - expr l = mk_tmp_local_from_binding(e); - return find_unsynth_metavar(instantiate(binding_body(e), l)); - } else { - return optional>(); - } -} - -bool old_type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) { - if (is_app(e1)) { - if (auto p1 = find_unsynth_metavar(e1)) { - if (mk_nested_instance(p1->first, p1->second)) { - return is_def_eq_core(instantiate_uvars_mvars(e1), e2); - } - } - } - if (is_app(e2)) { - if (auto p2 = find_unsynth_metavar(e2)) { - if (mk_nested_instance(p2->first, p2->second)) { - return is_def_eq_core(e1, instantiate_uvars_mvars(e2)); - } - } - } - if (try_unification_hints(e1, e2)) { - return true; - } - return false; -} - -struct old_type_context::unification_hint_fn { - old_type_context & m_owner; - unification_hint m_hint; - buffer > m_assignment; - - unification_hint_fn(old_type_context & o, unification_hint const & hint): - m_owner(o), m_hint(hint) { m_assignment.resize(m_hint.get_num_vars()); } - - bool syntactic_match(expr const & pattern, expr const & e) { - unsigned idx; - switch (pattern.kind()) { - case expr_kind::Var: - idx = var_idx(pattern); - if (!m_assignment[idx]) { - m_assignment[idx] = some_expr(e); - return true; - } else { - return m_owner.is_def_eq(*m_assignment[idx], e); - } - case expr_kind::Constant: - return is_constant(e) && const_name(pattern) == const_name(e) - && m_owner.is_def_eq(const_levels(pattern), const_levels(e)); - case expr_kind::Sort: - return is_sort(e) && m_owner.is_def_eq(sort_level(pattern), sort_level(e)); - case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::Let: - // Remark: we do not traverse inside of binders. - return pattern == e; - case expr_kind::App: - return is_app(e) && syntactic_match(app_fn(pattern), app_fn(e)) && syntactic_match(app_arg(pattern), app_arg(e)); - case expr_kind::Local: case expr_kind::Meta: - break; - } - lean_unreachable(); - } - - bool operator()(expr const & lhs, expr const & rhs) { - if (!syntactic_match(m_hint.get_lhs(), lhs)) { - lean_trace(name({"old_type_context", "unification_hint"}), tout() << "LHS does not match\n";); - return false; - } else if (!syntactic_match(m_hint.get_rhs(), rhs)) { - lean_trace(name({"old_type_context", "unification_hint"}), tout() << "RHS does not match\n";); - return false; - } else { - auto instantiate_assignment_fn = [&](expr const & e, unsigned offset) { - if (is_var(e)) { - unsigned idx = var_idx(e) + offset; - if (idx < m_assignment.size()) { - lean_assert(m_assignment[idx]); - return m_assignment[idx]; - } - } - return none_expr(); - }; - buffer constraints; - to_buffer(m_hint.get_constraints(), constraints); - for (expr_pair const & p : constraints) { - expr new_lhs = replace(p.first, instantiate_assignment_fn); - expr new_rhs = replace(p.second, instantiate_assignment_fn); - expr new_lhs_inst = m_owner.instantiate_uvars_mvars(new_lhs); - expr new_rhs_inst = m_owner.instantiate_uvars_mvars(new_rhs); - bool success = m_owner.is_def_eq(new_lhs, new_rhs); - lean_trace(name({"old_type_context", "unification_hint"}), - tout() << new_lhs_inst << " =?= " << new_rhs_inst << "..." - << (success ? "success" : "failed") << "\n";); - if (!success) return false; - } - lean_trace(name({"old_type_context", "unification_hint"}), tout() << "hint successfully applied\n";); - return true; - } - } -}; - -bool old_type_context::try_unification_hints(expr const & e1, expr const & e2) { - expr e1_fn = get_app_fn(e1); - expr e2_fn = get_app_fn(e2); - if (is_constant(e1_fn) && is_constant(e2_fn)) { - buffer hints; - get_unification_hints(m_env, const_name(e1_fn), const_name(e2_fn), hints); - for (unification_hint const & hint : hints) { - scope s(*this); - lean_trace(name({"old_type_context", "unification_hint"}), - tout() << e1 << " =?= " << e2 - << ", pattern: " << hint.get_lhs() << " =?= " << hint.get_rhs() << "\n";); - if (unification_hint_fn(*this, hint)(e1, e2)) { - s.commit(); - return true; - } - } - } - return false; -} - -bool old_type_context::validate_assignment(expr const & m, buffer const & locals, expr const & v) { - // Basic check: m does not occur in v - bool ok = true; - for_each(v, [&](expr const & e, unsigned) { - if (!ok) - return false; // stop search - if (is_mvar(e)) { - if (m == e) { - ok = false; // failed 2 - return false; - } - return false; - } - if (is_internal_local(e)) { - if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { - return mlocal_name(a) != mlocal_name(e); })) { - ok = false; // failed 3 - return false; - } - } - return true; - }); - return ok; -} - -bool old_type_context::update_options(options const & opts) { - options o = opts; - unsigned max_depth = get_class_instance_max_depth(o); - bool trans_instances = get_class_trans_instances(o); - bool r = true; - if (m_ci_max_depth != max_depth || - m_ci_trans_instances != trans_instances) { - r = false; - } - m_ci_max_depth = max_depth; - m_ci_trans_instances = trans_instances; - return r; -} - -[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw generic_exception(m, msg); } - -void old_type_context::trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r) { - auto out = tout(); - if (!m_ci_displayed_trace_header && m_ci_choices.size() == m_ci_choices_ini_sz + 1) { - out << tclass("class_instances"); - if (m_pip) { - if (auto fname = m_pip->get_file_name()) { - out << fname << ":"; - } - if (m_ci_pos) - out << m_ci_pos->first << ":" << m_ci_pos->second << ":"; - } - out << " class-instance resolution trace" << endl; - m_ci_displayed_trace_header = true; - } - out << tclass("class_instances") << "(" << depth << ") "; - out << mvar << " : " << instantiate_uvars_mvars(mvar_type) << " := " << r << endl; -} - -// Try to synthesize e.m_mvar using instance inst : inst_type. -// trans_inst is true if inst is a transitive instance. -bool old_type_context::try_instance(ci_stack_entry const & e, expr const & inst, expr const & inst_type, bool trans_inst) { - try { - buffer locals; - expr const & mvar = e.m_mvar; - expr mvar_type = mlocal_type(mvar); - while (true) { - mvar_type = whnf(mvar_type); - if (!is_pi(mvar_type)) - break; - expr local = mk_internal_local_from_binding(mvar_type); - locals.push_back(local); - mvar_type = instantiate(binding_body(mvar_type), local); - } - expr type = inst_type; - expr r = inst; - buffer new_inst_mvars; - while (true) { - type = whnf(type); - if (!is_pi(type)) - break; - expr new_mvar = mk_mvar(Pi(locals, binding_domain(type))); - if (binding_info(type).is_inst_implicit()) { - new_inst_mvars.push_back(new_mvar); - } - expr new_arg = mk_app(new_mvar, locals); - r = mk_app(r, new_arg); - type = instantiate(binding_body(type), new_arg); - } - lean_trace_plain("class_instances", trace(e.m_depth, mk_app(mvar, locals), mvar_type, r);); - if (!is_def_eq(mvar_type, type)) { - return false; - } - r = Fun(locals, r); - // Remark: if the metavariable is already assigned, we should check whether - // the previous assignment (obtained by solving unification constraints) and the - // synthesized one are definitionally equal. We don't do that for performance reasons. - // Moreover, the is_def_eq defined here is not complete (e.g., it only unfolds reducible constants). - update_assignment(mvar, r); - // copy new_inst_mvars to stack - unsigned i = new_inst_mvars.size(); - while (i > 0) { - --i; - m_ci_state.m_stack = cons(ci_stack_entry(new_inst_mvars[i], e.m_depth+1, trans_inst), m_ci_state.m_stack); - } - return true; - } catch (exception &) { - return false; - } -} - -bool old_type_context::try_instance(ci_stack_entry const & e, name const & inst_name, bool trans_inst) { - if (auto decl = m_env.find(inst_name)) { - buffer ls_buffer; - unsigned num_univ_ps = decl->get_num_univ_params(); - for (unsigned i = 0; i < num_univ_ps; i++) - ls_buffer.push_back(mk_uvar()); - levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); - expr inst_cnst = mk_constant(inst_name, ls); - expr inst_type = instantiate_type_univ_params(*decl, ls); - return try_instance(e, inst_cnst, inst_type, trans_inst); - } else { - return false; - } -} - -list old_type_context::get_local_instances(name const & cname) { - buffer selected; - for (pair const & p : m_ci_local_instances) { - if (p.first == cname) - selected.push_back(p.second); - } - return to_list(selected); -} - -bool old_type_context::is_ci_done() const { - return empty(m_ci_state.m_stack); -} - -bool old_type_context::mk_choice_point(expr const & mvar) { - lean_assert(is_mvar(mvar)); - if (m_ci_choices.size() > m_ci_choices_ini_sz + m_ci_max_depth) { - throw_class_exception("maximum class-instance resolution depth has been reached " - "(the limit can be increased by setting option 'class.instance_max_depth') " - "(the class-instance resolution trace can be visualized " - "by setting option 'trace.class_instances')", - infer(m_ci_main_mvar)); - } - // Remark: we initially tried to reject branches where mvar_type contained unassigned metavariables. - // The idea was to make the procedure easier to understand. - // However, it turns out this is too restrictive. The group_theory folder contains the following instance. - // nsubg_setoid : Π {A : Type} [s : group A] (N : set A) [is_nsubg : @is_normal_subgroup A s N], setoid A - // When it is used, it creates a subproblem for - // is_nsubg : @is_normal_subgroup A s ?N - // where ?N is not known. Actually, we can only find the value for ?N by constructing the instance is_nsubg. - expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar)); - m_ci_choices.push_back(ci_choice()); - push(); - ci_choice & r = m_ci_choices.back(); - auto cname = is_class(mvar_type); - if (!cname) - return false; - r.m_local_instances = get_local_instances(*cname); - r.m_instances = get_class_instances(m_env, *cname); - if (empty(r.m_local_instances) && empty(r.m_trans_instances) && empty(r.m_instances)) - return false; - r.m_state = m_ci_state; - return true; -} - -bool old_type_context::process_next_alt_core(ci_stack_entry const & e, list & insts) { - while (!empty(insts)) { - expr inst = head(insts); - insts = tail(insts); - expr inst_type = infer(inst); - bool trans_inst = false; - if (try_instance(e, inst, inst_type, trans_inst)) - return true; - } - return false; -} - -bool old_type_context::process_next_alt_core(ci_stack_entry const & e, list & inst_names, bool trans_inst) { - while (!empty(inst_names)) { - name inst_name = head(inst_names); - inst_names = tail(inst_names); - if (try_instance(e, inst_name, trans_inst)) - return true; - } - return false; -} - -bool old_type_context::process_next_alt(ci_stack_entry const & e) { - lean_assert(m_ci_choices.size() > m_ci_choices_ini_sz); - lean_assert(!m_ci_choices.empty()); - std::vector & cs = m_ci_choices; - list locals = cs.back().m_local_instances; - if (process_next_alt_core(e, locals)) { - cs.back().m_local_instances = locals; - return true; - } - cs.back().m_local_instances = list(); - if (!e.m_trans_inst_subproblem) { - list trans_insts = cs.back().m_trans_instances; - if (process_next_alt_core(e, trans_insts, true)) { - cs.back().m_trans_instances = trans_insts; - return true; - } - cs.back().m_trans_instances = list(); - list insts = cs.back().m_instances; - if (process_next_alt_core(e, insts, false)) { - cs.back().m_instances = insts; - return true; - } - cs.back().m_instances = list(); - } - return false; -} - -bool old_type_context::process_next_mvar() { - lean_assert(!is_ci_done()); - ci_stack_entry e = head(m_ci_state.m_stack); - if (!mk_choice_point(e.m_mvar)) - return false; - m_ci_state.m_stack = tail(m_ci_state.m_stack); - return process_next_alt(e); -} - -bool old_type_context::backtrack() { - if (m_ci_choices.size() == m_ci_choices_ini_sz) - return false; - lean_assert(!m_ci_choices.empty()); - while (true) { - m_ci_choices.pop_back(); - pop(); - if (m_ci_choices.size() == m_ci_choices_ini_sz) - return false; - m_ci_state = m_ci_choices.back().m_state; - ci_stack_entry e = head(m_ci_state.m_stack); - m_ci_state.m_stack = tail(m_ci_state.m_stack); - if (process_next_alt(e)) - return true; - } -} - -optional old_type_context::search() { - while (!is_ci_done()) { - if (!process_next_mvar()) { - if (!backtrack()) - return none_expr(); - } - } - return some_expr(instantiate_uvars_mvars(m_ci_main_mvar)); -} - -optional old_type_context::next_solution() { - if (m_ci_choices.size() == m_ci_choices_ini_sz) - return none_expr(); - pop(); push(); // restore assignment - m_ci_state = m_ci_choices.back().m_state; - ci_stack_entry e = head(m_ci_state.m_stack); - m_ci_state.m_stack = tail(m_ci_state.m_stack); - if (process_next_alt(e)) - return search(); - else if (backtrack()) - return search(); - else - return none_expr(); -} - -void old_type_context::init_search(expr const & type) { - m_ci_state = ci_state(); - m_ci_main_mvar = mk_mvar(type); - m_ci_state.m_stack = to_list(ci_stack_entry(m_ci_main_mvar, 0)); - m_ci_choices_ini_sz = m_ci_choices.size(); -} - -void old_type_context::cache_ci_result(expr const & type, optional const & inst) { - if (!m_ci_multiple_instances) { - // We do not cache results when multiple instances have to be generated. - m_ci_cache.insert(mk_pair(type, inst)); - } -} - -optional old_type_context::ensure_no_meta(optional r) { - while (true) { - if (!r) { - cache_ci_result(mlocal_type(m_ci_main_mvar), r); - return none_expr(); - } - if (!has_expr_metavar_relaxed(*r)) { - cache_ci_result(mlocal_type(m_ci_main_mvar), r); - return r; - } - r = next_solution(); - } -} - -optional old_type_context::mk_class_instance_core(expr const & type) { - if (!m_ci_multiple_instances) { - /* We do not cache results when multiple instances have to be generated. */ - auto it = m_ci_cache.find(type); - if (it != m_ci_cache.end()) { - /* instance/failure is already cached */ - lean_trace("class_instances", - if (it->second) - tout() << "cached instance for " << type << "\n" << *(it->second) << "\n"; - else - tout() << "cached failure for " << type << "\n";); - return it->second; - } - } - init_search(type); - auto r = search(); - return ensure_no_meta(r); -} - -void old_type_context::restore_choices(unsigned old_sz) { - lean_assert(old_sz <= m_ci_choices.size()); - while (m_ci_choices.size() > old_sz) { - m_ci_choices.pop_back(); - pop(); - } - lean_assert(m_ci_choices.size() == old_sz); -} - -optional old_type_context::mk_class_instance(expr const & type) { - m_ci_choices.clear(); - ci_choices_scope scope(*this); - lean_trace_init_bool("class_instances", get_pp_purify_metavars_name(), false); - lean_trace_init_bool("class_instances", get_pp_implicit_name(), true); - m_ci_displayed_trace_header = false; - auto r = mk_class_instance_core(type); - if (r) - scope.commit(); - return r; -} - -optional old_type_context::mk_subsingleton_instance(expr const & type) { - auto it = m_ss_cache.find(type); - if (it != m_ss_cache.end()) - return it->second; - expr Type = whnf(infer(type)); - if (!is_sort(Type)) { - m_ss_cache.insert(mk_pair(type, none_expr())); - return none_expr(); - } - level lvl = sort_level(Type); - expr subsingleton; - if (is_standard(m_env)) - subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); - else - subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_prop_name(), {lvl}), type)); - auto r = mk_class_instance(subsingleton); - m_ss_cache.insert(mk_pair(type, r)); - return r; -} - -optional old_type_context::next_class_instance() { - if (!m_ci_multiple_instances) - return none_expr(); - auto r = next_solution(); - return ensure_no_meta(r); -} - -/** \brief Create a nested type class instance of the given type - \remark This method is used to resolve nested type class resolution problems. */ -optional old_type_context::mk_nested_instance(expr const & type) { - ci_choices_scope scope(*this); - flet save_choice_sz(m_ci_choices_ini_sz, m_ci_choices_ini_sz); - flet save_state(m_ci_state, ci_state()); - flet save_main_mvar(m_ci_main_mvar, expr()); - unsigned old_choices_sz = m_ci_choices.size(); - auto r = mk_class_instance_core(type); - if (r) - scope.commit(); - m_ci_choices.resize(old_choices_sz); // cut search - return r; -} - -/** \brief Create a nested type class instance of the given type, and assign it to metavariable \c m. - Return true iff the instance was successfully created. - \remark This method is used to resolve nested type class resolution problems. */ -bool old_type_context::mk_nested_instance(expr const & m, expr const & m_type) { - lean_assert(is_mvar(m)); - if (auto r = mk_nested_instance(m_type)) { - update_assignment(m, *r); - return true; - } else { - return false; - } -} - -old_type_context::scope_pos_info::scope_pos_info(old_type_context & o, pos_info_provider const * pip, expr const & pos_ref): - m_owner(o), - m_old_pip(m_owner.m_pip), - m_old_pos(m_owner.m_ci_pos) { - m_owner.m_pip = pip; - if (pip) - m_owner.m_ci_pos = pip->get_pos_info(pos_ref); -} - -old_type_context::scope_pos_info::~scope_pos_info() { - m_owner.m_pip = m_old_pip; - m_owner.m_ci_pos = m_old_pos; -} - -expr normalizer::normalize_binding(expr const & e) { - expr d = normalize(binding_domain(e)); - expr l = m_ctx.mk_tmp_local(binding_name(e), d, binding_info(e)); - expr b = abstract(normalize(instantiate(binding_body(e), l)), l); - return update_binding(e, d, b); -} - -optional normalizer::unfold_recursor_core(expr const & f, unsigned i, - buffer const & idxs, buffer & args, bool is_rec) { - if (i == idxs.size()) { - expr new_app = mk_rev_app(f, args); - if (is_rec) - return some_expr(normalize(new_app)); - else if (optional r = unfold_app(env(), new_app)) - return some_expr(normalize(*r)); - else - return none_expr(); - } else { - unsigned idx = idxs[i]; - if (idx >= args.size()) - return none_expr(); - expr & arg = args[args.size() - idx - 1]; - if (!is_constructor_app(env(), arg)) - return none_expr(); - return unfold_recursor_core(f, i+1, idxs, args, is_rec); - } -} - -optional normalizer::unfold_recursor_major(expr const & f, unsigned idx, buffer & args) { - buffer idxs; - idxs.push_back(idx); - return unfold_recursor_core(f, 0, idxs, args, true); -} - -expr normalizer::normalize_app(expr const & e) { - buffer args; - bool modified = false; - expr f = get_app_rev_args(e, args); - for (expr & a : args) { - expr new_a = a; - if (m_eval_nested_prop || !m_ctx.is_prop(m_ctx.infer(a))) - new_a = normalize(a); - if (new_a != a) - modified = true; - a = new_a; - } - - if (is_constant(f)) { - if (auto idx = inductive::get_elim_major_idx(env(), const_name(f))) { - if (auto r = unfold_recursor_major(f, *idx, args)) - return *r; - } - } - if (!modified) - return e; - expr r = mk_rev_app(f, args); - if (is_constant(f) && env().is_recursor(const_name(f))) { - return normalize(r); - } else { - return r; - } -} - -expr normalizer::normalize_macro(expr const & e) { - // This method is invoked for macros that are not unfolded at whnf because - // the predicate should_unfold_macro(e) returned false - buffer new_args; - for (unsigned i = 0; i < macro_num_args(e); i++) - new_args.push_back(normalize(macro_arg(e, i))); - return update_macro(e, new_args.size(), new_args.data()); -} - -expr normalizer::normalize(expr e) { - check_system("normalize"); - if (!should_normalize(e)) - return e; - e = m_ctx.whnf(e); - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::Meta: case expr_kind::Local: - return e; - case expr_kind::Macro: - return normalize_macro(e); - case expr_kind::Lambda: { - e = normalize_binding(e); - if (m_use_eta) - return try_eta(e); - else - return e; - } - case expr_kind::Pi: - return normalize_binding(e); - case expr_kind::App: - return normalize_app(e); - case expr_kind::Let: - // whnf unfolds let-expressions - lean_unreachable(); - } - lean_unreachable(); // LCOV_EXCL_LINE -} - -normalizer::normalizer(old_type_context & ctx, bool eta, bool nested_prop): - m_ctx(ctx), m_use_eta(eta), m_eval_nested_prop(nested_prop) { - if (!is_standard(env())) - nested_prop = true; -} - -void initialize_old_type_context() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_internal_prefix = new name(name::mk_internal_unique_name()); - g_class_instance_max_depth = new name{"class", "instance_max_depth"}; - g_class_trans_instances = new name{"class", "trans_instances"}; -} - -void finalize_old_type_context() { - delete g_tmp_prefix; - delete g_internal_prefix; - delete g_class_instance_max_depth; - delete g_class_trans_instances; -} -} diff --git a/src/library/old_type_context.h b/src/library/old_type_context.h deleted file mode 100644 index 61e5e72ff7..0000000000 --- a/src/library/old_type_context.h +++ /dev/null @@ -1,568 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include -#include "util/fresh_name.h" -#include "util/scoped_map.h" -#include "kernel/environment.h" -#include "kernel/abstract_type_context.h" -#include "library/io_state.h" -#include "library/io_state_stream.h" -#include "library/projection.h" - -namespace lean { -unsigned get_class_instance_max_depth(options const & o); -bool get_class_trans_instances(options const & o); - -/** \brief Type inference, normalization and definitional equality. - It is similar to the kernel type checker but it also supports unification variables. - - Unification problems are eagerly solved. However, only higher-order patterns - are supported. - - This is a generic class containing several virtual methods that must - be implemeneted by "customers" (e.g., blast tactic). - - This class also implements type class resolution. - - Here are some notes on managing meta-variables and implementing validate_assignment. - One issue in the elaborator and automated procedures is that we may create a meta-variable ?M - in one context, and a unification constraint containing ?M in a different context. - Here are two basic examples: - - 1) forall (x : _) (A : Type) (y : A), x = y - The "_" becomes a fresh meta-variable ?m, and the equality "x = y" produces the - following unification constraint - - ?m =?= A - - It is incorrect to solve this constraint by assigning ?m := A. - The problem is that the term "A" is not available in the context where ?m was created. - - - 2) Consider the two following unification constraints - - (fun x, ?m) a =?= a - (fun x, ?m) b =?= b - - If we apply beta-reduction to them, we get - - ?m =?= a - ?m =?= b - - These simultaneous unification problem cannot be solved. - - In the Lean 0.2 elaborator, we addressed the issues above by making sure that - only *closed terms* (terms not containing local constants) - can be assigned to metavariables. So a metavariable that occurs in a - context records the parameters it depends on. For example, we - encode a "_" in the context (x : nat) (y : bool) as ?m x y, - where ?m is a fresh metavariable. - - So, example 1) would not be solved because we cannot assign "A" - (which is local constant aka free variable) to ?m. - In example 2), we encode it as - - (fun x, ?m x) a =?= a - (fun x, ?m x) b =?= b - - After applying beta-reduction to them, we get - - ?m a =?= a - ?m b =?= b - - Which has the solution ?m := fun x, x - - The solution used in the Lean 0.2 elaborator is correct, but it may produce performance problems - for procedures that have to create many meta-variables and the context is not small. - For example, if the context contains N declarations, then the type of each meta-variable - created will have N-nested Pi's. - This is the case of the blast tactic, the simplifier and the type class resolution procedure. - - In the simplifier and type class resolution procedures we create many - "temporary" meta variables and unification constraints that should be solved in the - **same** context. So, the problems described above do not occur, and - the solution used in the elaborator is an over-kill. - - So, type_context provides a more liberal approach. It allows "customers" of this - class to provide their own validation mechanism for meta-variable assignments. - In the simplifier and type class resolution, we use very basic validation. - Given `?m x_1 ... x_n =?= t`, before assigning `?m := fun x_1 ... x_n, t`, - we check whether ?m does not occurs in t, and whether all internal local constants - in t occur in `x_1 ... x_n`. - - In blast, we have our own mechanism for tracking hypotheses (i.e., the representation - of local constants in the blast search branches). This is a more efficient - representation that doesn't require us to create N-nested Pi expressions - whenever we want to create a meta-variable in a branch that has N hypotheses. - - In blast, the full local context is a telescope of the form - - 1- (all hypotheses in the current state) - 2- (all temporary local constants created by auxiliary procedure) Example: simplifier goes inside of a lambda. - 3- (all internal local constants created by type_context) Example: when processing is_def_eq. -*/ -class old_type_context : public abstract_type_context { - friend struct ext_ctx; - environment m_env; - // postponed universe constraints - std::vector> m_postponed; - name_map m_proj_info; - bool m_in_is_def_eq{false}; - - // Internal (configuration) options for customers - - /** If m_ignore_external_mvars is true, then we treat (external) expression meta-variables - as wildcards. That is, (?M t_1 ... t_n) matches any term T. We say a meta-variable is - external when is_mvar returns false for it, and this module can't assign it. */ - bool m_ignore_external_mvars; - - /** If m_check_types is true, then whenever we assign a meta-variable, - we check whether the type of the value matches the type of the meta-variable. - When this option is enabled, we turn on m_ignore_external_mvars while checking types. - - At this point, this option is useful only for helping us solve universe unification constraints. - For example, consider the following unification problem - Given: - p : Type.{l1} - q : Type.{l2} - ?m1 : Type.{?u1} - ?m2 : Type.{?u2} - - decidable.{max ?u1 u2} (?m1 -> ?m2) =?= decidable.{max l1 l2} (q -> p) - - If m_check_types is turned off, the is_def_eq implemented here produces the incorrect solution - - ?u1 := l1 - ?u2 := l2 - ?m1 := q - ?m2 := p - - This solution is type incorrect. - - ?m1 : Type.{l1} q : Type.{l2} - ?m2 : Type.{l2} p : Type.{l1} - - TODO(Leo,Daniel): checking types is extra overhead, and it seems unnecessary most of the time. - We should investigate how often this kind of constraint occurs in blast. - */ - bool m_check_types; - - /** Temporary flag to override/ignore the is_extra_opaque predicate. - We use it when inferring types and we want to be sure a type is Pi-type. */ - bool m_relax_is_opaque; - - typedef scoped_map> infer_cache; - infer_cache m_infer_cache; - - typedef std::unordered_map, name_hash> is_transparent_cache; - is_transparent_cache m_is_transparent_cache[2]; - - bool is_opaque(declaration const & d) const; - optional is_transparent(name const & n); - optional reduce_projection(expr const & e); - optional norm_ext(expr const & e); - expr whnf_core(expr const & e); - expr unfold_name_core(expr e, unsigned h); - expr unfold_names(expr const & e, unsigned h); - optional is_delta(expr const & e); - expr whnf_core(expr e, unsigned h); - - lbool quick_is_def_eq(level const & l1, level const & l2); - bool full_is_def_eq(level const & l1, level const & l2); - bool is_def_eq(level const & l1, level const & l2); - bool is_def_eq(levels const & ls1, levels const & ls2); - - lbool quick_is_def_eq(expr const & e1, expr const & e2); - bool is_def_eq_core(expr const & e1, expr const & e2); - bool is_def_eq_args(expr const & e1, expr const & e2); - bool is_def_eq_binding(expr e1, expr e2); - bool is_def_eq_eta(expr const & e1, expr const & e2); - bool is_def_eq_proof_irrel(expr const & e1, expr const & e2); - - expr subst_mvar(expr const & e); - bool process_assignment_core(expr const & ma, expr const & v); - bool process_assignment(expr const & ma, expr const & v); - enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff }; - reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n); - lbool lazy_delta_reduction(expr & t_n, expr & s_n); - reduction_status ext_reduction_step(expr & t_n, expr & s_n); - lbool reduce_def_eq(expr & t_n, expr & s_n); - - bool process_postponed(unsigned old_sz); - - expr infer_constant(expr const & e); - expr infer_macro(expr const & e); - expr infer_lambda(expr e); - expr infer_pi(expr const & e); - expr infer_app(expr const & e); - void ensure_sort(expr const & e, expr const & ref); - void ensure_pi(expr const & e, expr const & ref); - - struct scope { - old_type_context & m_owner; - bool m_keep; - unsigned m_postponed_sz; - scope(old_type_context & o):m_owner(o), m_keep(false), m_postponed_sz(o.m_postponed.size()) { m_owner.push(); } - ~scope() { m_owner.m_postponed.resize(m_postponed_sz); if (!m_keep) m_owner.pop(); } - void commit() { m_postponed_sz = m_owner.m_postponed.size(); m_owner.commit(); m_keep = true; } - }; - - // Data-structures for type class resolution - - struct ci_stack_entry { - // We only use transitive instances when we can solve the problem in a single step. - // That is, the transitive instance does not have any instance argument, OR - // it uses local instances to fill them. - // We accomplish that by not considering global instances when solving - // transitive instance subproblems. - expr m_mvar; - unsigned m_depth; - bool m_trans_inst_subproblem; - ci_stack_entry(expr const & m, unsigned d, bool s = false): - m_mvar(m), m_depth(d), m_trans_inst_subproblem(s) {} - }; - - struct ci_state { - bool m_trans_inst_subproblem; - list m_stack; // stack of meta-variables that need to be synthesized; - }; - - struct ci_choice { - list m_local_instances; - list m_trans_instances; - list m_instances; - ci_state m_state; - }; - - struct ci_choices_scope { - old_type_context & m_owner; - unsigned m_ci_choices_sz; - bool m_keep{false}; - ci_choices_scope(old_type_context & o):m_owner(o), m_ci_choices_sz(o.m_ci_choices.size()) {} - ~ci_choices_scope() { if (!m_keep) m_owner.restore_choices(m_ci_choices_sz); } - void commit() { m_keep = true; } - }; - - pos_info_provider const * m_pip; - std::vector> m_ci_local_instances; - expr_struct_map> m_ci_cache; - bool m_ci_multiple_instances; - expr m_ci_main_mvar; - ci_state m_ci_state; // active state - std::vector m_ci_choices; - unsigned m_ci_choices_ini_sz; - bool m_ci_displayed_trace_header; - optional m_ci_pos; - - /* subsingleton instance cache, we also cache failures */ - expr_struct_map> m_ss_cache; - - // configuration options - unsigned m_ci_max_depth; - bool m_ci_trans_instances; - bool m_ci_trace_instances; - - optional constant_is_class(expr const & e); - optional is_full_class(expr type); - lbool is_quick_class(expr const & type, name & result); - - optional> find_unsynth_metavar_at_args(expr const & e); - optional> find_unsynth_metavar(expr const & e); - - expr mk_internal_local(name const & n, expr const & type, binder_info const & bi = binder_info()); - expr mk_internal_local(expr const & type, binder_info const & bi = binder_info()); - expr mk_internal_local_from_binding(expr const & b) { - return mk_internal_local(binding_name(b), binding_domain(b), binding_info(b)); - } - - void trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r); - bool try_instance(ci_stack_entry const & e, expr const & inst, expr const & inst_type, bool trans_inst); - bool try_instance(ci_stack_entry const & e, name const & inst_name, bool trans_inst); - list get_local_instances(name const & cname); - bool is_ci_done() const; - bool mk_choice_point(expr const & mvar); - bool process_next_alt_core(ci_stack_entry const & e, list & insts); - bool process_next_alt_core(ci_stack_entry const & e, list & inst_names, bool trans_inst); - bool process_next_alt(ci_stack_entry const & e); - bool process_next_mvar(); - bool backtrack(); - optional search(); - optional next_solution(); - void init_search(expr const & type); - void restore_choices(unsigned old_sz); - optional ensure_no_meta(optional r); - optional mk_nested_instance(expr const & type); - bool mk_nested_instance(expr const & m, expr const & m_type); - optional mk_class_instance_core(expr const & type); - void cache_ci_result(expr const & type, optional const & inst); -public: - old_type_context(environment const & env, options const & o, bool multiple_instances = false); - virtual ~old_type_context(); - - void set_local_instances(list const & insts); - - virtual environment const & env() const override { return m_env; } - - /** \brief Opaque constants are never unfolded by this procedure. - The is_def_eq method will lazily unfold non-opaque constants. - - \remark This class always treats projections and theorems as opaque. */ - virtual bool is_extra_opaque(name const & n) const = 0; - - /** \brief This method is invoked when a term is being put in weak-head-normal-form. - It is used to decide whether a macro should be unfolded or not. */ - virtual bool should_unfold_macro(expr const &) const { return true; } - - /** \brief Return true iff \c e is an internal local constant created by this object */ - bool is_internal_local(expr const & e) const; - - /** \brief Create a temporary local constant */ - expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()); - - /** \brief Create a temporary local constant using the given pretty print name. - The pretty printing name has not semantic significance. */ - expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); - - virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi) override { - return mk_tmp_local(pp_name, type, bi); - } - - /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */ - expr mk_tmp_local_from_binding(expr const & b) { - return mk_tmp_local(binding_name(b), binding_domain(b), binding_info(b)); - } - - /** \brief Return true if \c e was created using \c mk_tmp_local */ - bool is_tmp_local(expr const & e) const; - - /** \brief Return true if \c l represents a universe unification variable. - \remark This is supposed to be a subset of is_meta(l). - \remark This method is only invoked when is_meta(l) is true. */ - virtual bool is_uvar(level const & l) const = 0; - - /** \brief This method is invoked by is_def_eq for universe terms. It allows the customer - to ignore a unification sub-problem for universe terms. */ - virtual bool ignore_universe_def_eq(level const &, level const &) const { return false; } - - /** \brief Return true if \c e represents a unification variable. - \remark This is supposed to be a subset of is_metavar(e). - \remark This method is only invoked when is_metavar(l) is true. - This module will only assign a metavariable \c m when is_mvar(m) is true. - This feature allows us to treat some (external) meta-variables as constants. */ - virtual bool is_mvar(expr const & e) const = 0; - - /** \brief Return the assignment for universe unification variable - \c u, and none if it is not assigned. - \pre is_uvar(u) */ - virtual optional get_assignment(level const & u) const = 0; - - /** \brief Return the assignment for unification variable - \c m, and none if it is not assigned. - \pre is_mvar(u) */ - virtual optional get_assignment(expr const & m) const = 0; - - /** \brief Update the assignment for \c u. - \pre is_uvar(u) */ - virtual void update_assignment(level const & u, level const & v) = 0; - /** \brief Update the assignment for \c m. - \pre is_mvar(m) */ - virtual void update_assignment(expr const & m, expr const & v) = 0; - - /** \brief Given a metavariable m that takes locals as arguments, this method - should return true if m can be assigned to an abstraction of \c v. - - \remark This method should check at least if m does not occur in v, and - whether all internal local constants in v occur in locals. - The default implementation only checks that. */ - virtual bool validate_assignment(expr const & m, buffer const & locals, expr const & v); - /** \brief Given a metavariable and the value \c v that has already been abstracted. - Check if the types match. - \remark By checking the types we may be able to assign additional metavariables. - The default implementation is: - - return is_def_eq_core(infer_metavar(m), infer(v)); */ - virtual bool validate_assignment_types(expr const & m, expr const & v); - - /** \brief Return the type of a local constant (local or not). - \remark This method allows the customer to store the type of local constants - in a different place. */ - virtual expr infer_local(expr const & e) const = 0; - - /** \brief Return the type of a meta-variable (even if it is not a unification one) */ - virtual expr infer_metavar(expr const & e) const = 0; - - virtual level mk_uvar() = 0; - - virtual expr mk_mvar(expr const &) = 0; - - /** \brief Save the current assignment and metavariable declarations */ - virtual void push_core() = 0; - /** \brief Retore assignment (inverse for push) */ - virtual void pop_core() = 0; - /** \brief Return the number of checkpoints created using \c push and not popped yet. */ - virtual unsigned get_num_check_points() const = 0; - /** \brief Keep the changes since last push */ - virtual void commit() = 0; - - /** \brief This method is invoked before failure. - The "customer" may try to assign unassigned mvars in the given expression. - The result is true to indicate that some metavariable has been assigned. - - The default implementation tries to invoke type class resolution to - assign unassigned metavariables in the given terms. */ - virtual bool on_is_def_eq_failure(expr const &, expr const &); - - bool try_unification_hints(expr const &, expr const &); - struct unification_hint_fn; - friend struct unification_hint_fn; - - bool is_assigned(level const & u) const { return static_cast(get_assignment(u)); } - bool is_assigned(expr const & m) const { return static_cast(get_assignment(m)); } - - bool has_assigned_uvar(level const & l) const; - bool has_assigned_uvar(levels const & ls) const; - bool has_assigned_uvar_mvar(expr const & e) const; - - void push(); - void pop(); - - /** \brief Expand macro using extension context */ - optional expand_macro(expr const & m); - - /** \brief Instantiate assigned universe unification variables occurring in \c l */ - level instantiate_uvars(level const & l); - - /** \brief Instantiate assigned unification variables occurring in \c e */ - expr instantiate_uvars_mvars(expr const & e); - - /** \brief Put the given term in weak-head-normal-form (modulo is_opaque predicate) */ - virtual expr whnf(expr const & e) override; - - /** \brief Similar to previous method but ignores the is_extra_opaque predicate. */ - virtual expr relaxed_whnf(expr const & e) override; - - /** \brief Return true if \c e is a proposition */ - bool is_prop(expr const & e); - - /** \brief Infer the type of \c e. */ - virtual expr infer(expr const & e) override; - - /** \brief Put \c e in whnf, it is a Pi, then return whnf, otherwise return e */ - expr try_to_pi(expr const & e); - /** \brief Put \c e in relaxed_whnf, it is a Pi, then return whnf, otherwise return e */ - expr relaxed_try_to_pi(expr const & e); - - /** \brief Return true if \c e1 and \c e2 are definitionally equal. - When \c e1 and \c e2, this method is not as complete as the one in the kernel. - That is, it may return false even when \c e1 and \c e2 may be definitionally equal. - - It is precise if \c e1 and \c e2 do not contain metavariables. - */ - virtual bool is_def_eq(expr const & e1, expr const & e2) override; - /** \brief Similar to \c is_def_eq, but sets m_relax_is_opaque */ - virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override; - - /** \brief Return the universe level for type A. If A is not a type return none. */ - optional get_level_core(expr const & A); - /** \brief Similar to previous method, but throws exception instead */ - level get_level(expr const & A); - - /** \brief If \c type is a type class, return its name */ - optional is_class(expr const & type); - - /** \brief Try to synthesize an instance of the type class \c type */ - optional mk_class_instance(expr const & type); - optional next_class_instance(); - /** \brief Try to synthesize an instance of (subsingleton type) - \remark This method is virtual because we need a refinement - at legacy_type_context to workaround an integration problem with the elaborator. */ - virtual optional mk_subsingleton_instance(expr const & type); - - /** \brief Given \c ma of the form ?m t_1 ... t_n, (try to) assign - ?m to (an abstraction of) v. Return true if success and false otherwise. - - \remark If ?m is already assigned, we just check if ma and v are definitionally - equal. */ - bool assign(expr const & ma, expr const & v); - /** \brief Similar to \c assign but sets m_relax_is_opaque */ - bool relaxed_assign(expr const & ma, expr const & v); - - - /** \brief Similar to \c assign, but it replaces the existing assignment - if the metavariable is already assigned. - - Application: for implicit instance arguments, we want the term to be the one - generated by type class resolution even when it can be inferred by type inference. */ - bool force_assign(expr const & ma, expr const & v); - /** \brief Similar to \c force_assign but sets m_relax_is_opaque */ - bool relaxed_force_assign(expr const & ma, expr const & v); - - /** \brief Clear all internal caches used to speedup computation */ - void clear_cache(); - /** \brief Clear internal type inference cache used to speedup computation */ - void clear_infer_cache(); - - /** \brief Update configuration options. - Return true iff the new options do not change the behavior of the object. - \remark We assume pretty-printing options are irrelevant. */ - bool update_options(options const & opts); - - /** \brief Return true if the local instances at \c insts are compatible with the ones - in the type inference object. This method is used to decide whether a type inference - object can be reused by the elaborator. */ - bool compatible_local_instances(list const & insts); - - /** \brief Auxiliary object used to set position information for the type class resolution trace. */ - class scope_pos_info { - old_type_context & m_owner; - pos_info_provider const * m_old_pip; - optional m_old_pos; - public: - scope_pos_info(old_type_context & o, pos_info_provider const * pip, expr const & pos_ref); - ~scope_pos_info(); - }; -}; - -/** \brief Simple normalizer */ -class normalizer { - old_type_context & m_ctx; - bool m_use_eta; - bool m_eval_nested_prop; - - expr normalize_binding(expr const & e); - optional unfold_recursor_core(expr const & f, unsigned i, - buffer const & idxs, buffer & args, bool is_rec); - expr normalize_app(expr const & e); - expr normalize_macro(expr const & e); - expr normalize(expr e); - -public: - /* - eta == true : enable eta reduction - nested_prop == true : nested propositions are simplified (ignored if HoTT library) - */ - normalizer(old_type_context & ctx, bool eta = true, bool nested_prop = false); - virtual ~normalizer() {} - - optional unfold_recursor_major(expr const & f, unsigned idx, buffer & args); - - /** \brief Auxiliary predicate for controlling which subterms will be normalized. */ - virtual bool should_normalize(expr const &) const { return true; } - - environment const & env() const { return m_ctx.env(); } - - expr operator()(expr const & e) { - return normalize(e); - } -}; - -void initialize_old_type_context(); -void finalize_old_type_context(); -}