summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/c/urweb.c21
-rw-r--r--src/cjr_print.sml2
-rw-r--r--src/elab_env.sml72
-rw-r--r--src/monoize.sml57
-rw-r--r--tests/whiteout.ur6
-rw-r--r--tests/whiteout.urp6
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-30 17:21:21 +0000