Tweaks to table signatures and MonoOpt summarizing

2 files changed, 30 insertions, 10 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 07818a57..8902409d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2237,14 +2237,21 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
       | L.SgiTable (x, c, pe, ce) =>
         let
             val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
-            val x' = x ^ "_hidden_constraints"
-            val (env', hidden_n) = E.pushCNamed env x' cstK NONE
-            val hidden = (L'.CNamed hidden_n, loc)
 
             val (c', ck, gs') = elabCon (env, denv) c
             val pkey = cunif (loc, cstK)
             val visible = cunif (loc, cstK)
-            val uniques = (L'.CConcat (visible, hidden), loc)
+            val (env', ds, uniques) =
+                case (#1 pe, #1 ce) of
+                    (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
+                    let
+                        val x' = x ^ "_hidden_constraints"
+                        val (env', hidden_n) = E.pushCNamed env x' cstK NONE
+                        val hidden = (L'.CNamed hidden_n, loc)
+                    in
+                        (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc))
+                    end
+                  | _ => (env, [], visible)
 
             val ct = tableOf ()
             val ct = (L'.CApp (ct, c'), loc)
@@ -2272,8 +2279,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
             checkCon env' pe' pet pst;
             checkCon env' ce' cet cst;
 
-            ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
-              (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
+            (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
         end
 
       | L.SgiStr (x, sgn) =>
diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml
index bb23a21a..5e735b79 100644
--- a/src/mono_reduce.sml
+++ b/src/mono_reduce.sml
@@ -77,7 +77,7 @@ fun impure (e, _) =
       | EDml _ => true
       | ENextval _ => true
       | ESetval _ => true
-      | EUnurlify _ => true
+      | EUnurlify _ => false
       | EAbs _ => false
 
       | EPrim _ => false
@@ -257,8 +257,11 @@ datatype event =
          WritePage
        | ReadDb
        | WriteDb
+       | ReadCookie
+       | WriteCookie
        | UseRel
        | Unsure
+       | Abort
 
 fun p_event e =
     let
@@ -268,8 +271,11 @@ fun p_event e =
             WritePage => string "WritePage"
           | ReadDb => string "ReadDb"
           | WriteDb => string "WriteDb"
+          | ReadCookie => string "ReadCookie"
+          | WriteCookie => string "WriteCookie"
           | UseRel => string "UseRel"
           | Unsure => string "Unsure"
+          | Abort => string "Abort"
     end
 
 val p_events = Print.p_list p_event
@@ -377,6 +383,8 @@ fun reduce file =
                       | ENone _ => []
                       | ESome (_, e) => summarize d e
                       | EFfi _ => []
+                      | EFfiApp ("Basis", "get_cookie", [e]) =>
+                        summarize d e @ [ReadCookie]
                       | EFfiApp (m, x, es) =>
                         if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then
                             List.concat (map (summarize d) es) @ [Unsure]
@@ -440,9 +448,9 @@ fun reduce file =
                         end
                       | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
 
-                      | EError (e, _) => summarize d e @ [Unsure]
-                      | EReturnBlob {blob = e1, mimeType = e2, ...} => summarize d e1 @ summarize d e2 @ [Unsure]
-                      | ERedirect (e, _) => summarize d e @ [Unsure]
+                      | EError (e, _) => summarize d e @ [Abort]
+                      | EReturnBlob {blob = e1, mimeType = e2, ...} => summarize d e1 @ summarize d e2 @ [Abort]
+                      | ERedirect (e, _) => summarize d e @ [Abort]
 
                       | EWrite e => summarize d e @ [WritePage]
                                     
@@ -526,6 +534,8 @@ fun reduce file =
                                 val writesPage = does WritePage
                                 val readsDb = does ReadDb
                                 val writesDb = does WriteDb
+                                val readsCookie = does ReadCookie
+                                val writesCookie = does ReadCookie
 
                                 fun verifyUnused eff =
                                     case eff of
@@ -542,6 +552,10 @@ fun reduce file =
                                           | WritePage => not writesPage andalso verifyCompatible effs
                                           | ReadDb => not writesDb andalso verifyCompatible effs
                                           | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
+                                          | ReadCookie => not writesCookie andalso verifyCompatible effs
+                                          | WriteCookie => not writesCookie andalso not readsCookie
+                                                           andalso verifyCompatible effs
+                                          | Abort => true
                             in
                                 (*Print.prefaces "verifyCompatible"
                                                  [("e'", MonoPrint.p_exp env e'),