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(-) 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