(* Copyright (c) 2010, Adam Chlipala
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * - Redistributions of source code must retain the above copyright notice,
 *   this list of conditions and the following disclaimer.
 * - Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 * - The names of contributors may not be used to endorse or promote products
 *   derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * 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 
 * 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
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

structure Iflow :> IFLOW = struct

open Mono
open Sql

structure IS = IntBinarySet
structure IM = IntBinaryMap

structure SK = struct
type ord_key = string
val compare = String.compare
end

structure SS = BinarySetFn(SK)
structure SM = BinaryMapFn(SK)

val writers = ["htmlifyInt_w",
               "htmlifyFloat_w",
               "htmlifyString_w",
               "htmlifyBool_w",
               "htmlifyTime_w",
               "attrifyInt_w",
               "attrifyFloat_w",
               "attrifyString_w",
               "attrifyChar_w",
               "urlifyInt_w",
               "urlifyFloat_w",
               "urlifyString_w",
               "urlifyBool_w",
               "set_cookie"]

val writers = SS.addList (SS.empty, writers)

local
    open Print
    val string = PD.string
in

fun p_func f =
    string (case f of
                DtCon0 s => s
              | DtCon1 s => s
              | UnCon s => "un" ^ s
              | Other s => s)

fun p_exp e =
    case e of
        Const p => Prim.p_t p
      | Var n => string ("x" ^ Int.toString n)
      | Lvar n => string ("X" ^ Int.toString n)
      | Func (f, es) => box [p_func f,
                             string "(",
                             p_list p_exp es,
                             string ")"]
      | Recd xes => box [string "{",
                         p_list (fn (x, e) => box [string x,
                                                   space,
                                                   string "=",
                                                   space,
                                                   p_exp e]) xes,
                         string "}"]
      | Proj (e, x) => box [p_exp e,
                            string ("." ^ x)]

fun p_bop s es =
    case es of
        [e1, e2] => box [p_exp e1,
                         space,
                         string s,
                         space,
                         p_exp e2]
      | _ => raise Fail "Iflow.p_bop"

fun p_reln r es =
    case r of
        Known =>
        (case es of
             [e] => box [string "known(",
                         p_exp e,
                         string ")"]
           | _ => raise Fail "Iflow.p_reln: Known")
      | Sql s => box [string (s ^ "("),
                      p_list p_exp es,
                      string ")"]
      | PCon0 s => box [string (s ^ "("),
                        p_list p_exp es,
                        string ")"]
      | 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

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 ")"]
      | Reln (r, es) => p_reln r es
      | Cond (e, p) => box [string "(",
                            p_exp e,
                            space,
                            string "==",
                            space,
                            p_prop p,
                            string ")"]

end

fun isKnown e =
    case e of
        Const _ => true
      | Func (_, es) => List.all isKnown es
      | Recd xes => List.all (isKnown o #2) xes
      | Proj (e, _) => isKnown e
      | _ => false

fun simplify unif =
    let
        fun simplify e =
            case e of
                Const _ => e
              | Var _ => e
              | Lvar n =>
                (case IM.find (unif, n) of
                     NONE => e
                   | SOME e => simplify e)
              | Func (f, es) => Func (f, map simplify es)
              | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
              | Proj (e, s) => Proj (simplify e, s)
    in
        simplify
    end

datatype atom =
         AReln of reln * exp list
       | ACond of exp * prop

fun p_atom a =
    p_prop (case a of
                AReln x => Reln x
              | ACond x => Cond x)

(* Congruence closure *)
structure Cc :> sig
    type database

    exception Contradiction

    val database : unit -> database
    val clear : database -> unit

    val assert : database * atom -> unit
    val check : database * atom -> bool

    val p_database : database Print.printer

    val builtFrom : database * {Base : exp list, Derived : exp} -> bool

    val p_repOf : database -> exp Print.printer
end = struct

local
    val count = ref 0
in
fun nodeId () =
    let
        val n = !count
    in
        count := n + 1;
        n
    end
end

exception Contradiction
exception Undetermined

structure CM = BinaryMapFn(struct
                           type ord_key = Prim.t
                           val compare = Prim.compare
                           end)

datatype node = Node of {Id : int,
                         Rep : node ref option ref,
                         Cons : node ref SM.map ref,
                         Variety : variety,
                         Known : bool ref,
                         Ge : Int64.int option ref}

     and variety =
         Dt0 of string
       | Dt1 of string * node ref
       | Prim of Prim.t
       | Recrd of node ref SM.map ref * bool
       | Nothing

type representative = node ref

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}

fun database () = {Vars = ref IM.empty,
                   Consts = ref CM.empty,
                   Con0s = ref SM.empty,
                   Records = ref [],
                   Funcs = ref []}

