adam@0
|
1 class json a = {ToJson : a -> string,
|
adam@0
|
2 FromJson : string -> a * string}
|
adam@0
|
3
|
adam@0
|
4 fun mkJson [a] (x : {ToJson : a -> string,
|
adam@0
|
5 FromJson : string -> a * string}) = x
|
adam@0
|
6
|
adam@0
|
7 fun skipSpaces s =
|
adam@0
|
8 let
|
adam@0
|
9 val len = String.length s
|
adam@0
|
10
|
adam@0
|
11 fun skip i =
|
adam@0
|
12 if i >= len then
|
adam@0
|
13 ""
|
adam@0
|
14 else
|
adam@0
|
15 let
|
adam@0
|
16 val ch = String.sub s i
|
adam@0
|
17 in
|
adam@0
|
18 if Char.isSpace ch then
|
adam@0
|
19 skip (i+1)
|
adam@0
|
20 else
|
adam@0
|
21 String.substring s {Start = i, Len = len-i}
|
adam@0
|
22 end
|
adam@0
|
23 in
|
adam@0
|
24 skip 0
|
adam@0
|
25 end
|
adam@0
|
26
|
adam@0
|
27 fun toJson [a] (j : json a) : a -> string = j.ToJson
|
adam@0
|
28
|
adam@0
|
29 fun fromJson [a] (j : json a) (s : string) : a =
|
adam@0
|
30 let
|
adam@0
|
31 val (v, s') = j.FromJson (skipSpaces s)
|
adam@0
|
32 in
|
adam@0
|
33 if String.all Char.isSpace s' then
|
adam@0
|
34 v
|
adam@0
|
35 else
|
adam@0
|
36 error <xml>Extra content at end of JSON record: {[s']}</xml>
|
adam@0
|
37 end
|
adam@0
|
38
|
adam@0
|
39 fun escape s =
|
adam@0
|
40 let
|
adam@0
|
41 val len = String.length s
|
adam@0
|
42
|
adam@0
|
43 fun esc i =
|
adam@0
|
44 if i >= len then
|
adam@0
|
45 "\""
|
adam@0
|
46 else
|
adam@0
|
47 let
|
adam@0
|
48 val ch = String.sub s i
|
adam@0
|
49 in
|
adam@0
|
50 (if ch = #"\"" || ch = #"\\" then
|
adam@0
|
51 "\\" ^ String.str ch
|
adam@0
|
52 else
|
adam@0
|
53 String.str ch) ^ esc (i+1)
|
adam@0
|
54 end
|
adam@0
|
55 in
|
adam@0
|
56 "\"" ^ esc 0
|
adam@0
|
57 end
|
adam@0
|
58
|
adam@0
|
59 fun unescape s =
|
adam@0
|
60 let
|
adam@0
|
61 val len = String.length s
|
adam@0
|
62
|
adam@0
|
63 fun findEnd i =
|
adam@0
|
64 if i >= len then
|
adam@0
|
65 error <xml>JSON unescape: string ends before quote: {[s]}</xml>
|
adam@0
|
66 else
|
adam@0
|
67 let
|
adam@0
|
68 val ch = String.sub s i
|
adam@0
|
69 in
|
adam@0
|
70 case ch of
|
adam@0
|
71 #"\"" => i
|
adam@0
|
72 | #"\\" =>
|
adam@0
|
73 if i+1 >= len then
|
adam@0
|
74 error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
|
adam@0
|
75 else
|
adam@0
|
76 findEnd (i+2)
|
adam@0
|
77 | _ => findEnd (i+1)
|
adam@0
|
78 end
|
adam@0
|
79
|
adam@0
|
80 val last = findEnd 1
|
adam@0
|
81
|
adam@0
|
82 fun unesc i =
|
adam@0
|
83 if i >= last then
|
adam@0
|
84 ""
|
adam@0
|
85 else
|
adam@0
|
86 let
|
adam@0
|
87 val ch = String.sub s i
|
adam@0
|
88 in
|
adam@0
|
89 case ch of
|
adam@0
|
90 #"\\" =>
|
adam@0
|
91 if i+1 >= len then
|
adam@0
|
92 error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
|
adam@0
|
93 else
|
adam@0
|
94 String.str (String.sub s (i+1)) ^ unesc (i+2)
|
adam@0
|
95 | _ => String.str ch ^ unesc (i+1)
|
adam@0
|
96 end
|
adam@0
|
97 in
|
adam@0
|
98 if len = 0 || String.sub s 0 <> #"\"" then
|
adam@0
|
99 error <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
|
adam@0
|
100 else
|
adam@0
|
101 (unesc 1, String.substring s {Start = last+1, Len = len-last-1})
|
adam@0
|
102 end
|
adam@0
|
103
|
adam@0
|
104 val json_string = {ToJson = escape,
|
adam@0
|
105 FromJson = unescape}
|
adam@0
|
106
|
adam@0
|
107 fun numIn [a] (_ : read a) s : a * string =
|
adam@0
|
108 let
|
adam@0
|
109 val len = String.length s
|
adam@0
|
110
|
adam@0
|
111 fun findEnd i =
|
adam@0
|
112 if i >= len then
|
adam@0
|
113 i
|
adam@0
|
114 else
|
adam@0
|
115 let
|
adam@0
|
116 val ch = String.sub s i
|
adam@0
|
117 in
|
adam@0
|
118 if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then
|
adam@0
|
119 findEnd (i+1)
|
adam@0
|
120 else
|
adam@0
|
121 i
|
adam@0
|
122 end
|
adam@0
|
123
|
adam@0
|
124 val last = findEnd 0
|
adam@0
|
125 in
|
adam@0
|
126 (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last})
|
adam@0
|
127 end
|
adam@0
|
128
|
adam@0
|
129 fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show,
|
adam@0
|
130 FromJson = numIn}
|
adam@0
|
131
|
adam@0
|
132 val json_int = json_num
|
adam@0
|
133 val json_float = json_num
|
adam@0
|
134
|
adam@0
|
135 val json_bool = {ToJson = fn b => if b then "true" else "false",
|
adam@0
|
136 FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then
|
adam@0
|
137 (True, String.substring s {Start = 4, Len = String.length s - 4})
|
adam@0
|
138 else if String.isPrefix {Full = s, Prefix = "false"} then
|
adam@0
|
139 (False, String.substring s {Start = 5, Len = String.length s - 5})
|
adam@0
|
140 else
|
adam@0
|
141 error <xml>JSON: bad boolean string: {[s]}</xml>}
|
adam@0
|
142
|
adam@0
|
143 fun json_list [a] (j : json a) : json (list a) =
|
adam@0
|
144 let
|
adam@0
|
145 fun toJ' (ls : list a) : string =
|
adam@0
|
146 case ls of
|
adam@0
|
147 [] => ""
|
adam@0
|
148 | x :: ls => "," ^ toJson j x ^ toJ' ls
|
adam@0
|
149
|
adam@0
|
150 fun toJ (x : list a) : string =
|
adam@0
|
151 case x of
|
adam@0
|
152 [] => "[]"
|
adam@0
|
153 | x :: [] => "[" ^ toJson j x ^ "]"
|
adam@0
|
154 | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]"
|
adam@0
|
155
|
adam@0
|
156 fun fromJ (s : string) : list a * string =
|
adam@0
|
157 let
|
adam@0
|
158 fun fromJ' (s : string) : list a * string =
|
adam@0
|
159 if String.length s = 0 then
|
adam@0
|
160 error <xml>JSON list doesn't end with ']'</xml>
|
adam@0
|
161 else
|
adam@0
|
162 let
|
adam@0
|
163 val ch = String.sub s 0
|
adam@0
|
164 in
|
adam@0
|
165 case ch of
|
adam@0
|
166 #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1})
|
adam@0
|
167 | _ =>
|
adam@0
|
168 let
|
adam@0
|
169 val (x, s') = j.FromJson s
|
adam@0
|
170 val s' = skipSpaces s'
|
adam@0
|
171 val s' = if String.length s' = 0 then
|
adam@0
|
172 error <xml>JSON list doesn't end with ']'</xml>
|
adam@0
|
173 else if String.sub s' 0 = #"," then
|
adam@0
|
174 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
|
adam@0
|
175 else
|
adam@0
|
176 s'
|
adam@0
|
177
|
adam@0
|
178 val (ls, s'') = fromJ' s'
|
adam@0
|
179 in
|
adam@0
|
180 (x :: ls, s'')
|
adam@0
|
181 end
|
adam@0
|
182 end
|
adam@0
|
183 in
|
adam@0
|
184 if String.length s = 0 || String.sub s 0 <> #"[" then
|
adam@0
|
185 error <xml>JSON list doesn't start with '[': {[s]}</xml>
|
adam@0
|
186 else
|
adam@0
|
187 fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
|
adam@0
|
188 end
|
adam@0
|
189 in
|
adam@0
|
190 {ToJson = toJ,
|
adam@0
|
191 FromJson = fromJ}
|
adam@0
|
192 end
|