max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel): type_checker::context ==> type_checker::state

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-13 14:06:57 -07:00
parent c02e2d3b56
commit b8dceda9b7
3 changed files with 53 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

58
src/kernel/type_checker.cpp
View file

@ -24,7 +24,7 @@ namespace lean {
static name * g_kernel_fresh = nullptr;
static expr * g_dont_care = nullptr;
type_checker::context::context(environment const & env):
type_checker::state::state(environment const & env):
m_env(env), m_ngen(*g_kernel_fresh) {}
/** \brief Make sure \c e "is" a sort, and return the corresponding sort.
@ -96,7 +96,7 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
expr e = _e;
while (is_lambda(e)) {
expr d = instantiate_rev(binding_domain(e), fvars.size(), fvars.data());
expr fvar = m_lctx.mk_local_decl(m_ctx->m_ngen, binding_name(e), d, binding_info(e));
expr fvar = m_lctx.mk_local_decl(m_st->m_ngen, binding_name(e), d, binding_info(e));
fvars.push_back(fvar);
if (!infer_only) {
ensure_sort_core(infer_type_core(d, infer_only), d);
@ -116,7 +116,7 @@ expr type_checker::infer_pi(expr const & _e, bool infer_only) {
expr d = instantiate_rev(binding_domain(e), fvars.size(), fvars.data());
expr t1 = ensure_sort_core(infer_type_core(d, infer_only), d);
us.push_back(sort_level(t1));
expr fvar = m_lctx.mk_local_decl(m_ctx->m_ngen, binding_name(e), d, binding_info(e));
expr fvar = m_lctx.mk_local_decl(m_st->m_ngen, binding_name(e), d, binding_info(e));
fvars.push_back(fvar);
e = binding_body(e);
}
@ -167,7 +167,7 @@ expr type_checker::infer_let(expr const & _e, bool infer_only) {
while (is_let(e)) {
expr type = instantiate_rev(let_type(e), fvars.size(), fvars.data());
expr val = instantiate_rev(let_value(e), fvars.size(), fvars.data());
expr fvar = m_lctx.mk_local_decl(m_ctx->m_ngen, let_name(e), type, val);
expr fvar = m_lctx.mk_local_decl(m_st->m_ngen, let_name(e), type, val);
fvars.push_back(fvar);
if (!infer_only) {
ensure_sort_core(infer_type_core(type, infer_only), type);
@ -227,8 +227,8 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
lean_assert(!has_loose_bvars(e));
check_system("type checker");
auto it = m_ctx->m_infer_type[infer_only].find(e);
if (it != m_ctx->m_infer_type[infer_only].end())
auto it = m_st->m_infer_type[infer_only].find(e);
if (it != m_st->m_infer_type[infer_only].end())
return it->second;
expr r;
@ -251,7 +251,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
case expr_kind::Let: r = infer_let(e, infer_only); break;
}
m_ctx->m_infer_type[infer_only].insert(mk_pair(e, r));
m_st->m_infer_type[infer_only].insert(mk_pair(e, r));
return r;
}
@ -347,8 +347,8 @@ expr type_checker::whnf_core(expr const & e) {
}
// check cache
auto it = m_ctx->m_whnf_core.find(e);
if (it != m_ctx->m_whnf_core.end())
auto it = m_st->m_whnf_core.find(e);
if (it != m_st->m_whnf_core.end())
return it->second;
// do the actual work
@ -396,7 +396,7 @@ expr type_checker::whnf_core(expr const & e) {
break;
}
m_ctx->m_whnf_core.insert(mk_pair(e, r));
m_st->m_whnf_core.insert(mk_pair(e, r));
return r;
}
@ -455,8 +455,8 @@ expr type_checker::whnf(expr const & e) {
}
// check cache
auto it = m_ctx->m_whnf.find(e);
if (it != m_ctx->m_whnf.end())
auto it = m_st->m_whnf.find(e);
if (it != m_st->m_whnf.end())
return it->second;
expr t = e;
@ -466,7 +466,7 @@ expr type_checker::whnf(expr const & e) {
t = *next_t;
} else {
auto r = t1;
m_ctx->m_whnf.insert(mk_pair(e, r));
m_st->m_whnf.insert(mk_pair(e, r));
return r;
}
}
@ -497,7 +497,7 @@ bool type_checker::is_def_eq_binding(expr t, expr s) {
// free variable is used inside t or s
if (!var_s_type)
var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
subst.push_back(m_lctx.mk_local_decl(m_ctx->m_ngen, binding_name(s), *var_s_type, binding_info(s)));
subst.push_back(m_lctx.mk_local_decl(m_st->m_ngen, binding_name(s), *var_s_type, binding_info(s)));
} else {
subst.push_back(*g_dont_care); // don't care
}
@ -530,7 +530,7 @@ bool type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
if (m_ctx->m_eqv_manager.is_equiv(t, s, use_hash))
if (m_st->m_eqv_manager.is_equiv(t, s, use_hash))
return l_true;
if (t.kind() == s.kind()) {
switch (t.kind()) {
@ -615,21 +615,21 @@ bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
bool type_checker::failed_before(expr const & t, expr const & s) const {
if (hash(t) < hash(s)) {
return m_ctx->m_failure.find(mk_pair(t, s)) != m_ctx->m_failure.end();
return m_st->m_failure.find(mk_pair(t, s)) != m_st->m_failure.end();
} else if (hash(t) > hash(s)) {
return m_ctx->m_failure.find(mk_pair(s, t)) != m_ctx->m_failure.end();
return m_st->m_failure.find(mk_pair(s, t)) != m_st->m_failure.end();
} else {
return
m_ctx->m_failure.find(mk_pair(t, s)) != m_ctx->m_failure.end() ||
m_ctx->m_failure.find(mk_pair(s, t)) != m_ctx->m_failure.end();
m_st->m_failure.find(mk_pair(t, s)) != m_st->m_failure.end() ||
m_st->m_failure.find(mk_pair(s, t)) != m_st->m_failure.end();
}
}
void type_checker::cache_failure(expr const & t, expr const & s) {
if (hash(t) <= hash(s))
m_ctx->m_failure.insert(mk_pair(t, s));
m_st->m_failure.insert(mk_pair(t, s));
else
m_ctx->m_failure.insert(mk_pair(s, t));
m_st->m_failure.insert(mk_pair(s, t));
}
static name * g_id_delta = nullptr;
@ -760,29 +760,29 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
bool type_checker::is_def_eq(expr const & t, expr const & s) {
bool r = is_def_eq_core(t, s);
if (r)
m_ctx->m_eqv_manager.add_equiv(t, s);
m_st->m_eqv_manager.add_equiv(t, s);
return r;
}
type_checker::type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only):
m_ctx_owner(true), m_ctx(new context(env)),
m_st_owner(true), m_st(new state(env)),
m_lctx(lctx), m_non_meta_only(non_meta_only), m_lparams(nullptr) {
}
type_checker::type_checker(context & ctx, local_ctx const & lctx, bool non_meta_only):
m_ctx_owner(false), m_ctx(&ctx), m_lctx(lctx),
type_checker::type_checker(state & st, local_ctx const & lctx, bool non_meta_only):
m_st_owner(false), m_st(&st), m_lctx(lctx),
m_non_meta_only(non_meta_only), m_lparams(nullptr) {
}
type_checker::type_checker(type_checker && src):
m_ctx_owner(src.m_ctx_owner), m_ctx(src.m_ctx), m_lctx(std::move(src.m_lctx)),
m_st_owner(src.m_st_owner), m_st(src.m_st), m_lctx(std::move(src.m_lctx)),
m_non_meta_only(src.m_non_meta_only), m_lparams(src.m_lparams) {
src.m_ctx_owner = false;
src.m_st_owner = false;
}
type_checker::~type_checker() {
if (m_ctx_owner)
delete m_ctx;
if (m_st_owner)
delete m_st;
}
void initialize_type_checker() {

15
src/kernel/type_checker.h
View file

@ -22,7 +22,7 @@ namespace lean {
type \c A is convertible to a type \c B, etc. */
class type_checker {
public:
class context {
class state {
typedef expr_map<expr> infer_cache;
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
environment m_env;
@ -34,14 +34,14 @@ public:
expr_pair_set m_failure;
friend type_checker;
public:
context(environment const & env);
state(environment const & env);
environment & env() { return m_env; }
environment const & env() const { return m_env; }
name_generator & ngen() { return m_ngen; }
};
private:
bool m_ctx_owner;
context * m_ctx;
bool m_st_owner;
state * m_st;
local_ctx m_lctx;
bool m_non_meta_only;
/* When `m_lparams != nullptr, the `check` method makes sure all level parameters
@ -90,16 +90,15 @@ private:
expr check_ignore_undefined_universes(expr const & e);
public:
/** \brief Create a type checker for the given environment. */
type_checker(context & ctx, local_ctx const & lctx, bool non_meta_only = true);
type_checker(state & st, local_ctx const & lctx, bool non_meta_only = true);
type_checker(state & st, bool non_meta_only = true):type_checker(st, local_ctx(), non_meta_only) {}
type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only = true);
type_checker(environment const & env, bool non_meta_only = true):type_checker(env, local_ctx(), non_meta_only) {}
type_checker(context & ctx, bool non_meta_only = true):type_checker(ctx, local_ctx(), non_meta_only) {}
type_checker(type_checker &&);
type_checker(type_checker const &) = delete;
~type_checker();
environment const & env() const { return m_ctx->m_env; }
environment const & env() const { return m_st->m_env; }
/** \brief Return the type of \c t.
It does not check whether the input expression is type correct or not.

34
src/library/compiler/lcnf.cpp
View file

@ -21,26 +21,26 @@ Author: Leonardo de Moura
namespace lean {
class to_lcnf_fn {
typedef rb_expr_map<expr> cache;
type_checker::context m_ctx;
local_ctx m_lctx;
cache m_cache;
buffer<expr> m_fvars;
name m_x;
unsigned m_next_idx{1};
type_checker::state m_st;
local_ctx m_lctx;
cache m_cache;
buffer<expr> m_fvars;
name m_x;
unsigned m_next_idx{1};
public:
to_lcnf_fn(environment const & env, local_ctx const & lctx):
m_ctx(env), m_lctx(lctx), m_x("_x") {}
m_st(env), m_lctx(lctx), m_x("_x") {}
environment & env() { return m_ctx.env(); }
environment & env() { return m_st.env(); }
name_generator & ngen() { return m_ctx.ngen(); }
name_generator & ngen() { return m_st.ngen(); }
expr infer_type(expr const & e) { return type_checker(m_ctx, m_lctx).infer(e); }
expr infer_type(expr const & e) { return type_checker(m_st, m_lctx).infer(e); }
expr whnf(expr const & e) { return type_checker(m_ctx, m_lctx).whnf(e); }
expr whnf(expr const & e) { return type_checker(m_st, m_lctx).whnf(e); }
expr whnf_infer_type(expr const & e) {
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
return tc.whnf(tc.infer(e));
}
@ -180,7 +180,7 @@ public:
return visit(eta_expand(mk_app(fn, args), basic_arity - args.size()), root);
}
lean_assert(args.size() >= basic_arity);
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
expr lhs = tc.whnf(args[nparams + nindices + 1]);
expr rhs = tc.whnf(args[nparams + nindices + 2]);
optional<name> lhs_constructor = is_constructor_app(env(), lhs);
@ -226,7 +226,7 @@ public:
minor_idx = 5;
else
minor_idx = 3;
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
expr minor = args[minor_idx];
expr minor_type = tc.whnf(tc.infer(minor));
expr eq_rec_type = tc.whnf(tc.infer(mk_app(fn, eq_rec_nargs, args.data())));
@ -250,7 +250,7 @@ public:
} else {
/* Remark: args.size() may be greater than 2, but
(lc_unreachable a_1 ... a_n) is equivalent to (lc_unreachable) */
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
expr type = tc.whnf(tc.infer(mk_app(fn, args)));
level lvl = sort_level(tc.ensure_type(type));
return mk_let_decl(mk_app(mk_constant(get_lc_unreachable_name(), {lvl}), type), root);
@ -297,7 +297,7 @@ public:
if (is_lc_proof(e)) return false;
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
e_type = tc.whnf(e_type);
if (is_sort(e_type)) {
return false;
@ -460,7 +460,7 @@ public:
}
{
type_checker tc(m_ctx, m_lctx);
type_checker tc(m_st, m_lctx);
expr type = tc.whnf(tc.infer(e));
if (is_sort(type)) {
// Types are not pre-processed