git.iko.soy/Idris-dev
on ca34dec help sign in
Idris-dev/libs/contrib/Language/JSON/Data.idr
98 lines 3.4 kB history raw
1module Language.JSON.Data
3import Data.String.Extra
5%access private
6%default total
8public export
9data JSON
10 = JNull
11 | JBoolean Bool
12 | JNumber Double
13 | JString String
14 | JArray (List JSON)
15 | JObject (List (String, JSON))
17%name JSON json
19showChar : Char -> String
20showChar c
21 = case c of
22 '\b' => "\\b"
23 '\f' => "\\f"
24 '\n' => "\\n"
25 '\r' => "\\r"
26 '\t' => "\\t"
27 '\\' => "\\\\"
28 '"' => "\\\""
29 c => if isControl c || c >= '\127'
30 then "\\u" ++ b16ToHexString (fromInteger (cast (ord c)))
31 else singleton c
33showString : String -> String
34showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
36||| Convert a JSON value into its string representation.
37||| No whitespace is added.
38stringify : JSON -> String
39stringify JNull = "null"
40stringify (JBoolean x) = if x then "true" else "false"
41stringify (JNumber x) = show x
42stringify (JString x) = showString x
43stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
44 where
45 stringifyValues : List JSON -> String
46 stringifyValues [] = ""
47 stringifyValues (x :: xs) = stringify x
48 ++ if isNil xs
49 then ""
50 else "," ++ stringifyValues xs
51stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
52 where
53 stringifyProp : (String, JSON) -> String
54 stringifyProp (key, value) = showString key ++ ":" ++ stringify value
56 stringifyProps : List (String, JSON) -> String
57 stringifyProps [] = ""
58 stringifyProps (x :: xs) = stringifyProp x
59 ++ if isNil xs
60 then ""
61 else "," ++ stringifyProps xs
63export
64Show JSON where
65 show = stringify
67||| Format a JSON value, indenting by `n` spaces per nesting level.
68|||
69||| @curr The current indentation amount, measured in spaces.
70||| @n The amount of spaces to indent per nesting level.
71export
72format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
73format {curr} n json = indent curr $ formatValue curr n json
74 where
75 formatValue : (curr, n : Nat) -> JSON -> String
76 formatValue _ _ (JArray []) = "[]"
77 formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs
78 ++ indent curr "]"
79 where
80 formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String
81 formatValues (x :: xs) = format {curr=(curr + n)} n x
82 ++ case nonEmpty xs of
83 Yes ok => ",\n" ++ formatValues xs
84 No _ => "\n"
85 formatValue _ _ (JObject []) = "{}"
86 formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs
87 ++ indent curr "}"
88 where
89 formatProp : (String, JSON) -> String
90 formatProp (key, value) = indent (curr + n) (showString key ++ ": ")
91 ++ formatValue (curr + n) n value
93 formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String
94 formatProps (x :: xs) = formatProp x
95 ++ case nonEmpty xs of
96 Yes ok => ",\n" ++ formatProps xs
97 No _ => "\n"
98 formatValue _ _ x = stringify x