refactor(library): add has_to_string back (but it produces unquoted values)

See issue #1664

leanpkg/leanpkg/main.lean

@@ -185,7 +185,7 @@ def main : ∀ (args : list string), io unit
       version := "1"
     } user_toml_fn,
   exec_cmd {cmd := "leanpkg", args := ["add", dep], cwd := dot_lean_dir}
-| ["dump"] := read_manifest >>= io.print_ln
+| ["dump"] := read_manifest >>= io.print_ln ∘ repr
 | _ := io.fail usage
 
 end leanpkg

library/init/data/basic.lean

@@ -10,3 +10,4 @@ import init.data.sigma.basic init.data.subtype.basic
 import init.data.fin.basic init.data.list.basic init.data.char.basic
 import init.data.string.basic init.data.option.basic init.data.set
 import init.data.unsigned.basic init.data.ordering init.data.repr
+import init.data.to_string

library/init/data/to_string.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.data.string.basic init.data.bool.basic init.data.subtype.basic
+import init.data.unsigned.basic init.data.prod init.data.sum.basic init.data.nat.div
+import init.data.repr
+open sum subtype nat
+
+universes u v
+
+class has_to_string (α : Type u) :=
+(to_string : α → string)
+
+def to_string {α : Type u} [has_to_string α] : α → string :=
+has_to_string.to_string
+
+instance : has_to_string string :=
+⟨λ s, s⟩
+
+instance : has_to_string bool :=
+⟨λ b, cond b "tt" "ff"⟩
+
+instance {p : Prop} : has_to_string (decidable p) :=
+-- Remark: type class inference will not consider local instance `b` in the new elaborator
+⟨λ b : decidable p, @ite p b _ "tt" "ff"⟩
+
+protected def list.to_string_aux {α : Type u} [has_to_string α] : bool → list α → string
+| b  []      := ""
+| tt (x::xs) := to_string x ++ list.to_string_aux ff xs
+| ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs
+
+protected def list.to_string {α : Type u} [has_to_string α] : list α → string
+| []      := "[]"
+| (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]"
+
+instance {α : Type u} [has_to_string α] : has_to_string (list α) :=
+⟨list.to_string⟩
+
+instance : has_to_string unit :=
+⟨λ u, "star"⟩
+
+instance : has_to_string nat :=
+⟨λ n, repr n⟩
+
+instance : has_to_string char :=
+⟨λ c, c.to_string⟩
+
+instance (n : nat) : has_to_string (fin n) :=
+⟨λ f, to_string (fin.val f)⟩
+
+instance : has_to_string unsigned :=
+⟨λ n, to_string (fin.val n)⟩
+
+instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
+⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end⟩
+
+instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α ⊕ β) :=
+⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end⟩
+
+instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α × β) :=
+⟨λ ⟨a, b⟩, "(" ++ to_string a ++ ", " ++ to_string b ++ ")"⟩
+
+instance {α : Type u} {β : α → Type v} [has_to_string α] [s : ∀ x, has_to_string (β x)] : has_to_string (sigma β) :=
+⟨λ ⟨a, b⟩, "⟨"  ++ to_string a ++ ", " ++ to_string b ++ "⟩"⟩
+
+instance {α : Type u} {p : α → Prop} [has_to_string α] : has_to_string (subtype p) :=
+⟨λ s, to_string (val s)⟩

library/init/meta/exceptional.lean

@@ -16,7 +16,6 @@ meta inductive exceptional (α : Type)
 section
 open exceptional
 variables {α : Type}
-/- TODO(Leo): has_to_string
 variables [has_to_string α]
 
 protected meta def exceptional.to_string : exceptional α → string
@@ -25,7 +24,6 @@ protected meta def exceptional.to_string : exceptional α → string
 
 meta instance : has_to_string (exceptional α) :=
 has_to_string.mk exceptional.to_string
--/
 end
 
 namespace exceptional

library/init/meta/format.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.options init.function
+import init.meta.options init.function init.data.to_string
 
 universes u v
 
@@ -33,10 +33,8 @@ meta instance : inhabited format :=
 meta instance : has_append format :=
 ⟨format.compose⟩
 
-/- TODO(Leo): has_to_string
 meta instance : has_to_string format :=
 ⟨λ f, format.to_string f options.mk⟩
--/
 
 meta class has_to_format (α : Type u) :=
 (to_format : α → format)

library/init/meta/interaction_monad.lean

@@ -7,7 +7,7 @@ prelude
 import init.function init.data.option.basic init.util
 import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail
 import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment
-import init.meta.pexpr init.data.repr init.data.string.basic
+import init.meta.pexpr init.data.repr init.data.string.basic init.data.to_string
 
 universes u v
 
@@ -18,8 +18,6 @@ meta inductive interaction_monad.result (state : Type) (α : Type u)
 open interaction_monad.result
 
 section
-
-/- TODO(Leo): has_to_string
 variables {state : Type} {α : Type u}
 variables [has_to_string α]
 
@@ -30,7 +28,6 @@ meta def interaction_monad.result_to_string : result state α → string
 
 meta instance interaction_monad.result_has_string : has_to_string (result state α) :=
 ⟨interaction_monad.result_to_string⟩
--/
 end
 
 meta def interaction_monad.result.clamp_pos {state : Type} {α : Type u} (line0 line col : ℕ) : result state α → result state α

library/init/meta/tactic.lean

@@ -29,10 +29,8 @@ end tactic_state
 meta instance : has_to_format tactic_state :=
 ⟨tactic_state.to_format⟩
 
-/- TODO(Leo): has_to_string
 meta instance : has_to_string tactic_state :=
-⟨λ s, (to_fmt s).to_string s.get_options⟩
--/
+⟨λ s, format.to_string (to_fmt s) s.get_options⟩
 
 @[reducible] meta def tactic := interaction_monad tactic_state
 @[reducible] meta def tactic_result := interaction_monad.result tactic_state
@@ -958,7 +956,7 @@ do dec_e ← (mk_app `decidable [e] <|> fail "by_cases tactic failed, type is no
    swap
 
 private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i :=
-let n := base <.> ("_aux_" ++ to_string i) in
+let n := base <.> ("_aux_" ++ repr i) in
 if ¬env.contains n then n
 else get_undeclared_const (i+1)
 

library/system/io.lean

@@ -128,11 +128,10 @@ interface.term.get_line
 def cmdline_args : io (list string) :=
 return interface.term.cmdline_args
 
-/- TODO(Leo): has_to_string -/
-def print {α} [has_repr α] (s : α) : io unit :=
-put_str ∘ repr $ s
+def print {α} [has_to_string α] (s : α) : io unit :=
+put_str ∘ to_string $ s
 
-def print_ln {α} [has_repr α] (s : α) : io unit :=
+def print_ln {α} [has_to_string α] (s : α) : io unit :=
 print s >> put_str "\n"
 
 def handle : Type :=