Merge branch 'upstream' into dfsg_clean20200209+dfsgdfsg_clean

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. *)