@@ -0,0 +1,98 @@
1+module Language.JSON.Data
2+
3+import Data.String.Extra
4+
5+%access private
6+%default total
7+
8+public export
9+data JSON
10+ = JNull
11+ | JBoolean Bool
12+ | JNumber Double
13+ | JString String
14+ | JArray (List JSON)
15+ | JObject (List (String, JSON))
16+
17+%name JSON json
18+
19+showChar : Char -> String
20+showChar 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
32+
33+showString : String -> String
34+showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
35+
36+||| Convert a JSON value into its string representation.
37+||| No whitespace is added.
38+stringify : JSON -> String
39+stringify JNull = "null"
40+stringify (JBoolean x) = if x then "true" else "false"
41+stringify (JNumber x) = show x
42+stringify (JString x) = showString x
43+stringify (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
51+stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
52+ where
53+ stringifyProp : (String, JSON) -> String
54+ stringifyProp (key, value) = showString key ++ ":" ++ stringify value
55+
56+ stringifyProps : List (String, JSON) -> String
57+ stringifyProps [] = ""
58+ stringifyProps (x :: xs) = stringifyProp x
59+ ++ if isNil xs
60+ then ""
61+ else "," ++ stringifyProps xs
62+
63+export
64+Show JSON where
65+ show = stringify
66+
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.
71+export
72+format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
73+format {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
92+
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