feat: add helper class ReprAtom

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

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  := ⟨⟩

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"

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),