queryX

10 files changed, 65 insertions, 33 deletions

diff --git a/lib/top.ur b/lib/top.ur
index af009242..7c18da21 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -26,3 +26,11 @@ fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
                         [[nm] ~ rest] =>
                         fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
                 <xml></xml>
+
+fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) =
+        [tables ~ exps] =>
+        fn (f : $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+                -> xml ctx [] []) =>
+        query q
+                (fn fs acc => return <xml>{acc}{f fs}</xml>)
+                <xml></xml>
diff --git a/lib/top.urs b/lib/top.urs
index 0e211373..b124caa2 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -19,3 +19,9 @@ val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
                 -> tf1 t -> tf2 t -> xml ctx [] [])
         -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
+
+val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
+        -> sql_query tables exps -> tables ~ exps
+        -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+                -> xml ctx [] [])
+        -> transaction (xml ctx [] [])
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 5602c8d2..8dff81e7 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -314,7 +314,7 @@ and hnormCon (env, denv) c =
     in
         case c of
             CDisjoint cs => doDisj cs
-          | TDisjoint cs => doDisj cs
+          | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
           | _ => (cAll, [])
     end
 
diff --git a/src/elab.sml b/src/elab.sml
index 8e77d773..6fcb857a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -46,10 +46,14 @@ datatype explicitness =
          Explicit
        | Implicit
 
+datatype auto_instantiate =
+         Instantiate
+       | LeaveAlone
+
 datatype con' =
          TFun of con * con
        | TCFun of explicitness * string * kind * con
-       | TDisjoint of con * con * con
+       | TDisjoint of auto_instantiate * con * con * con
        | TRecord of con
 
        | CRel of int
diff --git a/src/elab_print.sml b/src/elab_print.sml
index f56f57dc..bb1c2a85 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -80,15 +80,15 @@ fun p_con' par env (c, _) =
                                                 string "->",
                                                 space,
                                                 p_con (E.pushCRel env x k) c])
-      | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
-                                                    space,
-                                                    string "~",
-                                                    space,
-                                                    p_con env c2,
-                                                    space,
-                                                    string "->",
-                                                    space,
-                                                    p_con env c3])
+      | TDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                       space,
+                                                       string "~",
+                                                       space,
+                                                       p_con env c2,
+                                                       space,
+                                                       string "->",
+                                                       space,
+                                                       p_con env c3])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
                                                          box [p_name env x,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6f56d9c9..242ffdbc 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -119,14 +119,14 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (TCFun (e, x, k', c'), loc)))
