comparison json.ur @ 0:63697ef80a2c

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