summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/basis.urs2
-rw-r--r--src/iflow.sml49
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_print.sml3
-rw-r--r--src/mono_shake.sml1
-rw-r--r--src/mono_util.sml3
-rw-r--r--src/monoize.sml2
7 files changed, 51 insertions, 10 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 3241cc9a..5a30f3f4 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -804,6 +804,8 @@ val sendClient : tables ::: {{Type}} -> exps ::: {Type}
-> [tables ~ exps] => sql_query [] tables exps
-> sql_policy
+val sendOwnIds : sql_sequence -> sql_policy
+
val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
=> sql_query [] ([New = fs] ++ tables) []
-> sql_policy
diff --git a/src/iflow.sml b/src/iflow.sml
index 3ff3d100..77f25a91 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -482,7 +482,7 @@ type database = {Vars : representative IM.map ref,
Consts : representative CM.map ref,
Con0s : representative SM.map ref,
Records : (representative SM.map * representative) list ref,
- Funcs : ((string * representative list) * representative) list ref }
+ Funcs : ((string * representative list) * representative) list ref}
fun database () = {Vars = ref IM.empty,
Consts = ref CM.empty,
@@ -847,6 +847,7 @@ fun assert (db, a) =
else
();
#Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
+
compactFuncs ())
and compactFuncs () =
@@ -1450,9 +1451,9 @@ fun expIn rv env rvOf =
let
fun default () =
let
- val (rvN, e) = rv rvN
+ val (rvN, e') = rv rvN
in
- (inl e, rvN)
+ (inl e', rvN)
end
in
case e of
@@ -1686,7 +1687,7 @@ fun insertProp rvN rv e =
let
val t =
case v of
- "New" => "$New"
+ "New" => t ^ "$New"
| _ => t
in
And (p, Reln (Sql t, [rvOf v]))
@@ -1767,7 +1768,7 @@ fun updateProp rvN rv e =
let
val t =
case v of
- "New" => "$New"
+ "New" => t ^ "$New"
| _ => t
in
And (p, Reln (Sql t, [rvOf v]))
@@ -1989,6 +1990,8 @@ fun evalExp env (e as (_, loc), st) =
let
val (st, nv) = St.nextVar st
in
+ (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
+ ("nv", p_exp (Var nv))];*)
(Var nv, st)
end
@@ -2233,7 +2236,7 @@ fun evalExp env (e as (_, loc), st) =
st es
in
(Recd [], St.addInsert (st, (loc, And (St.ambient st,
- Reln (Sql "$New", [Recd es])))))
+ Reln (Sql (tab ^ "$New"), [Recd es])))))
end
| Delete (tab, e) =>
let
@@ -2302,13 +2305,19 @@ fun evalExp env (e as (_, loc), st) =
| (inr p, st) => (p, st)
val p = And (p,
- And (Reln (Sql "$New", [Recd fs]),
+ And (Reln (Sql (tab ^ "$New"), [Recd fs]),
And (Reln (Sql "$Old", [Var old]),
Reln (Sql tab, [Var old]))))
in
(Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
end)
+ | ENextval (EPrim (Prim.String seq), _) =>
+ let
+ val (st, nv) = St.nextVar st
+ in
+ (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv]))))
+ end
| ENextval _ => default ()
| ESetval _ => default ()
@@ -2416,6 +2425,16 @@ fun check file =
in
(vals, inserts, deletes, updates, client, insert, delete, p :: update)
end
+ | PolSequence e =>
+ (case #1 e of
+ EPrim (Prim.String seq) =>
+ let
+ val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
+ val outs = [Lvar 0]
+ in
+ (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
+ end
+ | _ => (vals, inserts, deletes, updates, client, insert, delete, update))
end
| _ => (vals, inserts, deletes, updates, client, insert, delete, update)
@@ -2434,8 +2453,14 @@ fun check file =
if decompH p
(fn hyps =>
List.exists (fn p' =>
- decompG p'
- (fn goals => imply (hyps, goals, NONE)))
+ if decompG p'
+ (fn goals => imply (hyps, goals, NONE)) then
+ ((*reset ();
+ Print.prefaces "Match" [("hyp", p_prop p),
+ ("goal", p_prop p')];*)
+ true)
+ else
+ false)
pols) then
()
else
@@ -2487,7 +2512,11 @@ fun check file =
client
orelse tryCombos (0, client, True, [])
orelse (reset ();
- Print.preface ("Untenable hypotheses",
+ Print.preface ("Untenable hypotheses"
+ ^ (case fl of
+ Control Where => " (WHERE clause)"
+ | Control Case => " (case discriminee)"
+ | Data => " (returned data value)"),
Print.p_list p_atom hyps);
false)
end) then
diff --git a/src/mono.sml b/src/mono.sml
index 79cde237..9a960cd0 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -128,6 +128,7 @@ datatype policy =
| PolInsert of exp
| PolDelete of exp
| PolUpdate of exp
+ | PolSequence of exp
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 b8016ff8..25a8e9d8 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -426,6 +426,9 @@ fun p_policy env pol =
| PolUpdate e => box [string "mayUpdate",
space,
p_exp env e]
+ | PolSequence e => box [string "sendOwnIds",
+ space,
+ p_exp env e]
fun p_decl env (dAll as (d, _) : decl) =
case d of
diff --git a/src/mono_shake.sml b/src/mono_shake.sml
index 6b248636..b42c9535 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -65,6 +65,7 @@ fun shake file =
| PolInsert e1 => e1
| PolDelete e1 => e1
| PolUpdate e1 => e1
+ | PolSequence e1 => e1
in
usedVars st e1
end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 085b68f8..6bbbecb1 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -553,6 +553,9 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
| PolUpdate e =>
S.map2 (mfe ctx e,
PolUpdate)
+ | PolSequence e =>
+ S.map2 (mfe ctx e,
+ PolSequence)
and mfvi ctx (x, n, t, e, s) =
S.bind2 (mft t,
diff --git a/src/monoize.sml b/src/monoize.sml
index 601b690f..3983624b 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3752,6 +3752,8 @@ fun monoDecl (env, fm) (all as (d, loc)) =
(e, L'.PolDelete)
| L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "mayUpdate"), _), _), _), _), _), e) =>
(e, L'.PolUpdate)
+ | L.EFfiApp ("Basis", "sendOwnIds", [e]) =>
+ (e, L'.PolSequence)
| _ => (poly (); (e, L'.PolClient))
val (e, fm) = monoExp (env, St.empty, fm) e
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-16 23:04:19 +0000