# HG changeset patch # User Adam Chlipala # Date 1291306257 18000 # Node ID 63697ef80a2c9cfffbc0399a6ee33aeddd59faf9 JSON, minus records and nulls diff -r 000000000000 -r 63697ef80a2c .hgignore --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/.hgignore Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,6 @@ +syntax: glob + +*~ + +*.exe +*.sql diff -r 000000000000 -r 63697ef80a2c json.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/json.ur Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,192 @@ +class json a = {ToJson : a -> string, + FromJson : string -> a * string} + +fun mkJson [a] (x : {ToJson : a -> string, + FromJson : string -> a * string}) = x + +fun skipSpaces s = + let + val len = String.length s + + fun skip i = + if i >= len then + "" + else + let + val ch = String.sub s i + in + if Char.isSpace ch then + skip (i+1) + else + String.substring s {Start = i, Len = len-i} + end + in + skip 0 + end + +fun toJson [a] (j : json a) : a -> string = j.ToJson + +fun fromJson [a] (j : json a) (s : string) : a = + let + val (v, s') = j.FromJson (skipSpaces s) + in + if String.all Char.isSpace s' then + v + else + error Extra content at end of JSON record: {[s']} + end + +fun escape s = + let + val len = String.length s + + fun esc i = + if i >= len then + "\"" + else + let + val ch = String.sub s i + in + (if ch = #"\"" || ch = #"\\" then + "\\" ^ String.str ch + else + String.str ch) ^ esc (i+1) + end + in + "\"" ^ esc 0 + end + +fun unescape s = + let + val len = String.length s + + fun findEnd i = + if i >= len then + error JSON unescape: string ends before quote: {[s]} + else + let + val ch = String.sub s i + in + case ch of + #"\"" => i + | #"\\" => + if i+1 >= len then + error JSON unescape: Bad escape sequence: {[s]} + else + findEnd (i+2) + | _ => findEnd (i+1) + end + + val last = findEnd 1 + + fun unesc i = + if i >= last then + "" + else + let + val ch = String.sub s i + in + case ch of + #"\\" => + if i+1 >= len then + error JSON unescape: Bad escape sequence: {[s]} + else + String.str (String.sub s (i+1)) ^ unesc (i+2) + | _ => String.str ch ^ unesc (i+1) + end + in + if len = 0 || String.sub s 0 <> #"\"" then + error JSON unescape: String doesn't start with double quote: {[s]} + else + (unesc 1, String.substring s {Start = last+1, Len = len-last-1}) + end + +val json_string = {ToJson = escape, + FromJson = unescape} + +fun numIn [a] (_ : read a) s : a * string = + let + val len = String.length s + + fun findEnd i = + if i >= len then + i + else + let + val ch = String.sub s i + in + if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then + findEnd (i+1) + else + i + end + + val last = findEnd 0 + in + (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last}) + end + +fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show, + FromJson = numIn} + +val json_int = json_num +val json_float = json_num + +val json_bool = {ToJson = fn b => if b then "true" else "false", + FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then + (True, String.substring s {Start = 4, Len = String.length s - 4}) + else if String.isPrefix {Full = s, Prefix = "false"} then + (False, String.substring s {Start = 5, Len = String.length s - 5}) + else + error JSON: bad boolean string: {[s]}} + +fun json_list [a] (j : json a) : json (list a) = + let + fun toJ' (ls : list a) : string = + case ls of + [] => "" + | x :: ls => "," ^ toJson j x ^ toJ' ls + + fun toJ (x : list a) : string = + case x of + [] => "[]" + | x :: [] => "[" ^ toJson j x ^ "]" + | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]" + + fun fromJ (s : string) : list a * string = + let + fun fromJ' (s : string) : list a * string = + if String.length s = 0 then + error JSON list doesn't end with ']' + else + let + val ch = String.sub s 0 + in + case ch of + #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1}) + | _ => + let + val (x, s') = j.FromJson s + val s' = skipSpaces s' + val s' = if String.length s' = 0 then + error JSON list doesn't end with ']' + else if String.sub s' 0 = #"," then + skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1}) + else + s' + + val (ls, s'') = fromJ' s' + in + (x :: ls, s'') + end + end + in + if String.length s = 0 || String.sub s 0 <> #"[" then + error JSON list doesn't start with '[': {[s]} + else + fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1})) + end + in + {ToJson = toJ, + FromJson = fromJ} + end diff -r 000000000000 -r 63697ef80a2c json.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/json.urs Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,13 @@ +class json + +val toJson : a ::: Type -> json a -> a -> string +val fromJson : a ::: Type -> json a -> string -> a + +val mkJson : a ::: Type -> {ToJson : a -> string, + FromJson : string -> a * string} -> json a + +val json_string : json string +val json_int : json int +val json_float : json float +val json_bool : json bool +val json_list : a ::: Type -> json a -> json (list a) diff -r 000000000000 -r 63697ef80a2c meta.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/meta.urp Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,3 @@ +$/char +$/string +json diff -r 000000000000 -r 63697ef80a2c tests/testJson.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/testJson.ur Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,13 @@ +fun main () : transaction page = return + {[Json.toJson (1 :: 2 :: 8 :: [])]}
+ {[Json.fromJson "[1,2, 8]" : list int]} +
+ {[Json.toJson (1.2 :: 2.4 :: (-8.8) :: [])]}
+ {[Json.fromJson "[1.4,-2.7, 8.215506]" : list float]} +
+ {[Json.toJson ("hi" :: "bye" :: "tricky\\\" one!" :: [])]}
+ {[Json.fromJson "[\"abc\", \"\\\\whoa\"]" : list string]} +
+ {[Json.toJson (True :: False :: True :: [])]}
+ {[Json.fromJson "[true,false, true]" : list bool]} +
diff -r 000000000000 -r 63697ef80a2c tests/testJson.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/testJson.urp Thu Dec 02 11:10:57 2010 -0500 @@ -0,0 +1,5 @@ +library ../meta +rewrite all TestJson/* + +$/list +testJson