Refactor frontend pretty printer

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

src/exprlib/context_to_lambda.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "context_to_lambda.h"
 
 namespace lean {
-static expr g_foo = Const("foo");
+static expr g_fake = Const(name(name(0u), "context_to_lambda"));
 expr context_to_lambda(context const & c, expr const & e) {
     if (!c) {
         return e;
@@ -15,10 +15,31 @@ expr context_to_lambda(context const & c, expr const & e) {
         context_entry const & entry = head(c);
         expr t;
         if (entry.get_body())
-            t = g_foo(entry.get_domain(), entry.get_body());
+            t = mk_app(g_fake, entry.get_domain(), entry.get_body());
         else
-            t = g_foo(entry.get_domain());
+            t = mk_app(g_fake, entry.get_domain());
         return context_to_lambda(tail(c), mk_lambda(entry.get_name(), t, e));
     }
 }
+bool is_fake_context(expr const & e) {
+    return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e),0) == g_fake;
+}
+name const & fake_context_name(expr const & e) {
+    lean_assert(is_fake_context(e));
+    return abst_name(e);
+}
+expr const & fake_context_domain(expr const & e) {
+    lean_assert(is_fake_context(e));
+    return arg(abst_domain(e), 1);
+}
+expr const & fake_context_value(expr const & e) {
+    lean_assert(is_fake_context(e));
+    if (num_args(abst_domain(e)) > 2)
+        return arg(abst_domain(e), 2);
+    else
+        return expr::null();
+}
+expr const & fake_context_rest(expr const & e) {
+    return abst_body(e);
+}
 }

src/exprlib/context_to_lambda.h

@@ -11,16 +11,55 @@ namespace lean {
    \brief Given the context (n_1 : T_1 [:= V_1]) ... (n_k : T_k [:= V_k]) and expression e into,
    return the "meaningless" lambda expression:
 
-   (lambda (n_1 : (foo T_1 V_1)) ... (lambda (n_k : (foo T_k V_k)) e))
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
 
-   The constant "foo" is irrelevant, it is just used as a marker.
+   The constant "fake" is irrelevant, it is just used as a marker.
    It is used to "glue" T_i and V_i.
 
    This little hack allows us to use the machinery for instantiating
    lambdas with contexts.
 
    \remark If a context entry (n_i : T_i [:= V_i]) does not have a
-   value V_i, then we just use (foo T_i).
+   value V_i, then we just use (fake T_i).
 */
 expr context_to_lambda(context const & c, expr const & e);
+
+/**
+   \brief Return true if \c e is a fake context created using
+   context_to_lambda.
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
+*/
+bool is_fake_context(expr const & e);
+
+/**
+   \brief Return the name n_1 of the head of the (fake) context
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
+
+   \pre is_fake_context(e)
+*/
+name const & fake_context_name(expr const & e);
+
+/**
+   \brief Return the domain T_1 of the head of the (fake) context
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
+
+   \pre is_fake_context(e)
+*/
+expr const & fake_context_domain(expr const & e);
+
+/**
+   \brief Return the value V_1 of the head of the (fake) context
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
+
+   \pre is_fake_context(e)
+   \remark If the head does not have a value, then return a null expression
+*/
+expr const & fake_context_value(expr const & e);
+/**
+   \brief Return the rest (lambda (n_2 : (fake T_2 V_2)) ... (lambda (n_k : (fake T_k V_k)) e)) of the fake context
+   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
+
+   \pre is_fake_context(e)
+*/
+expr const & fake_context_rest(expr const & e);
 }

src/exprlib/printer.cpp

@@ -144,7 +144,7 @@ std::ostream & operator<<(std::ostream & out, context const & ctx) {
         out << tail(ctx);
         out << head(ctx).get_name() << " : " << head(ctx).get_domain();
         if (head(ctx).get_body()) {
-            out << " := " << head(ctx).get_body();
+            out << " := " << mk_pair(head(ctx).get_body(), tail(ctx));
         }
         out << "\n";
     }

