summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-11-20 10:45:22 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-11-20 10:45:22 -0500
commite85b176783c81cbbfbd35bbda989cd7703272378 (patch)
treee61d2420230a82c747cb1a257ecb129179d95019
parentaa6e63371697ca158bd9b1fe9e68ecbd59fbf72a (diff)
queryL1 and List.sort
-rw-r--r--lib/ur/list.ur28
-rw-r--r--lib/ur/list.urs2
-rw-r--r--lib/ur/top.ur5
-rw-r--r--lib/ur/top.urs4
4 files changed, 39 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index bb814714..71d8fa98 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -280,6 +280,34 @@ fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
[];
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 --git a/lib/ur/list.urs b/lib/ur/list.urs
index 7ce3c61f..a0cec8fb 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -69,6 +69,8 @@ val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
-> ($(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 --git a/lib/ur/top.ur b/lib/ur/top.ur
index ae6cb74a..32d06a43 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -228,6 +228,11 @@ fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) =
(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 --git a/lib/ur/top.urs b/lib/ur/top.urs
index 7ddc6bee..a18bf437 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -129,6 +129,10 @@ val queryL : tables ::: {{Type}} -> exps ::: {Type}
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)