@@ -47,54 +47,97 @@ instance : ToJson String := ⟨fun s => s⟩
4747instance : FromJson System.FilePath := ⟨fun j => System.FilePath.mk <$> Json.getStr? j⟩
4848instance : ToJson System.FilePath := ⟨fun p => p.toString⟩
4949
50+ protected def _root_.Array.fromJson? [FromJson α] : Json → Except String (Array α)
51+ | Json.arr a => a.mapM fromJson?
52+ | j => throw s! "expected JSON array, got '{ j} '"
53+
5054instance [FromJson α] : FromJson (Array α) where
51- fromJson?
52- | Json.arr a => a.mapM fromJson?
53- | j => throw s! "expected JSON array, got '{ j} '"
55+ fromJson? := Array.fromJson?
56+
57+ protected def _root_.Array.toJson [ToJson α] (a : Array α) : Json :=
58+ Json.arr (a.map toJson)
5459
55- instance [ToJson α] : ToJson (Array α) :=
56- ⟨fun a => Json.arr (a.map toJson)⟩
60+ instance [ToJson α] : ToJson (Array α) where
61+ toJson := Array.toJson
62+
63+ protected def _root_.List.fromJson? [FromJson α] (j : Json) : Except String (List α) :=
64+ (fromJson? j (α := Array α)).map Array.toList
5765
5866instance [FromJson α] : FromJson (List α) where
59- fromJson? j := (fromJson? j (α := Array α)).map Array.toList
67+ fromJson? := List.fromJson?
68+
69+ protected def _root_.List.toJson [ToJson α] (a : List α) : Json :=
70+ toJson a.toArray
6071
6172instance [ToJson α] : ToJson (List α) where
62- toJson xs := toJson xs.toArray
73+ toJson := List.toJson
74+
75+ protected def _root_.Option.fromJson? [FromJson α] : Json → Except String (Option α)
76+ | Json.null => Except.ok none
77+ | j => some <$> fromJson? j
6378
6479instance [FromJson α] : FromJson (Option α) where
65- fromJson?
66- | Json.null => Except.ok none
67- | j => some <$> fromJson? j
80+ fromJson? := Option.fromJson?
81+
82+ protected def _root_.Option.toJson [ToJson α] : Option α → Json
83+ | none => Json.null
84+ | some a => toJson a
85+
86+ instance [ToJson α] : ToJson (Option α) where
87+ toJson := Option.toJson
6888
69- instance [ToJson α] : ToJson (Option α) :=
70- ⟨fun
71- | none => Json.null
72- | some a => toJson a⟩
89+ protected def _root_.Prod.fromJson? {α : Type u} {β : Type v} [FromJson α] [FromJson β] : Json → Except String (α × β)
90+ | Json.arr #[ja, jb] => do
91+ let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up
92+ let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up
93+ return (a, b)
94+ | j => throw s! "expected pair, got '{ j} '"
7395
7496instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) where
75- fromJson?
76- | Json.arr #[ja, jb] => do
77- let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up
78- let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up
79- return (a, b)
80- | j => throw s! "expected pair, got '{ j} '"
97+ fromJson? := Prod.fromJson?
98+
99+ protected def _root_.Prod.toJson [ToJson α] [ToJson β] : α × β → Json
100+ | (a, b) => Json.arr #[toJson a, toJson b]
81101
82102instance [ToJson α] [ToJson β] : ToJson (α × β) where
83- toJson := fun (a, b) => Json.arr #[toJson a, toJson b]
103+ toJson := Prod.toJson
104+
105+ protected def Name.fromJson? (j : Json) : Except String Name := do
106+ let s ← j.getStr?
107+ if s == "[anonymous]" then
108+ return Name.anonymous
109+ else
110+ let n := s.toName
111+ if n.isAnonymous then throw s! "expected a `Name`, got '{ j} '"
112+ return n
84113
85114instance : FromJson Name where
86- fromJson? j := do
87- let s ← j.getStr?
88- if s == "[anonymous]" then
89- return Name.anonymous
90- else
91- let n := s.toName
92- if n.isAnonymous then throw s! "expected a `Name`, got '{ j} '"
93- return n
115+ fromJson? := Name.fromJson?
94116
95117instance : ToJson Name where
96118 toJson n := toString n
97119
120+ protected def NameMap.fromJson? [FromJson α] : Json → Except String (NameMap α)
121+ | .obj obj => obj.foldM (init := {}) fun m k v => do
122+ if k == "[anonymous]" then
123+ return m.insert .anonymous (← fromJson? v)
124+ else
125+ let n := k.toName
126+ if n.isAnonymous then
127+ throw s! "expected a `Name`, got '{ k} '"
128+ else
129+ return m.insert n (← fromJson? v)
130+ | j => throw s! "expected a `NameMap`, got '{ j} '"
131+
132+ instance [FromJson α] : FromJson (NameMap α) where
133+ fromJson? := NameMap.fromJson?
134+
135+ protected def NameMap.toJson [ToJson α] (m : NameMap α) : Json :=
136+ Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf
137+
138+ instance [ToJson α] : ToJson (NameMap α) where
139+ toJson := NameMap.toJson
140+
98141/-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript
99142cannot represent 64-bit numbers. -/
100143def bignumFromJson? (j : Json) : Except String Nat := do
@@ -106,58 +149,77 @@ def bignumFromJson? (j : Json) : Except String Nat := do
106149def bignumToJson (n : Nat) : Json :=
107150 toString n
108151
152+ protected def _root_.USize.fromJson? (j : Json) : Except String USize := do
153+ let n ← bignumFromJson? j
154+ if n ≥ USize.size then
155+ throw "value '{j}' is too large for `USize`"
156+ return USize.ofNat n
157+
109158instance : FromJson USize where
110- fromJson? j := do
111- let n ← bignumFromJson? j
112- if n ≥ USize.size then
113- throw "value '{j}' is too large for `USize`"
114- return USize.ofNat n
159+ fromJson? := USize.fromJson?
115160
116161instance : ToJson USize where
117162 toJson v := bignumToJson (USize.toNat v)
118163
164+ protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do
165+ let n ← bignumFromJson? j
166+ if n ≥ UInt64.size then
167+ throw "value '{j}' is too large for `UInt64`"
168+ return UInt64.ofNat n
169+
119170instance : FromJson UInt64 where
120- fromJson? j := do
121- let n ← bignumFromJson? j
122- if n ≥ UInt64.size then
123- throw "value '{j}' is too large for `UInt64`"
124- return UInt64.ofNat n
171+ fromJson? := UInt64.fromJson?
125172
126173instance : ToJson UInt64 where
127174 toJson v := bignumToJson (UInt64.toNat v)
128175
176+ protected def _root_.Float.toJson (x : Float) : Json :=
177+ match JsonNumber.fromFloat? x with
178+ | Sum.inl e => Json.str e
179+ | Sum.inr n => Json.num n
180+
129181instance : ToJson Float where
130- toJson x :=
131- match JsonNumber.fromFloat? x with
132- | Sum.inl e => Json.str e
133- | Sum.inr n => Json.num n
182+ toJson := Float.toJson
183+
184+ protected def _root_.Float.fromJson? : Json → Except String Float
185+ | (Json.str "Infinity" ) => Except.ok (1 .0 / 0 .0 )
186+ | (Json.str "-Infinity" ) => Except.ok (-1 .0 / 0 .0 )
187+ | (Json.str "NaN" ) => Except.ok (0 .0 / 0 .0 )
188+ | (Json.num jn) => Except.ok jn.toFloat
189+ | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."
134190
135191instance : FromJson Float where
136- fromJson? := fun
137- | (Json.str "Infinity" ) => Except.ok (1 .0 / 0 .0 )
138- | (Json.str "-Infinity" ) => Except.ok (-1 .0 / 0 .0 )
139- | (Json.str "NaN" ) => Except.ok (0 .0 / 0 .0 )
140- | (Json.num jn) => Except.ok jn.toFloat
141- | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."
192+ fromJson? := Float.fromJson?
193+
194+ protected def RBMap.toJson [ToJson α] (m : RBMap String α cmp) : Json :=
195+ Json.obj <| RBNode.map (fun _ => toJson) <| m.val
142196
143197instance [ToJson α] : ToJson (RBMap String α cmp) where
144- toJson m := Json.obj <| RBNode.map (fun _ => toJson) <| m.val
198+ toJson := RBMap.toJson
199+
200+ protected def RBMap.fromJson? [FromJson α] (j : Json) : Except String (RBMap String α cmp) := do
201+ let o ← j.getObj?
202+ o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅
145203
146204instance {cmp} [FromJson α] : FromJson (RBMap String α cmp) where
147- fromJson? j := do
148- let o ← j.getObj?
149- o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅
205+ fromJson? := RBMap.fromJson?
150206
151207namespace Json
152208
153- instance : FromJson Structured := ⟨fun
154- | arr a => return Structured.arr a
155- | obj o => return Structured.obj o
156- | j => throw s! "expected structured object, got '{ j} '"
209+ protected def Structured.fromJson? : Json → Except String Structured
210+ | .arr a => return Structured.arr a
211+ | .obj o => return Structured.obj o
212+ | j => throw s! "expected structured object, got '{ j} '"
213+
214+ instance : FromJson Structured where
215+ fromJson? := Structured.fromJson?
216+
217+ protected def Structured.toJson : Structured → Json
218+ | .arr a => .arr a
219+ | .obj o => .obj o
157220
158- instance : ToJson Structured := ⟨fun
159- | Structured.arr a => arr a
160- | Structured.obj o => obj o⟩
221+ instance : ToJson Structured where
222+ toJson := Structured.toJson
161223
162224def toStructured? [ToJson α] (v : α) : Except String Structured :=
163225 fromJson? (toJson v)
0 commit comments