comparison json.ur @ 30:4e673b535434

Optimizing JSON generation
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Dec 2014 19:52:51 -0500
parents 7530b2b54353
children
comparison
equal deleted inserted replaced
29:7530b2b54353 30:4e673b535434
37 error <xml>Extra content at end of JSON record: {[s']}</xml> 37 error <xml>Extra content at end of JSON record: {[s']}</xml>
38 end 38 end
39 39
40 fun escape s = 40 fun escape s =
41 let 41 let
42 val len = String.length s 42 fun esc s =
43 43 case s of
44 fun esc i = 44 "" => "\""
45 if i >= len then 45 | _ =>
46 "\"" 46 let
47 else 47 val ch = String.sub s 0
48 let
49 val ch = String.sub s i
50 in 48 in
51 (if ch = #"\"" || ch = #"\\" then 49 (if ch = #"\"" || ch = #"\\" then
52 "\\" ^ String.str ch 50 "\\" ^ String.str ch
53 else 51 else
54 String.str ch) ^ esc (i+1) 52 String.str ch) ^ esc (String.suffix s 1)
55 end 53 end
56 in 54 in
57 "\"" ^ esc 0 55 "\"" ^ esc s
58 end 56 end
59 57
60 fun unescape s = 58 fun unescape s =
61 let 59 let
62 val len = String.length s 60 val len = String.length s
208 fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts = 206 fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
209 {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string] 207 {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
210 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc => 208 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
211 escape name ^ ":" ^ j.ToJson v ^ (case acc of 209 escape name ^ ":" ^ j.ToJson v ^ (case acc of
212 "" => "" 210 "" => ""
213 | _ => "," ^ acc)) 211 | acc => "," ^ acc))
214 "" fl jss names r ^ "}", 212 "" fl jss names r ^ "}",
215 FromJson = fn s => 213 FromJson = fn s =>
216 let 214 let
217 fun fromJ s (r : $(map option ts)) : $(map option ts) * string = 215 fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
218 if String.length s = 0 then 216 if String.length s = 0 then