# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1260732858 18000
# Node ID d89f98f0b4bb89c0cea0678c4376e4c2f1db54a1
# Parent  b2311dfb3158267de06d365f329da68926d7d391
Fixing a bug in DInitializer elaboration

diff -r b2311dfb3158 -r d89f98f0b4bb lib/ur/top.ur
--- a/lib/ur/top.ur	Sun Dec 13 14:20:41 2009 -0500
+++ b/lib/ur/top.ur	Sun Dec 13 14:34:18 2009 -0500
@@ -271,6 +271,9 @@
                 None => error <xml>Query returned no rows</xml>
               | Some r => r.nm)
 
+fun nonempty [fs] [us] (t : sql_table fs us) =
+    oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
+
 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
     [t ::: Type] (_ : sql_injectable (option t))
     (e1 : sql_exp tables agg exps (option t))
diff -r b2311dfb3158 -r d89f98f0b4bb lib/ur/top.urs
--- a/lib/ur/top.urs	Sun Dec 13 14:20:41 2009 -0500
+++ b/lib/ur/top.urs	Sun Dec 13 14:34:18 2009 -0500
@@ -173,6 +173,9 @@
     sql_query (mapU [] tabs) [nm = t]
     -> transaction t
 
+val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
+               -> transaction bool
+
 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
                  -> t ::: Type -> sql_injectable (option t)
                  -> sql_exp tables agg exps (option t)
diff -r b2311dfb3158 -r d89f98f0b4bb src/elaborate.sml
--- a/src/elaborate.sml	Sun Dec 13 14:20:41 2009 -0500
+++ b/src/elaborate.sml	Sun Dec 13 14:34:18 2009 -0500
@@ -3671,12 +3671,12 @@
                 end
               | L.DInitializer e =>
                 let
-                    val (e', t, gs) = elabExp (env, denv) e
+                    val (e', t, gs') = elabExp (env, denv) e
                     val t' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc),
                                        (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc)
                 in
                     checkCon env e' t t';
-                    ([(L'.DInitializer e', loc)], (env, denv, gs))
+                    ([(L'.DInitializer e', loc)], (env, denv, gs' @ gs))
                 end
 
         (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)