diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-04-04 17:18:41 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-04-04 17:18:41 -0400 |
| commit | 165c413fa6e074d791ef616a1b0d0bcf188be3b2 (patch) | |
| tree | 256d88decd7a8c8d4f86cb636b841dbfd544c2d0 | |
| parent | a0a4eb331eefb3a3a29f35fba4295101ed84aee0 (diff) | |
WHERE-dependent checking
| -rw-r--r-- | src/iflow.sml | 34 | ||||
| -rw-r--r-- | tests/policy.ur | 9 |
2 files changed, 35 insertions, 8 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index be49fa59..d5f677f4 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -508,15 +508,39 @@ fun queryProp rv oe e = 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 --git a/tests/policy.ur b/tests/policy.ur index b821d1d1..9cc230bf 100644 --- a/tests/policy.ur +++ b/tests/policy.ur @@ -8,8 +8,11 @@ table order : { Id : order, Fruit : fruit, Qty : int, Code : int } 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 @@ fun main () = x2 <- queryX (SELECT fruit.Nam, order.Qty FROM fruit, order - WHERE order.Fruit = fruit.Id) + WHERE fruit.Id = order.Fruit) (fn x => <xml><li>{[x.Fruit.Nam]}: {[x.Order.Qty]}</li></xml>); return <xml><body> |