From 04a61bdffea012d37d2d08183879003774d29e6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Apr 2014 18:32:50 -0700 Subject: [PATCH] feat(kernel/type_checker): remove dead code, add basic whnf procedure Signed-off-by: Leonardo de Moura --- src/kernel/expr.h | 7 +- src/kernel/type_checker.cpp | 703 ++++++------------------------------ src/kernel/type_checker.h | 8 +- 3 files changed, 119 insertions(+), 599 deletions(-) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 7c0157e1e..7fa585218 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -260,9 +260,9 @@ public: macro():m_rc(0) {} virtual ~macro() {} virtual name get_name() const = 0; - virtual expr get_type(buffer const & arg_types) const = 0; - virtual expr expand1(buffer const & args) const = 0; - virtual expr expand(buffer const & args) const = 0; + virtual expr get_type(unsigned num_args, expr const * arg_types) const = 0; + virtual optional expand1(unsigned num_args, expr const * args) const = 0; + virtual optional expand(unsigned num_args, expr const * args) const = 0; virtual int push_lua(lua_State * L) const; virtual bool operator==(macro const & other) const; bool operator<(macro const & other) const; @@ -340,6 +340,7 @@ template expr mk_app(T const & args) { return mk_app(args.size(), ar expr mk_rev_app(expr const & f, unsigned num_args, expr const * args); expr mk_rev_app(unsigned num_args, expr const * args); template expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); } +template expr mk_rev_app(expr const & f, T const & args) { return mk_rev_app(f, args.size(), args.data()); } inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); } inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index f6e235048..f8d1d95d7 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -4,638 +4,157 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel/type_checker.h" - - - -#if 0 -#include "util/freset.h" -#include "util/flet.h" #include "util/interrupt.h" -#include "kernel/environment.h" #include "kernel/type_checker.h" #include "kernel/expr_maps.h" -#include "kernel/kernel_exception.h" -#include "kernel/normalizer.h" #include "kernel/instantiate.h" -#include "kernel/free_vars.h" -#include "kernel/error_msgs.h" -#include "kernel/constraint.h" -#include "kernel/metavar.h" +#include "kernel/max_sharing.h" namespace lean { -expr pi_body_at(expr const & pi, expr const & a) { - lean_assert(is_pi(pi)); - if (closed(binder_body(pi))) - return binder_body(pi); - else - return instantiate(binder_body(pi), a); -} -/** \brief Auxiliary functional object used to implement infer_type. */ -class type_checker::imp { - typedef expr_map cache; +/** \brief Auxiliary functional object used to implement type checker. */ +struct type_checker::imp { + environment m_env; + name_generator m_gen; + constraint_handler & m_chandler; + bool m_memoize; + name_set m_extra_opaque; + max_sharing_fn m_sharing; + expr_map m_cache; + expr_map m_whnf_cache; - ro_environment::weak_ref m_env; - normalizer m_normalizer; - cache m_cache; - name_generator * m_name_gen; - constraints m_constraints; // constraints generated so far - bool m_infer_only; + imp(environment const & env, name_generator const & g, constraint_handler & h, bool memoize, name_set const & extra_opaque): + m_env(env), m_gen(g), m_chandler(h), m_memoize(memoize), m_extra_opaque(extra_opaque) {} - ro_environment env() const { return ro_environment(m_env); } - expr normalize(expr const & e) { return m_normalizer(e); } - - level mk_meta_univ() { - return ::lean::mk_meta_univ(m_name_gen->next()); - } - - void add_eq_constraint(expr const & t, expr const & s, justification const & j) { - m_constraints = add(m_constraints, mk_eq_cnstr(t, s, j)); - } - - expr check_sort(expr const & e, expr const & s) { - if (is_sort(e)) - return e; - expr u = normalize(e); - if (is_sort(u)) - return u; - if (has_metavar(u)) { - expr r = mk_sort(mk_meta_univ()); - justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & s) { - return pp_type_expected(fmt, o, s.instantiate_metavars_wo_jst(e)); - }); - add_eq_constraint(e, r, j); - return r; - } - throw_kernel_exception(env(), s, [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, e); }); - } - - expr check_pi(expr const & e, expr const & s, context const & ctx) { - if (is_pi(e)) - return e; - expr u = normalize(e); - if (is_pi(u)) - return u; - if (has_metavar(u)) { - // Create two fresh variables A and B, - // and assign r == (Pi(x : A), B) - expr A = m_menv->mk_metavar(ctx); - expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); - expr p = mk_pi(g_x_name, A, B); - justification jst = mk_function_expected_justification(ctx, s); - m_uc->push_back(mk_eq_constraint(ctx, e, p, jst)); - return p; - } - throw function_expected_exception(env(), ctx, s); - } -}; - -static name g_x_name("x"); -/** \brief Auxiliary functional object used to implement infer_type. */ -class type_checker::imp { - // TODO(Leo): we should consider merging check_pi and check_sigma. - // They are very similar - expr check_sigma(expr const & e, expr const & s, context const & ctx) { - if (is_sigma(e)) - return e; - expr r = normalize(e, ctx, false); - if (is_sigma(r)) - return r; - if (has_metavar(r) && m_menv && m_uc) { - // Create two fresh variables A and B, - // and assign r == (Pi(x : A), B) - expr A = m_menv->mk_metavar(ctx); - expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); - expr p = mk_sigma(g_x_name, A, B); - justification jst = mk_pair_expected_justification(ctx, s); - m_uc->push_back(mk_eq_constraint(ctx, e, p, jst)); - return p; - } - throw pair_expected_exception(env(), ctx, s); - } - - /** - \brief Given \c t (a Pi term), this method returns the body (aka range) - of the function space for the element e in the domain of the Pi. - */ - expr get_pi_body(expr const & t, expr const & e) { - lean_assert(is_pi(t)); - if (is_arrow(t)) - return lower_free_vars(abst_body(t), 1, 1); + expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; } + expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); } + expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); } + expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); } + optional expand_macro(expr const & m, unsigned num, expr const * args) { + lean_assert(is_macro(m)); + if (auto new_m = to_macro(m).expand(num, args)) + return some_expr(max_sharing(*new_m)); else - return instantiate(abst_body(t), e); + return none_expr(); + } + expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) { + return max_sharing(lean::instantiate_params(e, ps, ls)); } - expr get_range(expr t, expr const & e, context const & ctx) { - unsigned num = num_args(e); - for (unsigned i = 1; i < num; i++) { - expr const & a = arg(e, i); - if (is_pi(t)) { - t = get_pi_body(t, a); - } else { - t = normalize(t, ctx, false); - if (is_pi(t)) { - t = get_pi_body(t, a); - } else if (has_metavar(t) && m_menv && m_uc) { - // Create two fresh variables A and B, - // and assign r == (Pi(x : A), B) - expr A = m_menv->mk_metavar(ctx); - expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); - expr p = mk_pi(g_x_name, A, B); - justification jst = mk_function_expected_justification(ctx, e); - m_uc->push_back(mk_eq_constraint(ctx, t, p, jst)); - t = get_pi_body(p, a); - } else { - throw function_expected_exception(env(), ctx, e); - } - } - } - return t; + bool check_memoized(expr const & e) const { + return !m_memoize || m_sharing.already_processed(e); } - expr save_result(expr const & e, expr const & r, bool shared) { - if (shared) - m_cache[e] = r; - return r; - } + /** \brief Weak head normal form core procedure. It does not perform delta reduction nor extensions. */ + expr whnf_core(expr const & e) { + check_system("whnf"); + lean_assert(check_memoized(e)); - expr infer_type_core(expr const & e, context const & ctx) { - check_system("type checker"); - // cheap cases, we do not cache results + // handle easy cases switch (e.kind()) { - case expr_kind::MetaVar: - if (m_menv) { - if (m_menv->is_assigned(e)) - return infer_type_core(*(m_menv->get_subst(e)), ctx); - else - return m_menv->get_type(e); - } else { - throw unexpected_metavar_occurrence(env(), e); - } - case expr_kind::Constant: { - if (const_type(e)) { - return *const_type(e); - } else { - object const & obj = env()->get_object(const_name(e)); - if (obj.has_type()) - return obj.get_type(); - else - throw has_no_type_exception(env(), e); - } + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + return e; + case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: break; } - case expr_kind::Var: { - auto const & entry = lookup(ctx, var_idx(e)); - if (entry.get_domain()) - return lift_free_vars(*(entry.get_domain()), var_idx(e) + 1); - // Remark: the case where ce.get_domain() is not - // available is not considered cheap. - break; - } - case expr_kind::Value: - if (m_infer_only) { - return to_value(e).get_type(); - } else { - name const & n = to_value(e).get_name(); - object obj = env()->get_object(n); - if ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e))) { - return to_value(e).get_type(); - } else { - throw invalid_builtin_value_reference(env(), e); - } - } - case expr_kind::Type: - return mk_type(ty_level(e) + 1); - case expr_kind::App: case expr_kind::Lambda: - case expr_kind::Pi: case expr_kind::Let: - case expr_kind::Sigma: case expr_kind::Proj: - case expr_kind::Pair: - break; // expensive cases - } - bool shared = false; - if (is_shared(e)) { - shared = true; - auto it = m_cache.find(e); - if (it != m_cache.end()) + // check cache + if (m_memoize) { + auto it = m_whnf_cache.find(e); + if (it != m_whnf_cache.end()) return it->second; } + // do the actual work expr r; switch (e.kind()) { - case expr_kind::MetaVar: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: - lean_unreachable(); // LCOV_EXCL_LINE; - case expr_kind::Var: { - unsigned i = var_idx(e); - auto p = lookup_ext(ctx, i); - context_entry const & def = p.first; - context const & def_ctx = p.second; - lean_assert(ctx.size() > def_ctx.size()); - lean_assert(!def.get_domain()); // was handled as cheap - optional const & b = def.get_body(); - lean_assert(b); - expr t = infer_type_core(*b, def_ctx); - r = lift_free_vars(t, var_idx(e) + 1); + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Macro: + if (auto m = expand_macro(e, 0, 0)) + r = whnf_core(*m); + else + r = e; break; - } - case expr_kind::App: - if (m_infer_only) { - expr const & f = arg(e, 0); - expr f_t = infer_type_core(f, ctx); - r = get_range(f_t, e, ctx); - } else { - unsigned num = num_args(e); - lean_assert(num >= 2); - buffer arg_types; - for (unsigned i = 0; i < num; i++) { - arg_types.push_back(infer_type_core(arg(e, i), ctx)); + case expr_kind::Let: + r = whnf_core(instantiate(let_body(e), let_value(e))); + break; + case expr_kind::App: { + buffer args; + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); + } + expr f = whnf_core(*it); + if (is_lambda(f)) { + unsigned m = 1; + unsigned num_args = args.size(); + while (is_lambda(binder_body(f)) && m < num_args) { + f = binder_body(f); + m++; } - expr f_t = check_pi(arg_types[0], e, ctx); - unsigned i = 1; - while (true) { - expr const & c = arg(e, i); - expr const & c_t = arg_types[i]; - // thunk for creating justification object if needed - auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); }; - if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification)) - throw app_type_mismatch_exception(env(), ctx, e, i, arg_types.size(), arg_types.data()); - f_t = pi_body_at(f_t, c); - i++; - if (i == num) { - r = f_t; - break; - } - f_t = check_pi(f_t, e, ctx); - } - } - break; - case expr_kind::Pair: - if (m_infer_only) { - r = pair_type(e); - } else { - expr const & t = pair_type(e); - expr sig = check_sigma(t, t, ctx); - expr f_t = infer_type_core(pair_first(e), ctx); - expr s_t = infer_type_core(pair_second(e), ctx); - auto mk_fst_justification = [&]() { return mk_pair_type_match_justification(ctx, e, true); }; - if (!is_convertible(f_t, abst_domain(sig), ctx, mk_fst_justification)) - throw pair_type_mismatch_exception(env(), ctx, e, true, f_t, sig); - auto mk_snd_justification = [&]() { return mk_pair_type_match_justification(ctx, e, false); }; - expr expected = instantiate(abst_body(sig), pair_first(e)); - if (!is_convertible(s_t, expected, ctx, mk_snd_justification)) { - throw pair_type_mismatch_exception(env(), ctx, e, false, s_t, sig); - } - r = sig; - } - break; - case expr_kind::Proj: { - expr t = check_sigma(infer_type_core(proj_arg(e), ctx), e, ctx); - if (proj_first(e)) { - r = abst_domain(t); - } else { - expr const & b = abst_body(t); - if (closed(b)) - r = b; - else - r = instantiate(b, mk_proj1(proj_arg(e))); - } - break; - } - case expr_kind::Lambda: - if (!m_infer_only) { - expr d = infer_type_core(abst_domain(e), ctx); - check_type(d, abst_domain(e), ctx); - } - { - freset reset(m_cache); - r = mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))); - } - break; - case expr_kind::Sigma: case expr_kind::Pi: { - expr t1 = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx); - if (is_bool(t1)) - t1 = Type(); - expr t2; - context new_ctx = extend(ctx, abst_name(e), abst_domain(e)); - { - freset reset(m_cache); - t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx); - } - if (is_bool(t2)) { - if (is_pi(e)) { - r = Bool; + lean_assert(m <= num_args); + r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data())); + break; + } else if (is_macro(f)) { + auto m = expand_macro(f, args.size(), args.data()); + if (m) { + r = whnf_core(*m); break; - } else { - t2 = Type(); } } - if (is_type(t1) && is_type(t2)) { - r = mk_type(max(ty_level(t1), ty_level(t2))); - } else { - lean_assert(m_uc); - justification jst = mk_max_type_justification(ctx, e); - r = m_menv->mk_metavar(ctx); - m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst)); - } - break; - } - case expr_kind::Let: { - optional lt; - if (m_infer_only) { - lt = let_type(e); - } else { - if (let_type(e)) { - expr value_ty = infer_type_core(let_value(e), ctx); - expr ty = infer_type_core(*let_type(e), ctx); - check_type(ty, *let_type(e), ctx); // check if it is really a type - // thunk for creating justification object if needed - auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); }; - if (!is_convertible(value_ty, *let_type(e), ctx, mk_justification)) - throw def_type_mismatch_exception(env(), ctx, let_name(e), *let_type(e), let_value(e), value_ty); - lt = let_type(e); - } else { - lt = infer_type_core(let_value(e), ctx); - } - } - { - freset reset(m_cache); - expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); - r = instantiate(t, let_value(e)); - } + r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data()); break; }} - return save_result(e, r, shared); + + if (m_memoize) + m_whnf_cache.insert(mk_pair(e, r)); + return r; } - bool is_convertible_core(expr const & given, expr const & expected) { - if (given == expected) { - return true; - } else { - expr const * g = &given; - expr const * e = &expected; - while (true) { - if (is_type(*e) && is_type(*g)) { - if (env()->is_ge(ty_level(*e), ty_level(*g))) - return true; - } - - if (is_type(*e) && *g == mk_bool_type()) - return true; - - if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) { - g = &abst_body(*g); - e = &abst_body(*e); - } else { - return false; - } + /** \brief Expand \c e if it is non-opaque constant with weight >= w */ + expr unfold_name_core(expr e, unsigned w) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) { + if (d->is_definition() && !d->is_opaque() && d->get_weight() >= w && !m_extra_opaque.contains(d->get_name())) + return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_level_params(e)), w); } } + return e; } - template - bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) { - if (is_convertible_core(given, expected)) - return true; - expr new_given = normalize(given, ctx, false); - expr new_expected = normalize(expected, ctx, false); - if (is_convertible_core(new_given, new_expected)) - return true; - if (m_menv && m_uc && (has_metavar(new_given) || has_metavar(new_expected))) { - m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification())); - return true; - } - return false; - } + /** + \brief Expand constants and application where the function is a constant. - void set_ctx(context const & ctx) { - if (!is_eqp(m_ctx, ctx)) { - clear(); - m_ctx = ctx; + The unfolding is only performend if the constant corresponds to + a non-opaque definition with weight >= w, and it is not in the + set of extra_opaque constants. + */ + expr unfold_names(expr const & e, unsigned w) { + if (is_app(e)) { + expr const * it = &e; + while (is_app(*it)) { + it = &(app_fn(*it)); + } + expr f = unfold_name_core(*it, w); + if (is_eqp(f, *it)) { + return e; + } else { + buffer args; + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); + } + return mk_rev_app(f, args.size(), args.data()); + } + } else { + return unfold_name_core(e, w); } } - void update_menv(optional const & menv) { - if (m_menv.update(menv)) - clear_cache(); - } - - struct set_infer_only { - imp & m_ref; - bool m_old_infer_only; - set_infer_only(imp & r, bool flag):m_ref(r), m_old_infer_only(m_ref.m_infer_only) { - if (m_ref.m_infer_only != flag) - m_ref.clear_cache(); - m_ref.m_infer_only = flag; - } - ~set_infer_only() { - if (m_ref.m_infer_only != m_old_infer_only) - m_ref.clear_cache(); - m_ref.m_infer_only = m_old_infer_only; - } - }; - -public: - imp(ro_environment const & env, bool infer_only): - m_env(env), - m_normalizer(env) { - m_uc = nullptr; - m_infer_only = infer_only; - } - - expr infer_check(expr const & e, context const & ctx, optional const & menv, buffer * uc, - bool infer_only) { - clear_cache(); // temp hack - set_infer_only set(*this, infer_only); - set_ctx(ctx); - update_menv(menv); - flet set_uc(m_uc, uc); - return infer_type_core(e, ctx); - } - - expr infer_type(expr const & e, context const & ctx, optional const & menv, buffer * uc) { - return infer_check(e, ctx, menv, uc, true); - } - - expr check(expr const & e, context const & ctx, optional const & menv, buffer * uc) { - return infer_check(e, ctx, menv, uc, false); - } - - bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional const & menv) { - set_ctx(ctx); - update_menv(menv); - auto mk_justification = [](){ - lean_unreachable(); return justification(); // LCOV_EXCL_LINE - }; - return is_convertible(t1, t2, ctx, mk_justification); - } - - bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional const & menv) { - set_ctx(ctx); - update_menv(menv); - if (t1 == t2) - return true; - expr new_t1 = normalize(t1, ctx, false); - expr new_t2 = normalize(t2, ctx, false); - return new_t1 == new_t2; - } - - void check_type(expr const & e, context const & ctx) { - set_ctx(ctx); - update_menv(none_menv()); - expr t = infer_type_core(e, ctx); - check_type(t, e, ctx); - } - - bool is_proposition(expr const & e, context const & ctx, optional const & menv) { - // Catch easy cases - switch (e.kind()) { - case expr_kind::Lambda: case expr_kind::Type: - return false; - case expr_kind::Pi: - return is_proposition(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)), menv); - default: - break; - } - expr t = infer_type(e, ctx, menv, nullptr); - if (is_bool(t)) - return true; - else - return is_bool(normalize(t, ctx, false)); - } - - expr ensure_pi(expr const & e, context const & ctx, optional const & menv) { - set_ctx(ctx); - update_menv(menv); - try { - return check_pi(e, expr(), ctx); - } catch (exception &) { - throw exception("internal bug, expression is not a Pi"); - } - } - - expr ensure_sigma(expr const & e, context const & ctx, optional const & menv) { - set_ctx(ctx); - update_menv(menv); - try { - return check_sigma(e, expr(), ctx); - } catch (exception &) { - throw exception("internal bug, expression is not a Sigma"); - } - } - - void clear_cache() { - m_cache.clear(); - m_normalizer.clear(); - } - - void clear() { - clear_cache(); - m_menv.clear(); - m_ctx = context(); - } - - normalizer & get_normalizer() { - return m_normalizer; - } }; - -type_checker::type_checker(ro_environment const & env, bool infer_only):m_ptr(new imp(env, infer_only)) {} -type_checker::~type_checker() {} -expr type_checker::infer_type(expr const & e, context const & ctx, optional const & menv, buffer * uc) { - return m_ptr->infer_type(e, ctx, menv, uc); } -expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer & uc) { - return m_ptr->infer_type(e, ctx, some_menv(menv), &uc); -} -expr type_checker::infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv) { - // metavariable environment is not updated when unification constraints are not provided - return infer_type(e, ctx, some_menv(menv.to_rw()), nullptr); -} -expr type_checker::infer_type(expr const & e, context const & ctx, optional const & menv) { - return infer_type(e, ctx, ro_metavar_env::to_rw(menv), nullptr); -} -expr type_checker::infer_type(expr const & e, context const & ctx) { - return infer_type(e, ctx, none_menv(), nullptr); -} -expr type_checker::check(expr const & e, context const & ctx, optional const & menv, buffer * uc) { - return m_ptr->check(e, ctx, menv, uc); -} -expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv, buffer & uc) { - return m_ptr->check(e, ctx, some_menv(menv), &uc); -} -expr type_checker::check(expr const & e, context const & ctx, ro_metavar_env const & menv) { - // metavariable environment is not updated when unification constraints are not provided - return check(e, ctx, some_menv(menv.to_rw()), nullptr); -} -expr type_checker::check(expr const & e, context const & ctx) { - return check(e, ctx, none_menv(), nullptr); -} -bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, optional const & menv) { - return m_ptr->is_convertible(t1, t2, ctx, ro_metavar_env::to_rw(menv)); -} -bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { - return m_ptr->is_convertible(t1, t2, ctx, none_menv()); -} -bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx, optional const & menv) { - return m_ptr->is_definitionally_equal(t1, t2, ctx, ro_metavar_env::to_rw(menv)); -} -bool type_checker::is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx) { - return m_ptr->is_definitionally_equal(t1, t2, ctx, none_menv()); -} -void type_checker::check_type(expr const & e, context const & ctx) { - m_ptr->check_type(e, ctx); -} -expr type_checker::ensure_pi(expr const & e, context const & ctx, optional const & menv) { - return m_ptr->ensure_pi(e, ctx, ro_metavar_env::to_rw(menv)); -} -expr type_checker::ensure_pi(expr const & e, context const & ctx) { - return m_ptr->ensure_pi(e, ctx, none_menv()); -} -expr type_checker::ensure_sigma(expr const & e, context const & ctx, optional const & menv) { - return m_ptr->ensure_sigma(e, ctx, ro_metavar_env::to_rw(menv)); -} -expr type_checker::ensure_sigma(expr const & e, context const & ctx) { - return m_ptr->ensure_sigma(e, ctx, none_menv()); -} -bool type_checker::is_proposition(expr const & e, context const & ctx, optional const & menv) { - return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv)); -} -bool type_checker::is_proposition(expr const & e, context const & ctx) { - return is_proposition(e, ctx, none_ro_menv()); -} -bool type_checker::is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) { - return is_proposition(e, ctx, some_ro_menv(menv)); -} -bool type_checker::is_flex_proposition(expr e, context ctx, optional const & menv) { - while (is_pi(e)) { - ctx = extend(ctx, abst_name(e), abst_domain(e)); - e = abst_body(e); - } - return is_proposition(e, ctx, menv); -} -bool type_checker::is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) { - return is_flex_proposition(e, ctx, some_ro_menv(menv)); -} -bool type_checker::is_flex_proposition(expr const & e, context const & ctx) { - return is_flex_proposition(e, ctx, none_ro_menv()); -} -void type_checker::clear() { m_ptr->clear(); } -normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } -expr type_check(expr const & e, ro_environment const & env, context const & ctx) { - return type_checker(env).check(e, ctx); -} -bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) { - return type_checker(env).is_convertible(given, expected, ctx); -} -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional const & menv) { - return type_checker(env).is_proposition(e, ctx, menv); -} -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv) { - return is_proposition(e, env, ctx, some_ro_menv(menv)); -} -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) { - return is_proposition(e, env, ctx, none_ro_menv()); -} -} -#endif diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index b14d40881..6260cfad9 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/name_generator.h" +#include "util/name_set.h" #include "kernel/environment.h" #include "kernel/constraint.h" @@ -25,7 +26,7 @@ public: The type checker produces constraints, and they are sent to the constraint handler. */ class type_checker { - class imp; + struct imp; std::unique_ptr m_ptr; public: /** @@ -34,15 +35,14 @@ public: The following set of options is supported: - memoize: inferred types are memoized/cached - - unique_expr: hash consing is performed on input expressions, it improves the effectiveness of memoize - extra_opaque: additional definitions that should be treated as opaque */ - type_checker(environment const & env, name_generator const & g, constraint_handler & h, options const & o = options()); + type_checker(environment const & env, name_generator const & g, constraint_handler & h, bool memoize = false, name_set const & extra_opaque = name_set()); /** \brief Similar to the previous constructor, but if a method tries to create a constraint, then an exception is thrown. */ - type_checker(environment const & env, name_generator const & g, options const & o = options()); + type_checker(environment const & env, name_generator const & g, bool memoize = false, name_set const & extra_opaque = name_set()); ~type_checker(); /**