refactor(kernel): add formatter and simplify contexts

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
-instantiate.cpp
+instantiate.cpp context.cpp formatter.cpp
 # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
 # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp
 # justification.cpp unification_constraint.cpp kernel_exception.cpp

src/kernel/context.cpp

@@ -7,84 +7,16 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/exception.h"
 #include "kernel/context.h"
-#include "kernel/metavar.h"
-#include "kernel/free_vars.h"
 
 namespace lean {
-context::context(std::initializer_list<std::pair<char const *, expr const &>> const & l) {
-    for (auto const & p : l)
-        m_list = cons(context_entry(name(p.first), p.second), m_list);
-}
-
-std::pair<context_entry const &, context> context::lookup_ext(unsigned i) const {
-    list<context_entry> const * it1 = &m_list;
-    while (*it1) {
+std::pair<name, expr> const & lookup(context const & c, unsigned i) {
+    auto const * it = &c;
+    while (*it) {
         if (i == 0)
-            return std::pair<context_entry const &, context>(head(*it1), context(tail(*it1)));
+            return head(*it);
         --i;
-        it1 = &tail(*it1);
+        it = &tail(*it);
     }
     throw exception("unknown free variable");
 }
-
-context_entry const & context::lookup(unsigned i) const {
-    list<context_entry> const * it1 = &m_list;
-    while (*it1) {
-        if (i == 0)
-            return head(*it1);
-        --i;
-        it1 = &tail(*it1);
-    }
-    throw exception("unknown free variable");
-}
-
-optional<context_entry> context::find(unsigned i) const {
-    list<context_entry> const * it1 = &m_list;
-    while (*it1) {
-        if (i == 0)
-            return some(head(*it1));
-        --i;
-        it1 = &tail(*it1);
-    }
-    return optional<context_entry>();
-}
-
-list<context_entry> truncate_core(list<context_entry> const & l, unsigned s) {
-    if (s == 0) {
-        return list<context_entry>();
-    } else {
-        return cons(head(l), truncate_core(tail(l), s-1));
-    }
-}
-
-context context::truncate(unsigned s) const {
-    return context(truncate_core(m_list, s));
-}
-
-struct remove_no_applicable {};
-static list<context_entry> remove_core(list<context_entry> const & l, unsigned s, unsigned n, metavar_env const & menv) {
-    if (l) {
-        if (s == 0) {
-            if (n > 0) {
-                return remove_core(tail(l), 0, n-1, menv);
-            } else {
-                return l;
-            }
-        } else {
-            if (has_free_var(head(l), s-1, s+n-1, menv))
-                throw remove_no_applicable();
-            return cons(lower_free_vars(head(l), s+n-1, n, menv), remove_core(tail(l), s-1, n, menv));
-        }
-    } else {
-        return l;
-    }
-}
-
-optional<context> context::remove(unsigned s, unsigned n, metavar_env const & menv) const {
-    try {
-        return some(context(remove_core(m_list, s, n, menv)));
-    } catch (remove_no_applicable&) {
-        return optional<context>();
-    }
-}
 }

src/kernel/context.h

@@ -11,93 +11,8 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-/**
-   \brief An element of the Lean context.
-   \see context
-*/
-class context_entry {
-    name            m_name;
-    optional<expr>  m_domain;
-    optional<expr>  m_body;
-public:
-    context_entry(name const & n, optional<expr> const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {}
-    context_entry(name const & n, expr const & d, optional<expr> const & b):m_name(n), m_domain(d), m_body(b) {}
-    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) {}
-    name const & get_name() const   { return m_name; }
-    optional<expr> const & get_domain() const { return m_domain; }
-    optional<expr> const & get_body() const   { return m_body; }
-    friend bool operator==(context_entry const & e1, context_entry const & e2) { return e1.m_domain == e2.m_domain && e1.m_body == e2.m_body; }
-    friend bool operator!=(context_entry const & e1, context_entry const & e2) { return !(e1 == e2); }
-};
-
-class metavar_env;
-
-/**
-   \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, optional<expr> const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
-    context(context const & c, name const & n, expr const & d, optional<expr> const & b):m_list(context_entry(n, d, b), 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(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
-    context(context const & c, context_entry const & e):m_list(e, c.m_list) {}
-    context(unsigned sz, context_entry const * es):context(to_list(es, es + sz)) {}
-    context(std::initializer_list<std::pair<char const *, expr const &>> const & l);
-    context_entry const & lookup(unsigned vidx) const;
-    std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
-    /** \brief Similar to lookup, but always succeed */
-    optional<context_entry> find(unsigned vidx) const;
-    bool empty() const { return is_nil(m_list); }
-    explicit operator bool() const { return !empty(); }
-    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 a new context where entries at positions >= s are removed.
-    */
-    context truncate(unsigned s) const;
-    /**
-       \brief Return a new context where the entries at positions [s, s+n) were removed.
-
-       The free variables in entries [0, s) are lowered.
-       That is, if this context is of the form
-       [ce_m, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0]
-       Then, the resultant context is of the form
-       [ce_m, ..., ce_{s+n}, lower(ce_{s-1}, n, n), ..., lower(ce_0, s+n-1, n)]
-
-       \pre size() >= s + n
-
-       If for some i in [0, s), has_free_var(ce_i, s - 1 - i, s + n - 1 - i), then return none.
-       That is, the lower operations must be valid.
-    */
-    optional<context> remove(unsigned s, unsigned n, metavar_env const & menv) const;
-    friend bool operator==(context const & ctx1, context const & ctx2) { return ctx1.m_list == ctx2.m_list; }
-    friend bool operator!=(context const & ctx1, context const & ctx2) { return !(ctx1 == ctx2); }
-};
-
-/**
-   \brief Return the context entry for the free variable with de
-   Bruijn index \c i, and the context for this entry.
-*/
-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.
-*/
-inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); }
-inline optional<context_entry> find(context const & c, unsigned i) { return c.find(i); }
-inline context extend(context const & c, name const & n, optional<expr> const & d, expr const & b) { return context(c, n, d, b); }
-inline context extend(context const & c, name const & n, expr const & d, optional<expr> const & b) { return context(c, n, d, b); }
-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 empty(context const & c) { return c.empty(); }
-
-std::ostream & operator<<(std::ostream & out, context const & ctx);
+typedef list<std::pair<name, expr>> context;
+inline context extend(context const & c, name const & n, expr const & t) { return cons(mk_pair(n, t), c); }
+std::pair<name, expr> const & lookup(context const & c, unsigned i);
+optional<std::pair<name, expr>> find(context const & c, unsigned i);
 }

