summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/ur/basis.urs2
-rw-r--r--src/iflow.sml21
-rw-r--r--src/mono.sml2
-rw-r--r--src/mono_print.sml12
-rw-r--r--src/mono_shake.sml2
-rw-r--r--src/mono_util.sml4
-rw-r--r--src/monoize.sml11
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))