summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs26
-rw-r--r--lib/ur/datetime.ur3
-rw-r--r--lib/ur/datetime.urs1
-rw-r--r--lib/ur/json.ur190
-rw-r--r--lib/ur/json.urs10
-rw-r--r--lib/ur/list.ur87
-rw-r--r--lib/ur/list.urs16
-rw-r--r--lib/ur/listPair.ur26
-rw-r--r--lib/ur/listPair.urs5
-rw-r--r--lib/ur/option.ur5
-rw-r--r--lib/ur/option.urs2
-rw-r--r--lib/ur/top.ur21
-rw-r--r--lib/ur/top.urs16
13 files changed, 386 insertions, 22 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 66cc0e50..9d6e56d5 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -79,6 +79,9 @@ val toupper : char -> char
val ord : char -> int
val chr : int -> char
+val iscodepoint : int -> bool
+val issingle : char -> bool
+
(** String operations *)
val strlen : string -> int
@@ -92,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
@@ -274,6 +278,8 @@ con serialized :: Type -> Type
val serialize : t ::: Type -> t -> serialized t
val deserialize : t ::: Type -> serialized t -> t
val sql_serialized : t ::: Type -> sql_injectable_prim (serialized t)
+val unsafeSerializedToString : t ::: Type -> serialized t -> string
+val unsafeSerializedFromString : t ::: Type -> string -> serialized t
con primary_key :: {Type} -> {{Unit}} -> Type
val no_primary_key : fs ::: {Type} -> primary_key fs []
@@ -566,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
@@ -620,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
@@ -803,6 +816,7 @@ type id
val fresh : transaction id
val giveFocus : id -> transaction unit
val show_id : show id
+val anchorUrl : id -> url
val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ [Dyn]] => unit
-> tag [Signal = signal (xml ([Dyn] ++ ctx) use bind)] ([Dyn] ++ ctx) [] use bind
@@ -830,7 +844,7 @@ val meta : unit -> tag [Nam = meta, Content = string, Id = id] head [] [] []
datatype mouseButton = Left | Right | Middle
-type mouseEvent = { ScreenX : int, ScreenY : int, ClientX : int, ClientY : int,
+type mouseEvent = { ScreenX : int, ScreenY : int, ClientX : int, ClientY : int, OffsetX : int, OffsetY : int,
CtrlKey : bool, ShiftKey : bool, AltKey : bool, MetaKey : bool,
Button : mouseButton }
@@ -1014,6 +1028,8 @@ val checkMime : string -> option mimeType
val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
val blobSize : blob -> int
val textBlob : string -> blob
+val textOfBlob : blob -> option string
+(* Returns [Some] exactly when the blob contains no zero bytes. *)
type postBody
val postType : postBody -> string
@@ -1069,7 +1085,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 817ec16e..1222cdbf 100644
--- a/lib/ur/json.ur
+++ b/lib/ur/json.ur
@@ -51,9 +51,7 @@ fun escape s =
| #"\r" => "\\r"
| #"\t" => "\\t"
| #"\"" => "\\\""
- | #"\'" => "\\\'"
| #"\\" => "\\\\"
- | #"/" => "\\/"
| x => String.str ch
) ^ esc (String.suffix s 1)
end
@@ -61,64 +59,143 @@ 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"
| #"\"" => "\""
- | #"\'" => "\'"
| #"\\" => "\\"
| #"/" => "/"
| 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 time = case String.split time #"." of
+ None => time
+ | Some (time, _) => time
+
+ 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
@@ -261,6 +338,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))
+ withRequired 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
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 95d6fbc8..1eb7626a 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -31,6 +31,16 @@ fun foldl [a] [b] (f : a -> b -> b) =
foldl'
end
+fun foldli [a] [b] (f : int -> a -> b -> b) =
+ let
+ fun foldli' i acc ls =
+ case ls of
+ [] => acc
+ | x :: ls => foldli' (i + 1) (f i x acc) ls
+ in
+ foldli' 0
+ end
+
val rev = fn [a] =>
let
fun rev' acc (ls : list a) =
@@ -101,6 +111,16 @@ fun mp [a] [b] f =
mp' []
end
+fun mapConcat [a] [b] f =
+ let
+ fun mapConcat' acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => mapConcat' (revAppend (f x) acc) ls
+ in
+ mapConcat' []
+ end
+
fun mapi [a] [b] f =
let
fun mp' n acc ls =
@@ -153,6 +173,26 @@ fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
mapM' []
end
+fun mapConcatM [m] (_ : monad m) [a] [b] f =
+ let
+ fun mapConcatM' acc ls =
+ case ls of
+ [] => return (rev acc)
+ | x :: ls' => ls <- f x; mapConcatM' (revAppend ls acc) ls'
+ in
+ mapConcatM' []
+ end
+
+fun mapMi [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
+ let
+ fun mapM' i acc ls =
+ case ls of
+ [] => return (rev acc)
+ | x :: ls => x' <- f i x; mapM' (i + 1) (x' :: acc) ls
+ in
+ mapM' 0 []
+ end
+
fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
let
fun mapPartialM' acc ls =
@@ -283,6 +323,20 @@ fun search [a] [b] f =
search'
end
+fun searchM [m] (_ : monad m) [a] [b] f =
+ let
+ fun search' ls =
+ case ls of
+ [] => return None
+ | x :: ls =>
+ o <- f x;
+ case o of
+ None => search' ls
+ | v => return v
+ in
+ search'
+ end
+
fun foldlM [m] (_ : monad m) [a] [b] f =
let
fun foldlM' acc ls =
@@ -319,7 +373,7 @@ fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
filterM' []
end
-fun all [m] f =
+fun all [a] f =
let
fun all' ls =
case ls of
@@ -329,6 +383,21 @@ fun all [m] f =
all'
end
+fun allM [m] (_ : monad m) [a] f =
+ let
+ fun all' ls =
+ case ls of
+ [] => return True
+ | x :: ls =>
+ b <- f x;
+ if b then
+ all' ls
+ else
+ return False
+ in
+ all'
+ end
+
fun app [m] (_ : monad m) [a] f =
let
fun app' ls =
@@ -454,6 +523,22 @@ fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
None => (x, y) :: ls
| Some _ => ls
+fun assocAddSorted [a] [b] (_ : eq a) (_ : ord a) (x : a) (y : b) (ls : t (a * b)) =
+ let
+ fun aas (ls : t (a * b)) (acc : t (a * b)) =
+ case ls of
+ [] => rev ((x, y) :: acc)
+ | (x', y') :: ls' =>
+ if x' = x then
+ revAppend ((x, y) :: acc) ls'
+ else if x < x' then
+ revAppend ((x, y) :: acc) ls
+ else
+ aas ls' ((x', y') :: acc)
+ in
+ aas ls []
+ end
+
fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
= @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
x :: xs) [] fl
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index fe730152..f81f38a4 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -7,6 +7,8 @@ val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
val foldlAbort : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
val foldlMapAbort : a ::: Type -> b ::: Type -> c ::: Type
-> (a -> b -> option (c * b)) -> b -> t a -> option (t c * b)
+val foldli : a ::: Type -> b ::: Type
+ -> (int -> a -> b -> b) -> b -> t a -> b
val foldr : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
@@ -20,6 +22,10 @@ val append : a ::: Type -> t a -> t a -> t a
val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val mapConcat : a ::: Type -> b ::: Type -> (a -> t b) -> t a -> t b
+
+val mapConcatM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (t b)) -> t a -> m (t b)
+
val mapPartial : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
val mapi : a ::: Type -> b ::: Type -> (int -> a -> b) -> t a -> t b
@@ -31,6 +37,9 @@ val mapXi : a ::: Type -> ctx ::: {Unit} -> (int -> a -> xml ctx [] []) -> t a -
val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
-> (a -> m b) -> t a -> m (t b)
+val mapMi : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (int -> a -> m b) -> t a -> m (t b)
+
val mapPartialM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (option b)) -> t a -> m (t b)
val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit}
@@ -64,8 +73,12 @@ val findM : m ::: (Type -> Type) -> monad m -> a ::: Type -> (a -> m bool) -> t
val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
+val searchM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (option b)) -> t a -> m (option b)
+
val all : a ::: Type -> (a -> bool) -> t a -> bool
+val allM : m ::: (Type -> Type) -> monad m -> a ::: Type -> (a -> m bool) -> t a -> m bool
+
val app : m ::: (Type -> Type) -> monad m -> a ::: Type
-> (a -> m unit) -> t a -> m unit
@@ -104,6 +117,9 @@ val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
val assocAdd : a ::: Type -> b ::: Type -> eq a -> a -> b -> t (a * b) -> t (a * b)
+val assocAddSorted : a ::: Type -> b ::: Type -> eq a -> ord a -> a -> b -> t (a * b) -> t (a * b)
+(* Assume the list is already sorted in ascending order and maintain that ordering. *)
+
(** Converting records to lists *)
val recToList : a ::: Type -> r ::: {Unit} -> folder r -> $(mapU a r) -> t a
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index 94b92872..52c73cd8 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -40,7 +40,31 @@ fun mp [a] [b] [c] (f : a -> b -> c) =
case (ls1, ls2) of
([], []) => []
| (x1 :: ls1, x2 :: ls2) => f x1 x2 :: map' ls1 ls2
- | _ => error <xml>ListPair.map2: Unequal list lengths</xml>
+ | _ => error <xml>ListPair.mp: Unequal list lengths</xml>
in
map'
end
+
+fun mapM [m] (_ : monad m) [a] [b] [c] (f : a -> b -> m c) =
+ let
+ fun mapM' ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => return []
+ | (x1 :: ls1, x2 :: ls2) =>
+ y <- f x1 x2;
+ ls <- mapM' ls1 ls2;
+ return (y :: ls)
+ | _ => error <xml>ListPair.mapM: Unequal list lengths</xml>
+ in
+ mapM'
+ end
+
+fun unzip [a] [b] (ls : list (a * b)) : list a * list b =
+ let
+ fun unzip' ls ls1 ls2 =
+ case ls of
+ [] => (List.rev ls1, List.rev ls2)
+ | (x1, x2) :: ls => unzip' ls (x1 :: ls1) (x2 :: ls2)
+ in
+ unzip' ls [] []
+ end
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
index b473e226..91d8807d 100644
--- a/lib/ur/listPair.urs
+++ b/lib/ur/listPair.urs
@@ -8,3 +8,8 @@ val all : a ::: Type -> b ::: Type -> (a -> b -> bool) -> list a -> list b -> bo
val mp : a ::: Type -> b ::: Type -> c ::: Type
-> (a -> b -> c) -> list a -> list b -> list c
+
+val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> m c) -> list a -> list b -> m (list c)
+
+val unzip : a ::: Type -> b ::: Type -> list (a * b) -> list a * list b
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index baa08466..dd186161 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -59,3 +59,8 @@ fun unsafeGet [a] (o : option a) =
case o of
None => error <xml>Option.unsafeGet: encountered None</xml>
| Some v => v
+
+fun mapM [m] (_ : monad m) [a] [b] (f : a -> m b) (x : t a) : m (t b) =
+ case x of
+ None => return None
+ | Some y => z <- f y; return (Some z)
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index c30c40e7..705c0313 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -14,3 +14,5 @@ val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
val get : a ::: Type -> a -> option a -> a
val unsafeGet : a ::: Type -> option a -> a
+
+val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m b) -> t a -> m (t b)
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 02567917..92f1ecdd 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -172,6 +172,17 @@ fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {
f [nm] [t] [rest] r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
(fn _ _ _ => i)
+fun foldR4 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf4 :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tf4 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf4 r) -> tr r]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> _ -> _ -> tr rest) r1 r2 r3 r4 =>
+ f [nm] [t] [rest] r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
+ (fn _ _ _ _ => i)
+
fun mapUX [tf :: Type] [ctx :: {Unit}]
(f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
@@foldR [fn _ => tf] [fn _ => xml ctx [] []]
@@ -224,6 +235,16 @@ fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {
<xml>{f [nm] [t] [rest] r1 r2 r3}{acc}</xml>)
<xml/>
+fun mapX4 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf4 :: K -> Type] [ctx :: {Unit}]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tf4 t -> xml ctx [] []) =
+ @@foldR4 [tf1] [tf2] [tf3] [tf4] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ r1 r2 r3 r4 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2 r3 r4}{acc}</xml>)
+ <xml/>
+
fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
(f : $fs -> state -> transaction state) (i : state) =
query q (fn r => f r.t) i
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index ec098955..a367a989 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -121,6 +121,15 @@ val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type
-> tr []
-> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
+(* Fold (generalized safe zip) along four heterogenously-typed records *)
+val foldR4 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf4 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tf4 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf4 r) -> tr r
+
(* Generate some XML by mapping over a uniformly-typed record *)
val mapUX : tf :: Type -> ctx :: {Unit}
-> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
@@ -159,6 +168,13 @@ val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
-> r ::: {K} -> folder r
-> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
+val mapX4 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf4 :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tf4 t -> xml ctx [] [])
+ -> r ::: {K} -> folder r
+ -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf4 r) -> xml ctx [] []
+
(* Note that the next two functions return elements in the _reverse_ of the natural order!
* Such a choice interacts well with the time complexity of standard list operations.
* It's easy to regain the natural order by inverting a query's 'ORDER BY' condition. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 09:49:07 +0000