diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 6595667409..d8762c87a8 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -69,7 +69,13 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b @[extern "lean_float_to_string"] constant Float.toString : Float → String -instance : ToString Float := ⟨Float.toString⟩ +instance : ToString Float where + toString := Float.toString + +instance : Repr Float where + reprPrec n _ := Float.toString n + +instance : ReprAtom Float := ⟨⟩ abbrev Nat.toFloat (n : Nat) : Float := Float.ofNat n diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index d814697d19..b1925e0a6a 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -27,6 +27,10 @@ abbrev reprStr [Repr α] (a : α) : String := abbrev reprArg [Repr α] (a : α) : Format := reprPrec a maxPrec! +/- Auxiliary class for marking types that should be considered atomic by `Repr` methods. + We use it at `Repr (List α)` to decide whether `bracketFill` should be used or not. -/ +class ReprAtom (α : Type u) + -- This instance is needed because `id` is not reducible instance [Repr α] : Repr (id α) := inferInstanceAs (Repr α) @@ -50,11 +54,6 @@ instance : Repr (Decidable p) where | Decidable.isTrue _, prec => Repr.addAppParen "isTrue _" prec | Decidable.isFalse _, prec => Repr.addAppParen "isFalse _" prec -instance [Repr α] : Repr (List α) where - reprPrec - | [], _ => "[]" - | as, _ => Format.bracketFill "[" (@Format.joinSep _ ⟨repr⟩ as ("," ++ Format.line)) "]" - instance : Repr PUnit.{u+1} where reprPrec _ _ := "PUnit.unit" @@ -88,7 +87,7 @@ instance [Repr α] [ReprTuple β] : ReprTuple (α × β) where instance [Repr α] [ReprTuple β] : Repr (α × β) where reprPrec | (a, b), _ => - Format.bracketFill "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")" + Format.bracket "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")" instance {β : α → Type v} [Repr α] [s : (x : α) → Repr (β x)] : Repr (Sigma β) where reprPrec | ⟨a, b⟩, _ => Format.bracket "⟨" (repr a ++ ", " ++ repr b) "⟩" @@ -192,6 +191,9 @@ def Char.quote (c : Char) : String := instance : Repr Char where reprPrec c _ := c.quote +protected def Char.repr (c : Char) : String := + c.quote + def String.quote (s : String) : String := if s.isEmpty = true then "\"\"" else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\"" @@ -224,5 +226,23 @@ instance : Repr UInt64 where instance : Repr USize where reprPrec n _ := repr n.toNat -protected def Char.repr (c : Char) : String := - c.quote +instance [Repr α] : Repr (List α) where + reprPrec + | [], _ => "[]" + | as, _ => Format.bracket "[" (@Format.joinSep _ ⟨repr⟩ as ("," ++ Format.line)) "]" + +instance [Repr α] [ReprAtom α] : Repr (List α) where + reprPrec + | [], _ => "[]" + | as, _ => Format.bracketFill "[" (@Format.joinSep _ ⟨repr⟩ as ("," ++ Format.line)) "]" + +instance : ReprAtom Bool := ⟨⟩ +instance : ReprAtom Nat := ⟨⟩ +instance : ReprAtom Int := ⟨⟩ +instance : ReprAtom Char := ⟨⟩ +instance : ReprAtom String := ⟨⟩ +instance : ReprAtom UInt8 := ⟨⟩ +instance : ReprAtom UInt16 := ⟨⟩ +instance : ReprAtom UInt32 := ⟨⟩ +instance : ReprAtom UInt64 := ⟨⟩ +instance : ReprAtom USize := ⟨⟩ diff --git a/tests/lean/repr.lean b/tests/lean/repr.lean index dc8432be71..bce39c0531 100644 --- a/tests/lean/repr.lean +++ b/tests/lean/repr.lean @@ -7,3 +7,7 @@ #eval repr ("hello", 1, true, false, 'a', "testing tuples", "another string", "another string", "testing bigger tuples that should not fit in a single line", 20) #eval List.iota 50 |>.toArray #eval List.iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even" + +instance : ReprAtom (Except String (Option Nat)) := ⟨⟩ + +#eval List.iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even" diff --git a/tests/lean/repr.lean.expected.out b/tests/lean/repr.lean.expected.out index 2d38dc98a0..b4e2f6d54b 100644 --- a/tests/lean/repr.lean.expected.out +++ b/tests/lean/repr.lean.expected.out @@ -1,13 +1,62 @@ (1, 2, 3) (some 1, some (some true)) -[some (some 10), some (some 9), some (some 8), some (some 7), some (some 6), some (some 5), some (some 4), - some (some 3), some (some 2), some (some 1)] -[(15, some 15), (14, some 14), (13, some 13), (12, some 12), (11, some 11), (10, some 10), (9, some 9), (8, some 8), - (7, some 7), (6, some 6), (5, some 5), (4, some 4), (3, some 3), (2, some 2), (1, some 1)] -("hello", 1, true, false, 'a', "testing tuples", "another string", "another string", - "testing bigger tuples that should not fit in a single line", 20) +[some (some 10), + some (some 9), + some (some 8), + some (some 7), + some (some 6), + some (some 5), + some (some 4), + some (some 3), + some (some 2), + some (some 1)] +[(15, some 15), + (14, some 14), + (13, some 13), + (12, some 12), + (11, some 11), + (10, some 10), + (9, some 9), + (8, some 8), + (7, some 7), + (6, some 6), + (5, some 5), + (4, some 4), + (3, some 3), + (2, some 2), + (1, some 1)] +("hello", + 1, + true, + false, + 'a', + "testing tuples", + "another string", + "another string", + "testing bigger tuples that should not fit in a single line", + 20) #[50, 49, 48, 47, 46, 45, 44, 43, 42, 41, 40, 39, 38, 37, 36, 35, 34, 33, 32, 31, 30, 29, 28, 27, 26, 25, 24, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1] +[Except.ok (some 20), + Except.error "no even", + Except.ok (some 18), + Except.error "no even", + Except.ok (some 16), + Except.error "no even", + Except.ok (some 14), + Except.error "no even", + Except.ok (some 12), + Except.error "no even", + Except.ok (some 10), + Except.error "no even", + Except.ok (some 8), + Except.error "no even", + Except.ok (some 6), + Except.error "no even", + Except.ok (some 4), + Except.error "no even", + Except.ok (some 2), + Except.error "no even"] [Except.ok (some 20), Except.error "no even", Except.ok (some 18), Except.error "no even", Except.ok (some 16), Except.error "no even", Except.ok (some 14), Except.error "no even", Except.ok (some 12), Except.error "no even", Except.ok (some 10), Except.error "no even", Except.ok (some 8), Except.error "no even", Except.ok (some 6),