Add formatter API

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

src/exprlib/CMakeLists.txt

@@ -1,2 +1,3 @@
-add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp)
+add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
+  formatter.cpp)
 target_link_libraries(exprlib ${LEAN_LIBS})

src/exprlib/formatter.cpp

@@ -0,0 +1,34 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <sstream>
+#include "formatter.h"
+#include "printer.h"
+
+namespace lean {
+class simple_formatter : public formatter {
+public:
+    virtual format operator()(expr const & e) {
+        std::ostringstream s; s << e; return format(s.str());
+    }
+    virtual format operator()(context const & c) {
+        std::ostringstream s; s << c; return format(s.str());
+    }
+    virtual format operator()(context const & c, expr const & e, bool format_ctx) {
+        std::ostringstream s;
+        if (format_ctx)
+            s << c << "|-\n";
+        s << mk_pair(e,c);
+        return format(s.str());
+    }
+    virtual format operator()(environment const & env) {
+        std::ostringstream s; s << env; return format(s.str());
+    }
+};
+std::shared_ptr<formatter> mk_simple_formatter() {
+    return std::shared_ptr<formatter>(new simple_formatter());
+}
+}

src/exprlib/formatter.h

@@ -0,0 +1,38 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <memory>
+#include "context.h"
+
+namespace lean {
+class environment;
+/**
+   \brief API for formatting expressions, contexts and environments.
+*/
+class formatter {
+public:
+    virtual ~formatter() {}
+    /** \brief Format the given expression. */
+    virtual format operator()(expr const & e) = 0;
+    /** \brief Format the given context. */
+    virtual format operator()(context const & c) = 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 = false) = 0;
+    /** \brief Format the given environment */
+    virtual format operator()(environment const & env) = 0;
+};
+/**
+   \brief Return simple expression formatter that just uses printer module.
+*/
+std::shared_ptr<formatter> mk_simple_formatter();
+}

src/exprlib/printer.h

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 namespace lean {
 std::ostream & operator<<(std::ostream & out, context const & ctx);
 std::ostream & operator<<(std::ostream & out, expr const & e);
-std::ostream & operator<<(std::ostream & out, std::pair<context const &, expr const &> const & p);
+std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context const &> const & p);
 class environment;
 std::ostream & operator<<(std::ostream & out, environment const & env);
 }

src/frontend/frontend.cpp

@@ -14,41 +14,6 @@ Author: Leonardo de Moura
 #include "pp.h"
 
 namespace lean {
-/**
-    \brief Create object for tracking notation/operator declarations.
-    This object is mainly used for pretty printing.
-*/
-class notation_declaration : public neutral_object_cell {
-    operator_info m_op;
-    name          m_name;
-public:
-    notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {}
-    virtual ~notation_declaration() {}
-    static char const * g_keyword;
-    virtual char const * keyword() const { return g_keyword; }
-    virtual format pp(environment const &) const {
-        char const * cmd;
-        switch (m_op.get_fixity()) {
-        case fixity::Infix:     cmd = "Infix";   break;
-        case fixity::Infixl:    cmd = "Infixl";  break;
-        case fixity::Infixr:    cmd = "Infixr";  break;
-        case fixity::Prefix:    cmd = "Prefix";  break;
-        case fixity::Postfix:   cmd = "Postfix"; break;
-        case fixity::Mixfixl:   cmd = "Mixfixl"; break;
-        case fixity::Mixfixr:   cmd = "Mixfixr"; break;
-        case fixity::Mixfixc:   cmd = "Mixfixc"; break;
-        }
-        format r = highlight_command(format(cmd));
-        if (m_op.get_precedence() != 0)
-            r += format{space(), format(m_op.get_precedence())};
-        for (auto p : m_op.get_op_name_parts())
-            r += format{space(), format(p)};
-        r += format{space(), format(m_name)};
-        return r;
-    }
-};
-char const * notation_declaration::g_keyword = "Notation";
-
 /** \brief Implementation of the Lean frontend */
 struct frontend::imp {
     // Remark: only named objects are stored in the dictionary.

src/frontend/operator_info.cpp

@@ -101,53 +101,46 @@ operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedenc
     lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixc, precedence));
 }
 
