diff options
| -rw-r--r-- | lib/ur/basis.urs | 2 | ||||
| -rw-r--r-- | src/iflow.sml | 21 | ||||
| -rw-r--r-- | src/mono.sml | 2 | ||||
| -rw-r--r-- | src/mono_print.sml | 12 | ||||
| -rw-r--r-- | src/mono_shake.sml | 2 | ||||
| -rw-r--r-- | src/mono_util.sml | 4 | ||||
| -rw-r--r-- | src/monoize.sml | 11 |
7 files changed, 34 insertions, 20 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 7b17dd05..8bc2b6ea 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -819,6 +819,8 @@ val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables] => 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 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 diff --git a/src/mono.sml b/src/mono.sml index 2f5ab117..0db9a684 100644 --- a/src/mono.sml +++ b/src/mono.sml @@ -129,7 +129,7 @@ datatype policy = | 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 diff --git a/src/mono_print.sml b/src/mono_print.sml index 693b5e3e..74467e08 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -429,11 +429,13 @@ fun p_policy env pol = | 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 diff --git a/src/mono_shake.sml b/src/mono_shake.sml index 6a5aefae..581f1357 100644 --- a/src/mono_shake.sml +++ b/src/mono_shake.sml @@ -67,7 +67,7 @@ fun shake file = | PolDelete e1 => e1 | PolUpdate e1 => e1 | PolSequence e1 => e1 - | PolEqualKnown {table = e1, ...} => e1 + | PolEqual {table = e1, ...} => e1 in usedVars st e1 end diff --git a/src/mono_util.sml b/src/mono_util.sml index cb01a958..b0baa395 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -556,9 +556,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} = | 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, diff --git a/src/monoize.sml b/src/monoize.sml index 5054cc9f..f72c76a0 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -3811,7 +3811,16 @@ fun monoDecl (env, fm) (all as (d, loc)) = ((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)) |