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 | 7e8e31fc6375ba9a0b9db891c3ecbc89fbf6d374 (patch) | |
tree | 256d88decd7a8c8d4f86cb636b841dbfd544c2d0 /src/iflow.sml | |
parent | 20f0e57e0e9e418ef08ce8bdb202b6d10de1c86b (diff) |
WHERE-dependent checking
Diffstat (limited to 'src/iflow.sml')
-rw-r--r-- | src/iflow.sml | 34 |
1 files changed, 29 insertions, 5 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)) = |