Mercurial > urweb
changeset 684:f0224c7f12bb
Expunging nullable fields
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 29 Mar 2009 14:13:50 -0400 |
| parents | 9a2c18dab11d |
| children | c73c5fe72388 |
| files | src/c/urweb.c src/cjr_print.sml src/elab_env.sml src/monoize.sml tests/whiteout.ur tests/whiteout.urp |
| diffstat | 6 files changed, 111 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/src/c/urweb.c Sun Mar 29 13:30:01 2009 -0400 +++ b/src/c/urweb.c Sun Mar 29 14:13:50 2009 -0400 @@ -1869,8 +1869,13 @@ 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 @@ 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;
--- a/src/cjr_print.sml Sun Mar 29 13:30:01 2009 -0400 +++ b/src/cjr_print.sml Sun Mar 29 14:13:50 2009 -0400 @@ -2760,6 +2760,8 @@ 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
--- a/src/elab_env.sml Sun Mar 29 13:30:01 2009 -0400 +++ b/src/elab_env.sml Sun Mar 29 14:13:50 2009 -0400 @@ -190,6 +190,7 @@ | 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 @@ | 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 @@ | (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 @@ | 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 @@ 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 @@ | 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_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 @@ 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 @@ 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 @@ 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 @@ 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
--- a/src/monoize.sml Sun Mar 29 13:30:01 2009 -0400 +++ b/src/monoize.sml Sun Mar 29 14:13:50 2009 -0400 @@ -2500,33 +2500,44 @@ | _ => 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/whiteout.ur Sun Mar 29 14:13:50 2009 -0400 @@ -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>