sendOwnIds policies

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