From 0a4e03efc5fcc973207396d7596f3aaaf0e2fd6d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Aug 2013 08:18:01 -0700
Subject: [PATCH] Remove option name::separator, it can't be configured during
 runtime

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontend/operator_info.cpp | 18 ++++++-----------
 src/frontend/operator_info.h   |  2 --
 src/kernel/level.cpp           | 10 +++++-----
 src/kernel/level.h             |  2 +-
 src/kernel/pp.cpp              |  7 +++----
 src/tests/util/sexpr.cpp       |  1 -
 src/util/name.cpp              | 35 ++++++++++------------------------
 src/util/name.h                | 19 +++---------------
 src/util/sexpr/format.cpp      | 24 ++++-------------------
 src/util/sexpr/format.h        |  2 --
 src/util/sexpr/options.cpp     |  9 ++-------
 src/util/sexpr/options.h       |  2 --
 12 files changed, 34 insertions(+), 97 deletions(-)

diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp
index 57362bd9ca..6306ff1387 100644
--- a/src/frontend/operator_info.cpp
+++ b/src/frontend/operator_info.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 */
 #include "operator_info.h"
 #include "rc.h"
-#include "options.h"
 
 namespace lean {
 
@@ -87,7 +86,7 @@ operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedenc
 
 static char const * g_arrow               = "\u21a6";
 
-format pp(operator_info const & o, options const & opt) {
+format pp(operator_info const & o) {
     format r;
     switch (o.get_fixity()) {
     case fixity::Infix:   r = format(o.get_associativity() == associativity::Left ? "Infixl" : "Infixr"); break;
@@ -105,36 +104,31 @@ format pp(operator_info const & o, options const & opt) {
 
     switch (o.get_fixity()) {
     case fixity::Infix: case fixity::Prefix: case fixity::Postfix:
-        r += pp(o.get_op_name(), opt); break;
+        r += pp(o.get_op_name()); break;
     case fixity::Mixfixl:
-        for (auto p : o.get_op_name_parts()) r += format{pp(p, opt), format(" _")};
+        for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")};
         break;
     case fixity::Mixfixr:
-        for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p, opt)};
+        for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p)};
         break;
     case fixity::Mixfixc: {
         bool first = true;
         for (auto p : o.get_op_name_parts()) {
             if (first) first = false; else r += format(" _ ");
-            r += pp(p, opt);
+            r += pp(p);
         }
     }}
 
     list<name> const & l = o.get_internal_names();
     if (!is_nil(l)) {
         r += format{space(), format(g_arrow)};
-        for (auto n : l) r += format{space(), pp(n, opt)};
+        for (auto n : l) r += format{space(), pp(n)};
     }
     return r;
 }
 
-format pp(operator_info const & o) {
-    return pp(o, options());
-}
-
 std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;
 }
-
 }
diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h
index f947730d3f..b373e59fe9 100644
--- a/src/frontend/operator_info.h
+++ b/src/frontend/operator_info.h
@@ -95,8 +95,6 @@ inline operator_info mixfixl(std::initializer_list<name> const & l, unsigned pre
 inline operator_info mixfixr(std::initializer_list<name> const & l, unsigned precedence) { return mixfixr(l.size(), l.begin(), precedence); }
 inline operator_info mixfixc(std::initializer_list<name> const & l, unsigned precedence) { return mixfixc(l.size(), l.begin(), precedence); }
 
-class options;
-format pp(operator_info const & o, options const &);
 format pp(operator_info const & o);
 std::ostream & operator<<(std::ostream & out, operator_info const & o);
 }
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 25057bf167..f8cd87392f 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -192,23 +192,23 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
     return out;
 }
 
-format pp(level const & l, char const * sep) {
+format pp(level const & l) {
     switch (kind(l)) {
     case level_kind::UVar:
         if (l.is_bottom())
             return format(0);
         else
-            return format(uvar_name(l).to_string(sep));
+            return pp(uvar_name(l));
     case level_kind::Lift:
         if (lift_of(l).is_bottom())
             return format(lift_offset(l));
         else
-            return format{pp(lift_of(l), sep), format(" + "), format(lift_offset(l))};
+            return format{pp(lift_of(l)), format(" + "), format(lift_offset(l))};
     case level_kind::Max: {
-        format r = pp(max_level(l, 0), sep);
+        format r = pp(max_level(l, 0));
         for (unsigned i = 1; i < max_size(l); i++) {
             r += format(" \u2293 ");
-            r += pp(max_level(l, i), sep);
+            r += pp(max_level(l, i));
         }
         return r;
     }}
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 7e8e57cd25..4c79df2a4c 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -65,5 +65,5 @@ inline bool is_max (level const & l) { return kind(l) == level_kind::Max;  }
 inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); }
 inline level const * max_end_levels(level const & l)   { return max_begin_levels(l) + max_size(l); }
 