src/frontend/frontend.cpp

@@ -189,7 +189,7 @@ bool frontend::has_children() const { return m_imp->has_children(); }
 bool frontend::has_parent() const { return m_imp->has_parent(); }
 frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_imp->m_parent); }
 
-environment const & frontend::env() const { return m_imp->m_env; }
+environment const & frontend::get_environment() const { return m_imp->m_env; }
 
 level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.add_uvar(n, l); }
 level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); }
@@ -203,7 +203,5 @@ void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name cons
 void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); }
 void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); }
 operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); }
-
-void frontend::display(std::ostream & out) const { m_imp->m_env.display(out); }
 }
 

src/frontend/frontend.h

@@ -43,8 +43,8 @@ public:
     // =======================================
 
     /** \brief Coercion frontend -> environment. */
-    environment const & env() const;
+    environment const & get_environment() const;
-    operator environment const &() const { return env(); }
+    operator environment const &() const { return get_environment(); }
 
     level add_uvar(name const & n, level const & l);
     level add_uvar(name const & n);
@@ -68,9 +68,5 @@ public:
     */
     operator_info find_op_for(name const & n) const;
     // =======================================
-
-    /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
-    void display(std::ostream & out) const;
 };
-inline std::ostream & operator<<(std::ostream & out, frontend const & f) { f.display(out); return out; }
 }

src/frontend/operator_info.cpp

@@ -118,7 +118,7 @@ char const * to_string(fixity f) {
 
 format pp(operator_info const & o) {
     format r;
-    r = format(to_string(o.get_fixity()));
+    r = highlight_command(format(to_string(o.get_fixity())));
     if (o.get_precedence() != 0)
         r += format{space(), format(o.get_precedence())};
     for (auto p : o.get_op_name_parts())

src/frontend/pp.cpp

@@ -13,35 +13,10 @@ Author: Leonardo de Moura
 #include "occurs.h"
 #include "instantiate.h"
 #include "builtin_notation.h"
+#include "context_to_lambda.h"
+#include "printer.h"
 #include "options.h"
 
-namespace lean {
-
-format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
-    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
-                        operator()(t), space(), highlight_keyword(format(":=")), line(), operator()(v)};
-    return group(nest(def));
-}
-
-format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
-    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
-    return group(nest(def));
-}
-
-void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
-    out << mk_pair(operator()(e, c), get_options());
-}
-
-void expr_formatter::pp(std::ostream & out, expr const & e) {
-    pp(out, e, context());
-}
-
-format expr_formatter::nest(format const & f) {
-    return ::lean::nest(get_pp_indent(get_options()), f);
-}
-
-}
-
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
 #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
 #endif
