summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2019-10-11 17:18:02 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2019-10-11 17:18:02 -0400
commitb71c7b9ec4580326772a212fbe011322ae1ac063 (patch)
tree82fa78cde166dafa9e0fa5bd3441aa758682bb25
parentf7b684dbdae9229a69258a7e575395af120d2654 (diff)
JSON instance for times, based on RFC 3339 (because Google APIs use it)
-rw-r--r--lib/ur/json.ur47
-rw-r--r--lib/ur/json.urs1
2 files changed, 48 insertions, 0 deletions
diff --git a/lib/ur/json.ur b/lib/ur/json.ur
index 0865ab33..58822d4b 100644
--- a/lib/ur/json.ur
+++ b/lib/ur/json.ur
@@ -145,6 +145,53 @@ fun unescape s =
val json_string = {ToJson = escape,
FromJson = unescape}
+fun rfc3339_out s =
+ let
+ val out1 = timef "%Y-%m-%dT%H:%M:%S%z" s
+ val len = String.length out1
+ in
+ if len < 2 then
+ error <xml>timef output too short</xml>
+ else
+ String.substring out1 {Start = 0, Len = len - 2} ^ ":"
+ ^ String.suffix out1 (len - 2)
+ end
+
+fun rfc3339_in s =
+ case String.split s #"T" of
+ None => error <xml>Invalid RFC 3339 string "{[s]}"</xml>
+ | Some (date, time) =>
+ case String.msplit {Haystack = time, Needle = "Z+-"} of
+ None => error <xml>Invalid RFC 3339 string "{[s]}"</xml>
+ | Some (time, sep, rest) =>
+ let
+ val t = case readUtc (date ^ " " ^ time) of
+ None => error <xml>Invalid RFC 3339 string "{[s]}"</xml>
+ | Some t => t
+
+ fun withOffset multiplier =
+ case String.split rest #":" of
+ None => error <xml>Invalid RFC 3339 string "{[s]}"</xml>
+ | Some (h, m) =>
+ case (read h, read m) of
+ (Some h, Some m) => addSeconds t (multiplier * 60 * (60 * h + m))
+ | _ => error <xml>Invalid RFC 3339 string "{[s]}"</xml>
+ in
+ case sep of
+ #"Z" => t
+ | #"+" => withOffset (-1)
+ | #"-" => withOffset 1
+ | _ => error <xml>msplit returns impossible separator</xml>
+ end
+
+val json_time = {ToJson = fn tm => escape (rfc3339_out tm),
+ FromJson = fn s =>
+ let
+ val (v, s') = unescape s
+ in
+ (rfc3339_in v, s')
+ end}
+
fun numIn [a] (_ : read a) s : a * string =
let
val len = String.length s
diff --git a/lib/ur/json.urs b/lib/ur/json.urs
index 56f5a897..7b83d03d 100644
--- a/lib/ur/json.urs
+++ b/lib/ur/json.urs
@@ -13,6 +13,7 @@ val json_string : json string
val json_int : json int
val json_float : json float
val json_bool : json bool
+val json_time : json time
val json_option : a ::: Type -> json a -> json (option a)
val json_list : a ::: Type -> json a -> json (list a)