adamc@1200: (* Copyright (c) 2010, Adam Chlipala
adamc@1200:  * All rights reserved.
adamc@1200:  *
adamc@1200:  * Redistribution and use in source and binary forms, with or without
adamc@1200:  * modification, are permitted provided that the following conditions are met:
adamc@1200:  *
adamc@1200:  * - Redistributions of source code must retain the above copyright notice,
adamc@1200:  *   this list of conditions and the following disclaimer.
adamc@1200:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200:  *   this list of conditions and the following disclaimer in the documentation
adamc@1200:  *   and/or other materials provided with the distribution.
adamc@1200:  * - The names of contributors may not be used to endorse or promote products
adamc@1200:  *   derived from this software without specific prior written permission.
adamc@1200:  *
adamc@1200:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@1200:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200:  * POSSIBILITY OF SUCH DAMAGE.
adamc@1200:  *)
adamc@1200: 
adamc@1200: structure Iflow :> IFLOW = struct
adamc@1200: 
adamc@1200: open Mono
adamc@1200: 
adamc@1207: structure IS = IntBinarySet
adamc@1202: structure IM = IntBinaryMap
adamc@1202: 
adamc@1215: structure SK = struct
adamc@1215: type ord_key = string
adamc@1215: val compare = String.compare
adamc@1215: end
adamc@1215: 
adamc@1215: structure SS = BinarySetFn(SK)
adamc@1215: structure SM = BinaryMapFn(SK)
adamc@1200: 
adamc@1200: val writers = ["htmlifyInt_w",
adamc@1200:                "htmlifyFloat_w",
adamc@1200:                "htmlifyString_w",
adamc@1200:                "htmlifyBool_w",
adamc@1200:                "htmlifyTime_w",
adamc@1200:                "attrifyInt_w",
adamc@1200:                "attrifyFloat_w",
adamc@1200:                "attrifyString_w",
adamc@1200:                "attrifyChar_w",
adamc@1200:                "urlifyInt_w",
adamc@1200:                "urlifyFloat_w",
adamc@1200:                "urlifyString_w",
adamc@1213:                "urlifyBool_w",
adamc@1213:                "set_cookie"]
adamc@1200: 
adamc@1200: val writers = SS.addList (SS.empty, writers)
adamc@1200: 
adamc@1200: type lvar = int
adamc@1200: 
adamc@1215: datatype func =
adamc@1215:          DtCon0 of string
adamc@1215:        | DtCon1 of string
adamc@1215:        | UnCon of string
adamc@1215:        | Other of string
adamc@1215: 
adamc@1200: datatype exp =
adamc@1200:          Const of Prim.t
adamc@1200:        | Var of int
adamc@1200:        | Lvar of lvar
adamc@1215:        | Func of func * exp list
adamc@1200:        | Recd of (string * exp) list
adamc@1200:        | Proj of exp * string
adamc@1200:        | Finish
adamc@1200: 
adamc@1200: datatype reln =
adamc@1207:          Known
adamc@1207:        | Sql of string
adamc@1215:        | PCon0 of string
adamc@1215:        | PCon1 of string
adamc@1200:        | Eq
adamc@1210:        | Ne
adamc@1210:        | Lt
adamc@1210:        | Le
adamc@1210:        | Gt
adamc@1210:        | Ge
adamc@1200: 
adamc@1200: datatype prop =
adamc@1200:          True
adamc@1200:        | False
adamc@1200:        | Unknown
adamc@1200:        | And of prop * prop
adamc@1200:        | Or of prop * prop
adamc@1200:        | Reln of reln * exp list
adamc@1212:        | Cond of exp * prop
adamc@1200: 
adamc@1215: val unif = ref (IM.empty : exp IM.map)
adamc@1215: 
adamc@1215: fun reset () = unif := IM.empty
adamc@1215: fun save () = !unif
adamc@1215: fun restore x = unif := x
adamc@1215: 
adamc@1200: local
adamc@1207:     open Print
adamc@1207:     val string = PD.string
adamc@1207: in
adamc@1207: 
adamc@1215: fun p_func f =
adamc@1215:     string (case f of
adamc@1215:                 DtCon0 s => s
adamc@1215:               | DtCon1 s => s
adamc@1215:               | UnCon s => "un" ^ s
adamc@1215:               | Other s => s)
adamc@1215: 
adamc@1207: fun p_exp e =
adamc@1207:     case e of
adamc@1207:         Const p => Prim.p_t p
adamc@1207:       | Var n => string ("x" ^ Int.toString n)
adamc@1215:       | Lvar n =>
adamc@1215:         (case IM.find (!unif, n) of
adamc@1215:              NONE => string ("X" ^ Int.toString n)
adamc@1215:            | SOME e => p_exp e)
adamc@1215:       | Func (f, es) => box [p_func f,
adamc@1215:                              string "(",
adamc@1207:                              p_list p_exp es,
adamc@1207:                              string ")"]
adamc@1207:       | Recd xes => box [string "{",
adamc@1210:                          p_list (fn (x, e) => box [string x,
adamc@1207:                                                    space,
adamc@1207:                                                    string "=",
adamc@1207:                                                    space,
adamc@1207:                                                    p_exp e]) xes,
adamc@1207:                          string "}"]
adamc@1207:       | Proj (e, x) => box [p_exp e,
adamc@1207:                             string ("." ^ x)]
adamc@1207:       | Finish => string "FINISH"
adamc@1207: 
adamc@1210: fun p_bop s es =
adamc@1210:     case es of
adamc@1210:         [e1, e2] => box [p_exp e1,
adamc@1210:                          space,
adamc@1210:                          string s,
adamc@1210:                          space,
adamc@1210:                          p_exp e2]
adamc@1210:       | _ => raise Fail "Iflow.p_bop"
adamc@1210: 
adamc@1207: fun p_reln r es =
adamc@1207:     case r of
adamc@1207:         Known =>
adamc@1207:         (case es of
adamc@1207:              [e] => box [string "known(",
adamc@1207:                          p_exp e,
adamc@1207:                          string ")"]
adamc@1207:            | _ => raise Fail "Iflow.p_reln: Known")
adamc@1207:       | Sql s => box [string (s ^ "("),
adamc@1207:                       p_list p_exp es,
adamc@1207:                       string ")"]
adamc@1215:       | PCon0 s => box [string (s ^ "("),
adamc@1215:                         p_list p_exp es,
adamc@1215:                         string ")"]
adamc@1215:       | PCon1 s => box [string (s ^ "("),
adamc@1211:                         p_list p_exp es,
adamc@1211:                         string ")"]
adamc@1210:       | Eq => p_bop "=" es
adamc@1210:       | Ne => p_bop "<>" es
adamc@1210:       | Lt => p_bop "<" es
adamc@1210:       | Le => p_bop "<=" es
adamc@1210:       | Gt => p_bop ">" es
adamc@1210:       | Ge => p_bop ">=" es
adamc@1207: 
adamc@1207: fun p_prop p =
adamc@1207:     case p of
adamc@1207:         True => string "True"
adamc@1207:       | False => string "False"
adamc@1207:       | Unknown => string "??"
adamc@1207:       | And (p1, p2) => box [string "(",
adamc@1207:                              p_prop p1,
adamc@1207:                              string ")",
adamc@1207:                              space,
adamc@1207:                              string "&&",
adamc@1207:                              space,
adamc@1207:                              string "(",
adamc@1207:                              p_prop p2,
adamc@1207:                              string ")"]
adamc@1207:       | Or (p1, p2) => box [string "(",
adamc@1207:                             p_prop p1,
adamc@1207:                             string ")",
adamc@1207:                             space,
adamc@1207:                             string "||",
adamc@1207:                             space,
adamc@1207:                             string "(",
adamc@1207:                             p_prop p2,
adamc@1207:                             string ")"]
adamc@1207:       | Reln (r, es) => p_reln r es
adamc@1212:       | Cond (e, p) => box [string "(",
adamc@1212:                             p_exp e,
adamc@1212:                             space,
adamc@1212:                             string "==",
adamc@1212:                             space,
adamc@1212:                             p_prop p,
adamc@1212:                             string ")"]
adamc@1207: 
adamc@1207: end
adamc@1207: 
adamc@1207: local
adamc@1202:     val count = ref 1
adamc@1200: in
adamc@1200: fun newLvar () =
adamc@1200:     let
adamc@1200:         val n = !count
adamc@1200:     in
adamc@1200:         count := n + 1;
adamc@1200:         n
adamc@1200:     end
adamc@1200: end
adamc@1200: 
adamc@1200: fun isKnown e =
adamc@1200:     case e of
adamc@1200:         Const _ => true
adamc@1200:       | Func (_, es) => List.all isKnown es
adamc@1200:       | Recd xes => List.all (isKnown o #2) xes
adamc@1200:       | Proj (e, _) => isKnown e
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun isFinish e =
adamc@1200:     case e of
adamc@1200:         Finish => true
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun simplify e =
adamc@1200:     case e of
adamc@1200:         Const _ => e
adamc@1200:       | Var _ => e
adamc@1208:       | Lvar n =>
adamc@1208:         (case IM.find (!unif, n) of
adamc@1208:              NONE => e
adamc@1208:            | SOME e => simplify e)
adamc@1215:       | Func (f, es) => Func (f, map simplify es)
adamc@1215:       | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
adamc@1215:       | Proj (e, s) => Proj (simplify e, s)
adamc@1200:       | Finish => Finish
adamc@1200: 
adamc@1212: datatype atom =
adamc@1212:          AReln of reln * exp list
adamc@1212:        | ACond of exp * prop
adamc@1212: 
adamc@1212: fun p_atom a =
adamc@1212:     p_prop (case a of
adamc@1212:                 AReln x => Reln x
adamc@1212:               | ACond x => Cond x)
adamc@1212: 
adamc@1202: fun lvarIn lv =
adamc@1202:     let
adamc@1202:         fun lvi e =
adamc@1202:             case e of
adamc@1202:                 Const _ => false
adamc@1202:               | Var _ => false
adamc@1202:               | Lvar lv' => lv' = lv
adamc@1202:               | Func (_, es) => List.exists lvi es
adamc@1202:               | Recd xes => List.exists (lvi o #2) xes
adamc@1202:               | Proj (e, _) => lvi e
adamc@1202:               | Finish => false
adamc@1202:     in
adamc@1202:         lvi
adamc@1202:     end
adamc@1202: 
adamc@1212: fun lvarInP lv =
adamc@1212:     let
adamc@1212:         fun lvi p =
adamc@1212:             case p of
adamc@1212:                 True => false
adamc@1212:               | False => false
adamc@1212:               | Unknown => true
adamc@1212:               | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212:               | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212:               | Reln (_, es) => List.exists (lvarIn lv) es
adamc@1212:               | Cond (e, p) => lvarIn lv e orelse lvi p
adamc@1212:     in
adamc@1212:         lvi
adamc@1212:     end
adamc@1212: 
adamc@1212: fun varIn lv =
adamc@1212:     let
adamc@1212:         fun lvi e =
adamc@1212:             case e of
adamc@1212:                 Const _ => false
adamc@1212:               | Lvar _ => false
adamc@1212:               | Var lv' => lv' = lv
adamc@1212:               | Func (_, es) => List.exists lvi es
adamc@1212:               | Recd xes => List.exists (lvi o #2) xes
adamc@1212:               | Proj (e, _) => lvi e
adamc@1212:               | Finish => false
adamc@1212:     in
adamc@1212:         lvi
adamc@1212:     end
adamc@1212: 
adamc@1212: fun varInP lv =
adamc@1212:     let
adamc@1212:         fun lvi p =
adamc@1212:             case p of
adamc@1212:                 True => false
adamc@1212:               | False => false
adamc@1212:               | Unknown => false
adamc@1212:               | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212:               | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212:               | Reln (_, es) => List.exists (varIn lv) es
adamc@1212:               | Cond (e, p) => varIn lv e orelse lvi p
adamc@1212:     in
adamc@1212:         lvi
adamc@1212:     end
adamc@1212: 
adamc@1202: fun eq' (e1, e2) =
adamc@1202:     case (e1, e2) of
adamc@1202:         (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202:       | (Var n1, Var n2) => n1 = n2
adamc@1202: 
adamc@1202:       | (Lvar n1, _) =>
adamc@1202:         (case IM.find (!unif, n1) of
adamc@1202:              SOME e1 => eq' (e1, e2)
adamc@1202:            | NONE =>
adamc@1202:              case e2 of
adamc@1202:                  Lvar n2 =>
adamc@1202:                  (case IM.find (!unif, n2) of
adamc@1202:                       SOME e2 => eq' (e1, e2)
adamc@1202:                     | NONE => n1 = n2
adamc@1208:                               orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202:                                       true))
adamc@1202:                | _ =>
adamc@1202:                  if lvarIn n1 e2 then
adamc@1202:                      false
adamc@1202:                  else
adamc@1202:                      (unif := IM.insert (!unif, n1, e2);
adamc@1202:                       true))
adamc@1202: 
adamc@1202:       | (_, Lvar n2) =>
adamc@1202:         (case IM.find (!unif, n2) of
adamc@1202:              SOME e2 => eq' (e1, e2)
adamc@1202:            | NONE =>
adamc@1202:              if lvarIn n2 e1 then
adamc@1202:                  false
adamc@1202:              else
adamc@1213:                  ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
adamc@1213:                                          ("e1", p_exp e1)];*)
adamc@1213:                   unif := IM.insert (!unif, n2, e1);
adamc@1202:                   true))
adamc@1202:                                        
adamc@1202:       | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202:       | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202:       | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202:       | (Finish, Finish) => true
adamc@1202:       | _ => false
adamc@1202: 
adamc@1202: fun eq (e1, e2) =
adamc@1202:     let
adamc@1203:         val saved = save ()
adamc@1202:     in
adamc@1202:         if eq' (simplify e1, simplify e2) then
adamc@1202:             true
adamc@1202:         else
adamc@1203:             (restore saved;
adamc@1202:              false)
adamc@1202:     end
adamc@1202: 
adamc@1208: val debug = ref false
adamc@1208: 
adamc@1211: fun eeq (e1, e2) =
adamc@1211:     case (e1, e2) of
adamc@1211:         (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211:       | (Var n1, Var n2) => n1 = n2
adamc@1211:       | (Lvar n1, Lvar n2) => n1 = n2
adamc@1211:       | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211:       | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211:                                   List.all (fn (x2, e2) =>
adamc@1211:                                                List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211:       | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211:       | (Finish, Finish) => true
adamc@1211:       | _ => false
adamc@1211:              
adamc@1208: (* Congruence closure *)
adamc@1208: structure Cc :> sig
adamc@1215:     type database
adamc@1215: 
adamc@1215:     exception Contradiction
adamc@1215:     exception Undetermined
adamc@1215: 
adamc@1215:     val database : unit -> database
adamc@1215: 
adamc@1215:     val assert : database * atom -> unit
adamc@1215:     val check : database * atom -> bool
adamc@1215: 
adamc@1215:     val p_database : database Print.printer
adamc@1218: 
adamc@1218:     val builtFrom : database * {Base : exp list, Derived : exp} -> bool
adamc@1208: end = struct
adamc@1208: 
adamc@1215: exception Contradiction
adamc@1215: exception Undetermined
adamc@1208: 
adamc@1215: structure CM = BinaryMapFn(struct
adamc@1215:                            type ord_key = Prim.t
adamc@1215:                            val compare = Prim.compare
adamc@1215:                            end)
adamc@1208: 
adamc@1215: datatype node = Node of {Rep : node ref option ref,
adamc@1215:                          Cons : node ref SM.map ref,
adamc@1215:                          Variety : variety,
adamc@1215:                          Known : bool ref}
adamc@1208: 
adamc@1215:      and variety =
adamc@1215:          Dt0 of string
adamc@1215:        | Dt1 of string * node ref
adamc@1215:        | Prim of Prim.t
adamc@1221:        | Recrd of node ref SM.map ref * bool
adamc@1215:        | VFinish
adamc@1215:        | Nothing
adamc@1208: 
adamc@1215: type representative = node ref
adamc@1215: 
adamc@1215: val finish = ref (Node {Rep = ref NONE,
adamc@1215:                         Cons = ref SM.empty,
adamc@1215:                         Variety = VFinish,
adamc@1218:                         Known = ref true})
adamc@1215: 
adamc@1215: type database = {Vars : representative IM.map ref,
adamc@1215:                  Consts : representative CM.map ref,
adamc@1215:                  Con0s : representative SM.map ref,
adamc@1215:                  Records : (representative SM.map * representative) list ref,
adamc@1215:                  Funcs : ((string * representative list) * representative) list ref }
adamc@1215: 
adamc@1215: fun database () = {Vars = ref IM.empty,
adamc@1215:                    Consts = ref CM.empty,
adamc@1215:                    Con0s = ref SM.empty,
adamc@1215:                    Records = ref [],
adamc@1215:                    Funcs = ref []}
adamc@1215: 
adamc@1215: fun unNode n =
adamc@1215:     case !n of
adamc@1215:         Node r => r
adamc@1215: 
adamc@1215: open Print
adamc@1215: val string = PD.string
adamc@1215: val newline = PD.newline
adamc@1215: 
adamc@1215: fun p_rep n =
adamc@1215:     case !(#Rep (unNode n)) of
adamc@1215:         SOME n => p_rep n
adamc@1215:       | NONE =>
adamc@1221:         box [string (Int.toString (Unsafe.cast n) ^ ":"),
adamc@1221:              space,
adamc@1221:              case #Variety (unNode n) of
adamc@1221:                  Nothing => string "?"
adamc@1221:                | Dt0 s => string ("Dt0(" ^ s ^ ")")
adamc@1221:                | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
adamc@1221:                                    space,
adamc@1221:                                    p_rep n,
adamc@1221:                                    string ")"]
adamc@1221:                | Prim p => Prim.p_t p
adamc@1221:                | Recrd (ref m, b) => box [string "{",
adamc@1221:                                           p_list (fn (x, n) => box [string x,
adamc@1221:                                                                     space,
adamc@1221:                                                                     string "=",
adamc@1221:                                                                     space,
adamc@1221:                                                                     p_rep n]) (SM.listItemsi m),
adamc@1221:                                           string "}",
adamc@1221:                                           if b then
adamc@1221:                                               box [space,
adamc@1221:                                                    string "(complete)"]
adamc@1221:                                           else
adamc@1221:                                               box []]
adamc@1221:                | VFinish => string "FINISH"]
adamc@1215: 
adamc@1215: fun p_database (db : database) =
adamc@1215:     box [string "Vars:",
adamc@1215:          newline,
adamc@1215:          p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
adamc@1215:                                                space,
adamc@1215:                                                string "=",
adamc@1215:                                                space,
adamc@1218:                                                p_rep n,
adamc@1218:                                                if !(#Known (unNode n)) then
adamc@1218:                                                    box [space,
adamc@1218:                                                         string "(known)"]
adamc@1218:                                                else
adamc@1218:                                                    box []]) (IM.listItemsi (!(#Vars db)))]
adamc@1215: 
adamc@1215: fun repOf (n : representative) : representative =
adamc@1215:     case !(#Rep (unNode n)) of
adamc@1215:         NONE => n
adamc@1215:       | SOME r =>
adamc@1215:         let
adamc@1215:             val r = repOf r
adamc@1215:         in
adamc@1215:             #Rep (unNode n) := SOME r;
adamc@1215:             r
adamc@1215:         end
adamc@1215: 
adamc@1215: fun markKnown r =
adamc@1221:     let
adamc@1221:         val r = repOf r
adamc@1221:     in
adamc@1221:         (*Print.preface ("markKnown", p_rep r);*)
adamc@1221:         if !(#Known (unNode r)) then
adamc@1221:             ()(*TextIO.print "Already known\n"*)
adamc@1221:         else
adamc@1221:             (#Known (unNode r) := true;
adamc@1221:              SM.app markKnown (!(#Cons (unNode r)));
adamc@1221:              case #Variety (unNode r) of
adamc@1221:                  Dt1 (_, r) => markKnown r
adamc@1221:                | Recrd (xes, _) => SM.app markKnown (!xes)
adamc@1221:                | _ => ())
adamc@1221:     end
adamc@1215: 
adamc@1215: fun representative (db : database, e) =
adamc@1208:     let
adamc@1215:         fun rep e =
adamc@1215:             case e of
adamc@1215:                 Const p => (case CM.find (!(#Consts db), p) of
adamc@1215:                                 SOME r => repOf r
adamc@1215:                               | NONE =>
adamc@1215:                                 let
adamc@1215:                                     val r = ref (Node {Rep = ref NONE,
adamc@1215:                                                        Cons = ref SM.empty,
adamc@1215:                                                        Variety = Prim p,
adamc@1219:                                                        Known = ref true})
adamc@1215:                                 in
adamc@1215:                                     #Consts db := CM.insert (!(#Consts db), p, r);
adamc@1215:                                     r
adamc@1215:                                 end)
adamc@1215:               | Var n => (case IM.find (!(#Vars db), n) of
adamc@1215:                               SOME r => repOf r
adamc@1215:                             | NONE =>
adamc@1215:                               let
adamc@1215:                                   val r = ref (Node {Rep = ref NONE,
adamc@1215:                                                      Cons = ref SM.empty,
adamc@1215:                                                      Variety = Nothing,
adamc@1215:                                                      Known = ref false})
adamc@1215:                               in
adamc@1215:                                   #Vars db := IM.insert (!(#Vars db), n, r);
adamc@1215:                                   r
adamc@1215:                               end)
adamc@1215:               | Lvar n =>
adamc@1215:                 (case IM.find (!unif, n) of
adamc@1215:                      NONE => raise Undetermined
adamc@1215:                    | SOME e => rep e)
adamc@1215:               | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
adamc@1215:                                             SOME r => repOf r
adamc@1215:                                           | NONE =>
adamc@1215:                                             let
adamc@1215:                                                 val r = ref (Node {Rep = ref NONE,
adamc@1215:                                                                    Cons = ref SM.empty,
adamc@1215:                                                                    Variety = Dt0 f,
adamc@1218:                                                                    Known = ref true})
adamc@1215:                                             in
adamc@1215:                                                 #Con0s db := SM.insert (!(#Con0s db), f, r);
adamc@1215:                                                 r
adamc@1215:                                             end)
adamc@1215:               | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
adamc@1215:               | Func (DtCon1 f, [e]) =>
adamc@1215:                 let
adamc@1215:                     val r = rep e
adamc@1215:                 in
adamc@1215:                     case SM.find (!(#Cons (unNode r)), f) of
adamc@1215:                         SOME r => repOf r
adamc@1215:                       | NONE =>
adamc@1215:                         let
adamc@1215:                             val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1215:                                                 Variety = Dt1 (f, r),
adamc@1221:                                                 Known = ref (!(#Known (unNode r)))})
adamc@1215:                         in
adamc@1215:                             #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
adamc@1215:                             r'
adamc@1215:                         end
adamc@1215:                 end
adamc@1215:               | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
adamc@1215:               | Func (UnCon f, [e]) =>
adamc@1215:                 let
adamc@1215:                     val r = rep e
adamc@1215:                 in
adamc@1215:                     case #Variety (unNode r) of
adamc@1215:                         Dt1 (f', n) => if f' = f then
adamc@1215:                                            repOf n
adamc@1215:                                        else
adamc@1215:                                            raise Contradiction
adamc@1215:                       | Nothing =>
adamc@1215:                         let
adamc@1215:                             val cons = ref SM.empty
adamc@1215:                             val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                                 Cons = cons,
adamc@1215:                                                 Variety = Nothing,
adamc@1221:                                                 Known = ref (!(#Known (unNode r)))})
adamc@1215: 
adamc@1215:                             val r'' = ref (Node {Rep = ref NONE,
adamc@1215:                                                  Cons = #Cons (unNode r),
adamc@1215:                                                  Variety = Dt1 (f, r'),
adamc@1215:                                                  Known = #Known (unNode r)})
adamc@1215:                         in
adamc@1215:                             cons := SM.insert (!cons, f, r'');
adamc@1215:                             #Rep (unNode r) := SOME r'';
adamc@1215:                             r'
adamc@1215:                         end
adamc@1215:                       | VFinish => r
adamc@1215:                       | _ => raise Contradiction
adamc@1215:                 end
adamc@1215:               | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
adamc@1215:               | Func (Other f, es) =>
adamc@1215:                 let
adamc@1215:                     val rs = map rep es
adamc@1215:                 in
adamc@1215:                     case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
adamc@1215:                         NONE =>
adamc@1215:                         let
adamc@1215:                             val r = ref (Node {Rep = ref NONE,
adamc@1215:                                                Cons = ref SM.empty,
adamc@1215:                                                Variety = Nothing,
adamc@1215:                                                Known = ref false})
adamc@1215:                         in
adamc@1215:                             #Funcs db := ((f, rs), r) :: (!(#Funcs db));
adamc@1215:                             r
adamc@1215:                         end
adamc@1215:                       | SOME (_, r) => repOf r
adamc@1215:                 end
adamc@1215:               | Recd xes =>
adamc@1215:                 let
adamc@1215:                     val xes = map (fn (x, e) => (x, rep e)) xes
adamc@1215:                     val len = length xes
adamc@1215:                 in
adamc@1215:                     case List.find (fn (xes', _) =>
adamc@1215:                                        SM.numItems xes' = len
adamc@1215:                                        andalso List.all (fn (x, n) =>
adamc@1215:                                                             case SM.find (xes', x) of
adamc@1215:                                                                 NONE => false
adamc@1215:                                                              | SOME n' => n = repOf n') xes)
adamc@1215:                          (!(#Records db)) of
adamc@1215:                         SOME (_, r) => repOf r
adamc@1215:                       | NONE =>
adamc@1215:                         let
adamc@1215:                             val xes = foldl SM.insert' SM.empty xes
adamc@1215: 
adamc@1215:                             val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1221:                                                 Variety = Recrd (ref xes, true),
adamc@1215:                                                 Known = ref false})
adamc@1215:                         in
adamc@1215:                             #Records db := (xes, r') :: (!(#Records db));
adamc@1215:                             r'
adamc@1215:                         end
adamc@1215:                 end
adamc@1215:               | Proj (e, f) =>
adamc@1215:                 let
adamc@1215:                     val r = rep e
adamc@1215:                 in
adamc@1215:                     case #Variety (unNode r) of
adamc@1221:                         Recrd (xes, _) =>
adamc@1215:                         (case SM.find (!xes, f) of
adamc@1215:                              SOME r => repOf r
adamc@1216:                            | NONE => let
adamc@1215:                                   val r = ref (Node {Rep = ref NONE,
adamc@1215:                                                      Cons = ref SM.empty,
adamc@1215:                                                      Variety = Nothing,
adamc@1221:                                                      Known = ref (!(#Known (unNode r)))})
adamc@1215:                               in
adamc@1215:                                  xes := SM.insert (!xes, f, r);
adamc@1215:                                  r
adamc@1215:                               end)
adamc@1215:                       | Nothing =>
adamc@1215:                         let
adamc@1215:                             val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1215:                                                 Variety = Nothing,
adamc@1221:                                                 Known = ref (!(#Known (unNode r)))})
adamc@1215:                                      
adamc@1215:                             val r'' = ref (Node {Rep = ref NONE,
adamc@1215:                                                  Cons = #Cons (unNode r),
adamc@1221:                                                  Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
adamc@1215:                                                  Known = #Known (unNode r)})
adamc@1215:                         in
adamc@1215:                             #Rep (unNode r) := SOME r'';
adamc@1215:                             r'
adamc@1215:                         end
adamc@1215:                       | VFinish => r 
adamc@1215:                       | _ => raise Contradiction                             
adamc@1215:                 end
adamc@1215:               | Finish => finish
adamc@1208:     in
adamc@1215:         rep e
adamc@1208:     end
adamc@1208: 
adamc@1215: fun assert (db, a) =
adamc@1215:     case a of
adamc@1215:         ACond _ => ()
adamc@1215:       | AReln x =>
adamc@1215:         case x of
adamc@1221:             (Known, [e]) =>
adamc@1221:             ((*Print.prefaces "Before" [("e", p_exp e),
adamc@1221:                                       ("db", p_database db)];*)
adamc@1221:              markKnown (representative (db, e))(*;
adamc@1221:              Print.prefaces "After" [("e", p_exp e),
adamc@1221:                                      ("db", p_database db)]*))
adamc@1215:           | (PCon0 f, [e]) =>
adamc@1215:             let
adamc@1215:                 val r = representative (db, e)
adamc@1215:             in
adamc@1215:                 case #Variety (unNode r) of
adamc@1215:                     Dt0 f' => if f = f' then
adamc@1215:                                   ()
adamc@1215:                               else
adamc@1215:                                   raise Contradiction
adamc@1215:                   | Nothing =>
adamc@1215:                     let
adamc@1215:                         val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                             Cons = ref SM.empty,
adamc@1215:                                             Variety = Dt0 f,
adamc@1215:                                             Known = ref false})
adamc@1215:                     in
adamc@1215:                         #Rep (unNode r) := SOME r'
adamc@1215:                     end
adamc@1215:                   | _ => raise Contradiction
adamc@1215:             end
adamc@1215:           | (PCon1 f, [e]) =>
adamc@1215:             let
adamc@1215:                 val r = representative (db, e)
adamc@1215:             in
adamc@1215:                 case #Variety (unNode r) of
adamc@1215:                     Dt1 (f', e') => if f = f' then
adamc@1215:                                         ()
adamc@1215:                                     else
adamc@1215:                                         raise Contradiction
adamc@1215:                   | Nothing =>
adamc@1215:                     let
adamc@1215:                         val r'' = ref (Node {Rep = ref NONE,
adamc@1215:                                              Cons = ref SM.empty,
adamc@1215:                                              Variety = Nothing,
adamc@1215:                                              Known = ref false})
adamc@1214: 
adamc@1215:                         val r' = ref (Node {Rep = ref NONE,
adamc@1215:                                             Cons = ref SM.empty,
adamc@1215:                                             Variety = Dt1 (f, r''),
adamc@1215:                                             Known = ref false})
adamc@1215:                     in
adamc@1215:                         #Rep (unNode r) := SOME r'
adamc@1215:                     end
adamc@1215:                   | _ => raise Contradiction
adamc@1215:             end
adamc@1215:           | (Eq, [e1, e2]) =>
adamc@1215:             let
adamc@1215:                 fun markEq (r1, r2) =
adamc@1215:                     if r1 = r2 then
adamc@1215:                         ()
adamc@1215:                     else case (#Variety (unNode r1), #Variety (unNode r2)) of
adamc@1215:                              (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
adamc@1215:                                                        ()
adamc@1215:                                                    else
adamc@1215:                                                        raise Contradiction
adamc@1215:                            | (Dt0 f1, Dt0 f2) => if f1 = f2 then
adamc@1215:                                                      ()
adamc@1215:                                                  else
adamc@1215:                                                      raise Contradiction
adamc@1215:                            | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
adamc@1215:                                                                  markEq (r1, r2)
adamc@1215:                                                              else
adamc@1215:                                                                  raise Contradiction
adamc@1221:                            | (Recrd (xes1, _), Recrd (xes2, _)) =>
adamc@1215:                              let
adamc@1215:                                  fun unif (xes1, xes2) =
adamc@1215:                                      SM.appi (fn (x, r1) =>
adamc@1215:                                                  case SM.find (xes2, x) of
adamc@1215:                                                      NONE => ()
adamc@1215:                                                    | SOME r2 => markEq (r1, r2)) xes1
adamc@1215:                              in
adamc@1215:                                  unif (!xes1, !xes2);
adamc@1215:                                  unif (!xes2, !xes1)
adamc@1215:                              end
adamc@1215:                            | (VFinish, VFinish) => ()
adamc@1218:                            | (Nothing, _) => mergeNodes (r1, r2)
adamc@1218:                            | (_, Nothing) => mergeNodes (r2, r1)
adamc@1215:                            | _ => raise Contradiction
adamc@1214: 
adamc@1218:                 and mergeNodes (r1, r2) =
adamc@1218:                     (#Rep (unNode r1) := SOME r2;
adamc@1218:                      if !(#Known (unNode r1)) then
adamc@1218:                          markKnown r2
adamc@1218:                      else
adamc@1218:                          ();
adamc@1218:                      if !(#Known (unNode r2)) then
adamc@1218:                          markKnown r1
adamc@1218:                      else
adamc@1218:                          ();
adamc@1218:                      #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
adamc@1218:                      compactFuncs ())
adamc@1218: 
adamc@1215:                 and compactFuncs () =
adamc@1214:                     let
adamc@1215:                         fun loop funcs =
adamc@1215:                             case funcs of
adamc@1215:                                 [] => []
adamc@1215:                               | (fr as ((f, rs), r)) :: rest =>
adamc@1215:                                 let
adamc@1215:                                     val rest = List.filter (fn ((f' : string, rs'), r') =>
adamc@1215:                                                                if f' = f
adamc@1215:                                                                   andalso ListPair.allEq (fn (r1, r2) =>
adamc@1215:                                                                                              repOf r1 = repOf r2)
adamc@1215:                                                                                          (rs, rs') then
adamc@1215:                                                                    (markEq (r, r');
adamc@1215:                                                                     false)
adamc@1215:                                                                else
adamc@1215:                                                                    true) rest
adamc@1215:                                 in
adamc@1215:                                     fr :: loop rest
adamc@1215:                                 end
adamc@1214:                     in
adamc@1215:                         #Funcs db := loop (!(#Funcs db))
adamc@1214:                     end
adamc@1215:             in
adamc@1215:                 markEq (representative (db, e1), representative (db, e2))
adamc@1215:             end
adamc@1215:           | _ => ()
adamc@1214: 
adamc@1215: fun check (db, a) =
adamc@1215:     case a of
adamc@1215:         ACond _ => false
adamc@1215:       | AReln x =>
adamc@1215:         case x of
adamc@1221:             (Known, [e]) =>
adamc@1221:             let
adamc@1221:                 fun isKnown r =
adamc@1221:                     let
adamc@1221:                         val r = repOf r
adamc@1221:                     in
adamc@1221:                         !(#Known (unNode r))
adamc@1221:                         orelse case #Variety (unNode r) of
adamc@1221:                                    Dt1 (_, r) => isKnown r
adamc@1221:                                  | Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
adamc@1221:                                  | _ => false
adamc@1221:                     end
adamc@1221: 
adamc@1221:                 val r = representative (db, e)
adamc@1221:             in
adamc@1221:                 isKnown r
adamc@1221:             end
adamc@1215:           | (PCon0 f, [e]) =>
adamc@1215:             (case #Variety (unNode (representative (db, e))) of
adamc@1215:                  Dt0 f' => f' = f
adamc@1215:                | _ => false)
adamc@1215:           | (PCon1 f, [e]) =>
adamc@1215:             (case #Variety (unNode (representative (db, e))) of
adamc@1215:                  Dt1 (f', _) => f' = f
adamc@1215:                | _ => false)
adamc@1215:           | (Eq, [e1, e2]) =>
adamc@1214:             let
adamc@1215:                 val r1 = representative (db, e1)
adamc@1215:                 val r2 = representative (db, e2)
adamc@1214:             in
adamc@1215:                 repOf r1 = repOf r2
adamc@1214:             end
adamc@1215:           | _ => false
adamc@1212: 
adamc@1218: fun builtFrom (db, {Base = bs, Derived = d}) =
adamc@1218:     let
adamc@1218:         val bs = map (fn b => representative (db, b)) bs
adamc@1218: 
adamc@1218:         fun loop d =
adamc@1218:             let
adamc@1218:                 val d = repOf d
adamc@1218:             in
adamc@1218:                 List.exists (fn b => repOf b = d) bs
adamc@1218:                 orelse case #Variety (unNode d) of
adamc@1218:                            Dt0 _ => true
adamc@1218:                          | Dt1 (_, d) => loop d
adamc@1218:                          | Prim _ => true
adamc@1221:                          | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
adamc@1218:                          | VFinish => true
adamc@1218:                          | Nothing => false
adamc@1218:             end
adamc@1218:     in
adamc@1218:         loop (representative (db, d))
adamc@1218:     end
adamc@1218: 
adamc@1208: end
adamc@1208: 
adamc@1215: fun decomp fals or =
adamc@1215:     let
adamc@1215:         fun decomp p k =
adamc@1215:             case p of
adamc@1215:                 True => k []
adamc@1215:               | False => fals
adamc@1215:               | Unknown => k []
adamc@1215:               | And (p1, p2) => 
adamc@1215:                 decomp p1 (fn ps1 =>
adamc@1215:                               decomp p2 (fn ps2 =>
adamc@1215:                                             k (ps1 @ ps2)))
adamc@1215:               | Or (p1, p2) =>
adamc@1215:                 or (decomp p1 k, fn () => decomp p2 k)
adamc@1215:               | Reln x => k [AReln x]
adamc@1215:               | Cond x => k [ACond x]
adamc@1215:     in
adamc@1215:         decomp
adamc@1215:     end
adamc@1202: 
adamc@1218: fun imply (hyps, goals, outs) =
adamc@1218:     let
adamc@1218:         fun gls goals onFail acc =
adamc@1218:             case goals of
adamc@1218:                 [] =>
adamc@1218:                 (let
adamc@1218:                      val cc = Cc.database ()
adamc@1218:                      val () = app (fn a => Cc.assert (cc, a)) hyps
adamc@1218:                  in
adamc@1221:                      (*Print.preface ("db", Cc.p_database cc);*)
adamc@1218:                      (List.all (fn a =>
adamc@1218:                                    if Cc.check (cc, a) then
adamc@1218:                                        true
adamc@1218:                                    else
adamc@1218:                                        ((*Print.prefaces "Can't prove"
adamc@1218:                                                        [("a", p_atom a),
adamc@1218:                                                         ("hyps", Print.p_list p_atom hyps),
adamc@1218:                                                         ("db", Cc.p_database cc)];*)
adamc@1218:                                         false)) acc
adamc@1218:                       (*andalso (Print.preface ("Finding", Cc.p_database cc); true)*)
adamc@1220:                       andalso (case outs of
adamc@1220:                                    NONE => true
adamc@1220:                                  | SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
adamc@1220:                                                                    Base = outs})))
adamc@1218:                      handle Cc.Contradiction => false
adamc@1218:                  end handle Cc.Undetermined => false)
adamc@1218:                 orelse onFail ()
adamc@1218:               | (g as AReln (Sql gf, [ge])) :: goals =>
adamc@1218:                 let
adamc@1218:                     fun hps hyps =
adamc@1218:                         case hyps of
adamc@1218:                             [] => gls goals onFail (g :: acc)
adamc@1218:                           | (h as AReln (Sql hf, [he])) :: hyps =>
adamc@1218:                             if gf = hf then
adamc@1218:                                 let
adamc@1218:                                     val saved = save ()
adamc@1218:                                 in
adamc@1218:                                     if eq (ge, he) then
adamc@1218:                                         let
adamc@1218:                                             val changed = IM.numItems (!unif)
adamc@1218:                                                           <> IM.numItems saved
adamc@1218:                                         in
adamc@1218:                                             gls goals (fn () => (restore saved;
adamc@1218:                                                                  changed
adamc@1218:                                                                  andalso hps hyps))
adamc@1218:                                                 acc
adamc@1218:                                         end
adamc@1218:                                     else
adamc@1218:                                         hps hyps
adamc@1218:                                 end
adamc@1218:                             else
adamc@1218:                                 hps hyps
adamc@1218:                           | _ :: hyps => hps hyps 
adamc@1218:                 in
adamc@1218:                     hps hyps
adamc@1218:                 end
adamc@1218:               | g :: goals => gls goals onFail (g :: acc)
adamc@1218:     in
adamc@1218:         reset ();
adamc@1218:         (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
adamc@1218:                                    ("goals", Print.p_list p_atom goals)];*)
adamc@1218:         gls goals (fn () => false) []
adamc@1218:     end handle Cc.Contradiction => true
adamc@1200: 
adamc@1200: fun patCon pc =
adamc@1200:     case pc of
adamc@1200:         PConVar n => "C" ^ Int.toString n
adamc@1200:       | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200: 
adamc@1200: datatype chunk =
adamc@1200:          String of string
adamc@1200:        | Exp of Mono.exp
adamc@1200: 
adamc@1200: fun chunkify e =
adamc@1200:     case #1 e of
adamc@1200:         EPrim (Prim.String s) => [String s]
adamc@1207:       | EStrcat (e1, e2) =>
adamc@1207:         let
adamc@1207:             val chs1 = chunkify e1
adamc@1207:             val chs2 = chunkify e2
adamc@1207:         in
adamc@1207:             case chs2 of
adamc@1207:                 String s2 :: chs2' =>
adamc@1207:                 (case List.last chs1 of
adamc@1207:                      String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207:                    | _ => chs1 @ chs2)
adamc@1207:               | _ => chs1 @ chs2
adamc@1207:         end
adamc@1200:       | _ => [Exp e]
adamc@1200: 
adamc@1201: type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201: 
adamc@1201: fun always v chs = SOME (v, chs)
adamc@1201: 
adamc@1202: fun parse p s =
adamc@1202:     case p (chunkify s) of
adamc@1201:         SOME (v, []) => SOME v
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1201: fun const s chs =
adamc@1201:     case chs of
adamc@1201:         String s' :: chs => if String.isPrefix s s' then
adamc@1201:                                 SOME ((), if size s = size s' then
adamc@1201:                                               chs
adamc@1201:                                           else
adamc@1201:                                               String (String.extract (s', size s, NONE)) :: chs)
adamc@1201:                             else
adamc@1201:                                 NONE
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1201: fun follow p1 p2 chs =
adamc@1201:     case p1 chs of
adamc@1201:         NONE => NONE
adamc@1201:       | SOME (v1, chs) =>
adamc@1201:         case p2 chs of
adamc@1201:             NONE => NONE
adamc@1201:           | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201: 
adamc@1201: fun wrap p f chs =
adamc@1201:     case p chs of
adamc@1201:         NONE => NONE
adamc@1201:       | SOME (v, chs) => SOME (f v, chs)
adamc@1201: 
adamc@1209: fun wrapP p f chs =
adamc@1209:     case p chs of
adamc@1209:         NONE => NONE
adamc@1209:       | SOME (v, chs) =>
adamc@1209:         case f v of
adamc@1209:             NONE => NONE
adamc@1209:           | SOME r => SOME (r, chs)
adamc@1209: 
adamc@1201: fun alt p1 p2 chs =
adamc@1201:     case p1 chs of
adamc@1201:         NONE => p2 chs
adamc@1201:       | v => v
adamc@1201: 
adamc@1207: fun altL ps =
adamc@1207:     case rev ps of
adamc@1207:         [] => (fn _ => NONE)
adamc@1207:       | p :: ps =>
adamc@1207:         foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207: 
adamc@1204: fun opt p chs =
adamc@1204:     case p chs of
adamc@1204:         NONE => SOME (NONE, chs)
adamc@1204:       | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204: 
adamc@1201: fun skip cp chs =
adamc@1201:     case chs of
adamc@1201:         String "" :: chs => skip cp chs
adamc@1201:       | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201:                                 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201:                             else
adamc@1201:                                 SOME ((), chs)
adamc@1201:       | _ => SOME ((), chs)
adamc@1201: 
adamc@1201: fun keep cp chs =
adamc@1201:     case chs of
adamc@1201:         String "" :: chs => keep cp chs
adamc@1201:       | String s :: chs' =>
adamc@1201:         let
adamc@1201:             val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201:         in
adamc@1201:             if Substring.isEmpty befor then
adamc@1201:                 NONE
adamc@1201:             else
adamc@1201:                 SOME (Substring.string befor,
adamc@1201:                       if Substring.isEmpty after then
adamc@1201:                           chs'
adamc@1201:                       else
adamc@1201:                           String (Substring.string after) :: chs')
adamc@1201:         end
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1204: fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204:                         (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204: 
adamc@1204: fun log name p chs =
adamc@1206:     (if !debug then
adamc@1206:          case chs of
adamc@1207:              String s :: _ => print (name ^ ": " ^ s ^ "\n")
adamc@1206:            | _ => print (name ^ ": blocked!\n")
adamc@1206:      else
adamc@1206:          ();
adamc@1204:      p chs)
adamc@1201: 
adamc@1201: fun list p chs =
adamc@1207:     altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207:                (fn (v, ((), ls)) => v :: ls),
adamc@1207:           wrap (ws p) (fn v => [v]),
adamc@1207:           always []] chs
adamc@1201: 
adamc@1201: val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201: 
adamc@1211: val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211:                                        SOME (String.extract (s, 2, NONE))
adamc@1201:                                    else
adamc@1211:                                        NONE)
adamc@1211: val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211:                                         SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211:                                               ^ String.extract (s, 4, NONE))
adamc@1211:                                     else
adamc@1211:                                         NONE)
adamc@1201: 
adamc@1211: val field = wrap (follow t_ident
adamc@1201:                          (follow (const ".")
adamc@1201:                                  uw_ident))
adamc@1201:                  (fn (t, ((), f)) => (t, f))
adamc@1201: 
adamc@1206: datatype Rel =
adamc@1206:          Exps of exp * exp -> prop
adamc@1206:        | Props of prop * prop -> prop
adamc@1206: 
adamc@1204: datatype sqexp =
adamc@1206:          SqConst of Prim.t
adamc@1206:        | Field of string * string
adamc@1206:        | Binop of Rel * sqexp * sqexp
adamc@1207:        | SqKnown of sqexp
adamc@1207:        | Inj of Mono.exp
adamc@1211:        | SqFunc of string * sqexp
adamc@1211:        | Count
adamc@1204: 
adamc@1210: fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210: 
adamc@1210: val sqbrel = altL [cmp "=" Eq,
adamc@1210:                    cmp "<>" Ne,
adamc@1210:                    cmp "<=" Le,
adamc@1210:                    cmp "<" Lt,
adamc@1210:                    cmp ">=" Ge,
adamc@1210:                    cmp ">" Gt,
adamc@1207:                    wrap (const "AND") (fn () => Props And),
adamc@1207:                    wrap (const "OR") (fn () => Props Or)]
adamc@1204: 
adamc@1204: datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204: 
adamc@1209: fun string chs =
adamc@1206:     case chs of
adamc@1209:         String s :: chs =>
adamc@1209:         if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209:             let
adamc@1209:                 fun loop (cs, acc) =
adamc@1209:                     case cs of
adamc@1209:                         [] => NONE
adamc@1209:                       | c :: cs =>
adamc@1209:                         if c = #"'" then
adamc@1209:                             SOME (String.implode (rev acc), cs)
adamc@1209:                         else if c = #"\\" then
adamc@1209:                             case cs of
adamc@1209:                                 c :: cs => loop (cs, c :: acc)
adamc@1209:                               | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209:                         else
adamc@1209:                             loop (cs, c :: acc)
adamc@1209:             in
adamc@1209:                 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209:                     NONE => NONE
adamc@1209:                   | SOME (s, []) => SOME (s, chs)
adamc@1209:                   | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209:             end
adamc@1209:         else
adamc@1209:             NONE
adamc@1209:       | _ => NONE                            
adamc@1206: 
adamc@1209: val prim =
adamc@1209:     altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209:                               (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209:                        (opt (const "::float8"))) #1,
adamc@1209:           wrap (follow (wrapP (keep Char.isDigit)
adamc@1209:                               (Option.map Prim.Int o Int64.fromString))
adamc@1209:                        (opt (const "::int8"))) #1,
adamc@1209:           wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209:                (Prim.String o #1 o #2)]
adamc@1206: 
adamc@1207: fun known' chs =
adamc@1207:     case chs of
adamc@1207:         Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207:       | _ => NONE
adamc@1207: 
adamc@1207: fun sqlify chs =
adamc@1207:     case chs of
adamc@1207:         Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207:         if String.isPrefix "sqlify" f then
adamc@1207:             SOME (e, chs)
adamc@1207:         else
adamc@1207:             NONE
adamc@1207:       | _ => NONE
adamc@1207: 
adamc@1211: fun constK s = wrap (const s) (fn () => s)
adamc@1211: 
adamc@1211: val funcName = altL [constK "COUNT",
adamc@1211:                      constK "MIN",
adamc@1211:                      constK "MAX",
adamc@1211:                      constK "SUM",
adamc@1211:                      constK "AVG"]
adamc@1211: 
adamc@1204: fun sqexp chs =
adamc@1206:     log "sqexp"
adamc@1207:     (altL [wrap prim SqConst,
adamc@1211:            wrap field Field,
adamc@1207:            wrap known SqKnown,
adamc@1211:            wrap func SqFunc,
adamc@1211:            wrap (const "COUNT(*)") (fn () => Count),
adamc@1207:            wrap sqlify Inj,
adamc@1211:            wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211:                                                                   (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211:                 (fn ((), (e, _)) => e),
adamc@1207:            wrap (follow (ws (const "("))
adamc@1207:                         (follow (wrap
adamc@1207:                                      (follow sqexp
adamc@1207:                                              (alt
adamc@1207:                                                   (wrap
adamc@1207:                                                        (follow (ws sqbrel)
adamc@1207:                                                                (ws sqexp))
adamc@1207:                                                        inl)
adamc@1207:                                                   (always (inr ()))))
adamc@1207:                                      (fn (e1, sm) =>
adamc@1207:                                          case sm of
adamc@1207:                                              inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207:                                            | inr () => e1))
adamc@1207:                                 (const ")")))
adamc@1207:                 (fn ((), (e, ())) => e)])
adamc@1207:     chs
adamc@1206: 
adamc@1207: and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211:                      (fn ((), ((), (e, ()))) => e) chs
adamc@1211:                 
adamc@1211: and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211:                     (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211: 
adamc@1211: datatype sitem =
adamc@1211:          SqField of string * string
adamc@1211:        | SqExp of sqexp * string
adamc@1211: 
adamc@1211: val sitem = alt (wrap field SqField)
adamc@1211:             (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211:              (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207: 
adamc@1207: val select = log "select"
adamc@1207:              (wrap (follow (const "SELECT ") (list sitem))
adamc@1207:                    (fn ((), ls) => ls))
adamc@1201: 
adamc@1201: val fitem = wrap (follow uw_ident
adamc@1201:                          (follow (const " AS ")
adamc@1201:                                  t_ident))
adamc@1201:                  (fn (t, ((), f)) => (t, f))
adamc@1201: 
adamc@1207: val from = log "from"
adamc@1207:            (wrap (follow (const "FROM ") (list fitem))
adamc@1207:                  (fn ((), ls) => ls))
adamc@1201: 
adamc@1204: val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204:            (fn ((), ls) => ls)
adamc@1204: 
adamc@1207: val query = log "query"
adamc@1207:                 (wrap (follow (follow select from) (opt wher))
adamc@1207:                       (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201: 
adamc@1220: datatype dml =
adamc@1220:          Insert of string * (string * sqexp) list
adamc@1221:        | Delete of string * sqexp
adamc@1220: 
adamc@1220: val insert = log "insert"
adamc@1220:              (wrapP (follow (const "INSERT INTO ")
adamc@1220:                             (follow uw_ident
adamc@1220:                                     (follow (const " (")
adamc@1220:                                             (follow (list uw_ident)
adamc@1220:                                                     (follow (const ") VALUES (")
adamc@1220:                                                             (follow (list sqexp)
adamc@1220:                                                                     (const ")")))))))
adamc@1220:               (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
adamc@1221:                   (SOME (tab, ListPair.zipEq (fs, es)))
adamc@1220:                   handle ListPair.UnequalLengths => NONE))
adamc@1220: 
adamc@1221: val delete = log "delete"
adamc@1221:                  (wrap (follow (const "DELETE FROM ")
adamc@1221:                                (follow uw_ident
adamc@1221:                                        (follow (const " AS T_T WHERE ")
adamc@1221:                                                sqexp)))
adamc@1221:                        (fn ((), (tab, ((), es))) => (tab, es)))
adamc@1221: 
adamc@1220: val dml = log "dml"
adamc@1221:               (altL [wrap insert Insert,
adamc@1221:                      wrap delete Delete])
adamc@1220: 
adamc@1215: fun removeDups (ls : (string * string) list) =
adamc@1211:     case ls of
adamc@1211:         [] => []
adamc@1211:       | x :: ls =>
adamc@1211:         let
adamc@1211:             val ls = removeDups ls
adamc@1211:         in
adamc@1211:             if List.exists (fn x' => x' = x) ls then
adamc@1211:                 ls  
adamc@1211:             else
adamc@1211:                 x :: ls
adamc@1211:         end
adamc@1211: 
adamc@1212: datatype queryMode =
adamc@1218:          SomeCol
adamc@1212:        | AllCols of exp
adamc@1212: 
adamc@1220: fun expIn rv env rvOf =
adamc@1220:     let
adamc@1220:         fun expIn (e, rvN) =
adamc@1220:             let
adamc@1220:                 fun default () =
adamc@1220:                     let
adamc@1220:                         val (rvN, e) = rv rvN
adamc@1220:                     in
adamc@1220:                         (inl e, rvN)
adamc@1220:                     end
adamc@1220:             in
adamc@1220:                 case e of
adamc@1220:                     SqConst p => (inl (Const p), rvN)
adamc@1220:                   | Field (v, f) => (inl (Proj (rvOf v, f)), rvN)
adamc@1220:                   | Binop (bo, e1, e2) =>
adamc@1220:                     let
adamc@1220:                         val (e1, rvN) = expIn (e1, rvN)
adamc@1220:                         val (e2, rvN) = expIn (e2, rvN)
adamc@1220:                     in
adamc@1220:                         (inr (case (bo, e1, e2) of
adamc@1220:                                   (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1220:                                 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1220:                                 | _ => Unknown), rvN)
adamc@1220:                     end
adamc@1220:                   | SqKnown e =>
adamc@1220:                     (case expIn (e, rvN) of
adamc@1220:                          (inl e, rvN) => (inr (Reln (Known, [e])), rvN)
adamc@1220:                        | _ => (inr Unknown, rvN))
adamc@1220:                   | Inj e =>
adamc@1220:                     let
adamc@1220:                         fun deinj e =
adamc@1220:                             case #1 e of
adamc@1220:                                 ERel n => (List.nth (env, n), rvN)
adamc@1220:                               | EField (e, f) =>
adamc@1220:                                 let
adamc@1220:                                     val (e, rvN) = deinj e
adamc@1220:                                 in
adamc@1220:                                     (Proj (e, f), rvN)
adamc@1220:                                 end
adamc@1220:                               | _ =>
adamc@1220:                                 let
adamc@1220:                                     val (rvN, e) = rv rvN
adamc@1220:                                 in
adamc@1220:                                     (e, rvN)
adamc@1220:                                 end
adamc@1220: 
adamc@1220:                         val (e, rvN) = deinj e
adamc@1220:                     in
adamc@1220:                         (inl e, rvN)
adamc@1220:                     end
adamc@1220:                   | SqFunc (f, e) =>
adamc@1220:                     (case expIn (e, rvN) of
adamc@1220:                          (inl e, rvN) => (inl (Func (Other f, [e])), rvN)
adamc@1220:                        | _ => default ())
adamc@1220:                      
adamc@1220:                   | Count => default ()
adamc@1220:             end
adamc@1220:     in
adamc@1220:         expIn
adamc@1220:     end
adamc@1216: 
adamc@1214: fun queryProp env rvN rv oe e =
adamc@1216:     let
adamc@1216:         fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1216:                                  ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1218:                           (rvN, Unknown, Unknown, [], []))
adamc@1216:     in
adamc@1216:         case parse query e of
adamc@1216:             NONE => default ()
adamc@1216:           | SOME r =>
adamc@1216:             let
adamc@1216:                 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1216:                                                        let
adamc@1216:                                                            val (rvN, e) = rv rvN
adamc@1216:                                                        in
adamc@1216:                                                            ((v, e), rvN)
adamc@1216:                                                        end) rvN (#From r)
adamc@1214: 
adamc@1216:                 fun rvOf v =
adamc@1216:                     case List.find (fn (v', _) => v' = v) rvs of
adamc@1216:                         NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1216:                       | SOME (_, e) => e
adamc@1214: 
adamc@1216:                 fun usedFields e =
adamc@1216:                     case e of
adamc@1216:                         SqConst _ => []
adamc@1216:                       | Field (v, f) => [(v, f)]
adamc@1216:                       | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1216:                       | SqKnown _ => []
adamc@1216:                       | Inj _ => []
adamc@1216:                       | SqFunc (_, e) => usedFields e
adamc@1216:                       | Count => []
adamc@1214: 
adamc@1216:                 val p =
adamc@1216:                     foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1211: 
adamc@1220:                 val expIn = expIn rv env rvOf
adamc@1205: 
adamc@1220:                 val (p, rvN) = case #Where r of
adamc@1220:                                    NONE => (p, rvN)
adamc@1220:                                  | SOME e =>
adamc@1220:                                    case expIn (e, rvN) of
adamc@1220:                                        (inr p', rvN) => (And (p, p'), rvN)
adamc@1220:                                      | _ => (p, rvN)
adamc@1210: 
adamc@1216:                 fun normal () =
adamc@1218:                     case oe of
adamc@1218:                         SomeCol =>
adamc@1220:                         let
adamc@1220:                             val (sis, rvN) =
adamc@1220:                                 ListUtil.foldlMap
adamc@1220:                                     (fn (si, rvN) =>
adamc@1220:                                         case si of
adamc@1220:                                             SqField (v, f) => (Proj (rvOf v, f), rvN)
adamc@1220:                                           | SqExp (e, f) =>
adamc@1220:                                             case expIn (e, rvN) of
adamc@1220:                                                 (inr _, _) =>
adamc@1220:                                                 let
adamc@1220:                                                     val (rvN, e) = rv rvN
adamc@1220:                                                 in
adamc@1220:                                                     (e, rvN)
adamc@1220:                                                 end
adamc@1220:                                               | (inl e, rvN) => (e, rvN)) rvN (#Select r)
adamc@1220:                         in
adamc@1220:                             (rvN, p, True, sis)
adamc@1220:                         end
adamc@1218:                       | AllCols oe =>
adamc@1220:                         let
adamc@1220:                             val (p', rvN) =
adamc@1220:                                 foldl (fn (si, (p, rvN)) =>
adamc@1220:                                           let
adamc@1220:                                               val (p', rvN) =
adamc@1220:                                                   case si of
adamc@1220:                                                       SqField (v, f) => (Reln (Eq, [Proj (Proj (oe, v), f),
adamc@1220:                                                                                     Proj (rvOf v, f)]), rvN)
adamc@1220:                                                     | SqExp (e, f) =>
adamc@1220:                                                       case expIn (e, rvN) of
adamc@1220:                                                           (inr p, rvN) => (Cond (Proj (oe, f), p), rvN)
adamc@1220:                                                         | (inl e, rvN) => (Reln (Eq, [Proj (oe, f), e]), rvN)
adamc@1220:                                           in
adamc@1220:                                               (And (p, p'), rvN)
adamc@1220:                                           end)
adamc@1220:                                       (True, rvN) (#Select r)
adamc@1220:                         in
adamc@1220:                             (rvN, And (p, p'), True, [])
adamc@1220:                         end
adamc@1217: 
adamc@1218:                 val (rvN, p, wp, outs) =
adamc@1217:                     case #Select r of
adamc@1217:                         [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1217:                         (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1217:                              Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1218:                              (case oe of
adamc@1218:                                   SomeCol =>
adamc@1218:                                   let
adamc@1218:                                       val (rvN, oe) = rv rvN
adamc@1218:                                   in
adamc@1218:                                       (rvN,
adamc@1218:                                        Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
adamc@1218:                                            And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1218:                                                 p)),
adamc@1218:                                        Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1218:                                        [oe])
adamc@1218:                                   end
adamc@1218:                                 | AllCols oe =>
adamc@1218:                                   let
adamc@1221:                                       fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
adamc@1218:                                   in
adamc@1218:                                       (rvN,
adamc@1221:                                        Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
adamc@1221:                                            And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1218:                                                 p)),
adamc@1221:                                        oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1218:                                        [])
adamc@1218:                                   end)
adamc@1217:                            | _ => normal ())
adamc@1217:                       | _ => normal ()
adamc@1216:             in
adamc@1217:                 (rvN, p, wp, case #Where r of
adamc@1217:                                  NONE => []
adamc@1218:                                | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e), outs)
adamc@1216:             end
adamc@1220:     end
adamc@1220: 
adamc@1220: fun insertProp rvN rv e =
adamc@1220:     let
adamc@1220:         fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1220:                                  ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1220:                           Unknown)
adamc@1220:     in
adamc@1220:         case parse query e of
adamc@1220:             NONE => default ()
adamc@1220:           | SOME r =>
adamc@1220:             let
adamc@1220:                 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1220:                                                        let
adamc@1220:                                                            val (rvN, e) = rv rvN
adamc@1220:                                                        in
adamc@1220:                                                            ((v, e), rvN)
adamc@1220:                                                        end) rvN (#From r)
adamc@1220: 
adamc@1220:                 fun rvOf v =
adamc@1220:                     case List.find (fn (v', _) => v' = v) rvs of
adamc@1220:                         NONE => raise Fail "Iflow.insertProp: Bad table variable"
adamc@1220:                       | SOME (_, e) => e
adamc@1220: 
adamc@1220:                 val p =
adamc@1220:                     foldl (fn ((t, v), p) =>
adamc@1220:                               let
adamc@1220:                                   val t =
adamc@1220:                                       case v of
adamc@1220:                                           "New" => "$New"
adamc@1220:                                         | _ => t
adamc@1220:                               in
adamc@1220:                                   And (p, Reln (Sql t, [rvOf v]))
adamc@1220:                               end) True (#From r)
adamc@1220: 
adamc@1220:                 val expIn = expIn rv [] rvOf
adamc@1220:             in
adamc@1220:                 case #Where r of
adamc@1220:                     NONE => p
adamc@1220:                   | SOME e =>
adamc@1220:                     case expIn (e, rvN) of
adamc@1220:                         (inr p', _) => And (p, p')
adamc@1220:                       | _ => p
adamc@1220:             end
adamc@1216:     end
adamc@1200: 
adamc@1221: fun deleteProp rvN rv e =
adamc@1221:     let
adamc@1221:         fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1221:                                  ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1221:                           Unknown)
adamc@1221:     in
adamc@1221:         case parse query e of
adamc@1221:             NONE => default ()
adamc@1221:           | SOME r =>
adamc@1221:             let
adamc@1221:                 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1221:                                                        let
adamc@1221:                                                            val (rvN, e) = rv rvN
adamc@1221:                                                        in
adamc@1221:                                                            ((v, e), rvN)
adamc@1221:                                                        end) rvN (#From r)
adamc@1221: 
adamc@1221:                 fun rvOf v =
adamc@1221:                     case List.find (fn (v', _) => v' = v) rvs of
adamc@1221:                         NONE => raise Fail "Iflow.deleteProp: Bad table variable"
adamc@1221:                       | SOME (_, e) => e
adamc@1221: 
adamc@1221:                 val p =
adamc@1221:                     foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1221: 
adamc@1221:                 val expIn = expIn rv [] rvOf
adamc@1221:             in
adamc@1221:                 And (Reln (Sql "$Old", [rvOf "Old"]),
adamc@1221:                      case #Where r of
adamc@1221:                          NONE => p
adamc@1221:                        | SOME e =>
adamc@1221:                          case expIn (e, rvN) of
adamc@1221:                              (inr p', _) => And (p, p')
adamc@1221:                            | _ => p)
adamc@1221:             end
adamc@1221:     end
adamc@1221: 
adamc@1211: fun evalPat env e (pt, _) =
adamc@1211:     case pt of
adamc@1211:         PWild => (env, True)
adamc@1211:       | PVar _ => (e :: env, True)
adamc@1211:       | PPrim _ => (env, True)
adamc@1215:       | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
adamc@1211:       | PCon (_, pc, SOME pt) =>
adamc@1211:         let
adamc@1215:             val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211:         in
adamc@1215:             (env, And (p, Reln (PCon1 (patCon pc), [e])))
adamc@1211:         end
adamc@1211:       | PRecord xpts =>
adamc@1211:         foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211:                   let
adamc@1211:                       val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211:                   in
adamc@1211:                       (env, And (p', p))
adamc@1211:                   end) (env, True) xpts
adamc@1215:       | PNone _ => (env, Reln (PCon0 "None", [e]))
adamc@1211:       | PSome (_, pt) =>
adamc@1211:         let
adamc@1215:             val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211:         in
adamc@1215:             (env, And (p, Reln (PCon1 "Some", [e])))
adamc@1211:         end
adamc@1211: 
adamc@1211: fun peq (p1, p2) =
adamc@1211:     case (p1, p2) of
adamc@1211:         (True, True) => true
adamc@1211:       | (False, False) => true
adamc@1211:       | (Unknown, Unknown) => true
adamc@1211:       | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211:       | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211:       | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212:       | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211:       | _ => false
adamc@1211: 
adamc@1211: fun removeRedundant p1 =
adamc@1211:     let
adamc@1211:         fun rr p2 =
adamc@1211:             if peq (p1, p2) then
adamc@1211:                 True
adamc@1211:             else
adamc@1211:                 case p2 of
adamc@1211:                     And (x, y) => And (rr x, rr y)
adamc@1211:                   | Or (x, y) => Or (rr x, rr y)
adamc@1211:                   | _ => p2
adamc@1211:     in
adamc@1211:         rr
adamc@1211:     end
adamc@1211: 
adamc@1218: datatype cflow = Case | Where
adamc@1218: datatype flow = Data | Control of cflow
adamc@1218: type check = ErrorMsg.span * exp * prop
adamc@1221: type dml = ErrorMsg.span * prop
adamc@1218: 
adamc@1217: structure St :> sig
adamc@1217:     type t
adamc@1217:     val create : {Var : int,
adamc@1217:                   Ambient : prop} -> t
adamc@1217: 
adamc@1217:     val curVar : t -> int
adamc@1217:     val nextVar : t -> t * int
adamc@1217: 
adamc@1217:     val ambient : t -> prop
adamc@1217:     val setAmbient : t * prop -> t
adamc@1217: 
adamc@1218:     val paths : t -> (check * cflow) list
adamc@1218:     val addPath : t * (check * cflow) -> t
adamc@1218:     val addPaths : t * (check * cflow) list -> t
adamc@1218:     val clearPaths : t -> t
adamc@1218:     val setPaths : t * (check * cflow) list -> t
adamc@1217: 
adamc@1218:     val sent : t -> (check * flow) list
adamc@1218:     val addSent : t * (check * flow) -> t
adamc@1218:     val setSent : t * (check * flow) list -> t
adamc@1220: 
adamc@1221:     val inserted : t -> dml list
adamc@1221:     val addInsert : t * dml -> t
adamc@1221: 
adamc@1221:     val deleted : t -> dml list
adamc@1221:     val addDelete : t * dml -> t
adamc@1217: end = struct
adamc@1217: 
adamc@1217: type t = {Var : int,
adamc@1217:           Ambient : prop,
adamc@1218:           Path : (check * cflow) list,
adamc@1220:           Sent : (check * flow) list,
adamc@1221:           Insert : dml list,
adamc@1221:           Delete : dml list}
adamc@1217: 
adamc@1217: fun create {Var = v, Ambient = p} = {Var = v,
adamc@1217:                                      Ambient = p,
adamc@1217:                                      Path = [],
adamc@1220:                                      Sent = [],
adamc@1221:                                      Insert = [],
adamc@1221:                                      Delete = []}
adamc@1217: 
adamc@1217: fun curVar (t : t) = #Var t
adamc@1217: fun nextVar (t : t) = ({Var = #Var t + 1,
adamc@1217:                         Ambient = #Ambient t,
adamc@1217:                         Path = #Path t,
adamc@1220:                         Sent = #Sent t,
adamc@1221:                         Insert = #Insert t,
adamc@1221:                         Delete = #Delete t}, #Var t)
adamc@1217: 
adamc@1217: fun ambient (t : t) = #Ambient t
adamc@1217: fun setAmbient (t : t, p) = {Var = #Var t,
adamc@1217:                              Ambient = p,
adamc@1217:                              Path = #Path t,
adamc@1220:                              Sent = #Sent t,
adamc@1221:                              Insert = #Insert t,
adamc@1221:                              Delete = #Delete t}
adamc@1217: 
adamc@1218: fun paths (t : t) = #Path t
adamc@1217: fun addPath (t : t, c) = {Var = #Var t,
adamc@1217:                           Ambient = #Ambient t,
adamc@1217:                           Path = c :: #Path t,
adamc@1220:                           Sent = #Sent t,
adamc@1221:                           Insert = #Insert t,
adamc@1221:                           Delete = #Delete t}
adamc@1218: fun addPaths (t : t, cs) = {Var = #Var t,
adamc@1218:                             Ambient = #Ambient t,
adamc@1218:                             Path = cs @ #Path t,
adamc@1220:                             Sent = #Sent t,
adamc@1221:                             Insert = #Insert t,
adamc@1221:                             Delete = #Delete t}
adamc@1218: fun clearPaths (t : t) = {Var = #Var t,
adamc@1218:                           Ambient = #Ambient t,
adamc@1218:                           Path = [],
adamc@1220:                           Sent = #Sent t,
adamc@1221:                           Insert = #Insert t,
adamc@1221:                           Delete = #Delete t}
adamc@1218: fun setPaths (t : t, cs) = {Var = #Var t,
adamc@1218:                             Ambient = #Ambient t,
adamc@1218:                             Path = cs,
adamc@1220:                             Sent = #Sent t,
adamc@1221:                             Insert = #Insert t,
adamc@1221:                             Delete = #Delete t}
adamc@1217: 
adamc@1217: fun sent (t : t) = #Sent t
adamc@1217: fun addSent (t : t, c) = {Var = #Var t,
adamc@1217:                           Ambient = #Ambient t,
adamc@1217:                           Path = #Path t,
adamc@1220:                           Sent = c :: #Sent t,
adamc@1221:                           Insert = #Insert t,
adamc@1221:                           Delete = #Delete t}
adamc@1217: fun setSent (t : t, cs) = {Var = #Var t,
adamc@1217:                            Ambient = #Ambient t,
adamc@1217:                            Path = #Path t,
adamc@1220:                            Sent = cs,
adamc@1221:                            Insert = #Insert t,
adamc@1221:                            Delete = #Delete t}
adamc@1220: 
adamc@1220: fun inserted (t : t) = #Insert t
adamc@1220: fun addInsert (t : t, c) = {Var = #Var t,
adamc@1220:                             Ambient = #Ambient t,
adamc@1220:                             Path = #Path t,
adamc@1220:                             Sent = #Sent t,
adamc@1221:                             Insert = c :: #Insert t,
adamc@1221:                             Delete = #Delete t}
adamc@1221: 
adamc@1221: fun deleted (t : t) = #Delete t
adamc@1221: fun addDelete (t : t, c) = {Var = #Var t,
adamc@1221:                             Ambient = #Ambient t,
adamc@1221:                             Path = #Path t,
adamc@1221:                             Sent = #Sent t,
adamc@1221:                             Insert = #Insert t,
adamc@1221:                             Delete = c :: #Delete t}
adamc@1217: 
adamc@1217: end
adamc@1217: 
adamc@1217: fun evalExp env (e as (_, loc), st) =
adamc@1200:     let
adamc@1200:         fun default () =
adamc@1217:             let
adamc@1217:                 val (st, nv) = St.nextVar st
adamc@1217:             in
adamc@1217:                 (Var nv, st)
adamc@1217:             end
adamc@1200: 
adamc@1217:         fun addSent (p, e, st) =
adamc@1218:             let
adamc@1218:                 val st = if isKnown e then
adamc@1218:                              st
adamc@1218:                          else
adamc@1218:                              St.addSent (st, ((loc, e, p), Data))
adamc@1218: 
adamc@1218:                 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
adamc@1218:             in
adamc@1218:                 St.clearPaths st
adamc@1218:             end
adamc@1200:     in
adamc@1200:         case #1 e of
adamc@1200:             EPrim p => (Const p, st)
adamc@1200:           | ERel n => (List.nth (env, n), st)
adamc@1200:           | ENamed _ => default ()
adamc@1215:           | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
adamc@1200:           | ECon (_, pc, SOME e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1215:                 (Func (DtCon1 (patCon pc), [e]), st)
adamc@1200:             end
adamc@1215:           | ENone _ => (Func (DtCon0 "None", []), st)
adamc@1200:           | ESome (_, e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1215:                 (Func (DtCon1 "Some", [e]), st)
adamc@1200:             end
adamc@1200:           | EFfi _ => default ()
adamc@1213: 
adamc@1200:           | EFfiApp (m, s, es) =>
adamc@1200:             if m = "Basis" andalso SS.member (writers, s) then
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1217:                     (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
adamc@1200:                 end
adamc@1200:             else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200:                 default ()
adamc@1200:             else
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1215:                     (Func (Other (m ^ "." ^ s), es), st)
adamc@1200:                 end
adamc@1213: 
adamc@1213:           | EApp (e1, e2) =>
adamc@1213:             let
adamc@1213:                 val (e1, st) = evalExp env (e1, st)
adamc@1213:             in
adamc@1213:                 case e1 of
adamc@1213:                     Finish => (Finish, st)
adamc@1213:                   | _ => default ()
adamc@1213:             end
adamc@1213: 
adamc@1200:           | EAbs _ => default ()
adamc@1200:           | EUnop (s, e1) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1215:                 (Func (Other s, [e1]), st)
adamc@1200:             end
adamc@1200:           | EBinop (s, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1215:                 (Func (Other s, [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | ERecord xets =>
adamc@1200:             let
adamc@1200:                 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200:                                                       let
adamc@1200:                                                           val (e, st) = evalExp env (e, st)
adamc@1200:                                                       in
adamc@1200:                                                           ((x, e), st)
adamc@1200:                                                       end) st xets
adamc@1200:             in
adamc@1200:                 (Recd xes, st)
adamc@1200:             end
adamc@1200:           | EField (e, s) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Proj (e, s), st)
adamc@1200:             end
adamc@1218:           | ECase (e, pes, {result = res, ...}) =>
adamc@1211:             let
adamc@1211:                 val (e, st) = evalExp env (e, st)
adamc@1217:                 val (st, r) = St.nextVar st
adamc@1217:                 val orig = St.ambient st
adamc@1218:                 val origPaths = St.paths st
adamc@1211: 
adamc@1218:                 val st = St.addPath (st, ((loc, e, orig), Case))
adamc@1218: 
adamc@1218:                 val (st, paths) =
adamc@1218:                     foldl (fn ((pt, pe), (st, paths)) =>
adamc@1218:                               let
adamc@1218:                                   val (env, pp) = evalPat env e pt
adamc@1218:                                   val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
adamc@1218:                                                   
adamc@1218:                                   val this = And (removeRedundant orig (St.ambient st'),
adamc@1218:                                                   Reln (Eq, [Var r, pe]))
adamc@1218:                               in
adamc@1218:                                   (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths),
adamc@1218:                                    St.paths st' @ paths)
adamc@1218:                               end) (St.setAmbient (st, False), []) pes
adamc@1218: 
adamc@1218:                 val st = case #1 res of
adamc@1218:                              TRecord [] => St.setPaths (st, origPaths)
adamc@1218:                            | _ => St.setPaths (st, paths)
adamc@1211:             in
adamc@1217:                 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
adamc@1211:             end
adamc@1200:           | EStrcat (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1215:                 (Func (Other "cat", [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | EError _ => (Finish, st)
adamc@1200:           | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200:             let
adamc@1200:                 val (b, st) = evalExp env (b, st)
adamc@1200:                 val (m, st) = evalExp env (m, st)
adamc@1200:             in
adamc@1217:                 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
adamc@1200:             end
adamc@1200:           | ERedirect (e, _) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1217:                 (Finish, addSent (St.ambient st, e, st))
adamc@1200:             end
adamc@1200:           | EWrite e =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1217:                 (Recd [], addSent (St.ambient st, e, st))
adamc@1200:             end
adamc@1200:           | ESeq (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp env (e2, st)
adamc@1200:             end
adamc@1200:           | ELet (_, _, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp (e1 :: env) (e2, st)
adamc@1200:             end
adamc@1200:           | EClosure (n, es) =>
adamc@1200:             let
adamc@1200:                 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:             in
adamc@1215:                 (Func (Other ("Cl" ^ Int.toString n), es), st)
adamc@1200:             end
adamc@1200: 
adamc@1200:           | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (q, st)
adamc@1200:                 val (i, st) = evalExp env (i, st)
adamc@1200: 
adamc@1217:                 val (st', r) = St.nextVar st
adamc@1217:                 val (st', acc) = St.nextVar st'
adamc@1200: 
adamc@1200:                 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200: 
adamc@1218:                 val (st', qp, qwp, used, _) =
adamc@1214:                     queryProp env
adamc@1217:                               st' (fn st' =>
adamc@1217:                                       let
adamc@1217:                                           val (st', rv) = St.nextVar st'
adamc@1217:                                       in
adamc@1217:                                           (st', Var rv)
adamc@1217:                                       end)
adamc@1214:                               (AllCols (Var r)) q
adamc@1200: 
adamc@1217:                 val p' = And (qp, St.ambient st')
adamc@1200: 
adamc@1217:                 val (st, res) = if varInP acc (St.ambient st') then
adamc@1217:                                     let
adamc@1217:                                         val (st, r) = St.nextVar st
adamc@1217:                                     in
adamc@1217:                                         (st, Var r)
adamc@1217:                                     end
adamc@1217:                                 else
adamc@1217:                                     let
adamc@1217:                                         val (st, out) = St.nextVar st'
adamc@1217:                                                   
adamc@1217:                                         val p = Or (Reln (Eq, [Var out, i]),
adamc@1217:                                                     And (Reln (Eq, [Var out, b]),
adamc@1217:                                                          p'))
adamc@1217:                                     in
adamc@1217:                                         (St.setAmbient (st, p), Var out)
adamc@1217:                                     end
adamc@1210: 
adamc@1218:                 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
adamc@1212: 
adamc@1217:                 val p' = And (p', qwp)
adamc@1218:                 val paths = map (fn e => ((loc, e, p'), Where)) used
adamc@1200:             in
adamc@1218:                 (res, St.addPaths (St.setSent (st, sent), paths))
adamc@1200:             end
adamc@1220:           | EDml e =>
adamc@1220:             (case parse dml e of
adamc@1220:                  NONE => (print ("Warning: Information flow checker can't parse DML command at "
adamc@1220:                                  ^ ErrorMsg.spanToString loc ^ "\n");
adamc@1220:                           default ())
adamc@1220:                | SOME d =>
adamc@1220:                  case d of
adamc@1220:                      Insert (tab, es) =>
adamc@1220:                      let
adamc@1220:                          val (st, new) = St.nextVar st
adamc@1220: 
adamc@1220:                          fun rv st =
adamc@1220:                              let
adamc@1220:                                  val (st, n) = St.nextVar st
adamc@1220:                              in
adamc@1220:                                  (st, Var n)
adamc@1220:                              end
adamc@1220: 
adamc@1220:                          val expIn = expIn rv env (fn "New" => Var new
adamc@1221:                                                     | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1220: 
adamc@1220:                          val (es, st) = ListUtil.foldlMap
adamc@1220:                                             (fn ((x, e), st) =>
adamc@1220:                                                 let
adamc@1220:                                                     val (e, st) = case expIn (e, st) of
adamc@1220:                                                                       (inl e, st) => (e, st)
adamc@1220:                                                                     | (inr _, _) => raise Fail
adamc@1220:                                                                                               ("Iflow.evalExp: Selecting "
adamc@1220:                                                                                                ^ "boolean expression")
adamc@1220:                                                 in
adamc@1220:                                                     ((x, e), st)
adamc@1220:                                                 end)
adamc@1220:                                             st es
adamc@1220:                      in
adamc@1220:                          (Recd [], St.addInsert (st, (loc, And (St.ambient st,
adamc@1220:                                                                 Reln (Sql "$New", [Recd es])))))
adamc@1221:                      end
adamc@1221:                    | Delete (tab, e) =>
adamc@1221:                      let
adamc@1221:                          val (st, old) = St.nextVar st
adamc@1221: 
adamc@1221:                          fun rv st =
adamc@1221:                              let
adamc@1221:                                  val (st, n) = St.nextVar st
adamc@1221:                              in
adamc@1221:                                  (st, Var n)
adamc@1221:                              end
adamc@1221: 
adamc@1221:                          val expIn = expIn rv env (fn "T" => Var old
adamc@1221:                                                     | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221: 
adamc@1221:                          val (p, st) = case expIn (e, st) of
adamc@1221:                                            (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean" 
adamc@1221:                                          | (inr p, st) => (p, st)
adamc@1221: 
adamc@1221:                          val p = And (p,
adamc@1221:                                       And (Reln (Sql "$Old", [Var old]),
adamc@1221:                                            Reln (Sql tab, [Var old])))
adamc@1221:                      in
adamc@1221:                          (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
adamc@1220:                      end)
adamc@1220:                      
adamc@1200:           | ENextval _ => default ()
adamc@1200:           | ESetval _ => default ()
adamc@1200: 
adamc@1213:           | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1217:             let
adamc@1217:                 val (st, nv) = St.nextVar st
adamc@1217:             in
adamc@1217:                 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
adamc@1217:             end
adamc@1213: 
adamc@1200:           | EUnurlify _ => default ()
adamc@1200:           | EJavaScript _ => default ()
adamc@1200:           | ESignalReturn _ => default ()
adamc@1200:           | ESignalBind _ => default ()
adamc@1200:           | ESignalSource _ => default ()
adamc@1200:           | EServerCall _ => default ()
adamc@1200:           | ERecv _ => default ()
adamc@1200:           | ESleep _ => default ()
adamc@1200:           | ESpawn _ => default ()
adamc@1200:     end
adamc@1200: 
adamc@1200: fun check file =
adamc@1200:     let
adamc@1213:         val file = MonoReduce.reduce file
adamc@1213:         val file = MonoOpt.optimize file
adamc@1213:         val file = Fuse.fuse file
adamc@1213:         val file = MonoOpt.optimize file
adamc@1216:         val file = MonoShake.shake file
adamc@1213:         (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213: 
adamc@1207:         val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207:                               case d of
adamc@1207:                                   DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207:                                 | _ => exptd) IS.empty file
adamc@1207: 
adamc@1221:         fun decl ((d, _), (vals, inserts, deletes, client, insert, delete)) =
adamc@1200:             case d of
adamc@1207:                 DVal (_, n, _, e, _) =>
adamc@1200:                 let
adamc@1207:                     val isExptd = IS.member (exptd, n)
adamc@1207: 
adamc@1207:                     fun deAbs (e, env, nv, p) =
adamc@1200:                         case #1 e of
adamc@1207:                             EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207:                                                         if isExptd then
adamc@1207:                                                             And (p, Reln (Known, [Var nv]))
adamc@1207:                                                         else
adamc@1207:                                                             p)
adamc@1207:                           | _ => (e, env, nv, p)
adamc@1200: 
adamc@1207:                     val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200: 
adamc@1217:                     val (_, st) = evalExp env (e, St.create {Var = nv,
adamc@1217:                                                              Ambient = p})
adamc@1200:                 in
adamc@1221:                     (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, client, insert, delete)
adamc@1200:                 end
adamc@1202: 
adamc@1220:               | DPolicy pol =>
adamc@1218:                 let
adamc@1220:                     fun rv rvN = (rvN + 1, Lvar rvN)
adamc@1218:                 in
adamc@1220:                     case pol of
adamc@1220:                         PolClient e =>
adamc@1220:                         let
adamc@1220:                             val (_, p, _, _, outs) = queryProp [] 0 rv SomeCol e
adamc@1220:                         in
adamc@1221:                             (vals, inserts, deletes, (p, outs) :: client, insert, delete)
adamc@1220:                         end
adamc@1220:                       | PolInsert e =>
adamc@1220:                         let
adamc@1220:                             val p = insertProp 0 rv e
adamc@1220:                         in
adamc@1221:                             (vals, inserts, deletes, client, p :: insert, delete)
adamc@1221:                         end
adamc@1221:                       | PolDelete e =>
adamc@1221:                         let
adamc@1221:                             val p = deleteProp 0 rv e
adamc@1221:                         in
adamc@1221:                             (vals, inserts, deletes, client, insert, p :: delete)
adamc@1220:                         end
adamc@1218:                 end
adamc@1214:                                         
adamc@1221:               | _ => (vals, inserts, deletes, client, insert, delete)
adamc@1202: 
adamc@1203:         val () = reset ()
adamc@1202: 
adamc@1221:         val (vals, inserts, deletes, client, insert, delete) = foldl decl ([], [], [], [], [], []) file
adamc@1220: 
adamc@1220:         val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
adamc@1220:         val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
adamc@1221: 
adamc@1221:         fun doDml (cmds, pols) =
adamc@1221:             app (fn (loc, p) =>
adamc@1221:                     if decompH p
adamc@1221:                                (fn hyps =>
adamc@1221:                                    List.exists (fn p' =>
adamc@1221:                                                    decompG p'
adamc@1221:                                                            (fn goals => imply (hyps, goals, NONE)))
adamc@1221:                                                pols) then
adamc@1221:                         ()
adamc@1221:                     else
adamc@1221:                         (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1221:                          Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
adamc@1200:     in
adamc@1218:         app (fn ((loc, e, p), fl) =>
adamc@1207:                 let
adamc@1213:                     fun doOne e =
adamc@1213:                         let
adamc@1213:                             val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213:                         in
adamc@1220:                             if decompH p
adamc@1220:                                        (fn hyps =>
adamc@1220:                                            (fl <> Control Where
adamc@1220:                                             andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
adamc@1220:                                            orelse List.exists (fn (p', outs) =>
adamc@1220:                                                                   decompG p'
adamc@1220:                                                                           (fn goals => imply (hyps, goals, SOME outs)))
adamc@1220:                                                               client) then
adamc@1213:                                 ()
adamc@1213:                             else
adamc@1213:                                 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1216:                                  Print.preface ("The state satisifies this predicate:", p_prop p))
adamc@1213:                         end
adamc@1213: 
adamc@1213:                     fun doAll e =
adamc@1213:                         case e of
adamc@1213:                             Const _ => ()
adamc@1213:                           | Var _ => doOne e
adamc@1213:                           | Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1216:                           | Func (UnCon _, [_]) => doOne e
adamc@1215:                           | Func (_, es) => app doAll es
adamc@1213:                           | Recd xes => app (doAll o #2) xes
adamc@1213:                           | Proj _ => doOne e
adamc@1213:                           | Finish => ()
adamc@1207:                 in
adamc@1213:                     doAll e
adamc@1220:                 end) vals;
adamc@1220: 
adamc@1221:         doDml (inserts, insert);
adamc@1221:         doDml (deletes, delete)
adamc@1200:     end
adamc@1200: 
adamc@1213: val check = fn file =>
adamc@1213:                let
adamc@1213:                    val oldInline = Settings.getMonoInline ()
adamc@1213:                in
adamc@1213:                    (Settings.setMonoInline (case Int.maxInt of
adamc@1213:                                                 NONE => 1000000
adamc@1213:                                               | SOME n => n);
adamc@1213:                     check file;
adamc@1213:                     Settings.setMonoInline oldInline)
adamc@1213:                    handle ex => (Settings.setMonoInline oldInline;
adamc@1213:                                  raise ex)
adamc@1213:                end
adamc@1213: 
adamc@1200: end
adamc@1213: