From 33c4b44b2bfda273cd1ada1c02be926979016caf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Sep 2013 11:11:45 -0700 Subject: [PATCH] Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_elaborator.cpp | 13 +++---- src/kernel/context.cpp | 23 +++--------- src/kernel/context.h | 49 ++++++++++++++++---------- src/kernel/normalizer.cpp | 8 ++--- src/kernel/type_checker.cpp | 4 +-- src/library/context_to_lambda.cpp | 11 +++--- src/library/printer.cpp | 15 ++++---- src/tests/kernel/occurs.cpp | 4 +-- 8 files changed, 67 insertions(+), 60 deletions(-) diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 0be416ed0..99277cb93 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -178,8 +178,8 @@ class elaborator::imp { auto p = lookup_ext(c, i); context_entry const & def = p.first; context const & def_c = p.second; - lean_assert(length(c) > length(def_c)); - return lift_free_vars_mmv(def.get_domain(), 0, length(c) - length(def_c)); + lean_assert(c.size() > def_c.size()); + return lift_free_vars_mmv(def.get_domain(), 0, c.size() - def_c.size()); } expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) { @@ -196,7 +196,7 @@ class elaborator::imp { context_entry const & entry = p.first; context const & entry_ctx = p.second; if (entry.get_body()) { - return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, length(ctx) - length(entry_ctx)); + return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, ctx.size() - entry_ctx.size()); } } catch (exception&) { // this can happen if we access a variable out of scope @@ -477,7 +477,7 @@ class elaborator::imp { } bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { - if (is_app(e1) && is_meta(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && length(ctx) > 0) { + if (is_app(e1) && is_meta(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && !is_empty(ctx)) { return true; } else { return false; @@ -486,8 +486,9 @@ class elaborator::imp { void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) { context const & ctx = c.m_ctx; - m_constraints.push_back(constraint(arg(e1,0), mk_lambda(car(ctx).get_name(), - lift_free_vars_mmv(car(ctx).get_domain(), 1, 1), + context_entry const & head = ::lean::lookup(ctx, 0); + m_constraints.push_back(constraint(arg(e1,0), mk_lambda(head.get_name(), + lift_free_vars_mmv(head.get_domain(), 1, 1), lift_free_vars_mmv(e2, 1, 1)), c)); } diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index a3a75814d..d8a96c401 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -8,19 +8,19 @@ Author: Leonardo de Moura #include "exception.h" namespace lean { -std::pair lookup_ext(context const & c, unsigned i) { - context const * it1 = &c; +std::pair context::lookup_ext(unsigned i) const { + list const * it1 = &m_list; while (*it1) { if (i == 0) - return std::pair(head(*it1), tail(*it1)); + return std::pair(head(*it1), context(tail(*it1))); --i; it1 = &tail(*it1); } throw exception("unknown free variable"); } -context_entry const & lookup(context const & c, unsigned i) { - context const * it1 = &c; +context_entry const & context::lookup(unsigned i) const { + list const * it1 = &m_list; while (*it1) { if (i == 0) return head(*it1); @@ -29,17 +29,4 @@ context_entry const & lookup(context const & c, unsigned i) { } throw exception("unknown free variable"); } - -/** - \brief Return a new context where the names used in the context - entries of \c c do not shadow constants occurring in \c c and \c es[sz]. - - Recall that the names in context entries are just "suggestions". - These names are used to name free variables in \c es[sz] (and - dependent entries in \c c). -*/ -context sanitize_names(context const & c, unsigned sz, expr const * es); -inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); } -inline context sanitize_names(context const & c, std::initializer_list const & l) { return sanitize_names(c, l.size(), l.begin()); } - } diff --git a/src/kernel/context.h b/src/kernel/context.h index c2b97a770..537db6101 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -9,40 +9,53 @@ Author: Leonardo de Moura #include "list.h" namespace lean { -class context_entry; -typedef list context; +/** + \brief An element of the Lean context. + \see context +*/ class context_entry { name m_name; expr m_domain; expr m_body; - friend context extend(context const & c, name const & n, expr const & d, expr const & b); - friend context extend(context const & c, name const & n, expr const & d); +public: context_entry(name const & n, expr const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {} context_entry(name const & n, expr const & d):m_name(n), m_domain(d) {} -public: - ~context_entry() {} name const & get_name() const { return m_name; } expr const & get_domain() const { return m_domain; } expr const & get_body() const { return m_body; } }; + +/** + \brief A context is essentially a mapping from free-variables to types (and definition/body). +*/ +class context { + list m_list; + explicit context(list const & l):m_list(l) {} +public: + context() {} + context(context const & c, name const & n, expr const & d):m_list(context_entry(n,d), c.m_list) {} + context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n,d,b), c.m_list) {} + context_entry const & lookup(unsigned vidx) const; + std::pair lookup_ext(unsigned vidx) const; + bool is_empty() const { return is_nil(m_list); } + unsigned size() const { return length(m_list); } + typedef list::iterator iterator; + iterator begin() const { return m_list.begin(); } + iterator end() const { return m_list.end(); } + friend bool is_eqp(context const & c1, context const & c2) { return is_eqp(c1.m_list, c2.m_list); } +}; + /** \brief Return the context entry for the free variable with de Bruijn index \c i, and the context for this entry. */ -std::pair lookup_ext(context const & c, unsigned i); +inline std::pair lookup_ext(context const & c, unsigned i) { return c.lookup_ext(i); } /** \brief Return the context entry for the free variable with de Bruijn index \c i. */ -context_entry const & lookup(context const & c, unsigned i); - -inline context extend(context const & c, name const & n, expr const & d, expr const & b) { - return context(context_entry(n, d, b), c); -} -inline context extend(context const & c, name const & n, expr const & d) { - return context(context_entry(n, d), c); -} -inline bool is_empty(context const & c) { - return is_nil(c); -} +inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); } +inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); } +inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); } +inline bool is_empty(context const & c) { return c.is_empty(); } } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 0c28ef73e..f9a2eb6c9 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -99,10 +99,10 @@ class normalizer::imp { if (entry.get_body()) { save_context save(*this); // it restores the context and cache m_ctx = entry_c; - unsigned k = length(m_ctx); + unsigned k = m_ctx.size(); return svalue(reify(normalize(entry.get_body(), value_stack(), k), k)); } else { - return svalue(length(entry_c)); + return svalue(entry_c.size()); } } @@ -275,7 +275,7 @@ public: expr operator()(expr const & e, context const & ctx) { set_ctx(ctx); - unsigned k = length(m_ctx); + unsigned k = m_ctx.size(); return reify(normalize(e, value_stack(), k), k); } @@ -283,7 +283,7 @@ public: if (is_convertible_core(expected, given)) return true; set_ctx(ctx); - unsigned k = length(m_ctx); + unsigned k = m_ctx.size(); expr e_n = reify(normalize(expected, value_stack(), k), k); expr g_n = reify(normalize(given, value_stack(), k), k); return is_convertible_core(e_n, g_n); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 563c64bcc..5cb89b7ae 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -27,8 +27,8 @@ class type_checker::imp { auto p = lookup_ext(c, i); context_entry const & def = p.first; context const & def_c = p.second; - lean_assert(length(c) > length(def_c)); - return lift_free_vars(def.get_domain(), length(c) - length(def_c)); + lean_assert(c.size() > def_c.size()); + return lift_free_vars(def.get_domain(), c.size() - def_c.size()); } expr check_pi(expr const & e, expr const & s, context const & ctx) { diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp index 14e607ed8..c451d77b8 100644 --- a/src/library/context_to_lambda.cpp +++ b/src/library/context_to_lambda.cpp @@ -8,19 +8,22 @@ Author: Leonardo de Moura namespace lean { static expr g_fake = Const(name(name(0u), "context_to_lambda")); -expr context_to_lambda(context const & c, expr const & e) { - if (!c) { +expr context_to_lambda(context::iterator it, context::iterator const & end, expr const & e) { + if (it == end) { return e; } else { - context_entry const & entry = head(c); + context_entry const & entry = *it; expr t; if (entry.get_body()) t = mk_app(g_fake, entry.get_domain(), entry.get_body()); else t = mk_app(g_fake, entry.get_domain()); - return context_to_lambda(tail(c), mk_lambda(entry.get_name(), t, e)); + return context_to_lambda(++it, end, mk_lambda(entry.get_name(), t, e)); } } +expr context_to_lambda(context const & c, expr const & e) { + return context_to_lambda(c.begin(), c.end(), e); +} bool is_fake_context(expr const & e) { return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e),0) == g_fake; } diff --git a/src/library/printer.cpp b/src/library/printer.cpp index 1df2c64ac..d6944b840 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -162,13 +162,16 @@ std::ostream & operator<<(std::ostream & out, std::pair