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
(case ch of
#"\n" => "\\n"
| #"\r" => "\\r"
| #"\t" => "\\t"
| #"\"" => "\\\""
| #"\'" => "\\\'"
| #"\\" => "\\\\"
| x => 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
(case String.sub s (i+1) of
#"n" => "\n"
| #"r" => "\r"
| #"t" => "\t"
| #"\"" => "\""
| #"\'" => "\'"
| #"\\" => "\\"
| x => error JSON unescape: Bad escape char: {[x]})
^
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 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 =>
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 r => (r, skipOne s'))
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