# HG changeset patch # User Adam Chlipala # Date 1218903338 14400 # Node ID 1487c712eb12438c5cd57ff985e704dc8f78a388 # Parent 63a2f2322c1fdb5fe18c3836a751fc960069db53 Stub WHERE support diff -r 63a2f2322c1f -r 1487c712eb12 lib/basis.lig --- a/lib/basis.lig Sat Aug 16 10:54:46 2008 -0400 +++ b/lib/basis.lig Sat Aug 16 12:15:38 2008 -0400 @@ -14,14 +14,26 @@ (*** Queries *) con sql_query :: {{Type}} -> Type +con sql_exp :: {{Type}} -> Type -> Type val sql_query : tables :: {({Type} * {Type})} - -> $(fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => + -> {From : $(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) + [nm = sql_table (selected_unselected.1 ++ selected_unselected.2)] ++ acc) [] tables), + Where : sql_exp (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => selected_unselected.1 ~ selected_unselected.2 => + [nm = selected_unselected.1 ++ selected_unselected.2] ++ acc) [] tables) bool} -> sql_query (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => [nm] ~ acc => [nm = selected_unselected.1] ++ acc) [] tables) +con sql_type :: Type -> Type +val sql_bool : sql_type bool +val sql_int : sql_type int +val sql_float : sql_type float +val sql_string : sql_type string + +val sql_inject : tables ::: {{Type}} -> t ::: Type -> t -> sql_type t -> sql_exp tables t + (** XML *) diff -r 63a2f2322c1f -r 1487c712eb12 src/elab_ops.sml --- a/src/elab_ops.sml Sat Aug 16 10:54:46 2008 -0400 +++ b/src/elab_ops.sml Sat Aug 16 12:15:38 2008 -0400 @@ -136,6 +136,7 @@ | ((CRecord (_, []), _), c2') => c2' | ((CConcat (c11, c12), loc), c2') => hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc) + | (c1', (CRecord (_, []), _)) => c1' | _ => cAll) | CProj (c, n) => diff -r 63a2f2322c1f -r 1487c712eb12 src/elaborate.sml --- a/src/elaborate.sml Sat Aug 16 10:54:46 2008 -0400 +++ b/src/elaborate.sml Sat Aug 16 12:15:38 2008 -0400 @@ -682,9 +682,14 @@ end and consEq (env, denv) (c1, c2) = - (case unifyCons (env, denv) c1 c2 of - [] => true - | _ => false) + let + val gs = unifyCons (env, denv) c1 c2 + in + List.all (fn (loc, env, denv, c1, c2) => + case D.prove env denv (c1, c2, loc) of + [] => true + | _ => false) gs + end handle CUnify _ => false and consNeq env (c1, c2) = @@ -857,7 +862,9 @@ and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = let - fun err f = raise CUnify' (f (c1All, c2All)) + fun err f = (prefaces "unifyCons'' fails" [("c1All", p_con env c1All), + ("c2All", p_con env c2All)]; + raise CUnify' (f (c1All, c2All))) fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) in @@ -956,7 +963,6 @@ unifyKinds ran1 ran2; []) - | _ => err CIncompatible end diff -r 63a2f2322c1f -r 1487c712eb12 src/lacweb.grm --- a/src/lacweb.grm Sat Aug 16 10:54:46 2008 -0400 +++ b/src/lacweb.grm Sat Aug 16 12:15:38 2008 -0400 @@ -72,6 +72,13 @@ tabs end +fun sql_inject (v, t, loc) = + let + val e = (EApp ((EVar (["Basis"], "sql_inject"), loc), (v, loc)), loc) + in + (EApp (e, (t, loc)), loc) + end + %% %header (functor LacwebLrValsFn(structure Token : TOKEN)) @@ -95,7 +102,8 @@ | NOTAGS of string | BEGIN_TAG of string | END_TAG of string - | SELECT | FROM | AS + | SELECT | FROM | AS | CWHERE + | TRUE | FALSE %nonterm file of decl list @@ -166,6 +174,8 @@ | seli of select_item | selis of select_item list | select of select + | sqlexp of exp + | wopt of exp %verbose (* print summary of errors *) @@ -554,7 +564,8 @@ | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright)) | LBRACE eexp RBRACE (eexp) -query : SELECT select FROM tables (let +query : SELECT select FROM tables wopt + (let val loc = s (SELECTleft, tablesright) val sel = @@ -579,7 +590,11 @@ val e = (EVar (["Basis"], "sql_query"), loc) val e = (ECApp (e, sel), loc) - val e = (EApp (e, (ERecord tables, loc)), loc) + val re = (ERecord [((CName "From", loc), + (ERecord tables, loc)), + ((CName "Where", loc), + wopt)], loc) + val e = (EApp (e, re), loc) in e end) @@ -609,3 +624,15 @@ select : STAR (Star) | selis (Items selis) + +sqlexp : TRUE (sql_inject (EVar (["Basis"], "True"), + EVar (["Basis"], "sql_bool"), + s (TRUEleft, TRUEright))) + | FALSE (sql_inject (EVar (["Basis"], "False"), + EVar (["Basis"], "sql_bool"), + s (FALSEleft, FALSEright))) + +wopt : (sql_inject (EVar (["Basis"], "True"), + EVar (["Basis"], "sql_bool"), + ErrorMsg.dummySpan)) + | CWHERE sqlexp (sqlexp) diff -r 63a2f2322c1f -r 1487c712eb12 src/lacweb.lex --- a/src/lacweb.lex Sat Aug 16 10:54:46 2008 -0400 +++ b/src/lacweb.lex Sat Aug 16 12:15:38 2008 -0400 @@ -288,6 +288,10 @@ "SELECT" => (Tokens.SELECT (pos yypos, pos yypos + size yytext)); "FROM" => (Tokens.FROM (pos yypos, pos yypos + size yytext)); "AS" => (Tokens.AS (pos yypos, pos yypos + size yytext)); + "WHERE" => (Tokens.CWHERE (pos yypos, pos yypos + size yytext)); + + "TRUE" => (Tokens.TRUE (pos yypos, pos yypos + size yytext)); + "FALSE" => (Tokens.FALSE (pos yypos, pos yypos + size yytext)); {id} => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext)); {cid} => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext)); diff -r 63a2f2322c1f -r 1487c712eb12 tests/where.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/where.lac Sat Aug 16 12:15:38 2008 -0400 @@ -0,0 +1,6 @@ +table t1 : {A : int, B : string, C : float} +table t2 : {A : float, D : int} + +val q1 = (SELECT * FROM t1) +val q2 = (SELECT * FROM t1 WHERE TRUE) +val q3 = (SELECT * FROM t1 WHERE FALSE)