Expunging nullable fields

6 files changed, 111 insertions, 53 deletions

diff --git a/src/c/urweb.c b/src/c/urweb.c
index 8ad50711..e74474f7 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -1869,8 +1869,13 @@ void uw_expunger(uw_context ctx, uw_Basis_client cli);
 static failure_kind uw_expunge(uw_context ctx, uw_Basis_client cli) {
   int r = setjmp(ctx->jmp_buf);
 
-  if (r == 0)
+  if (r == 0) {
+    if (uw_db_begin(ctx))
+      uw_error(ctx, FATAL, "Error running SQL BEGIN");
     uw_expunger(ctx, cli);
+    if (uw_db_commit(ctx))
+      uw_error(ctx, FATAL, "Error running SQL COMMIT");
+  }
 
   return r;
 }
@@ -1892,16 +1897,20 @@ void uw_prune_clients(uw_context ctx) {
         prev->next = next;
       else
         clients_used = next;
+      uw_reset(ctx);
       while (fk == UNLIMITED_RETRY) {
-        uw_reset(ctx);
         fk = uw_expunge(ctx, c->id);
-        if (fk == SUCCESS) {
-          free_client(c);
-          break;
+        if (fk == UNLIMITED_RETRY) {
+          uw_db_rollback(ctx);
+          printf("Unlimited retry during expunge: %s\n", uw_error_message(ctx));
         }
       }
-      if (fk != SUCCESS)
+      if (fk == SUCCESS)
+        free_client(c);
+      else {
+        uw_db_rollback(ctx);
         printf("Expunge blocked by error: %s\n", uw_error_message(ctx));
+      }
     }
     else
       prev = c;
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 21e53a51..3b1705af 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2760,6 +2760,8 @@ fun p_file env (ds, ps) =
                       string "int uw_db_commit(uw_context ctx) { return 0; };",
                       newline,
                       string "int uw_db_rollback(uw_context ctx) { return 0; };",
+                      newline,
+                      string "void uw_expunger(uw_context ctx, uw_Basis_client cli) { };",
                       newline]]
     end
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index de33ec56..370e504f 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -190,6 +190,7 @@ datatype class_key =
        | CkRel of int
        | CkProj of int * string list * string
        | CkApp of class_key * class_key
+       | CkOther of con
 
 fun ck2s ck =
     case ck of
@@ -197,6 +198,7 @@ fun ck2s ck =
       | CkRel n => "Rel(" ^ Int.toString n ^ ")"
       | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
       | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
+      | CkOther _ => "Other"
 
 type class_key_n = class_key * int
 
