Roll back WHERE checking

10 files changed, 18 insertions, 129 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 8bc2b6ea..f6141bc7 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -819,11 +819,6 @@ 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
-
 val also : sql_policy -> sql_policy -> sql_policy
 
 val debug : string -> transaction unit
diff --git a/src/iflow.sml b/src/iflow.sml
index c70240a7..92e568a1 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1228,9 +1228,6 @@ structure St :> sig
     val allowSend : atom list * exp list -> unit
     val send : check -> unit
 
-    val allowEqual : { table : string, field : string, known : bool } -> unit
-    val mayTest : prop -> bool
-
     val allowInsert : atom list -> unit
     val insert : ErrorMsg.span -> unit
 
@@ -1509,40 +1506,11 @@ val deletable = ref ([] : atom list list)
 fun allowDelete v = deletable := v :: !deletable
 val delete = doable deletable
 
-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]) =>
-        let
-            val (_, hs, _) = !hyps
-
-            fun tableInHyps (tab, x) = List.exists (fn AReln (Sql tab', [Var x']) => tab' = tab andalso x' = x
-                                                     | _ => false) hs
-
-            fun allowed (tab, v) =
-                case tab of
-                    Proj (Var tab, fd) =>
-                    List.exists (fn {table = tab', field = fd', known} =>
-                                    fd' = fd
-                                    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
-                (assert [AReln (Eq, [e1, e2])];
-                 true)
-            else
-                false
-        end
-      | _ => false
-
 fun reset () = (Cc.clear db;
                 path := [];
                 hyps := (0, [], ref false);
                 nvar := 0;
                 sendable := [];
-                testable := [];
                 insertable := [];
                 updatable := [];
                 deletable := [])
@@ -1692,8 +1660,7 @@ type 'a doQuery = {
      Add : atom -> unit,
      Save : unit -> 'a,
      Restore : 'a -> unit,
-     Cont : queryMode,
-     Send : exp -> unit
+     Cont : queryMode
 }
 
 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
@@ -1732,24 +1699,24 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
                             val saved = #Save arg ()
                             fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
 
-                            fun leavesE e =
+                            fun usedFields e =
                                 case e of
