michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/type_checker): remove type_checker::imp

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-22 13:39:58 -07:00
parent 29a00c46d0
commit edb2e85898
3 changed files with 493 additions and 485 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/kernel/inductive/inductive.cpp
View file

@ -169,6 +169,7 @@ static environment update(environment const & env, inductive_env_ext const & ext
/** \brief Helper functional object for processing inductive datatype declarations. */
struct add_inductive_fn {
typedef std::unique_ptr<type_checker> type_checker_ptr;
environment m_env;
level_param_names m_level_names; // universe level parameters
unsigned m_num_params;
@ -176,7 +177,7 @@ struct add_inductive_fn {
unsigned m_decls_sz; // length(m_decls)
list<level> m_levels; // m_level_names ==> m_levels
name_generator m_ngen;
type_checker m_tc;
type_checker_ptr m_tc;
level m_elim_level; // extra universe level for eliminator.
bool m_dep_elim; // true if using dependent elimination
@ -199,7 +200,7 @@ struct add_inductive_fn {
unsigned num_params,
list<inductive_decl> const & decls):
m_env(env), m_level_names(level_params), m_num_params(num_params), m_decls(decls),
m_ngen(g_tmp_prefix), m_tc(m_env) {
m_ngen(g_tmp_prefix), m_tc(new type_checker(m_env)) {
m_decls_sz = length(m_decls);
m_levels = param_names_to_levels(level_params);
}
@ -209,10 +210,11 @@ struct add_inductive_fn {
/** \brief Make sure the latest environment is being used by m_tc. */
void updt_type_checker() {
type_checker tc(m_env);
m_tc.swap(tc);
m_tc.reset(new type_checker(m_env));
}
type_checker & tc() { return *(m_tc.get()); }
/** \brief Return a fresh name. */
name mk_fresh_name() { return m_ngen.next(); }
@ -233,7 +235,7 @@ struct add_inductive_fn {
bool to_prop = false; // set to true if the inductive datatypes live in Bool/Prop (Type 0)
for (auto d : m_decls) {
expr t = inductive_decl_type(d);
m_tc.check(t, m_level_names);
tc().check(t, m_level_names);
unsigned i = 0;
m_it_num_args.push_back(0);
while (is_pi(t)) {
@ -243,7 +245,7 @@ struct add_inductive_fn {
m_param_consts.push_back(l);
t = instantiate(binding_body(t), l);
} else {
if (!m_tc.is_def_eq(binding_domain(t), get_param_type(i)))
if (!tc().is_def_eq(binding_domain(t), get_param_type(i)))
throw kernel_exception(m_env, "parameters of all inductive datatypes must match");
t = instantiate(binding_body(t), m_param_consts[i]);
}
@ -255,7 +257,7 @@ struct add_inductive_fn {
}
if (i != m_num_params)
throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration");
t = m_tc.ensure_sort(t);
t = tc().ensure_sort(t);
if (m_env.impredicative()) {
// if the environment is impredicative, then the resultant universe is 0 (Bool/Prop),
// or is never zero (under any parameter assignment).
@ -298,7 +300,7 @@ struct add_inductive_fn {
bool is_valid_it_app(expr const & t, unsigned d_idx) {
buffer<expr> args;
expr I = get_app_args(t, args);
if (!m_tc.is_def_eq(I, m_it_consts[d_idx]) || args.size() != m_it_num_args[d_idx])
if (!tc().is_def_eq(I, m_it_consts[d_idx]) || args.size() != m_it_num_args[d_idx])
return false;
for (unsigned i = 0; i < m_num_params; i++) {
if (m_param_consts[i] != args[i])
@ -333,15 +335,15 @@ struct add_inductive_fn {
Return none otherwise.
*/
optional<unsigned> is_rec_argument(expr t) {
t = m_tc.whnf(t);
t = tc().whnf(t);
while (is_pi(t))
t = m_tc.whnf(instantiate(binding_body(t), mk_local_for(t)));
t = tc().whnf(instantiate(binding_body(t), mk_local_for(t)));
return is_valid_it_app(t);
}
/** \brief Check if \c t contains only positive occurrences of the inductive datatypes being declared. */
void check_positivity(expr t, name const & intro_name, int arg_idx) {
t = m_tc.whnf(t);
t = tc().whnf(t);
if (!has_it_occ(t)) {
// nonrecursive argument
} else if (is_pi(t)) {
@ -365,17 +367,17 @@ struct add_inductive_fn {
void check_intro_rule(unsigned d_idx, intro_rule const & ir) {
expr t = intro_rule_type(ir);
name n = intro_rule_name(ir);
m_tc.check(t, m_level_names);
tc().check(t, m_level_names);
unsigned i = 0;
bool found_rec = false;
while (is_pi(t)) {
if (i < m_num_params) {
if (!m_tc.is_def_eq(binding_domain(t), get_param_type(i)))
if (!tc().is_def_eq(binding_domain(t), get_param_type(i)))
throw kernel_exception(m_env, sstream() << "arg #" << (i + 1) << " of '" << n << "' "
<< "does not match inductive datatypes parameters'");
t = instantiate(binding_body(t), m_param_consts[i]);
} else {
expr s = m_tc.ensure_type(binding_domain(t));
expr s = tc().ensure_type(binding_domain(t));
// the sort is ok IF
// 1- its level is <= inductive datatype level, OR
// 2- m_env is impredicative and inductive datatype is at level 0
@ -454,7 +456,7 @@ struct add_inductive_fn {
unsigned i = 0;
while (is_pi(t)) {
if (i >= m_num_params) {
expr s = m_tc.ensure_type(binding_domain(t));
expr s = tc().ensure_type(binding_domain(t));
if (!is_zero(sort_level(s)))
return true;
}
@ -566,12 +568,12 @@ struct add_inductive_fn {
// populate v using u
for (unsigned i = 0; i < u.size(); i++) {
expr u_i = u[i];
expr u_i_ty = m_tc.whnf(mlocal_type(u_i));
expr u_i_ty = tc().whnf(mlocal_type(u_i));
buffer<expr> xs;
while (is_pi(u_i_ty)) {
expr x = mk_local_for(u_i_ty);
xs.push_back(x);
u_i_ty = m_tc.whnf(instantiate(binding_body(u_i_ty), x));
u_i_ty = tc().whnf(instantiate(binding_body(u_i_ty), x));
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
@ -702,12 +704,12 @@ struct add_inductive_fn {
if (m_dep_elim) {
for (unsigned i = 0; i < u.size(); i++) {
expr u_i = u[i];
expr u_i_ty = m_tc.whnf(mlocal_type(u_i));
expr u_i_ty = tc().whnf(mlocal_type(u_i));
buffer<expr> xs;
while (is_pi(u_i_ty)) {
expr x = mk_local_for(u_i_ty);
xs.push_back(x);
u_i_ty = m_tc.whnf(instantiate(binding_body(u_i_ty), x));
u_i_ty = tc().whnf(instantiate(binding_body(u_i_ty), x));
}
buffer<expr> it_indices;
unsigned it_idx = get_I_indices(u_i_ty, it_indices);
@ -718,7 +720,7 @@ struct add_inductive_fn {
}
expr e_app = mk_app(mk_app(mk_app(e[minor_idx], b), u), v);
expr comp_rhs = Fun(m_param_consts, Fun(C, Fun(e, Fun(b, Fun(u, e_app)))));
m_tc.check(comp_rhs, get_elim_level_param_names());
tc().check(comp_rhs, get_elim_level_param_names());
ext.add_comp_rhs(intro_rule_name(ir), get_elim_name(d_idx), b.size() + u.size(), comp_rhs);
minor_idx++;
}

864
src/kernel/type_checker.cpp
View file

@ -32,482 +32,437 @@ add_cnstr_fn mk_no_contranint_fn() {
return add_cnstr_fn([](constraint const &) { throw no_constraints_allowed_exception(); });
}
/** \brief Auxiliary functional object used to implement type checker. */
struct type_checker::imp {
typedef scoped_map<expr, expr, expr_hash, is_bi_equal_proc> cache;
type_checker::scope::scope(type_checker & tc):
m_tc(tc), m_old_cs_size(m_tc.m_cs.size()), m_old_cache_cs(m_tc.m_cache_cs), m_keep(false) {
m_tc.m_infer_type_cache[0].push();
m_tc.m_infer_type_cache[1].push();
m_tc.m_cache_cs = true;
}
type_checker::scope::~scope() {
if (m_keep) {
// keep results
m_tc.m_infer_type_cache[0].keep();
m_tc.m_infer_type_cache[1].keep();
} else {
// restore caches
m_tc.m_infer_type_cache[0].pop();
m_tc.m_infer_type_cache[1].pop();
m_tc.m_cs.shrink(m_old_cs_size);
}
m_tc.m_cache_cs = m_old_cache_cs;
}
/** \brief Interface type_checker <-> converter */
class converter_context : public converter::context {
imp & m_imp;
public:
converter_context(imp & i):m_imp(i) {}
virtual name mk_fresh_name() { return m_imp.m_gen.next(); }
virtual expr infer_type(expr const & e) { return m_imp.infer_type(e); }
virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); }
};
/** \brief Interface type_checker <-> macro & normalizer_extension */
class type_checker_context : public extension_context {
imp & m_imp;
public:
type_checker_context(imp & i):m_imp(i) {}
virtual environment const & env() const { return m_imp.m_env; }
virtual expr whnf(expr const & e) { return m_imp.whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) { return m_imp.is_def_eq(e1, e2, j); }
virtual expr infer_type(expr const & e) { return m_imp.infer_type(e); }
virtual name mk_fresh_name() { return m_imp.m_gen.next(); }
virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); }
};
environment m_env;
name_generator m_gen;
add_cnstr_fn m_add_cnstr_fn;
std::unique_ptr<converter> m_conv;
// In the type checker cache, we must take into account binder information.
// Examples:
// The type of (lambda x : A, t) is (Pi x : A, typeof(t))
// The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t))
cache m_infer_type_cache[2];
converter_context m_conv_ctx;
type_checker_context m_tc_ctx;
bool m_memoize;
// temp flag
level_param_names m_params;
buffer<constraint> m_cs; // temporary cache of constraints
bool m_cache_cs; // true if we should cache the constraints; false if we should send to m_add_cnstr_fn
// Auxiliary object used to restore cache and filter constraints
// when a failure occurs in the type checker.
// That is, we should not keep cached results, and we should not sent constraints
// when a failure occurs.
struct scope {
imp & m_imp;
unsigned m_old_cs_size;
bool m_old_cache_cs;
bool m_keep;
scope(imp & i):m_imp(i), m_old_cs_size(m_imp.m_cs.size()), m_old_cache_cs(m_imp.m_cache_cs), m_keep(false) {
m_imp.m_infer_type_cache[0].push();
m_imp.m_infer_type_cache[1].push();
m_imp.m_cache_cs = true;
void type_checker::scope::keep() {
m_keep = true;
if (!m_old_cache_cs) {
lean_assert(m_old_cs_size == 0);
// send results to m_add_cnstr_fn
try {
for (auto const & c : m_tc.m_cs)
m_tc.m_add_cnstr_fn(c);
} catch (...) {
m_tc.m_cs.clear();
throw;
}
~scope() {
if (m_keep) {
// keep results
m_imp.m_infer_type_cache[0].keep();
m_imp.m_infer_type_cache[1].keep();
} else {
// restore caches
m_imp.m_infer_type_cache[0].pop();
m_imp.m_infer_type_cache[1].pop();
m_imp.m_cs.shrink(m_old_cs_size);
}
m_imp.m_cache_cs = m_old_cache_cs;
}
void keep() {
m_keep = true;
if (!m_old_cache_cs) {
lean_assert(m_old_cs_size == 0);
// send results to m_add_cnstr_fn
try {
for (auto const & c : m_imp.m_cs)
m_imp.m_add_cnstr_fn(c);
} catch (...) {
m_imp.m_cs.clear();
throw;
}
m_imp.m_cs.clear();
}
}
};
imp(environment const & env, name_generator const & g, add_cnstr_fn const & h, std::unique_ptr<converter> && conv, bool memoize):
m_env(env), m_gen(g), m_add_cnstr_fn(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this),
m_memoize(memoize), m_cache_cs(false) {
m_tc.m_cs.clear();
}
}
optional<expr> expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, m_tc_ctx);
}
optional<expr> type_checker::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, m_tc_ctx);
}
/**
\brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant.
*/
std::pair<expr, expr> open_binding_body(expr const & e) {
expr local = mk_local(m_gen.next(), binding_name(e), binding_domain(e));
return mk_pair(instantiate(binding_body(e), local), local);
}
/**
\brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant.
*/
std::pair<expr, expr> type_checker::open_binding_body(expr const & e) {
expr local = mk_local(m_gen.next(), binding_name(e), binding_domain(e));
return mk_pair(instantiate(binding_body(e), local), local);
}
/** \brief Add given constraint using m_add_cnstr_fn. */
void add_cnstr(constraint const & c) {
if (m_cache_cs)
m_cs.push_back(c);
else
m_add_cnstr_fn(c);
}
/** \brief Add given constraint using m_add_cnstr_fn. */
void type_checker::add_cnstr(constraint const & c) {
if (m_cache_cs)
m_cs.push_back(c);
else
m_add_cnstr_fn(c);
}
/**
\brief Given a metavariable application ((?m t_1) ... t_k)
Create a telescope with the types of t_1 ... t_k.
If t_i is a local constant, then we abstract the occurrences of t_i in the types of t_{i+1} ... t_k.
Return false if the telescope still contains local constants after the abstraction step.
*/
bool meta_to_telescope(expr const & e, buffer<expr> & telescope) {
lean_assert(is_meta(e));
lean_assert(closed(e));
buffer<optional<expr>> locals;
return meta_to_telescope_core(e, telescope, locals);
}
/**
\brief Given a metavariable application ((?m t_1) ... t_k)
Create a telescope with the types of t_1 ... t_k.
If t_i is a local constant, then we abstract the occurrences of t_i in the types of t_{i+1} ... t_k.
Return false if the telescope still contains local constants after the abstraction step.
*/
bool type_checker::meta_to_telescope(expr const & e, buffer<expr> & telescope) {
lean_assert(is_meta(e));
lean_assert(closed(e));
buffer<optional<expr>> locals;
return meta_to_telescope_core(e, telescope, locals);
}
/**
\brief Auxiliary method for meta_to_telescope
*/
bool meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & locals) {
lean_assert(is_meta(e));
if (is_app(e)) {
if (!meta_to_telescope_core(app_fn(e), telescope, locals))
return false;
// infer type and abstract local constants
unsigned n = locals.size();
expr t = replace(infer_type(app_arg(e)),
[&](expr const & e, unsigned offset) -> optional<expr> {
if (is_local(e)) {
for (unsigned i = 0; i < n; i++) {
if (locals[i] && is_eqp(*locals[i], e))
return some_expr(mk_var(offset + n - i - 1));
}
/** \brief Auxiliary method for meta_to_telescope */
bool type_checker::meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & locals) {
lean_assert(is_meta(e));
if (is_app(e)) {
if (!meta_to_telescope_core(app_fn(e), telescope, locals))
return false;
// infer type and abstract local constants
unsigned n = locals.size();
expr t = replace(infer_type(app_arg(e)),
[&](expr const & e, unsigned offset) -> optional<expr> {
if (is_local(e)) {
for (unsigned i = 0; i < n; i++) {
if (locals[i] && is_eqp(*locals[i], e))
return some_expr(mk_var(offset + n - i - 1));
}
return none_expr();
});
if (has_local(t))
return false;
telescope.push_back(t);
if (is_local(e))
locals.push_back(some_expr(e));
else
locals.push_back(none_expr());
}
return true;
}
return none_expr();
});
if (has_local(t))
return false;
telescope.push_back(t);
if (is_local(e))
locals.push_back(some_expr(e));
else
locals.push_back(none_expr());
}
return true;
}
/**
\brief Make sure \c e "is" a sort, and return the corresponding sort.
If \c e is not a sort, then the whnf procedure is invoked. Then, there are
two options: the normalize \c e is a sort, or it is a meta. If it is a meta,
a new constraint is created forcing it to be a sort.
/**
\brief Make sure \c e "is" a sort, and return the corresponding sort.
If \c e is not a sort, then the whnf procedure is invoked. Then, there are
two options: the normalize \c e is a sort, or it is a meta. If it is a meta,
a new constraint is created forcing it to be a sort.
\remark \c s is used to extract position (line number information) when an
error message is produced
*/
expr ensure_sort_core(expr e, expr const & s) {
if (is_sort(e))
return e;
e = whnf(e);
if (is_sort(e)) {
return e;
} else if (is_meta(e)) {
expr r = mk_sort(mk_meta_univ(m_gen.next()));
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
});
add_cnstr(mk_eq_cnstr(e, r, j));
return r;
} else {
// We don't want m_env (i.e., this->m_env) inside the following closure,
// because the type checker may be gone, when the closure is executed.
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, env, o, s); });
}
\remark \c s is used to extract position (line number information) when an
error message is produced
*/
expr type_checker::ensure_sort_core(expr e, expr const & s) {
if (is_sort(e))
return e;
e = whnf(e);
if (is_sort(e)) {
return e;
} else if (is_meta(e)) {
expr r = mk_sort(mk_meta_univ(m_gen.next()));
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
});
add_cnstr(mk_eq_cnstr(e, r, j));
return r;
} else {
// We don't want m_env (i.e., this->m_env) inside the following closure,
// because the type checker may be gone, when the closure is executed.
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, env, o, s); });
}
}
/** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */
expr ensure_pi_core(expr e, expr const & s) {
if (is_pi(e))
return e;
e = whnf(e);
if (is_pi(e)) {
return e;
} else if (is_meta(e)) {
buffer<expr> telescope;
if (!meta_to_telescope(e, telescope)) {
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); });
}
expr ta = mk_sort(mk_meta_univ(m_gen.next()));
expr A = mk_metavar(m_gen.next(), mk_pi(telescope, ta));
expr A_xs = mk_app_vars(A, telescope.size());
telescope.push_back(A_xs);
expr tb = mk_sort(mk_meta_univ(m_gen.next()));
expr B = mk_metavar(m_gen.next(), mk_pi(telescope, tb));
buffer<expr> args;
get_app_args(e, args);
expr A_args = mk_app(A, args.size(), args.data());
args.push_back(Var(0));
expr B_args = mk_app(B, args.size(), args.data());
expr r = mk_pi(g_x_name, A_args, B_args);
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
});
add_cnstr(mk_eq_cnstr(e, r, j));
return r;
} else {
/** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */
expr type_checker::ensure_pi_core(expr e, expr const & s) {
if (is_pi(e))
return e;
e = whnf(e);
if (is_pi(e)) {
return e;
} else if (is_meta(e)) {
buffer<expr> telescope;
if (!meta_to_telescope(e, telescope)) {
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); });
}
}
/**
\brief Create a justification for a let definition type mismatch,
\c e is the let expression, and \c val_type is the type inferred for the let value.
*/
justification mk_let_mismatch_jst(expr const & e, expr const & val_type) {
lean_assert(is_let(e));
return mk_justification(e,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_def_type_mismatch(fmt, m_env, o, let_name(e),
subst.instantiate_metavars_wo_jst(let_type(e)),
subst.instantiate_metavars_wo_jst(val_type));
});
}
static constexpr char const * g_macro_error_msg = "failed to type check macro expansion";
justification mk_macro_jst(expr const & e) {
return mk_justification(e,
[=](formatter const &, options const &, substitution const &) {
return format(g_macro_error_msg);
});
}
void check_level(level const & l, expr const & s) {
if (auto n1 = get_undef_global(l, m_env))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (auto n2 = get_undef_param(l, m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
}
/**
\brief Create a justification for a application type mismatch,
\c e is the application, \c fn_type and \c arg_type are the function and argument type.
*/
struct app_delayed_jst : public delayed_justification {
environment const & m_env;
expr const & m_e;
expr const & m_fn_type;
expr const & m_arg_type;
optional<justification> m_jst;
app_delayed_jst(environment const & env, expr const & e, expr const & f_type, expr const & a_type):
m_env(env), m_e(e), m_fn_type(f_type), m_arg_type(a_type) {}
virtual justification get() {
if (!m_jst) {
m_jst = mk_justification(app_arg(m_e),
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_app_type_mismatch(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(m_e),
subst.instantiate_metavars_wo_jst(binding_domain(m_fn_type)),
subst.instantiate_metavars_wo_jst(m_arg_type));
});
}
return *m_jst;
}
};
/**
\brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
\pre closed(e)
*/
expr infer_type_core(expr const & e, bool infer_only) {
if (is_var(e))
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
lean_assert(closed(e));
check_system("type checker");
if (m_memoize) {
auto it = m_infer_type_cache[infer_only].find(e);
if (it != m_infer_type_cache[infer_only].end())
return it->second;
}
expr r;
switch (e.kind()) {
case expr_kind::Local: case expr_kind::Meta:
r = mlocal_type(e);
break;
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort:
if (!infer_only)
check_level(sort_level(e), e);
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::Constant: {
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_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) {
for (level const & l : ls)
check_level(l, e);
}
r = instantiate_params(d.get_type(), ps, ls);
break;
}
case expr_kind::Macro: {
buffer<expr> arg_types;
for (unsigned i = 0; i < macro_num_args(e); i++)
arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only));
r = macro_def(e).get_type(e, arg_types.data(), m_tc_ctx);
if (!infer_only && macro_def(e).trust_level() >= m_env.trust_lvl()) {
optional<expr> m = expand_macro(e);
if (!m)
throw_kernel_exception(m_env, "failed to expand macro", e);
expr t = infer_type_core(*m, infer_only);
simple_delayed_justification jst([=]() { return mk_macro_jst(e); });
if (!is_def_eq(r, t, jst))
throw_kernel_exception(m_env, g_macro_error_msg, e);
}
break;
}
case expr_kind::Lambda: {
if (!infer_only) {
expr t = infer_type_core(binding_domain(e), infer_only);
ensure_sort_core(t, binding_domain(e));
}
auto b = open_binding_body(e);
r = mk_pi(binding_name(e), binding_domain(e), abstract_local(infer_type_core(b.first, infer_only), b.second), binding_info(e));
break;
}
case expr_kind::Pi: {
expr t1 = ensure_sort_core(infer_type_core(binding_domain(e), infer_only), binding_domain(e));
auto b = open_binding_body(e);
expr t2 = ensure_sort_core(infer_type_core(b.first, infer_only), binding_body(e));
if (m_env.impredicative())
r = mk_sort(mk_imax(sort_level(t1), sort_level(t2)));
else
r = mk_sort(mk_max(sort_level(t1), sort_level(t2)));
break;
}
case expr_kind::App: {
expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), app_fn(e));
if (!infer_only) {
expr a_type = infer_type_core(app_arg(e), infer_only);
app_delayed_jst jst(m_env, e, f_type, a_type);
if (!is_def_eq(a_type, binding_domain(f_type), jst)) {
environment env = m_env;
throw_kernel_exception(m_env, app_arg(e),
[=](formatter const & fmt, options const & o) {
return pp_app_type_mismatch(fmt, env, o, e, binding_domain(f_type), a_type);
expr ta = mk_sort(mk_meta_univ(m_gen.next()));
expr A = mk_metavar(m_gen.next(), mk_pi(telescope, ta));
expr A_xs = mk_app_vars(A, telescope.size());
telescope.push_back(A_xs);
expr tb = mk_sort(mk_meta_univ(m_gen.next()));
expr B = mk_metavar(m_gen.next(), mk_pi(telescope, tb));
buffer<expr> args;
get_app_args(e, args);
expr A_args = mk_app(A, args.size(), args.data());
args.push_back(Var(0));
expr B_args = mk_app(B, args.size(), args.data());
expr r = mk_pi(g_x_name, A_args, B_args);
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
});
}
}
r = instantiate(binding_body(f_type), app_arg(e));
break;
add_cnstr(mk_eq_cnstr(e, r, j));
return r;
} else {
environment env = m_env;
throw_kernel_exception(env, s,
[=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); });
}
}
/**
\brief Create a justification for a let definition type mismatch,
\c e is the let expression, and \c val_type is the type inferred for the let value.
*/
justification type_checker::mk_let_mismatch_jst(expr const & e, expr const & val_type) {
lean_assert(is_let(e));
return mk_justification(e,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_def_type_mismatch(fmt, m_env, o, let_name(e),
subst.instantiate_metavars_wo_jst(let_type(e)),
subst.instantiate_metavars_wo_jst(val_type));
});
}
static constexpr char const * g_macro_error_msg = "failed to type check macro expansion";
justification type_checker::mk_macro_jst(expr const & e) {
return mk_justification(e,
[=](formatter const &, options const &, substitution const &) {
return format(g_macro_error_msg);
});
}
void type_checker::check_level(level const & l, expr const & s) {
if (auto n1 = get_undef_global(l, m_env))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (auto n2 = get_undef_param(l, m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
}
/**
\brief Create a justification for a application type mismatch,
\c e is the application, \c fn_type and \c arg_type are the function and argument type.
*/
struct app_delayed_jst : public delayed_justification {
environment const & m_env;
expr const & m_e;
expr const & m_fn_type;
expr const & m_arg_type;
optional<justification> m_jst;
app_delayed_jst(environment const & env, expr const & e, expr const & f_type, expr const & a_type):
m_env(env), m_e(e), m_fn_type(f_type), m_arg_type(a_type) {}
virtual justification get() {
if (!m_jst) {
m_jst = mk_justification(app_arg(m_e),
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_app_type_mismatch(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(m_e),
subst.instantiate_metavars_wo_jst(binding_domain(m_fn_type)),
subst.instantiate_metavars_wo_jst(m_arg_type));
});
}
case expr_kind::Let:
if (!infer_only) {
ensure_sort_core(infer_type_core(let_type(e), infer_only), let_type(e));
expr val_type = infer_type_core(let_value(e), infer_only);
simple_delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); });
if (!is_def_eq(val_type, let_type(e), jst)) {
environment env = m_env;
throw_kernel_exception(env, e,
[=](formatter const & fmt, options const & o) {
return pp_def_type_mismatch(fmt, env, o, let_name(e), let_type(e), val_type);
});
}
}
r = infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
break;
}
if (m_memoize)
m_infer_type_cache[infer_only].insert(mk_pair(e, r));
return r;
}
expr infer_type(expr const & e) {
scope mk_scope(*this);
expr r = infer_type_core(e, true);
mk_scope.keep();
return r;
}
expr check(expr const & e, level_param_names const & ps) {
scope mk_scope(*this);
flet<level_param_names> updt(m_params, ps);
expr r = infer_type_core(e, false);
mk_scope.keep();
return r;
}
expr ensure_sort(expr const & e, expr const & s) {
scope mk_scope(*this);
expr r = ensure_sort_core(e, s);
mk_scope.keep();
return r;
}
expr ensure_pi(expr const & e, expr const & s) {
scope mk_scope(*this);
expr r = ensure_pi_core(e, s);
mk_scope.keep();
return r;
}
/** \brief Return true iff \c t and \c s are definitionally equal */
bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst) {
scope mk_scope(*this);
bool r = m_conv->is_def_eq(t, s, m_conv_ctx, jst);
if (r) mk_scope.keep();
return r;
}
bool is_def_eq(expr const & t, expr const & s) {
scope mk_scope(*this);
bool r = m_conv->is_def_eq(t, s, m_conv_ctx);
if (r) mk_scope.keep();
return r;
}
bool is_def_eq(expr const & t, expr const & s, justification const & j) {
as_delayed_justification djst(j);
return is_def_eq(t, s, djst);
}
/** \brief Return true iff \c e is a proposition */
bool is_prop(expr const & e) {
scope mk_scope(*this);
bool r = whnf(infer_type(e)) == Bool;
if (r) mk_scope.keep();
return r;
}
expr whnf(expr const & t) { return m_conv->whnf(t, m_conv_ctx); }
void push() {
lean_assert(!m_cache_cs);
m_infer_type_cache[0].push();
m_infer_type_cache[1].push();
}
void pop() {
lean_assert(!m_cache_cs);
m_infer_type_cache[0].pop();
m_infer_type_cache[1].pop();
}
unsigned num_scopes() const {
lean_assert(m_infer_type_cache[0].num_scopes() == m_infer_type_cache[1].num_scopes());
return m_infer_type_cache[0].num_scopes();
return *m_jst;
}
};
/**
\brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
\pre closed(e)
*/
expr type_checker::infer_type_core(expr const & e, bool infer_only) {
if (is_var(e))
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
lean_assert(closed(e));
check_system("type checker");
if (m_memoize) {
auto it = m_infer_type_cache[infer_only].find(e);
if (it != m_infer_type_cache[infer_only].end())
return it->second;
}
expr r;
switch (e.kind()) {
case expr_kind::Local: case expr_kind::Meta:
r = mlocal_type(e);
break;
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort:
if (!infer_only)
check_level(sort_level(e), e);
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::Constant: {
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_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) {
for (level const & l : ls)
check_level(l, e);
}
r = instantiate_params(d.get_type(), ps, ls);
break;
}
case expr_kind::Macro: {
buffer<expr> arg_types;
for (unsigned i = 0; i < macro_num_args(e); i++)
arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only));
r = macro_def(e).get_type(e, arg_types.data(), m_tc_ctx);
if (!infer_only && macro_def(e).trust_level() >= m_env.trust_lvl()) {
optional<expr> m = expand_macro(e);
if (!m)
throw_kernel_exception(m_env, "failed to expand macro", e);
expr t = infer_type_core(*m, infer_only);
simple_delayed_justification jst([=]() { return mk_macro_jst(e); });
if (!is_def_eq(r, t, jst))
throw_kernel_exception(m_env, g_macro_error_msg, e);
}
break;
}
case expr_kind::Lambda: {
if (!infer_only) {
expr t = infer_type_core(binding_domain(e), infer_only);
ensure_sort_core(t, binding_domain(e));
}
auto b = open_binding_body(e);
r = mk_pi(binding_name(e), binding_domain(e), abstract_local(infer_type_core(b.first, infer_only), b.second), binding_info(e));
break;
}
case expr_kind::Pi: {
expr t1 = ensure_sort_core(infer_type_core(binding_domain(e), infer_only), binding_domain(e));
auto b = open_binding_body(e);
expr t2 = ensure_sort_core(infer_type_core(b.first, infer_only), binding_body(e));
if (m_env.impredicative())
r = mk_sort(mk_imax(sort_level(t1), sort_level(t2)));
else
r = mk_sort(mk_max(sort_level(t1), sort_level(t2)));
break;
}
case expr_kind::App: {
expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), app_fn(e));
if (!infer_only) {
expr a_type = infer_type_core(app_arg(e), infer_only);
app_delayed_jst jst(m_env, e, f_type, a_type);
if (!is_def_eq(a_type, binding_domain(f_type), jst)) {
environment env = m_env;
throw_kernel_exception(m_env, app_arg(e),
[=](formatter const & fmt, options const & o) {
return pp_app_type_mismatch(fmt, env, o, e, binding_domain(f_type), a_type);
});
}
}
r = instantiate(binding_body(f_type), app_arg(e));
break;
}
case expr_kind::Let:
if (!infer_only) {
ensure_sort_core(infer_type_core(let_type(e), infer_only), let_type(e));
expr val_type = infer_type_core(let_value(e), infer_only);
simple_delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); });
if (!is_def_eq(val_type, let_type(e), jst)) {
environment env = m_env;
throw_kernel_exception(env, e,
[=](formatter const & fmt, options const & o) {
return pp_def_type_mismatch(fmt, env, o, let_name(e), let_type(e), val_type);
});
}
}
r = infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
break;
}
if (m_memoize)
m_infer_type_cache[infer_only].insert(mk_pair(e, r));
return r;
}
expr type_checker::infer_type(expr const & e) {
scope mk_scope(*this);
expr r = infer_type_core(e, true);
mk_scope.keep();
return r;
}
expr type_checker::check(expr const & e, level_param_names const & ps) {
scope mk_scope(*this);
flet<level_param_names> updt(m_params, ps);
expr r = infer_type_core(e, false);
mk_scope.keep();
return r;
}
expr type_checker::ensure_sort(expr const & e, expr const & s) {
scope mk_scope(*this);
expr r = ensure_sort_core(e, s);
mk_scope.keep();
return r;
}
expr type_checker::ensure_pi(expr const & e, expr const & s) {
scope mk_scope(*this);
expr r = ensure_pi_core(e, s);
mk_scope.keep();
return r;
}
/** \brief Return true iff \c t and \c s are definitionally equal */
bool type_checker::is_def_eq(expr const & t, expr const & s, delayed_justification & jst) {
scope mk_scope(*this);
bool r = m_conv->is_def_eq(t, s, m_conv_ctx, jst);
if (r) mk_scope.keep();
return r;
}
bool type_checker::is_def_eq(expr const & t, expr const & s) {
scope mk_scope(*this);
bool r = m_conv->is_def_eq(t, s, m_conv_ctx);
if (r) mk_scope.keep();
return r;
}
bool type_checker::is_def_eq(expr const & t, expr const & s, justification const & j) {
as_delayed_justification djst(j);
return is_def_eq(t, s, djst);
}
/** \brief Return true iff \c e is a proposition */
bool type_checker::is_prop(expr const & e) {
scope mk_scope(*this);
bool r = whnf(infer_type(e)) == Bool;
if (r) mk_scope.keep();
return r;
}
expr type_checker::whnf(expr const & t) {
return m_conv->whnf(t, m_conv_ctx);
}
void type_checker::push() {
lean_assert(!m_cache_cs);
m_infer_type_cache[0].push();
m_infer_type_cache[1].push();
}
void type_checker::pop() {
lean_assert(!m_cache_cs);
m_infer_type_cache[0].pop();
m_infer_type_cache[1].pop();
}
unsigned type_checker::num_scopes() const {
lean_assert(m_infer_type_cache[0].num_scopes() == m_infer_type_cache[1].num_scopes());
return m_infer_type_cache[0].num_scopes();
}
static add_cnstr_fn g_no_constraint_fn = mk_no_contranint_fn();
type_checker::type_checker(environment const & env, name_generator const & g, add_cnstr_fn const & h,
std::unique_ptr<converter> && conv, bool memoize):
m_ptr(new imp(env, g, h, std::move(conv), memoize)) {}
m_env(env), m_gen(g), m_add_cnstr_fn(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this),
m_memoize(memoize), m_cache_cs(false) {
}
type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize):
type_checker(env, g, g_no_constraint_fn, std::move(conv), memoize) {}
@ -518,17 +473,6 @@ type_checker::type_checker(environment const & env):
type_checker(env, name_generator(g_tmp_prefix), g_no_constraint_fn, mk_default_converter(env), true) {}
type_checker::~type_checker() {}
expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
expr type_checker::check(expr const & t, level_param_names const & ps) { return m_ptr->check(t, ps); }
bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); }
bool type_checker::is_def_eq(expr const & t, expr const & s, justification const & j) { return m_ptr->is_def_eq(t, s, j); }
bool type_checker::is_prop(expr const & t) { return m_ptr->is_prop(t); }
expr type_checker::whnf(expr const & t) { return m_ptr->whnf(t); }
expr type_checker::ensure_pi(expr const & t, expr const & s) { return m_ptr->ensure_pi(t, s); }
expr type_checker::ensure_sort(expr const & t, expr const & s) { return m_ptr->ensure_sort(t, s); }
void type_checker::push() { m_ptr->push(); }
void type_checker::pop() { m_ptr->pop(); }
unsigned type_checker::num_scopes() const { return m_ptr->num_scopes(); }
static void check_no_metavar(environment const & env, expr const & e) {
if (has_metavar(e))

72
src/kernel/type_checker.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include "util/name_generator.h"
#include "util/name_set.h"
#include "util/scoped_map.h"
#include "kernel/environment.h"
#include "kernel/constraint.h"
#include "kernel/converter.h"
@ -35,8 +36,71 @@ public:
The type checker produces constraints, and they are sent to the constraint handler.
*/
class type_checker {
struct imp;
std::unique_ptr<imp> m_ptr;
typedef scoped_map<expr, expr, expr_hash, is_bi_equal_proc> cache;
class converter_context : public converter::context {
type_checker & m_tc;
public:
converter_context(type_checker & tc):m_tc(tc) {}
virtual name mk_fresh_name() { return m_tc.m_gen.next(); }
virtual expr infer_type(expr const & e) { return m_tc.infer_type(e); }
virtual void add_cnstr(constraint const & c) { m_tc.add_cnstr(c); }
};
/** \brief Interface type_checker <-> macro & normalizer_extension */
class type_checker_context : public extension_context {
type_checker & m_tc;
public:
type_checker_context(type_checker & tc):m_tc(tc) {}
virtual environment const & env() const { return m_tc.m_env; }
virtual expr whnf(expr const & e) { return m_tc.whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) { return m_tc.is_def_eq(e1, e2, j); }
virtual expr infer_type(expr const & e) { return m_tc.infer_type(e); }
virtual name mk_fresh_name() { return m_tc.m_gen.next(); }
virtual void add_cnstr(constraint const & c) { m_tc.add_cnstr(c); }
};
environment m_env;
name_generator m_gen;
add_cnstr_fn m_add_cnstr_fn;
std::unique_ptr<converter> m_conv;
// In the type checker cache, we must take into account binder information.
// Examples:
// The type of (lambda x : A, t) is (Pi x : A, typeof(t))
// The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t))
cache m_infer_type_cache[2];
converter_context m_conv_ctx;
type_checker_context m_tc_ctx;
bool m_memoize;
// temp flag
level_param_names m_params;
buffer<constraint> m_cs; // temporary cache of constraints
bool m_cache_cs; // true if we should cache the constraints; false if we should send to m_add_cnstr_fn
struct scope {
type_checker & m_tc;
unsigned m_old_cs_size;
bool m_old_cache_cs;
bool m_keep;
scope(type_checker & tc);
~scope();
void keep();
};
optional<expr> expand_macro(expr const & m);
std::pair<expr, expr> open_binding_body(expr const & e);
void add_cnstr(constraint const & c);
bool meta_to_telescope(expr const & e, buffer<expr> & telescope);
bool meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & locals);
expr ensure_sort_core(expr e, expr const & s);
expr ensure_pi_core(expr e, expr const & s);
justification mk_let_mismatch_jst(expr const & e, expr const & val_type);
justification mk_macro_jst(expr const & e);
void check_level(level const & l, expr const & s);
expr infer_type_core(expr const & e, bool infer_only);
expr infer_type(expr const & e);
bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
public:
/**
\brief Create a type checker for the given environment. The auxiliary names created by this
@ -69,7 +133,7 @@ public:
The result is meaningful only if the constraints sent to the
constraint handler can be solved.
*/
expr infer(expr const & t);
expr infer(expr const & t) { return infer_type(t); }
/**
\brief Type check the given expression, and return the type of \c t.
@ -106,8 +170,6 @@ public:
void pop();
/** \brief Return the number of backtracking points. */
unsigned num_scopes() const;
void swap(type_checker & tc) { std::swap(m_ptr, tc.m_ptr); }
};
/**