From 03a99986bbeea2fa474a3b25958893f3fc149aeb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Sep 2018 15:28:03 -0700 Subject: [PATCH] feat(kernel): implement `local_decl` using runtime --- src/kernel/local_ctx.cpp | 45 +++++++++++++------- src/kernel/local_ctx.h | 80 +++++++++++------------------------ src/library/local_context.cpp | 19 ++++++--- src/library/local_context.h | 3 +- 4 files changed, 69 insertions(+), 78 deletions(-) diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp index e2e0d5b16e..18d965f481 100644 --- a/src/kernel/local_ctx.cpp +++ b/src/kernel/local_ctx.cpp @@ -21,31 +21,46 @@ bool is_local_decl_ref(expr const & e) { // TODO(Leo): delete return is_local(e) && local_type(e) == *g_dummy_type; } -void local_decl::cell::dealloc() { - delete this; +local_decl::local_decl():object_ref(*g_dummy_decl) {} + +local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v): + object_ref(mk_cnstr(0, n, un, t, v, sizeof(unsigned) + sizeof(unsigned char))) { + cnstr_set_scalar(raw(), sizeof(object*)*4, 0); + cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char), idx); } -local_decl::cell::cell(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi): - m_name(n), m_user_name(un), m_type(t), m_value(v), m_bi(bi), m_idx(idx), m_rc(1) {} - -local_decl::local_decl():local_decl(*g_dummy_decl) {} - -local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi) { - m_ptr = new cell(idx, n, un, t, v, bi); +local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi): + object_ref(mk_cnstr(0, n, un, t, object_ref(box(0)), sizeof(unsigned) + sizeof(unsigned char))) { + cnstr_set_scalar(raw(), sizeof(object*)*4, static_cast(bi)); + cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char), idx); } -local_decl::local_decl(local_decl const & d, expr const & t, optional const & v): - local_decl(d.m_ptr->m_idx, d.m_ptr->m_name, d.m_ptr->m_user_name, t, v, d.m_ptr->m_bi) {} +local_decl::local_decl(local_decl const & d, expr const & t, expr const & v): + local_decl(d.get_idx(), d.get_name(), d.get_user_name(), t, v) {} + +local_decl::local_decl(local_decl const & d, expr const & t): + local_decl(d.get_idx(), d.get_name(), d.get_user_name(), t, d.get_info()) {} expr local_decl::mk_ref() const { - return mk_local_ref(m_ptr->m_name, m_ptr->m_user_name, m_ptr->m_bi); + // TODO(Leo): + return mk_local_ref(get_name(), get_user_name(), get_info()); } -local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info bi) { +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, bi); + local_decl d(idx, n, un, type, value); + m_name2local_decl.insert(n, d); + m_idx2local_decl.insert(idx, d); + return d; +} + +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); m_idx2local_decl.insert(idx, d); return d; @@ -123,7 +138,7 @@ void initialize_local_ctx() { g_dummy_type = new expr(mk_constant(name::mk_internal_unique_name())); g_dummy_decl = new local_decl(std::numeric_limits::max(), name("__local_decl_for_default_constructor"), name("__local_decl_for_default_constructor"), - mk_Prop(), optional(), mk_binder_info()); + mk_Prop(), mk_binder_info()); } void finalize_local_ctx() { diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index 31c62b8ed6..cd959b525d 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -11,47 +11,32 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -/* TODO(Leo): implement using runtime objects */ -class local_decl { -public: - struct cell { - /* : := - m_user_name is used for interacting with the user, and it may not be not unique. */ - name m_name; /* this one is unique */ - name m_user_name; - expr m_type; - optional m_value; - binder_info m_bi; - unsigned m_idx; - MK_LEAN_RC(); // Declare m_rc counter - void dealloc(); - cell(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, - binder_info bi); - }; -private: - cell * m_ptr; +class local_decl : public object_ref { friend class local_ctx; friend class local_context; friend void initialize_local_ctx(); - local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi); - local_decl(local_decl const & d, expr const & t, optional const & v); + local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v); + local_decl(local_decl const & d, expr const & t, expr const & v); + local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi); + local_decl(local_decl const & d, expr const & t); public: local_decl(); - local_decl(local_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - local_decl(local_decl && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - ~local_decl() { if (m_ptr) m_ptr->dec_ref(); } - local_decl & operator=(local_decl const & s) { LEAN_COPY_REF(s); } - local_decl & operator=(local_decl && s) { LEAN_MOVE_REF(s); } - - friend bool is_eqp(local_decl const & a, local_decl const & b) { return a.m_ptr == b.m_ptr; } - - name const & get_name() const { return m_ptr->m_name; } - name const & get_user_name() const { return m_ptr->m_user_name; } - expr const & get_type() const { return m_ptr->m_type; } - optional const & get_value() const { return m_ptr->m_value; } - binder_info get_info() const { return m_ptr->m_bi; } + local_decl(local_decl const & other):object_ref(other) {} + local_decl(local_decl && other):object_ref(other) {} + 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(); } + name const & get_name() const { return static_cast(cnstr_obj_ref(raw(), 0)); } + name const & get_user_name() const { return static_cast(cnstr_obj_ref(raw(), 1)); } + expr const & get_type() const { return static_cast(cnstr_obj_ref(raw(), 2)); } + optional get_value() const { + /* Remark: if we decide to expose `local_decl` in Lean, we will need to use Lean `option` type. */ + if (is_scalar(cnstr_obj(raw(), 3))) return none_expr(); + else return some_expr(static_cast(cnstr_obj_ref(raw(), 3))); + } + binder_info get_info() const { return static_cast(cnstr_scalar(raw(), sizeof(object*)*4)); } + unsigned get_idx() const { return cnstr_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char)); } expr mk_ref() const; - unsigned get_idx() const { return m_ptr->m_idx; } }; /* Plain local context object used by the kernel type checker. */ @@ -64,35 +49,20 @@ protected: template expr mk_binding(unsigned num, expr const * fvars, expr const & b) const; - local_decl mk_local_decl(name const & n, name const & un, expr const & type, - optional const & value, binder_info bi); + local_decl mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi); + local_decl mk_local_decl(name const & n, name const & un, expr const & type, expr const & value); + public: local_ctx():m_next_idx(0) {} bool empty() const { return m_idx2local_decl.empty(); } - expr mk_local_decl(name const & n, expr const & type, binder_info bi = mk_binder_info()) { - return mk_local_decl(n, n, type, none_expr(), bi).mk_ref(); - } - - expr mk_local_decl(name const & n, expr const & type, expr const & value) { - return mk_local_decl(n, n, type, some_expr(value), mk_binder_info()).mk_ref(); - } - - expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi = mk_binder_info()) { - return mk_local_decl(n, un, type, none_expr(), bi).mk_ref(); - } - - expr mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) { - return mk_local_decl(n, un, type, some_expr(value), mk_binder_info()).mk_ref(); - } - expr mk_local_decl(name_generator & g, name const & un, expr const & type, binder_info bi = mk_binder_info()) { - return mk_local_decl(g.next(), un, type, bi); + return mk_local_decl(g.next(), un, type, bi).mk_ref(); } expr mk_local_decl(name_generator & g, name const & un, expr const & type, expr const & value) { - return mk_local_decl(g.next(), un, type, some_expr(value), mk_binder_info()).mk_ref(); + return mk_local_decl(g.next(), un, type, value).mk_ref(); } /** \brief Return the local declarations for the given reference. diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index c4b559df09..cd3683f244 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -148,7 +148,7 @@ void local_context::erase_user_name(local_decl const & 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 = local_ctx::mk_local_decl(n, un, type, value, bi); + local_decl d = value ? local_ctx::mk_local_decl(n, un, type, *value) : local_ctx::mk_local_decl(n, un, type, bi); insert_user_name(d); return d.mk_ref(); } @@ -213,7 +213,11 @@ void local_context::pop_local_decl() { bool local_context::rename_user_name(name const & from, name const & to) { if (auto d = find_local_decl_from_user_name(from)) { erase_user_name(*d); - local_decl new_d(d->get_idx(), d->get_name(), to, d->get_type(), d->get_value(), d->get_info()); + local_decl new_d; + if (d->get_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); insert_user_name(new_d); @@ -388,11 +392,12 @@ 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.m_ptr->m_type); - optional new_value; - if (d.m_ptr->m_value) - new_value = mctx.instantiate_mvars(*d.m_ptr->m_value); - local_decl new_d(d, new_type, new_value); + 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)); + 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.insert_user_name(d); diff --git a/src/library/local_context.h b/src/library/local_context.h index 0f94005c80..ea2495565e 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -53,7 +53,8 @@ class local_context : public local_ctx { optional const & value, binder_info bi); static local_decl update_local_decl(local_decl const & d, expr const & t, optional const & v) { - return local_decl(d, t, v); + if (v) return local_decl(d, t, *v); + else return local_decl(d, t); } public: local_context() {}