Progress towards invalidation based on equalities of fields.

8 files changed, 368 insertions, 352 deletions

diff --git a/caching-tests/test.db b/caching-tests/test.db
index 66b6ad88..a4661341 100644
--- a/caching-tests/test.db
+++ b/caching-tests/test.db
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index c150631c..56310b81 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -3400,19 +3400,24 @@ fun p_file env (ds, ps) =
                           let val i = Int.toString index
                               fun paramRepeat itemi sep =
                                   let
-                                      val rec f =
-                                       fn 0 => itemi (Int.toString 0)
-                                        | n => f (n-1) ^ itemi (Int.toString n)
+                                      fun f n =
+                                          if n < 0 then ""
+                                          else if n = 0 then itemi (Int.toString 0)
+                                          else f (n-1) ^ sep ^ itemi (Int.toString n)
                                   in
                                       f (params - 1)
                                   end
-                              val args = paramRepeat (fn p => "uw_Basis_string p" ^ p) ", "
+                              fun paramRepeatInit itemi sep =
+                                  if params = 0 then "" else sep ^ paramRepeat itemi sep
+                              val args = paramRepeatInit (fn p => "uw_Basis_string p" ^ p) ", "
                               val decls = paramRepeat (fn p => "uw_Basis_string param" ^ i ^ "_" ^ p ^ " = NULL;") "\n"
                               val sets = paramRepeat (fn p => "param" ^ i ^ "_" ^ p
                                                              ^ " = strdup(p" ^ p ^ ");") "\n"
                               val frees = paramRepeat (fn p => "free(param" ^ i ^ "_" ^ p ^ ");") "\n"
