From 10c32fcf94a7963e71d59f3c3c537507366f0761 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 16:11:48 -0700 Subject: [PATCH] chore: `HasToString` => `ToString` --- src/Init/Control/EState.lean | 2 +- src/Init/Control/Except.lean | 4 +- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/ByteArray/Basic.lean | 2 +- src/Init/Data/Float.lean | 2 +- src/Init/Data/FloatArray/Basic.lean | 2 +- src/Init/Data/Int/Basic.lean | 2 +- src/Init/Data/ToString/Basic.lean | 60 +++++++++---------- src/Init/LeanInit.lean | 2 +- src/Init/System/IO.lean | 10 ++-- src/Init/System/IOError.lean | 2 +- src/Init/Util.lean | 2 +- src/Lean/Compiler/IR/Basic.lean | 4 +- src/Lean/Compiler/IR/Borrow.lean | 2 +- src/Lean/Compiler/IR/ElimDeadBranches.lean | 2 +- src/Lean/Compiler/IR/EmitC.lean | 6 +- src/Lean/Compiler/IR/Format.lean | 8 +-- src/Lean/Data/Format.lean | 4 +- src/Lean/Data/Json/Basic.lean | 2 +- src/Lean/Data/Json/Printer.lean | 2 +- src/Lean/Data/KVMap.lean | 4 +- src/Lean/Data/LBool.lean | 2 +- src/Lean/Data/LOption.lean | 2 +- src/Lean/Data/Lsp/Basic.lean | 2 +- src/Lean/Data/OpenDecl.lean | 2 +- src/Lean/Data/Options.lean | 2 +- src/Lean/Data/Position.lean | 2 +- src/Lean/Data/Trie.lean | 2 +- src/Lean/Elab/App.lean | 4 +- src/Lean/Elab/DeclModifiers.lean | 4 +- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/StructInst.lean | 4 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Environment.lean | 2 +- src/Lean/Exception.lean | 2 +- src/Lean/Expr.lean | 4 +- src/Lean/Level.lean | 2 +- src/Lean/Meta/RecursorInfo.lean | 4 +- src/Lean/MetavarContext.lean | 2 +- src/Lean/Parser/Basic.lean | 4 +- src/Lean/Syntax.lean | 2 +- src/Std/Data/PersistentArray.lean | 2 +- src/Std/Data/PersistentHashMap.lean | 2 +- tests/bench/deriv.lean | 2 +- tests/compiler/float_cases_bug.lean | 2 +- tests/compiler/reusebug.lean | 2 +- tests/compiler/t2.lean | 2 +- tests/compiler/t4.lean | 2 +- tests/compiler/termparsertest1.lean | 2 +- .../termparsertest1.lean.expected.out | 4 +- ...compiler_slow_with_many_constructors2.lean | 2 +- tests/elabissues/vars.lean | 6 +- tests/lean/PPRoundtrip.lean | 4 +- tests/lean/PPRoundtrip.lean.expected.out | 5 +- tests/lean/StxQuot.lean | 2 +- tests/lean/run/catchThe.lean | 2 +- tests/lean/run/deriv.lean | 4 +- tests/lean/run/doNotation1.lean | 2 +- tests/lean/run/doNotation4.lean | 2 +- tests/lean/run/doNotation6.lean | 2 +- tests/lean/run/forBodyResultTypeIssue.lean | 4 +- tests/lean/run/frontend1.lean | 10 ++-- tests/lean/run/meta2.lean | 8 +-- tests/lean/run/synth1.lean | 2 +- tests/lean/run/termparsertest1.lean | 2 +- tests/lean/run/toExpr.lean | 2 +- tests/lean/run/typeclass_easy.lean | 2 +- tests/playground/eval2.lean | 2 +- tests/playground/lazylist.lean | 6 +- tests/playground/parser/syntax.lean | 2 +- tests/playground/pldi/intro.lean | 6 +- tests/playground/termparsertest1.lean | 2 +- 72 files changed, 138 insertions(+), 139 deletions(-) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 8dbb0a399f..5109250d33 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -16,7 +16,7 @@ inductive Result (ε σ α : Type u) variables {ε σ α : Type u} -instance [HasToString ε] [HasToString α] : HasToString (Result ε σ α) := { +instance [ToString ε] [ToString α] : ToString (Result ε σ α) := { toString := fun | Result.ok a _ => "ok: " ++ toString a | Result.error e _ => "error: " ++ toString e diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 050bc64c25..340d2537cf 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -26,7 +26,7 @@ instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) : section variables {ε : Type u} {α : Type v} -protected def Except.toString [HasToString ε] [HasToString α] : Except ε α → String +protected def Except.toString [ToString ε] [ToString α] : Except ε α → String | Except.error e => "(error " ++ toString e ++ ")" | Except.ok a => "(ok " ++ toString a ++ ")" @@ -34,7 +34,7 @@ protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String | Except.error e => "(error " ++ repr e ++ ")" | Except.ok a => "(ok " ++ repr a ++ ")" -instance [HasToString ε] [HasToString α] : HasToString (Except ε α) := ⟨Except.toString⟩ +instance [ToString ε] [ToString α] : ToString (Except ε α) := ⟨Except.toString⟩ instance [HasRepr ε] [HasRepr α] : HasRepr (Except ε α) := ⟨Except.repr⟩ end diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index ab7cfe2b05..d1b59cc00d 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -440,7 +440,7 @@ a.foldr List.cons [] instance [HasRepr α] : HasRepr (Array α) := ⟨fun a => "#" ++ repr a.toList⟩ -instance [HasToString α] : HasToString (Array α) := +instance [ToString α] : ToString (Array α) := ⟨fun a => "#" ++ toString a.toList⟩ section diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 0429efa323..941c21d047 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -84,4 +84,4 @@ def List.toByteArray (bs : List UInt8) : ByteArray := | b::bs, r => loop bs (r.push b) loop bs ByteArray.empty -instance : HasToString ByteArray := ⟨fun bs => bs.toList.toString⟩ +instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩ diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 4314affcce..60ea966a8e 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -69,7 +69,7 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b @[extern "lean_float_to_string"] constant Float.toString : Float → String -instance : HasToString Float := ⟨Float.toString⟩ +instance : ToString Float := ⟨Float.toString⟩ abbrev Nat.toFloat (n : Nat) : Float := Float.ofNat n diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index bf86c2c564..b57e99fd89 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -77,4 +77,4 @@ def List.toFloatArray (ds : List Float) : FloatArray := loop ds FloatArray.empty -instance : HasToString FloatArray := ⟨fun ds => ds.toList.toString⟩ +instance : ToString FloatArray := ⟨fun ds => ds.toList.toString⟩ diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 6a8a23fce3..fb379da266 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -123,7 +123,7 @@ protected def repr : Int → String | negSucc m => "-" ++ Nat.repr (succ m) instance : HasRepr Int := ⟨Int.repr⟩ -instance : HasToString Int := ⟨Int.repr⟩ +instance : ToString Int := ⟨Int.repr⟩ instance : HasOfNat Int := ⟨Int.ofNat⟩ @[extern "lean_int_div"] diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index abe8092a99..f6d464d233 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -13,78 +13,78 @@ open Sum Subtype Nat universes u v -class HasToString (α : Type u) := +class ToString (α : Type u) := (toString : α → String) -export HasToString (toString) +export ToString (toString) -- This instance is needed because `id` is not reducible -instance {α} [HasToString α] : HasToString (id α) := - inferInstanceAs (HasToString α) +instance {α} [ToString α] : ToString (id α) := + inferInstanceAs (ToString α) -instance {α} [HasToString α] : HasToString (Id α) := - inferInstanceAs (HasToString α) +instance {α} [ToString α] : ToString (Id α) := + inferInstanceAs (ToString α) -instance : HasToString String := +instance : ToString String := ⟨fun s => s⟩ -instance : HasToString Substring := +instance : ToString Substring := ⟨fun s => s.toString⟩ -instance : HasToString String.Iterator := +instance : ToString String.Iterator := ⟨fun it => it.remainingToString⟩ -instance : HasToString Bool := +instance : ToString Bool := ⟨fun b => cond b "true" "false"⟩ -instance {p : Prop} : HasToString (Decidable p) := ⟨fun h => +instance {p : Prop} : ToString (Decidable p) := ⟨fun h => match h with | Decidable.isTrue _ => "true" | Decidable.isFalse _ => "false"⟩ -protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String +protected def List.toStringAux {α : Type u} [ToString α] : Bool → List α → String | b, [] => "" | true, x::xs => toString x ++ List.toStringAux false xs | false, x::xs => ", " ++ toString x ++ List.toStringAux false xs -protected def List.toString {α : Type u} [HasToString α] : List α → String +protected def List.toString {α : Type u} [ToString α] : List α → String | [] => "[]" | x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]" -instance {α : Type u} [HasToString α] : HasToString (List α) := +instance {α : Type u} [ToString α] : ToString (List α) := ⟨List.toString⟩ -instance : HasToString PUnit.{u+1} := +instance : ToString PUnit.{u+1} := ⟨fun _ => "()"⟩ -instance {α : Type u} [HasToString α] : HasToString (ULift.{v} α) := +instance {α : Type u} [ToString α] : ToString (ULift.{v} α) := ⟨fun v => toString v.1⟩ -instance : HasToString Unit := +instance : ToString Unit := ⟨fun u => "()"⟩ -instance : HasToString Nat := +instance : ToString Nat := ⟨fun n => repr n⟩ -instance : HasToString Char := +instance : ToString Char := ⟨fun c => c.toString⟩ -instance (n : Nat) : HasToString (Fin n) := +instance (n : Nat) : ToString (Fin n) := ⟨fun f => toString (Fin.val f)⟩ -instance : HasToString UInt8 := +instance : ToString UInt8 := ⟨fun n => toString n.toNat⟩ -instance : HasToString UInt16 := +instance : ToString UInt16 := ⟨fun n => toString n.toNat⟩ -instance : HasToString UInt32 := +instance : ToString UInt32 := ⟨fun n => toString n.toNat⟩ -instance : HasToString UInt64 := +instance : ToString UInt64 := ⟨fun n => toString n.toNat⟩ -instance : HasToString USize := +instance : ToString USize := ⟨fun n => toString n.toNat⟩ def addParenHeuristic (s : String) : String := @@ -92,19 +92,19 @@ def addParenHeuristic (s : String) : String := else if !s.any Char.isWhitespace then s else "(" ++ s ++ ")" -instance {α : Type u} [HasToString α] : HasToString (Option α) := ⟨fun +instance {α : Type u} [ToString α] : ToString (Option α) := ⟨fun | none => "none" | (some a) => "(some " ++ addParenHeuristic (toString a) ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) := ⟨fun +instance {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (Sum α β) := ⟨fun | (inl a) => "(inl " ++ addParenHeuristic (toString a) ++ ")" | (inr b) => "(inr " ++ addParenHeuristic (toString b) ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) := ⟨fun (a, b) => +instance {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (α × β) := ⟨fun (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩ -instance {α : Type u} {β : α → Type v} [HasToString α] [s : ∀ x, HasToString (β x)] : HasToString (Sigma β) := ⟨fun ⟨a, b⟩ => +instance {α : Type u} {β : α → Type v} [ToString α] [s : ∀ x, ToString (β x)] : ToString (Sigma β) := ⟨fun ⟨a, b⟩ => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩"⟩ -instance {α : Type u} {p : α → Prop} [HasToString α] : HasToString (Subtype p) := ⟨fun s => +instance {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p) := ⟨fun s => toString (val s)⟩ diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 463eb0d7b2..8356a6d9f1 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -100,7 +100,7 @@ def toStringWithSep (sep : String) : Name → String protected def toString : Name → String := toStringWithSep "." -instance : HasToString Name := ⟨Name.toString⟩ +instance : ToString Name := ⟨Name.toString⟩ protected def append : Name → Name → Name | n, anonymous => n diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index da41c5b8da..749088a9e2 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -85,7 +85,7 @@ instance : MonadIO IO := namespace IO -def ofExcept {ε α : Type} [HasToString ε] (e : Except ε α) : IO α := +def ofExcept {ε α : Type} [ToString ε] (e : Except ε α) : IO α := match e with | Except.ok a => pure a | Except.error e => throw (IO.userError (toString e)) @@ -279,17 +279,17 @@ def withStderr [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do let prev ← setStderr h try x finally discard $ setStderr prev -def print {α} [HasToString α] (s : α) : m Unit := do +def print {α} [ToString α] (s : α) : m Unit := do let out ← getStdout liftIO $ out.putStr $ toString s -def println {α} [HasToString α] (s : α) : m Unit := print ((toString s).push '\n') +def println {α} [ToString α] (s : α) : m Unit := print ((toString s).push '\n') -def eprint {α} [HasToString α] (s : α) : m Unit := do +def eprint {α} [ToString α] (s : α) : m Unit := do let out ← getStderr liftIO $ out.putStr $ toString s -def eprintln {α} [HasToString α] (s : α) : m Unit := eprint ((toString s).push '\n') +def eprintln {α} [ToString α] (s : α) : m Unit := eprint ((toString s).push '\n') @[export lean_io_eprintln] private def eprintlnAux (s : String) : IO Unit := eprintln s diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 058b618344..ec2f88e52b 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -187,7 +187,7 @@ def toString : IO.Error → String | unsupportedOperation code details => otherErrorToString "unsupported operation" code details | userError msg => msg -instance : HasToString IO.Error := ⟨ IO.Error.toString ⟩ +instance : ToString IO.Error := ⟨ IO.Error.toString ⟩ instance : Inhabited IO.Error := ⟨ userError "" ⟩ end IO.Error diff --git a/src/Init/Util.lean b/src/Init/Util.lean index f4dd98f92f..1e4a8d0a06 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -12,7 +12,7 @@ universes u v @[neverExtract, extern "lean_dbg_trace"] def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α := f () -def dbgTraceVal {α : Type u} [HasToString α] (a : α) : α := +def dbgTraceVal {α : Type u} [ToString α] (a : α) : α := dbgTrace (toString a) (fun _ => a) /- Display the given message if `a` is shared, that is, RC(a) > 1 -/ diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index bc32edf240..b08f7618dd 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -28,12 +28,12 @@ structure JoinPointId := (idx : Index) abbrev Index.lt (a b : Index) : Bool := a < b instance : HasBeq VarId := ⟨fun a b => a.idx == b.idx⟩ -instance : HasToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩ +instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩ instance : HasFormat VarId := ⟨fun a => toString a⟩ instance : Hashable VarId := ⟨fun a => hash a.idx⟩ instance : HasBeq JoinPointId := ⟨fun a b => a.idx == b.idx⟩ -instance : HasToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩ +instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩ instance : HasFormat JoinPointId := ⟨fun a => toString a⟩ instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩ diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index ce15e1c7ee..e6de57cc9c 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -65,7 +65,7 @@ let fmts := map.fold (fun fmt k ps => "{" ++ (Format.nest 1 fmts) ++ "}" instance : HasFormat ParamMap := ⟨ParamMap.fmt⟩ -instance : HasToString ParamMap := ⟨fun m => Format.pretty (format m)⟩ +instance : ToString ParamMap := ⟨fun m => Format.pretty (format m)⟩ namespace InitParamMap /- Mark parameters that take a reference as borrow -/ diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index f46cb1d662..f099938840 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -58,7 +58,7 @@ protected partial def format : Value → Format | ctor i vs => fmt "#" ++ if vs.isEmpty then fmt i.name else Format.paren (fmt i.name ++ @formatArray _ ⟨Value.format⟩ vs) instance : HasFormat Value := ⟨Value.format⟩ -instance : HasToString Value := ⟨Format.pretty ∘ Value.format⟩ +instance : ToString Value := ⟨Format.pretty ∘ Value.format⟩ /- Make sure constructors of recursive inductive datatypes can only occur once in each path. We use this function this function to implement a simple widening operation for our abstract diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index 3e06dd42f6..b93b18beae 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -35,13 +35,13 @@ match findEnvDecl env n with | some d => pure d | none => throw s!"unknown declaration '{n}'" -@[inline] def emit {α : Type} [HasToString α] (a : α) : M Unit := +@[inline] def emit {α : Type} [ToString α] (a : α) : M Unit := modify fun out => out ++ toString a -@[inline] def emitLn {α : Type} [HasToString α] (a : α) : M Unit := do +@[inline] def emitLn {α : Type} [ToString α] (a : α) : M Unit := do emit a; emit "\n" -def emitLns {α : Type} [HasToString α] (as : List α) : M Unit := +def emitLns {α : Type} [ToString α] (as : List α) : M Unit := as.forM fun a => emitLn a def argToCString (x : Arg) : String := diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean index 9bce7d53bf..ca093256d8 100644 --- a/src/Lean/Compiler/IR/Format.lean +++ b/src/Lean/Compiler/IR/Format.lean @@ -52,7 +52,7 @@ private def formatExpr : Expr → Format | Expr.isTaggedPtr x => "isTaggedPtr " ++ format x instance : HasFormat Expr := ⟨formatExpr⟩ -instance : HasToString Expr := ⟨fun e => Format.pretty (format e)⟩ +instance : ToString Expr := ⟨fun e => Format.pretty (format e)⟩ private partial def formatIRType : IRType → Format | IRType.float => "float" @@ -68,7 +68,7 @@ private partial def formatIRType : IRType → Format | IRType.union _ tys => "union " ++ Format.bracket "{" (@Format.joinSep _ ⟨formatIRType⟩ tys.toList ", ") "}" instance : HasFormat IRType := ⟨formatIRType⟩ -instance : HasToString IRType := ⟨toString ∘ format⟩ +instance : ToString IRType := ⟨toString ∘ format⟩ private def formatParam : Param → Format | { x := name, borrow := b, ty := ty } => "(" ++ format name ++ " : " ++ (if b then "@& " else "") ++ format ty ++ ")" @@ -118,7 +118,7 @@ partial def formatFnBody (fnBody : FnBody) (indent : Nat := 2) : Format := loop fnBody instance : HasFormat FnBody := ⟨formatFnBody⟩ -instance : HasToString FnBody := ⟨fun b => (format b).pretty⟩ +instance : ToString FnBody := ⟨fun b => (format b).pretty⟩ def formatDecl (decl : Decl) (indent : Nat := 2) : Format := match decl with @@ -131,6 +131,6 @@ instance : HasFormat Decl := ⟨formatDecl⟩ def declToString (d : Decl) : String := (format d).pretty -instance : HasToString Decl := ⟨declToString⟩ +instance : ToString Decl := ⟨declToString⟩ end Lean.IR diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean index 3088895a2d..bc372b7d84 100644 --- a/src/Lean/Data/Format.lean +++ b/src/Lean/Data/Format.lean @@ -207,7 +207,7 @@ export Lean.HasFormat (format) def fmt {α : Type u} [HasFormat α] : α → Format := format -instance {α : Type u} [HasToString α] : HasFormat α := ⟨text ∘ toString⟩ +instance {α : Type u} [ToString α] : HasFormat α := ⟨text ∘ toString⟩ -- note: must take precendence over the above instance to avoid premature formatting instance : HasFormat Format := ⟨id⟩ @@ -271,7 +271,7 @@ protected def Format.repr : Format → Format | group f FlattenBehavior.allOrNone => paren $ "Format.group" ++ line ++ Format.repr f | group f FlattenBehavior.fill => paren $ "Format.fill" ++ line ++ Format.repr f -instance : HasToString Format := ⟨Format.pretty⟩ +instance : ToString Format := ⟨Format.pretty⟩ instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩ diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 95d75565d1..a6cc4a6062 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -71,7 +71,7 @@ protected def shiftl : JsonNumber → Nat → JsonNumber protected def shiftr : JsonNumber → Nat → JsonNumber | ⟨m, e⟩, s => ⟨m, e + s⟩ -instance : HasToString JsonNumber := ⟨JsonNumber.toString⟩ +instance : ToString JsonNumber := ⟨JsonNumber.toString⟩ instance : HasRepr JsonNumber := ⟨fun ⟨m, e⟩ => "⟨" ++ m.repr ++ "," ++ e.repr ++ "⟩"⟩ diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean index fadd652911..00da573760 100644 --- a/src/Lean/Data/Json/Printer.lean +++ b/src/Lean/Data/Json/Printer.lean @@ -79,7 +79,7 @@ partial def compress : Json → String "{" ++ ",".intercalate ckvs ++ "}" instance : HasFormat Json := ⟨render⟩ -instance : HasToString Json := ⟨pretty⟩ +instance : ToString Json := ⟨pretty⟩ end Json end Lean diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean index 3562741302..b904b7af78 100644 --- a/src/Lean/Data/KVMap.lean +++ b/src/Lean/Data/KVMap.lean @@ -43,7 +43,7 @@ def DataValue.str : DataValue → String | DataValue.ofNat v => toString v | DataValue.ofInt v => toString v -instance : HasToString DataValue := ⟨DataValue.str⟩ +instance : ToString DataValue := ⟨DataValue.str⟩ instance : Coe String DataValue := ⟨DataValue.ofString⟩ instance : Coe Bool DataValue := ⟨DataValue.ofBool⟩ @@ -59,7 +59,7 @@ structure KVMap := namespace KVMap instance : Inhabited KVMap := ⟨{}⟩ -instance : HasToString KVMap := ⟨fun m => toString m.entries⟩ +instance : ToString KVMap := ⟨fun m => toString m.entries⟩ def empty : KVMap := {} diff --git a/src/Lean/Data/LBool.lean b/src/Lean/Data/LBool.lean index 009fd57077..1aae19673c 100644 --- a/src/Lean/Data/LBool.lean +++ b/src/Lean/Data/LBool.lean @@ -37,7 +37,7 @@ def toString : LBool → String | false => "false" | undef => "undef" -instance : HasToString LBool := ⟨toString⟩ +instance : ToString LBool := ⟨toString⟩ end LBool diff --git a/src/Lean/Data/LOption.lean b/src/Lean/Data/LOption.lean index a6aee94c4b..c5e4e5f988 100644 --- a/src/Lean/Data/LOption.lean +++ b/src/Lean/Data/LOption.lean @@ -17,7 +17,7 @@ variables {α : Type u} instance : Inhabited (LOption α) := ⟨none⟩ -instance [HasToString α] : HasToString (LOption α) := +instance [ToString α] : ToString (LOption α) := ⟨fun o => match o with | none => "none" | undef => "undef" | (some a) => "(some " ++ toString a ++ ")"⟩ def beq [HasBeq α] : LOption α → LOption α → Bool diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index ecb3d6b150..cd68a6ddfe 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -37,7 +37,7 @@ instance : HasToJson Position := ⟨fun o => ⟨"line", o.line⟩, ⟨"character", o.character⟩]⟩ -instance : HasToString Position := ⟨fun p => +instance : ToString Position := ⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ structure Range := (start : Position) («end» : Position) diff --git a/src/Lean/Data/OpenDecl.lean b/src/Lean/Data/OpenDecl.lean index 30e2f79c24..1266ebd355 100644 --- a/src/Lean/Data/OpenDecl.lean +++ b/src/Lean/Data/OpenDecl.lean @@ -14,7 +14,7 @@ inductive OpenDecl namespace OpenDecl instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩ -instance : HasToString OpenDecl := +instance : ToString OpenDecl := ⟨fun decl => match decl with | explicit id decl => toString id ++ " → " ++ toString decl | simple ns ex => toString ns ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩ diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 225ba45ab9..78c88d7aa9 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -11,7 +11,7 @@ def Options := KVMap def Options.empty : Options := {} instance : Inhabited Options := ⟨Options.empty⟩ -instance : HasToString Options := inferInstanceAs (HasToString KVMap) +instance : ToString Options := inferInstanceAs (ToString KVMap) structure OptionDecl := (defValue : DataValue) diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index a267fec7cf..da3f5dad5d 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -28,7 +28,7 @@ protected def lt : Position → Position → Bool instance : HasFormat Position := ⟨fun ⟨l, c⟩ => "⟨" ++ fmt l ++ ", " ++ fmt c ++ "⟩"⟩ -instance : HasToString Position := +instance : ToString Position := ⟨fun ⟨l, c⟩ => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩"⟩ instance : Inhabited Position := ⟨⟨1, 0⟩⟩ diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index 08f36fe936..209931b00f 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -84,7 +84,7 @@ private partial def toStringAux {α : Type} : Trie α → List Format | Trie.Node val map => map.fold (fun Fs c t => format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] -instance {α : Type} : HasToString (Trie α) := +instance {α : Type} : ToString (Trie α) := ⟨fun t => (flip Format.joinSep Format.line $ toStringAux t).pretty⟩ end Trie diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index c7ba737465..81aa291467 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -20,7 +20,7 @@ inductive Arg instance : Inhabited Arg := ⟨Arg.stx (arbitrary _)⟩ -instance : HasToString Arg := ⟨fun +instance : ToString Arg := ⟨fun | Arg.stx val => toString val | Arg.expr val => toString val⟩ @@ -30,7 +30,7 @@ structure NamedArg := (name : Name) (val : Arg) -instance : HasToString NamedArg := +instance : ToString NamedArg := ⟨fun s => "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")"⟩ instance : Inhabited NamedArg := ⟨{ name := arbitrary _, val := arbitrary _ }⟩ diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 08957a921a..9035570ec1 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -27,7 +27,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception inductive Visibility | regular | «protected» | «private» -instance : HasToString Visibility := ⟨fun +instance : ToString Visibility := ⟨fun | Visibility.regular => "regular" | Visibility.«private» => "private" | Visibility.«protected» => "protected"⟩ @@ -66,7 +66,7 @@ instance : HasFormat Modifiers := ⟨fun m => ++ m.attrs.toList.map (fun attr => fmt attr) Format.bracket "{" (Format.joinSep components ("," ++ Format.line)) "}"⟩ -instance : HasToString Modifiers := ⟨toString ∘ format⟩ +instance : ToString Modifiers := ⟨toString ∘ format⟩ section Methods diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index e01a713d27..af0706577e 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -157,7 +157,7 @@ inductive PatternVar -- anonymous variables (`_`) are encoded using metavariables | anonymousVar (mvarId : MVarId) -instance : HasToString PatternVar := ⟨fun +instance : ToString PatternVar := ⟨fun | PatternVar.localVar x => toString x | PatternVar.anonymousVar mvarId => s!"?m{mvarId}"⟩ diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 6091d6ca4c..687a32583d 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -232,10 +232,10 @@ partial def formatStruct : Struct → Format | Source.explicit _ src => "{" ++ format src ++ " with " ++ fieldsFmt ++ "}" instance : HasFormat Struct := ⟨formatStruct⟩ -instance : HasToString Struct := ⟨toString ∘ format⟩ +instance : ToString Struct := ⟨toString ∘ format⟩ instance : HasFormat (Field Struct) := ⟨formatField formatStruct⟩ -instance : HasToString (Field Struct) := ⟨toString ∘ format⟩ +instance : ToString (Field Struct) := ⟨toString ∘ format⟩ /- Recall that `structInstField` elements have the form diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index b5afeb0120..86dfc5a8c9 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -272,7 +272,7 @@ inductive LVal | fieldName (name : String) | getOp (idx : Syntax) -instance : HasToString LVal := ⟨fun +instance : ToString LVal := ⟨fun | LVal.fieldIdx i => toString i | LVal.fieldName n => n | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩ diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e8f1826112..02ec87117b 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -27,7 +27,7 @@ structure Import := (module : Name) (runtimeOnly : Bool := false) -instance : HasToString Import := ⟨fun imp => toString imp.module ++ if imp.runtimeOnly then " (runtime)" else ""⟩ +instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtimeOnly then " (runtime)" else ""⟩ /-- A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk. diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index 43f3765929..b5e8f1260d 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -73,7 +73,7 @@ def throwUnknownConstant {α} (constName : Name) : m α := def throwErrorAt {α} (ref : Syntax) (msg : MessageData) : m α := do withRef ref $ throwError msg -def ofExcept {ε α} [HasToString ε] (x : Except ε α) : m α := +def ofExcept {ε α} [ToString ε] (x : Except ε α) : m α := match x with | Except.ok a => pure a | Except.error e => throwError $ toString e diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index a994ebdfc5..abaf1dfd9c 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -679,7 +679,7 @@ def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr := def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr := (e.abstract fvars).instantiateRev vs -instance : HasToString Expr := ⟨Expr.dbgToString⟩ +instance : ToString Expr := ⟨Expr.dbgToString⟩ -- TODO: should not use dbgToString, but constructors. instance : HasRepr Expr := ⟨Expr.dbgToString⟩ @@ -737,7 +737,7 @@ protected def hash : ExprStructEq → USize instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩ instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩ instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩ -instance : HasToString ExprStructEq := ⟨fun e => toString e.val⟩ +instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩ instance : HasRepr ExprStructEq := ⟨fun e => repr e.val⟩ end ExprStructEq diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 12857c840a..74752f8677 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -413,7 +413,7 @@ protected def format (l : Level) : Format := (LevelToFormat.toResult l).format true instance : HasFormat Level := ⟨Level.format⟩ -instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩ +instance : ToString Level := ⟨Format.pretty ∘ Level.format⟩ /- The update functions here are defined using C code. They will try to avoid allocating new values using pointer equality. diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 1c13043e94..d9759602eb 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -23,7 +23,7 @@ inductive RecursorUnivLevelPos | motive -- marks where the universe of the motive should go | majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes -instance : HasToString RecursorUnivLevelPos := ⟨fun +instance : ToString RecursorUnivLevelPos := ⟨fun | RecursorUnivLevelPos.motive => "" | RecursorUnivLevelPos.majorType idx => toString idx⟩ @@ -56,7 +56,7 @@ def numMinors (info : RecursorInfo) : Nat := let r := r - info.motivePos - 1 r - (info.majorPos + 1 - info.firstIndexPos) -instance : HasToString RecursorInfo := ⟨fun info => +instance : ToString RecursorInfo := ⟨fun info => "{\n" ++ " name := " ++ toString info.recursorName ++ "\n" ++ " type := " ++ toString info.typeName ++ "\n" ++ diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index e3ac69ac60..aaf930193c 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -697,7 +697,7 @@ protected def Exception.toString : Exception → String ++ ", '" ++ toString decl.userName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator" ++ " (possible solution: use tactic 'clear' to remove '" ++ toString decl.userName ++ "' from local context)" -instance : HasToString Exception := ⟨Exception.toString⟩ +instance : ToString Exception := ⟨Exception.toString⟩ /-- `MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`. diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 4eff9fdaaa..c24ff6b8fb 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -153,7 +153,7 @@ protected def toString (e : Error) : String := ["expected " ++ expectedToString expected] "; ".intercalate $ unexpected ++ expected -instance : HasToString Error := ⟨Error.toString⟩ +instance : ToString Error := ⟨Error.toString⟩ protected def beq (e₁ e₂ : Error) : Bool := e₁.unexpected == e₂.unexpected && e₁.expected == e₂.expected @@ -290,7 +290,7 @@ def toStr : FirstTokens → String | tokens tks => toString tks | optTokens tks => "?" ++ toString tks -instance : HasToString FirstTokens := ⟨toStr⟩ +instance : ToString FirstTokens := ⟨toStr⟩ end FirstTokens diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 9a55395964..ffafa3b03c 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -322,7 +322,7 @@ def formatStx (stx : Syntax) (maxDepth : Option Nat := none) (showInfo := false) formatStxAux maxDepth showInfo 0 stx instance : HasFormat (Syntax) := ⟨formatStx⟩ -instance : HasToString (Syntax) := ⟨toString ∘ format⟩ +instance : ToString (Syntax) := ⟨toString ∘ format⟩ partial def structEq : Syntax → Syntax → Bool | Syntax.missing, Syntax.missing => true diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index e658487966..c9ed9d910f 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -345,7 +345,7 @@ collectStats r.root { numNodes := 0, depth := 0, tailSize := r.tail.size } 0 def Stats.toString (s : Stats) : String := s!"\{nodes := {s.numNodes}, depth := {s.depth}, tail size := {s.tailSize}}" -instance : HasToString Stats := ⟨Stats.toString⟩ +instance : ToString Stats := ⟨Stats.toString⟩ end PersistentArray diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean index aa682289b6..3a7f9ea8d1 100644 --- a/src/Std/Data/PersistentHashMap.lean +++ b/src/Std/Data/PersistentHashMap.lean @@ -319,7 +319,7 @@ collectStats m.root {} 1 def Stats.toString (s : Stats) : String := s!"\{ nodes := {s.numNodes}, null := {s.numNull}, collisions := {s.numCollisions}, depth := {s.maxDepth}}" -instance : HasToString Stats := ⟨Stats.toString⟩ +instance : ToString Stats := ⟨Stats.toString⟩ end PersistentHashMap end Std diff --git a/tests/bench/deriv.lean b/tests/bench/deriv.lean index 1c70bc3091..ecce838619 100644 --- a/tests/bench/deriv.lean +++ b/tests/bench/deriv.lean @@ -74,7 +74,7 @@ protected def Expr.toString : Expr → String | Pow f g => "(" ++ Expr.toString f ++ " ^ " ++ Expr.toString g ++ ")" | Ln f => "ln(" ++ Expr.toString f ++ ")" -instance : HasToString Expr := +instance : ToString Expr := ⟨Expr.toString⟩ def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr diff --git a/tests/compiler/float_cases_bug.lean b/tests/compiler/float_cases_bug.lean index e789988e21..1ac9b2673e 100644 --- a/tests/compiler/float_cases_bug.lean +++ b/tests/compiler/float_cases_bug.lean @@ -6,7 +6,7 @@ inductive Term : Type namespace Term instance : Inhabited Term := ⟨Term.const 0⟩ partial def hasToString : Term -> String | const n => "CONST(" ++ toString n ++ ")" | app ts => "APP" -instance : HasToString Term := ⟨hasToString⟩ +instance : ToString Term := ⟨hasToString⟩ end Term open Term diff --git a/tests/compiler/reusebug.lean b/tests/compiler/reusebug.lean index 66419a8254..a3a245f0b0 100644 --- a/tests/compiler/reusebug.lean +++ b/tests/compiler/reusebug.lean @@ -13,7 +13,7 @@ protected def Expr.toString : Expr → String | Add f g => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")" | Mul f g => "(" ++ Expr.toString f ++ " * " ++ Expr.toString g ++ ")" -instance : HasToString Expr := +instance : ToString Expr := ⟨Expr.toString⟩ partial def addAux : Expr → Expr → Expr diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean index 90fdaf18e5..bf15d75801 100644 --- a/tests/compiler/t2.lean +++ b/tests/compiler/t2.lean @@ -74,7 +74,7 @@ protected def Expr.toString : Expr → String | Pow f g => "(" ++ Expr.toString f ++ " ^ " ++ Expr.toString g ++ ")" | Ln f => "ln(" ++ Expr.toString f ++ ")" -instance : HasToString Expr := +instance : ToString Expr := ⟨Expr.toString⟩ def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean index 5aa9211fac..e6b3614301 100644 --- a/tests/compiler/t4.lean +++ b/tests/compiler/t4.lean @@ -18,7 +18,7 @@ protected def Expr.toString : Expr → String | Pow f g => "(" ++ Expr.toString f ++ " ^ " ++ Expr.toString g ++ ")" | Ln f => "ln(" ++ Expr.toString f ++ ")" -instance : HasToString Expr := +instance : ToString Expr := ⟨Expr.toString⟩ partial def pown : Int → Int → Int diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean index a5fcfb643b..977599cdda 100644 --- a/tests/compiler/termparsertest1.lean +++ b/tests/compiler/termparsertest1.lean @@ -68,7 +68,7 @@ test [ "(x : a)", "a -> b", "{x : a} -> b", -"{a : Type} -> [HasToString a] -> (x : a) -> b", +"{a : Type} -> [ToString a] -> (x : a) -> b", "f ({x : a} -> b)", "f (x : a) -> b", "f ((x : a) -> b)", diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out index 8dbea4881d..7aa09a2ac7 100644 --- a/tests/compiler/termparsertest1.lean.expected.out +++ b/tests/compiler/termparsertest1.lean.expected.out @@ -113,12 +113,12 @@ a -> b (Term.arrow `a "->" `b) {x : a} -> b (Term.depArrow (Term.implicitBinder "{" [`x] [":" `a] "}") "->" `b) -{a : Type} -> [HasToString a] -> (x : a) -> b +{a : Type} -> [ToString a] -> (x : a) -> b (Term.depArrow (Term.implicitBinder "{" [`a] [":" (Term.type "Type" [])] "}") "->" (Term.depArrow - (Term.instBinder "[" [] (Term.app `HasToString [`a]) "]") + (Term.instBinder "[" [] (Term.app `ToString [`a]) "]") "->" (Term.depArrow (Term.explicitBinder "(" [`x] [":" `a] [] ")") "->" `b))) f ({x : a} -> b) diff --git a/tests/elabissues/equation_compiler_slow_with_many_constructors2.lean b/tests/elabissues/equation_compiler_slow_with_many_constructors2.lean index 1eb191aa35..1960d06396 100644 --- a/tests/elabissues/equation_compiler_slow_with_many_constructors2.lean +++ b/tests/elabissues/equation_compiler_slow_with_many_constructors2.lean @@ -16,7 +16,7 @@ def hasToString : Op → String | add => "add" | mul => "mul" -instance : HasToString Op := ⟨hasToString⟩ +instance : ToString Op := ⟨hasToString⟩ def beq : Op → Op → Bool | add, add => true diff --git a/tests/elabissues/vars.lean b/tests/elabissues/vars.lean index 387861e8dd..dc9e8375be 100644 --- a/tests/elabissues/vars.lean +++ b/tests/elabissues/vars.lean @@ -1,8 +1,8 @@ -def f1 {α} [HasToString α] (a : α) : String := -- works +def f1 {α} [ToString α] (a : α) : String := -- works ">> " ++ toString a --- Moving `{α} [HasToString α]` to a `variables` break the example -variables {α} [HasToString α] +-- Moving `{α} [ToString α]` to a `variables` break the example +variables {α} [ToString α] def f2 (a : α) : String := ">> " ++ toString a diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index d98a5a4acf..878e6e15ce 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -65,7 +65,7 @@ def typeAs.{u} (α : Type u) (a : α) := () #eval checkM `(typeAs ({α : Type} → (a : α) → α) fun a => a) section set_option pp.explicit true - #eval checkM `(fun {α : Type} [HasToString α] (a : α) => toString a) + #eval checkM `(fun {α : Type} [ToString α] (a : α) => toString a) end #eval checkM `((α : Type) → α) @@ -74,7 +74,7 @@ end #eval checkM `((α : Type) → (a : α) → α) #eval checkM `((α : Type) → (a : α) → a = a) #eval checkM `({α : Type} → α) -#eval checkM `({α : Type} → [HasToString α] → α) +#eval checkM `({α : Type} → [ToString α] → α) -- TODO: hide `ofNat` #eval checkM `(0) diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index df8e6a4976..fdce2d248b 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -26,7 +26,7 @@ typeAs (a : α) => a fun {α : Type} [inst : - HasToString α] + ToString α] (a : α) => @toString α inst a (α : Type) → α @@ -38,8 +38,7 @@ Type → Type → Type {α : Type} → α {α : Type} → [inst : - HasToString - α] → + ToString α] → α 0 1 diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index 48d19eca4c..ad77179062 100644 --- a/tests/lean/StxQuot.lean +++ b/tests/lean/StxQuot.lean @@ -3,7 +3,7 @@ import Lean namespace Lean open Lean.Elab -def run {α} [HasToString α] : Unhygienic α → String := toString ∘ Unhygienic.run +def run {α} [ToString α] : Unhygienic α → String := toString ∘ Unhygienic.run #eval run `(Nat.one) #eval run `($Syntax.missing) diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean index 6d4144f2be..f2d8894db3 100644 --- a/tests/lean/run/catchThe.lean +++ b/tests/lean/run/catchThe.lean @@ -7,7 +7,7 @@ universes u v w abbrev M := ExceptT String $ MetaM -def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α) : MetaM Unit := do +def testM {α} [HasBeq α] [ToString α] (x : M α) (expected : α) : MetaM Unit := do let r ← x; match r with | Except.ok a => unless a == expected do throwError msg!"unexpected result {a}" diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean index 223d68af88..9a2801b095 100644 --- a/tests/lean/run/deriv.lean +++ b/tests/lean/run/deriv.lean @@ -69,14 +69,14 @@ partial def count : Expr → Nat | Ln f => count f partial def Expr.toString : Expr → String -| Val n => HasToString.toString n +| Val n => ToString.toString n | Var x => x | Add f g => "(" ++ toString f ++ " + " ++ toString g ++ ")" | Mul f g => "(" ++ toString f ++ " * " ++ toString g ++ ")" | Pow f g => "(" ++ toString f ++ " ^ " ++ toString g ++ ")" | Ln f => "ln(" ++ toString f ++ ")" -instance : HasToString Expr := +instance : ToString Expr := ⟨Expr.toString⟩ unsafe def nest (f : Expr → IO Expr) : Nat → Expr → IO Expr diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean index 4a7b89eb94..5fb625986f 100644 --- a/tests/lean/run/doNotation1.lean +++ b/tests/lean/run/doNotation1.lean @@ -23,7 +23,7 @@ let x := g2 b IO.println b pure (s+a) -def myPrint {α} [HasToString α] (a : α) : IO Unit := +def myPrint {α} [ToString α] (a : α) : IO Unit := IO.println s!">> {a}" def h₂ (x : Nat) : StateT Nat IO Nat := do diff --git a/tests/lean/run/doNotation4.lean b/tests/lean/run/doNotation4.lean index 4989b31ae7..73ee1c19d6 100644 --- a/tests/lean/run/doNotation4.lean +++ b/tests/lean/run/doNotation4.lean @@ -2,7 +2,7 @@ abbrev M := StateRefT Nat IO -def testM {α} [HasToString α] [HasBeq α] (init : Nat) (expected : α) (x : M α): IO Unit := do +def testM {α} [ToString α] [HasBeq α] (init : Nat) (expected : α) (x : M α): IO Unit := do let v ← x.run' init IO.println ("result " ++ toString v) unless v == expected do diff --git a/tests/lean/run/doNotation6.lean b/tests/lean/run/doNotation6.lean index ec750ba0c4..79b21b0cc6 100644 --- a/tests/lean/run/doNotation6.lean +++ b/tests/lean/run/doNotation6.lean @@ -2,7 +2,7 @@ abbrev M := StateRefT Nat IO -def testM {α} [HasToString α] [HasBeq α] (init : Nat) (expected : α) (x : M α): IO Unit := do +def testM {α} [ToString α] [HasBeq α] (init : Nat) (expected : α) (x : M α): IO Unit := do let v ← x.run' init IO.println ("result " ++ toString v) unless v == expected do diff --git a/tests/lean/run/forBodyResultTypeIssue.lean b/tests/lean/run/forBodyResultTypeIssue.lean index 9a9061d0e0..1fdb37e9fa 100644 --- a/tests/lean/run/forBodyResultTypeIssue.lean +++ b/tests/lean/run/forBodyResultTypeIssue.lean @@ -23,11 +23,11 @@ abbrev N := ExceptT (ULift.{u} String) Id def idM {α : Type u} (a : α) : N α := pure a -def checkEq {α : Type u} [HasBeq α] [HasToString α] (a b : α) : N PUnit := do +def checkEq {α : Type u} [HasBeq α] [ToString α] (a b : α) : N PUnit := do unless a == b do throw (ULift.up s!"{a} is not equal to {b}") -def g {α : Type u} [HasBeq α] [HasToString α] (xs : List α) (a : α) : N PUnit := do +def g {α : Type u} [HasBeq α] [ToString α] (xs : List α) (a : α) : N PUnit := do for x in xs do let a ← idM a checkEq x a diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index c651578848..2c6ddbc212 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -37,7 +37,7 @@ pure "hello" #eval runM "universe u universe v - export HasToString (toString) + export ToString (toString) section namespace foo.bla end bla end foo variable (p q : Prop) variable (_ b : _) @@ -70,12 +70,12 @@ structure S1 := structure S2 extends S1 := (z : Nat := 0) -def fD {α} [HasToString α] (a b : α) : String := +def fD {α} [ToString α] (a b : α) : String := toString a ++ toString b structure S3 := (w : Nat := 0) -(f : forall {α : Type} [HasToString α], α → α → String := @fD) +(f : forall {α : Type} [ToString α], α → α → String := @fD) structure S4 extends S2, S3 := (s : Nat := 0) @@ -194,8 +194,8 @@ f a #eval runM "#check let z := 2; x + y where x := z + 1; where y := x + x" #eval runM "variables {α β} axiom x (n : Nat) : α → α #check x 1 0" -#eval runM "#check HasToString.toString 0" -#eval runM "@[instance] axiom newInst : HasToString Nat #check newInst #check HasToString.toString 0" +#eval runM "#check ToString.toString 0" +#eval runM "@[instance] axiom newInst : ToString Nat #check newInst #check ToString.toString 0" #eval runM "variables {β σ} universes w1 w2 /-- Testing axiom -/ unsafe axiom Nat.aux (γ : Type w1) (v : Nat) : β → (α : Type _) → v = zero /- Nat.zero -/ → Array α #check @Nat.aux" #eval runM "def x : Nat := Nat.zero #check x" #eval runM "def x := Nat.zero #check x" diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index b84f00643d..34730ee0c3 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -226,7 +226,7 @@ def mkStateM (σ : Expr) : MetaM Expr := mkAppC `StateM #[σ] def mkMonad (m : Expr) : MetaM Expr := mkAppC `Monad #[m] def mkMonadState (σ m : Expr) : MetaM Expr := mkAppC `MonadState #[σ, m] def mkHasAdd (a : Expr) : MetaM Expr := mkAppC `HasAdd #[a] -def mkHasToString (a : Expr) : MetaM Expr := mkAppC `HasToString #[a] +def mkToString (a : Expr) : MetaM Expr := mkAppC `ToString #[a] def tst14 : MetaM Unit := do print "----- tst14 -----"; @@ -252,7 +252,7 @@ do print "----- tst15 -----"; def tst16 : MetaM Unit := do print "----- tst16 -----"; let prod ← mkProd nat nat; - let inst ← mkHasToString prod; + let inst ← mkToString prod; print inst; let r ← synthInstance inst; print r; @@ -264,7 +264,7 @@ def tst17 : MetaM Unit := do print "----- tst17 -----"; let prod ← mkProd nat nat; let prod ← mkProd boolE prod; - let inst ← mkHasToString prod; + let inst ← mkToString prod; print inst; let r ← synthInstance inst; print r; @@ -339,7 +339,7 @@ do print "----- tst22 -----"; print t; let t ← mkAppC `HasAdd.add #[y, x]; print t; - let t ← mkAppC `HasToString.toString #[x]; + let t ← mkAppC `ToString.toString #[x]; print t; pure () diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean index 101d5fce4a..4645754a07 100644 --- a/tests/lean/run/synth1.lean +++ b/tests/lean/run/synth1.lean @@ -24,7 +24,7 @@ instance coerceNatToBool : HasCoerce Nat Bool := instance coerceNatToInt : HasCoerce Nat Int := ⟨fun x => Int.ofNat x⟩ -def print {α} [HasToString α] (a : α) : MetaM Unit := +def print {α} [ToString α] (a : α) : MetaM Unit := trace! `Meta.synthInstance (toString a) diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean index 02c7f747c4..696d0feacd 100644 --- a/tests/lean/run/termparsertest1.lean +++ b/tests/lean/run/termparsertest1.lean @@ -70,7 +70,7 @@ test [ "(x : a)", "a -> b", "{x : a} -> b", -"{a : Type} -> [HasToString a] -> (x : a) -> b", +"{a : Type} -> [ToString a] -> (x : a) -> b", "f ({x : a} -> b)", "f (x : a) -> b", "f ((x : a) -> b)", diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean index 4ce97e7b24..23bf5607a2 100644 --- a/tests/lean/run/toExpr.lean +++ b/tests/lean/run/toExpr.lean @@ -2,7 +2,7 @@ import Lean open Lean -unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do +unsafe def test {α : Type} [ToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do let env ← getEnv; let auxName := `_toExpr._test; let decl := Declaration.defnDecl { diff --git a/tests/lean/run/typeclass_easy.lean b/tests/lean/run/typeclass_easy.lean index 5758d404e4..e62a98721b 100644 --- a/tests/lean/run/typeclass_easy.lean +++ b/tests/lean/run/typeclass_easy.lean @@ -1,6 +1,6 @@ -#synth HasToString (Nat × (Nat × Bool)) +#synth ToString (Nat × (Nat × Bool)) #synth HasAdd Nat diff --git a/tests/playground/eval2.lean b/tests/playground/eval2.lean index 9a3b1faa0f..fd51496fb7 100644 --- a/tests/playground/eval2.lean +++ b/tests/playground/eval2.lean @@ -12,7 +12,7 @@ unsafe def evalNatFn (fName : Name) (n : Nat) : IO Unit := do f ← evalConst (Nat → Nat) fName, IO.println (f n) -unsafe def evalVal (α : Type) [Inhabited α] [HasToString α] (n : Name) : IO Unit := +unsafe def evalVal (α : Type) [Inhabited α] [ToString α] (n : Name) : IO Unit := do v ← evalConst α n, IO.println v diff --git a/tests/playground/lazylist.lean b/tests/playground/lazylist.lean index 428e658391..0166072bae 100644 --- a/tests/playground/lazylist.lean +++ b/tests/playground/lazylist.lean @@ -123,16 +123,16 @@ partial def inits : LazyList α → LazyList (LazyList α) private def addOpenBracket (s : String) : String := if s.isEmpty then "[" else s -partial def approxToStringAux [HasToString α] : Nat → LazyList α → String → String +partial def approxToStringAux [ToString α] : Nat → LazyList α → String → String | _ nil r := (if r.isEmpty then "[" else r) ++ "]" | 0 _ r := (if r.isEmpty then "[" else r) ++ ", ..]" | (n+1) (cons a as) r := approxToStringAux n as ((if r.isEmpty then "[" else r ++ ", ") ++ toString a) | n (delayed as) r := approxToStringAux n as.get r -def approxToString [HasToString α] (as : LazyList α) (n : Nat := 10) : String := +def approxToString [ToString α] (as : LazyList α) (n : Nat := 10) : String := as.approxToStringAux n "" -instance [HasToString α] : HasToString (LazyList α) := +instance [ToString α] : ToString (LazyList α) := ⟨approxToString⟩ end LazyList diff --git a/tests/playground/parser/syntax.lean b/tests/playground/parser/syntax.lean index 0df325e6e6..6804034cd1 100644 --- a/tests/playground/parser/syntax.lean +++ b/tests/playground/parser/syntax.lean @@ -253,7 +253,7 @@ protected partial def formatStx : Syntax → Format | missing := "" instance : HasFormat Syntax := ⟨Syntax.formatStx⟩ -instance : HasToString Syntax := ⟨toString ∘ format⟩ +instance : ToString Syntax := ⟨toString ∘ format⟩ end Syntax end Parser diff --git a/tests/playground/pldi/intro.lean b/tests/playground/pldi/intro.lean index f9249130ae..6bf74c380f 100644 --- a/tests/playground/pldi/intro.lean +++ b/tests/playground/pldi/intro.lean @@ -36,11 +36,11 @@ inductive Tree (α : Type) namespace Tree -private def toStr {α} [HasToString α] : Tree α → String +private def toStr {α} [ToString α] : Tree α → String | leaf a => toString a | node left right => "(node " ++ toStr left ++ " " ++ toStr right ++ ")" -instance {α} [HasToString α] : HasToString (Tree α) := ⟨toStr⟩ +instance {α} [ToString α] : ToString (Tree α) := ⟨toStr⟩ end Tree @@ -62,7 +62,7 @@ structure Person := (name : String) (age : Nat := 0) -instance : HasToString Person := +instance : ToString Person := ⟨fun p => p.name ++ ":" ++ toString p.age⟩ #eval toString { name := "John", age := 30 : Person } diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean index 5e189dfaf2..e430fd966a 100644 --- a/tests/playground/termparsertest1.lean +++ b/tests/playground/termparsertest1.lean @@ -69,7 +69,7 @@ test [ "(x : a)", "a -> b", "{x : a} -> b", -"{a : Type} -> [HasToString a] -> (x : a) -> b", +"{a : Type} -> [ToString a] -> (x : a) -> b", "f ({x : a} -> b)", "f (x : a) -> b", "f ((x : a) -> b)",