diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-07-27 12:12:08 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-07-27 12:12:08 -0400 |
| commit | a5d7c214f42af261d900af8a7ac042b807c2abe2 (patch) | |
| tree | 5795313dd42f572e6c02b89ac43664a466b42c92 /src/iflow.sml | |
| parent | 8179b6224c5d4eb3b3fbe48e6acf5d630138c3da (diff) | |
equalAny policies
Diffstat (limited to 'src/iflow.sml')
| -rw-r--r-- | src/iflow.sml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index bf75775b..c70240a7 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -1228,7 +1228,7 @@ structure St :> sig 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 @@ val deletable = ref ([] : atom list list) 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 mayTest p = 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 @@ fun check file = 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 |