From 8956b5096cd268b6eb73040ede0688849084c5fe Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Thu, 25 Mar 2010 15:44:24 -0400
Subject: Subquery expressions

---
 lib/ur/top.ur | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'lib/ur/top.ur')

diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 617423db..ae6cb74a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -215,21 +215,21 @@ 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 query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] [])
+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
 
-fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [t = fs] [])
+fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] [])
             (f : $fs -> state -> state) (i : state) =
     query q (fn r s => return (f r.t s)) i
 
-fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) =
+fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) =
     query q
     (fn r ls => return (r :: ls))
     []
 
 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps)
+           [tables ~ exps] (q : sql_query [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> transaction unit) =
     query q
@@ -237,7 +237,7 @@ fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
           ()
 
 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps)
+           [tables ~ exps] (q : sql_query [] tables exps)
            (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                 -> xml ctx inp []) =
     query q
@@ -245,14 +245,14 @@ fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Ty
           <xml/>
 
 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            (q : sql_query [nm = fs] [])
+            (q : sql_query [] [nm = fs] [])
             (f : $fs -> xml ctx inp []) =
     query q
           (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
           <xml/>
 
 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-            [tables ~ exps] (q : sql_query tables exps)
+            [tables ~ exps] (q : sql_query [] tables exps)
             (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
                  -> transaction (xml ctx inp [])) =
     query q
@@ -262,7 +262,7 @@ fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {T
           <xml/>
 
 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [nm = fs] [])
+             (q : sql_query [] [nm = fs] [])
              (f : $fs -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -271,7 +271,7 @@ fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
           <xml/>
 
 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
-             (q : sql_query [] exps)
+             (q : sql_query [] [] exps)
              (f : $exps -> transaction (xml ctx inp [])) =
     query q
           (fn fs acc =>
@@ -281,42 +281,42 @@ fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
 
 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
             [tables ~ exps]
-            (q : sql_query tables exps) =
+            (q : sql_query [] tables exps) =
     query q
           (fn _ _ => return True)
           False
 
 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
                 [tables ~ exps]
-                (q : sql_query tables exps) =
+                (q : sql_query [] tables exps) =
     query q
           (fn fs _ => return (Some fs))
           None
 
-fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
+fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
-fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
+fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
     query q
           (fn fs _ => return (Some fs.nm))
           None
 
 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
-           [tables ~ exps] (q : sql_query tables exps) =
+           [tables ~ exps] (q : sql_query [] tables exps) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r)
 
-fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
+fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
               | Some r => r.nm)
 
-fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
+fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) =
     o <- oneOrNoRows q;
     return (case o of
                 None => error <xml>Query returned no rows</xml>
-- 
cgit v1.2.3