-format pp(level const & l, char const * sep = LEAN_NAME_SEPARATOR);
+format pp(level const & l);
 }
diff --git a/src/kernel/pp.cpp b/src/kernel/pp.cpp
index 5b5ff5aff8..fc68e62120 100644
--- a/src/kernel/pp.cpp
+++ b/src/kernel/pp.cpp
@@ -17,7 +17,6 @@ struct pp_fn {
     pp_fn(environment const * env):m_env(env) {}
 
     unsigned indent() const { return 2; }
-    char const * sep() const { return LEAN_NAME_SEPARATOR; }
     format pp_keyword(char const * k) { return highlight(format(k), format::format_color::ORANGE); }
     format pp_type_kwd() { return highlight(format("Type"), format::format_color::PINK); }
     format pp_eq_kwd() { return highlight(format(" = "), format::format_color::BLUE); }
@@ -47,7 +46,7 @@ struct pp_fn {
     }
 
     format pp_constant(expr const & e) {
-        return format(const_name(e).to_string(sep()));
+        return ::lean::pp(const_name(e));
     }
 
     format pp_value(expr const & e) {
@@ -58,7 +57,7 @@ struct pp_fn {
         if (e == Type()) {
             return pp_type_kwd();
         } else {
-            return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e), sep())};
+            return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e))};
         }
     }
 
@@ -112,7 +111,7 @@ struct pp_fn {
     }
 
     format pp_bname(expr const & binder) {
-        return format(abst_name(binder).to_string(sep()));
+        return ::lean::pp(abst_name(binder));
     }
 
     template<typename It>
diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp
index d70eb242a7..74e63d1af6 100644
--- a/src/tests/util/sexpr.cpp
+++ b/src/tests/util/sexpr.cpp
@@ -168,7 +168,6 @@ static void tst7() {
     sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) };
     std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
     std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n";
-    std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}, options(name{"name","separator"}, "-->")) << "\n";
 }
 
 int main() {
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 33c95cd8fc..22fa0e8f9a 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -47,11 +47,11 @@ struct name::imp {
 
     imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); }
 