-                              val eqs = paramRepeat (fn p => "strcmp(param" ^ i ^ "_" ^ p
-                                                             ^ ", p" ^ p ^ ")") " || "
+                              (* Starting || makes logic easier when there are no parameters. *)
+                              val eqs = paramRepeatInit (fn p => "strcmp(param" ^ i ^ "_" ^ p
+                                                                 ^ ", p" ^ p ^ ")")
+                                                        " || "
                           in box [string "static char *cacheQuery",
                                   string i,
                                   string " = NULL;",
@@ -3425,14 +3430,14 @@ fun p_file env (ds, ps) =
                                   newline,
                                   string "static uw_Basis_string uw_Sqlcache_check",
                                   string i,
-                                  string "(uw_context ctx, ",
+                                  string "(uw_context ctx",
                                   string args,
                                   string ") {\n puts(\"SQLCACHE: checked ",
                                   string i,
                                   string ".\");\n if (cacheQuery",
                                   string i,
                                   (* ASK: is returning the pointer okay? Should we duplicate? *)
-                                  string " == NULL || ",
+                                  string " == NULL",
                                   string eqs,
                                   string ") {\n puts(\"miss D:\");\n uw_recordingStart(ctx);\n return NULL;\n } else {\n puts(\"hit :D\");\n uw_write(ctx, cacheWrite",
                                   string i,
@@ -3442,7 +3447,7 @@ fun p_file env (ds, ps) =
                                   newline,
                                   string "static uw_unit uw_Sqlcache_store",
                                   string i,
-                                  string "(uw_context ctx, uw_Basis_string s, ",
+                                  string "(uw_context ctx, uw_Basis_string s",
                                   string args,
                                   string ") {\n free(cacheQuery",
                                   string i,
diff --git a/src/iflow.sml b/src/iflow.sml
index 40cf8993..f68d8f72 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -16,7 +16,7 @@
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
- * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
@@ -115,36 +115,36 @@ fun p_reln r es =
       | PCon1 s => box [string (s ^ "("),
                         p_list p_exp es,
                         string ")"]
-      | Eq => p_bop "=" es
-      | Ne => p_bop "<>" es
-      | Lt => p_bop "<" es
-      | Le => p_bop "<=" es
-      | Gt => p_bop ">" es
-      | Ge => p_bop ">=" es
+      | Cmp Eq => p_bop "=" es
+      | Cmp Ne => p_bop "<>" es
+      | Cmp Lt => p_bop "<" es
+      | Cmp Le => p_bop "<=" es
+      | Cmp Gt => p_bop ">" es
+      | Cmp Ge => p_bop ">=" es
 
 fun p_prop p =
     case p of
         True => string "True"
       | False => string "False"
       | Unknown => string "??"
-      | And (p1, p2) => box [string "(",
-                             p_prop p1,
-                             string ")",
-                             space,
-                             string "&&",
-                             space,
-                             string "(",
-                             p_prop p2,
-                             string ")"]
-      | Or (p1, p2) => box [string "(",
-                            p_prop p1,
-                            string ")",
-                            space,
-                            string "||",
-                            space,
-                            string "(",
-                            p_prop p2,
-                            string ")"]
+      | Lop (And, p1, p2) => box [string "(",
+                                  p_prop p1,
+                                  string ")",
+                                  space,
+                                  string "&&",
+                                  space,
+                                  string "(",
+                                  p_prop p2,
+                                  string ")"]
+      | Lop (Or, p1, p2) => box [string "(",
+                                 p_prop p1,
+                                 string ")",
+                                 space,
+                                 string "||",
+                                 space,
+                                 string "(",
+                                 p_prop p2,
+                                 string ")"]
       | Reln (r, es) => p_reln r es
       | Cond (e, p) => box [string "(",
                             p_exp e,
@@ -518,7 +518,7 @@ fun representative (db : database, e) =
                                                 Variety = Nothing,
                                                 Known = ref (!(#Known (unNode r))),
                                                 Ge = ref NONE})
-                                     
+
                             val r'' = ref (Node {Id = nodeId (),
                                                  Rep = ref NONE,
                                                  Cons = #Cons (unNode r),
@@ -529,7 +529,7 @@ fun representative (db : database, e) =
                             #Rep (unNode r) := SOME r'';
                             r'
                         end
-                      | _ => raise Contradiction                             
+                      | _ => raise Contradiction
                 end
     in
         rep e
@@ -687,9 +687,9 @@ fun assert (db, a) =
                         end
                       | _ => raise Contradiction
                 end
-              | (Eq, [e1, e2]) =>
+              | (Cmp Eq, [e1, e2]) =>
                 markEq (representative (db, e1), representative (db, e2))
-              | (Ge, [e1, e2]) =>
+              | (Cmp Ge, [e1, e2]) =>
                 let
                     val r1 = representative (db, e1)
                     val r2 = representative (db, e2)
@@ -734,14 +734,14 @@ fun check (db, a) =
              (case #Variety (unNode (representative (db, e))) of
                   Dt1 (f', _) => f' = f
                 | _ => false)
-           | (Eq, [e1, e2]) =>
+           | (Cmp Eq, [e1, e2]) =>
              let
                  val r1 = representative (db, e1)
                  val r2 = representative (db, e2)
              in
                  repOf r1 = repOf r2
              end
-           | (Ge, [e1, e2]) =>
+           | (Cmp Ge, [e1, e2]) =>
              let
                  val r1 = representative (db, e1)
                  val r2 = representative (db, e2)
@@ -848,7 +848,7 @@ fun setHyps (n', hs) =
             (hyps := (n', hs, ref false);
              Cc.clear db;
              app (fn a => Cc.assert (db, a)) hs)
-    end    
+    end
 
 fun useKeys () =
     let
@@ -872,7 +872,7 @@ fun useKeys () =
                                                               let
                                                                   val r =
                                                                       Cc.check (db,
-                                                                                AReln (Eq, [Proj (r1, f),
+                                                                                AReln (Cmp Eq, [Proj (r1, f),
                                                                                             Proj (r2, f)]))
                                                               in
                                                                   (*Print.prefaces "Fs"
@@ -888,7 +888,7 @@ fun useKeys () =
                                                                   r
                                                               end)) ks then
                                      (changed := true;
-                                      Cc.assert (db, AReln (Eq, [r1, r2]));
+                                      Cc.assert (db, AReln (Cmp Eq, [r1, r2]));
                                       finder (hyps, acc))
                                  else
                                      finder (hyps, a :: acc)
@@ -1115,7 +1115,7 @@ fun havocCookie cname =
         val (_, hs, _) = !hyps
     in
         hnames := n + 1;
-        hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
+        hyps := (n, List.filter (fn AReln (Cmp Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
     end
 
 fun check a = Cc.check (db, a)
@@ -1138,7 +1138,7 @@ fun removeDups (ls : (string * string) list) =
             val ls = removeDups ls
         in
             if List.exists (fn x' => x' = x) ls then
-                ls  
+                ls
             else
                 x :: ls
         end
@@ -1171,7 +1171,7 @@ fun expIn rv env rvOf =
                   | Null => inl (Func (DtCon0 "None", []))
                   | SqNot e =>
                     inr (case expIn e of
-                             inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
+                             inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
                            | inr _ => Unknown)
                   | Field (v, f) => inl (Proj (rvOf v, f))
                   | Computed _ => default ()
@@ -1181,15 +1181,15 @@ fun expIn rv env rvOf =
                         val e2 = expIn e2
                     in
                         inr (case (bo, e1, e2) of
-                                 (Exps f, inl e1, inl e2) => f (e1, e2)
-                               | (Props f, v1, v2) =>
+                                 (RCmp c, inl e1, inl e2) => Reln (Cmp c, [e1, e2])
+                               | (RLop l, v1, v2) =>
                                  let
                                      fun pin v =
                                          case v of
-                                             inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+                                             inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
                                            | inr p => p
                                  in
-                                     f (pin v1, pin v2)
+                                     Lop (l, pin v1, pin v2)
                                  end
                                | _ => Unknown)
                     end
@@ -1205,7 +1205,7 @@ fun expIn rv env rvOf =
                     (case expIn e of
                          inl e => inl (Func (Other f, [e]))
                        | _ => default ())
-                     
+
                   | Unmodeled => inl (Func (Other "allow", [rv ()]))
             end
     in
@@ -1219,8 +1219,8 @@ fun decomp {Save = save, Restore = restore, Add = add} =
                 True => (k () handle Cc.Contradiction => ())
               | False => ()
               | Unknown => ()
-              | And (p1, p2) => go p1 (fn () => go p2 k)
-              | Or (p1, p2) =>
+              | Lop (And, p1, p2) => go p1 (fn () => go p2 k)
+              | Lop (Or, p1, p2) =>
                 let
                     val saved = save ()
                 in
@@ -1351,7 +1351,7 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
                                    | SOME e =>
                                      let
                                          val p = case expIn e of
-                                                     inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+                                                     inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
                                                    | inr p => p
 
                                          val saved = #Save arg ()
@@ -1365,9 +1365,9 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
                             fun normal () = doWhere normal'
                         in
                             (case #Select r of
-                                 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
-                                 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
-                                      Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
+                                 [SqExp (Binop (RCmp bo, Count, SqConst (Prim.Int 0)), f)] =>
+                                 (case bo of
+                                      Gt =>
                                       (case #Cont arg of
                                            SomeCol _ => ()
                                          | AllCols k =>
@@ -1469,7 +1469,7 @@ fun evalExp env (e as (_, loc)) k =
                             evalExp env e (fn e => doArgs (es, e :: acc))
                 in
                     doArgs (es, [])
-                end            
+                end
     in
         case #1 e of
             EPrim p => k (Const p)
@@ -1519,7 +1519,7 @@ fun evalExp env (e as (_, loc)) k =
                                              ([], []) => (evalExp env' (#body rf) (fn _ => ());
                                                           St.reinstate saved;
                                                           default ())
-                                                         
+
                                            | (arg :: args, mode :: modes) =>
                                              evalExp env arg (fn arg =>
                                                                  let
@@ -1663,7 +1663,7 @@ fun evalExp env (e as (_, loc)) k =
                                            Save = St.stash,
                                            Restore = St.reinstate,
                                            Cont = AllCols (fn x =>
-                                                              (St.assert [AReln (Eq, [r, x])];
+                                                              (St.assert [AReln (Cmp Eq, [r, x])];
                                                                evalExp (acc :: r :: env) b k))} q
                               end)
           | EDml (e, _) =>
@@ -1697,15 +1697,15 @@ fun evalExp env (e as (_, loc)) k =
                    | Delete (tab, e) =>
                      let
                          val old = St.nextVar ()
-                                   
+
                          val expIn = expIn (Var o St.nextVar) env
                                            (fn "T" => Var old
                                              | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
 
                          val p = case expIn e of
-                                     inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" 
+                                     inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
                                    | inr p => p
-                                                          
+
                          val saved = St.stash ()
                      in
                          St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
@@ -1748,7 +1748,7 @@ fun evalExp env (e as (_, loc)) k =
                                                 (f, Proj (Var old, f)) :: fs) fs fs'
 
                          val p = case expIn e of
-                                           inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" 
+                                           inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
                                          | inr p => p
                          val saved = St.stash ()
                      in
@@ -1764,7 +1764,7 @@ fun evalExp env (e as (_, loc)) k =
                                            k (Recd []))
                                     handle Cc.Contradiction => ())
                      end)
-                     
+
           | ENextval (EPrim (Prim.String (_, seq)), _) =>
             let
                 val nv = St.nextVar ()
@@ -1780,7 +1780,7 @@ fun evalExp env (e as (_, loc)) k =
                 val e = Var (St.nextVar ())
                 val e' = Func (Other ("cookie/" ^ cname), [])
             in
-                St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
+                St.assert [AReln (Known, [e]), AReln (Cmp Eq, [e, e'])];
                 k e
             end
 
@@ -2159,7 +2159,7 @@ fun check (file : file) =
                              end
                            | _ => ())
                 end
-                                        
+
               | _ => ()
     in
         app decl (#1 file)
diff --git a/src/sources b/src/sources
index 7ad60517..33c01f94 100644
--- a/src/sources
+++ b/src/sources
@@ -171,6 +171,8 @@ $(SRC)/mono_print.sml
 $(SRC)/sql.sig
 $(SRC)/sql.sml
 
+$(SRC)/union_find_fn.sml
+
 $(SRC)/multimap_fn.sml
 
 $(SRC)/sqlcache.sig
diff --git a/src/sql.sig b/src/sql.sig
index cf2ae14a..5f5d1b23 100644
--- a/src/sql.sig
+++ b/src/sql.sig
@@ -26,24 +26,30 @@ datatype exp =
        | Recd of (string * exp) list
        | Proj of exp * string
 
-datatype reln =
-         Known
-       | Sql of string
-       | PCon0 of string
-       | PCon1 of string
-       | Eq
+datatype cmp =
+         Eq
        | Ne
        | Lt
        | Le
        | Gt
        | Ge
 
+datatype reln =
+         Known
+       | Sql of string
+       | PCon0 of string
+       | PCon1 of string
+       | Cmp of cmp
+
+datatype lop =
+         And
+       | Or
+
 datatype prop =
          True
        | False
        | Unknown
-       | And of prop * prop
-       | Or of prop * prop
+       | Lop of lop * prop * prop
        | Reln of reln * exp list
        | Cond of exp * prop
 
@@ -52,8 +58,8 @@ type 'a parser
 val parse : 'a parser -> Mono.exp -> 'a option
 
 datatype Rel =
-         Exps of exp * exp -> prop
-       | Props of prop * prop -> prop
+         RCmp of cmp
+       | RLop of lop
 
 datatype sqexp =
          SqConst of Prim.t
diff --git a/src/sql.sml b/src/sql.sml
index 7cfed022..59b4eac6 100644
--- a/src/sql.sml
+++ b/src/sql.sml
@@ -20,24 +20,30 @@ datatype exp =
        | Recd of (string * exp) list
        | Proj of exp * string
 
-datatype reln =
-         Known
-       | Sql of string
-       | PCon0 of string
-       | PCon1 of string
-       | Eq
+datatype cmp =
+         Eq
        | Ne
        | Lt
        | Le
        | Gt
        | Ge
 
+datatype reln =
+         Known
+       | Sql of string
+       | PCon0 of string
+       | PCon1 of string
+       | Cmp of cmp
+
+datatype lop =
+         And
+       | Or
+
 datatype prop =
          True
        | False
        | Unknown
-       | And of prop * prop
-       | Or of prop * prop
+       | Lop of lop * prop * prop
        | Reln of reln * exp list
        | Cond of exp * prop
 
@@ -183,8 +189,8 @@ val field = wrap (follow (opt (follow t_ident (const ".")))
                    | (NONE, f) => ("T", f)) (* Should probably deal with this MySQL/SQLite case better some day. *)
 
 datatype Rel =
-         Exps of exp * exp -> prop
-       | Props of prop * prop -> prop
+         RCmp of cmp
+       | RLop of lop
 
 datatype sqexp =
          SqConst of Prim.t
@@ -200,7 +206,7 @@ datatype sqexp =
        | Unmodeled
        | Null
 
-fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
+fun cmp s r = wrap (const s) (fn () => RCmp r)
 
 val sqbrel = altL [cmp "=" Eq,
                    cmp "<>" Ne,
@@ -208,8 +214,8 @@ val sqbrel = altL [cmp "=" Eq,
                    cmp "<" Lt,
                    cmp ">=" Ge,
                    cmp ">" Gt,
-                   wrap (const "AND") (fn () => Props And),
-                   wrap (const "OR") (fn () => Props Or)]
+                   wrap (const "AND") (fn () => RLop Or),
+                   wrap (const "OR") (fn () => RLop And)]
 
 datatype ('a, 'b) sum = inl of 'a | inr of 'b
 
diff --git a/src/sqlcache.sml b/src/sqlcache.sml
index d3c21371..59800ca3 100644
--- a/src/sqlcache.sml
+++ b/src/sqlcache.sml
@@ -1,6 +1,5 @@
 structure Sqlcache (* :> SQLCACHE *) = struct
 
-open Sql
 open Mono
 
 structure IS = IntBinarySet
@@ -10,13 +9,14 @@ structure SS = BinarySetFn(SK)
 structure SM = BinaryMapFn(SK)
 structure SIMM = MultimapFn(structure KeyMap = SM structure ValSet = IS)
 
-(* Filled in by cacheWrap during Sqlcache. *)
+(* Filled in by [cacheWrap] during [Sqlcache]. *)
 val ffiInfo : {index : int, params : int} list ref = ref []
 
 fun getFfiInfo () = !ffiInfo
 
 (* Some FFIs have writing as their only effect, which the caching records. *)
 val ffiEffectful =
+    (* TODO: have this less hard-coded. *)
     let
         val fs = SS.fromList ["htmlifyInt_w",
                               "htmlifyFloat_w",
@@ -40,7 +40,7 @@ val ffiEffectful =
 
 (* Effect analysis. *)
 
-(* Makes an exception for EWrite (which is recorded when caching). *)
+(* Makes an exception for [EWrite] (which is recorded when caching). *)
 fun effectful doPrint (effs : IS.set) (inFunction : bool) (bound : int) : Mono.exp -> bool =
     (* If result is true, expression is definitely effectful. If result is
        false, then expression is definitely not effectful if effs is fully
@@ -62,7 +62,6 @@ fun effectful doPrint (effs : IS.set) (inFunction : bool) (bound : int) : Mono.e
           | ECon (_, _, SOME e) => eff e
           | ENone _ => false
           | ESome (_, e) => eff e
-          (* TODO: use FFI whitelist. *)
           | EFfi (m, f) => if ffiEffectful (m, f) then tru "ffi" else false
           | EFfiApp (m, f, _) => if ffiEffectful (m, f) then tru "ffiapp" else false
           (* ASK: we're calling functions effectful if they have effects when
@@ -131,82 +130,188 @@ val effectfulMap =
     end
 
 
+(* Boolean formula normalization. *)
+
+datatype normalForm = Cnf | Dnf
+
+datatype 'atom formula =
+         Atom of 'atom
+       | Negate of 'atom formula
+       | Combo of normalForm * 'atom formula list
+
+val flipNf = fn Cnf => Dnf | Dnf => Cnf
+
+fun bind xs f = List.concat (map f xs)
+
+val rec cartesianProduct : 'a list list -> 'a list list =
+ fn [] => [[]]
+  | (xs :: xss) => bind (cartesianProduct xss)
+                        (fn ys => bind xs (fn x => [x :: ys]))
+
+fun normalize (negate : 'atom -> 'atom) (norm : normalForm) =
+ fn Atom x => [[x]]
+  | Negate f => map (map negate) (normalize negate (flipNf norm) f)
+  | Combo (n, fs) =>
+    let
+        val fss = bind fs (normalize negate n)
+    in
+        if n = norm then fss else cartesianProduct fss
+    end
+
+fun mapFormula mf =
+ fn Atom x => Atom (mf x)
+  | Negate f => Negate (mapFormula mf f)
+  | Combo (n, fs) => Combo (n, map (mapFormula mf) fs)
+
+
 (* SQL analysis. *)
 
-val useInjIfPossible =
- fn SqConst prim => Inj (EPrim (Prim.String (Prim.Normal, Prim.toString prim)),
-                         ErrorMsg.dummySpan)
-  | sqexp => sqexp
+val rec chooseTwos : 'a list -> ('a * 'a) list =
+ fn [] => []
+  | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys
+
+datatype atomExp =
+         QueryArg of int
+       | DmlRel of int
+       | Prim of Prim.t
+       | Field of string * string
 
-fun equalities (canonicalTable : string -> string) :
-    sqexp -> ((string * string) * Mono.exp) list option =
+structure AtomExpKey : ORD_KEY = struct
+
+type ord_key = atomExp
+
+val compare =
+ fn (QueryArg n1, QueryArg n2) => Int.compare (n1, n2)
+  | (QueryArg _, _) => LESS
+  | (_, QueryArg _) => GREATER
+  | (DmlRel n1, DmlRel n2) => Int.compare (n1, n2)
+  | (DmlRel _, _) => LESS
+  | (_, DmlRel _) => GREATER
+  | (Prim p1, Prim p2) => Prim.compare (p1, p2)
+  | (Prim _, _) => LESS
+  | (_, Prim _) => GREATER
+  | (Field (t1, f1), Field (t2, f2)) => String.compare (t1 ^ "." ^ f1, t2 ^ "." ^ f2)
+
+end
+
+structure UF = UnionFindFn(AtomExpKey)
+
+fun conflictMaps (fQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula,
+                  fDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula) =
     let
-        val rec eqs =
-         fn Binop (Exps f, e1, e2) =>
-            (* TODO: use a custom datatype in Exps instead of a function. *)
-            (case f (Var 1, Var 2) of
-                 Reln (Eq, [Var 1, Var 2]) =>
-                 let
-                     val (e1', e2') = (useInjIfPossible e1, useInjIfPossible e2)
-                 in
-                     case (e1', e2') of
-                         (Field (t, f), Inj i) => SOME [((canonicalTable t, f), i)]
-                       | (Inj i, Field (t, f)) => SOME [((canonicalTable t, f), i)]
-                       | _ => NONE
-                 end
-               | _ => NONE)
-          | Binop (Props f, e1, e2) =>
-            (* TODO: use a custom datatype in Props instead of a function. *)
-            (case f (True, False) of
-                 And (True, False) =>
-                 (case (eqs e1, eqs e2) of
-                      (SOME eqs1, SOME eqs2) => SOME (eqs1 @ eqs2)
-                    | _ => NONE)
-               | _ => NONE)
+        val toKnownEquality =
+         (* [NONE] here means unkown. Anything that isn't a comparison between
+            two knowns shouldn't be used, and simply dropping unused terms is
+            okay in disjunctive normal form. *)
+         fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2)
           | _ => NONE
+        val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list =
+            UF.classes
+            o List.foldl UF.union' UF.empty
+            o List.mapPartial toKnownEquality
+        fun addToEqs (eqs, n, e) =
+            case IM.find (eqs, n) of
+                (* Comparing to a constant seems better? *)
+                SOME (EPrim _) => eqs
+              | _ => IM.insert (eqs, n, e)
+        val accumulateEqs =
+         (* [NONE] means we have a contradiction. *)
+         fn (_, NONE) => NONE
+          | ((Prim p1, Prim p2), eqso) =>
+            (case Prim.compare (p1, p2) of
+                 EQUAL => eqso
+               | _ => NONE)
+          | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, EPrim p))
+          | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, ERel r))
+          | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, EPrim p))
+          | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, ERel r))
+          (* TODO: deal with equalities involving just [DmlRel]s and [Prim]s. *)
+          | (_, eqso) => eqso
+        val eqsOfClass : atomExp list -> Mono.exp' IM.map option =
+            List.foldl accumulateEqs (SOME IM.empty)
+            o chooseTwos
+        fun toAtomExps rel (cmp, e1, e2) =
+            let
+                val qa =
+                 (* Here [NONE] means unkown. *)
+                 fn Sql.SqConst p => SOME (Prim p)
+                  | Sql.Field tf => SOME (Field tf)
+                  | Sql.Inj (EPrim p, _) => SOME (Prim p)
+                  | Sql.Inj (ERel n, _) => SOME (rel n)
+                  (* We can't deal with anything else. *)
+                  | _ => NONE
+            in
+                (cmp, qa e1, qa e2)
+            end
+        fun negateCmp (cmp, e1, e2) =
+            (case cmp of
+                 Sql.Eq => Sql.Ne
+               | Sql.Ne => Sql.Eq
+               | Sql.Lt => Sql.Ge
+               | Sql.Le => Sql.Gt
+               | Sql.Gt => Sql.Le
+               | Sql.Ge => Sql.Lt,
+             e1, e2)
+        val markQuery = mapFormula (toAtomExps QueryArg)
+        val markDml = mapFormula (toAtomExps DmlRel)
+        val dnf = normalize negateCmp Dnf (Combo (Cnf, [markQuery fQuery, markDml fDml]))
+        (* If one of the terms in a conjunction leads to a contradiction, which
+           is represented by [NONE], drop the entire conjunction. *)
+        val sequenceOption = List.foldr (fn (SOME x, SOME xs) => SOME (x :: xs) | _ => NONE)
+                                        (SOME [])
     in
-        eqs
+        List.mapPartial (sequenceOption o map eqsOfClass o equivClasses) dnf
     end
 
-val equalitiesQuery =
- fn Query1 {From = tablePairs, Where = SOME exp, ...} =>
-    equalities
-        (* If we have [SELECT ... FROM T AS T' ...], use T, not T'. *)
-        (fn t =>
-            case List.find (fn (_, tAs) => t = tAs) tablePairs of
-                NONE => t
-              | SOME (tOrig, _) => tOrig)
-        exp
-  | Query1 {Where = NONE, ...} => SOME []
-  | _ => NONE
-
-val equalitiesDml =
- fn Insert (tab, eqs) => SOME (List.mapPartial
-                                   (fn (name, sqexp) =>
-                                       case useInjIfPossible sqexp of
-                                           Inj e => SOME ((tab, name), e)
-                                         | _ => NONE)
-                                   eqs)
-  | Delete (tab, exp) => equalities (fn _ => tab) exp
-  (* TODO: examine the updated values and not just the way they're filtered. *)
-  (* For example, UPDATE foo SET Id = 9001 WHERE Id = 42 should update both the
-     Id = 42 and Id = 9001 cache entries. Could also think of it as doing a
-     Delete immediately followed by an Insert. *)
-  | Update (tab, _, exp) => equalities (fn _ => tab) exp
+val rec sqexpToFormula =
+ fn Sql.SqTrue => Combo (Cnf, [])
+  | Sql.SqFalse => Combo (Dnf, [])
+  | Sql.SqNot e => Negate (sqexpToFormula e)
+  | Sql.Binop (Sql.RCmp c, e1, e2) => Atom (c, e1, e2)
+  | Sql.Binop (Sql.RLop l, p1, p2) => Combo (case l of Sql.And => Cnf | Sql.Or => Dnf,
+                                             [sqexpToFormula p1, sqexpToFormula p2])
+  (* ASK: any other sqexps that can be props? *)
+  | _ => raise Match
+
+val rec queryToFormula =
+ fn Sql.Query1 {From = tablePairs, Where = NONE, ...} => Combo (Cnf, [])
+  | Sql.Query1 {From = tablePairs, Where = SOME e, ...} =>
+    let
+        fun renameString table =
+            case List.find (fn (_, t) => table = t) tablePairs of
+                NONE => table
+              | SOME (realTable, _) => realTable
+        val renameSqexp =
+         fn Sql.Field (table, field) => Sql.Field (renameString table, field)
+          | e => e
+         fun renameAtom (cmp, e1, e2) = (cmp, renameSqexp e1, renameSqexp e2)
+    in
+        mapFormula renameAtom (sqexpToFormula e)
+    end
+  | Sql.Union (q1, q2) => Combo (Dnf, [queryToFormula q1, queryToFormula q2])
+
+val rec dmlToFormula =
+ fn Sql.Insert (table, vals) =>
+    Combo (Cnf, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals)
+  | Sql.Delete (_, wher) => sqexpToFormula wher
+  (* TODO: refine formula for the vals part, which could take into account the wher part. *)
+  | Sql.Update (table, vals, wher) => Combo (Dnf, [dmlToFormula (Sql.Insert (table, vals)),
+                                                   dmlToFormula (Sql.Delete (table, wher))])
 
 val rec tablesQuery =
- fn Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs)
-  | Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2)
+ fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs)
+  | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2)
 
 val tableDml =
- fn Insert (tab, _) => tab
-  | Delete (tab, _) => tab
-  | Update (tab, _, _) => tab
+ fn Sql.Insert (tab, _) => tab
+  | Sql.Delete (tab, _) => tab
+  | Sql.Update (tab, _, _) => tab
 
 
 (* Program instrumentation. *)
 
 fun stringExp s = (EPrim (Prim.String (Prim.Normal, s)), ErrorMsg.dummySpan)
+
 val stringTyp = (TFfi ("Basis", "string"), ErrorMsg.dummySpan)
 
 val sequence =
@@ -243,10 +348,10 @@ fun incRelsBound bound inc =
 
 val incRels = incRelsBound 0
 
-(* Filled in by instrumentQuery during Monoize, used during Sqlcache. *)
+(* Filled in by instrumentQuery during [Monoize], used during [Sqlcache]. *)
 val urlifiedRel0s : Mono.exp IM.map ref = ref IM.empty
 
-(* Used by Monoize. *)
+(* Used by [Monoize]. *)
 val instrumentQuery =
     let
         val nextQuery = ref 0
@@ -260,9 +365,12 @@ val instrumentQuery =
                     (ELet (varPrefix ^ Int.toString i, typ, query,
                            (* Uses a dummy FFI call to keep the urlified expression around, which
                               in turn keeps the declarations required for urlification safe from
-                              MonoShake. The dummy call is removed during Sqlcache. *)
-                           (* TODO: thread a Monoize.Fm.t through this module. *)
-                           (ESeq ((EFfiApp ("Sqlcache", "dummy", [(urlifiedRel0, stringTyp)]), loc),
+                              [MonoShake]. The dummy call is removed during [Sqlcache]. *)
+                           (* TODO: thread a [Monoize.Fm.t] through this module. *)
+                           (ESeq ((EFfiApp ("Sqlcache",
+                                            "dummy",
+                                            [(urlifiedRel0, stringTyp)]),
+                                   loc),
                                   (ERel 0, loc)),
                             loc)),
                      loc)
@@ -272,18 +380,18 @@ val instrumentQuery =
         iq
     end
 
-fun cacheWrap (query, i, urlifiedRel0, eqs) =
+fun cacheWrap (query, i, urlifiedRel0, args) =
     case query of
         (EQuery {state = typ, ...}, _) =>
         let
-            val () = ffiInfo := {index = i, params = length eqs} :: !ffiInfo
+            val () = ffiInfo := {index = i, params = length args} :: !ffiInfo
             val loc = ErrorMsg.dummySpan
             (* We ensure before this step that all arguments aren't effectful.
                by turning them into local variables as needed. *)
-            val args = map (fn (_, e) => (e, stringTyp)) eqs
-            val argsInc = map (fn (e, typ) => (incRels 1 e, typ)) args
-            val check = ffiAppCache ("check", i, args)
-            val store = ffiAppCache ("store", i, (urlifiedRel0, stringTyp) :: argsInc)
+            val argTyps = map (fn e => (e, stringTyp)) args
+            val argTypsInc = map (fn (e, typ) => (incRels 1 e, typ)) argTyps
+            val check = ffiAppCache ("check", i, argTyps)
+            val store = ffiAppCache ("store", i, (urlifiedRel0, stringTyp) :: argTypsInc)
             val rel0 = (ERel 0, loc)
         in
             (ECase (check,
@@ -315,18 +423,16 @@ fun addChecking file =
                         letBody) =>
             let
                 val loc = ErrorMsg.dummySpan
-                val chunks = chunkify origQueryText
+                val chunks = Sql.chunkify origQueryText
                 fun strcat (e1, e2) = (EStrcat (e1, e2), loc)
                 val (newQueryText, newVariables) =
                     (* Important that this is foldr (to oppose foldl below). *)
                     List.foldr
                         (fn (chunk, (qText, newVars)) =>
+                            (* Variable bound to the head of newBs will have the lowest index. *)
                             case chunk of
-                                Exp (e as (EPrim _, _)) => (strcat (e, qText), newVars)
-                              | Exp (e as (ERel _, _)) => (strcat (e, qText), newVars)
-                              | Exp (e as (ENamed _, _)) => (strcat (e, qText), newVars)
-                              (* Head of newVars has lowest index. *)
-                              | Exp e =>
+                                Sql.Exp (e as (EPrim _, _)) => (strcat (e, qText), newVars)
+                              | Sql.Exp e =>
                                 let
                                     val n = length newVars
                                 in
@@ -335,12 +441,15 @@ fun addChecking file =
                                        so we increment indices by n. *)
                                     (strcat ((ERel (~(n+1)), loc), qText), incRels n e :: newVars)
                                 end
-                              | String s => (strcat (stringExp s, qText), newVars))
+                              | Sql.String s => (strcat (stringExp s, qText), newVars))
                         (stringExp "", [])
                         chunks
                 fun wrapLets e' =
                     (* Important that this is foldl (to oppose foldr above). *)
-                    List.foldl (fn (v, e') => ELet ("sqlArgz", stringTyp, v, (e', loc))) e' newVariables
+                    List.foldl (fn (v, e') => ELet ("sqlArgz", stringTyp, v, (e', loc)))
+                               e'
+                               newVariables
+                val numArgs = length newVariables
                 (* Increment once for each new variable just made. *)
                 val queryExp = incRels (length newVariables)
                                        (EQuery {query = newQueryText,
@@ -352,6 +461,7 @@ fun addChecking file =
                                         queryLoc)
                 val (EQuery {query = queryText, ...}, _) = queryExp
                 (* val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)); *)
+                val args = List.tabulate (numArgs, fn n => (ERel n, loc))
                 fun bind x f = Option.mapPartial f x
                 fun guard b x = if b then x else NONE
                 (* DEBUG: set first boolean argument to true to turn on printing. *)
@@ -359,16 +469,15 @@ fun addChecking file =
                 val attempt =
                     (* Ziv misses Haskell's do notation.... *)
                     guard (safe 0 queryText andalso safe 0 initial andalso safe 2 body) (
-                    bind (parse query queryText) (fn queryParsed =>
+                    bind (Sql.parse Sql.query queryText) (fn queryParsed =>
                     bind (indexOfName v) (fn i =>
-                    bind (equalitiesQuery queryParsed) (fn eqs =>
                     bind (IM.find (!urlifiedRel0s, i)) (fn urlifiedRel0 =>
                     SOME (wrapLets (ELet (v, t,
-                                          cacheWrap (queryExp, i, urlifiedRel0, eqs),
+                                          cacheWrap (queryExp, i, urlifiedRel0, args),
                                           incRelsBound 1 (length newVariables) letBody)),
                           SS.foldr (fn (tab, qi) => SIMM.insert (qi, tab, i))
                                    queryInfo
-                                   (tablesQuery queryParsed)))))))
+                                   (tablesQuery queryParsed))))))
             in
                 case attempt of
                     SOME pair => pair
@@ -380,6 +489,22 @@ fun addChecking file =
         fileMapfold (fn exp => fn state => doExp state exp) file SIMM.empty
     end
 
+fun invalidations (nQueryArgs, query, dml) =
+    let
+        val loc = ErrorMsg.dummySpan
+        val optionToExp =
+         fn NONE => (ENone stringTyp, loc)
+          | SOME e => (ESome (stringTyp, (e, loc)), loc)
+        fun eqsToInvalidation eqs =
+            let
+                fun inv n = if n < 0 then [] else optionToExp (IM.find (eqs, n)) :: inv (n - 1)
+            in
+                inv (nQueryArgs - 1)
+            end
+    in
+        map (map eqsToInvalidation) (conflictMaps (queryToFormula query, dmlToFormula dml))
+    end
+
 fun addFlushing (file, queryInfo) =
     let
         val allIndices : int list = SM.foldr (fn (x, acc) => IS.listItems x @ acc) [] queryInfo
@@ -388,7 +513,7 @@ fun addFlushing (file, queryInfo) =
          fn dmlExp as EDml (dmlText, _) =>
             let
                 val indices =
-                    case parse dml dmlText of
+                    case Sql.parse Sql.dml dmlText of
                         SOME dmlParsed => SIMM.findList (queryInfo, tableDml dmlParsed)
                       | NONE => allIndices
             in
@@ -408,179 +533,4 @@ fun go file =
          file'
     end
 
-
-(* BEGIN OLD
-
-fun intExp (n, loc) = (EPrim (Prim.Int (Int64.fromInt n)), loc)
-fun intTyp loc = (TFfi ("Basis", "int"), loc)
-fun stringExp (s, loc) = (EPrim (Prim.String (Prim.Normal, s)), loc)
-
-fun boolPat (b, loc) = (PCon (Enum,
-                              PConFfi {mod = "Basis", datatyp = "bool", arg = NONE,
-                                       con = if b then "True" else "False"},
-                              NONE),
-                        loc)
-fun boolTyp loc = (TFfi ("Basis", "int"), loc)
-
-fun ffiAppExp (module, func, index, args, loc) =
-    (EFfiApp (module, func ^ Int.toString index, args), loc)
-
-val sequence =
- fn ((exp :: exps), loc) =>
-    List.foldl (fn (exp, seq) => (ESeq (seq, exp), loc)) exp exps
-  | _ => raise Match
-
-fun antiguardUnit (cond, exp, loc) =
-    (ECase (cond,
-            [(boolPat (false, loc), exp),
-             (boolPat (true, loc), (ERecord [], loc))],
-            {disc = boolTyp loc, result = (TRecord [], loc)}),
-     loc)
-
-fun underAbs f (exp as (exp', loc)) =
-    case exp' of
-        EAbs (x, y, z, body) => (EAbs (x, y, z, underAbs f body), loc)
-      | _ => f exp
-
-
-val rec tablesRead =
- fn Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs)
-  | Union (q1, q2) => SS.union (tablesRead q1, tablesRead q2)
-
-val tableWritten =
- fn Insert (tab, _) => tab
-  | Delete (tab, _) => tab
-  | Update (tab, _, _) => tab
-
-fun tablesInExp' exp' =
-    let
-        val nothing = {read = SS.empty, written = SS.empty}
-    in
-        case exp' of
-            EQuery {query = e, ...} =>
-            (case parse query e of
-                 SOME q => {read = tablesRead q, written = SS.empty}
-               | NONE => nothing)
-          | EDml (e, _) =>
-            (case parse dml e of
-                 SOME q => {read = SS.empty, written = SS.singleton (tableWritten q)}
-               | NONE => nothing)
-          | _ => nothing
-    end
-
-val tablesInExp =
-    let
-        fun addTables (exp', {read, written}) =
-            let
-                val {read = r, written = w} = tablesInExp' exp'
-            in
-                {read = SS.union (r, read), written = SS.union (w, written)}
-            end
-    in
-        MonoUtil.Exp.fold {typ = #2, exp = addTables}
-                          {read = SS.empty, written = SS.empty}
-    end
-
-fun addCacheCheck (index, exp) =
-    let
-        fun f (body as (_, loc)) =
-            let
-                val check = ffiAppExp ("Cache", "check", index, loc)
-                val store = ffiAppExp ("Cache", "store", index, loc)
-            in
-                antiguardUnit (check, sequence ([body, store], loc), loc)
-            end
-    in
-        underAbs f exp
-    end
-
-fun addCacheFlush (exp, tablesToIndices) =
-    let
-        fun addIndices (table, indices) = IS.union (indices, SIMM.find (tablesToIndices, table))
-        fun f (body as (_, loc)) =
-            let
-                fun mapFfi func = List.map (fn i => ffiAppExp ("Cache", func, i, loc))
-                val flushes =
-                    IS.listItems (SS.foldr addIndices IS.empty (#written (tablesInExp body)))
-            in
-                sequence (mapFfi "flush" flushes @ [body] @ mapFfi "ready" flushes, loc)
-            end
-    in
-        underAbs f exp
-    end
-
-val handlerIndices =
-    let
-        val isUnit =
-         fn (TRecord [], _) => true
-          | _ => false
-        fun maybeAdd (d, soFar as {readers, writers}) =
-            case d of
-                DExport (Link ReadOnly, _, name, typs, typ, _) =>
-                if List.all isUnit (typ::typs)
-                then {readers = IS.add (readers, name), writers = writers}
-                else soFar
-              | DExport (_, _, name, _, _, _) => (* Not read only. *)
-                {readers = readers, writers = IS.add (writers, name)}
-              | _ => soFar
-    in
-        MonoUtil.File.fold {typ = #2, exp = #2, decl = maybeAdd}
-                           {readers = IS.empty, writers = IS.empty}
-    end
-
-fun fileFoldMapiSelected f init (file, indices) =
-    let
-        fun doExp (original as ((a, index, b, exp, c), state)) =
-            if IS.member (indices, index)
-            then let val (newExp, newState) = f (index, exp, state)
-                 in ((a, index, b, newExp, c), newState) end
-            else original
-        fun doDecl decl state =
-            let
-                val result =
-                    case decl of
-                        DVal x =>
-                        let val (y, newState) = doExp (x, state)
-                        in (DVal y, newState) end
-                      | DValRec xs =>
-                        let val (ys, newState) = ListUtil.foldlMap doExp state xs
-                        in (DValRec ys, newState) end
-                      | _ => (decl, state)
-            in
-                Search.Continue result
-            end
-        fun nada x y = Search.Continue (x, y)
-    in
-        case MonoUtil.File.mapfold {typ = nada, exp = nada, decl = doDecl} file init of
-            Search.Continue x => x
-          | _ => raise Match (* Should never happen. *)
-    end
-
-fun fileMapSelected f = #1 o fileFoldMapiSelected (fn (_, x, _) => (f x, ())) ()
-
-val addCacheChecking =
-    let
-        fun f (index, exp, tablesToIndices) =
-            (addCacheCheck (index, exp),
-             SS.foldr (fn (table, tsToIs) => SIMM.insert (tsToIs, table, index))
-                      tablesToIndices
-                      (#read (tablesInExp exp)))
-    in
-        fileFoldMapiSelected f (SM.empty)
-    end
-
-fun addCacheFlushing (file, tablesToIndices, writers) =
-    fileMapSelected (fn exp => addCacheFlush (exp, tablesToIndices)) (file, writers)
-
-fun go file =
-    let
-        val {readers, writers} = handlerIndices file
-        val (fileWithChecks, tablesToIndices) = addCacheChecking (file, readers)
-    in
-        ffiIndices := IS.listItems readers;
-        addCacheFlushing (fileWithChecks, tablesToIndices, writers)
-    end
-
-END OLD *)
-
 end
diff --git a/src/union_find_fn.sml b/src/union_find_fn.sml
new file mode 100644
index 00000000..42b2d4d7
--- /dev/null
+++ b/src/union_find_fn.sml
@@ -0,0 +1,47 @@
+functor UnionFindFn(K : ORD_KEY) = struct
+
+structure M = BinaryMapFn(K)
+structure S = BinarySetFn(K)
+
+datatype entry =
+         Set of S.set
+       | Pointer of K.ord_key
+
+(* First map is the union-find tree, second stores equivalence classes. *)
+type unionFind = entry M.map ref * S.set M.map
+
+val empty : unionFind = (ref M.empty, M.empty)
+
+fun findPair (uf, x) =
+    case M.find (!uf, x) of
+        NONE => (S.singleton x, x)
+      | SOME (Set set) => (set, x)
+      | SOME (Pointer parent) =>
+        let
+            val (set, rep) = findPair (uf, parent)
+        in
+            uf := M.insert (!uf, x, Pointer rep);
+            (set, rep)
+        end
+
+fun find ((uf, _), x) = (S.listItems o #1 o findPair) (uf, x)
+
+fun classes (_, cs) = (map S.listItems o M.listItems) cs
+
+fun union ((uf, cs), x, y) =
+    let
+        val (xSet, xRep) = findPair (uf, x)
+        val (ySet, yRep) = findPair (uf, y)
+        val xySet = S.union (xSet, ySet)
+    in
+        (ref (M.insert (M.insert (!uf, yRep, Pointer xRep),
+                        xRep, Set xySet)),
+         M.insert (case M.find (cs, yRep) of
+                       NONE => cs
+                     | SOME _ => #1 (M.remove (cs, yRep)),
+                   xRep, xySet))
+    end
+
+fun union' ((x, y), uf) = union (uf, x, y)
+
+end