From 18cfce60b93a1a8ce568f9db8c1efa35f61a574d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 08:13:27 -0700 Subject: [PATCH] refactor(frontends/lean/local_context): simplify local_context representation --- src/frontends/lean/local_context.cpp | 75 +++++++++++++++++++--------- src/frontends/lean/local_context.h | 5 +- 2 files changed, 54 insertions(+), 26 deletions(-) diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp index ad558e817..940d9f527 100644 --- a/src/frontends/lean/local_context.cpp +++ b/src/frontends/lean/local_context.cpp @@ -5,9 +5,36 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/abstract.h" +#include "kernel/replace_fn.h" #include "frontends/lean/local_context.h" namespace lean { +/** \brief Given a list of local constants \c locals + (x_n : A_n) ... (x_0 : A_0) + and a term \c e + t[x_0, ..., x_n] + return + t[#n, ..., #0] +*/ +expr abstract_locals(expr const & e, list const & locals) { + lean_assert(std::all_of(locals.begin(), locals.end(), [](expr const & e) { return closed(e) && is_local(e); })); + if (!has_local(e)) + return e; + return replace(e, [=](expr const & m, unsigned offset) -> optional { + if (!has_local(m)) + return some_expr(m); // expression m does not contain local constants + if (is_local(m)) { + unsigned i = 0; + for (expr const & l : locals) { + if (mlocal_name(l) == mlocal_name(m)) + return some_expr(copy_tag(m, mk_var(offset + i))); + i++; + } + } + return none_expr(); + }); +} + local_context::local_context(name const & prefix):m_ngen(prefix) {} local_context::local_context(name const & prefix, list const & ctx): m_ngen(prefix) { @@ -16,31 +43,32 @@ local_context::local_context(name const & prefix, list const & ctx): void local_context::set_ctx(list const & ctx) { m_ctx = ctx; - m_ctx_buffer.clear(); - m_ctx_domain_buffer.clear(); - to_buffer(ctx, m_ctx_buffer); - std::reverse(m_ctx_buffer.begin(), m_ctx_buffer.end()); - for (unsigned i = 0; i < m_ctx_buffer.size(); i++) { - m_ctx_domain_buffer.push_back(abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.data())); + buffer tmp; + list it = ctx; + while (it) { + tmp.push_back(abstract_locals(head(it), tail(it))); + it = tail(it); } + m_ctx_abstracted = to_list(tmp.begin(), tmp.end()); + lean_assert(std::all_of(m_ctx_abstracted.begin(), m_ctx_abstracted.end(), [](expr const & e) { return is_local(e); })); } expr local_context::pi_abstract_context(expr e, tag g) const { - e = abstract_locals(e, m_ctx_buffer.size(), m_ctx_buffer.data()); - unsigned i = m_ctx_domain_buffer.size(); - while (i > 0) { - --i; - expr const & l = m_ctx_domain_buffer[i]; + e = abstract_locals(e, m_ctx); + for (expr const & l : m_ctx_abstracted) e = mk_pi(local_pp_name(l), mlocal_type(l), e, local_info(l)).set_tag(g); - } return e; } +static expr apply_context_core(expr const & f, list const & ctx, tag g) { + if (ctx) + return mk_app(apply_context_core(f, tail(ctx), g), head(ctx)).set_tag(g); + else + return f; +} + expr local_context::apply_context(expr const & f, tag g) const { - expr r = f; - for (unsigned i = 0; i < m_ctx_buffer.size(); i++) - r = mk_app(r, m_ctx_buffer[i]).set_tag(g); - return r; + return apply_context_core(f, m_ctx, g); } expr local_context::mk_type_metavar(tag g) { @@ -69,9 +97,11 @@ expr local_context::mk_meta(optional const & type, tag g) { } void local_context::add_local(expr const & l) { - m_ctx = cons(l, m_ctx); - m_ctx_domain_buffer.push_back(abstract_locals(l, m_ctx_buffer.size(), m_ctx_buffer.data())); - m_ctx_buffer.push_back(l); + lean_assert(is_local(l)); + m_ctx_abstracted = cons(abstract_locals(l, m_ctx), m_ctx_abstracted); + m_ctx = cons(l, m_ctx); + lean_assert(length(m_ctx) == length(m_ctx_abstracted)); + lean_assert(is_local(head(m_ctx_abstracted))); } optional local_context::find_meta(name const & n) const { @@ -86,10 +116,9 @@ list const & local_context::get_data() const { } local_context::scope::scope(local_context & main): - m_main(main), m_old_ctx(main.m_ctx), m_old_sz(main.m_ctx_buffer.size()) {} + m_main(main), m_old_ctx(main.m_ctx), m_old_ctx_abstracted(main.m_ctx_abstracted) {} local_context::scope::~scope() { - m_main.m_ctx = m_old_ctx; - m_main.m_ctx_buffer.shrink(m_old_sz); - m_main.m_ctx_domain_buffer.shrink(m_old_sz); + m_main.m_ctx = m_old_ctx; + m_main.m_ctx_abstracted = m_old_ctx_abstracted; } } diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h index 903a44ca7..731d9b95a 100644 --- a/src/frontends/lean/local_context.h +++ b/src/frontends/lean/local_context.h @@ -19,8 +19,7 @@ class local_context { name_generator m_ngen; mvar2meta m_mvar2meta; list m_ctx; // current local context: a list of local constants - buffer m_ctx_buffer; // m_ctx as a buffer - buffer m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg + list m_ctx_abstracted; // m_ctx where elements have been abstracted public: local_context(name const & prefix); local_context(name const & prefix, list const & ctx); @@ -94,7 +93,7 @@ public: class scope { local_context & m_main; list m_old_ctx; - unsigned m_old_sz; + list m_old_ctx_abstracted; public: scope(local_context & main); ~scope();