fix(library/init): name has_repr instance is actually a `has_to_s…

…tring` instance

See leanprover#1664

library/init/meta/name.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.ordering init.coe
+import init.data.ordering init.coe init.data.to_string
 
 /-- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/
 inductive name
@@ -48,12 +48,12 @@ def name.update_prefix : name → name → name
 | (mk_string s p)  new_p := mk_string s new_p
 | (mk_numeral s p) new_p := mk_numeral s new_p
 
-def name.repr_with_sep (sep : string) : name → string
+def name.to_string_with_sep (sep : string) : name → string
 | anonymous                := "[anonymous]"
 | (mk_string s anonymous)  := s
 | (mk_numeral v anonymous) := repr v
-| (mk_string s n)          := name.repr_with_sep n ++ sep ++ s
-| (mk_numeral v n)         := name.repr_with_sep n ++ sep ++ repr v
+| (mk_string s n)          := name.to_string_with_sep n ++ sep ++ s
+| (mk_numeral v n)         := name.to_string_with_sep n ++ sep ++ repr v
 
 private def name.components' : name -> list name
 | anonymous                := []
@@ -63,14 +63,11 @@ private def name.components' : name -> list name
 def name.components (n : name) : list name :=
 (name.components' n).reverse
 
-protected def name.repr : name → string :=
-name.repr_with_sep "."
-
-instance : has_repr name :=
-⟨name.repr⟩
-
 protected def name.to_string : name → string :=
-name.repr
+name.to_string_with_sep "."
+
+instance : has_to_string name :=
+⟨name.to_string⟩
 
 /- TODO(Leo): provide a definition in Lean. -/
 meta constant name.has_decidable_eq : decidable_eq name

library/init/native/default.lean

@@ -184,7 +184,7 @@ meta def bind_value (val : ir.expr) (body : name → ir_compiler ir.stmt) : ir_c
 
 -- not in love with this --solution-- hack, revisit
 meta def compile_local (n : name) : ir_compiler name :=
-return $ (mk_str_name "_$local$_" (name.repr_with_sep "_" n))
+return $ (mk_str_name "_$local$_" (name.to_string_with_sep "_" n))
 
 meta def mk_invoke (loc : name) (args : list ir.expr) : ir_compiler ir.expr :=
 let args'' := list.map assert_name args
@@ -292,7 +292,7 @@ meta def compile_builtin_cases (action : expr → ir_compiler ir.stmt) (scrut :
   return $ (n, case) :: cs'
 
 meta def in_lean_ns (n : name) : name :=
-  mk_simple_name ("lean::" ++ name.repr_with_sep "_" n)
+  mk_simple_name ("lean::" ++ name.to_string_with_sep "_" n)
 
 meta def mk_builtin_cases_on (case_name scrut : name) (cases : list (nat × ir.stmt)) (default : ir.stmt) : ir.stmt :=
 -- replace `ctor_index with a generated name

library/init/native/format.lean

@@ -27,7 +27,7 @@ format_concat
 namespace format_cpp
 
 meta def mangle_name (n : name) : format :=
-    to_fmt $ name.repr_with_sep "_" n
+    to_fmt $ name.to_string_with_sep "_" n
 
 private meta def mk_constructor_args : list name → list format
 | [] := []
@@ -46,7 +46,7 @@ meta def literal : ir.literal → format
 | (ir.literal.nat n) := to_fmt "lean::mk_vm_nat(" ++ to_fmt n ++ ")"
 
 meta def format_local (n : name) : format :=
-  to_fmt (name.repr_with_sep "_" n)
+  to_fmt (name.to_string_with_sep "_" n)
 
 meta def string_lit (s : string) : format :=
   format.bracket "\"" "\"" (to_fmt s)
@@ -76,10 +76,10 @@ meta def expr' (action : ir.stmt → format) : ir.expr → format
 | (ir.expr.panic err_msg) :=
   to_fmt "throw std::runtime_error(" ++ string_lit err_msg ++ ");"
 | (ir.expr.mk_native_closure n args) :=
-"lean::mk_native_closure(*g_env, lean::name({\"" ++ name.repr_with_sep "\", \"" n ++ "\"})" ++ "," ++
+"lean::mk_native_closure(*g_env, lean::name({\"" ++ name.to_string_with_sep "\", \"" n ++ "\"})" ++ "," ++
    format.bracket "{" "}" (comma_sep (list.map format_local args)) ++ ")"
  | (ir.expr.invoke n args) :=
- "lean::invoke(" ++ name.repr_with_sep "_" n ++ ", " ++
+ "lean::invoke(" ++ name.to_string_with_sep "_" n ++ ", " ++
  (comma_sep (list.map format_local args)) ++ ")"
  | (ir.expr.uninitialized) := ";"
  | (ir.expr.assign n val) := mangle_name n ++ " = " ++ expr' val
@@ -149,7 +149,7 @@ meta def expr := expr' stmt
 meta def format_param (param : name × ir.ty) :=
 ty (prod.snd param) ++
 format.space ++
-to_fmt (name.repr_with_sep "_" (mk_str_name "_$local$_" (name.repr_with_sep "_" (prod.fst param))))
+to_fmt (name.to_string_with_sep "_" (mk_str_name "_$local$_" (name.to_string_with_sep "_" (prod.fst param))))
 
 meta def format_argument_list (tys : list (name × ir.ty)) : format :=
   format.bracket "(" ")" (comma_sep (list.map format_param tys))