-              | TDisjoint (c1, c2, c3) =>
+              | TDisjoint (ai, c1, c2, c3) =>
                 S.bind2 (mfc ctx c1,
                       fn c1' =>
                          S.bind2 (mfc ctx c2,
                               fn c2' =>
                                  S.map2 (mfc ctx c3,
                                          fn c3' =>
-                                            (TDisjoint (c1', c2', c3'), loc))))
+                                            (TDisjoint (ai, c1', c2', c3'), loc))))
               | TRecord c =>
                 S.map2 (mfc ctx c,
                         fn c' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2b548969..e6e5453d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -239,7 +239,7 @@ fun elabCon (env, denv) (c, loc) =
             checkKind env c1' k1 (L'.KRecord ku1, loc);
             checkKind env c2' k2 (L'.KRecord ku2, loc);
 
-            ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
+            ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
         end
       | L.TRecord c =>
         let
@@ -824,7 +824,7 @@ and guessFold (env, denv) (c1, c2, gs, ex) =
 
 and unifyCons' (env, denv) c1 c2 =
     case (#1 c1, #1 c2) of
-        (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) =>
+        (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) =>
         let
             val gs1 = unifyCons' (env, denv) x1 x2
             val gs2 = unifyCons' (env, denv) y1 y2
@@ -983,7 +983,8 @@ fun foldType (dom, loc) =
                                     (L'.TCFun (L'.Explicit, "v", dom,
                                                (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
                                                           (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
-                                                                    (L'.TDisjoint ((L'.CRecord
+                                                                    (L'.TDisjoint (L'.Instantiate,
+                                                                                   (L'.CRecord
                                                                                         ((L'.KUnit, loc),
                                                                                          [((L'.CRel 2, loc),
                                                                                            (L'.CUnit, loc))]), loc),
@@ -1523,7 +1524,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 checkKind env c1' k1 (L'.KRecord ku1, loc);
                 checkKind env c2' k2 (L'.KRecord ku2, loc);
 
-                (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
+                (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
             end
 
           | L.ERecord xes =>
@@ -2661,6 +2662,17 @@ fun wildifyStr env (str, sgn) =
            | _ => str)
       | _ => str
 
+val makeInstantiable =
+    let
+        fun kind k = k
+        fun con c =
+            case c of
+                L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c)
+              | _ => c
+    in
+        U.Con.map {kind = kind, con = con}
+    end
+
 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
     let
         (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
@@ -2792,6 +2804,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
                     val gs3 = checkCon (env, denv) e' et c'
                     val (c', gs4) = normClassConstraint (env, denv) c'
                     val (env', n) = E.pushENamed env x c'
+                    val c' = makeInstantiable c'
                 in
                     (*prefaces "DVal" [("x", Print.PD.string x),
                                        ("c'", p_con env c')];*)
@@ -2828,6 +2841,8 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
                                                               val (e', et, gs1) = elabExp (env, denv) e
                                                                                   
                                                               val gs2 = checkCon (env, denv) e' et c'
+
+                                                              val c' = makeInstantiable c'
                                                           in
                                                               if allowable e then
                                                                   ()
diff --git a/src/explify.sml b/src/explify.sml
index 142ddfcb..76ef9551 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -49,7 +49,7 @@ fun explifyCon (c, loc) =
     case c of
         L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
       | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
-      | L.TDisjoint (_, _, c) => explifyCon c
+      | L.TDisjoint (_, _, _, c) => explifyCon c
       | L.TRecord c => (L'.TRecord (explifyCon c), loc)
 
       | L.CRel n => (L'.CRel n, loc)
diff --git a/src/mono_opt.sml b/src/mono_opt.sml
index 64eef7e3..997bb9be 100644
--- a/src/mono_opt.sml
+++ b/src/mono_opt.sml
@@ -293,6 +293,14 @@ fun exp e =
         else
             e
 
+      | EWrite (EQuery {exps, tables, state, query,
+                        initial = (EPrim (Prim.String ""), _),
+                        body = (EStrcat ((ERel 0, _), e'), _)}, loc) =>
+        EQuery {exps = exps, tables = tables, query = query,
+                state = (TRecord [], loc),
+                initial = (ERecord [], loc),
+                body = (optExp (EWrite e', loc), loc)}
+
       | _ => e
 
 and optExp e = #1 (U.Exp.map {typ = typ, exp = exp} e)
diff --git a/tests/crud.ur b/tests/crud.ur
index 95d2d4b9..7f0fc71c 100644
--- a/tests/crud.ur
+++ b/tests/crud.ur
@@ -14,10 +14,9 @@ end) = struct
 open constraints M
 val tab = M.tab
 
-fun list () =
-        rows <- query (SELECT * FROM tab AS T)
-                (fn (fs : {T : $([Id = int] ++ M.cols)}) acc => return <body>
-                        {acc}
+fun main () : transaction page =
+        rows <- queryX (SELECT * FROM tab AS T)
+                (fn (fs : {T : $([Id = int] ++ M.cols)}) => <body>
                         <tr>
                                 <td>{txt _ fs.T.Id}</td>
                                 {foldTRX2 [idT] [colMeta'] [tr]
@@ -28,13 +27,13 @@ fun list () =
                                                 </tr>)
                                         [M.cols] (fs.T -- #Id) M.cols}
                         </tr>
-                </body>) <body></body>;
+                </body>);
         return <html><head>
-                <title>List</title>
+                <title>{cdata M.title}</title>
 
                 </head><body>
 
-                <h1>List</h1>
+                <h1>{cdata M.title}</h1>
 
                 <table border={1}>
                 <tr> <th>ID</th> </tr>
@@ -42,12 +41,4 @@ fun list () =
                 </table>
         </body></html>
 
-fun main () : transaction page = return <html><head>
-        <title>{cdata M.title}</title>
-        </head><body>
-        <h1>{cdata M.title}</h1>
-
-        <li> <a link={list ()}>List all rows</a></li>
-</body></html>
-
 end