Add simple formatter tests

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

src/library/formatter.cpp

@@ -21,7 +21,7 @@ public:
     virtual format operator()(context const & c, expr const & e, bool format_ctx, options const &) {
         std::ostringstream s;
         if (format_ctx)
-            s << c << "|-\n";
+            s << c << " |- ";
         s << mk_pair(e, c);
         return format(s.str());
     }

src/library/printer.cpp

@@ -179,7 +179,7 @@ static void display_context_core(std::ostream & out, context const & ctx) {
         display_context_core(out, tail_ctx);
         if (!empty(tail_ctx))
             out << "; ";
-        out << head.get_name() << " : " << head.get_domain();
+        out << head.get_name() << " : " << mk_pair(head.get_domain(), tail_ctx);
         if (head.get_body()) {
             out << " := " << mk_pair(head.get_body(), tail_ctx);
         }

src/tests/library/CMakeLists.txt

@@ -4,3 +4,6 @@ add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker)
 add_executable(ho_unifier ho_unifier.cpp)
 target_link_libraries(ho_unifier ${EXTRA_LIBS})
 add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier)
+add_executable(formatter formatter.cpp)
+target_link_libraries(formatter ${EXTRA_LIBS})
+add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter)

src/tests/library/formatter.cpp

@@ -0,0 +1,47 @@
+/*
+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 <iostream>
+#include <sstream>
+#include "util/test.h"
+#include "kernel/environment.h"
+#include "kernel/abstract.h"
+#include "library/formatter.h"
+using namespace lean;
+
+static void check(format const & f, char const * expected) {
+    std::ostringstream strm;
+    strm << f;
+    std::cout << strm.str() << "\n";
+    lean_assert(strm.str() == expected);
+}
+
+static void tst1() {
+    environment env;
+    env.add_var("N", Type());
+    formatter fmt = mk_simple_formatter();
+    check(fmt(env), "Variable N : Type\n");
+    expr f  = Const("f");
+    expr a  = Const("a");
+    expr x  = Const("x");
+    expr y  = Const("y");
+    expr N  = Const("N");
+    expr F  = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
+    check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x = (f y a))))");
+    check(fmt(env.get_object("N")), "Variable N : Type");
+    context ctx;
+    ctx = extend(ctx, "x", f(a));
+    ctx = extend(ctx, "y", f(Var(0), N >> N));
+    ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
+    check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y = x]");
+    check(fmt(ctx, f(Var(0), Var(2))), "f z x");
+    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y = x] |- f z x");
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}