src/kernel/expr.cpp

@@ -15,8 +15,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
-// #include "kernel/free_vars.h"
-// #include "kernel/metavar.h"
+#include "kernel/free_vars.h"
 // #include "kernel/max_sharing.h"
 
 namespace lean {
@@ -336,24 +335,36 @@ expr update_mlocal(expr const & e, expr const & new_type) {
         return e;
 }
 
-#if 0
+bool is_atomic(expr const & e) {
+    switch (e.kind()) {
+    case expr_kind::Constant: case expr_kind::Sort:
+    case expr_kind::Macro:    case expr_kind::Var:
+        return true;
+    case expr_kind::App:      case expr_kind::Let:
+    case expr_kind::Meta:     case expr_kind::Local:
+    case expr_kind::Lambda:   case expr_kind::Pi:  case expr_kind::Sigma:
+    case expr_kind::Pair:     case expr_kind::Fst: case expr_kind::Snd:
+        return false;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
 
 bool is_arrow(expr const & t) {
     optional<bool> r = t.raw()->is_arrow();
     if (r) {
         return *r;
     } else {
-        bool res = is_pi(t) && !has_free_var(abst_body(t), 0);
+        bool res = is_pi(t) && !has_free_var(binder_body(t), 0);
         t.raw()->set_is_arrow(res);
         return res;
     }
 }
 
 bool is_cartesian(expr const & t) {
-    return is_sigma(t) && !has_free_var(abst_body(t), 0);
+    return is_sigma(t) && !has_free_var(binder_body(t), 0);
 }
 
-
+#if 0
 expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Var:      return mk_var(var_idx(a));

src/kernel/expr.h

@@ -359,6 +359,10 @@ inline bool is_let(expr const & e)        { return e.kind() == expr_kind::Let; }
 inline bool is_binder(expr const & e)     { return is_lambda(e) || is_pi(e) || is_sigma(e); }
 inline bool is_proj(expr const & e)       { return is_fst(e) || is_snd(e); }
 inline bool is_mlocal(expr const & e)     { return is_metavar(e) || is_local(e); }
+
+bool is_atomic(expr const & e);
+bool is_arrow(expr const & t);
+bool is_cartesian(expr const & t);
 // =======================================
 
 // =======================================

src/kernel/formatter.cpp

@@ -0,0 +1,161 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/formatter.h"
+#include "kernel/context.h"
+
+namespace lean {
+/**
+   \brief Very basic printer for expressions.
+   It is mainly used when debugging code.
+*/
+struct print_expr_fn {
+    std::ostream & m_out;
+
+    std::ostream & out() { return m_out; }
+
+    bool is_atomic(expr const & a) {
+        return ::lean::is_atomic(a) || is_mlocal(a);
+    }
+
+    void print_child(expr const & a, context const & c) {
+        if (is_atomic(a)) {
+            print(a, c);
+        } else {
+            out() << "("; print(a, c); out() << ")";
+        }
+    }
+
+    void print_macro(expr const & a) {
+        to_macro(a).display(out());
+    }
+
+    void print_sort(expr const & a) {
+        if (is_zero(sort_level(a))) {
+            out () << "Bool";
+        } else {
+            out() << "(Type " << sort_level(a) << ")";
+        }
+    }
+
+    void print_app(expr const & e, context const & c) {
+        expr const & f = app_fn(e);
+        if (is_app(f))
+            print(f, c);
+        else
+            print_child(f, c);
+        out() << " ";
+        print_child(app_arg(e), c);
+    }
+
+    void print_arrow_body(expr const & a, context const & c) {
+        if (is_atomic(a) || is_arrow(a))
+            return print(a, c);
+        else
+            return print_child(a, c);
+    }
+
+    void print_pair(expr const & e, context const & c) {
+        out() << "pair ";
+        print_child(pair_first(e), c);
+        out() << " ";
+        print_child(pair_second(e), c);
+        out() << " ";
+        print_child(pair_type(e), c);
+    }
+
+    void print_binder(char const * bname, expr const & e, context const & c) {
+        out() << bname << " " << binder_name(e) << " : ";
+        print_child(binder_domain(e), c);
+        out() << ", ";
+        print_child(binder_body(e), extend(c, binder_name(e), binder_domain(e)));
+    }
+
+    void print(expr const & a, context const & c) {
+        switch (a.kind()) {
+        case expr_kind::Meta: case expr_kind::Local:
+            out() << mlocal_name(a);
+            break;
+        case expr_kind::Var: {
+            auto e = find(c, var_idx(a));
+            if (e)
+                out() << e->first << "#" << var_idx(a);
+            else
+                out() << "#" << var_idx(a);
+            break;
+        }
+        case expr_kind::Constant:
+            out() << const_name(a);
+            break;
+        case expr_kind::App:
+            print_app(a, c);
+            break;
+        case expr_kind::Pair:
+            print_pair(a, c);
+            break;
+        case expr_kind::Fst: case expr_kind::Snd:
+            out() << (is_fst(a) ? "fst" : "snd") << " ";
+            print_child(proj_arg(a), c);
+            break;
+        case expr_kind::Sigma:
+            print_binder("sig", a, c);
+            break;
+        case expr_kind::Lambda:
+            print_binder("fun", a, c);
+            break;
+        case expr_kind::Pi:
+            if (!is_arrow(a)) {
+                print_binder("Pi", a, c);
+            } else {
+                print_child(binder_domain(a), c);
+                out() << " -> ";
+                print_arrow_body(binder_body(a), extend(c, binder_name(a), binder_domain(a)));
+            }
+            break;
+        case expr_kind::Let:
+            out() << "let " << let_name(a);
+            if (let_type(a)) {
+                out() << " : ";
+                print(*let_type(a), c);
+            }
+            out() << " := ";
+            print(let_value(a), c);
+            out() << " in ";
+            print_child(let_body(a), extend(c, let_name(a), let_value(a)));
+            break;
+        case expr_kind::Sort:
+            print_sort(a);
+            break;
+        case expr_kind::Macro:
+            print_macro(a);
+            break;
+        }
+    }
+
+    print_expr_fn(std::ostream & out):m_out(out) {}
+
+    void operator()(expr const & e, context const & c) {
+        print(e, c);
+    }
+};
+
+std::ostream & operator<<(std::ostream & out, expr const & e) {
+    print_expr_fn pr(out);
+    pr(e, context());
+    return out;
+}
+
+class simple_formatter_cell : public formatter_cell {
+public:
+    virtual format operator()(expr const & e, options const &) {
+        std::ostringstream s; s << e; return format(s.str());
+    }
+};
+formatter mk_simple_formatter() {
+    return mk_formatter(simple_formatter_cell());
+}
+void print(lean::expr const & a) { std::cout << a << std::endl; }
+}

src/kernel/formatter.h

@@ -7,8 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include "util/sexpr/options.h"
-#include "kernel/context.h"
-#include "kernel/environment.h"
+#include "kernel/expr.h"
 
 namespace lean {
 /**
@@ -19,16 +18,7 @@ public:
     virtual ~formatter_cell() {}
     /** \brief Format the given expression. */
     virtual format operator()(expr const & e, options const & opts) = 0;
-    /** \brief Format the given context. */
-    virtual format operator()(context const & c, options const & opts) = 0;
-    /**
-        \brief Format the given expression with respect to the given
-        context.
-
-        \remark If format_ctx == false, then the context is not formatted. It just provides names
-        for the free variables
-    */
-    virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) = 0;
+#if 0
     /** \brief Format the given object */
     virtual format operator()(object const & obj, options const & opts) = 0;
     /** \brief Format the given environment */
@@ -39,6 +29,7 @@ public:
         Not every formatter has an associated environment object.
     */
     virtual optional<ro_environment> get_environment() const { return optional<ro_environment>(); }
+#endif
 };
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@@ -48,16 +39,21 @@ class formatter {
     formatter(formatter_cell * c):m_cell(c) {}
 public:
     format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); }
-    format operator()(context const & c, options const & opts = options()) const { return (*m_cell)(c, opts); }
-    format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); }
+#if 0
     format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
     format operator()(ro_environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
     optional<ro_environment> get_environment() { return m_cell->get_environment(); }
-
+#endif
     template<typename FCell> friend formatter mk_formatter(FCell && fcell);
 };
 
 template<typename FCell> formatter mk_formatter(FCell && fcell) {
     return formatter(new FCell(std::forward<FCell>(fcell)));
 }
+
+std::ostream & operator<<(std::ostream & out, expr const & e);
+/**
+   \brief Create a simple formatter object based on operator<<
+*/
+formatter mk_simple_formatter();
 }

src/kernel/replace_fn.cpp

@@ -7,16 +7,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 
 namespace lean {
-bool replace_fn::is_atomic(expr const & e) {
-    switch (e.kind()) {
-    case expr_kind::Constant: case expr_kind::Sort:
-    case expr_kind::Macro:    case expr_kind::Var:
-        return true;
-    default:
-        return false;
-    }
-}
-
 void replace_fn::save_result(expr const & e, expr const & r, unsigned offset, bool shared) {
     if (shared)
         m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r));

src/kernel/replace_fn.h

@@ -52,7 +52,6 @@ class replace_fn {
     frame_stack                                     m_fs;
     result_stack                                    m_rs;
 
-    static bool is_atomic(expr const & e);
     void save_result(expr const & e, expr const & r, unsigned offset, bool shared);
     bool visit(expr const & e, unsigned offset);
     bool check_index(frame & f, unsigned idx);