Mercurial > meta

annotate json.ur @ 25:9f56676e7c4e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track addition of 'style' and 'dynStyle'
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 May 2012 15:16:27 -0400
parents 9d6b931fbd13
children 7530b2b54353
rev   line source
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
ezyang@23 28 fun fromJson' [a] (j : json a) : string -> a * string = j.FromJson
adam@0 29
adam@0 30 fun fromJson [a] (j : json a) (s : string) : a =
adam@0 31 let
adam@0 32 val (v, s') = j.FromJson (skipSpaces s)
adam@0 33 in
adam@0 34 if String.all Char.isSpace s' then
adam@0 35 v
adam@0 36 else
adam@0 37 error <xml>Extra content at end of JSON record: {[s']}</xml>
adam@0 38 end
adam@0 39
adam@0 40 fun escape s =
adam@0 41 let
adam@0 42 val len = String.length s
adam@0 43
adam@0 44 fun esc i =
adam@0 45 if i >= len then
adam@0 46 "\""
adam@0 47 else
adam@0 48 let
adam@0 49 val ch = String.sub s i
adam@0 50 in
adam@0 51 (if ch = #"\"" || ch = #"\\" then
adam@0 52 "\\" ^ String.str ch
adam@0 53 else
adam@0 54 String.str ch) ^ esc (i+1)
adam@0 55 end
adam@0 56 in
adam@0 57 "\"" ^ esc 0
adam@0 58 end
adam@0 59
adam@0 60 fun unescape s =
adam@0 61 let
adam@0 62 val len = String.length s
adam@0 63
adam@0 64 fun findEnd i =
adam@0 65 if i >= len then
adam@0 66 error <xml>JSON unescape: string ends before quote: {[s]}</xml>
adam@0 67 else
adam@0 68 let
adam@0 69 val ch = String.sub s i
adam@0 70 in
adam@0 71 case ch of
adam@0 72 #"\"" => i
adam@0 73 | #"\\" =>
adam@0 74 if i+1 >= len then
adam@0 75 error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
adam@0 76 else
adam@0 77 findEnd (i+2)
adam@0 78 | _ => findEnd (i+1)
adam@0 79 end
adam@0 80
adam@0 81 val last = findEnd 1
adam@0 82
adam@0 83 fun unesc i =
adam@0 84 if i >= last then
adam@0 85 ""
adam@0 86 else
adam@0 87 let
adam@0 88 val ch = String.sub s i
adam@0 89 in
adam@0 90 case ch of
adam@0 91 #"\\" =>
adam@0 92 if i+1 >= len then
adam@0 93 error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
adam@0 94 else
adam@0 95 String.str (String.sub s (i+1)) ^ unesc (i+2)
adam@0 96 | _ => String.str ch ^ unesc (i+1)
adam@0 97 end
adam@0 98 in
adam@0 99 if len = 0 || String.sub s 0 <> #"\"" then
adam@0 100 error <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
adam@0 101 else
adam@0 102 (unesc 1, String.substring s {Start = last+1, Len = len-last-1})
adam@0 103 end
adam@0 104
adam@0 105 val json_string = {ToJson = escape,
adam@0 106 FromJson = unescape}
adam@0 107
adam@0 108 fun numIn [a] (_ : read a) s : a * string =
adam@0 109 let
adam@0 110 val len = String.length s
adam@0 111
adam@0 112 fun findEnd i =
adam@0 113 if i >= len then
adam@0 114 i
adam@0 115 else
adam@0 116 let
adam@0 117 val ch = String.sub s i
adam@0 118 in
adam@0 119 if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then
adam@0 120 findEnd (i+1)
adam@0 121 else
adam@0 122 i
adam@0 123 end
adam@0 124
adam@0 125 val last = findEnd 0
adam@0 126 in
adam@0 127 (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last})
adam@0 128 end
adam@0 129
adam@0 130 fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show,
adam@0 131 FromJson = numIn}
adam@0 132
adam@0 133 val json_int = json_num
adam@0 134 val json_float = json_num
adam@0 135
adam@0 136 val json_bool = {ToJson = fn b => if b then "true" else "false",
adam@0 137 FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then
adam@0 138 (True, String.substring s {Start = 4, Len = String.length s - 4})
adam@0 139 else if String.isPrefix {Full = s, Prefix = "false"} then
adam@0 140 (False, String.substring s {Start = 5, Len = String.length s - 5})
adam@0 141 else
adam@0 142 error <xml>JSON: bad boolean string: {[s]}</xml>}
adam@0 143
adam@4 144 fun json_option [a] (j : json a) : json (option a) =
adam@4 145 {ToJson = fn v => case v of
adam@4 146 None => "null"
adam@4 147 | Some v => j.ToJson v,
adam@4 148 FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then
adam@4 149 (None, String.substring s {Start = 4, Len = String.length s - 4})
adam@4 150 else
adam@4 151 let
adam@4 152 val (v, s') = j.FromJson s
adam@4 153 in
adam@4 154 (Some v, s')
adam@4 155 end}
adam@4 156
adam@0 157 fun json_list [a] (j : json a) : json (list a) =
adam@0 158 let
adam@0 159 fun toJ' (ls : list a) : string =
adam@0 160 case ls of
adam@0 161 [] => ""
adam@0 162 | x :: ls => "," ^ toJson j x ^ toJ' ls
adam@0 163
adam@0 164 fun toJ (x : list a) : string =
adam@0 165 case x of
adam@0 166 [] => "[]"
adam@0 167 | x :: [] => "[" ^ toJson j x ^ "]"
adam@0 168 | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]"
adam@0 169
adam@0 170 fun fromJ (s : string) : list a * string =
adam@0 171 let
adam@0 172 fun fromJ' (s : string) : list a * string =
adam@0 173 if String.length s = 0 then
adam@0 174 error <xml>JSON list doesn't end with ']'</xml>
adam@0 175 else
adam@0 176 let
adam@0 177 val ch = String.sub s 0
adam@0 178 in
adam@0 179 case ch of
adam@0 180 #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1})
adam@0 181 | _ =>
adam@0 182 let
adam@0 183 val (x, s') = j.FromJson s
adam@0 184 val s' = skipSpaces s'
adam@0 185 val s' = if String.length s' = 0 then
adam@0 186 error <xml>JSON list doesn't end with ']'</xml>
adam@0 187 else if String.sub s' 0 = #"," then
adam@0 188 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
adam@0 189 else
adam@0 190 s'
adam@0 191
adam@0 192 val (ls, s'') = fromJ' s'
adam@0 193 in
adam@0 194 (x :: ls, s'')
adam@0 195 end
adam@0 196 end
adam@0 197 in
adam@0 198 if String.length s = 0 || String.sub s 0 <> #"[" then
adam@0 199 error <xml>JSON list doesn't start with '[': {[s]}</xml>
adam@0 200 else
adam@0 201 fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
adam@0 202 end
adam@0 203 in
adam@0 204 {ToJson = toJ,
adam@0 205 FromJson = fromJ}
adam@0 206 end
adam@1 207
adam@1 208 fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
adam@18 209 {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
adam@1 210 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
adam@1 211 escape name ^ ":" ^ j.ToJson v ^ (case acc of
adam@1 212 "" => ""
adam@1 213 | _ => "," ^ acc))
adam@1 214 "" fl jss names r ^ "}",
adam@2 215 FromJson = fn s =>
adam@2 216 let
adam@2 217 fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
adam@2 218 if String.length s = 0 then
adam@2 219 error <xml>JSON object doesn't end in brace</xml>
adam@2 220 else if String.sub s 0 = #"}" then
adam@2 221 (r, String.substring s {Start = 1, Len = String.length s - 1})
adam@2 222 else let
adam@2 223 val (name, s') = unescape s
adam@2 224 val s' = skipSpaces s'
adam@2 225 val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
ezyang@22 226 error <xml>No colon after JSON object field name</xml>
adam@2 227 else
adam@2 228 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
adam@2 229
adam@2 230 val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string]
adam@2 231 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r =>
adam@2 232 if name = name' then
adam@2 233 let
adam@2 234 val (v, s') = j.FromJson s'
adam@2 235 in
adam@2 236 (r -- nm ++ {nm = Some v}, s')
adam@2 237 end
adam@2 238 else
adam@2 239 let
adam@2 240 val (r', s') = acc (r -- nm)
adam@2 241 in
adam@2 242 (r' ++ {nm = r.nm}, s')
adam@2 243 end)
adam@2 244 (fn _ => error <xml>Unknown JSON object field name {[name]}</xml>)
adam@2 245 fl jss names r
adam@2 246
adam@2 247 val s' = skipSpaces s'
adam@2 248 val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
adam@2 249 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
adam@2 250 else
adam@2 251 s'
adam@2 252 in
adam@2 253 fromJ s' r
adam@2 254 end
adam@2 255 in
adam@2 256 if String.length s = 0 || String.sub s 0 <> #"{" then
adam@2 257 error <xml>JSON record doesn't begin with brace</xml>
adam@2 258 else
adam@2 259 let
adam@3 260 val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
adam@2 261 (@map0 [option] (fn [t ::_] => None) fl)
adam@2 262 in
adam@18 263 (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name =>
adam@18 264 case v of
adam@18 265 None => error <xml>Missing JSON object field {[name]}</xml>
adam@18 266 | Some v => v) fl r names, s')
adam@2 267 end
adam@2 268 end}
ezyang@22 269
ezyang@22 270 fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) =
ezyang@22 271 {ToJson = fn r => let val jnames = @map2 [json] [fn _ => string] [fn x => json x * string]
ezyang@22 272 (fn [t] (j : json t) (name : string) => (j, name)) fl jss names
ezyang@22 273 in @Variant.destrR [ident] [fn x => json x * string]
ezyang@22 274 (fn [p ::_] (v : p) (j : json p, name : string) =>
ezyang@22 275 "{" ^ escape name ^ ":" ^ j.ToJson v ^ "}") fl r jnames
ezyang@22 276 end,
ezyang@22 277 FromJson = fn s =>
ezyang@22 278 if String.length s = 0 || String.sub s 0 <> #"{" then
ezyang@22 279 error <xml>JSON variant doesn't begin with brace</xml>
ezyang@22 280 else
ezyang@22 281 let
ezyang@23 282 val (name, s') = unescape (skipSpaces (String.suffix s 1))
ezyang@22 283 val s' = skipSpaces s'
ezyang@22 284 val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
ezyang@22 285 error <xml>No colon after JSON object field name</xml>
ezyang@22 286 else
ezyang@22 287 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
ezyang@22 288
ezyang@22 289 val (r, s') = (@foldR2 [json] [fn _ => string]
ezyang@22 290 [fn ts => ts' :: {Type} -> [ts ~ ts'] => variant (ts ++ ts') * string]
ezyang@22 291 (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name'
ezyang@22 292 (acc : ts' :: {Type} -> [rest ~ ts'] => variant (rest ++ ts') * string) [fwd ::_] [[nm = t] ++ rest ~ fwd] =>
ezyang@22 293 if name = name'
ezyang@22 294 then
ezyang@22 295 let val (v, s') = j.FromJson s'
ezyang@22 296 in (make [nm] v, s')
ezyang@22 297 end
ezyang@22 298 else acc [fwd ++ [nm = t]]
ezyang@22 299 )
ezyang@22 300 (fn [fwd ::_] [[] ~ fwd] => error <xml>Unknown JSON object variant name {[name]}</xml>)
ezyang@22 301 fl jss names) [[]] !
ezyang@22 302
ezyang@22 303 val s' = skipSpaces s'
ezyang@22 304 val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
ezyang@22 305 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
ezyang@22 306 else
ezyang@22 307 s'
ezyang@22 308 in
ezyang@22 309 if String.length s' = 0 then
ezyang@22 310 error <xml>JSON object doesn't end in brace</xml>
ezyang@22 311 else if String.sub s' 0 = #"}" then
ezyang@22 312 (r, String.substring s' {Start = 1, Len = String.length s' - 1})
ezyang@22 313 else error <xml>Junk after JSON value in object</xml>
ezyang@22 314 end
ezyang@22 315 }
ezyang@22 316
ezyang@22 317 val json_unit : json unit = json_record {} {}
ezyang@23 318
ezyang@23 319 functor Recursive (M : sig
ezyang@23 320 con t :: Type -> Type
ezyang@23 321 val json_t : a ::: Type -> json a -> json (t a)
ezyang@23 322 end) = struct
ezyang@23 323 open M
ezyang@23 324
ezyang@23 325 datatype r = Rec of t r
ezyang@23 326
ezyang@23 327 fun rTo (Rec x) = (json_t {ToJson = rTo,
ezyang@23 328 FromJson = fn _ => error <xml>Tried to FromJson in ToJson!</xml>}).ToJson x
ezyang@23 329
ezyang@23 330 fun rFrom s =
ezyang@23 331 let
ezyang@23 332 val (x, s') = (json_t {ToJson = fn _ => error <xml>Tried to ToJson in FromJson!</xml>,
ezyang@23 333 FromJson = rFrom}).FromJson s
ezyang@23 334 in
ezyang@23 335 (Rec x, s')
ezyang@23 336 end
ezyang@23 337
ezyang@23 338 val json_r = {ToJson = rTo, FromJson = rFrom}
ezyang@23 339 end