From c697cf4c29cb9699cd77ff048ab5e15ba9ba4e9f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Jun 2018 14:06:34 -0700
Subject: [PATCH] chore(tests/util): remove exception test

---
 src/tests/util/CMakeLists.txt |  3 --
 src/tests/util/exception.cpp  | 95 -----------------------------------
 2 files changed, 98 deletions(-)
 delete mode 100644 src/tests/util/exception.cpp

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 0eb6732eb0..0e7eb6f68b 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -22,9 +22,6 @@ add_exec_test(rb_tree "rb_tree")
 add_executable(rb_map rb_map.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
 target_link_libraries(rb_map ${EXTRA_LIBS})
 add_exec_test(rb_map "rb_map")
-add_executable(exception exception.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
-target_link_libraries(exception ${EXTRA_LIBS})
-add_exec_test(exception "exception")
 add_executable(bit_tricks bit_tricks.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
 target_link_libraries(bit_tricks ${EXTRA_LIBS})
 add_exec_test(bit_tricks "bit_tricks")
diff --git a/src/tests/util/exception.cpp b/src/tests/util/exception.cpp
deleted file mode 100644
index 838ae3e36e..0000000000
--- a/src/tests/util/exception.cpp
+++ /dev/null
@@ -1,95 +0,0 @@
-/*
-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 <string>
-#include <functional>
-#include "runtime/sstream.h"
-#include "util/test.h"
-#include "util/parser_exception.h"
-#include "util/init_module.h"
-using namespace lean;
-
-static void tst1() {
-    try {
-        throw exception(std::string("foo"));
-    } catch (exception & ex) {
-        lean_assert(std::string("foo") == ex.what());
-    }
-}
-
-static void tst2() {
-    try {
-        throw parser_exception(std::string("foo"), "[string]", {10, 100});
-    } catch (parser_exception & ex) {
-        lean_assert(std::string("[string]:10:100: error: foo") == ex.what());
-    }
-}
-
-static void tst3() {
-    try {
-        throw parser_exception(sstream() << "msg " << 10 << " " << 20, "[stream]", {10, 100});
-    } catch (parser_exception & ex) {
-        lean_assert(std::string("[stream]:10:100: error: msg 10 20") == ex.what());
-    }
-}
-
-static void tst4() {
-    try {
-        throw interrupted();
-    } catch (interrupted & ex) {
-        lean_assert(std::string("interrupted") == ex.what());
-    }
-}
-
-class ex : public exception {
-    std::function<char const *()> m_f;
-public:
-    ex(std::function<char const *()> const & f):m_f(f) {}
-    virtual throwable * clone() const { return new ex(m_f); }
-    virtual void rethrow() const { throw *this; }
-    virtual char const * what() const noexcept { return m_f(); }
-};
-
-static void throw_ex() {
-    int x = 10;
-    std::string msg = "foo";
-    throw ex([=]() {
-            static std::string m;
-            std::ostringstream buffer;
-            buffer << "error, x: " << x << " " << msg;
-            m = buffer.str();
-            return m.c_str();
-        });
-}
-
-static void throw_catch_rethrow() {
-    try {
-        throw_ex();
-    } catch (ex & e) {
-        std::cout << "CATCH 1: {" << e.what() << "}\n";
-        std::unique_ptr<throwable> new_e(e.clone());
-        new_e->rethrow();
-    }
-}
-
-static void tst5() {
-    try {
-        throw_catch_rethrow();
-    } catch (ex & e) {
-        std::cout << "CATCH 2: {" << e.what() << "}\n";
-    }
-}
-
-int main() {
-    initialize_util_module();
-    tst1();
-    tst2();
-    tst3();
-    tst4();
-    tst5();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}