Mercurial > meta

annotate json.ur @ 3:189245a3c075

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wikipedia JSON example working
author Adam Chlipala <adam@chlipala.net>
date Thu, 02 Dec 2010 12:17:51 -0500
parents 478524b9d23a
children 8f7396495045
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
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
adam@1 193
adam@1 194 fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
adam@1 195 {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [id] [fn _ => string]
adam@1 196 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
adam@1 197 escape name ^ ":" ^ j.ToJson v ^ (case acc of
adam@1 198 "" => ""
adam@1 199 | _ => "," ^ acc))
adam@1 200 "" fl jss names r ^ "}",
adam@2 201 FromJson = fn s =>
adam@2 202 let
adam@2 203 fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
adam@2 204 if String.length s = 0 then
adam@2 205 error <xml>JSON object doesn't end in brace</xml>
adam@2 206 else if String.sub s 0 = #"}" then
adam@2 207 (r, String.substring s {Start = 1, Len = String.length s - 1})
adam@2 208 else let
adam@2 209 val (name, s') = unescape s
adam@2 210 val s' = skipSpaces s'
adam@2 211 val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
adam@2 212 error <xml>No colon after JSON object field naem</xml>
adam@2 213 else
adam@2 214 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
adam@2 215
adam@2 216 val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string]
adam@2 217 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r =>
adam@2 218 if name = name' then
adam@2 219 let
adam@2 220 val (v, s') = j.FromJson s'
adam@2 221 in
adam@2 222 (r -- nm ++ {nm = Some v}, s')
adam@2 223 end
adam@2 224 else
adam@2 225 let
adam@2 226 val (r', s') = acc (r -- nm)
adam@2 227 in
adam@2 228 (r' ++ {nm = r.nm}, s')
adam@2 229 end)
adam@2 230 (fn _ => error <xml>Unknown JSON object field name {[name]}</xml>)
adam@2 231 fl jss names r
adam@2 232
adam@2 233 val s' = skipSpaces s'
adam@2 234 val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
adam@2 235 skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
adam@2 236 else
adam@2 237 s'
adam@2 238 in
adam@2 239 fromJ s' r
adam@2 240 end
adam@2 241 in
adam@2 242 if String.length s = 0 || String.sub s 0 <> #"{" then
adam@2 243 error <xml>JSON record doesn't begin with brace</xml>
adam@2 244 else
adam@2 245 let
adam@3 246 val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
adam@2 247 (@map0 [option] (fn [t ::_] => None) fl)
adam@2 248 in
adam@2 249 (@map2 [option] [fn _ => string] [id] (fn [t] (v : option t) name =>
adam@2 250 case v of
adam@2 251 None => error <xml>Missing JSON object field {[name]}</xml>
adam@2 252 | Some v => v) fl r names, s')
adam@2 253 end
adam@2 254 end}