fun clear (t : database) = (#Vars t := IM.empty;
                            #Consts t := CM.empty;
                            #Con0s t := SM.empty;
                            #Records t := [];
                            #Funcs t := [])

fun unNode n =
    case !n of
        Node r => r

open Print
val string = PD.string
val newline = PD.newline

fun p_rep n =
    case !(#Rep (unNode n)) of
        SOME n => p_rep n
      | NONE =>
        box [string (Int.toString (#Id (unNode n)) ^ ":"),
             space,
             case #Variety (unNode n) of
                 Nothing => string "?"
               | Dt0 s => string ("Dt0(" ^ s ^ ")")
               | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
                                   space,
                                   p_rep n,
                                   string ")"]
               | Prim p => Prim.p_t p
               | Recrd (ref m, b) => box [string "{",
                                          p_list (fn (x, n) => box [string x,
                                                                    space,
                                                                    string "=",
                                                                    space,
                                                                    p_rep n]) (SM.listItemsi m),
                                          string "}",
                                          if b then
                                              box [space,
                                                   string "(complete)"]
                                          else
                                              box []],
             if !(#Known (unNode n)) then
                 string " (known)"
             else
                 box [],
             case !(#Ge (unNode n)) of
                 NONE => box []
               | SOME n => string (" (>= " ^ Int64.toString n ^ ")")]

fun p_database (db : database) =
    box [string "Vars:",
         newline,
         p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
                                               space,
                                               string "=",
                                               space,
                                               p_rep n]) (IM.listItemsi (!(#Vars db)))]

fun repOf (n : representative) : representative =
    case !(#Rep (unNode n)) of
        NONE => n
      | SOME r =>
        let
            val r = repOf r
        in
            #Rep (unNode n) := SOME r;
            r
        end

fun markKnown r =
    let
        val r = repOf r
    in
        (*Print.preface ("markKnown", p_rep r);*)
        if !(#Known (unNode r)) then
            ()(*TextIO.print "Already known\n"*)
        else
            (#Known (unNode r) := true;
             SM.app markKnown (!(#Cons (unNode r)));
             case #Variety (unNode r) of
                 Dt1 (_, r) => markKnown r
               | Recrd (xes, _) => SM.app markKnown (!xes)
               | _ => ())
    end

fun representative (db : database, e) =
    let
        fun rep e =
            case e of
                Const p => (case CM.find (!(#Consts db), p) of
                                SOME r => repOf r
                              | NONE =>
                                let
                                    val r = ref (Node {Id = nodeId (),
                                                       Rep = ref NONE,
                                                       Cons = ref SM.empty,
                                                       Variety = Prim p,
                                                       Known = ref true,
                                                       Ge = ref (case p of
                                                                     Prim.Int n => SOME n
                                                                   | _ => NONE)})
                                in
                                    #Consts db := CM.insert (!(#Consts db), p, r);
                                    r
                                end)
              | Var n => (case IM.find (!(#Vars db), n) of
                              SOME r => repOf r
                            | NONE =>
                              let
                                  val r = ref (Node {Id = nodeId (),
                                                     Rep = ref NONE,
                                                     Cons = ref SM.empty,
                                                     Variety = Nothing,
                                                     Known = ref false,
                                                     Ge = ref NONE})
                              in
                                  #Vars db := IM.insert (!(#Vars db), n, r);
                                  r
                              end)
              | Lvar _ => raise Undetermined
              | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
                                            SOME r => repOf r
                                          | NONE =>
                                            let
                                                val r = ref (Node {Id = nodeId (),
                                                                   Rep = ref NONE,
                                                                   Cons = ref SM.empty,
                                                                   Variety = Dt0 f,
                                                                   Known = ref true,
                                                                   Ge = ref NONE})
                                            in
                                                #Con0s db := SM.insert (!(#Con0s db), f, r);
                                                r
                                            end)
              | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
              | Func (DtCon1 f, [e]) =>
                let
                    val r = rep e
                in
                    case SM.find (!(#Cons (unNode r)), f) of
                        SOME r => repOf r
                      | NONE =>
                        let
                            val r' = ref (Node {Id = nodeId (),
                                                Rep = ref NONE,
                                                Cons = ref SM.empty,
                                                Variety = Dt1 (f, r),
                                                Known = ref (!(#Known (unNode r))),
                                                Ge = ref NONE})
                        in
                            #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
                            r'
                        end
                end
              | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
              | Func (UnCon f, [e]) =>
                let
                    val r = rep e
                in
                    case #Variety (unNode r) of
                        Dt1 (f', n) => if f' = f then
                                           repOf n
                                       else
                                           raise Contradiction
                      | Nothing =>
                        let
                            val cons = ref SM.empty
                            val r' = ref (Node {Id = nodeId (),
                                                Rep = ref NONE,
                                                Cons = cons,
                                                Variety = Nothing,
                                                Known = ref (!(#Known (unNode r))),
                                                Ge = ref NONE})

                            val r'' = ref (Node {Id = nodeId (),
                                                 Rep = ref NONE,
                                                 Cons = #Cons (unNode r),
                                                 Variety = Dt1 (f, r'),
                                                 Known = #Known (unNode r),
                                                 Ge = ref NONE})
                        in
                            cons := SM.insert (!cons, f, r'');
                            #Rep (unNode r) := SOME r'';
                            r'
                        end
                      | _ => raise Contradiction
                end
              | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
              | Func (Other f, es) =>
                let
                    val rs = map rep es
                in
                    case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
                        NONE =>
                        let
                            val r = ref (Node {Id = nodeId (),
                                               Rep = ref NONE,
                                               Cons = ref SM.empty,
                                               Variety = Nothing,
                                               Known = ref (f = "allow"),
                                               Ge = ref NONE})
                        in
                            #Funcs db := ((f, rs), r) :: (!(#Funcs db));
                            r
                        end
                      | SOME (_, r) => repOf r
                end
              | Recd xes =>
                let
                    val xes = map (fn (x, e) => (x, rep e)) xes
                    val len = length xes
                in
                    case List.find (fn (xes', _) =>
                                       SM.numItems xes' = len
                                       andalso List.all (fn (x, n) =>
                                                            case SM.find (xes', x) of
                                                                NONE => false
                                                             | SOME n' => n = repOf n') xes)
                         (!(#Records db)) of
                        SOME (_, r) => repOf r
                      | NONE =>
                        let
                            val xes = foldl SM.insert' SM.empty xes

                            val r' = ref (Node {Id = nodeId (),
                                                Rep = ref NONE,
                                                Cons = ref SM.empty,
                                                Variety = Recrd (ref xes, true),
                                                Known = ref false,
                                                Ge = ref NONE})
                        in
                            #Records db := (xes, r') :: (!(#Records db));
                            r'
                        end
                end
              | Proj (e, f) =>
                let
                    val r = rep e
                in
                    case #Variety (unNode r) of
                        Recrd (xes, _) =>
                        (case SM.find (!xes, f) of
                             SOME r => repOf r
                           | NONE => let
                                  val r = ref (Node {Id = nodeId (),
                                                     Rep = ref NONE,
                                                     Cons = ref SM.empty,
                                                     Variety = Nothing,
                                                     Known = ref (!(#Known (unNode r))),
                                                     Ge = ref NONE})
                              in
                                 xes := SM.insert (!xes, f, r);
                                 r
                              end)
                      | Nothing =>
                        let
                            val r' = ref (Node {Id = nodeId (),
                                                Rep = ref NONE,
                                                Cons = ref SM.empty,
                                                Variety = Nothing,
                                                Known = ref (!(#Known (unNode r))),
                                                Ge = ref NONE})
                                     
                            val r'' = ref (Node {Id = nodeId (),
                                                 Rep = ref NONE,
                                                 Cons = #Cons (unNode r),
                                                 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
                                                 Known = #Known (unNode r),
                                                 Ge = ref NONE})
                        in
                            #Rep (unNode r) := SOME r'';
                            r'
                        end
                      | _ => raise Contradiction                             
                end
    in
        rep e
    end

fun p_repOf db e = p_rep (representative (db, e))

fun assert (db, a) =
    let
        fun markEq (r1, r2) =
            let
                val r1 = repOf r1
                val r2 = repOf r2
            in
                if r1 = r2 then
                    ()
                else case (#Variety (unNode r1), #Variety (unNode r2)) of
                         (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
                                                   ()
                                               else
                                                   raise Contradiction
                       | (Dt0 f1, Dt0 f2) => if f1 = f2 then
                                                 ()
                                             else
                                                 raise Contradiction
                       | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
                                                             markEq (r1, r2)
                                                         else
                                                             raise Contradiction
                       | (Recrd (xes1, _), Recrd (xes2, _)) =>
                         let
                             fun unif (xes1, xes2) =
                                 SM.appi (fn (x, r1) =>
                                             case SM.find (!xes2, x) of
                                                 NONE => xes2 := SM.insert (!xes2, x, r1)
                                               | SOME r2 => markEq (r1, r2)) (!xes1)
                         in
                             unif (xes1, xes2);
                             unif (xes2, xes1)
                         end
                       | (Nothing, _) => mergeNodes (r1, r2)
                       | (_, Nothing) => mergeNodes (r2, r1)
                       | _ => raise Contradiction
            end

        and mergeNodes (r1, r2) =
            (#Rep (unNode r1) := SOME r2;
             if !(#Known (unNode r1)) then
                 markKnown r2
             else
                 ();
             if !(#Known (unNode r2)) then
                 markKnown r1
             else
                 ();
             #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));

             case !(#Ge (unNode r1)) of
                 NONE => ()
               | SOME n1 =>
                 case !(#Ge (unNode r2)) of
                     NONE => #Ge (unNode r2) := SOME n1
                   | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));

             compactFuncs ())

        and compactFuncs () =
            let
                fun loop funcs =
                    case funcs of
                        [] => []
                      | (fr as ((f, rs), r)) :: rest =>
                        let
                            val rest = List.filter (fn ((f' : string, rs'), r') =>
                                                       if f' = f
                                                          andalso ListPair.allEq (fn (r1, r2) =>
                                                                                     repOf r1 = repOf r2)
                                                                                 (rs, rs') then
                                                           (markEq (r, r');
                                                            false)
                                                       else
                                                           true) rest
                        in
                            fr :: loop rest
                        end
            in
                #Funcs db := loop (!(#Funcs db))
            end
    in
        case a of
            ACond _ => ()
          | AReln x =>
            case x of
                (Known, [e]) =>
                ((*Print.prefaces "Before" [("e", p_exp e),
                                            ("db", p_database db)];*)
                 markKnown (representative (db, e))(*;
                                                        Print.prefaces "After" [("e", p_exp e),
                                                                                ("db", p_database db)]*))
              | (PCon0 f, [e]) =>
                let
                    val r = representative (db, e)
                in
                    case #Variety (unNode r) of
                        Dt0 f' => if f = f' then
                                      ()
                                  else
                                      raise Contradiction
                      | Nothing =>
                        (case SM.find (!(#Con0s db), f) of
                             SOME r' => markEq (r, r')
                           | NONE =>
                             let
                                 val r' = ref (Node {Id = nodeId (),
                                                     Rep = ref NONE,
                                                     Cons = ref SM.empty,
                                                     Variety = Dt0 f,
                                                     Known = ref false,
                                                     Ge = ref NONE})
                             in
                                 #Rep (unNode r) := SOME r';
                                 #Con0s db := SM.insert (!(#Con0s db), f, r')
                             end)
                      | _ => raise Contradiction
                end
              | (PCon1 f, [e]) =>
                let
                    val r = representative (db, e)
                in
                    case #Variety (unNode r) of
                        Dt1 (f', e') => if f = f' then
                                            ()
                                        else
                                            raise Contradiction
                      | Nothing =>
                        let
                            val cons = ref SM.empty

                            val r'' = ref (Node {Id = nodeId (),
                                                 Rep = ref NONE,
                                                 Cons = cons,
                                                 Variety = Nothing,
                                                 Known = ref (!(#Known (unNode r))),
                                                 Ge = ref NONE})

                            val r' = ref (Node {Id = nodeId (),
                                                Rep = ref NONE,
                                                Cons = ref SM.empty,
                                                Variety = Dt1 (f, r''),
                                                Known = #Known (unNode r),
                                                Ge = ref NONE})
                        in
                            cons := SM.insert (!cons, f, r');
                            #Rep (unNode r) := SOME r'
                        end
                      | _ => raise Contradiction
                end
              | (Eq, [e1, e2]) =>
                markEq (representative (db, e1), representative (db, e2))
              | (Ge, [e1, e2]) =>
                let
                    val r1 = representative (db, e1)
                    val r2 = representative (db, e2)
                in
                    case !(#Ge (unNode (repOf r2))) of
                        NONE => ()
                      | SOME n2 =>
                        case !(#Ge (unNode (repOf r1))) of
                            NONE => #Ge (unNode (repOf r1)) := SOME n2
                          | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
                end
              | _ => ()
    end handle Undetermined => ()

fun check (db, a) =
    (case a of
         ACond _ => false
       | AReln x =>
         case x of
             (Known, [e]) =>
             let
                 fun isKnown r =
                     let
                         val r = repOf r
                     in
                         !(#Known (unNode r))
                         orelse case #Variety (unNode r) of
                                    Dt1 (_, r) => isKnown r
                                  | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
                                  | _ => false
                     end

                 val r = representative (db, e)
             in
                 isKnown r
             end
           | (PCon0 f, [e]) =>
             (case #Variety (unNode (representative (db, e))) of
                  Dt0 f' => f' = f
                | _ => false)
           | (PCon1 f, [e]) =>
             (case #Variety (unNode (representative (db, e))) of
                  Dt1 (f', _) => f' = f
                | _ => false)
           | (Eq, [e1, e2]) =>
             let
                 val r1 = representative (db, e1)
                 val r2 = representative (db, e2)
             in
                 repOf r1 = repOf r2
             end
           | (Ge, [e1, e2]) =>
             let
                 val r1 = representative (db, e1)
                 val r2 = representative (db, e2)
             in
                 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
                     (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
                   | _ => false
             end
           | _ => false)
    handle Undetermined => false

fun builtFrom (db, {Base = bs, Derived = d}) =
    let
        val bs = map (fn b => representative (db, b)) bs

        fun loop d =
            let
                val d = repOf d
            in
                !(#Known (unNode d))
                orelse List.exists (fn b => repOf b = d) bs
                orelse (case #Variety (unNode d) of
                            Dt0 _ => true
                          | Dt1 (_, d) => loop d
                          | Prim _ => true
                          | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
                          | Nothing => false)
                orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs)
                                   (SM.listItems (!(#Cons (unNode d))))
            end

        fun decomp e =
            case e of
                Func (Other _, es) => List.all decomp es
              | _ => loop (representative (db, e))
    in
        decomp d
    end handle Undetermined => false

end

val tabs = ref (SM.empty : (string list * string list list) SM.map)

fun patCon pc =
    case pc of
        PConVar n => "C" ^ Int.toString n
      | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c

type check = exp * ErrorMsg.span

structure St :> sig
    val reset : unit -> unit

    type stashed
    val stash : unit -> stashed
    val reinstate : stashed -> unit

    type stashedPath
    val stashPath : unit -> stashedPath
    val reinstatePath : stashedPath -> unit

    val nextVar : unit -> int

    val assert : atom list -> unit

    val addPath : check -> unit

    val allowSend : atom list * exp list -> unit
    val send : check -> unit

    val allowInsert : atom list -> unit
    val insert : ErrorMsg.span -> unit

    val allowDelete : atom list -> unit
    val delete : ErrorMsg.span -> unit

    val allowUpdate : atom list -> unit
    val update : ErrorMsg.span -> unit

    val havocReln : reln -> unit
    val havocCookie : string -> unit

    val check : atom -> bool

    val debug : unit -> unit
end = struct

val hnames = ref 1

type hyps = int * atom list * bool ref

val db = Cc.database ()
val path = ref ([] : ((int * atom list) * check) option ref list)
val hyps = ref (0, [] : atom list, ref false)
val nvar = ref 0

fun setHyps (n', hs) =
    let
        val (n, _, _) = !hyps
    in
        if n' = n then
            ()
        else
            (hyps := (n', hs, ref false);
             Cc.clear db;
             app (fn a => Cc.assert (db, a)) hs)
    end    

fun useKeys () =
    let
        val changed = ref false

        fun findKeys (hyps, acc) =
            case hyps of
                [] => rev acc
              | (a as AReln (Sql tab, [r1])) :: hyps =>
                (case SM.find (!tabs, tab) of
                     NONE => findKeys (hyps, a :: acc)
                   | SOME (_, []) => findKeys (hyps, a :: acc)
                   | SOME (_, ks) =>
                     let
                         fun finder (hyps, acc) =
                             case hyps of
                                 [] => rev acc
                               | (a as AReln (Sql tab', [r2])) :: hyps =>
                                 if tab' = tab andalso
                                    List.exists (List.all (fn f =>
                                                              let
                                                                  val r =
                                                                      Cc.check (db,
                                                                                AReln (Eq, [Proj (r1, f),
                                                                                            Proj (r2, f)]))
                                                              in
                                                                  (*Print.prefaces "Fs"
                                                                                   [("tab",
                                                                                     Print.PD.string tab),
                                                                                    ("r1",
                                                                                     p_exp (Proj (r1, f))),
                                                                                    ("r2",
                                                                                     p_exp (Proj (r2, f))),
                                                                                    ("r",
                                                                                     Print.PD.string
                                                                                         (Bool.toString r))];*)
                                                                  r
                                                              end)) ks then
                                     (changed := true;
                                      Cc.assert (db, AReln (Eq, [r1, r2]));
                                      finder (hyps, acc))
                                 else
                                     finder (hyps, a :: acc)
                               | a :: hyps => finder (hyps, a :: acc)

                         val hyps = finder (hyps, [])
                     in
                         findKeys (hyps, a :: acc)
                     end)
              | a :: hyps => findKeys (hyps, a :: acc)

        fun loop hs =
            let
                val hs = findKeys (hs, [])
            in
                if !changed then
                    (changed := false;
                     loop hs)
                else
                    ()
            end

        val (_, hs, _) = !hyps
    in
        (*print "useKeys\n";*)
        loop hs
    end

fun complete () =
    let
        val (_, _, bf) = !hyps
    in
        if !bf then
            ()
        else
            (bf := true;
             useKeys ())
    end

type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
fun reinstate (nv, p, h) =
    (nvar := nv;
     path := p;
     setHyps h)

type stashedPath = ((int * atom list) * check) option ref list
fun stashPath () = !path
fun reinstatePath p = path := p

fun nextVar () =
    let
        val n = !nvar
    in
        nvar := n + 1;
        n
    end

fun assert ats =
    let
        val n = !hnames
        val (_, hs, _) = !hyps
    in
        hnames := n + 1;
        hyps := (n, ats @ hs, ref false);
        app (fn a => Cc.assert (db, a)) ats
    end

fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path

val sendable = ref ([] : (atom list * exp list) list)

fun checkGoals goals k =
    let
        fun checkGoals goals unifs =
            case goals of
                [] => k unifs
              | AReln (Sql tab, [Lvar lv]) :: goals =>
                let
                    val saved = stash ()
                    val (_, hyps, _) = !hyps

                    fun tryAll unifs hyps =
                        case hyps of
                            [] => false
                          | AReln (Sql tab', [e]) :: hyps =>
                            (tab' = tab andalso
                             checkGoals goals (IM.insert (unifs, lv, e)))
                            orelse tryAll unifs hyps
                          | _ :: hyps => tryAll unifs hyps
                in
                    tryAll unifs hyps
                end
              | (g as AReln (r, es)) :: goals =>
                (complete ();
                 (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
                      true
                  else
                      ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
                       false))
                 andalso checkGoals goals unifs)
              | ACond _ :: _ => false
    in
        checkGoals goals IM.empty
    end

fun buildable (e, loc) =
    let
        fun doPols pols acc =
            case pols of
                [] =>
                let
                    val b = Cc.builtFrom (db, {Base = acc, Derived = e})
                in
                    (*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
                                                ("Derived", p_exp e),
                                                ("Hyps", Print.p_list p_atom (#2 (!hyps))),
                                                ("Good", Print.PD.string (Bool.toString b))];*)
                    b
                end
              | (goals, es) :: pols =>
                checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
                orelse doPols pols acc
    in
        if doPols (!sendable) [] then
            ()
        else
            let
                val (_, hs, _) = !hyps
            in
                ErrorMsg.errorAt loc "The information flow policy may be violated here.";
                Print.prefaces "Situation" [("User learns", p_exp e),
                                            ("Hypotheses", Print.p_list p_atom hs),
                                            ("E-graph", Cc.p_database db)]
            end
    end

fun checkPaths () =
    let
        val (n, hs, _) = !hyps
        val hs = (n, hs)
    in
        app (fn r =>
                case !r of
                    NONE => ()
                  | SOME (hs, e) =>
                    (r := NONE;
                     setHyps hs;
                     buildable e)) (!path);
        setHyps hs
    end

fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
                                           ("exps", Print.p_list p_exp (#2 v))];*)
                   sendable := v :: !sendable)

fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
                     complete ();
                     checkPaths ();
                     if isKnown e then
                         ()
                     else
                         buildable (e, loc))

fun doable pols (loc : ErrorMsg.span) =
    let
        val pols = !pols
    in
        complete ();
        if List.exists (fn goals =>
                           if checkGoals goals (fn _ => true) then
                               ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
                                                        ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
                                true)
                           else
                               ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
                                                           ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
                                false)) pols then
            ()
        else
            let
                val (_, hs, _) = !hyps
            in
                ErrorMsg.errorAt loc "The database update policy may be violated here.";
                Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
                                            ("E-graph", Cc.p_database db)*)]
            end
    end

val insertable = ref ([] : atom list list)
fun allowInsert v = insertable := v :: !insertable
val insert = doable insertable

val updatable = ref ([] : atom list list)
fun allowUpdate v = updatable := v :: !updatable
val update = doable updatable

val deletable = ref ([] : atom list list)
fun allowDelete v = deletable := v :: !deletable
val delete = doable deletable

fun reset () = (Cc.clear db;
                path := [];
                hyps := (0, [], ref false);
                nvar := 0;
                sendable := [];
                insertable := [];
                updatable := [];
                deletable := [])

fun havocReln r =
    let
        val n = !hnames
        val (_, hs, _) = !hyps
    in
        hnames := n + 1;
        hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
    end

fun havocCookie cname =
    let
        val cname = "cookie/" ^ cname
        val n = !hnames
        val (_, hs, _) = !hyps
    in
        hnames := n + 1;
        hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
    end

fun check a = Cc.check (db, a)

fun debug () =
    let
        val (_, hs, _) = !hyps
    in
        Print.preface ("Hyps", Print.p_list p_atom hs)
    end

end


fun removeDups (ls : (string * string) list) =
    case ls of
        [] => []
      | x :: ls =>
        let
            val ls = removeDups ls
        in
            if List.exists (fn x' => x' = x) ls then
                ls  
            else
                x :: ls
        end

fun deinj env e =
    case #1 e of
        ERel n => SOME (List.nth (env, n))
      | EField (e, f) =>
        (case deinj env e of
             NONE => NONE
           | SOME e => SOME (Proj (e, f)))
      | EApp ((EFfi mf, _), e) =>
        if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
            NONE
        else (case deinj env e of
                  NONE => NONE
                | SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
      | _ => NONE

fun expIn rv env rvOf =
    let
        fun expIn e =
            let
                fun default () = inl (rv ())
            in
                case e of
                    SqConst p => inl (Const p)
                  | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
                  | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
                  | Null => inl (Func (DtCon0 "None", []))
                  | SqNot e =>
                    inr (case expIn e of
                             inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
                           | inr _ => Unknown)
                  | Field (v, f) => inl (Proj (rvOf v, f))
                  | Computed _ => default ()
                  | Binop (bo, e1, e2) =>
                    let
                        val e1 = expIn e1
                        val e2 = expIn e2
                    in
                        inr (case (bo, e1, e2) of
                                 (Exps f, inl e1, inl e2) => f (e1, e2)
                               | (Props f, v1, v2) =>
                                 let
                                     fun pin v =
                                         case v of
                                             inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
                                           | inr p => p
                                 in
                                     f (pin v1, pin v2)
                                 end
                               | _ => Unknown)
                    end
                  | SqKnown e =>
                    (case expIn e of
                         inl e => inr (Reln (Known, [e]))
                       | _ => inr Unknown)
                  | Inj e =>
                    inl (case deinj env e of
                             NONE => rv ()
                           | SOME e => e)
                  | SqFunc (f, e) =>
                    (case expIn e of
                         inl e => inl (Func (Other f, [e]))
                       | _ => default ())
                     
                  | Unmodeled => inl (Func (Other "allow", [rv ()]))
            end
    in
        expIn
    end

fun decomp {Save = save, Restore = restore, Add = add} =
    let
        fun go p k =
            case p of
                True => (k () handle Cc.Contradiction => ())
              | False => ()
              | Unknown => ()
              | And (p1, p2) => go p1 (fn () => go p2 k)
              | Or (p1, p2) =>
                let
                    val saved = save ()
                in
                    go p1 k;
                    restore saved;
                    go p2 k
                end
              | Reln x => (add (AReln x); k ())
              | Cond x => (add (ACond x); k ())
    in
        go
    end

datatype queryMode =
         SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
       | AllCols of exp -> unit

type 'a doQuery = {
     Env : exp list,
     NextVar : unit -> exp,
     Add : atom -> unit,
     Save : unit -> 'a,
     Restore : 'a -> unit,
     Cont : queryMode
}

fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
    let
        fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
    in
        case parse query e of
            NONE => default ()
          | SOME q =>
            let
                fun doQuery q =
                    case q of
                        Query1 r =>
                        let
                            val new = ref NONE
                            val old = ref NONE

                            val rvs = map (fn (tab, v) =>
                                              let
                                                  val nv = #NextVar arg ()
                                              in
                                                  case v of
                                                      "New" => new := SOME (tab, nv)
                                                    | "Old" => old := SOME (tab, nv)
                                                    | _ => ();
                                                  (v, nv)
                                              end) (#From r)

                            fun rvOf v =
                                case List.find (fn (v', _) => v' = v) rvs of
                                    NONE => raise Fail "Iflow.queryProp: Bad table variable"
                                  | SOME (_, e) => e

                            val expIn = expIn (#NextVar arg) (#Env arg) rvOf

                            val saved = #Save arg ()
                            fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)

                            fun usedFields e =
                                case e of
                                    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
                                    SomeCol k =>
                                    let
                                        val sis = map (fn si =>
                                                          case si of
                                                              SqField (v, f) => Proj (rvOf v, f)
                                                            | SqExp (e, f) =>
                                                              case expIn e of
                                                                  inr _ => #NextVar arg ()
                                                                | inl e => e) (#Select r)
                                    in
                                        k {New = !new, Old = !old, Outs = sis}
                                    end
                                  | AllCols k =>
                                    let
                                        val (ts, es) =
                                            foldl (fn (si, (ts, es)) =>
                                                      case si of
                                                          SqField (v, f) =>
                                                          let
                                                              val fs = getOpt (SM.find (ts, v), SM.empty)
                                                          in
                                                              (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
                                                          end
                                                        | SqExp (e, f) =>
                                                          let
                                                              val e =
                                                                  case expIn e of
                                                                      inr _ => #NextVar arg ()
                                                                    | inl e => e
                                                          in
                                                              (ts, SM.insert (es, f, e))
                                                          end)
                                                  (SM.empty, SM.empty) (#Select r)
                                    in
                                        k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
                                                     (SM.listItemsi ts)
                                                 @ SM.listItemsi es))
                                    end

                            fun doWhere final =
                                (addFrom ();
                                 case #Where r of
                                     NONE => final ()
                                   | SOME e =>
                                     let
                                         val p = case expIn e of
                                                     inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
                                                   | inr p => p

                                         val saved = #Save arg ()
                                     in
                                         decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
                                                p (fn () => final () handle Cc.Contradiction => ());
                                         #Restore arg saved
                                     end)
                                handle Cc.Contradiction => ()

                            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)]) =>
                                      (case #Cont arg of
                                           SomeCol _ => ()
                                         | AllCols k =>
                                           let
                                               fun answer e = k (Recd [(f, e)])

                                               val saved = #Save arg ()
                                               val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
                                                        handle Cc.Contradiction => ()
                                           in
                                               #Restore arg saved;
                                               (*print "True time!\n";*)
                                               doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
                                               #Restore arg saved
                                           end)
                                    | _ => normal ())
                               | _ => normal ())
                            before #Restore arg saved
                        end
                      | Union (q1, q2) =>
                        let
                            val saved = #Save arg ()
                        in
                            doQuery q1;
                            #Restore arg saved;
                            doQuery q2;
                            #Restore arg saved
                        end
            in
                doQuery q
            end
    end

fun evalPat env e (pt, _) =
    case pt of
        PWild => env
      | PVar _ => e :: env
      | PPrim _ => env
      | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
      | PCon (_, pc, SOME pt) =>
        let
            val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
        in
            St.assert [AReln (PCon1 (patCon pc), [e])];
            env
        end
      | PRecord xpts =>
        foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
      | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
      | PSome (_, pt) =>
        let
            val env = evalPat env (Func (UnCon "Some", [e])) pt
        in
            St.assert [AReln (PCon1 "Some", [e])];
            env
        end

datatype arg_mode = Fixed | Decreasing | Arbitrary
type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
val rfuns = ref (IM.empty : rfun IM.map)

fun evalExp env (e as (_, loc)) k =
    let
        (*val () = St.debug ()*)
        (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)

        fun default () = k (Var (St.nextVar ()))

        fun doFfi (m, s, es) =
            if m = "Basis" andalso SS.member (writers, s) then
                let
                    fun doArgs es =
                        case es of
                            [] =>
                            (if s = "set_cookie" then
                                 case es of
                                     [_, (cname, _), _, _, _] =>
                                     (case #1 cname of
                                          EPrim (Prim.String cname) =>
                                          St.havocCookie cname
                                        | _ => ())
                                   | _ => ()
                             else
                                 ();
                             k (Recd []))
                          | (e, _) :: es =>
                            evalExp env e (fn e => (St.send (e, loc); doArgs es))
                in
                    doArgs es
                end
            else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
                default ()
            else
                let
                    fun doArgs (es, acc) =
                        case es of
                            [] => k (Func (Other (m ^ "." ^ s), rev acc))
                          | (e, _) :: es =>
                            evalExp env e (fn e => doArgs (es, e :: acc))
                in
                    doArgs (es, [])
                end            
    in
        case #1 e of
            EPrim p => k (Const p)
          | ERel n => k (List.nth (env, n))
          | ENamed _ => default ()
          | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
          | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
          | ENone _ => k (Func (DtCon0 "None", []))
          | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
          | EFfi _ => default ()

          | EFfiApp ("Basis", "rand", []) =>
            let
                val e = Var (St.nextVar ())
            in
                St.assert [AReln (Known, [e])];
                k e
            end
          | EFfiApp x => doFfi x
          | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [(e, (TRecord [], loc))])

          | EApp (e1 as (EError _, _), _) => evalExp env e1 k

          | EApp (e1, e2) =>
            let
                fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
                                   Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
                                   default ())

                fun doArgs (e, args) =
                    case #1 e of
                        EApp (e1, e2) => doArgs (e1, e2 :: args)
                      | ENamed n =>
                        (case IM.find (!rfuns, n) of
                             NONE => adefault ()
                           | SOME rf =>
                             if length (#args rf) <> length args then
                                 adefault ()
                             else
                                 let
                                     val () = (SS.app (St.havocReln o Sql) (#tables rf);
                                               SS.app St.havocCookie (#cookies rf))
                                     val saved = St.stash ()

                                     fun doArgs (args, modes, env') =
                                         case (args, modes) of
                                             ([], []) => (evalExp env' (#body rf) (fn _ => ());
                                                          St.reinstate saved;
                                                          default ())
                                                         
                                           | (arg :: args, mode :: modes) =>
                                             evalExp env arg (fn arg =>
                                                                 let
                                                                     val v = case mode of
                                                                                 Arbitrary => Var (St.nextVar ())
                                                                               | Fixed => arg
                                                                               | Decreasing =>
                                                                                 let
                                                                                     val v = Var (St.nextVar ())
                                                                                 in
                                                                                     if St.check (AReln (Known, [arg])) then
                                                                                         St.assert [(AReln (Known, [v]))]
                                                                                     else
                                                                                         ();
                                                                                     v
                                                                                 end
                                                                 in
                                                                     doArgs (args, modes, v :: env')
                                                                 end)
                                           | _ => raise Fail "Iflow.doArgs: Impossible"
                                 in
                                     doArgs (args, #args rf, [])
                                 end)
                          | _ => adefault ()
            in
                doArgs (e, [])
            end

          | EAbs _ => default ()
          | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
          | EBinop (_, s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
          | ERecord xets =>
            let
                fun doFields (xes, acc) =
                    case xes of
                        [] => k (Recd (rev acc))
                      | (x, e, _) :: xes =>
                        evalExp env e (fn e => doFields (xes, (x, e) :: acc))
            in
                doFields (xets, [])
            end
          | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
          | ECase (e, pes, {result = res, ...}) =>
            evalExp env e (fn e =>
                              if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
                                            | _ => false) pes then
                                  (St.send (e, loc);
                                   k (Recd []))
                              else
                                  (St.addPath (e, loc);
                                   app (fn (p, pe) =>
                                           let
                                               val saved = St.stash ()
                                           in
                                               let
                                                   val env = evalPat env e p
                                               in
                                                   evalExp env pe k;
                                                   St.reinstate saved
                                               end
                                               handle Cc.Contradiction => St.reinstate saved
                                           end) pes))
          | EStrcat (e1, e2) =>
            evalExp env e1 (fn e1 =>
                evalExp env e2 (fn e2 =>
                                   k (Func (Other "cat", [e1, e2]))))
          | EError (e, _) => evalExp env e (fn e => St.send (e, loc))
          | EReturnBlob {blob = b, mimeType = m, ...} =>
            evalExp env b (fn b =>
                              (St.send (b, loc);
                               evalExp env m
                               (fn m => St.send (m, loc))))
          | ERedirect (e, _) =>
            evalExp env e (fn e => St.send (e, loc))
          | EWrite e =>
            evalExp env e (fn e => (St.send (e, loc);
                                    k (Recd [])))
          | ESeq (e1, e2) =>
            let
                val path = St.stashPath ()
            in
                evalExp env e1 (fn _ => (St.reinstatePath path; evalExp env e2 k))
            end
          | ELet (_, _, e1, e2) =>
            evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
          | EClosure (n, es) =>
            let
                fun doArgs (es, acc) =
                    case es of
                        [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
                      | e :: es =>
                        evalExp env e (fn e => doArgs (es, e :: acc))
            in
                doArgs (es, [])
            end

          | EQuery {query = q, body = b, initial = i, state = state, ...} =>
            evalExp env i (fn i =>
                              let
                                  val r = Var (St.nextVar ())
                                  val acc = Var (St.nextVar ())

                                  val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
                                                                   exp = fn (e, st as (cs, ts)) =>
                                                                            case e of
                                                                                EDml (e, _) =>
                                                                                (case parse dml e of
                                                                                     NONE => st
                                                                                   | SOME c =>
                                                                                     case c of
                                                                                         Insert _ => st
                                                                                       | Delete (tab, _) =>
                                                                                         (cs, SS.add (ts, tab))
                                                                                       | Update (tab, _, _) =>
                                                                                         (cs, SS.add (ts, tab)))
                                                                              | EFfiApp ("Basis", "set_cookie",
                                                                                         [_, ((EPrim (Prim.String cname), _), _),
                                                                                          _, _, _]) =>
                                                                                (SS.add (cs, cname), ts)
                                                                              | _ => st}
                                                                  (SS.empty, SS.empty) b
                              in
                                  case (#1 state, SS.isEmpty ts, SS.isEmpty cs) of
                                          (TRecord [], true, true) => ()
                                        | _ =>
                                          let
                                              val saved = St.stash ()
                                          in
                                              (k i)
                                              handle Cc.Contradiction => ();
                                              St.reinstate saved
                                          end;

                                  SS.app (St.havocReln o Sql) ts;
                                  SS.app St.havocCookie cs;

                                  doQuery {Env = env,
                                           NextVar = Var o St.nextVar,
                                           Add = fn a => St.assert [a],
                                           Save = St.stash,
                                           Restore = St.reinstate,
                                           Cont = AllCols (fn x =>
                                                              (St.assert [AReln (Eq, [r, x])];
                                                               evalExp (acc :: r :: env) b k))} q
                              end)
          | EDml (e, _) =>
            (case parse dml e of
                 NONE => (print ("Warning: Information flow checker can't parse DML command at "
                                 ^ ErrorMsg.spanToString loc ^ "\n");
                          default ())
               | SOME d =>
                 case d of
                     Insert (tab, es) =>
                     let
                         val new = St.nextVar ()

                         val expIn = expIn (Var o St.nextVar) env
                                           (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")

                         val es = map (fn (x, e) =>
                                          case expIn e of
                                              inl e => (x, e)
                                            | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
                                  es

                         val saved = St.stash ()
                     in
                         St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
                         St.insert loc;
                         St.reinstate saved;
                         St.assert [AReln (Sql tab, [Recd es])];
                         k (Recd [])
                     end
                   | 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" 
                                   | inr p => p
                                                          
                         val saved = St.stash ()
                     in
                         St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
                                    AReln (Sql (tab), [Var old])];
                         decomp {Save = St.stash,
                                 Restore = St.reinstate,
                                 Add = fn a => St.assert [a]} p
                                (fn () => (St.delete loc;
                                           St.reinstate saved;
                                           St.havocReln (Sql tab);
                                           k (Recd []))
                                    handle Cc.Contradiction => ())
                     end
                   | Update (tab, fs, e) =>
                     let
                         val new = St.nextVar ()
                         val old = St.nextVar ()

                         val expIn = expIn (Var o St.nextVar) env
                                           (fn "T" => Var old
                                             | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")

                         val fs = map
                                      (fn (x, e) =>
                                          (x, case expIn e of
                                                  inl e => e
                                                | inr _ => raise Fail
                                                                     ("Iflow.evalExp: Selecting "
                                                                      ^ "boolean expression")))
                                      fs

                         val fs' = case SM.find (!tabs, tab) of
                                       NONE => raise Fail "Iflow.evalExp: Updating unknown table"
                                     | SOME (fs', _) => fs'

                         val fs = foldl (fn (f, fs) =>
                                            if List.exists (fn (f', _) => f' = f) fs then
                                                fs
                                            else
                                                (f, Proj (Var old, f)) :: fs) fs fs'

                         val p = case expIn e of
                                           inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" 
                                         | inr p => p
                         val saved = St.stash ()
                     in
                         St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
                                    AReln (Sql (tab ^ "$Old"), [Var old]),
                                    AReln (Sql tab, [Var old])];
                         decomp {Save = St.stash,
                                 Restore = St.reinstate,
                                 Add = fn a => St.assert [a]} p
                                (fn () => (St.update loc;
                                           St.reinstate saved;
                                           St.havocReln (Sql tab);
                                           k (Recd []))
                                    handle Cc.Contradiction => ())
                     end)
                     
          | ENextval (EPrim (Prim.String seq), _) =>
            let
                val nv = St.nextVar ()
            in
                St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
                k (Var nv)
            end
          | ENextval _ => default ()
          | ESetval _ => default ()

          | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String cname), _), _)]), _), _, _) =>
            let
                val e = Var (St.nextVar ())
                val e' = Func (Other ("cookie/" ^ cname), [])
            in
                St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
                k e
            end

          | EUnurlify _ => default ()
          | EJavaScript _ => default ()
          | ESignalReturn _ => default ()
          | ESignalBind _ => default ()
          | ESignalSource _ => default ()
          | EServerCall _ => default ()
          | ERecv _ => default ()
          | ESleep _ => default ()
          | ESpawn _ => default ()
    end

datatype var_source = Input of int | SubInput of int | Unknown

fun check file =
    let
        val () = (St.reset ();
                  rfuns := IM.empty)

        val file = MonoReduce.reduce file
        val file = MonoOpt.optimize file
        val file = Fuse.fuse file
        val file = MonoOpt.optimize file
        val file = MonoShake.shake file
        (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)

        val exptd = foldl (fn ((d, _), exptd) =>
                              case d of
                                  DExport (_, _, n, _, _, _) => IS.add (exptd, n)
                                | _ => exptd) IS.empty file

        fun decl (d, loc) =
            case d of
                DTable (tab, fs, pk, _) =>
                let
                    val ks =
                        case #1 pk of
                            EPrim (Prim.String s) =>
                            (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
                                 [] => []
                               | pk => [pk])
                          | _ => []
                in
                    if size tab >= 3 then
                        tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
                                           (map #1 fs,
                                            map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
                                                              ^ String.extract (s, 4, NONE))) ks))
                    else
                        raise Fail "Table name does not begin with uw_"
                end
              | DVal (x, n, _, e, _) =>
                let
                    (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)

                    val isExptd = IS.member (exptd, n)

                    val saved = St.stash ()

                    fun deAbs (e, env, ps) =
                        case #1 e of
                            EAbs (_, _, _, e) =>
                            let
                                val nv = Var (St.nextVar ())
                            in
                                deAbs (e, nv :: env,
                                       if isExptd then
                                           AReln (Known, [nv]) :: ps
                                       else
                                           ps)
                            end
                          | _ => (e, env, ps)

                    val (e, env, ps) = deAbs (e, [], [])
                in
                    St.assert ps;
                    (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
                    St.reinstate saved
                end

              | DValRec [(x, n, _, e, _)] =>
                let
                    val tables = ref SS.empty
                    val cookies = ref SS.empty

                    fun deAbs (e, env, modes) =
                        case #1 e of
                            EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
                          | _ => (e, env, rev modes)

                    val (e, env, modes) = deAbs (e, [], [])

                    fun doExp env (e as (_, loc)) =
                        case #1 e of
                            EPrim _ => e
                          | ERel _ => e
                          | ENamed _ => e
                          | ECon (_, _, NONE) => e
                          | ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
                          | ENone _ => e
                          | ESome (t, e) => (ESome (t, doExp env e), loc)
                          | EFfi _ => e
                          | EFfiApp (m, f, es) =>
                            (case (m, f, es) of
                                 ("Basis", "set_cookie", [_, ((EPrim (Prim.String cname), _), _), _, _, _]) =>
                                 cookies := SS.add (!cookies, cname)
                               | _ => ();
                             (EFfiApp (m, f, map (fn (e, t) => (doExp env e, t)) es), loc))

                          | EApp (e1, e2) =>
                            let
                                fun default () = (EApp (doExp env e1, doExp env e2), loc)

                                fun explore (e, args) =
                                    case #1 e of
                                        EApp (e1, e2) => explore (e1, e2 :: args)
                                      | ENamed n' =>
                                        if n' = n then
                                            let
                                                fun doArgs (pos, args, modes) =
                                                    case (args, modes) of
                                                        ((e1, _) :: args, m1 :: modes) =>
                                                        (case e1 of
                                                             ERel n =>
                                                             (case List.nth (env, n) of
                                                                  Input pos' =>
                                                                  if pos' = pos then
                                                                      ()
                                                                  else
                                                                      m1 := Arbitrary
                                                                | SubInput pos' =>
                                                                  if pos' = pos then
                                                                      if !m1 = Arbitrary then
                                                                          ()
                                                                      else
                                                                          m1 := Decreasing
                                                                  else
                                                                      m1 := Arbitrary
                                                                | Unknown => m1 := Arbitrary)
                                                           | _ => m1 := Arbitrary;
                                                         doArgs (pos + 1, args, modes))
                                                      | (_ :: _, []) => ()
                                                      | ([], ms) => app (fn m => m := Arbitrary) ms
                                            in
                                                doArgs (0, args, modes);
                                                (EFfi ("Basis", "?"), loc)
                                            end
                                        else
                                            default ()
                                      | _ => default ()
                            in
                                explore (e, [])
                            end
                          | EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
                          | EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
                          | EBinop (bi, bo, e1, e2) => (EBinop (bi, bo, doExp env e1, doExp env e2), loc)
                          | ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
                          | EField (e1, f) => (EField (doExp env e1, f), loc)
                          | ECase (e, pes, ts) =>
                            let
                                val source =
                                    case #1 e of
                                        ERel n =>
                                        (case List.nth (env, n) of
                                             Input n => SOME n
                                           | SubInput n => SOME n
                                           | Unknown => NONE)
                                      | _ => NONE

                                fun doV v =
                                    let
                                        fun doPat (p, env) =
                                            case #1 p of
                                                PWild => env
                                              | PVar _ => v :: env
                                              | PPrim _ => env
                                              | PCon (_, _, NONE) => env
                                              | PCon (_, _, SOME p) => doPat (p, env)
                                              | PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
                                              | PNone _ => env
                                              | PSome (_, p) => doPat (p, env)
                                    in
                                        (ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
                                    end
                            in
                                case source of
                                    NONE => doV Unknown
                                  | SOME inp => doV (SubInput inp)
                            end
                          | EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
                          | EError (e1, t) => (EError (doExp env e1, t), loc)
                          | EReturnBlob {blob = b, mimeType = m, t} =>
                            (EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
                          | ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
                          | EWrite e1 => (EWrite (doExp env e1), loc)
                          | ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
                          | ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
                          | EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
                          | EQuery {exps, tables, state, query, body, initial} =>
                            (EQuery {exps = exps, tables = tables, state = state,
                                     query = doExp env query,
                                     body = doExp (Unknown :: Unknown :: env) body,
                                     initial = doExp env initial}, loc)
                          | EDml (e1, mode) =>
                            (case parse dml e1 of
                                 NONE => ()
                               | SOME c =>
                                 case c of
                                     Insert _ => ()
                                   | Delete (tab, _) =>
                                     tables := SS.add (!tables, tab)
                                   | Update (tab, _, _) =>
                                     tables := SS.add (!tables, tab);
                             (EDml (doExp env e1, mode), loc))
                          | ENextval e1 => (ENextval (doExp env e1), loc)
                          | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
                          | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
                          | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
                          | ESignalReturn _ => e
                          | ESignalBind _ => e
                          | ESignalSource _ => e
                          | EServerCall _ => e
                          | ERecv _ => e
                          | ESleep _ => e
                          | ESpawn _ => e

                    val e = doExp env e
                in
                    rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
                                                    args = map (fn r => !r) modes, body = e})
                end

              | DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."

              | DPolicy pol =>
                let
                    val rvN = ref 0
                    fun rv () =
                        let
                            val n = !rvN
                        in
                            rvN := n + 1;
                            Lvar n
                        end

                    val atoms = ref ([] : atom list)
                    fun doQ k = doQuery {Env = [],
                                         NextVar = rv,
                                         Add = fn a => atoms := a :: !atoms,
                                         Save = fn () => !atoms,
                                         Restore = fn ls => atoms := ls,
                                         Cont = SomeCol (fn r => k (rev (!atoms), r))}

                    fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
                                                            tab' <> tab
                                                            orelse List.all (fn Lvar lv' => lv' <> lv
                                                                              | _ => false) nams
                                                          | _ => true)
                in
                    case pol of
                        PolClient e =>
                        doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
                      | PolInsert e =>
                        doQ (fn (ats, {New = SOME (tab, new), ...}) =>
                                St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab (tab, [new]) ats)
                              | _ => raise Fail "Iflow: No New in mayInsert policy") e
                      | PolDelete e =>
                        doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
                                St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab (tab, [old]) ats)
                              | _ => raise Fail "Iflow: No Old in mayDelete policy") e
                      | PolUpdate e =>
                        doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
                                St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
                                                :: AReln (Sql (tab ^ "$New"), [new])
                                                :: untab (tab, [new, old]) ats)
                              | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
                      | PolSequence e =>
                        (case #1 e of
                             EPrim (Prim.String seq) =>
                             let
                                 val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
                                 val outs = [Lvar 0]
                             in
                                 St.allowSend ([p], outs)
                             end
                           | _ => ())
                end
                                        
              | _ => ()
    in
        app decl file
    end

val check = fn file =>
               let
                   val oldInline = Settings.getMonoInline ()
               in
                   (Settings.setMonoInline (case Int.maxInt of
                                                NONE => 1000000
                                              | SOME n => n);
                    check file;
                    Settings.setMonoInline oldInline)
                   handle ex => (Settings.setMonoInline oldInline;
                                 raise ex)
               end

end