diff src/iflow.sml @ 1281:60e19545841b

equalAny policies
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Jul 2010 12:12:08 -0400
parents 3d06e0f7a6f3
children a9a500d22ebc
line wrap: on
line diff
--- a/src/iflow.sml	Tue Jul 27 11:42:30 2010 -0400
+++ b/src/iflow.sml	Tue Jul 27 12:12:08 2010 -0400
@@ -1228,7 +1228,7 @@
     val allowSend : atom list * exp list -> unit
     val send : check -> unit
 
-    val allowEqualKnown : { table : string, field : string } -> unit
+    val allowEqual : { table : string, field : string, known : bool } -> unit
     val mayTest : prop -> bool
 
     val allowInsert : atom list -> unit
@@ -1509,8 +1509,8 @@
 fun allowDelete v = deletable := v :: !deletable
 val delete = doable deletable
 
-val testable = ref ([] : { table : string, field : string } list)
-fun allowEqualKnown v = testable := v :: !testable
+val testable = ref ([] : { table : string, field : string, known : bool } list)
+fun allowEqual v = testable := v :: !testable
 fun mayTest p =
     case p of
         Reln (Eq, [e1, e2]) =>
@@ -1523,14 +1523,14 @@
             fun allowed (tab, v) =
                 case tab of
                     Proj (Var tab, fd) =>
-                    List.exists (fn {table = tab', field = fd'} =>
+                    List.exists (fn {table = tab', field = fd', known} =>
                                     fd' = fd
-                                    andalso tableInHyps (tab', tab)) (!testable)
-                    andalso Cc.check (db, AReln (Known, [v]))
+                                    andalso tableInHyps (tab', tab)
+                                    andalso (not known orelse Cc.check (db, AReln (Known, [v])))) (!testable)
                   | _ => false
         in
             if allowed (e1, e2) orelse allowed (e2, e1) then
-                (Cc.assert (db, AReln (Eq, [e1, e2]));
+                (assert [AReln (Eq, [e1, e2])];
                  true)
             else
                 false
@@ -2527,10 +2527,11 @@
                                  St.allowSend ([p], outs)
                              end
                            | _ => ())
-                      | PolEqualKnown {table = tab, field = nm} =>
+                      | PolEqual {table = tab, field = nm, known} =>
                         (case #1 tab of
-                             EPrim (Prim.String tab) => St.allowEqualKnown {table = String.extract (tab, 3, NONE),
-                                                                            field = nm}
+                             EPrim (Prim.String tab) => St.allowEqual {table = String.extract (tab, 3, NONE),
+                                                                       field = nm,
+                                                                       known = known}
                            | _ => ErrorMsg.errorAt loc "Table for 'equalKnown' policy isn't fully resolved.")
                 end