From ae97cfdd6877b2a5e433c6d5a88e1a24db449b14 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Aug 2019 11:50:20 -0700 Subject: [PATCH] feat(kernel/local_ctx): use `LocalContext` --- src/kernel/local_ctx.cpp | 52 +++++++++++++------------ src/kernel/local_ctx.h | 33 +++++++--------- src/library/equations_compiler/util.cpp | 13 +++---- src/library/local_context.cpp | 50 ++++++++++-------------- src/library/local_context.h | 20 ++++------ src/library/message_builder.cpp | 3 ++ 6 files changed, 78 insertions(+), 93 deletions(-) diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp index 24dd94fad1..e63a6cf035 100644 --- a/src/kernel/local_ctx.cpp +++ b/src/kernel/local_ctx.cpp @@ -43,37 +43,42 @@ expr local_decl::mk_ref() const { return mk_local_ref(get_name(), get_user_name(), get_info()); } +object * mk_empty_local_ctx_core(object*); +uint8 local_ctx_is_empty_core(object*); +object * local_ctx_mk_local_decl_core(object * lctx, object * name, object * user_name, object * expr, uint8 bi); +object * local_ctx_mk_let_decl_core(object * lctx, object * name, object * user_name, object * type, object * value); +object * local_ctx_find_core(object * lctx, object * name); +object * local_ctx_erase_core(object * lctx, object * name); + +local_ctx::local_ctx():object_ref(mk_empty_local_ctx_core(box(0))) { +} + +bool local_ctx::empty() const { + return local_ctx_is_empty_core(to_obj_arg()); +} + local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) { - lean_assert(!m_name2local_decl.contains(n)); - unsigned idx = m_next_idx; - m_next_idx++; - local_decl d(idx, n, un, type, value); - m_name2local_decl.insert(n, d); - return d; + object * p = local_ctx_mk_let_decl_core(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg()); + local_decl decl(cnstr_get(p, 0)); + m_obj = cnstr_get(p, 1); + free_heap_obj(p); + return decl; } local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi) { - lean_assert(!m_name2local_decl.contains(n)); - unsigned idx = m_next_idx; - m_next_idx++; - local_decl d(idx, n, un, type, bi); - m_name2local_decl.insert(n, d); - return d; + object * p = local_ctx_mk_local_decl_core(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), static_cast(bi)); + local_decl decl(cnstr_get(p, 0)); + m_obj = cnstr_get(p, 1); + free_heap_obj(p); + return decl; } optional local_ctx::find_local_decl(name const & n) const { - if (auto r = m_name2local_decl.find(n)) - return optional(*r); - else - return optional(); + return to_optional(local_ctx_find_core(to_obj_arg(), n.to_obj_arg())); } -optional local_ctx::find_local_decl(expr const & e) const { - return find_local_decl(local_name(e)); -} - -local_decl const & local_ctx::get_local_decl(name const & n) const { - if (local_decl const * r = m_name2local_decl.find(n)) +local_decl local_ctx::get_local_decl(name const & n) const { + if (optional r = find_local_decl(n)) return *r; else throw exception(sstream() << "unknown free variable: " << n); @@ -85,8 +90,7 @@ expr local_ctx::get_local(name const & n) const { } void local_ctx::clear(local_decl const & d) { - lean_assert(find_local_decl(d.get_name())); - m_name2local_decl.erase(d.get_name()); + m_obj = local_ctx_erase_core(m_obj, d.get_name().to_obj_arg()); } template diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index 1a1daed55f..8da39cafb3 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -28,6 +28,8 @@ public: local_decl(); local_decl(local_decl const & other):object_ref(other) {} local_decl(local_decl && other):object_ref(other) {} + local_decl(obj_arg o):object_ref(o) {} + local_decl(b_obj_arg o, bool):object_ref(o, true) {} local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; } local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; } friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); } @@ -47,16 +49,17 @@ public: }; /* Plain local context object used by the kernel type checker. */ -class local_ctx { +class local_ctx : public object_ref { protected: - unsigned m_next_idx; - name_map m_name2local_decl; // mapping from unique identifier to local_decl - template expr mk_binding(unsigned num, expr const * fvars, expr const & b) const; public: - local_ctx():m_next_idx(0) {} + local_ctx(); + local_ctx(local_ctx const & other):object_ref(other) {} + local_ctx(local_ctx && other):object_ref(other) {} + local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; } + local_ctx & operator=(local_ctx && other) { object_ref::operator=(other); return *this; } - bool empty() const { return m_name2local_decl.empty(); } + bool empty() const; /* Low level `mk_local_decl` */ local_decl mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi); @@ -71,14 +74,12 @@ public: return mk_local_decl(g.next(), un, type, value).mk_ref(); } - /** \brief Return the local declarations for the given reference. - - \pre is_fvar(e) */ - optional find_local_decl(expr const & e) const; + /** \brief Return the local declarations for the given reference. */ optional find_local_decl(name const & n) const; + optional find_local_decl(expr const & e) const { return find_local_decl(fvar_name(e)); } - local_decl const & get_local_decl(name const & n) const; - local_decl const & get_local_decl(expr const & e) const { return get_local_decl(fvar_name(e)); } + local_decl get_local_decl(name const & n) const; + local_decl get_local_decl(expr const & e) const { return get_local_decl(fvar_name(e)); } /* \brief Return type of the given free variable. \pre is_fvar(e) */ @@ -99,14 +100,6 @@ public: expr mk_pi(expr const & fvar, expr const & e) { return mk_pi(1, &fvar, e); } expr mk_lambda(std::initializer_list const & fvars, expr const & e) { return mk_lambda(fvars.size(), fvars.begin(), e); } expr mk_pi(std::initializer_list const & fvars, expr const & e) { return mk_pi(fvars.size(), fvars.begin(), e); } - - friend bool is_decl_eqp(local_ctx const & ctx1, local_ctx const & ctx2) { - return is_eqp(ctx1.m_name2local_decl, ctx2.m_name2local_decl); - } - - friend bool equal_locals(local_ctx const & ctx1, local_ctx const & ctx2) { - return is_decl_eqp(ctx1, ctx2) || ctx1.m_name2local_decl.equal_keys(ctx2.m_name2local_decl); - } }; void initialize_local_ctx(); diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index e40a69f7b4..ee1498de18 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -240,15 +240,14 @@ list erase_inaccessible_annotations(list const & es) { local_context erase_inaccessible_annotations(local_context const & lctx) { local_context r; - r.m_next_idx = lctx.m_next_idx; lctx.m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { expr new_type = erase_inaccessible_annotations(d.get_type()); - optional new_value; - if (auto val = d.get_value()) - new_value = erase_inaccessible_annotations(*val); - auto new_d = local_context::update_local_decl(d, new_type, new_value); - r.m_name2local_decl.insert(d.get_name(), new_d); - r.m_idx2local_decl.insert(d.get_idx(), new_d); + if (auto val = d.get_value()) { + expr new_value = erase_inaccessible_annotations(*val); + r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, new_value); + } else { + r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, d.get_info()); + } }); return r; } diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 767df87c7f..f2b4de467b 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -125,6 +125,18 @@ bool depends_on(expr const & e, metavar_context const & mctx, local_context cons return depends_on_fn(mctx, lctx, num, locals)(e); } +local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi) { + local_decl d = local_ctx::mk_local_decl(n, un, type, bi); + m_idx2local_decl.insert(d.get_idx(), d); + return d; +} + +local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value) { + local_decl d = local_ctx::mk_local_decl(n, un, type, value); + m_idx2local_decl.insert(d.get_idx(), d); + return d; +} + expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info bi) { local_decl d = value ? local_ctx::mk_local_decl(n, un, type, *value) : local_ctx::mk_local_decl(n, un, type, bi); m_idx2local_decl.insert(d.get_idx(), d); @@ -165,6 +177,7 @@ void local_context::clear(local_decl const & d) { lean_assert(find_local_decl(d.get_name())); local_ctx::clear(d); m_idx2local_decl.erase(d.get_idx()); + lean_assert(!find_local_decl(d.get_name())); } optional local_context::find_local_decl_from_user_name(name const & n) const { @@ -196,23 +209,7 @@ void local_context::for_each_after(local_decl const & d, std::functionget_value()) - new_d = local_decl(d->get_idx(), d->get_name(), to, d->get_type(), *d->get_value()); - else - new_d = local_decl(d->get_idx(), d->get_name(), to, d->get_type(), d->get_info()); - m_idx2local_decl.insert(d->get_idx(), new_d); - m_name2local_decl.insert(d->get_name(), new_d); - return true; - } else { - return false; - } + clear(d); } optional local_context::has_dependencies(local_decl const & d, metavar_context const & mctx) const { @@ -229,15 +226,15 @@ optional local_context::has_dependencies(local_decl const & d, metav bool local_context::is_subset_of(name_set const & ls) const { // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class - return !static_cast(m_name2local_decl.find_if([&](name const & n, local_decl const &) { - return !ls.contains(n); + return !static_cast(m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { + return !ls.contains(d.get_name()); })); } bool local_context::is_subset_of(local_context const & ctx) const { // TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class - return !static_cast(m_name2local_decl.find_if([&](name const & n, local_decl const &) { - return !ctx.m_name2local_decl.contains(n); + return !static_cast(m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { + return !ctx.find_local_decl(d.get_name()); })); } @@ -250,8 +247,7 @@ local_context local_context::remove(buffer const & locals) const { local_context r = *this; for (expr const & l : locals) { local_decl d = get_local_decl(l); - r.m_name2local_decl.erase(local_name(l)); - r.m_idx2local_decl.erase(d.get_idx()); + r.clear(d); } lean_assert(r.well_formed()); return r; @@ -375,16 +371,12 @@ name local_context::get_unused_name(name const & suggestion) const { local_context local_context::instantiate_mvars(metavar_context & mctx) const { local_context r; - r.m_next_idx = m_next_idx; m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { expr new_type = mctx.instantiate_mvars(d.get_type()); - local_decl new_d; if (auto v = d.get_value()) - new_d = local_decl(d, new_type, mctx.instantiate_mvars(*v)); + r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, mctx.instantiate_mvars(*v)); else - new_d = local_decl(d, new_type); - r.m_name2local_decl.insert(d.get_name(), new_d); - r.m_idx2local_decl.insert(d.get_idx(), new_d); + r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, d.get_info()); }); return r; } diff --git a/src/library/local_context.h b/src/library/local_context.h index 9d2271c783..1b0f960876 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -51,11 +51,15 @@ class local_context : public local_ctx { else return local_decl(d, t); } + local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi); + local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value); + public: local_context() {} - explicit local_context(local_ctx const & lctx): local_ctx(lctx) {} - - bool empty() const { return m_idx2local_decl.empty(); } + local_context(local_context const & lctx):local_ctx(lctx), m_idx2local_decl(lctx.m_idx2local_decl) {} + local_context(local_context && lctx):local_ctx(lctx), m_idx2local_decl(lctx.m_idx2local_decl) {} + local_context & operator=(local_context const & other) { local_ctx::operator=(other); m_idx2local_decl = other.m_idx2local_decl; return *this; } + local_context & operator=(local_context && other) { local_ctx::operator=(other); m_idx2local_decl = other.m_idx2local_decl; return *this; } expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info()); expr mk_local_decl(expr const & type, expr const & value); @@ -76,8 +80,6 @@ public: optional find_last_local_decl() const; local_decl get_last_local_decl() const; - bool rename_user_name(name const & from, name const & to); - /** \brief Execute fn for each local declaration created after \c d. */ void for_each_after(local_decl const & d, std::function const & fn) const; @@ -129,14 +131,6 @@ public: /** \brief Remove the given local decl. */ void clear(local_decl const & d); - friend bool is_decl_eqp(local_context const & ctx1, local_context const & ctx2) { - return is_eqp(ctx1.m_name2local_decl, ctx2.m_name2local_decl); - } - - friend bool equal_locals(local_context const & ctx1, local_context const & ctx2) { - return is_decl_eqp(ctx1, ctx2) || ctx1.m_name2local_decl.equal_keys(ctx2.m_name2local_decl); - } - /** \brief Erase inaccessible annotations from the local context. This function is defined in the file library/equations_compiler/util.h. It is a little bit hackish (like instantiate_mvars) since it reuses the names diff --git a/src/library/message_builder.cpp b/src/library/message_builder.cpp index 44964ae93f..5e7ea6c8bb 100644 --- a/src/library/message_builder.cpp +++ b/src/library/message_builder.cpp @@ -77,6 +77,8 @@ message_builder & message_builder::set_exception(std::exception const & ex, bool } else if (dynamic_cast(&ex)) { *this << "invalid declaration, it contains free variables"; } else if (auto kex = dynamic_cast(&ex)) { + // TODO(Leo) FIX +#if 0 type_context_old ctx(kex->get_environment(), get_global_ios().get_options(), metavar_context(), local_context(kex->get_local_ctx())); auto fmt = get_global_ios().get_formatter_factory()(kex->get_environment(), get_global_ios().get_options(), @@ -99,6 +101,7 @@ message_builder & message_builder::set_exception(std::exception const & ex, bool } else { lean_unreachable(); } +#endif } else { *this << ex.what(); }