summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/top.ur8
-rw-r--r--lib/top.urs6
-rw-r--r--src/disjoint.sml2
-rw-r--r--src/elab.sml6
-rw-r--r--src/elab_print.sml18
-rw-r--r--src/elab_util.sml4
-rw-r--r--src/elaborate.sml23
-rw-r--r--src/explify.sml2
-rw-r--r--src/mono_opt.sml8
-rw-r--r--tests/crud.ur21
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 03:32:21 +0000