Mercurial > urweb
changeset 750:059074c8d2fc
LEFT JOIN
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 28 Apr 2009 11:05:28 -0400 |
| parents | 16bfd9e244cd |
| children | f95d652086cd |
| files | lib/ur/basis.urs src/elab_env.sig src/elab_env.sml src/elaborate.sml src/monoize.sml src/urweb.grm src/urweb.lex tests/join.ur |
| diffstat | 8 files changed, 181 insertions(+), 35 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Apr 28 10:11:56 2009 -0400 +++ b/lib/ur/basis.urs Tue Apr 28 11:05:28 2009 -0400 @@ -235,6 +235,17 @@ -> 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}}
--- a/src/elab_env.sig Tue Apr 28 10:11:56 2009 -0400 +++ b/src/elab_env.sig Tue Apr 28 11:05:28 2009 -0400 @@ -71,7 +71,7 @@ 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
--- a/src/elab_env.sml Tue Apr 28 10:11:56 2009 -0400 +++ b/src/elab_env.sml Tue Apr 28 11:05:28 2009 -0400 @@ -507,6 +507,8 @@ (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 @@ | (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 @@ 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 @@ 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
--- a/src/elaborate.sml Tue Apr 28 10:11:56 2009 -0400 +++ b/src/elaborate.sml Tue Apr 28 11:05:28 2009 -0400 @@ -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 @@ 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 @@ 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 @@ 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 @@ | _ => 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)
--- a/src/monoize.sml Tue Apr 28 10:11:56 2009 -0400 +++ b/src/monoize.sml Tue Apr 28 11:05:28 2009 -0400 @@ -189,6 +189,8 @@ (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 @@ ((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 @@ 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 @@ (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)
--- a/src/urweb.grm Tue Apr 28 10:11:56 2009 -0400 +++ b/src/urweb.grm Tue Apr 28 11:05:28 2009 -0400 @@ -213,7 +213,7 @@ | 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 @@ %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 @@ (#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)
--- a/src/urweb.lex Tue Apr 28 10:11:56 2009 -0400 +++ b/src/urweb.lex Tue Apr 28 11:05:28 2009 -0400 @@ -341,6 +341,7 @@ <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));
--- a/tests/join.ur Tue Apr 28 10:11:56 2009 -0400 +++ b/tests/join.ur Tue Apr 28 11:05:28 2009 -0400 @@ -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/>