feat(kernel/type_checker): remove dead code, add basic whnf procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
188da7e4c6
commit
04a61bdffe
3 changed files with 119 additions and 599 deletions
|
@ -260,9 +260,9 @@ public:
|
||||||
macro():m_rc(0) {}
|
macro():m_rc(0) {}
|
||||||
virtual ~macro() {}
|
virtual ~macro() {}
|
||||||
virtual name get_name() const = 0;
|
virtual name get_name() const = 0;
|
||||||
virtual expr get_type(buffer<expr> const & arg_types) const = 0;
|
virtual expr get_type(unsigned num_args, expr const * arg_types) const = 0;
|
||||||
virtual expr expand1(buffer<expr> const & args) const = 0;
|
virtual optional<expr> expand1(unsigned num_args, expr const * args) const = 0;
|
||||||
virtual expr expand(buffer<expr> const & args) const = 0;
|
virtual optional<expr> expand(unsigned num_args, expr const * args) const = 0;
|
||||||
virtual int push_lua(lua_State * L) const;
|
virtual int push_lua(lua_State * L) const;
|
||||||
virtual bool operator==(macro const & other) const;
|
virtual bool operator==(macro const & other) const;
|
||||||
bool operator<(macro const & other) const;
|
bool operator<(macro const & other) const;
|
||||||
|
@ -340,6 +340,7 @@ template<typename T> 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(expr const & f, unsigned num_args, expr const * args);
|
||||||
expr mk_rev_app(unsigned num_args, expr const * args);
|
expr mk_rev_app(unsigned num_args, expr const * args);
|
||||||
template<typename T> expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); }
|
template<typename T> expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); }
|
||||||
|
template<typename T> 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_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_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); }
|
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); }
|
||||||
|
|
|
@ -4,638 +4,157 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
*/
|
*/
|
||||||
#include "kernel/type_checker.h"
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
#include "util/freset.h"
|
|
||||||
#include "util/flet.h"
|
|
||||||
#include "util/interrupt.h"
|
#include "util/interrupt.h"
|
||||||
#include "kernel/environment.h"
|
|
||||||
#include "kernel/type_checker.h"
|
#include "kernel/type_checker.h"
|
||||||
#include "kernel/expr_maps.h"
|
#include "kernel/expr_maps.h"
|
||||||
#include "kernel/kernel_exception.h"
|
|
||||||
#include "kernel/normalizer.h"
|
|
||||||
#include "kernel/instantiate.h"
|
#include "kernel/instantiate.h"
|
||||||
#include "kernel/free_vars.h"
|
#include "kernel/max_sharing.h"
|
||||||
#include "kernel/error_msgs.h"
|
|
||||||
#include "kernel/constraint.h"
|
|
||||||
#include "kernel/metavar.h"
|
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
expr pi_body_at(expr const & pi, expr const & a) {
|
|
||||||
lean_assert(is_pi(pi));
|
/** \brief Auxiliary functional object used to implement type checker. */
|
||||||
if (closed(binder_body(pi)))
|
struct type_checker::imp {
|
||||||
return binder_body(pi);
|
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<expr> m_cache;
|
||||||
|
expr_map<expr> m_whnf_cache;
|
||||||
|
|
||||||
|
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) {}
|
||||||
|
|
||||||
|
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<expr> 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
|
else
|
||||||
return instantiate(binder_body(pi), a);
|
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));
|
||||||
}
|
}
|
||||||
|
|
||||||
/** \brief Auxiliary functional object used to implement infer_type. */
|
bool check_memoized(expr const & e) const {
|
||||||
class type_checker::imp {
|
return !m_memoize || m_sharing.already_processed(e);
|
||||||
typedef expr_map<expr> 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;
|
|
||||||
|
|
||||||
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) {
|
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor extensions. */
|
||||||
m_constraints = add(m_constraints, mk_eq_cnstr(t, s, j));
|
expr whnf_core(expr const & e) {
|
||||||
}
|
check_system("whnf");
|
||||||
|
lean_assert(check_memoized(e));
|
||||||
|
|
||||||
expr check_sort(expr const & e, expr const & s) {
|
// handle easy cases
|
||||||
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);
|
|
||||||
else
|
|
||||||
return instantiate(abst_body(t), e);
|
|
||||||
}
|
|
||||||
|
|
||||||
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;
|
|
||||||
}
|
|
||||||
|
|
||||||
expr save_result(expr const & e, expr const & r, bool shared) {
|
|
||||||
if (shared)
|
|
||||||
m_cache[e] = r;
|
|
||||||
return r;
|
|
||||||
}
|
|
||||||
|
|
||||||
expr infer_type_core(expr const & e, context const & ctx) {
|
|
||||||
check_system("type checker");
|
|
||||||
// cheap cases, we do not cache results
|
|
||||||
switch (e.kind()) {
|
switch (e.kind()) {
|
||||||
case expr_kind::MetaVar:
|
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
|
||||||
if (m_menv) {
|
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant:
|
||||||
if (m_menv->is_assigned(e))
|
return e;
|
||||||
return infer_type_core(*(m_menv->get_subst(e)), ctx);
|
case expr_kind::Macro: case expr_kind::Let: case expr_kind::App:
|
||||||
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);
|
|
||||||
}
|
|
||||||
break;
|
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;
|
// check cache
|
||||||
if (is_shared(e)) {
|
if (m_memoize) {
|
||||||
shared = true;
|
auto it = m_whnf_cache.find(e);
|
||||||
auto it = m_cache.find(e);
|
if (it != m_whnf_cache.end())
|
||||||
if (it != m_cache.end())
|
|
||||||
return it->second;
|
return it->second;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// do the actual work
|
||||||
expr r;
|
expr r;
|
||||||
switch (e.kind()) {
|
switch (e.kind()) {
|
||||||
case expr_kind::MetaVar: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
|
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
|
||||||
lean_unreachable(); // LCOV_EXCL_LINE;
|
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant:
|
||||||
case expr_kind::Var: {
|
lean_unreachable(); // LCOV_EXCL_LINE
|
||||||
unsigned i = var_idx(e);
|
case expr_kind::Macro:
|
||||||
auto p = lookup_ext(ctx, i);
|
if (auto m = expand_macro(e, 0, 0))
|
||||||
context_entry const & def = p.first;
|
r = whnf_core(*m);
|
||||||
context const & def_ctx = p.second;
|
|
||||||
lean_assert(ctx.size() > def_ctx.size());
|
|
||||||
lean_assert(!def.get_domain()); // was handled as cheap
|
|
||||||
optional<expr> 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);
|
|
||||||
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<expr> arg_types;
|
|
||||||
for (unsigned i = 0; i < num; i++) {
|
|
||||||
arg_types.push_back(infer_type_core(arg(e, i), ctx));
|
|
||||||
}
|
|
||||||
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
|
else
|
||||||
r = instantiate(b, mk_proj1(proj_arg(e)));
|
r = e;
|
||||||
|
break;
|
||||||
|
case expr_kind::Let:
|
||||||
|
r = whnf_core(instantiate(let_body(e), let_value(e)));
|
||||||
|
break;
|
||||||
|
case expr_kind::App: {
|
||||||
|
buffer<expr> 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++;
|
||||||
|
}
|
||||||
|
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;
|
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<cache> 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<cache> 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;
|
|
||||||
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<expr> 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<cache> 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;
|
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) {
|
/** \brief Expand \c e if it is non-opaque constant with weight >= w */
|
||||||
if (given == expected) {
|
expr unfold_name_core(expr e, unsigned w) {
|
||||||
return true;
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
\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 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 {
|
} else {
|
||||||
expr const * g = &given;
|
buffer<expr> args;
|
||||||
expr const * e = &expected;
|
expr const * it = &e;
|
||||||
while (true) {
|
while (is_app(*it)) {
|
||||||
if (is_type(*e) && is_type(*g)) {
|
args.push_back(app_arg(*it));
|
||||||
if (env()->is_ge(ty_level(*e), ty_level(*g)))
|
it = &(app_fn(*it));
|
||||||
return true;
|
}
|
||||||
|
return mk_rev_app(f, args.size(), args.data());
|
||||||
}
|
}
|
||||||
|
|
||||||
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 {
|
} else {
|
||||||
return false;
|
return unfold_name_core(e, w);
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
template<typename MkJustification>
|
|
||||||
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;
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_ctx(context const & ctx) {
|
|
||||||
if (!is_eqp(m_ctx, ctx)) {
|
|
||||||
clear();
|
|
||||||
m_ctx = ctx;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void update_menv(optional<metavar_env> 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<metavar_env> const & menv, buffer<unification_constraint> * uc,
|
|
||||||
bool infer_only) {
|
|
||||||
clear_cache(); // temp hack
|
|
||||||
set_infer_only set(*this, infer_only);
|
|
||||||
set_ctx(ctx);
|
|
||||||
update_menv(menv);
|
|
||||||
flet<unification_constraints*> set_uc(m_uc, uc);
|
|
||||||
return infer_type_core(e, ctx);
|
|
||||||
}
|
|
||||||
|
|
||||||
expr infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
|
|
||||||
return infer_check(e, ctx, menv, uc, true);
|
|
||||||
}
|
|
||||||
|
|
||||||
expr check(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
|
|
||||||
return infer_check(e, ctx, menv, uc, false);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool is_convertible(expr const & t1, expr const & t2, context const & ctx, optional<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> 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<metavar_env> const & menv, buffer<unification_constraint> * 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<unification_constraint> & 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<ro_metavar_env> 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<metavar_env> const & menv, buffer<unification_constraint> * uc) {
|
|
||||||
return m_ptr->check(e, ctx, menv, uc);
|
|
||||||
}
|
|
||||||
expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & 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<ro_metavar_env> 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<ro_metavar_env> 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<ro_metavar_env> 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<ro_metavar_env> 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<ro_metavar_env> 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<ro_metavar_env> 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<ro_metavar_env> 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
|
|
||||||
|
|
|
@ -8,6 +8,7 @@ Author: Leonardo de Moura
|
||||||
#include <memory>
|
#include <memory>
|
||||||
#include <utility>
|
#include <utility>
|
||||||
#include "util/name_generator.h"
|
#include "util/name_generator.h"
|
||||||
|
#include "util/name_set.h"
|
||||||
#include "kernel/environment.h"
|
#include "kernel/environment.h"
|
||||||
#include "kernel/constraint.h"
|
#include "kernel/constraint.h"
|
||||||
|
|
||||||
|
@ -25,7 +26,7 @@ public:
|
||||||
The type checker produces constraints, and they are sent to the constraint handler.
|
The type checker produces constraints, and they are sent to the constraint handler.
|
||||||
*/
|
*/
|
||||||
class type_checker {
|
class type_checker {
|
||||||
class imp;
|
struct imp;
|
||||||
std::unique_ptr<imp> m_ptr;
|
std::unique_ptr<imp> m_ptr;
|
||||||
public:
|
public:
|
||||||
/**
|
/**
|
||||||
|
@ -34,15 +35,14 @@ public:
|
||||||
|
|
||||||
The following set of options is supported:
|
The following set of options is supported:
|
||||||
- memoize: inferred types are memoized/cached
|
- 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
|
- 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
|
\brief Similar to the previous constructor, but if a method tries to create a constraint, then an
|
||||||
exception is thrown.
|
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();
|
~type_checker();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
Loading…
Reference in a new issue