@@ -67,17 +42,19 @@ format expr_formatter::nest(format const & f) {
 #endif
 
 namespace lean {
-static format g_Type_fmt     = highlight_builtin(format("Type"));
+static format g_Type_fmt      = highlight_builtin(format("Type"));
-static format g_eq_fmt       = format("=");
+static format g_eq_fmt        = format("=");
-static char const * g_eq_sym = "eq";
+static char const * g_eq_sym  = "eq";
-static unsigned g_eq_sz      = strlen(g_eq_sym);
+static unsigned g_eq_sz       = strlen(g_eq_sym);
-static format g_eq_sym_fmt   = format(g_eq_sym);
+static format g_eq_sym_fmt    = format(g_eq_sym);
-static format g_lambda_fmt   = highlight_keyword(format("\u03BB"));
+static format g_lambda_fmt    = highlight_keyword(format("\u03BB"));
-static format g_Pi_fmt       = highlight_keyword(format("\u03A0"));
+static format g_Pi_fmt        = highlight_keyword(format("\u03A0"));
-static format g_arrow_fmt    = highlight_keyword(format("\u2192"));
+static format g_arrow_fmt     = highlight_keyword(format("\u2192"));
-static format g_ellipsis_fmt = highlight(format("\u2026"));
+static format g_ellipsis_fmt  = highlight(format("\u2026"));
-static format g_let_fmt      = highlight_keyword(format("let"));
+static format g_let_fmt       = highlight_keyword(format("let"));
-static format g_in_fmt       = highlight_keyword(format("in"));
+static format g_in_fmt        = highlight_keyword(format("in"));
+static format g_assign_fmt    = highlight_keyword(format(":="));
+static format g_geq_fmt       = format("\u2265");
 
 static name g_pp_max_depth       {"pp", "max_depth"};
 static name g_pp_max_steps       {"pp", "max_steps"};
@@ -93,12 +70,27 @@ bool     get_pp_notation(options const & opts)        { return opts.get_bool(g_p
 bool     get_pp_extra_lets(options const & opts)      { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); }
 unsigned get_pp_alias_min_depth(options const & opts) { return opts.get_unsigned(g_pp_alias_min_depth, LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH); }
 
+/**
+   \brief Return a fresh name for the given abstraction.
+   By fresh, we mean a name that is not used for any constant in abst_body(e).
+   The resultant name is based on abst_name(e).
+*/
+name get_unused_name(expr const & e) {
+    name const & n = abst_name(e);
+    name n1    = n;
+    unsigned i = 1;
+    while (occurs(n1, abst_body(e))) {
+        n1 = name(n, i);
+        i++;
+    }
+    return n1;
+}
+
 /** \brief Functional object for pretty printing expressions */
 class pp_fn {
     typedef scoped_map<expr, name, expr_hash, expr_eqp> aliases;
     typedef std::vector<std::pair<name, format>>        aliases_defs;
     frontend const & m_frontend;
-    context const &  m_context;
     // State
     aliases          m_aliases;
     aliases_defs     m_aliases_defs;
@@ -349,13 +341,7 @@ class pp_fn {
     */
     std::pair<expr, expr> collect_nested(expr const & e, expr T, expr_kind k, buffer<std::pair<name, expr>> & r) {
         if (e.kind() == k) {
-            name const & n = abst_name(e);
+            name n1    = get_unused_name(e);
-            name n1    = n;
-            unsigned i = 1;
-            while (occurs(n1, abst_body(e))) {
-                n1 = name(n, i);
-                i++;
-            }
             r.push_back(mk_pair(n1, abst_domain(e)));
             expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
             if (T)
@@ -432,7 +418,7 @@ class pp_fn {
             format body_sep;
             if (T) {
                 format T_f = pp(T, 0).first;
-                body_sep = format{space(), colon(), space(), T_f, space(), highlight_keyword(format(":="))};
+                body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt};
             } else {
                 body_sep = comma();
             }
@@ -570,9 +556,8 @@ class pp_fn {
     }
 
 public:
-    pp_fn(frontend const & fe, context const & ctx, options const & opts):
+    pp_fn(frontend const & fe, options const & opts):
-        m_frontend(fe),
+        m_frontend(fe) {
-        m_context(ctx) {
         set_options(opts);
     }
 
@@ -588,49 +573,141 @@ public:
     }
 };
 
-class pp_expr_formatter : public expr_formatter {
+class pp_formatter : public formatter {
     frontend const & m_frontend;
     options          m_options;
-public:
+    unsigned         m_indent;
-    pp_expr_formatter(frontend const & fe, options const & opts):
+
-        m_frontend(fe),
+    format pp(expr const & e) {
-        m_options(opts) {
+        return pp_fn(m_frontend, m_options)(e);
     }
 
-    virtual ~pp_expr_formatter() {
+    format pp(context const & c, expr const & e, bool include_e) {
+        format r;
+        bool first = true;
+        expr c2   = context_to_lambda(c, e);
+        while (is_fake_context(c2)) {
+            name n1 = get_unused_name(c2);
+            format entry = format{format(n1), space(), colon(), space(), pp(fake_context_domain(c2))};
+            expr val = fake_context_value(c2);
+            if (val)
+                entry += format{space(), g_assign_fmt, nest(m_indent, format{line(), pp(val)})};
+            if (first) {
+                r = group(entry);
+                first = false;
+            } else {
+                r += format{line(), group(entry)};
+            }
+            c2 = instantiate_with_closed(fake_context_rest(c2), mk_constant(n1));
+        }
+        if (include_e) {
+            if (first)
+                r += format{line(), pp(c2)};
+            else
+                r = pp(c2);
+        } else {
+            return r;
+        }
+        return r;
     }
 
-    virtual options get_options() const {
+    format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v) {
-        return m_options;
+        format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
+                            pp(t), space(), g_assign_fmt, line(), pp(v)};
+        return group(nest(m_indent, def));
     }
 
-    // TODO: remove context parameter from expr_formatter
+    format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v) {
-    // The context pretty printer must open the expression
-    // before pretty-printing it.
-    virtual format operator()(expr const & e, context const & c) {
-        return pp_fn(m_frontend, c, m_options)(e);
-    }
-
-    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
         expr it1 = t;
         expr it2 = v;
         while (is_pi(it1) && is_lambda(it2)) {
             if (abst_domain(it1) != abst_domain(it2))
-                return expr_formatter::operator()(kwd, n, t, v);
+                return pp_definition(kwd, n, t, v);
             it1 = abst_body(it1);
             it2 = abst_body(it2);
         }
         if (!is_lambda(v) || is_pi(it1) || is_lambda(it2)) {
-            return expr_formatter::operator()(kwd, n, t, v);
+            return pp_definition(kwd, n, t, v);
         } else {
             lean_assert(is_lambda(v));
-            format def = pp_fn(m_frontend, context(), m_options).pp_definition(v, t);
+            format def = pp_fn(m_frontend, m_options).pp_definition(v, t);
             return format{highlight_command(format(kwd)), space(), format(n), def};
         }
     }
+
+    format pp_uvar_decl(object const & obj) {
+        return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format("\u2265"), space(), ::lean::pp(obj.get_cnstr_level())};
+    }
+
+    format pp_postulate(object const & obj) {
+        return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), colon(), space(), pp(obj.get_type())};
+    }
+
+    format pp_definition(object const & obj) {
+        return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value());
+    }
+
+    format pp_notation_decl(object const & obj) {
+        return ::lean::pp(*(static_cast<notation_declaration const *>(obj.cell())));
+    }
+
+public:
+    pp_formatter(frontend const & fe, options const & opts):
+        m_frontend(fe),
+        m_options(opts) {
+        m_indent = get_pp_indent(opts);
+    }
+
+    virtual ~pp_formatter() {
+    }
+
+    virtual format operator()(expr const & e) {
+        return pp(e);
+    }
+
+    virtual format operator()(context const & c) {
+        return pp(c, Type(), false);
+    }
+
+    virtual format operator()(context const & c, expr const & e, bool format_ctx) {
+        if (format_ctx) {
+            return pp(c, e, true);
+        } else {
+            expr c2   = context_to_lambda(c, e);
+            while (is_fake_context(c2)) {
+                expr const & rest = fake_context_rest(c2);
+                name n1 = get_unused_name(rest);
+                c2 = instantiate_with_closed(rest, mk_constant(n1));
+            }
+            return pp(c2);
+        }
+    }
+
+    virtual format operator()(environment const & env) {
+        format r;
+        bool first = true;
+        std::for_each(env.begin_objects(),
+                      env.end_objects(),
+                      [&](object const & obj) {
+                          if (first) first = false; else r += line();
+                          switch (obj.kind()) {
+                          case object_kind::UVarDeclaration:  r += pp_uvar_decl(obj); break;
+                          case object_kind::Postulate:        r += pp_postulate(obj); break;
+                          case object_kind::Definition:       r += pp_definition(obj); break;
+                          case object_kind::Neutral:          r += pp_notation_decl(obj); break;
+                          }
+                      });
+        return r;
+    }
 };
 
-std::shared_ptr<expr_formatter> mk_pp_expr_formatter(frontend const & fe, options const & opts) {
+std::shared_ptr<formatter> mk_pp_formatter(frontend const & fe, options const & opts) {
-    return std::shared_ptr<expr_formatter>(new pp_expr_formatter(fe, opts));
+    return std::shared_ptr<formatter>(new pp_formatter(fe, opts));
+}
+
+std::ostream & operator<<(std::ostream & out, frontend const & fe) {
+    auto pp = mk_pp_formatter(fe, options());
+    out << (*pp)(fe.get_environment());
+    return out;
 }
 }

src/frontend/pp.h

@@ -6,28 +6,11 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "context.h"
+#include "formatter.h"
+#include "options.h"
 
 namespace lean {
-
 class frontend;
-class expr_formatter {
+std::shared_ptr<formatter> mk_pp_formatter(frontend const & fe, options const & opts = options());
-public:
+std::ostream & operator<<(std::ostream & out, frontend const & fe);
-    virtual ~expr_formatter() {}
-    /** \brief Convert expression in the given context into a format object. */
-    virtual format operator()(expr const & e, context const & c = context()) = 0;
-    /** \brief format a definition. */
-    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
-    /** \brief format a postulate. */
-    virtual format operator()(char const * kwd, name const & n, expr const & t);
-
-    /** \brief Return options for pretty printing. */
-    virtual options get_options() const = 0;
-
-    void pp(std::ostream & out, expr const & e, context const & c);
-    void pp(std::ostream & out, expr const & e);
-
-    /** \brief Nest the given format object using the setting provided by get_options. */
-    format nest(format const & f);
-};
-std::shared_ptr<expr_formatter> mk_pp_formatter(frontend const & fe, options const & opts);
 }

src/kernel/expr.h

@@ -337,6 +337,10 @@ inline unsigned      var_idx(expr const & e)              { return to_var(e)->ge
 /** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */
 inline bool          is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr const & e)           { return to_constant(e)->get_name(); }
+/** \brief Return true iff the given expression is a constant with name \c n. */
+inline bool          is_constant(expr const & e, name const & n) {
+    return is_constant(e) && const_name(e) == n;
+}
 inline value const & to_value(expr const & e)             { return to_value(e.raw()); }
 inline unsigned      num_args(expr const & e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }

src/tests/frontend/frontend.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "frontend.h"
 #include "environment.h"
 #include "operator_info.h"
+#include "pp.h"
 #include "test.h"
 using namespace lean;
 
@@ -15,7 +16,7 @@ static void tst1() {
     f.add_uvar("tst");
     frontend c = f.mk_child();
     lean_assert(c.get_uvar("tst") == f.get_uvar("tst"));
-    lean_assert(f.env().has_children());
+    lean_assert(f.get_environment().has_children());
 }
 
 static void tst2() {
@@ -49,10 +50,27 @@ static void tst2() {
 static void tst3() {
     frontend f;
     std::cout << "====================\n";
-    std::cout << f;
+    std::cout << f << "\n";
+}
+
+static void tst4() {
+    frontend f;
+    std::shared_ptr<formatter> fmt_ptr = mk_pp_formatter(f);
+    formatter & fmt = *fmt_ptr;
+    expr Bool = Const("Bool");
+    context c;
+    c = extend(c, "x", Bool);
+    c = extend(c, "y", Bool);
+    c = extend(c, "x", Bool, Var(1));
+    c = extend(c, "x", Bool, Var(2));
+    c = extend(c, "z", Bool, Var(1));
+    c = extend(c, "x", Bool, Var(4));
+    std::cout << fmt(c) << "\n";
 }
 
 int main() {
+    tst4();
+    return 0;
     tst1();
     tst2();
     tst3();