0 | module Language.JSON.Data
  1 |
  2 | import Data.Bits
  3 | import Data.List
  4 | import Data.String.Extra
  5 | import Data.String
  6 |
  7 | %default total
  8 |
  9 | public export
 10 | data JSON
 11 |    = JNull
 12 |    | JBoolean Bool
 13 |    | JNumber Double
 14 |    | JString String
 15 |    | JArray (List JSON)
 16 |    | JObject (List (String, JSON))
 17 |
 18 | %name JSON json
 19 |
 20 | public export
 21 | Eq JSON where
 22 |     JNull == JNull = True
 23 |     JBoolean x == JBoolean y = x == y
 24 |     JNumber x == JNumber y = x == y
 25 |     JString x == JString y = x == y
 26 |     JArray xs == JArray ys = assert_total $ xs == ys
 27 |     JObject xs == JObject ys = assert_total $ on (==) (sortBy $ compare `on` fst) xs ys
 28 |     _ == _ = False
 29 |
 30 | private
 31 | b16ToHexString : Bits16 -> String
 32 | b16ToHexString n =
 33 |   case n of
 34 |     0 => "0"
 35 |     1 => "1"
 36 |     2 => "2"
 37 |     3 => "3"
 38 |     4 => "4"
 39 |     5 => "5"
 40 |     6 => "6"
 41 |     7 => "7"
 42 |     8 => "8"
 43 |     9 => "9"
 44 |     10 => "A"
 45 |     11 => "B"
 46 |     12 => "C"
 47 |     13 => "D"
 48 |     14 => "E"
 49 |     15 => "F"
 50 |     other => assert_total $
 51 |                b16ToHexString (n `shiftR` 4) ++
 52 |                b16ToHexString (n .&. 15)
 53 |
 54 | private
 55 | showChar : Char -> String
 56 | showChar c
 57 |   = case c of
 58 |          '\b' => "\\b"
 59 |          '\f' => "\\f"
 60 |          '\n' => "\\n"
 61 |          '\r' => "\\r"
 62 |          '\t' => "\\t"
 63 |          '\\' => "\\\\"
 64 |          '"'  => "\\\""
 65 |          c => if isControl c || c >= '\127'
 66 |                  then let hex = b16ToHexString (cast $ ord c)
 67 |                        in "\\u" ++ justifyRight 4 '0' hex
 68 |                  else singleton c
 69 |
 70 | private
 71 | showString : String -> String
 72 | showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
 73 |
 74 | ||| Convert a JSON value into its string representation.
 75 | ||| No whitespace is added.
 76 | private
 77 | stringify : JSON -> String
 78 | stringify JNull = "null"
 79 | stringify (JBoolean x) = if x then "true" else "false"
 80 | stringify (JNumber x) = show x
 81 | stringify (JString x) = showString x
 82 | stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
 83 |   where
 84 |     stringifyValues : List JSON -> String
 85 |     stringifyValues [] = ""
 86 |     stringifyValues (x :: xs) = stringify x
 87 |                              ++ if isNil xs
 88 |                                    then ""
 89 |                                    else "," ++ stringifyValues xs
 90 | stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
 91 |   where
 92 |     stringifyProp : (String, JSON) -> String
 93 |     stringifyProp (key, value) = showString key ++ ":" ++ stringify value
 94 |
 95 |     stringifyProps : List (String, JSON) -> String
 96 |     stringifyProps [] = ""
 97 |     stringifyProps (x :: xs) = stringifyProp x
 98 |                             ++ if isNil xs
 99 |                                   then ""
