summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/basis.urs11
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml87
-rw-r--r--src/elaborate.sml61
-rw-r--r--src/monoize.sml37
-rw-r--r--src/urweb.grm14
-rw-r--r--src/urweb.lex1
-rw-r--r--tests/join.ur3
8 files changed, 181 insertions, 35 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index a81ba30a..a67d007a 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -235,6 +235,17 @@ val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
-> sql_exp (tabs1 ++ tabs2) [] [] bool
-> sql_from_items (tabs1 ++ tabs2)
+class nullify :: Type -> Type -> Type
+val nullify_option : t ::: Type -> nullify (option t) (option t)
+val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
+
+val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
+ -> [tabs1 ~ tabs2]
+ => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
+ -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+ -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
+ -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
+
val sql_query1 : tables ::: {{Type}}
-> grouped ::: {{Type}}
-> selectedFields ::: {{Type}}
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 4b927a16..1621722f 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -71,7 +71,7 @@ signature ELAB_ENV = sig
val pushClass : env -> int -> env
val isClass : env -> Elab.con -> bool
- val resolveClass : env -> Elab.con -> Elab.exp option
+ val resolveClass : (Elab.con -> Elab.con) -> env -> Elab.con -> Elab.exp option
val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list
val pushERel : env -> string -> Elab.con -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 62a310f2..7b20a700 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -507,6 +507,8 @@ fun unifyCons rs =
(CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2)
| (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2)
+ | (CUnif _, _) => ()
+
| (c1', CRel n2) =>
if n2 < d then
case c1' of
@@ -587,7 +589,56 @@ fun unifySubst (rs : con list) =
| (d, _) => d}
0
-fun resolveClass (env : env) =
+fun postUnify x =
+ let
+ fun unify (c1, c2) =
+ case (#1 c1, #1 c2) of
+ (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2)
+ | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2)
+
+ | (CUnif (_, _, _, r), _) => r := SOME c2
+
+ | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2))
+ | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2))
+ | (TRecord c1, TRecord c2) => unify (c1, c2)
+ | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
+ (unify (a1, a2); unify (b1, b2); unify (c1, c2))
+
+ | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
+ | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
+ | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
+ if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
+ | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2))
+ | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2))
+
+ | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2)
+ | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2))
+ | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2)
+
+ | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
+
+ | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
+ (unifyKinds (k1, k2);
+ ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2)
+ handle ListPair.UnequalLengths => raise Unify)
+ | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2))
+ | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
+
+ | (CUnit, CUnit) => ()
+
+ | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2)
+ handle ListPair.UnequalLengths => raise Unify)
+ | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2);
+ if n1 = n2 then () else raise Unify)
+
+ | _ => raise Unify
+ in
+ unify x
+ end
+
+fun postUnifies x = (postUnify x; true) handle Unify => false
+
+fun resolveClass (hnorm : con -> con) (env : env) =
let
fun resolve c =
let
@@ -608,7 +659,8 @@ fun resolveClass (env : env) =
let
val eos = map (resolve o unifySubst rs) cs
in
- if List.exists (not o Option.isSome) eos then
+ if List.exists (not o Option.isSome) eos
+ orelse not (postUnifies (c, unifySubst rs c')) then
tryRules rules'
else
let
@@ -634,9 +686,34 @@ fun resolveClass (env : env) =
tryGrounds (#ground class)
end
in
- case class_head_in c of
- SOME f => doHead f
- | _ => NONE
+ case #1 c of
+ TRecord c =>
+ (case #1 (hnorm c) of
+ CRecord (_, xts) =>
+ let
+ fun resolver (xts, acc) =
+ case xts of
+ [] => SOME (ERecord acc, #2 c)
+ | (x, t) :: xts =>
+ let
+ val t = hnorm t
+
+ val t = case t of
+ (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
+ | _ => t
+ in
+ case resolve t of
+ NONE => NONE
+ | SOME e => resolver (xts, (x, e, t) :: acc)
+ end
+ in
+ resolver (xts, [])
+ end
+ | _ => NONE)
+ | _ =>
+ case class_head_in c of
+ SOME f => doHead f
+ | _ => NONE
end
in
resolve
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ea4c28bd..709871da 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1131,26 +1131,35 @@
| (L'.TFun (dom, ran), _) =>
let
fun default () = (e, t, [])
+
+ fun isInstance () =
+ if infer <> L.TypesOnly then
+ let
+ val r = ref NONE
+ val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
+ in
+ (e, t, TypeClass (env, dom, r, loc) :: gs)
+ end
+ else
+ default ()
+
+ fun hasInstance c =
+ case #1 (hnormCon env c) of
+ L'.CApp (cl, x) =>
+ let
+ val cl = hnormCon env cl
+ in
+ isClassOrFolder env cl
+ end
+ | L'.TRecord c => U.Con.exists {kind = fn _ => false,
+ con = fn c =>
+ E.isClass env (hnormCon env (c, loc))} c
+ | _ => false
in
- case #1 (hnormCon env dom) of
- L'.CApp (cl, x) =>
- let
- val cl = hnormCon env cl
- in
- if infer <> L.TypesOnly then
- if isClassOrFolder env cl then
- let
- val r = ref NONE
- val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
- in
- (e, t, TypeClass (env, dom, r, loc) :: gs)
- end
- else
- default ()
- else
- default ()
- end
- | _ => default ()
+ if hasInstance dom then
+ isInstance ()
+ else
+ default ()
end
| (L'.TDisjoint (r1, r2, t'), loc) =>
if infer <> L.TypesOnly then
@@ -3638,7 +3647,7 @@ fun elabFile basis topStr topSgn env file =
let
val c = normClassKey env c
in
- case E.resolveClass env c of
+ case E.resolveClass (hnormCon env) env c of
SOME e => r := SOME e
| NONE => expError env (Unresolvable (loc, c))
end) gs
@@ -3688,11 +3697,6 @@ fun elabFile basis topStr topSgn env file =
if ErrorMsg.anyErrors () then
()
else
- app (fn f => f ()) (!checks);
-
- if ErrorMsg.anyErrors () then
- ()
- else
app (fn Disjoint (loc, env, denv, c1, c2) =>
(case D.prove env denv (c1, c2, loc) of
[] => ()
@@ -3708,7 +3712,7 @@ fun elabFile basis topStr topSgn env file =
val c = normClassKey env c
in
- case E.resolveClass env c of
+ case E.resolveClass (hnormCon env) env c of
SOME e => r := SOME e
| NONE =>
case #1 (hnormCon env c) of
@@ -3747,6 +3751,11 @@ fun elabFile basis topStr topSgn env file =
| _ => default ()
end) gs;
+ if ErrorMsg.anyErrors () then
+ ()
+ else
+ app (fn f => f ()) (!checks);
+
(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
:: ds
@ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
diff --git a/src/monoize.sml b/src/monoize.sml
index 98a32492..1a502e51 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -189,6 +189,8 @@ fun monoType env =
(L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc)
| L.CApp ((L.CFfi ("Basis", "sql_injectable"), _), t) =>
(L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc)
+ | L.CApp ((L.CApp ((L.CFfi ("Basis", "nullify"), _), _), _), _) =>
+ (L'.TRecord [], loc)
| L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_unary"), _), _), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_binary"), _), _), _), _), _), _) =>
@@ -581,6 +583,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
((L'.ERecord [("Lt", lt, (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc)),
("Le", le, (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc))],
loc), fm)
+
+ fun outerRec xts =
+ (L'.TRecord (map (fn ((L.CName x, _), (L.CRecord (_, xts), _)) =>
+ (x, (L'.TRecord (map (fn (x', _) => (x, (L'.TRecord [], loc))) xts), loc))
+ | (x, all as (_, loc)) =>
+ (E.errorAt loc "Unsupported record field constructor";
+ Print.eprefaces' [("Name", CorePrint.p_con env x),
+ ("Constructor", CorePrint.p_con env all)];
+ ("", dummyTyp))) xts), loc)
in
case e of
L.EPrim p => ((L'.EPrim p, loc), fm)
@@ -1702,6 +1713,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
+ | L.ECApp ((L.EFfi ("Basis", "nullify_option"), _), _) =>
+ ((L'.ERecord [], loc), fm)
+ | L.ECApp ((L.EFfi ("Basis", "nullify_prim"), _), _) =>
+ ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc),
+ (L'.ERecord [], loc)), loc),
+ fm)
+
| L.ECApp ((L.EFfi ("Basis", "sql_subset"), _), _) =>
((L'.ERecord [], loc), fm)
| L.ECApp ((L.EFfi ("Basis", "sql_subset_all"), _), _) =>
@@ -1744,6 +1762,25 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
(L'.EPrim (Prim.String ")"), loc)]), loc)), loc)), loc),
fm)
end
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_left_join"), _), _), _), (L.CRecord (_, right), _)) =>
+ let
+ val s = (L'.TFfi ("Basis", "string"), loc)
+ in
+ ((L'.EAbs ("_", outerRec right,
+ (L'.TFun (s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc)), loc),
+ (L'.EAbs ("tab1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc),
+ (L'.EAbs ("tab2", s, (L'.TFun (s, s), loc),
+ (L'.EAbs ("on", s, s,
+ strcat [(L'.EPrim (Prim.String "("), loc),
+ (L'.ERel 2, loc),
+ (L'.EPrim (Prim.String " LEFT JOIN "), loc),
+ (L'.ERel 1, loc),
+ (L'.EPrim (Prim.String " ON "), loc),
+ (L'.ERel 0, loc),
+ (L'.EPrim (Prim.String ")"), loc)]),
+ loc)), loc)), loc)), loc),
+ fm)
+ end
| L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_order_by_Nil"), _), _), _), _) =>
((L'.EPrim (Prim.String ""), loc), fm)
diff --git a/src/urweb.grm b/src/urweb.grm
index 723ed8b1..c1f0b1ca 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -213,7 +213,7 @@ datatype attr = Class of exp | Normal of con * exp
| CURRENT_TIMESTAMP
| NE | LT | LE | GT | GE
| CCONSTRAINT | UNIQUE | CHECK | PRIMARY | FOREIGN | KEY | ON | NO | ACTION | RESTRICT | CASCADE | REFERENCES
- | JOIN | INNER | CROSS
+ | JOIN | INNER | CROSS | LEFT
%nonterm
file of decl list
@@ -361,7 +361,7 @@ datatype attr = Class of exp | Normal of con * exp
%nonassoc DCOLON TCOLON
%left UNION INTERSECT EXCEPT
%right COMMA
-%right JOIN INNER CROSS
+%right JOIN INNER CROSS LEFT
%right OR
%right CAND
%nonassoc EQ NE LT LE GT GE IS
@@ -1468,6 +1468,16 @@ fitem : table' ([#1 table'], #2 table')
(#1 fitem1 @ #1 fitem2,
(EApp (e, tru), loc))
end)
+ | fitem LEFT JOIN fitem ON sqlexp (let
+ val loc = s (fitem1left, sqlexpright)
+
+ val e = (EVar (["Basis"], "sql_left_join", Infer), loc)
+ val e = (EApp (e, #2 fitem1), loc)
+ val e = (EApp (e, #2 fitem2), loc)
+ in
+ (#1 fitem1 @ #1 fitem2,
+ (EApp (e, sqlexp), loc))
+ end)
tname : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
| LBRACE cexp RBRACE (cexp)
diff --git a/src/urweb.lex b/src/urweb.lex
index c20e9206..517054b3 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -341,6 +341,7 @@ notags = [^<{\n]+;
<INITIAL> "JOIN" => (Tokens.JOIN (pos yypos, pos yypos + size yytext));
<INITIAL> "INNER" => (Tokens.INNER (pos yypos, pos yypos + size yytext));
<INITIAL> "CROSS" => (Tokens.CROSS (pos yypos, pos yypos + size yytext));
+<INITIAL> "LEFT" => (Tokens.LEFT (pos yypos, pos yypos + size yytext));
<INITIAL> "UNION" => (Tokens.UNION (pos yypos, pos yypos + size yytext));
<INITIAL> "INTERSECT" => (Tokens.INTERSECT (pos yypos, pos yypos + size yytext));
diff --git a/tests/join.ur b/tests/join.ur
index 30a0e744..74f49eec 100644
--- a/tests/join.ur
+++ b/tests/join.ur
@@ -1,8 +1,9 @@
-table t : { A : int }
+table t : { A : int, B : string, C : option string }
fun main () =
r <- oneRow (SELECT * FROM t);
r <- oneRow (SELECT * FROM t AS T1, t AS T2);
r <- oneRow (SELECT * FROM t AS T1 CROSS JOIN t AS T2);
r <- oneRow (SELECT * FROM t AS T1 JOIN t AS T2 ON T1.A = T2.A);
+ r <- oneRow (SELECT * FROM t AS T1 LEFT JOIN t AS T2 ON T1.A = T2.A);
return <xml/>
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 02:08:13 +0000