# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1290267922 18000
# Node ID 4172863d049df21725cf8619703cde41b20a8dc6
# Parent  add5ae41969e2a81b9235e3cb82700ba5240d0b7
queryL1 and List.sort

diff -r add5ae41969e -r 4172863d049d lib/ur/list.ur
--- a/lib/ur/list.ur	Sat Nov 20 09:48:03 2010 -0500
+++ b/lib/ur/list.ur	Sat Nov 20 10:45:22 2010 -0500
@@ -280,6 +280,34 @@
                 [];
     return (rev ls)
 
+fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
+    let
+        fun split ls acc1 acc2 =
+            case ls of
+                [] => (rev acc1, rev acc2)
+              | x :: [] => (rev (x :: acc1), rev acc2)
+              | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
+
+        fun merge ls1 ls2 acc =
+            case (ls1, ls2) of
+                ([], _) => revAppend acc ls2
+              | (_, []) => revAppend acc ls1
+              | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
+
+        fun sort' ls =
+            case ls of
+                [] => ls
+              | _ :: [] => ls
+              | _ =>
+                let
+                    val (ls1, ls2) = split ls [] []
+                in
+                    merge (sort' ls1) (sort' ls2) []
+                end
+    in
+        sort' ls
+    end
+
 fun assoc [a] [b] (_ : eq a) (x : a) =
     let
         fun assoc' (ls : list (a * b)) =
diff -r add5ae41969e -r 4172863d049d lib/ur/list.urs
--- a/lib/ur/list.urs	Sat Nov 20 09:48:03 2010 -0500
+++ b/lib/ur/list.urs	Sat Nov 20 10:45:22 2010 -0500
@@ -69,6 +69,8 @@
     -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t))
     -> transaction (list t)
 
+val sort : a ::: Type -> (a -> a -> bool) (* > predicate *) -> t a -> t a
+
 (** Association lists *)
 
 val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
diff -r add5ae41969e -r 4172863d049d lib/ur/top.ur
--- a/lib/ur/top.ur	Sat Nov 20 09:48:03 2010 -0500
+++ b/lib/ur/top.ur	Sat Nov 20 10:45:22 2010 -0500
@@ -228,6 +228,11 @@
     (fn r ls => return (r :: ls))
     []
 
+fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [t = fs] []) =
+    query q
+    (fn r ls => return (r.t :: ls))
+    []
+
 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
            [tables ~ exps] (q : sql_query [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
diff -r add5ae41969e -r 4172863d049d lib/ur/top.urs
--- a/lib/ur/top.urs	Sat Nov 20 09:48:03 2010 -0500
+++ b/lib/ur/top.urs	Sat Nov 20 10:45:22 2010 -0500
@@ -129,6 +129,10 @@
                   sql_query [] tables exps
                   -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
 
+val queryL1 : t ::: Name -> fs ::: {Type}
+              -> sql_query [] [t = fs] []
+              -> transaction (list $fs)
+
 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
              -> sql_query [] [t = fs] []
              -> ($fs -> state -> transaction state)