From fbd25cac9f13c500289c4544ef6c888c532b0366 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Aug 2013 08:48:52 -0700
Subject: [PATCH] Add hierarchical names tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/name.cpp | 29 ++++++++++++++++++++++++++++-
 src/util/debug.cpp      |  4 ++--
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 638de8e0c..4f10f7b66 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "name.h"
+#include <cstring>
+#include <sstream>
 #include "test.h"
+#include "name.h"
 using namespace lean;
 
 static void tst1() {
@@ -82,10 +84,35 @@ static void tst4() {
     lean_assert(!is_prefix_of(name(name("bla"), 1u), name(name(name(0u), 1u), "foo")));
 }
 
+static void tst5() {
+    name n(0u);
+    lean_assert(n.size() == 1);
+    lean_assert(name().size() > 0);
+    lean_assert(name({"foo", "bla", "boing"}).get_prefix() == name({"foo", "bla"}));
+    lean_assert(!name({"foo", "bla", "boing"}).is_atomic());
+    lean_assert(name({"foo"}).is_atomic());
+    lean_assert(strcmp(name({"foo", "bla", "boing"}).get_string(), "boing") == 0);
+    lean_assert(name(name(0u), 1u).get_numeral() == 1u);
+    lean_assert(name(2u).get_numeral() == 2u);
+    lean_assert(name::anonymous().is_anonymous());
+    name n1("foo");
+    name n2 = n1;
+    lean_assert(n2 == n1);
+    std::cout << name::anonymous() << "\n";
+    std::cout << name({"foo", "bla", "boing"}).get_prefix() << "\n";
+    lean_assert(name("foo").is_string());
+    lean_assert(name(0u).is_numeral());
+    lean_assert(name(name(0u), "foo").is_string());
+    lean_assert(name(name("foo"), 0u).is_numeral());
+    lean_assert(name(name(0u), "foo").get_prefix().is_numeral());
+    lean_assert(name(name("foo"), 0u).get_prefix().is_string());
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 0461a8ea2..6653b130b 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -25,7 +25,7 @@ static std::unique_ptr<std::set<std::string>> g_enabled_debug_tags;
 bool has_violations() {
     return g_has_violations;
 }
-
+// LCOV_EXCL_START
 void enable_assertions(bool f) {
     g_enable_assertions = f;
 }
@@ -102,5 +102,5 @@ void invoke_debugger() {
         }
     }
 }
-
+// LCOV_EXCL_STOP
 }