-                                    Const _ => []
-                                  | Var _ => []
-                                  | Lvar _ => []
-                                  | Func (_, es) => List.concat (map leavesE es)
-                                  | Recd xes => List.concat (map (leavesE o #2) xes)
-                                  | Proj _ => [e]
-
-                            fun leavesP p =
-                                case p of
-                                    True => []
-                                  | False => []
-                                  | Unknown => []
-                                  | And (p1, p2) => leavesP p1 @ leavesP p2
-                                  | Or (p1, p2) => leavesP p1 @ leavesP p2
-                                  | Reln (_, es) => List.concat (map leavesE es)
-                                  | Cond (e, p) => e :: leavesP p
+                                    SqConst _ => []
+                                  | SqTrue => []
+                                  | SqFalse => []
+                                  | Null => []
+                                  | SqNot e => usedFields e
+                                  | Field (v, f) => [(false, Proj (rvOf v, f))]
+                                  | Computed _ => []
+                                  | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
+                                  | SqKnown _ => []
+                                  | Inj e =>
+                                    (case deinj (#Env arg) e of
+                                         NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
+                                                  [])
+                                       | SOME e => [(true, e)])
+                                  | SqFunc (_, e) => usedFields e
+                                  | Unmodeled => []
 
                             fun normal' () =
                                 case #Cont arg of
@@ -1802,17 +1769,8 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
                                                      inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
                                                    | inr p => p
 
-                                         fun getConjuncts p =
-                                             case p of
-                                                 And (p1, p2) => getConjuncts p1 @ getConjuncts p2
-                                               | _ => [p]
-
                                          val saved = #Save arg ()
-
-                                         val conjs = getConjuncts p
-                                         val conjs = List.filter (not o St.mayTest) conjs
                                      in
-                                         app (fn p => app (#Send arg) (leavesP p)) conjs;
                                          decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
                                                 p (fn () => final () handle Cc.Contradiction => ());
                                          #Restore arg saved
@@ -2118,7 +2076,6 @@ fun evalExp env (e as (_, loc)) k =
                                            Add = fn a => St.assert [a],
                                            Save = St.stash,
                                            Restore = St.reinstate,
-                                           Send = fn e => St.send (e, loc),
                                            Cont = AllCols (fn x =>
                                                               (St.assert [AReln (Eq, [r, x])];
                                                                evalExp (acc :: r :: env) b k))} q
@@ -2491,7 +2448,6 @@ fun check file =
                                          Add = fn a => atoms := a :: !atoms,
                                          Save = fn () => !atoms,
                                          Restore = fn ls => atoms := ls,
-                                         Send = fn _ => (),
                                          Cont = SomeCol (fn r => k (rev (!atoms), r))}
 
                     fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
@@ -2527,12 +2483,6 @@ fun check file =
                                  St.allowSend ([p], outs)
                              end
                            | _ => ())
-                      | PolEqual {table = tab, field = nm, known} =>
-                        (case #1 tab of
-                             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 0db9a684..9a960cd0 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -129,7 +129,6 @@ datatype policy =
        | PolDelete of exp
        | PolUpdate of exp
        | PolSequence of exp
-       | 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 74467e08..25a8e9d8 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -429,13 +429,6 @@ fun p_policy env pol =
       | PolSequence e => box [string "sendOwnIds",
                               space,
                               p_exp env e]
-      | 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 581f1357..50c4b387 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -67,7 +67,6 @@ fun shake file =
                                    | PolDelete e1 => e1
                                    | PolUpdate e1 => e1
                                    | PolSequence e1 => e1
-                                   | PolEqual {table = e1, ...} => e1
                     in
                         usedVars st e1
                     end
diff --git a/src/mono_util.sml b/src/mono_util.sml
index b0baa395..6bbbecb1 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -556,9 +556,6 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
               | PolSequence e =>
                 S.map2 (mfe ctx e,
                         PolSequence)
-              | PolEqual {table = tab, field = nm, known = b} =>
-                S.map2 (mfe ctx tab,
-                        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 f72c76a0..d43002cb 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3804,24 +3804,6 @@ fun monoDecl (env, fm) (all as (d, loc)) =
                                     (e, L'.PolUpdate)
                                   | L.EFfiApp ("Basis", "sendOwnIds", [e]) =>
                                     (e, L'.PolSequence)
-                                  | L.EApp ((L.ECApp
-                                             ((L.ECApp
-                                                   ((L.ECApp
-                                                         ((L.ECApp
-                                                               ((L.EFfi ("Basis", "equalKnown"), _), nm), _), _), _),
-                                                    _), _), _), _), tab) =>
-                                    (case #1 nm of
-                                         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))
 
                             val (e, fm) = monoExp (env, St.empty, fm) e
diff --git a/tests/equalKnown.ur b/tests/equalKnown.ur
deleted file mode 100644
index 4af32490..00000000
--- a/tests/equalKnown.ur
+++ /dev/null
@@ -1,24 +0,0 @@
-type fruit = int
-table fruit : { Id : fruit, Nam : string, Weight : float, Secret : string }
-  PRIMARY KEY Id,
-  CONSTRAINT Nam UNIQUE Nam
-
-policy sendClient (SELECT fruit.Id, fruit.Nam
-                   FROM fruit)
-
-policy sendClient (SELECT fruit.Weight
-                   FROM fruit
-                   WHERE known(fruit.Secret))
-
-policy equalKnown[#Secret] fruit
-
-fun main () =
-    x1 <- queryX (SELECT fruit.Id, fruit.Nam, fruit.Weight
-                  FROM fruit
-                  WHERE fruit.Nam = "apple"
-                    AND fruit.Secret = "tasty")
-                 (fn x => <xml><li>{[x.Fruit.Id]}: {[x.Fruit.Nam]}, {[x.Fruit.Weight]}</li></xml>);
-
-    return <xml><body>
-      <ul>{x1}</ul>
-    </body></xml>
diff --git a/tests/equalKnown.urp b/tests/equalKnown.urp
deleted file mode 100644
index 380321fd..00000000
--- a/tests/equalKnown.urp
+++ /dev/null
@@ -1 +0,0 @@
-equalKnown
diff --git a/tests/equalKnown.urs b/tests/equalKnown.urs
deleted file mode 100644
index 6ac44e0b..00000000
--- a/tests/equalKnown.urs
+++ /dev/null
@@ -1 +0,0 @@
-val main : unit -> transaction page