changeset 223:bbe5899a9585

Queries back to working as well as before, after start of refactoring to support grouping
author Adam Chlipala <adamc@hcoop.net>
date Thu, 21 Aug 2008 12:49:29 -0400
parents 36fef91a6bbf
children cb8a68964ebb
files lib/basis.lig src/elaborate.sml src/lacweb.grm src/print.sml src/source_print.sml
diffstat 5 files changed, 159 insertions(+), 86 deletions(-) [+]
line wrap: on
line diff
--- 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 *)
 
--- 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, _)) =
--- 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
--- 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)
--- 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,