From ab81a57d86ada65a784d079a8da239af7c098193 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 23 Jul 2013 16:20:44 -0700
Subject: [PATCH] Add test cases for format

---
 src/tests/util/CMakeLists.txt |  3 +++
 src/tests/util/format.cpp     | 45 +++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/tests/util/format.cpp

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 2d788ecd6..9596712e6 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -4,3 +4,6 @@ add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt)
 add_executable(name name.cpp)
 target_link_libraries(name ${EXTRA_LIBS})
 add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name)
+add_executable(format format.cpp)
+target_link_libraries(format ${EXTRA_LIBS})
+add_test(format ${CMAKE_CURRENT_BINARY_DIR}/format)
diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp
new file mode 100644
index 000000000..d66224e45
--- /dev/null
+++ b/src/tests/util/format.cpp
@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Soonho Kong
+*/
+#include "format.h"
+#include "test.h"
+
+using namespace lean;
+
+static void tst1() {
+    format f_atom1("foo");
+    format f_atom2("bar");
+    format f_atom3(1);
+    format f_atom4(3.1415);
+    format f1(f_atom1, f_atom2);
+    format f2(f1);
+    format f3 = choice(f1, f2);
+    format f4 = nest(3, f3);
+    format f5 = line();
+    format f6(f4, f5);
+    format f7(f6, f3);
+
+    std::cout << "f_atom1 = " << f_atom1 << std::endl
+              << "f_atom2 = " << f_atom2 << std::endl
+              << "f_atom3 = " << f_atom3 << std::endl
+              << "f_atom4 = " << f_atom4 << std::endl
+        ;
+
+    std::cout << "f1 = " << f1 << std::endl
+              << "f2 = " << f2 << std::endl
+              << "f3 = " << f3 << std::endl
+              << "f4 = " << f4 << std::endl
+              << "f5 = " << f5 << std::endl
+              << "f6 = " << f6 << std::endl
+              << "f7 = " << f7 << std::endl
+        ;
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return has_violations() ? 1 : 0;
+}