Mercurial > urweb
changeset 207:cc68da3801bc
Non-star SELECT
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 14 Aug 2008 18:35:08 -0400 |
| parents | cb8493759a7b |
| children | 63a2f2322c1f |
| files | lib/basis.lig src/disjoint.sml src/elab.sml src/elab_ops.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/lacweb.grm src/source.sml src/source_print.sml tests/table.lac |
| diffstat | 11 files changed, 264 insertions(+), 45 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.lig Thu Aug 14 15:27:35 2008 -0400 +++ b/lib/basis.lig Thu Aug 14 18:35:08 2008 -0400 @@ -15,10 +15,12 @@ con sql_query :: {{Type}} -> Type -val sql_query : tables ::: {{Type}} - -> $(fold (fn nm => fn ts => fn acc => [nm] ~ acc => - [nm = sql_table ts] ++ acc) [] tables) - -> sql_query tables +val sql_query : tables :: {({Type} * {Type})} + -> $(fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => selected_unselected.1 ~ selected_unselected.2 => + [nm = sql_table (selected_unselected.1 ++ selected_unselected.2)] ++ acc) [] tables) + -> sql_query (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => [nm] ~ acc => + [nm = selected_unselected.1] ++ acc) [] tables) (** XML *)
--- a/src/disjoint.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/disjoint.sml Thu Aug 14 18:35:08 2008 -0400 @@ -30,7 +30,7 @@ open Elab open ElabOps -datatype piece = +datatype piece_fst = NameC of string | NameR of int | NameN of int @@ -39,6 +39,8 @@ | RowN of int | RowM of int * string list * string +type piece = piece_fst * int list + fun p2s p = case p of NameC s => "NameC(" ^ s ^ ")" @@ -55,20 +57,9 @@ type ord_key = piece -fun join (o1, o2) = - case o1 of - EQUAL => o2 () - | v => v +open Order -fun joinL f (os1, os2) = - case (os1, os2) of - (nil, nil) => EQUAL - | (nil, _) => LESS - | (h1 :: t1, h2 :: t2) => - join (f (h1, h2), fn () => joinL f (t1, t2)) - | (_ :: _, nil) => GREATER - -fun compare (p1, p2) = +fun compare' (p1, p2) = case (p1, p2) of (NameC s1, NameC s2) => String.compare (s1, s2) | (NameR n1, NameR n2) => Int.compare (n1, n2) @@ -102,6 +93,10 @@ | (RowN _, _) => LESS | (_, RowN _) => GREATER +fun compare ((p1, ns1), (p2, ns2)) = + join (compare' (p1, p2), + fn () => joinL Int.compare (ns1, ns2)) + end structure PS = BinarySetFn(PK) @@ -116,7 +111,7 @@ fun nameToRow (c, loc) = (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) -fun pieceToRow (p, loc) = +fun pieceToRow' (p, loc) = case p of NameC s => nameToRow (CName s, loc) | NameR n => nameToRow (CRel n, loc) @@ -126,16 +121,21 @@ | RowN n => (CNamed n, loc) | RowM (n, xs, x) => (CModProj (n, xs, x), loc) +fun pieceToRow ((p, ns), loc) = + foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns + datatype piece' = Piece of piece | Unknown of con -fun pieceEnter p = +fun pieceEnter' p = case p of NameR n => NameR (n + 1) | RowR n => RowR (n + 1) | _ => p +fun pieceEnter (p, n) = (pieceEnter' p, n) + fun enter denv = PM.foldli (fn (p, pset, denv') => PM.insert (denv', pieceEnter p, PS.map pieceEnter pset)) @@ -143,7 +143,7 @@ fun prove1 denv (p1, p2) = case (p1, p2) of - (NameC s1, NameC s2) => s1 <> s2 + ((NameC s1, _), (NameC s2, _)) => s1 <> s2 | _ => case PM.find (denv, p1) of NONE => false @@ -151,15 +151,29 @@ fun decomposeRow (env, denv) c = let + fun decomposeProj c = + let + val (c, gs) = hnormCon (env, denv) c + in + case #1 c of + CProj (c, n) => + let + val (c', ns, gs') = decomposeProj c + in + (c', ns @ [n], gs @ gs') + end + | _ => (c, [], gs) + end + fun decomposeName (c, (acc, gs)) = let - val (cAll as (c, _), gs') = hnormCon (env, denv) c + val (cAll as (c, _), ns, gs') = decomposeProj c val acc = case c of - CName s => Piece (NameC s) :: acc - | CRel n => Piece (NameR n) :: acc - | CNamed n => Piece (NameN n) :: acc - | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc + CName s => Piece (NameC s, ns) :: acc + | CRel n => Piece (NameR n, ns) :: acc + | CNamed n => Piece (NameN n, ns) :: acc + | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc | _ => Unknown cAll :: acc in (acc, gs' @ gs) @@ -167,15 +181,15 @@ fun decomposeRow (c, (acc, gs)) = let - val (cAll as (c, _), gs') = hnormCon (env, denv) c + val (cAll as (c, _), ns, gs') = decomposeProj c val gs = gs' @ gs in case c of CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs))) - | CRel n => (Piece (RowR n) :: acc, gs) - | CNamed n => (Piece (RowN n) :: acc, gs) - | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x)) :: acc, gs) + | CRel n => (Piece (RowR n, ns) :: acc, gs) + | CNamed n => (Piece (RowN n, ns) :: acc, gs) + | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) | _ => (Unknown cAll :: acc, gs) end in @@ -200,7 +214,7 @@ let val pset = Option.getOpt (PM.find (denv, p), PS.empty) val ps = case p of - NameC _ => List.filter (fn NameC _ => false | _ => true) ps + (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps | _ => ps val pset = PS.addList (pset, ps) in
--- a/src/elab.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/elab.sml Thu Aug 14 18:35:08 2008 -0400 @@ -35,6 +35,7 @@ | KName | KRecord of kind | KUnit + | KTuple of kind list | KError | KUnif of ErrorMsg.span * string * kind option ref @@ -66,6 +67,9 @@ | CUnit + | CTuple of con list + | CProj of con * int + | CError | CUnif of ErrorMsg.span * kind * string * con option ref
--- a/src/elab_ops.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/elab_ops.sml Thu Aug 14 18:35:08 2008 -0400 @@ -138,6 +138,11 @@ hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc) | _ => cAll) + | CProj (c, n) => + (case hnormCon env c of + (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1)) + | _ => cAll) + | _ => cAll end
--- a/src/elab_print.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/elab_print.sml Thu Aug 14 18:35:08 2008 -0400 @@ -49,6 +49,9 @@ | KName => string "Name" | KRecord k => box [string "{", p_kind k, string "}"] | KUnit => string "Unit" + | KTuple ks => box [string "(", + p_list_sep (box [space, string "*", space]) p_kind ks, + string ")"] | KError => string "<ERROR>" | KUnif (_, _, ref (SOME k)) => p_kind' par k @@ -177,6 +180,13 @@ | CUnit => string "()" + | CTuple cs => box [string "(", + p_list (p_con env) cs, + string ")"] + | CProj (c, n) => box [p_con env c, + string ".", + string (Int.toString n)] + | CError => string "<ERROR>" | CUnif (_, _, _, ref (SOME c)) => p_con' par env c | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
--- a/src/elab_util.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/elab_util.sml Thu Aug 14 18:35:08 2008 -0400 @@ -68,6 +68,11 @@ | KUnit => S.return2 kAll + | KTuple ks => + S.map2 (ListUtil.mapfold mfk ks, + fn ks' => + (KTuple ks', loc)) + | KError => S.return2 kAll | KUnif (_, _, ref (SOME k)) => mfk' k @@ -180,6 +185,16 @@ | CUnit => S.return2 cAll + | CTuple cs => + S.map2 (ListUtil.mapfold (mfc ctx) cs, + fn cs' => + (CTuple cs', loc)) + + | CProj (c, n) => + S.map2 (mfc ctx c, + fn c' => + (CProj (c', n), loc)) + | CError => S.return2 cAll | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll
--- a/src/elaborate.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/elaborate.sml Thu Aug 14 18:35:08 2008 -0400 @@ -86,6 +86,9 @@ unifyKinds' r1 r2) | (L'.KName, L'.KName) => () | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 + | (L'.KTuple ks1, L'.KTuple ks2) => + ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) + handle ListPair.UnequalLengths => err KIncompatible) | (L'.KError, _) => () | (_, L'.KError) => () @@ -125,6 +128,8 @@ | UnboundStrInCon of ErrorMsg.span * string | WrongKind of L'.con * L'.kind * L'.kind * kunify_error | DuplicateField of ErrorMsg.span * string + | ProjBounds of L'.con * int + | ProjMismatch of L'.con * L'.kind fun conError env err = case err of @@ -142,6 +147,14 @@ kunifyError kerr) | DuplicateField (loc, s) => ErrorMsg.errorAt loc ("Duplicate record field " ^ s) + | ProjBounds (c, n) => + (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection"; + eprefaces' [("Constructor", p_con env c), + ("Index", Print.PD.string (Int.toString n))]) + | ProjMismatch (c, k) => + (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; + eprefaces' [("Constructor", p_con env c), + ("Kind", p_kind k)]) fun checkKind env c k1 k2 = unifyKinds k1 k2 @@ -212,6 +225,7 @@ | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (elabKind k), loc) | L.KUnit => (L'.KUnit, loc) + | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) | L.KWild => kunif loc fun foldKind (dom, ran, loc)= @@ -222,6 +236,11 @@ (L'.KArrow ((L'.KRecord dom, loc), ran), loc)), loc)), loc) +fun hnormKind (kAll as (k, _)) = + case k of + L'.KUnif (_, _, ref (SOME k)) => hnormKind k + | _ => kAll + fun elabCon (env, denv) (c, loc) = case c of L.CAnnot (c, k) => @@ -411,6 +430,32 @@ | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) + | L.CTuple cs => + let + val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) => + let + val (c', k, gs') = elabCon (env, denv) c + in + (c' :: cs', k :: ks, gs' @ gs) + end) ([], [], []) cs + in + ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs) + end + | L.CProj (c, n) => + let + val (c', k, gs) = elabCon (env, denv) c + in + case hnormKind k of + (L'.KTuple ks, _) => + if n <= 0 orelse n > length ks then + (conError env (ProjBounds (c', n)); + (cerror, kerror, [])) + else + ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs) + | k => (conError env (ProjMismatch (c', k)); + (cerror, kerror, [])) + end + | L.CWild k => let val k' = elabKind k @@ -509,11 +554,6 @@ exception CUnify of L'.con * L'.con * cunify_error -fun hnormKind (kAll as (k, _)) = - case k of - L'.KUnif (_, _, ref (SOME k)) => hnormKind k - | _ => kAll - fun kindof env (c, loc) = case c of L'.TFun _ => ktype @@ -553,6 +593,12 @@ | L'.CUnit => (L'.KUnit, loc) + | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) + | L'.CProj (c, n) => + (case hnormKind (kindof env c) of + (L'.KTuple ks, _) => List.nth (ks, n - 1) + | k => raise CUnify' (CKindof (k, c))) + | L'.CError => kerror | L'.CUnif (_, k, _, _) => k @@ -862,6 +908,20 @@ else err CIncompatible + | (L'.CTuple cs1, L'.CTuple cs2) => + ((ListPair.foldlEq (fn (c1, c2, gs) => + let + val gs' = unifyCons' (env, denv) c1 c2 + in + gs' @ gs + end) [] (cs1, cs2)) + handle ListPair.UnequalLengths => err CIncompatible) + | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => + if n1 = n2 then + unifyCons' (env, denv) c1 c2 + else + err CIncompatible + | (L'.CError, _) => [] | (_, L'.CError) => [] @@ -869,8 +929,6 @@ | (_, L'.CRecord _) => isRecord () | (L'.CConcat _, _) => isRecord () | (_, L'.CConcat _) => isRecord () - (*| (L'.CUnif (_, (L'.KRecord _, _), _, _), _) => isRecord () - | (_, L'.CUnif (_, (L'.KRecord _, _), _, _)) => isRecord ()*) | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => if r1 = r2 then @@ -2908,7 +2966,11 @@ val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) val () = case gs of [] => () - | _ => raise Fail "Unresolved disjointness constraints in Basis" + | _ => (app (fn (_, env, _, c1, c2) => + prefaces "Unresolved" + [("c1", p_con env c1), + ("c2", p_con env c2)]) gs; + raise Fail "Unresolved disjointness constraints in Basis") val (env', basis_n) = E.pushStrNamed env "Basis" sgn
--- a/src/lacweb.grm Thu Aug 14 15:27:35 2008 -0400 +++ b/src/lacweb.grm Thu Aug 14 18:35:08 2008 -0400 @@ -39,6 +39,39 @@ TRecord c => c | _ => t +datatype select_item = + Field of con * con + +datatype select = + Star + | Items of select_item list + +fun eqTnames ((c1, _), (c2, _)) = + case (c1, c2) of + (CVar (ms1, x1), CVar (ms2, x2)) => ms1 = ms2 andalso x1 = x2 + | (CName x1, CName x2) => x1 = x2 + | _ => false + +fun amend_select loc (si, tabs) = + let + val (tx, c) = case si of + Field (tx, fx) => (tx, (CRecord ([(fx, (CWild (KType, loc), loc))]), loc)) + + val (tabs, found) = ListUtil.foldlMap (fn ((tx', c'), found) => + if eqTnames (tx, tx') then + ((tx', (CConcat (c, c'), loc)), true) + else + ((tx', c'), found)) + false tabs + in + if found then + () + else + ErrorMsg.errorAt loc "Select of field from unbound table"; + + tabs + end + %% %header (functor LacwebLrValsFn(structure Token : TOKEN)) @@ -84,6 +117,7 @@ | str of str | kind of kind + | ktuple of kind list | kcolon of explicitness | path of string list * string @@ -95,6 +129,7 @@ | capps of con | cterm of con | ctuple of con list + | ctuplev of con list | ident of con | idents of con list | rcon of (con * con) list @@ -126,6 +161,12 @@ | tables of (con * exp) list | tname of con | table of con * exp + | tident of con + | fident of con + | seli of select_item + | selis of select_item list + | select of select + %verbose (* print summary of errors *) %pos int (* positions *) @@ -270,6 +311,10 @@ | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) + | LPAREN ktuple RPAREN (KTuple ktuple, s (LPARENleft, RPARENright)) + +ktuple : kind STAR kind ([kind1, kind2]) + | kind STAR ktuple (kind :: ktuple) capps : cterm (cterm) | capps cterm (CApp (capps, cterm), s (cappsleft, ctermright)) @@ -319,9 +364,15 @@ | HASH INT (CName (Int64.toString INT), s (HASHleft, INTright)) | path (CVar path, s (pathleft, pathright)) + | path DOT INT (CProj ((CVar path, s (pathleft, pathright)), Int64.toInt INT), + s (pathleft, INTright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) | FOLD (CFold, s (FOLDleft, FOLDright)) | UNIT (CUnit, s (UNITleft, UNITright)) + | LPAREN ctuplev RPAREN (CTuple ctuplev, s (LPARENleft, RPARENright)) + +ctuplev: cexp COMMA cexp ([cexp1, cexp2]) + | cexp COMMA ctuplev (cexp :: ctuplev) ctuple : capps STAR capps ([capps1, capps2]) | capps STAR ctuple (capps :: ctuple) @@ -503,11 +554,34 @@ | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright)) | LBRACE eexp RBRACE (eexp) -query : SELECT STAR FROM tables (let +query : SELECT select FROM tables (let val loc = s (SELECTleft, tablesright) + + val sel = + case select of + Star => map (fn (nm, _) => + (nm, (CTuple [(CWild (KRecord (KType, loc), loc), + loc), + (CRecord [], loc)], + loc))) tables + | Items sis => + let + val tabs = map (fn (nm, _) => (nm, (CRecord [], loc))) tables + val tabs = foldl (amend_select loc) tabs sis + in + map (fn (nm, c) => (nm, + (CTuple [c, + (CWild (KRecord (KType, loc), loc), + loc)], loc))) tabs + end + + val sel = (CRecord sel, loc) + + val e = (EVar (["Basis"], "sql_query"), loc) + val e = (ECApp (e, sel), loc) + val e = (EApp (e, (ERecord tables, loc)), loc) in - (EApp ((EVar (["Basis"], "sql_query"), loc), - (ERecord tables, loc)), loc) + e end) tables : table ([table]) @@ -516,7 +590,22 @@ tname : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) | LBRACE cexp RBRACE (cexp) -table : SYMBOL ((CName (capitalize SYMBOL), s (SYMBOLleft, SYMBOLright)), +table : SYMBOL ((CName SYMBOL, s (SYMBOLleft, SYMBOLright)), (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))) | SYMBOL AS tname (tname, (EVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))) | LBRACE eexp RBRACE AS tname (tname, eexp) + +tident : SYMBOL (CName SYMBOL, s (SYMBOLleft, SYMBOLright)) + | CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | LBRACE cexp RBRACE (cexp) + +fident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | LBRACE cexp RBRACE (cexp) + +seli : tident DOT fident (Field (tident, fident)) + +selis : seli ([seli]) + | seli COMMA selis (seli :: selis) + +select : STAR (Star) + | selis (Items selis)
--- a/src/source.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/source.sml Thu Aug 14 18:35:08 2008 -0400 @@ -35,6 +35,7 @@ | KName | KRecord of kind | KUnit + | KTuple of kind list | KWild withtype kind = kind' located @@ -64,6 +65,9 @@ | CUnit + | CTuple of con list + | CProj of con * int + | CWild of kind withtype con = con' located
--- a/src/source_print.sml Thu Aug 14 15:27:35 2008 -0400 +++ b/src/source_print.sml Thu Aug 14 18:35:08 2008 -0400 @@ -46,6 +46,9 @@ | KRecord k => box [string "{", p_kind k, string "}"] | KUnit => string "Unit" | KWild => string "_" + | KTuple ks => box [string "(", + p_list_sep (box [space, string "*", space]) p_kind ks, + string ")"] and p_kind k = p_kind' false k @@ -154,6 +157,13 @@ string "::", space, p_kind k] + + | CTuple cs => box [string "(", + p_list p_con cs, + string ")"] + | CProj (c, n) => box [p_con c, + string ".", + string (Int.toString n)] and p_con c = p_con' false c
--- a/tests/table.lac Thu Aug 14 15:27:35 2008 -0400 +++ b/tests/table.lac Thu Aug 14 18:35:08 2008 -0400 @@ -1,12 +1,16 @@ table t1 : {A : int, B : string, C : float} +table t2 : {A : float, D : int} val q1 = (SELECT * FROM t1) -table t2 : {A : float, D : int} - val q2 = (SELECT * FROM t1, t2) (*val q3 = (SELECT * FROM t1, t1)*) val q3 = (SELECT * FROM t1, t1 AS T2) val q4 = (SELECT * FROM {t1} AS T, t1 AS T2) + +val q5 = (SELECT t1.A FROM t1) +val q6 = (SELECT t1.B, t1.C, t1.A FROM t1) + +val q7 = (SELECT t1.A, t2.A FROM t1, t2)