@@ -227,6 +229,10 @@ fun compare' x =
       | (CkApp (f1, x1), CkApp (f2, x2)) =>
         join (compare' (f1, f2),
               fn () => compare' (x1, x2))
+      | (CkApp _, _) => LESS
+      | (_, CkApp _) => GREATER
+
+      | (CkOther _, CkOther _) => EQUAL
 fun compare ((k1, n1), (k2, n2)) =
     join (Int.compare (n1, n2),
        fn () => compare' (k1, k2))
@@ -309,6 +315,7 @@ fun liftClassKey' ck =
       | CkRel n => CkRel (n + 1)
       | CkProj _ => ck
       | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
+      | CkOther c => CkOther (lift c)
 
 fun liftClassKey (ck, n) = (liftClassKey' ck, n)
 
@@ -513,17 +520,14 @@ fun isClass (env : env) c =
         find (class_name_in c)
     end
 
-fun class_key_in (c, _) =
+fun class_key_in (all as (c, _)) =
     case c of
-        CRel n => SOME (CkRel n)
-      | CNamed n => SOME (CkNamed n)
-      | CModProj x => SOME (CkProj x)
+        CRel n => CkRel n
+      | CNamed n => CkNamed n
+      | CModProj x => CkProj x
       | CUnif (_, _, _, ref (SOME c)) => class_key_in c
-      | CApp (c1, c2) =>
-        (case (class_key_in c1, class_key_in c2) of
-             (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
-           | _ => NONE)
-      | _ => NONE
+      | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2)
+      | _ => CkOther all
 
 fun class_key_out loc =
     let
@@ -533,6 +537,7 @@ fun class_key_out loc =
               | CkNamed n => (CNamed n, loc)
               | CkProj x => (CModProj x, loc)
               | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc)
+              | CkOther c => c
     in
         cko
     end
@@ -540,8 +545,8 @@ fun class_key_out loc =
 fun class_pair_in (c, _) =
     case c of
         CApp (f, x) =>
-        (case (class_name_in f, class_key_in x) of
-             (SOME f, SOME x) => SOME (f, x)
+        (case class_name_in f of
+             SOME f => SOME (f, class_key_in x)
            | _ => NONE)
       | CUnif (_, _, _, ref (SOME c)) => class_pair_in c
       | _ => NONE
@@ -550,13 +555,17 @@ fun sub_class_key (n, c) =
     let
         fun csk k =
             case k of
-                CkRel n' => if n' = n then
-                                c
-                            else
-                                k
-              | CkNamed _ => k
-              | CkProj _ => k
-              | CkApp (k1, k2) => CkApp (csk k1, csk k2)
+                CkRel n' => SOME (if n' = n then
+                                      c
+                                  else
+                                      k)
+              | CkNamed _ => SOME k
+              | CkProj _ => SOME k
+              | CkApp (k1, k2) =>
+                (case (csk k1, csk k2) of
+                     (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
+                   | _ => NONE)
+              | CkOther _ => NONE
     in
         csk
     end
@@ -604,12 +613,17 @@ fun resolveClass (env : env) c =
                                     val es = map (fn (cn, ck) =>
                                                      let
                                                          val ck = ListUtil.foldli (fn (i, arg, ck) =>
-                                                                                      sub_class_key (len - i - 1,
-                                                                                                     arg)
-                                                                                                    ck)
-                                                                                  ck args
+                                                                                      case ck of
+                                                                                          NONE => NONE
+                                                                                        | SOME ck =>
+                                                                                          sub_class_key (len - i - 1,
+                                                                                                         arg)
+                                                                                                        ck)
+                                                                                  (SOME ck) args
                                                      in
-                                                         doPair (cn, ck)
+                                                         case ck of
+                                                             NONE => NONE
+                                                           | SOME ck => doPair (cn, ck)
                                                      end) cs
                                 in
                                     if List.exists (not o Option.isSome) es then
@@ -687,6 +701,12 @@ datatype rule =
          Normal of int * (class_name * class_key) list * class_key
        | Inclusion of class_name
 
+fun containsOther k =
+    case k of
+        CkOther _ => true
+      | CkApp (k1, k2) => containsOther k1 orelse containsOther k2
+      | _ => false
+
 fun rule_in c =
     let
         fun quantifiers (c, nvars) =
@@ -707,7 +727,11 @@ fun rule_in c =
                                 let
                                     fun dearg (ck, i) =
                                         if i >= nvars then
-                                            SOME (cn, Normal (nvars, hyps, ck))
+                                            if containsOther ck
+                                               orelse List.exists (fn (_, k) => containsOther k) hyps then
+                                                NONE
+                                            else
+                                                SOME (cn, Normal (nvars, hyps, ck))
                                         else case ck of
                                                  CkApp (ck, CkRel i') =>
                                                  if i' = i then
diff --git a/src/monoize.sml b/src/monoize.sml
index 50678be4..361986d2 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -2500,33 +2500,44 @@ fun monoize env file =
                                                  | _ => st)
                                             | _ => st) ([], []) xts
 
+                            fun cond (x, v) =
+                                (L'.EStrcat ((L'.EPrim (Prim.String ("uw_" ^ x
+                                                                     ^ (case v of
+                                                                            Client => ""
+                                                                          | Channel => " >> 32")
+                                                                     ^ " = ")), loc),
+                                             target), loc)
+
+                            val e =
+                                foldl (fn ((x, v), e) =>
+                                          (L'.ESeq (
+                                           (L'.EDml (L'.EStrcat (
+                                                     (L'.EPrim (Prim.String ("UPDATE uw_"
+                                                                             ^ tab
+                                                                             ^ " SET uw_"
+                                                                             ^ x
+                                                                             ^ " = NULL WHERE ")), loc),
+                                                     cond (x, v)), loc), loc),
+                                           e), loc))
+                                      e nullable
+
                             val e =
                                 case notNullable of
                                     [] => e
                                   | eb :: ebs =>
-                                    let
-                                        fun cond (x, v) =
-                                            (L'.EStrcat ((L'.EPrim (Prim.String ("uw_" ^ x
-                                                                                 ^ (case v of
-                                                                                        Client => ""
-                                                                                      | Channel => " >> 32")
-                                                                                 ^ " = ")), loc),
-                                                         target), loc)
-                                    in
-                                        (L'.ESeq (
-                                         (L'.EDml (foldl
-                                                       (fn (eb, s) =>
-                                                           (L'.EStrcat (s,
-                                                                        (L'.EStrcat ((L'.EPrim (Prim.String " AND "),
-                                                                                      loc),
-                                                                                     cond eb), loc)), loc))
-                                                       (L'.EStrcat ((L'.EPrim (Prim.String ("DELETE FROM uw_"
-                                                                                            ^ tab
-                                                                                            ^ " WHERE ")), loc),
-                                                                    cond eb), loc)
-                                                       ebs), loc),
-                                         e), loc)
-                                    end
+                                    (L'.ESeq (
+                                     (L'.EDml (foldl
+                                                   (fn (eb, s) =>
+                                                       (L'.EStrcat (s,
+                                                                    (L'.EStrcat ((L'.EPrim (Prim.String " AND "),
+                                                                                  loc),
+                                                                                 cond eb), loc)), loc))
+                                                   (L'.EStrcat ((L'.EPrim (Prim.String ("DELETE FROM uw_"
+                                                                                        ^ tab
+                                                                                        ^ " WHERE ")), loc),
+                                                                cond eb), loc)
+                                                   ebs), loc),
+                                     e), loc)
                         in
                             e
                         end
diff --git a/tests/whiteout.ur b/tests/whiteout.ur
new file mode 100644
index 00000000..5fb9d57b
--- /dev/null
+++ b/tests/whiteout.ur
@@ -0,0 +1,6 @@
+table t : { Chan : option (channel unit) }
+
+fun main () : transaction page =
+    ch <- channel;
+    dml (INSERT INTO t (Chan) VALUES ({[Some ch]}));
+    return <xml><body>Did it.</body></xml>
diff --git a/tests/whiteout.urp b/tests/whiteout.urp
new file mode 100644
index 00000000..a8c3d0af
--- /dev/null
+++ b/tests/whiteout.urp
@@ -0,0 +1,6 @@
+debug
+database dbname=whiteout
+sql whiteout.sql
+timeout 5
+
+whiteout