From b8dceda9b780768ce09ff921a7dc6d4da5e65121 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Sep 2018 14:06:57 -0700 Subject: [PATCH] chore(kernel): `type_checker::context` ==> `type_checker::state` --- src/kernel/type_checker.cpp | 58 +++++++++++++++++------------------ src/kernel/type_checker.h | 15 +++++---- src/library/compiler/lcnf.cpp | 34 ++++++++++---------- 3 files changed, 53 insertions(+), 54 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 8a87574b5d..1faaf94ce6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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() { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 6c77909389..3125409c18 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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 infer_cache; typedef std::unordered_set 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. diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index e54ff99781..efba556d64 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -21,26 +21,26 @@ Author: Leonardo de Moura namespace lean { class to_lcnf_fn { typedef rb_expr_map cache; - type_checker::context m_ctx; - local_ctx m_lctx; - cache m_cache; - buffer m_fvars; - name m_x; - unsigned m_next_idx{1}; + type_checker::state m_st; + local_ctx m_lctx; + cache m_cache; + buffer 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 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