100 |                                   else "," ++ stringifyProps xs
101 |
102 | export
103 | Show JSON where
104 |   show = stringify
105 |
106 | export
107 | [Idris] Show JSON where
108 |   showPrec d JNull = "JNull"
109 |   showPrec d (JBoolean x) = showCon d "JBoolean" $ showArg x
110 |   showPrec d (JNumber x) = showCon d "JNumber" $ showArg x
111 |   showPrec d (JString x) = showCon d "JString" $ showArg x
112 |   showPrec d (JArray xs) = assert_total $ showCon d "JArray" $ showArg xs
113 |   showPrec d (JObject xs) = assert_total $ showCon d "JObject" $ showArg xs
114 |
115 | ||| Format a JSON value, indenting by `n` spaces per nesting level.
116 | |||
117 | ||| @curr The current indentation amount, measured in spaces.
118 | ||| @n The amount of spaces to indent per nesting level.
119 | export
120 | format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
121 | format {curr} n json = indent curr $ formatValue curr n json
122 |   where
123 |     formatValue : (curr, n : Nat) -> JSON -> String
124 |     formatValue _ _ (JArray []) = "[]"
125 |     formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs
126 |                                            ++ indent curr "]"
127 |       where
128 |         formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String
129 |         formatValues (x :: xs) = format {curr=(curr + n)} n x
130 |                               ++ case xs of
131 |                                       _ :: _ => ",\n" ++ formatValues xs
132 |                                       [] => "\n"
133 |     formatValue _ _ (JObject []) = "{}"
134 |     formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs
135 |                                             ++ indent curr "}"
136 |       where
137 |         formatProp : (String, JSON) -> String
138 |         formatProp (key, value) = indent (curr + n) (showString key ++ ": ")
139 |                                ++ formatValue (curr + n) n value
140 |
141 |         formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String
142 |         formatProps (x :: xs) = formatProp x
143 |                              ++ case xs of
144 |                                      _ :: _ => ",\n" ++ formatProps xs
145 |                                      [] => "\n"
146 |     formatValue _ _ x = stringify x
147 |
148 | public export
149 | Cast () JSON where
150 |   cast () = JNull
151 |
152 | public export
153 | Cast Bool JSON where
154 |   cast = JBoolean
155 |
156 | public export
157 | Cast Double JSON where
158 |   cast = JNumber
159 |
160 | public export
161 | Cast String JSON where
162 |   cast = JString
163 |
164 | public export
165 | Cast a JSON => Cast (List a) JSON where
166 |   cast xs = JArray $ map cast xs
167 |
168 | public export
169 | lookup : String -> JSON -> Maybe JSON
170 | lookup key (JObject xs) = lookup key xs
171 | lookup key json = Nothing
172 |
173 | public export
174 | update : (Maybe JSON -> Maybe JSON) -> String -> JSON -> JSON
175 | update f key (JObject xs) = JObject $ updateAttr f key xs
176 |   where
177 |     updateAttr : (Maybe JSON -> Maybe JSON) -> String -> List (String, JSON) -> List (String, JSON)
178 |     updateAttr f key [] = do
179 |         let Just y = f Nothing
180 |             | Nothing => []
181 |         [(key, y)]
182 |     updateAttr f key ((nm, x) :: xs) = if key == nm
183 |         then do
184 |             let Just y = f (Just x)
185 |                 | Nothing => xs
186 |             (nm, y) :: xs
187 |         else (nm, x) :: updateAttr f key xs
188 | update f key json = json
189 |
190 | public export
191 | traverseJSON : Monad m => (JSON -> m JSON) -> JSON -> m JSON
192 | traverseJSON f (JArray xs) = do
193 |     xs <- assert_total $ traverse (traverseJSON f) xs
194 |     f $ JArray xs
195 | traverseJSON f (JObject xs) = do
196 |     xs <- traverse (assert_total $ bitraverse pure $ traverseJSON f) xs
197 |     f $ JObject xs
198 | traverseJSON f json = f json
199 |
200 | public export
201 | traverseJSON_ : Monad m => (JSON -> m ()) -> JSON -> m ()
202 | traverseJSON_ f json = ignore $ traverseJSON (\x => f x *> pure x) json
203 |