From f0c60c01bb078da639efd3aaf33bc2f0ff996169 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 26 Aug 2016 19:26:49 -0400 Subject: Import Json module from old Meta library (thanks to Edward Z. Yang for code contributions) --- lib/ur/json.ur | 345 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 345 insertions(+) create mode 100644 lib/ur/json.ur (limited to 'lib/ur/json.ur') diff --git a/lib/ur/json.ur b/lib/ur/json.ur new file mode 100644 index 00000000..bd74f299 --- /dev/null +++ b/lib/ur/json.ur @@ -0,0 +1,345 @@ +con 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) : string -> a * string = j.FromJson + +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 + fun esc s = + case s of + "" => "\"" + | _ => + let + val ch = String.sub s 0 + in + (if ch = #"\"" || ch = #"\\" then + "\\" ^ String.str ch + else + String.str ch) ^ esc (String.suffix s 1) + end + in + "\"" ^ esc s + 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_option [a] (j : json a) : json (option a) = + {ToJson = fn v => case v of + None => "null" + | Some v => j.ToJson v, + FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then + (None, String.substring s {Start = 4, Len = String.length s - 4}) + else + let + val (v, s') = j.FromJson s + in + (Some v, s') + end} + +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 + +fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts = + {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string] + (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc => + escape name ^ ":" ^ j.ToJson v ^ (case acc of + "" => "" + | acc => "," ^ acc)) + "" fl jss names r ^ "}", + FromJson = fn s => + let + fun fromJ s (r : $(map option ts)) : $(map option ts) * string = + if String.length s = 0 then + error JSON object doesn't end in brace + else if String.sub s 0 = #"}" then + (r, String.substring s {Start = 1, Len = String.length s - 1}) + else let + val (name, s') = unescape s + val s' = skipSpaces s' + val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then + error No colon after JSON object field name + else + skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1}) + + val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string] + (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r => + if name = name' then + let + val (v, s') = j.FromJson s' + in + (r -- nm ++ {nm = Some v}, s') + end + else + let + val (r', s') = acc (r -- nm) + in + (r' ++ {nm = r.nm}, s') + end) + (fn _ => error Unknown JSON object field name {[name]}) + fl jss names r + + val s' = skipSpaces s' + val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then + skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1}) + else + s' + in + fromJ s' r + end + in + if String.length s = 0 || String.sub s 0 <> #"{" then + error JSON record doesn't begin with brace + else + let + val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1})) + (@map0 [option] (fn [t ::_] => None) fl) + in + (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name => + case v of + None => error Missing JSON object field {[name]} + | Some v => v) fl r names, s') + end + end} + +fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] + (f : p :: K -> f p -> fr p -> t) + [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = + match v + (@Top.mp [fr] [fn p => f p -> t] + (fn [p] (m : fr p) (v : f p) => f [p] v m) + fl r) + +fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) = + {ToJson = fn r => let val jnames = @map2 [json] [fn _ => string] [fn x => json x * string] + (fn [t] (j : json t) (name : string) => (j, name)) fl jss names + in @destrR [ident] [fn x => json x * string] + (fn [p ::_] (v : p) (j : json p, name : string) => + "{" ^ escape name ^ ":" ^ j.ToJson v ^ "}") fl r jnames + end, + FromJson = fn s => + if String.length s = 0 || String.sub s 0 <> #"{" then + error JSON variant doesn't begin with brace + else + let + val (name, s') = unescape (skipSpaces (String.suffix s 1)) + val s' = skipSpaces s' + val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then + error No colon after JSON object field name + else + skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1}) + + val (r, s') = (@foldR2 [json] [fn _ => string] + [fn ts => ts' :: {Type} -> [ts ~ ts'] => variant (ts ++ ts') * string] + (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name' + (acc : ts' :: {Type} -> [rest ~ ts'] => variant (rest ++ ts') * string) [fwd ::_] [[nm = t] ++ rest ~ fwd] => + if name = name' + then + let val (v, s') = j.FromJson s' + in (make [nm] v, s') + end + else acc [fwd ++ [nm = t]] + ) + (fn [fwd ::_] [[] ~ fwd] => error Unknown JSON object variant name {[name]}) + fl jss names) [[]] ! + + val s' = skipSpaces s' + val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then + skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1}) + else + s' + in + if String.length s' = 0 then + error JSON object doesn't end in brace + else if String.sub s' 0 = #"}" then + (r, String.substring s' {Start = 1, Len = String.length s' - 1}) + else error Junk after JSON value in object + end + } + +val json_unit : json unit = json_record {} {} + +functor Recursive (M : sig + con t :: Type -> Type + val json_t : a ::: Type -> json a -> json (t a) + end) = struct + open M + + datatype r = Rec of t r + + fun rTo (Rec x) = (json_t {ToJson = rTo, + FromJson = fn _ => error Tried to FromJson in ToJson!}).ToJson x + + fun rFrom s = + let + val (x, s') = (json_t {ToJson = fn _ => error Tried to ToJson in FromJson!, + FromJson = rFrom}).FromJson s + in + (Rec x, s') + end + + val json_r = {ToJson = rTo, FromJson = rFrom} +end -- cgit v1.2.3 From de0a0f3c917f66646d1982281fae750c49f261d6 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 27 Aug 2016 10:51:38 -0400 Subject: Json: parse records with extra fields --- lib/ur/json.ur | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) (limited to 'lib/ur/json.ur') diff --git a/lib/ur/json.ur b/lib/ur/json.ur index bd74f299..9288a6dd 100644 --- a/lib/ur/json.ur +++ b/lib/ur/json.ur @@ -203,6 +203,48 @@ fun json_list [a] (j : json a) : json (list a) = FromJson = fromJ} end +fun skipOne s = + let + fun skipOne s dquote squote brace bracket = + if String.length s = 0 then + s + else + let + val ch = String.sub s 0 + val rest = String.suffix s 1 + in + case ch of + #"\"" => skipOne rest (not dquote) squote brace bracket + | #"'" => skipOne rest dquote (not squote) brace bracket + | #"\\" => if String.length s >= 2 then + skipOne (String.suffix s 2) dquote squote brace bracket + else + "" + | #"{" => skipOne rest dquote squote (brace + 1) bracket + | #"}" => if brace = 0 then + s + else + skipOne rest dquote squote (brace - 1) bracket + + | #"[" => skipOne rest dquote squote brace (bracket + 1) + | #"]" => + if bracket = 0 then + s + else + skipOne rest dquote squote brace (bracket - 1) + + | #"," => + if not dquote && not squote && brace = 0 && bracket = 0 then + s + else + skipOne rest dquote squote brace bracket + + | _ => skipOne rest dquote squote brace bracket + end + in + skipOne s False False 0 0 + end + fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts = {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string] (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc => @@ -239,7 +281,7 @@ fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : in (r' ++ {nm = r.nm}, s') end) - (fn _ => error Unknown JSON object field name {[name]}) + (fn r => (r, skipOne s')) fl jss names r val s' = skipSpaces s' -- cgit v1.2.3