Mercurial > urweb
diff src/iflow.sml @ 1205:7cd11380cdf1
WHERE-dependent checking
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 04 Apr 2010 17:18:41 -0400 |
parents | 7af5e2af64f4 |
children | 772760df4c4c |
line wrap: on
line diff
--- 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)) =