-    static void display_core(std::ostream & out, char const * sep, imp * p) {
+    static void display_core(std::ostream & out, imp * p) {
         lean_assert(p != nullptr);
         if (p->m_prefix) {
-            display_core(out, sep, p->m_prefix);
-            out << sep;
+            display_core(out, p->m_prefix);
+            out << lean_name_separator;
         }
         if (p->m_is_string)
             out << p->m_str;
@@ -59,11 +59,11 @@ struct name::imp {
             out << p->m_k;
     }
 
-    static void display(std::ostream & out, char const * sep, imp * p) {
+    static void display(std::ostream & out, imp * p) {
         if (p == nullptr)
             out << anonymous_str;
         else
-            display_core(out, sep, p);
+            display_core(out, p);
     }
 
     friend void copy_limbs(imp * p, std::vector<name::imp *> & limbs) {
@@ -238,12 +238,12 @@ static unsigned num_digits(unsigned k) {
     return r;
 }
 
-size_t name::size(char const * sep) const {
+size_t name::size() const {
     if (m_ptr == nullptr) {
         return strlen(anonymous_str);
     } else {
         imp * i       = m_ptr;
-        size_t sep_sz = strlen(sep);
+        size_t sep_sz = strlen(lean_name_separator);
         size_t r      = 0;
         while (true) {
             if (i->m_is_string) {
@@ -262,33 +262,18 @@ size_t name::size(char const * sep) const {
     }
 }
 
-size_t name::size() const {
-    return size(LEAN_NAME_SEPARATOR);
-}
-
 unsigned name::hash() const {
     return m_ptr ? m_ptr->m_hash : 11;
 }
 
-std::string name::to_string(char const * sep) const {
+std::string name::to_string() const {
     std::ostringstream s;
-    imp::display(s, sep, m_ptr);
+    imp::display(s, m_ptr);
     return s.str();
 }
 
-std::string name::to_string() const {
-    return to_string(LEAN_NAME_SEPARATOR);
-}
-
 std::ostream & operator<<(std::ostream & out, name const & n) {
-    name::imp::display(out, LEAN_NAME_SEPARATOR, n.m_ptr);
-    return out;
-}
-
-name::sep::sep(name const & n, char const * s):m_name(n), m_sep(s) {}
-
-std::ostream & operator<<(std::ostream & out, name::sep const & s) {
-    name::imp::display(out, s.m_sep, s.m_name.m_ptr);
+    name::imp::display(out, n.m_ptr);
     return out;
 }
 }
diff --git a/src/util/name.h b/src/util/name.h
index 86933e68d4..fcb2ba570c 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -7,11 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 
-#ifndef LEAN_NAME_SEPARATOR
-#define LEAN_NAME_SEPARATOR "::"
-#endif
-
 namespace lean {
+constexpr char const * lean_name_separator = "::";
 enum class name_kind { ANONYMOUS, STRING, NUMERAL };
 /**
    \brief Hierarchical names.
@@ -52,25 +49,15 @@ public:
     bool is_atomic() const;
     name get_prefix() const;
     /**
-       \brief Convert this hierarchical name into a string using the given separator to "glue" the different limbs.
+       \brief Convert this hierarchical name into a string.
     */
-    std::string to_string(char const * sep) const;
     std::string to_string() const;
     /**
-       \brief Size of the this name (in characters) when using the given separator.
+       \brief Size of the this name (in characters).
     */
-    size_t size(char const * sep) const;
     size_t size() const;
     unsigned hash() const;
     friend std::ostream & operator<<(std::ostream & out, name const & n);
-    class sep {
-        name const & m_name;
-        char const * m_sep;
-    public:
-        sep(name const & n, char const * s);
-        friend std::ostream & operator<<(std::ostream & out, sep const & s);
-    };
-    friend std::ostream & operator<<(std::ostream & out, sep const & s);
 };
 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; } };
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 8ff7d96bdb..90d7bfa68f 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -302,21 +302,11 @@ unsigned get_pp_indent(options const & o) {
     return o.get_int(g_pp_indent, LEAN_DEFAULT_INDENTATION);
 }
 
-format pp(name const & n, char const * sep) {
-    return format(n.to_string(sep));
-}
-
-format pp(name const & n, options const & o) {
-    return pp(n, get_name_separator(o));
-}
-
 format pp(name const & n) {
-    return pp(n, get_name_separator(options()));
+    return format(n.to_string());
 }
 
 struct sexpr_pp_fn {
-    char const * m_sep;
-
     format apply(sexpr const & s) {
         switch (s.kind()) {
         case sexpr_kind::NIL:         return format("nil");
@@ -328,7 +318,7 @@ struct sexpr_pp_fn {
         case sexpr_kind::BOOL:        return format(to_bool(s) ? "true" : "false");
         case sexpr_kind::INT:         return format(to_int(s));
         case sexpr_kind::DOUBLE:      return format(to_double(s));
-        case sexpr_kind::NAME:        return pp(to_name(s), m_sep);
+        case sexpr_kind::NAME:        return pp(to_name(s));
         case sexpr_kind::MPZ:         return format(to_mpz(s));
         case sexpr_kind::MPQ:         return format(to_mpq(s));
         case sexpr_kind::CONS: {
@@ -350,18 +340,12 @@ struct sexpr_pp_fn {
         return format();
     }
 
-    format operator()(sexpr const & s, options const & o) {
-        m_sep    = get_name_separator(o);
+    format operator()(sexpr const & s) {
         return apply(s);
     }
 };
 
-format pp(sexpr const & s, options const & o) {
-    return sexpr_pp_fn()(s, o);
-}
-
 format pp(sexpr const & s) {
-    return pp(s, options());
+    return sexpr_pp_fn()(s);
 }
-
 }
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index 4bc7eae1b0..eba21c0695 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -286,8 +286,6 @@ class options;
 unsigned get_pp_indent(options const & o);
 
 /** \brief Format a hierarchical name */
-format pp(name const & n, char const * s);
-format pp(name const & n, options const & o);
 format pp(name const & n);
 
 /** \brief Format a S-expression */
diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp
index 51d859eb6b..036757412e 100644
--- a/src/util/sexpr/options.cpp
+++ b/src/util/sexpr/options.cpp
@@ -84,14 +84,13 @@ options options::update(name const & n, sexpr const & v) const {
 }
 
 format pp(options const & o) {
-    char const * sep = get_name_separator(o);
     format r;
     bool first = true;
     for_each(o.m_value, [&](sexpr const & p) {
             if (first) { first = false; } else { r += comma(); r += line(); }
             name const & n = to_name(head(p));
-            unsigned sz = n.size(sep);
-            r += group(nest(sz+3, format{pp(head(p), o), space(), format(g_arrow), space(), pp(tail(p), o)}));
+            unsigned sz = n.size();
+            r += group(nest(sz+3, format{pp(head(p)), space(), format(g_arrow), space(), pp(tail(p))}));
         });
     return group(nest(1, format{format(g_left_angle_bracket), r, format(g_right_angle_bracket)}));
 }
@@ -106,8 +105,4 @@ std::ostream & operator<<(std::ostream & out, options const & o) {
     out << g_right_angle_bracket;
     return out;
 }
-static name g_name_separator{"name", "separator"};
-char const * get_name_separator(options const & o) {
-    return o.get_string(g_name_separator, "::");
-}
 }
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index 339f38747b..a9f428816d 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -51,6 +51,4 @@ public:
 };
 template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
 template<typename T> options update(options const & o, char const * n, T const & v) { return o.update(name(n), sexpr(v)); }
-/** \brief Return the separator for hierarchical names */
-char const * get_name_separator(options const & o);
 }