Mercurial > urweb
changeset 1281:60e19545841b
equalAny policies
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 27 Jul 2010 12:12:08 -0400 |
| parents | 3d06e0f7a6f3 |
| children | a9a500d22ebc |
| files | lib/ur/basis.urs src/iflow.sml src/mono.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml |
| diffstat | 7 files changed, 34 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Jul 27 11:42:30 2010 -0400 +++ b/lib/ur/basis.urs Tue Jul 27 12:12:08 2010 -0400 @@ -819,6 +819,8 @@ => sql_query [] ([Old = fs, New = fs] ++ tables) [] -> sql_policy +val equalAny : nm :: Name -> t ::: Type -> fs ::: {Type} -> ks ::: {{Unit}} + -> [[nm] ~ fs] => sql_table ([nm = t] ++ fs) ks -> sql_policy val equalKnown : nm :: Name -> t ::: Type -> fs ::: {Type} -> ks ::: {{Unit}} -> [[nm] ~ fs] => sql_table ([nm = t] ++ fs) ks -> sql_policy
--- 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
--- a/src/mono.sml Tue Jul 27 11:42:30 2010 -0400 +++ b/src/mono.sml Tue Jul 27 12:12:08 2010 -0400 @@ -129,7 +129,7 @@ | PolDelete of exp | PolUpdate of exp | PolSequence of exp - | PolEqualKnown of {table : exp, field : string} + | PolEqual of {table : exp, field : string, known : bool} datatype decl' = DDatatype of (string * int * (string * int * typ option) list) list
--- a/src/mono_print.sml Tue Jul 27 11:42:30 2010 -0400 +++ b/src/mono_print.sml Tue Jul 27 12:12:08 2010 -0400 @@ -429,11 +429,13 @@ | PolSequence e => box [string "sendOwnIds", space, p_exp env e] - | PolEqualKnown {table = tab, field = nm} => box [string "equalKnown[", - string nm, - string "]", - space, - p_exp env tab] + | PolEqual {table = tab, field = nm, known} => box [string "equal", + string (if known then "Known" else "Any"), + string "[", + string nm, + string "]", + space, + p_exp env tab] fun p_decl env (dAll as (d, _) : decl) = case d of
--- a/src/mono_shake.sml Tue Jul 27 11:42:30 2010 -0400 +++ b/src/mono_shake.sml Tue Jul 27 12:12:08 2010 -0400 @@ -67,7 +67,7 @@ | PolDelete e1 => e1 | PolUpdate e1 => e1 | PolSequence e1 => e1 - | PolEqualKnown {table = e1, ...} => e1 + | PolEqual {table = e1, ...} => e1 in usedVars st e1 end
--- a/src/mono_util.sml Tue Jul 27 11:42:30 2010 -0400 +++ b/src/mono_util.sml Tue Jul 27 12:12:08 2010 -0400 @@ -556,9 +556,9 @@ | PolSequence e => S.map2 (mfe ctx e, PolSequence) - | PolEqualKnown {table = tab, field = nm} => + | PolEqual {table = tab, field = nm, known = b} => S.map2 (mfe ctx tab, - fn tab => PolEqualKnown {table = tab, field = nm}) + fn tab => PolEqual {table = tab, field = nm, known = b}) and mfvi ctx (x, n, t, e, s) = S.bind2 (mft t,
--- a/src/monoize.sml Tue Jul 27 11:42:30 2010 -0400 +++ b/src/monoize.sml Tue Jul 27 12:12:08 2010 -0400 @@ -3811,7 +3811,16 @@ ((L.EFfi ("Basis", "equalKnown"), _), nm), _), _), _), _), _), _), _), tab) => (case #1 nm of - L.CName nm => (tab, fn tab => L'.PolEqualKnown {table = tab, field = nm}) + L.CName nm => (tab, fn tab => L'.PolEqual {table = tab, field = nm, known = true}) + | _ => (poly (); (e, L'.PolClient))) + | L.EApp ((L.ECApp + ((L.ECApp + ((L.ECApp + ((L.ECApp + ((L.EFfi ("Basis", "equalAny"), _), nm), _), _), _), + _), _), _), _), tab) => + (case #1 nm of + L.CName nm => (tab, fn tab => L'.PolEqual {table = tab, field = nm, known = false}) | _ => (poly (); (e, L'.PolClient))) | _ => (poly (); (e, L'.PolClient))