summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-01-20 12:43:12 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-01-20 12:43:12 -0500
commit93f37507d93bb10ed7f67074c62a478b31f151e3 (patch)
tree71ae95eb9c0a648b24d0a8cc703ed353d5472def /lib
parent6ec77d7dce5bbc965d0dc44545f3f15d8a9fb181 (diff)
queryXI and queryX1I
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/top.ur37
-rw-r--r--lib/ur/top.urs12
2 files changed, 49 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 0fdbae7a..1edca44e 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -255,6 +255,30 @@ fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Ty
(fn fs acc => return <xml>{acc}{f fs}</xml>)
<xml/>
+fun rev [a] (ls : list a) : list a =
+ let
+ fun rev' ls acc =
+ case ls of
+ [] => acc
+ | x :: ls => rev' ls (x :: acc)
+ in
+ rev' ls []
+ end
+
+fun queryXI [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp []) =
+ let
+ fun qxi ls i =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f i x}{qxi ls (i+1)}</xml>
+ in
+ ls <- queryL q;
+ return (qxi ls 0)
+ end
+
fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
(q : sql_query [] [] [nm = fs] [])
(f : $fs -> xml ctx inp []) =
@@ -262,6 +286,19 @@ fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
(fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
<xml/>
+fun queryX1I [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ (q : sql_query [] [] [nm = fs] [])
+ (f : int -> $fs -> xml ctx inp []) =
+ let
+ fun qx1i ls i =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f i x.nm}{qx1i ls (i+1)}</xml>
+ in
+ ls <- queryL q;
+ return (qx1i ls 0)
+ end
+
fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {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 ed3b4c14..0af3e09c 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -164,11 +164,23 @@ val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp :::
-> xml ctx inp [])
-> transaction (xml ctx inp [])
+val queryXI : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> (int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-> sql_query [] [] [nm = fs] []
-> ($fs -> xml ctx inp [])
-> transaction (xml ctx inp [])
+val queryX1I : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> (int -> $fs -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
-> [tables ~ exps] =>
sql_query [] [] tables exps