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)) =