From 6272408f128c92f0d8848502f42644260ab20df2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Aug 2013 08:20:42 -0700
Subject: [PATCH] Add format tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/format.cpp | 17 +++++++++++++++++
 src/util/sexpr/format.cpp | 20 ++++++++++----------
 2 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
index 14cb214f2..b170050b3 100644
--- a/src/tests/util/format.cpp
+++ b/src/tests/util/format.cpp
@@ -6,10 +6,12 @@ Author: Soonho Kong
 */
 #include <vector>
 #include <algorithm>
+#include <sstream>
 #include "format.h"
 #include "test.h"
 #include "sexpr_funcs.h"
 #include "options.h"
+#include "mpq.h"
 using namespace lean;
 
 using std::cout;
@@ -98,9 +100,24 @@ static void tst3() {
     cout << mk_pair(f1, options({"pp", "colors"}, false)) << "\n";
 }
 
+static void tst4() {
+    std::ostringstream s;
+    s << "(" << format() << ") ";
+    s << "(" << (format("foo") ^ format("bar")) << ") ";
+    s << pp(sexpr()) << " ";
+    s << pp(sexpr("test")) << " ";
+    sexpr s1(mpz(100));
+    sexpr s2(mpq(1,2));
+    sexpr s3{s1, s2};
+    s << pp(s3);
+    std::cout << s.str() << "\n";
+    lean_assert(s.str() == "() (foo bar) nil \"test\" (100 1/2)");
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 3552cc145..d7390705c 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -63,8 +63,8 @@ std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) {
     case format::format_kind::CHOICE:
     case format::format_kind::COMPOSE:
     case format::format_kind::FLAT_COMPOSE:
-        lean_unreachable();
-        break;
+        lean_unreachable(); // LCOV_EXCL_LINE
+        break;              // LCOV_EXCL_LINE
 
     case format::format_kind::NIL:
         out << "";
@@ -189,8 +189,8 @@ sexpr format::flatten(sexpr const & s) {
     case format_kind::COLOR_END:
         return s;
     }
-    lean_unreachable();
-    return s;
+    lean_unreachable(); // LCOV_EXCL_LINE
+    return s;           // LCOV_EXCL_LINE
 }
 format format::flatten(format const & f){
     return format(flatten(f.m_value));
@@ -296,8 +296,8 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
         return space_upto_line_break(x, available, found_newline);
     }
     }
-    lean_unreachable();
-    return 0;
+    lean_unreachable(); // LCOV_EXCL_LINE
+    return 0;           // LCOV_EXCL_LINE
 }
 
 sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
@@ -352,8 +352,8 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
         }
     }
     }
-    lean_unreachable();
-    return sexpr();
+    lean_unreachable(); // LCOV_EXCL_LINE
+    return sexpr();     // LCOV_EXCL_LINE
 }
 
 sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
@@ -423,8 +423,8 @@ struct sexpr_pp_fn {
                 }
             }
         }}
-        lean_unreachable();
-        return format();
+        lean_unreachable(); // LCOV_EXCL_LINE
+        return format();    // LCOV_EXCL_LINE
     }
 
     format operator()(sexpr const & s) {