From 02cbe4969f473abaaa9f004afe90d8fd298d6f82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 May 2025 01:27:14 -0700 Subject: [PATCH] fix: exponential compilation times due to inlined instances (#8254) This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr` instances, which was causing exponential compilation times in `deriving` clauses for large structures. --- src/Init/Data/Array/Basic.lean | 14 +- src/Init/Data/Array/Subarray.lean | 6 +- src/Init/Data/BitVec/Basic.lean | 8 +- src/Init/Data/Float.lean | 5 +- src/Init/Data/Float32.lean | 5 +- src/Init/Data/Repr.lean | 26 ++- src/Lean/Data/Json/FromToJson.lean | 192 +++++++++++------- .../lean/run/tojson_fromjson_perf_issue.lean | 107 ++++++++++ 8 files changed, 272 insertions(+), 91 deletions(-) create mode 100644 tests/lean/run/tojson_fromjson_perf_issue.lean diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 288544f890..9e640a8f36 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -2158,13 +2158,15 @@ Examples: /-! ### Repr and ToString -/ +protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format := + let _ : Std.ToFormat α := ⟨repr⟩ + if xs.size == 0 then + "#[]" + else + Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]" + instance {α : Type u} [Repr α] : Repr (Array α) where - reprPrec xs _ := - let _ : Std.ToFormat α := ⟨repr⟩ - if xs.size == 0 then - "#[]" - else - Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]" + reprPrec xs _ := Array.repr xs instance [ToString α] : ToString (Array α) where toString xs := "#" ++ toString xs.toList diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index a1f8f46b81..04b7af62bd 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -464,8 +464,12 @@ instance : Append (Subarray α) where let a := x.toArray ++ y.toArray a.toSubarray 0 a.size +/-- `Subarray` representation. -/ +protected def Subarray.repr [Repr α] (s : Subarray α) : Std.Format := + repr s.toArray ++ ".toSubarray" + instance [Repr α] : Repr (Subarray α) where - reprPrec s _ := repr s.toArray ++ ".toSubarray" + reprPrec s _ := Subarray.repr s instance [ToString α] : ToString (Subarray α) where toString s := toString s.toArray diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 9fd2839a6a..7465f9a711 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -199,7 +199,13 @@ protected def toHex {n : Nat} (x : BitVec n) : String := let t := (List.replicate ((n+3) / 4 - s.length) '0').asString t ++ s -instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n +/-- `BitVec` representation. -/ +protected def BitVec.repr (a : BitVec n) : Std.Format := + "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n + +instance : Repr (BitVec n) where + reprPrec a _ := BitVec.repr a + instance : ToString (BitVec n) where toString a := toString (repr a) end repr_toString diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index f0331b7504..92286dcb2f 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -291,8 +291,11 @@ implementation. instance : Inhabited Float where default := UInt64.toFloat 0 +protected def Float.repr (n : Float) (prec : Nat) : Std.Format := + if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n + instance : Repr Float where - reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n + reprPrec := Float.repr instance : ReprAtom Float := ⟨⟩ diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean index 1ad084e52c..1427c2a1f8 100644 --- a/src/Init/Data/Float32.lean +++ b/src/Init/Data/Float32.lean @@ -292,8 +292,11 @@ implementation. instance : Inhabited Float32 where default := UInt64.toFloat32 0 +protected def Float32.repr (n : Float32) (prec : Nat) : Std.Format := + if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n + instance : Repr Float32 where - reprPrec n prec := if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n + reprPrec := Float32.repr instance : ReprAtom Float32 := ⟨⟩ diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index ad6e5b22b1..d461c8bf09 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -55,10 +55,12 @@ This instance allows us to use `Empty` as a type parameter without causing insta instance : Repr Empty where reprPrec := nofun +protected def Bool.repr : Bool → Nat → Format + | true, _ => "true" + | false, _ => "false" + instance : Repr Bool where - reprPrec - | true, _ => "true" - | false, _ => "false" + reprPrec := Bool.repr def Repr.addAppParen (f : Format) (prec : Nat) : Format := if prec >= max_prec then @@ -66,10 +68,12 @@ def Repr.addAppParen (f : Format) (prec : Nat) : Format := else f +protected def Decidable.repr : Decidable p → Nat → Format + | .isTrue _, prec => Repr.addAppParen "isTrue _" prec + | .isFalse _, prec => Repr.addAppParen "isFalse _" prec + instance : Repr (Decidable p) where - reprPrec - | Decidable.isTrue _, prec => Repr.addAppParen "isTrue _" prec - | Decidable.isFalse _, prec => Repr.addAppParen "isFalse _" prec + reprPrec := Decidable.repr instance : Repr PUnit.{u+1} where reprPrec _ _ := "PUnit.unit" @@ -109,8 +113,11 @@ export ReprTuple (reprTuple) instance [Repr α] : ReprTuple α where reprTuple a xs := repr a :: xs +protected def Prod.reprTuple [Repr α] [ReprTuple β] : α × β → List Format → List Format + | (a, b), xs => reprTuple b (repr a :: xs) + instance [Repr α] [ReprTuple β] : ReprTuple (α × β) where - reprTuple | (a, b), xs => reprTuple b (repr a :: xs) + reprTuple := Prod.reprTuple protected def Prod.repr [Repr α] [ReprTuple β] : α × β → Nat → Format | (a, b), _ => Format.bracket "(" (Format.joinSep (reprTuple b [repr a]).reverse ("," ++ Format.line)) ")" @@ -118,8 +125,11 @@ protected def Prod.repr [Repr α] [ReprTuple β] : α × β → Nat → Format instance [Repr α] [ReprTuple β] : Repr (α × β) where reprPrec := Prod.repr +protected def Sigma.repr {β : α → Type v} [Repr α] [(x : α) → Repr (β x)] : Sigma β → Nat → Format + | ⟨a, b⟩, _ => Format.bracket "⟨" (repr a ++ ", " ++ repr b) "⟩" + instance {β : α → Type v} [Repr α] [(x : α) → Repr (β x)] : Repr (Sigma β) where - reprPrec | ⟨a, b⟩, _ => Format.bracket "⟨" (repr a ++ ", " ++ repr b) "⟩" + reprPrec := Sigma.repr instance {p : α → Prop} [Repr α] : Repr (Subtype p) where reprPrec s prec := reprPrec s.val prec diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index a69bcd6e5c..f1224cc51b 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -47,69 +47,96 @@ instance : ToJson String := ⟨fun s => s⟩ instance : FromJson System.FilePath := ⟨fun j => System.FilePath.mk <$> Json.getStr? j⟩ instance : ToJson System.FilePath := ⟨fun p => p.toString⟩ -instance [FromJson α] : FromJson (Array α) where - fromJson? - | Json.arr a => a.mapM fromJson? - | j => throw s!"expected JSON array, got '{j}'" +protected def _root_.Array.fromJson? [FromJson α] : Json → Except String (Array α) + | Json.arr a => a.mapM fromJson? + | j => throw s!"expected JSON array, got '{j}'" -instance [ToJson α] : ToJson (Array α) := - ⟨fun a => Json.arr (a.map toJson)⟩ +instance [FromJson α] : FromJson (Array α) where + fromJson? := Array.fromJson? + +protected def _root_.Array.toJson [ToJson α] (a : Array α) : Json := + Json.arr (a.map toJson) + +instance [ToJson α] : ToJson (Array α) where + toJson := Array.toJson + +protected def _root_.List.fromJson? [FromJson α] (j : Json) : Except String (List α) := + (fromJson? j (α := Array α)).map Array.toList instance [FromJson α] : FromJson (List α) where - fromJson? j := (fromJson? j (α := Array α)).map Array.toList + fromJson? := List.fromJson? + +protected def _root_.List.toJson [ToJson α] (a : List α) : Json := + toJson a.toArray instance [ToJson α] : ToJson (List α) where - toJson xs := toJson xs.toArray + toJson := List.toJson + +protected def _root_.Option.fromJson? [FromJson α] : Json → Except String (Option α) + | Json.null => Except.ok none + | j => some <$> fromJson? j instance [FromJson α] : FromJson (Option α) where - fromJson? - | Json.null => Except.ok none - | j => some <$> fromJson? j + fromJson? := Option.fromJson? -instance [ToJson α] : ToJson (Option α) := - ⟨fun - | none => Json.null - | some a => toJson a⟩ +protected def _root_.Option.toJson [ToJson α] : Option α → Json + | none => Json.null + | some a => toJson a + +instance [ToJson α] : ToJson (Option α) where + toJson := Option.toJson + +protected def _root_.Prod.fromJson? {α : Type u} {β : Type v} [FromJson α] [FromJson β] : Json → Except String (α × β) + | Json.arr #[ja, jb] => do + let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up + let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up + return (a, b) + | j => throw s!"expected pair, got '{j}'" instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) where - fromJson? - | Json.arr #[ja, jb] => do - let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up - let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up - return (a, b) - | j => throw s!"expected pair, got '{j}'" + fromJson? := Prod.fromJson? + +protected def _root_.Prod.toJson [ToJson α] [ToJson β] : α × β → Json + | (a, b) => Json.arr #[toJson a, toJson b] instance [ToJson α] [ToJson β] : ToJson (α × β) where - toJson := fun (a, b) => Json.arr #[toJson a, toJson b] + toJson := Prod.toJson + +protected def Name.fromJson? (j : Json) : Except String Name := do + let s ← j.getStr? + if s == "[anonymous]" then + return Name.anonymous + else + let n := s.toName + if n.isAnonymous then throw s!"expected a `Name`, got '{j}'" + return n instance : FromJson Name where - fromJson? j := do - let s ← j.getStr? - if s == "[anonymous]" then - return Name.anonymous - else - let n := s.toName - if n.isAnonymous then throw s!"expected a `Name`, got '{j}'" - return n + fromJson? := Name.fromJson? instance : ToJson Name where toJson n := toString n -instance [FromJson α] : FromJson (NameMap α) where - fromJson? - | .obj obj => obj.foldM (init := {}) fun m k v => do - if k == "[anonymous]" then - return m.insert .anonymous (← fromJson? v) +protected def NameMap.fromJson? [FromJson α] : Json → Except String (NameMap α) + | .obj obj => obj.foldM (init := {}) fun m k v => do + if k == "[anonymous]" then + return m.insert .anonymous (← fromJson? v) + else + let n := k.toName + if n.isAnonymous then + throw s!"expected a `Name`, got '{k}'" else - let n := k.toName - if n.isAnonymous then - throw s!"expected a `Name`, got '{k}'" - else - return m.insert n (← fromJson? v) - | j => throw s!"expected a `NameMap`, got '{j}'" + return m.insert n (← fromJson? v) + | j => throw s!"expected a `NameMap`, got '{j}'" + +instance [FromJson α] : FromJson (NameMap α) where + fromJson? := NameMap.fromJson? + +protected def NameMap.toJson [ToJson α] (m : NameMap α) : Json := + Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf instance [ToJson α] : ToJson (NameMap α) where - toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf + toJson := NameMap.toJson /-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript cannot represent 64-bit numbers. -/ @@ -122,58 +149,77 @@ def bignumFromJson? (j : Json) : Except String Nat := do def bignumToJson (n : Nat) : Json := toString n +protected def _root_.USize.fromJson? (j : Json) : Except String USize := do + let n ← bignumFromJson? j + if n ≥ USize.size then + throw "value '{j}' is too large for `USize`" + return USize.ofNat n + instance : FromJson USize where - fromJson? j := do - let n ← bignumFromJson? j - if n ≥ USize.size then - throw "value '{j}' is too large for `USize`" - return USize.ofNat n + fromJson? := USize.fromJson? instance : ToJson USize where toJson v := bignumToJson (USize.toNat v) +protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do + let n ← bignumFromJson? j + if n ≥ UInt64.size then + throw "value '{j}' is too large for `UInt64`" + return UInt64.ofNat n + instance : FromJson UInt64 where - fromJson? j := do - let n ← bignumFromJson? j - if n ≥ UInt64.size then - throw "value '{j}' is too large for `UInt64`" - return UInt64.ofNat n + fromJson? := UInt64.fromJson? instance : ToJson UInt64 where toJson v := bignumToJson (UInt64.toNat v) +protected def _root_.Float.toJson (x : Float) : Json := + match JsonNumber.fromFloat? x with + | Sum.inl e => Json.str e + | Sum.inr n => Json.num n + instance : ToJson Float where - toJson x := - match JsonNumber.fromFloat? x with - | Sum.inl e => Json.str e - | Sum.inr n => Json.num n + toJson := Float.toJson + +protected def _root_.Float.fromJson? : Json → Except String Float + | (Json.str "Infinity") => Except.ok (1.0 / 0.0) + | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0) + | (Json.str "NaN") => Except.ok (0.0 / 0.0) + | (Json.num jn) => Except.ok jn.toFloat + | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'." instance : FromJson Float where - fromJson? := fun - | (Json.str "Infinity") => Except.ok (1.0 / 0.0) - | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0) - | (Json.str "NaN") => Except.ok (0.0 / 0.0) - | (Json.num jn) => Except.ok jn.toFloat - | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'." + fromJson? := Float.fromJson? + +protected def RBMap.toJson [ToJson α] (m : RBMap String α cmp) : Json := + Json.obj <| RBNode.map (fun _ => toJson) <| m.val instance [ToJson α] : ToJson (RBMap String α cmp) where - toJson m := Json.obj <| RBNode.map (fun _ => toJson) <| m.val + toJson := RBMap.toJson + +protected def RBMap.fromJson? [FromJson α] (j : Json) : Except String (RBMap String α cmp) := do + let o ← j.getObj? + o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅ instance {cmp} [FromJson α] : FromJson (RBMap String α cmp) where - fromJson? j := do - let o ← j.getObj? - o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅ + fromJson? := RBMap.fromJson? namespace Json -instance : FromJson Structured := ⟨fun - | arr a => return Structured.arr a - | obj o => return Structured.obj o - | j => throw s!"expected structured object, got '{j}'"⟩ +protected def Structured.fromJson? : Json → Except String Structured + | .arr a => return Structured.arr a + | .obj o => return Structured.obj o + | j => throw s!"expected structured object, got '{j}'" -instance : ToJson Structured := ⟨fun - | Structured.arr a => arr a - | Structured.obj o => obj o⟩ +instance : FromJson Structured where + fromJson? := Structured.fromJson? + +protected def Structured.toJson : Structured → Json + | .arr a => .arr a + | .obj o => .obj o + +instance : ToJson Structured where + toJson := Structured.toJson def toStructured? [ToJson α] (v : α) : Except String Structured := fromJson? (toJson v) diff --git a/tests/lean/run/tojson_fromjson_perf_issue.lean b/tests/lean/run/tojson_fromjson_perf_issue.lean new file mode 100644 index 0000000000..d7ececeea6 --- /dev/null +++ b/tests/lean/run/tojson_fromjson_perf_issue.lean @@ -0,0 +1,107 @@ +import Lean.Data.Json +open Lean + +structure Foo where + a1 : Option Nat + a2 : Option Nat + a3 : Option Nat + a4 : Option Nat + a5 : Option Nat + a6 : Option Nat + a7 : Option Nat + a8 : Option Nat + a9 : Option Nat + a10 : Option Nat + a11 : Option Nat + a12 : Option Nat + a13 : Option Nat + a14 : Option Nat + a15 : Option Nat + a16 : Option Nat + a17 : Option Nat + a18 : Option Nat + a19 : Option Nat + a20 : Option Nat + a21 : Option Nat + a22 : Option Nat + a23 : Option Nat + a24 : Option Nat + a25 : Option Nat + a26 : Option Nat + a27 : Option Nat + a28 : Option Nat + a29 : Option Nat + a30 : Option Nat + a31 : Option Nat + a32 : Option Nat + a33 : Option Nat + a34 : Option Nat + a35 : Option Nat + a36 : Option Nat + a37 : Option Nat + a38 : Option Nat + a39 : Option Nat + deriving ToJson, FromJson, Repr, BEq + +structure Boo where + a1 : String × Option Nat + a2 : String × Option Nat + a3 : String × Option Nat + a4 : String × Option Nat + a5 : String × Option Nat + a6 : String × Option Nat + a7 : String × Option Nat + a8 : String × Option Nat + a9 : String × Option Nat + a10 : Array Nat + a11 : Array Nat + a12 : Array Nat + a13 : Array Nat + a14 : Array Nat + a15 : Array Nat + a16 : Array Nat + a17 : Array Nat + a18 : Array Nat + a19 : Array Nat + a20 : Array Nat + a21 : Array Nat + a22 : Array Nat + a23 : Array Nat + a24 : Array Nat + a25 : Array Nat + a26 : Array Nat + a27 : Array Nat + a28 : Array Nat + a29 : List Nat + a30 : List Nat + a31 : List Nat + a32 : List Nat + a33 : List Nat + a34 : List Nat + a35 : List Nat + a36 : List Nat + a37 : List Nat + a38 : List Nat + a39 : List Nat + aa10 : Float × USize × UInt64 + aa11 : Float × USize × UInt64 + aa12 : Float × USize × UInt64 + aa13 : Float × USize × UInt64 + aa14 : Float × USize × UInt64 + aa15 : Float × USize × UInt64 + aa16 : Float × USize × UInt64 + aa17 : Float × USize × UInt64 + aa18 : Float × USize × UInt64 + aa19 : Float × USize × UInt64 + aa20 : Float × USize × UInt64 + aa21 : Float × USize × UInt64 + aa22 : Float × USize × UInt64 + aa23 : Float × USize × UInt64 + aa24 : Float × USize × UInt64 + aa25 : Float × USize × UInt64 + aa26 : Float × USize × UInt64 + aa27 : Float × USize × UInt64 + aa28 : Float × USize × UInt64 + aa29 : Float × USize × UInt64 + aa30 : Float × USize × UInt64 + deriving ToJson, FromJson, Repr, BEq