diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-11-20 10:45:22 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-11-20 10:45:22 -0500 |
commit | 61c8fdf76c28f65b8b483f68d2d1f5597fdf58ce (patch) | |
tree | e61d2420230a82c747cb1a257ecb129179d95019 /lib/ur | |
parent | f21f9e29d19a8b241c1d6d790904001fdf384d59 (diff) |
queryL1 and List.sort
Diffstat (limited to 'lib/ur')
-rw-r--r-- | lib/ur/list.ur | 28 | ||||
-rw-r--r-- | lib/ur/list.urs | 2 | ||||
-rw-r--r-- | lib/ur/top.ur | 5 | ||||
-rw-r--r-- | lib/ur/top.urs | 4 |
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) |