Import Json module from old Meta library (thanks to Edward Z. Yang for code contributions)

2 files changed, 376 insertions, 0 deletions

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 <xml>Extra content at end of JSON record: {[s']}</xml>
+    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 <xml>JSON unescape: string ends before quote: {[s]}</xml>
+            else
+                let
+                    val ch = String.sub s i
+                in
+                    case ch of
+                        #"\"" => i
+                      | #"\\" =>
+                        if i+1 >= len then
+                            error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+                        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 <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+                        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 <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
+        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 <xml>JSON: bad boolean string: {[s]}</xml>}
+
+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 <xml>JSON list doesn't end with ']'</xml>
+                    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 <xml>JSON list doesn't end with ']'</xml>
+                                             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 <xml>JSON list doesn't start with '[': {[s]}</xml>
+                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 <xml>JSON object doesn't end in brace</xml>
+                           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 <xml>No colon after JSON object field name</xml>
+                                            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 <xml>Unknown JSON object field name {[name]}</xml>)
+                                                  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 <xml>JSON record doesn't begin with brace</xml>
+                       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 <xml>Missing JSON object field {[name]}</xml>
+                                                                              | 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 <xml>JSON variant doesn't begin with brace</xml>
+                   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 <xml>No colon after JSON object field name</xml>
+                                    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 <xml>Unknown JSON object variant name {[name]}</xml>)
+                                            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 <xml>JSON object doesn't end in brace</xml>
+                           else if String.sub s' 0 = #"}" then
+                               (r, String.substring s' {Start = 1, Len = String.length s' - 1})
+                           else error <xml>Junk after JSON value in object</xml>
+                       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 <xml>Tried to FromJson in ToJson!</xml>}).ToJson x
+
+    fun rFrom s =
+        let
+            val (x, s') = (json_t {ToJson = fn _ => error <xml>Tried to ToJson in FromJson!</xml>,
+                                   FromJson = rFrom}).FromJson s
+        in
+            (Rec x, s')
+        end
+
+    val json_r = {ToJson = rTo, FromJson = rFrom}
+end
diff --git a/lib/ur/json.urs b/lib/ur/json.urs
new file mode 100644
index 00000000..b4bd6350
--- /dev/null
+++ b/lib/ur/json.urs
@@ -0,0 +1,31 @@
+(** The JSON text-based serialization format *)
+
+class json
+
+val toJson : a ::: Type -> json a -> a -> string
+val fromJson : a ::: Type -> json a -> string -> a
+val fromJson' : a ::: Type -> json a -> string -> a * string
+
+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_option : a ::: Type -> json a -> json (option a)
+val json_list : a ::: Type -> json a -> json (list a)
+
+val json_record : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json $ts
+val json_variant : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json (variant ts)
+
+val json_unit : json unit
+
+functor Recursive (M : sig
+                       con t :: Type -> Type
+                       val json_t : a ::: Type -> json a -> json (t a)
+                   end) : sig
+    datatype r = Rec of M.t r
+
+    val json_r : json r
+end