# HG changeset patch # User Adam Chlipala # Date 1219337369 14400 # Node ID bbe5899a95858835e66c3f68ba5bc12fcc379ab5 # Parent 36fef91a6bbf2d96972884f24b6a56bb10cafd82 Queries back to working as well as before, after start of refactoring to support grouping diff -r 36fef91a6bbf -r bbe5899a9585 lib/basis.lig --- a/lib/basis.lig Sat Aug 16 17:50:10 2008 -0400 +++ b/lib/basis.lig Thu Aug 21 12:49:29 2008 -0400 @@ -14,39 +14,53 @@ (*** Queries *) con sql_query :: {{Type}} -> Type -con sql_exp :: {{Type}} -> Type -> Type +con sql_exp :: {{Type}} -> {{Type}} -> Type -> Type -val sql_query : tables :: {({Type} * {Type})} - -> {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), - 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_subset :: {{Type}} -> {{Type}} -> Type +val sql_subset : keep_drop :: {({Type} * {Type})} + -> sql_subset + (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => fields.1 ~ fields.2 => + [nm = fields.1 ++ fields.2] ++ acc) [] keep_drop) + (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => + [nm] ~ acc => + [nm = fields.1] ++ acc) [] keep_drop) +val sql_subset_all : tables :: {{Type}} + -> sql_subset tables tables + +val sql_query : tables ::: {{Type}} + (*-> grouped ::: {{Type}}*) + -> selected ::: {{Type}} + -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc => + [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables), + Where : sql_exp tables [] bool, + (*GroupBy : sql_subset tables grouped, + Having : sql_exp grouped tables bool,*) + SelectFields : sql_subset tables selected} + -> sql_query selected val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> tab :: Name -> field :: Name - -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) fieldType + -> agg ::: {{Type}} + -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg fieldType class sql_injectable val sql_bool : sql_injectable bool val sql_int : sql_injectable int val sql_float : sql_injectable float val sql_string : sql_injectable string -val sql_inject : tables ::: {{Type}} -> t ::: Type -> t -> sql_injectable t -> sql_exp tables t +val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> t -> sql_injectable t -> sql_exp tables agg t con sql_unary :: Type -> Type -> Type val sql_not : sql_unary bool bool -val sql_unary : tables ::: {{Type}} -> arg ::: Type -> res ::: Type - -> sql_unary arg res -> sql_exp tables arg -> sql_exp tables res +val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> arg ::: Type -> res ::: Type + -> sql_unary arg res -> sql_exp tables agg arg -> sql_exp tables agg res con sql_binary :: Type -> Type -> Type -> Type val sql_and : sql_binary bool bool bool val sql_or : sql_binary bool bool bool -val sql_binary : tables ::: {{Type}} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type - -> sql_binary arg1 arg2 res -> sql_exp tables arg1 -> sql_exp tables arg2 -> sql_exp tables res +val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type + -> sql_binary arg1 arg2 res -> sql_exp tables agg arg1 -> sql_exp tables agg arg2 -> sql_exp tables agg res type sql_comparison val sql_eq : sql_comparison @@ -56,8 +70,8 @@ val sql_gt : sql_comparison val sql_ge : sql_comparison val sql_comparison : sql_comparison - -> tables ::: {{Type}} -> t ::: Type -> sql_exp tables t -> sql_exp tables t - -> sql_injectable t -> sql_exp tables bool + -> tables ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> sql_exp tables agg t -> sql_exp tables agg t + -> sql_injectable t -> sql_exp tables agg bool (** XML *) diff -r 36fef91a6bbf -r bbe5899a9585 src/elaborate.sml --- a/src/elaborate.sml Sat Aug 16 17:50:10 2008 -0400 +++ b/src/elaborate.sml Thu Aug 21 12:49:29 2008 -0400 @@ -640,6 +640,8 @@ | Cons => "Cons" | Unknown => "Unknown") +exception SummaryFailure + fun unifyRecordCons (env, denv) (c1, c2) = let fun rkindof c = @@ -701,8 +703,9 @@ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) = let + val loc = #2 k (*val () = eprefaces "Summaries" [("#1", p_summary env s1), - ("#2", p_summary env s2)]*) + ("#2", p_summary env s2)]*) fun eatMatching p (ls1, ls2) = let @@ -732,9 +735,11 @@ andalso consEq (env, denv) (x1, x2)) (#fields s1, #fields s2) (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), - ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) + ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2) + (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), + ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) fun unifFields (fs, others, unifs) = case (fs, others, unifs) of @@ -765,10 +770,37 @@ val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2) val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1) + (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), + ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) + + fun isGuessable (other, fs) = + let + val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure) + in + List.all (fn (loc, env, denv, c1, c2) => + case D.prove env denv (c1, c2, loc) of + [] => true + | _ => false) gs + end + handle SummaryFailure => false + + val (fs1, fs2, others1, others2) = + case (fs1, fs2, others1, others2) of + ([], _, [other1], []) => + if isGuessable (other1, fs2) then + ([], [], [], []) + else + (fs1, fs2, others1, others2) + | _ => (fs1, fs2, others1, others2) + + (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), + ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) + val clear = case (fs1, others1, fs2, others2) of ([], [], [], []) => true | _ => false val empty = (L'.CRecord (k, []), dummy) + fun pairOffUnifs (unifs1, unifs2) = case (unifs1, unifs2) of ([], _) => @@ -786,6 +818,81 @@ pairOffUnifs (rest1, rest2)) in pairOffUnifs (unifs1, unifs2) + (*before eprefaces "Summaries'" [("#1", p_summary env s1), + ("#2", p_summary env s2)]*) + end + +and guessFold (env, denv) (c1, c2, gs, ex) = + let + val loc = #2 c1 + + fun unfold (dom, ran, f, i, r, c) = + let + val nm = cunif (loc, (L'.KName, loc)) + val v = cunif (loc, dom) + val rest = cunif (loc, (L'.KRecord dom, loc)) + val acc = (L'.CFold (dom, ran), loc) + val acc = (L'.CApp (acc, f), loc) + val acc = (L'.CApp (acc, i), loc) + val acc = (L'.CApp (acc, rest), loc) + + val (iS, gs3) = summarizeCon (env, denv) i + + val app = (L'.CApp (f, nm), loc) + val app = (L'.CApp (app, v), loc) + val app = (L'.CApp (app, acc), loc) + val (appS, gs4) = summarizeCon (env, denv) app + + val (cS, gs5) = summarizeCon (env, denv) c + in + (*prefaces "Summaries" [("iS", p_con_summary iS), + ("appS", p_con_summary appS), + ("cS", p_con_summary cS)];*) + + if compatible (iS, appS) then + raise ex + else if compatible (cS, iS) then + let + (*val () = prefaces "Same?" [("i", p_con env i), + ("c", p_con env c)]*) + val gs6 = unifyCons (env, denv) i c + (*val () = TextIO.print "Yes!\n"*) + + val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) + in + gs @ gs3 @ gs5 @ gs6 @ gs7 + end + else if compatible (cS, appS) then + let + (*val () = prefaces "Same?" [("app", p_con env app), + ("c", p_con env c), + ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*) + val gs6 = unifyCons (env, denv) app c + (*val () = TextIO.print "Yes!\n"*) + + val singleton = (L'.CRecord (dom, [(nm, v)]), loc) + val concat = (L'.CConcat (singleton, rest), loc) + (*val () = prefaces "Pre-crew" [("r", p_con env r), + ("concat", p_con env concat)]*) + val gs7 = unifyCons (env, denv) r concat + in + (*prefaces "The crew" [("nm", p_con env nm), + ("v", p_con env v), + ("rest", p_con env rest)];*) + + gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 + end + else + raise ex + end + handle _ => raise ex + in + case (#1 c1, #1 c2) of + (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) => + unfold (dom, ran, f, i, r, c2) + | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) => + unfold (dom, ran, f, i, r, c1) + | _ => raise ex end and unifyCons' (env, denv) c1 c2 = @@ -798,68 +905,7 @@ in gs1 @ gs2 @ gs3 end - handle ex => - let - val loc = #2 c1 - - fun unfold (dom, f, i, r, c) = - let - val nm = cunif (loc, (L'.KName, loc)) - val v = cunif (loc, dom) - val rest = cunif (loc, (L'.KRecord dom, loc)) - - val (iS, gs3) = summarizeCon (env, denv) i - - val app = (L'.CApp (f, nm), loc) - val app = (L'.CApp (app, v), loc) - val app = (L'.CApp (app, rest), loc) - val (appS, gs4) = summarizeCon (env, denv) app - - val (cS, gs5) = summarizeCon (env, denv) c - in - (*prefaces "Summaries" [("iS", p_con_summary iS), - ("appS", p_con_summary appS), - ("cS", p_con_summary cS)];*) - - if compatible (iS, appS) then - raise ex - else if compatible (cS, iS) then - let - (*val () = prefaces "Same?" [("i", p_con env i), - ("c", p_con env c)]*) - val gs6 = unifyCons (env, denv) i c - (*val () = TextIO.print "Yes!\n"*) - - val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) - in - gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 - end - else if compatible (cS, appS) then - let - (*val () = prefaces "Same?" [("app", p_con env app), - ("c", p_con env c), - ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*) - val gs6 = unifyCons (env, denv) app c - (*val () = TextIO.print "Yes!\n"*) - - val singleton = (L'.CRecord (dom, [(nm, v)]), loc) - val concat = (L'.CConcat (singleton, rest), loc) - val gs7 = unifyCons (env, denv) r concat - in - gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 - end - else - raise ex - end - handle _ => raise ex - in - case (#1 c1, #1 c2) of - (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r), _) => - unfold (dom, f, i, r, c2) - | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r)) => - unfold (dom, f, i, r, c1) - | _ => raise ex - end + handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) end and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = diff -r 36fef91a6bbf -r bbe5899a9585 src/lacweb.grm --- a/src/lacweb.grm Sat Aug 16 17:50:10 2008 -0400 +++ b/src/lacweb.grm Thu Aug 21 12:49:29 2008 -0400 @@ -640,12 +640,24 @@ val sel = (CRecord sel, loc) + val hopt = (sql_inject (EVar (["Basis"], "True"), + EVar (["Basis"], "sql_bool"), + loc)) + val e = (EVar (["Basis"], "sql_query"), loc) - val e = (ECApp (e, sel), loc) + val _ = [((CName "GroupBy", loc), + (ECApp ((EVar (["Basis"], "sql_subset_all"), loc), + (CWild (KRecord (KType, loc), loc), loc)), loc)), + ((CName "Having", loc), + hopt)] val re = (ERecord [((CName "From", loc), (ERecord tables, loc)), ((CName "Where", loc), - wopt)], loc) + wopt), + ((CName "SelectFields", loc), + (ECApp ((EVar (["Basis"], "sql_subset"), loc), + sel), loc))], loc) + val e = (EApp (e, re), loc) in e diff -r 36fef91a6bbf -r bbe5899a9585 src/print.sml --- a/src/print.sml Sat Aug 16 17:50:10 2008 -0400 +++ b/src/print.sml Thu Aug 21 12:49:29 2008 -0400 @@ -52,7 +52,7 @@ | x :: rest => let val tokens = foldr (fn (x, tokens) => - sep :: f x :: tokens) + sep :: PD.cut :: f x :: tokens) [] rest in box (f x :: tokens) diff -r 36fef91a6bbf -r bbe5899a9585 src/source_print.sml --- a/src/source_print.sml Sat Aug 16 17:50:10 2008 -0400 +++ b/src/source_print.sml Thu Aug 21 12:49:29 2008 -0400 @@ -156,7 +156,8 @@ space, string "::", space, - p_kind k] + p_kind k, + string ")"] | CTuple cs => box [string "(", p_list p_con cs,