-static char const * g_arrow               = "\u21a6";
+char const * to_string(fixity f) {
+    switch (f) {
+    case fixity::Infix:   return "Infix";
+    case fixity::Infixl:  return "Infixl";
+    case fixity::Infixr:  return "Infixr";
+    case fixity::Prefix:  return "Prefix";
+    case fixity::Postfix: return "Postfix";
+    case fixity::Mixfixl: return "Mixfixl";
+    case fixity::Mixfixr: return "Mixfixr";
+    case fixity::Mixfixc: return "Mixfixc";
+    }
+    lean_unreachable();
+    return 0;
+}
 
 format pp(operator_info const & o) {
     format r;
-    switch (o.get_fixity()) {
-    case fixity::Infix:   r = format("Infix"); break;
-    case fixity::Infixl:  r = format("Infixl"); break;
-    case fixity::Infixr:  r = format("Infixr"); break;
-    case fixity::Prefix:  r = format("Prefix");  break;
-    case fixity::Postfix: r = format("Postfix"); break;
-    case fixity::Mixfixl:
-    case fixity::Mixfixr:
-    case fixity::Mixfixc: r = format("Mixfix"); break;
-    }
-
-    r += space();
-
+    r = format(to_string(o.get_fixity()));
     if (o.get_precedence() != 0)
-        r += format{format(o.get_precedence()), space()};
-
-    switch (o.get_fixity()) {
-    case fixity::Infix: case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix:
-        r += pp(o.get_op_name()); break;
-    case fixity::Mixfixl:
-        for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")};
-        break;
-    case fixity::Mixfixr:
-        for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p)};
-        break;
-    case fixity::Mixfixc: {
-        bool first = true;
-        for (auto p : o.get_op_name_parts()) {
-            if (first) first = false; else r += format(" _ ");
-            r += pp(p);
-        }
-    }}
-
-    list<name> const & l = o.get_internal_names();
-    if (!is_nil(l)) {
-        r += format{space(), format(g_arrow)};
-        for (auto n : l) r += format{space(), pp(n)};
-    }
+        r += format{space(), format(o.get_precedence())};
+    for (auto p : o.get_op_name_parts())
+        r += format{space(), format(p)};
     return r;
 }
 
+char const * notation_declaration::keyword() const {
+    return to_string(m_op.get_fixity());
+}
+
 std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;
 }
+
+format pp(notation_declaration const & n) {
+    return format{pp(n.get_op()), space(), format(n.get_internal_name())};
+}
+
+std::ostream & operator<<(std::ostream & out, notation_declaration const & n) {
+    out << pp(n);
+    return out;
+}
 }

src/frontend/operator_info.h

@@ -8,11 +8,13 @@ Author: Leonardo de Moura
 #include "name.h"
 #include "list.h"
 #include "format.h"
+#include "object.h"
 
 namespace lean {
 /**
    \brief Operator fixity.
    Prefix:   ID _
+   Infixl:    _ ID _
    Infixl:    _ ID _    (left associative)
    Infixr:    _ ID _    (right associative)
    Postfix:  _ ID
@@ -101,4 +103,22 @@ inline operator_info mixfixc(std::initializer_list<name> const & l, unsigned pre
 
 format pp(operator_info const & o);
 std::ostream & operator<<(std::ostream & out, operator_info const & o);
+
+/**
+    \brief Create object for tracking notation/operator declarations.
+    This object is mainly used for recording the declaration.
+*/
+class notation_declaration : public neutral_object_cell {
+    operator_info m_op;
+    name          m_name;
+public:
+    notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {}
+    virtual ~notation_declaration() {}
+    virtual char const * keyword() const;
+    operator_info get_op() const { return m_op; }
+    name const & get_internal_name() const { return m_name; }
+};
+
+format pp(notation_declaration const & n);
+std::ostream & operator<<(std::ostream & out, notation_declaration const & n);
 }

src/frontend/pp.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "context.h"
 
 namespace lean {
+
 class frontend;
 class expr_formatter {
 public:
@@ -28,5 +29,5 @@ public:
     /** \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_expr_formatter(frontend const & fe, options const & opts);
+std::shared_ptr<expr_formatter> mk_pp_formatter(frontend const & fe, options const & opts);
 }

src/kernel/object.h

@@ -58,7 +58,8 @@ public:
 
 /**
    \brief Neutral objects are mainly used for bookkeeping in
-   kernel frontends.
+   frontends built on top of the kernel.
+   The kernel does *not* create neutral objects.
 */
 class neutral_object_cell : public object_cell {
 public:
@@ -122,6 +123,8 @@ public:
     bool is_definition() const { return m_ptr->is_definition(); }
     bool is_opaque() const { return m_ptr->is_opaque(); }
     expr const & get_value() const { return m_ptr->get_value(); }
+
+    object_cell const * cell() const { return m_ptr; }
 };
 object mk_uvar_decl(name const & n, level const & l);
 object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);