# HG changeset patch # User Adam Chlipala # Date 1270415921 14400 # Node ID 7cd11380cdf1cc5967c0b0f198f3ec0b6ea2d87a # Parent 7af5e2af64f49b397b8338a25d74e56ae9a5fd39 WHERE-dependent checking diff -r 7af5e2af64f4 -r 7cd11380cdf1 src/iflow.sml --- a/src/iflow.sml Sun Apr 04 17:11:22 2010 -0400 +++ b/src/iflow.sml Sun Apr 04 17:18:41 2010 -0400 @@ -508,15 +508,39 @@ else fs) [] (#Select r))]))) True (#From r) + + fun expIn e = + case e of + Field (v, f) => inl (Proj (Proj (Lvar rv, v), f)) + | Binop (bo, e1, e2) => + (case (expIn e1, expIn e2) of + (inr _, _) => inr Unknown + | (_, inr _) => inr Unknown + | (inl e1, inl e2) => + let + val bo = case bo of + "=" => SOME Eq + | _ => NONE + in + case bo of + NONE => inr Unknown + | SOME bo => inr (Reln (bo, [e1, e2])) + end) + + val p = case #Where r of + NONE => p + | SOME e => + case expIn e of + inr p' => And (p, p') + | _ => p in case oe of NONE => p | SOME oe => - And (p, - foldl (fn ((v, f), p) => - Or (p, - Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) - False (#Select r)) + And (p, foldl (fn ((v, f), p) => + Or (p, + Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)]))) + False (#Select r)) end fun evalExp env (e as (_, loc), st as (nv, p, sent)) = diff -r 7af5e2af64f4 -r 7cd11380cdf1 tests/policy.ur --- a/tests/policy.ur Sun Apr 04 17:11:22 2010 -0400 +++ b/tests/policy.ur Sun Apr 04 17:18:41 2010 -0400 @@ -8,8 +8,11 @@ PRIMARY KEY Id, CONSTRAINT Fruit FOREIGN KEY Fruit REFERENCES fruit(Id) -policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight FROM fruit) -policy query_policy (SELECT order.Id, order.Fruit, order.Qty FROM order) +policy query_policy (SELECT fruit.Id, fruit.Nam, fruit.Weight + FROM fruit) +policy query_policy (SELECT order.Id, order.Fruit, order.Qty + FROM order, fruit + WHERE order.Fruit = fruit.Id) fun main () = x1 <- queryX (SELECT fruit.Id, fruit.Nam @@ -18,7 +21,7 @@ x2 <- queryX (SELECT fruit.Nam, order.Qty FROM fruit, order - WHERE order.Fruit = fruit.Id) + WHERE fruit.Id = order.Fruit) (fn x =>

{[x.Fruit.Nam]}: {[x.Order.Qty]}

); return