summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/js/urweb.js12
-rw-r--r--lib/ur/basis.urs16
-rw-r--r--lib/ur/datetime.ur3
-rw-r--r--lib/ur/datetime.urs1
-rw-r--r--lib/ur/json.ur183
-rw-r--r--lib/ur/json.urs10
6 files changed, 208 insertions, 17 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 66d427c8..59e5ad2c 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -2135,6 +2135,16 @@ function active(s) {
}
}
+function listen(s, onchange) {
+ var x = document.createElement("script");
+ x.dead = false;
+ x.signal = s;
+ x.sources = null;
+ x.closures = null;
+ x.recreate = onchange;
+ populate(x);
+}
+
function input(x, s, recreate, type, name) {
if (name) x.name = name;
if (type) x.type = type;
@@ -3270,7 +3280,7 @@ function confrm(s) {
}
function currentUrl() {
- return window.location;
+ return window.location.toString();
}
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index be13c684..dda48d2b 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -95,6 +95,7 @@ val strsindex : string -> string -> option int
val strcspn : string -> string -> int
val substring : string -> int -> int -> string
val str1 : char -> string
+val ofUnicode : int -> string
class show
val show : t ::: Type -> show t -> t -> string
@@ -571,9 +572,6 @@ val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
val sql_mod : sql_binary int int int
val sql_eq : t ::: Type -> sql_binary t t bool
-(* Note that the semantics of this operator on nullable types are different than for standard SQL!
- * Instead, we do it the sane way, where [NULL = NULL]. *)
-
val sql_ne : t ::: Type -> sql_binary t t bool
val sql_lt : t ::: Type -> sql_binary t t bool
val sql_le : t ::: Type -> sql_binary t t bool
@@ -625,6 +623,16 @@ val sql_known : t ::: Type -> sql_ufunc t bool
val sql_lower : sql_ufunc string string
val sql_upper : sql_ufunc string string
+con sql_bfunc :: Type -> Type -> Type -> Type
+val sql_bfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> dom1 ::: Type -> dom2 ::: Type -> ran ::: Type
+ -> sql_bfunc dom1 dom2 ran
+ -> sql_exp tables agg exps dom1
+ -> sql_exp tables agg exps dom2
+ -> sql_exp tables agg exps ran
+val sql_similarity : sql_bfunc string string float
+(* Only supported by Postgres for now, via the pg_trgm module *)
+
val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-> sql_injectable_prim t
-> sql_exp tables agg exps t
@@ -1076,7 +1084,7 @@ val ctel : ctext
val ccolor : ctext
val cnumber : cformTag ([Source = source (option float), Min = float, Max = float, Step = float, Size = int] ++ boxAttrs ++ inputAttrs) []
-val crange : cformTag ([Source = source (option float), Min = float, Max = float, Size = int] ++ boxAttrs ++ inputAttrs) []
+val crange : cformTag ([Source = source (option float), Min = float, Max = float, Size = int, Step = float] ++ boxAttrs ++ inputAttrs) []
val cdate : cformTag ([Source = source string, Min = string, Max = string, Size = int] ++ boxAttrs ++ inputAttrs) []
val cdatetime : cformTag ([Source = source string, Min = string, Max = string, Size = int] ++ boxAttrs ++ inputAttrs) []
val cdatetime_local : cformTag ([Source = source string, Min = string, Max = string, Size = int] ++ boxAttrs ++ inputAttrs) []
diff --git a/lib/ur/datetime.ur b/lib/ur/datetime.ur
index 9aeab291..99fd5a7d 100644
--- a/lib/ur/datetime.ur
+++ b/lib/ur/datetime.ur
@@ -88,7 +88,8 @@ fun intToMonth i = case i of
| n => error <xml>Invalid month number {[n]}</xml>
val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
-
+val ord_month = mkOrd {Lt = fn a b => monthToInt a < monthToInt b,
+ Le = fn a b => monthToInt a <= monthToInt b}
fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
dt.Hour dt.Minute dt.Second
diff --git a/lib/ur/datetime.urs b/lib/ur/datetime.urs
index 972f86bf..f8460443 100644
--- a/lib/ur/datetime.urs
+++ b/lib/ur/datetime.urs
@@ -20,6 +20,7 @@ val show_day_of_week : show day_of_week
val show_month : show month
val eq_day_of_week : eq day_of_week
val eq_month : eq month
+val ord_month : ord month
val dayOfWeekToInt : day_of_week -> int
val intToDayOfWeek : int -> day_of_week
val monthToInt : month -> int
diff --git a/lib/ur/json.ur b/lib/ur/json.ur
index 05406739..58822d4b 100644
--- a/lib/ur/json.ur
+++ b/lib/ur/json.ur
@@ -59,42 +59,71 @@ fun escape s =
"\"" ^ esc s
end
+fun unhex ch =
+ if Char.isDigit ch then
+ Char.toInt ch - Char.toInt #"0"
+ else if Char.isXdigit ch then
+ if Char.isUpper ch then
+ 10 + (Char.toInt ch - Char.toInt #"A")
+ else
+ 10 + (Char.toInt ch - Char.toInt #"a")
+ else
+ error <xml>Invalid hexadecimal digit "{[ch]}"</xml>
+
fun unescape s =
let
val len = String.length s
- fun findEnd i =
+ fun findEnd i s =
if i >= len then
error <xml>JSON unescape: string ends before quote: {[s]}</xml>
else
let
- val ch = String.sub s i
+ val ch = String.sub s 0
in
case ch of
#"\"" => i
| #"\\" =>
if i+1 >= len then
error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+ else if String.sub s 1 = #"u" then
+ if i+5 >= len then
+ error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+ else
+ findEnd (i+6) (String.suffix s 6)
else
- findEnd (i+2)
- | _ => findEnd (i+1)
+ findEnd (i+2) (String.suffix s 2)
+ | _ => findEnd (i+1) (String.suffix s 1)
end
- val last = findEnd 1
+ val last = findEnd 1 (String.suffix s 1)
- fun unesc i =
+ fun unesc i s =
if i >= last then
""
else
let
- val ch = String.sub s i
+ val ch = String.sub s 0
in
case ch of
#"\\" =>
if i+1 >= len then
error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+ else if String.sub s 1 = #"u" then
+ if i+5 >= len then
+ error <xml>JSON unescape: Unicode ends early</xml>
+ else
+ let
+ val n =
+ unhex (String.sub s 2) * (256*16)
+ + unhex (String.sub s 3) * 256
+ + unhex (String.sub s 4) * 16
+ + unhex (String.sub s 5)
+ in
+ ofUnicode n ^ unesc (i+6) (String.suffix s 6)
+ end
else
- (case String.sub s (i+1) of
+ (case String.sub s 1 of
#"n" => "\n"
| #"r" => "\r"
| #"t" => "\t"
@@ -103,19 +132,66 @@ fun unescape s =
| #"/" => "/"
| x => error <xml>JSON unescape: Bad escape char: {[x]}</xml>)
^
- unesc (i+2)
- | _ => String.str ch ^ unesc (i+1)
+ unesc (i+2) (String.suffix s 2)
+ | _ => String.str ch ^ unesc (i+1) (String.suffix s 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})
+ (unesc 1 (String.suffix s 1), String.suffix s (last+1))
end
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
@@ -258,6 +334,91 @@ fun skipOne s =
skipOne s False False 0 0
end
+fun json_record_withOptional [ts ::: {Type}] [ots ::: {Type}] [ts ~ ots]
+ (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts))
+ (ofl : folder ots) (ojss : $(map json ots)) (onames : $(map (fn _ => string) ots)): json $(ts ++ map option ots) =
+ {ToJson = fn r =>
+ let
+ val withRequired =
+ @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 --- _)
+
+ val withOptional =
+ @foldR3 [json] [fn _ => string] [option] [fn _ => string]
+ (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
+ case v of
+ None => acc
+ | Some v =>
+ escape name ^ ":" ^ j.ToJson v ^ (case acc of
+ "" => ""
+ | acc => "," ^ acc))
+ "" ofl ojss onames (r --- _)
+ in
+ "{" ^ withOptional ^ "}"
+ end,
+ FromJson = fn s =>
+ let
+ fun fromJ s (r : $(map option (ts ++ ots))) : $(map option (ts ++ ots)) * 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 r => (r, skipOne s'))
+ (@Folder.concat ! fl ofl) (jss ++ ojss) (names ++ onames) 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) (@Folder.concat ! fl ofl))
+ 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
+ ++ (r --- _), s')
+ end
+end}
+
+(* At the moment, the below code is largely copied and pasted from the last
+ * definition, because otherwise the compiler fails to inline enough for
+ * compilation to succeed. *)
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 =>
diff --git a/lib/ur/json.urs b/lib/ur/json.urs
index b4bd6350..ad49a40f 100644
--- a/lib/ur/json.urs
+++ b/lib/ur/json.urs
@@ -13,10 +13,20 @@ 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)
+(* By the way, time formatting follows RFC 3339, and we expose the more
+ * primitive formatting functions here. *)
+val rfc3339_out : time -> string
+val rfc3339_in : string -> time
+
val json_record : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json $ts
+val json_record_withOptional : ts ::: {Type} -> ots ::: {Type} -> [ts ~ ots]
+ => folder ts -> $(map json ts) -> $(map (fn _ => string) ts)
+ -> folder ots -> $(map json ots) -> $(map (fn _ => string) ots)
+ -> json $(ts ++ map option ots)
val json_variant : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json (variant ts)
val json_unit : json unit