From 5fed7744614fd47872b27f488e8e355a216c29d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 16:14:36 -0700 Subject: [PATCH] chore: `HasRepr` ==> `Repr` --- src/Init/Control/EState.lean | 2 +- src/Init/Control/Except.lean | 4 +- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Int/Basic.lean | 2 +- src/Init/Data/Random.lean | 2 +- src/Init/Data/Repr.lean | 58 ++++++++++++------------ src/Init/System/IO.lean | 2 +- src/Lean/Data/Format.lean | 2 +- src/Lean/Data/Json/Basic.lean | 2 +- src/Lean/Expr.lean | 4 +- src/Std/Data/RBMap.lean | 2 +- src/Std/Data/RBTree.lean | 2 +- tests/bench/rbmap3.lean | 2 +- tests/lean/repr_issue.lean | 2 +- tests/lean/run/125.lean | 2 +- tests/lean/run/IO_test.lean | 4 +- tests/lean/run/backtrackable_estate.lean | 2 +- 17 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 5109250d33..e948df4223 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -22,7 +22,7 @@ instance [ToString ε] [ToString α] : ToString (Result ε σ α) := { | Result.error e _ => "error: " ++ toString e } -instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := { +instance [Repr ε] [Repr α] : Repr (Result ε σ α) := { repr := fun | Result.error e _ => "(error " ++ repr e ++ ")" | Result.ok a _ => "(ok " ++ repr a ++ ")" diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 340d2537cf..bea8f2379b 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -30,12 +30,12 @@ protected def Except.toString [ToString ε] [ToString α] : Except ε α → Str | Except.error e => "(error " ++ toString e ++ ")" | Except.ok a => "(ok " ++ toString a ++ ")" -protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String +protected def Except.repr [Repr ε] [Repr α] : Except ε α → String | Except.error e => "(error " ++ repr e ++ ")" | Except.ok a => "(ok " ++ repr a ++ ")" instance [ToString ε] [ToString α] : ToString (Except ε α) := ⟨Except.toString⟩ -instance [HasRepr ε] [HasRepr α] : HasRepr (Except ε α) := ⟨Except.repr⟩ +instance [Repr ε] [Repr α] : Repr (Except ε α) := ⟨Except.repr⟩ end namespace Except diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index d1b59cc00d..7481e2468d 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -437,7 +437,7 @@ a.foldlStep (fun r a => Array.push r a) empty 2 def toList (a : Array α) : List α := a.foldr List.cons [] -instance [HasRepr α] : HasRepr (Array α) := +instance [Repr α] : Repr (Array α) := ⟨fun a => "#" ++ repr a.toList⟩ instance [ToString α] : ToString (Array α) := diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index fb379da266..a8e082eb0e 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -122,7 +122,7 @@ protected def repr : Int → String | ofNat m => Nat.repr m | negSucc m => "-" ++ Nat.repr (succ m) -instance : HasRepr Int := ⟨Int.repr⟩ +instance : Repr Int := ⟨Int.repr⟩ instance : ToString Int := ⟨Int.repr⟩ instance : HasOfNat Int := ⟨Int.ofNat⟩ diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index 702c2b6f90..c136425cd8 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -37,7 +37,7 @@ instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩ def stdRange := (1, 2147483562) -instance : HasRepr StdGen := { +instance : Repr StdGen := { repr := fun ⟨s1, s2⟩ => "⟨" ++ toString s1 ++ ", " ++ toString s2 ++ "⟩" } diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 5a0bbd3f22..c7f4d7665f 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -12,61 +12,61 @@ open Sum Subtype Nat universes u v -class HasRepr (α : Type u) := +class Repr (α : Type u) := (repr : α → String) -export HasRepr (repr) +export Repr (repr) -- This instance is needed because `id` is not reducible -instance {α : Type u} [HasRepr α] : HasRepr (id α) := - inferInstanceAs (HasRepr α) +instance {α : Type u} [Repr α] : Repr (id α) := + inferInstanceAs (Repr α) -instance : HasRepr Bool := +instance : Repr Bool := ⟨fun b => cond b "true" "false"⟩ -instance {α} [HasRepr α] : HasRepr (Id α) := - inferInstanceAs (HasRepr α) +instance {α} [Repr α] : Repr (Id α) := + inferInstanceAs (Repr α) -instance {p : Prop} : HasRepr (Decidable p) := { +instance {p : Prop} : Repr (Decidable p) := { repr := fun h => match h with | Decidable.isTrue _ => "true" | Decidable.isFalse _ => "false" } -protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String +protected def List.reprAux {α : Type u} [Repr α] : Bool → List α → String | b, [] => "" | true, x::xs => repr x ++ List.reprAux false xs | false, x::xs => ", " ++ repr x ++ List.reprAux false xs -protected def List.repr {α : Type u} [HasRepr α] : List α → String +protected def List.repr {α : Type u} [Repr α] : List α → String | [] => "[]" | x::xs => "[" ++ List.reprAux true (x::xs) ++ "]" -instance {α : Type u} [HasRepr α] : HasRepr (List α) := +instance {α : Type u} [Repr α] : Repr (List α) := ⟨List.repr⟩ -instance : HasRepr PUnit.{u+1} := +instance : Repr PUnit.{u+1} := ⟨fun u => "PUnit.unit"⟩ -instance {α : Type u} [HasRepr α] : HasRepr (ULift.{v} α) := +instance {α : Type u} [Repr α] : Repr (ULift.{v} α) := ⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩ -instance : HasRepr Unit := +instance : Repr Unit := ⟨fun u => "()"⟩ -instance {α : Type u} [HasRepr α] : HasRepr (Option α) := +instance {α : Type u} [Repr α] : Repr (Option α) := ⟨fun | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (Sum α β) := +instance {α : Type u} {β : Type v} [Repr α] [Repr β] : Repr (Sum α β) := ⟨fun | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) := +instance {α : Type u} {β : Type v} [Repr α] [Repr β] : Repr (α × β) := ⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩ -instance {α : Type u} {β : α → Type v} [HasRepr α] [s : ∀ x, HasRepr (β x)] : HasRepr (Sigma β) := +instance {α : Type u} {β : α → Type v} [Repr α] [s : ∀ x, Repr (β x)] : Repr (Sigma β) := ⟨fun ⟨a, b⟩ => "⟨" ++ repr a ++ ", " ++ repr b ++ "⟩"⟩ -instance {α : Type u} {p : α → Prop} [HasRepr α] : HasRepr (Subtype p) := +instance {α : Type u} {p : α → Prop} [Repr α] : Repr (Subtype p) := ⟨fun s => repr (val s)⟩ namespace Nat @@ -132,7 +132,7 @@ def toSuperscriptString (n : Nat) : String := end Nat -instance : HasRepr Nat := +instance : Repr Nat := ⟨Nat.repr⟩ def hexDigitRepr (n : Nat) : String := @@ -152,29 +152,29 @@ def Char.quoteCore (c : Char) : String := else if c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c else String.singleton c -instance : HasRepr Char := +instance : Repr Char := ⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩ def String.quote (s : String) : String := if s.isEmpty = true then "\"\"" else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\"" -instance : HasRepr String := +instance : Repr String := ⟨String.quote⟩ -instance : HasRepr Substring := +instance : Repr Substring := ⟨fun s => String.quote s.toString ++ ".toSubstring"⟩ -instance : HasRepr String.Iterator := +instance : Repr String.Iterator := ⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩ -instance (n : Nat) : HasRepr (Fin n) := +instance (n : Nat) : Repr (Fin n) := ⟨fun f => repr (Fin.val f)⟩ -instance : HasRepr UInt16 := ⟨fun n => repr n.toNat⟩ -instance : HasRepr UInt32 := ⟨fun n => repr n.toNat⟩ -instance : HasRepr UInt64 := ⟨fun n => repr n.toNat⟩ -instance : HasRepr USize := ⟨fun n => repr n.toNat⟩ +instance : Repr UInt16 := ⟨fun n => repr n.toNat⟩ +instance : Repr UInt32 := ⟨fun n => repr n.toNat⟩ +instance : Repr UInt64 := ⟨fun n => repr n.toNat⟩ +instance : Repr USize := ⟨fun n => repr n.toNat⟩ protected def Char.repr (c : Char) : String := repr c diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 749088a9e2..900b67a83a 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -468,7 +468,7 @@ class HasEval (α : Type u) := -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`) (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit) -instance {α : Type u} [HasRepr α] : HasEval α := +instance {α : Type u} [Repr α] : HasEval α := ⟨fun a _ => IO.println (repr (a ()))⟩ instance : HasEval Unit := diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean index bc372b7d84..d43aa78557 100644 --- a/src/Lean/Data/Format.lean +++ b/src/Lean/Data/Format.lean @@ -273,7 +273,7 @@ protected def Format.repr : Format → Format instance : ToString Format := ⟨Format.pretty⟩ -instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩ +instance : Repr Format := ⟨Format.pretty ∘ Format.repr⟩ def formatDataValue : DataValue → Format | DataValue.ofString v => format (repr v) diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index a6cc4a6062..db4ffc6304 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -73,7 +73,7 @@ protected def shiftr : JsonNumber → Nat → JsonNumber instance : ToString JsonNumber := ⟨JsonNumber.toString⟩ -instance : HasRepr JsonNumber := +instance : Repr JsonNumber := ⟨fun ⟨m, e⟩ => "⟨" ++ m.repr ++ "," ++ e.repr ++ "⟩"⟩ end JsonNumber diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index abaf1dfd9c..c0226e7a9f 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -682,7 +682,7 @@ def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr := instance : ToString Expr := ⟨Expr.dbgToString⟩ -- TODO: should not use dbgToString, but constructors. -instance : HasRepr Expr := ⟨Expr.dbgToString⟩ +instance : Repr Expr := ⟨Expr.dbgToString⟩ def isAtomic : Expr → Bool | Expr.const _ _ _ => true @@ -738,7 +738,7 @@ instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩ instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩ instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩ instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩ -instance : HasRepr ExprStructEq := ⟨fun e => repr e.val⟩ +instance : Repr ExprStructEq := ⟨fun e => repr e.val⟩ end ExprStructEq diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean index 4fbf488360..73315a2c43 100644 --- a/src/Std/Data/RBMap.lean +++ b/src/Std/Data/RBMap.lean @@ -257,7 +257,7 @@ def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat := | some ⟨k, v⟩ => some (k, v) | none => none -instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := +instance [Repr α] [Repr β] : Repr (RBMap α β lt) := ⟨fun t => "rbmapOf " ++ repr t.toList⟩ @[inline] def insert : RBMap α β lt → α → β → RBMap α β lt diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean index 0797b49744..a7353085a3 100644 --- a/src/Std/Data/RBTree.lean +++ b/src/Std/Data/RBTree.lean @@ -53,7 +53,7 @@ variables {α : Type u} {β : Type v} {lt : α → α → Bool} | some ⟨a, _⟩ => some a | none => none -instance [HasRepr α] : HasRepr (RBTree α lt) := +instance [Repr α] : Repr (RBTree α lt) := ⟨fun t => "rbtreeOf " ++ repr t.toList⟩ @[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt := diff --git a/tests/bench/rbmap3.lean b/tests/bench/rbmap3.lean index 2965f983f5..f152db97e3 100644 --- a/tests/bench/rbmap3.lean +++ b/tests/bench/rbmap3.lean @@ -206,7 +206,7 @@ t.val.depth f | some ⟨k, v⟩ => some (k, v) | none => none -instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) := +instance [Repr α] [Repr β] : Repr (Rbmap α β lt) := ⟨fun t => "rbmapOf " ++ repr t.toList⟩ variables [DecidableRel lt] diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean index 10f8f1808f..842373f442 100644 --- a/tests/lean/repr_issue.lean +++ b/tests/lean/repr_issue.lean @@ -12,6 +12,6 @@ def ex₂ : ExceptT String (StateT (Array Nat) Id) Nat := foo -- The following examples were producing an element of Type `id (Except String Nat)`. --- Type class resolution was failing to produce an instance for `HasRepr (id (Except String Nat))` because `id` is not transparent. +-- Type class resolution was failing to produce an instance for `Repr (id (Except String Nat))` because `id` is not transparent. #eval ex₁.run' (mkArray 10 1000) $.run #eval ex₂.run' (mkArray 10 1000) $.run diff --git a/tests/lean/run/125.lean b/tests/lean/run/125.lean index d54dc4d5d4..c24fb615b8 100644 --- a/tests/lean/run/125.lean +++ b/tests/lean/run/125.lean @@ -17,7 +17,7 @@ match foo with | mk1 b => s!"OH {b}" | mk2 b => s!"DR {b}" -instance : HasRepr Foo := ⟨fooRepr⟩ +instance : Repr Foo := ⟨fooRepr⟩ #eval elems Foo diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean index 17f038babb..a3e67ccd06 100644 --- a/tests/lean/run/IO_test.lean +++ b/tests/lean/run/IO_test.lean @@ -6,9 +6,9 @@ import Init.Data.ToString open IO.FS -instance : HasRepr UInt8 := ⟨ toString ⟩ +instance : Repr UInt8 := ⟨ toString ⟩ -def check_eq {α} [HasBeq α] [HasRepr α] (tag : String) (expected actual : α) : IO Unit := +def check_eq {α} [HasBeq α] [Repr α] (tag : String) (expected actual : α) : IO Unit := «unless» (expected == actual) $ throw $ IO.userError $ s!"assertion failure \"{tag}\":\n expected: {repr expected}\n actual: {repr actual}" diff --git a/tests/lean/run/backtrackable_estate.lean b/tests/lean/run/backtrackable_estate.lean index 4ab0fe01fd..653dbc3e06 100644 --- a/tests/lean/run/backtrackable_estate.lean +++ b/tests/lean/run/backtrackable_estate.lean @@ -5,7 +5,7 @@ structure MyState := (bs : Nat := 0) -- backtrackable state (ps : Nat := 0) -- non backtrackable state -instance : HasRepr MyState := +instance : Repr MyState := ⟨fun s => repr (s.bs, s.ps)⟩ instance : EStateM.Backtrackable Nat MyState :=