From d75a4739e44c10d9a8507ba6f2e453396aa0f6fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Sep 2014 13:09:42 -0700
Subject: [PATCH] refactor(util/name): move string_to_name to name module

---
 src/frontends/lean/server.cpp | 14 --------------
 src/util/name.cpp             | 15 +++++++++++++++
 src/util/name.h               |  2 ++
 3 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index f148c0e01..015d215e1 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -460,20 +460,6 @@ void server::show(bool valid) {
     m_out << "-- ENDSHOW" << std::endl;
 }
 
-static name string_to_name(std::string const & str) {
-    name result;
-    std::string id_part;
-    for (unsigned i = 0; i < str.size(); i++) {
-        if (str[i] == '.') {
-            result = name(result, id_part.c_str());
-            id_part.clear();
-        } else {
-            id_part.push_back(str[i]);
-        }
-    }
-    return name(result, id_part.c_str());
-}
-
 // Return true iff the last part of p is a prefix of the last part of n
 static bool is_last_prefix_of(name const & p, name const & n) {
     if (p.is_string() && n.is_string()) {
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 41ab6e5ae..52493398b 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -402,6 +402,21 @@ name name::replace_prefix(name const & prefix, name const & new_prefix) const {
         return name(p, get_numeral());
 }
 
+name string_to_name(std::string const & str) {
+    static_assert(*(lean_name_separator+1) == 0, "this function assumes the length of lean_name_separator is 1");
+    name result;
+    std::string id_part;
+    for (unsigned i = 0; i < str.size(); i++) {
+        if (str[i] == lean_name_separator[0]) {
+            result = name(result, id_part.c_str());
+            id_part.clear();
+        } else {
+            id_part.push_back(str[i]);
+        }
+    }
+    return name(result, id_part.c_str());
+}
+
 enum name_ll_kind { LL_ANON = 0, LL_STRING = 1, LL_INT = 2, LL_STRING_PREFIX = 3, LL_INT_PREFIX = 4 };
 name_ll_kind ll_kind(name const & n) {
     if (n.is_anonymous())
diff --git a/src/util/name.h b/src/util/name.h
index 3d1910941..adcacd7ad 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -156,6 +156,8 @@ public:
     struct ptr_eq { bool operator()(name const & n1, name const & n2) const { return n1.m_ptr == n2.m_ptr; } };
 };
 
+name string_to_name(std::string const & str);
+
 struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
 struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };
 struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } };