aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-21 12:49:29 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-21 12:49:29 -0400
commitbe0c07faab159e4c0d924c9656aa2cb47a363bef (patch)
tree34ed0c3c2149452895208ebdaf6a6ab732a75b41
parent024d9ab1d554d897787c9d38dc1761ba37a078de (diff)
Queries back to working as well as before, after start of refactoring to support grouping
-rw-r--r--lib/basis.lig52
-rw-r--r--src/elaborate.sml174
-rw-r--r--src/lacweb.grm16
-rw-r--r--src/print.sml2
-rw-r--r--src/source_print.sml3
5 files changed, 160 insertions, 87 deletions
diff --git a/lib/basis.lig b/lib/basis.lig
index 0e98a53f..8299f200 100644
--- a/lib/basis.lig
+++ b/lib/basis.lig
@@ -14,39 +14,53 @@ con sql_table :: {Type} -> Type
(*** Queries *)
con sql_query :: {{Type}} -> Type
-con sql_exp :: {{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_exp :: {{Type}} -> {{Type}} -> Type -> Type
+
+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_le : sql_comparison
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 --git a/src/elaborate.sml b/src/elaborate.sml
index 58918dbd..73889f74 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -640,6 +640,8 @@ fun p_con_summary s =
| Cons => "Cons"
| Unknown => "Unknown")
+exception SummaryFailure
+
fun unifyRecordCons (env, denv) (c1, c2) =
let
fun rkindof c =
@@ -701,8 +703,9 @@ and consNeq env (c1, c2) =
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 @@ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
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 @@ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
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 @@ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
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 @@ and unifyCons' (env, denv) c1 c2 =
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 --git a/src/lacweb.grm b/src/lacweb.grm
index e38ad6b0..1eb85181 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -640,12 +640,24 @@ query : SELECT select FROM tables wopt
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 --git a/src/print.sml b/src/print.sml
index a1efdb96..db6af55c 100644
--- a/src/print.sml
+++ b/src/print.sml
@@ -52,7 +52,7 @@ fun p_list_sep sep f ls =
| 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 --git a/src/source_print.sml b/src/source_print.sml
index 08231ab5..7ae2b23e 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -156,7 +156,8 @@ fun p_con' par (c, _) =
space,
string "::",
space,
- p_kind k]
+ p_kind k,
+ string ")"]
| CTuple cs => box [string "(",
p_list p_con cs,