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 <leonardo@microsoft.com>

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));
+        lean_assert(c.size() > def_c.size());
-        return lift_free_vars_mmv(def.get_domain(), 0, length(c) - length(def_c));
+        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(),
+        context_entry const & head = ::lean::lookup(ctx, 0);
-                                                           lift_free_vars_mmv(car(ctx).get_domain(), 1, 1),
+        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));
     }
 

src/kernel/context.cpp

@@ -8,19 +8,19 @@ Author: Leonardo de Moura
 #include "exception.h"
 
 namespace lean {
-std::pair<context_entry const &, context const &> lookup_ext(context const & c, unsigned i) {
+std::pair<context_entry const &, context> context::lookup_ext(unsigned i) const {
-    context const * it1 = &c;
+    list<context_entry> const * it1 = &m_list;
     while (*it1) {
         if (i == 0)
-            return std::pair<context_entry const &, context const &>(head(*it1), tail(*it1));
+            return std::pair<context_entry const &, context>(head(*it1), context(tail(*it1)));
         --i;
         it1 = &tail(*it1);
     }
     throw exception("unknown free variable");
 }
 
-context_entry const & lookup(context const & c, unsigned i) {
+context_entry const & context::lookup(unsigned i) const {
-    context const * it1 = &c;
+    list<context_entry> 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<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
-
 }

src/kernel/context.h

@@ -9,40 +9,53 @@ Author: Leonardo de Moura
 #include "list.h"
 
 namespace lean {
-class context_entry;
+/**
-typedef list<context_entry> 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);
+public:
-    friend context extend(context const & c, name const & n, expr const & d);
     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<context_entry> m_list;
+    explicit context(list<context_entry> 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<context_entry const &, context> lookup_ext(unsigned vidx) const;
+    bool is_empty() const { return is_nil(m_list); }
+    unsigned size() const { return length(m_list); }
+    typedef list<context_entry>::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<context_entry const &, context const &> lookup_ext(context const & c, unsigned i);
+inline std::pair<context_entry const &, context> 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_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, expr const & b) {
+inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); }
-    return context(context_entry(n, d, b), c);
+inline bool is_empty(context const & c) { return c.is_empty(); }
-}
-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);
-}
 }

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);

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));
+        lean_assert(c.size() > def_c.size());
-        return lift_free_vars(def.get_domain(), length(c) - length(def_c));
+        return lift_free_vars(def.get_domain(), c.size() - def_c.size());
     }
 
     expr check_pi(expr const & e, expr const & s, context const & ctx) {

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) {
+expr context_to_lambda(context::iterator it, context::iterator const & end, expr const & e) {
-    if (!c) {
+    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;
 }

src/library/printer.cpp

@@ -162,13 +162,16 @@ std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context co
 }
 
 static void display_context_core(std::ostream & out, context const & ctx) {
-    if (ctx) {
+    if (!is_empty(ctx)) {
-        display_context_core(out, tail(ctx));
+        auto p = lookup_ext(ctx, 0);
-        if (tail(ctx))
+        context_entry const & head  = p.first;
+        context const & tail_ctx    = p.second;
+        display_context_core(out, tail_ctx);
+        if (!is_empty(tail_ctx))
             out << "; ";
-        out << head(ctx).get_name() << " : " << head(ctx).get_domain();
+        out << head.get_name() << " : " << head.get_domain();
-        if (head(ctx).get_body()) {
+        if (head.get_body()) {
-            out << " := " << mk_pair(head(ctx).get_body(), tail(ctx));
+            out << " := " << mk_pair(head.get_body(), tail_ctx);
         }
     }
 }

src/tests/kernel/occurs.cpp

@@ -47,11 +47,11 @@ static void tst2() {
     context c;
     c = extend(c, "a", Type());
     std::cout << c;
-    lean_assert(length(c) == 1);
+    lean_assert(c.size() == 1);
     lean_assert(lookup(c, 0).get_name() == "a");
     auto p = lookup_ext(c, 0);
     lean_assert(p.first.get_name() == "a");
-    lean_assert(length(p.second) == 0);
+    lean_assert(p.second.size() == 0);
 }
 
 int main() {