0 | ||| Interfaces for converting values from/to JSON.
  1 | |||
  2 | ||| (C) The Idris Community, 2021
  3 | module Language.JSON.Interfaces
  4 |
  5 | import Data.SortedMap
  6 | import Data.String
  7 | import Language.JSON.Lexer
  8 | import Language.JSON.Parser
  9 |
 10 | import Language.JSON
 11 |
 12 | %default total
 13 |
 14 | -- TODO: Maybe we should be using a more expressive type than Maybe.
 15 | ||| A type that can be converted to JSON.
 16 | ||| An example type and implementation is:
 17 | ||| ```idris example
 18 | ||| record Position where
 19 | |||   constructor MkPosition
 20 | |||   x : Integer
 21 | |||   y : Integer
 22 | |||
 23 | ||| ToJSON Position where
 24 | |||   toJSON pos = JObject [("x", toJSON pos.x), ("y", toJSON pos.y)]
 25 | ||| ```
 26 | public export
 27 | interface ToJSON a where
 28 |   toJSON : a -> JSON
 29 |
 30 | ||| A type that can be possibly converted from JSON.
 31 | ||| An example type and implementation is:
 32 | ||| ```idris example
 33 | ||| record Position where
 34 | |||   constructor MkPosition
 35 | |||   x : Integer
 36 | |||   y : Integer
 37 | |||
 38 | ||| FromJSON Position where
 39 | |||   fromJSON (JObject arg) = do
 40 | |||     x <- lookup "x" arg >>= fromJSON
 41 | |||     y <- lookup "y" arg >>= fromJSON
 42 | |||     pure $ MkPosition x y
 43 | |||   fromJSON _ = neutral
 44 | ||| ```
 45 | public export
 46 | interface FromJSON a where
 47 |   fromJSON : JSON -> Maybe a
 48 |
 49 | export
 50 | ToJSON JSON where
 51 |   toJSON = id
 52 |
 53 | export
 54 | FromJSON JSON where
 55 |   fromJSON = pure
 56 |
 57 | export
 58 | ToJSON Integer where
 59 |   toJSON = JNumber . cast
 60 |
 61 | -- NOTE: In JSON all numbers are `Double`, for integers we should cast or fail
 62 | -- for invalid values?
 63 | export
 64 | FromJSON Integer where
 65 |   fromJSON (JNumber x) = pure (cast x)
 66 |   fromJSON _ = neutral
 67 |
 68 | export
 69 | ToJSON Int where
 70 |   toJSON = JNumber . cast
 71 |
 72 | export
 73 | FromJSON Int where
 74 |   fromJSON (JNumber x) = pure (cast x)
 75 |   fromJSON _ = neutral
 76 |
 77 | export
 78 | ToJSON Bits8 where
 79 |   toJSON = JNumber . cast . cast {to = Int}
 80 |
 81 | export
 82 | FromJSON Bits8 where
 83 |   fromJSON (JNumber x) = pure (fromInteger $ cast x)
 84 |   fromJSON _ = neutral
 85 |
 86 | export
 87 | ToJSON Bits16 where
 88 |   toJSON = JNumber . cast . cast {to = Int}
 89 |
 90 | export
 91 | FromJSON Bits16 where
 92 |   fromJSON (JNumber x) = pure (fromInteger $ cast x)
 93 |   fromJSON _ = neutral
 94 |
 95 | export
 96 | ToJSON Bits32 where
 97 |   toJSON = JNumber . cast . cast {to = Int}
 98 |
 99 | export
100 | FromJSON Bits32 where
101 |   fromJSON (JNumber x) = pure (fromInteger $ cast x)
102 |   fromJSON _ = neutral
103 |
104 | export
105 | ToJSON Bits64 where
106 |   toJSON = JNumber . cast . cast {to = Int}
107 |
108 | export
109 | FromJSON Bits64 where
110 |   fromJSON (JNumber x) = pure (fromInteger $ cast x)
111 |   fromJSON _ = neutral
112 |
113 | export
114 | ToJSON Double where
115 |   toJSON = JNumber
116 |
117 | export
118 | FromJSON Double where
119 |   fromJSON (JNumber x) = pure x
120 |   fromJSON _ = neutral
121 |
122 | export
123 | ToJSON Nat where
124 |   toJSON = JNumber . cast
125 |
126 | export
127 | FromJSON Nat where
128 |   fromJSON (JNumber x) = pure (fromInteger $ cast x)
129 |   fromJSON _ = neutral
130 |
131 | export
132 | ToJSON String where
133 |   toJSON = JString
134 |
135 | export
136 | FromJSON String where
137 |   fromJSON (JString s) = pure s
138 |   fromJSON _ = neutral
139 |
140 | export
141 | ToJSON Char where
142 |   toJSON = toJSON . String.singleton
143 |
144 | export
145 | FromJSON Char where
146 |   fromJSON (JString s) = case strM s of
147 |                               StrCons c "" => pure c
148 |                               _ => neutral
149 |   fromJSON _ = neutral
150 |
151 | export
152 | ToJSON Bool where
153 |   toJSON = JBoolean
154 |
155 | export
156 | FromJSON Bool where
157 |   fromJSON (JBoolean b) = pure b
158 |   fromJSON _ = neutral
159 |
160 | export
161 | ToJSON a => ToJSON (Maybe a) where
162 |   toJSON Nothing = JNull
163 |   toJSON (Just x) = toJSON x
164 |
165 | export
166 | FromJSON a => FromJSON (Maybe a) where
167 |   fromJSON JNull = pure Nothing
168 |   fromJSON json @{impl} = pure <$> fromJSON @{impl} json
169 |
170 | export
171 | ToJSON a => ToJSON (List a) where
172 |   toJSON = JArray . map toJSON
173 |
174 | export
175 | FromJSON a => FromJSON (List a) where
176 |   fromJSON (JArray xs) = traverse fromJSON xs
177 |   fromJSON _ = neutral
178 |
179 | export
180 | ToJSON () where
181 |   toJSON () = JObject empty
182 |
183 | export
184 | FromJSON () where
185 |   fromJSON (JObject xs) = guard $ null xs
186 |   fromJSON _ = neutral
187 |
188 | export
189 | (ToJSON a, ToJSON b) => ToJSON (a, b) where
190 |   toJSON (x, y) = JArray [toJSON x, toJSON y]
191 |
192 | export
193 | (FromJSON a, FromJSON b) => FromJSON (a, b) where
194 |   fromJSON (JArray [x, y]) = (,) <$> fromJSON x <*> fromJSON y
195 |   fromJSON _ = neutral
196 |
197 | export
198 | ToJSON v => ToJSON (SortedMap String v) where
199 |   toJSON m = JObject (toList $ toJSON <$> m)
200 |
201 | export
202 | FromJSON v => FromJSON (SortedMap String v) where
203 |   fromJSON (JObject xs) = fromList <$> traverse (\(k, v) => (k,) <$> fromJSON v) xs
204 |   fromJSON _ = neutral
205 |
206 | export
207 | ToJSON a => ToJSON (Inf a) where
208 |   toJSON x = toJSON x
209 |
210 | export
211 | FromJSON a => FromJSON (Inf a) where
212 |   fromJSON @{impl} x = map (\x => Delay x) (fromJSON @{impl} x)
213 |