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: 
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@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@1236:       | Lvar n => string ("X" ^ Int.toString n)
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: 
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@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@1236: fun simplify unif =
adamc@1236:     let
adamc@1236:         fun simplify e =
adamc@1236:             case e of
adamc@1236:                 Const _ => e
adamc@1236:               | Var _ => e
adamc@1236:               | Lvar n =>
adamc@1236:                 (case IM.find (unif, n) of
adamc@1236:                      NONE => e
adamc@1236:                    | SOME e => simplify e)
adamc@1236:               | Func (f, es) => Func (f, map simplify es)
adamc@1236:               | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
adamc@1236:               | Proj (e, s) => Proj (simplify e, s)
adamc@1236:     in
adamc@1236:         simplify
adamc@1236:     end
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@1208: val debug = ref 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@1236:     val clear : database -> unit
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@1238:     val builtFrom : database * {UseKnown : bool, Base : exp list, Derived : exp} -> bool
adamc@1226: 
adamc@1226:     val p_repOf : database -> exp Print.printer
adamc@1208: end = struct
adamc@1208: 
adamc@1244: local
adamc@1244:     val count = ref 0
adamc@1244: in
adamc@1244: fun nodeId () =
adamc@1244:     let
adamc@1244:         val n = !count
adamc@1244:     in
adamc@1244:         count := n + 1;
adamc@1244:         n
adamc@1244:     end
adamc@1244: end
adamc@1244: 
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@1244: datatype node = Node of {Id : int,
adamc@1244:                          Rep : node ref option ref,
adamc@1215:                          Cons : node ref SM.map ref,
adamc@1215:                          Variety : variety,
adamc@1245:                          Known : bool ref,
adamc@1245:                          Ge : Int64.int option 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:        | Nothing
adamc@1208: 
adamc@1215: type representative = node ref
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@1229:                  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@1236: fun clear (t : database) = (#Vars t := IM.empty;
adamc@1236:                             #Consts t := CM.empty;
adamc@1236:                             #Con0s t := SM.empty;
adamc@1236:                             #Records t := [];
adamc@1236:                             #Funcs t := [])
adamc@1236: 
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@1244:         box [string (Int.toString (#Id (unNode n)) ^ ":"),
adamc@1244:              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@1245:                                               box []],
adamc@1245:              if !(#Known (unNode n)) then
adamc@1245:                  string " (known)"
adamc@1245:              else
adamc@1245:                  box [],
adamc@1245:              case !(#Ge (unNode n)) of
adamc@1245:                  NONE => box []
adamc@1245:                | SOME n => string (" (>= " ^ Int64.toString n ^ ")")]
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@1245:                                                p_rep n]) (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@1244:                                     val r = ref (Node {Id = nodeId (),
adamc@1244:                                                        Rep = ref NONE,
adamc@1215:                                                        Cons = ref SM.empty,
adamc@1215:                                                        Variety = Prim p,
adamc@1245:                                                        Known = ref true,
adamc@1245:                                                        Ge = ref (case p of
adamc@1245:                                                                      Prim.Int n => SOME n
adamc@1245:                                                                    | _ => NONE)})
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@1244:                                   val r = ref (Node {Id = nodeId (),
adamc@1244:                                                      Rep = ref NONE,
adamc@1215:                                                      Cons = ref SM.empty,
adamc@1215:                                                      Variety = Nothing,
adamc@1245:                                                      Known = ref false,
adamc@1245:                                                      Ge = ref NONE})
adamc@1215:                               in
adamc@1215:                                   #Vars db := IM.insert (!(#Vars db), n, r);
adamc@1215:                                   r
adamc@1215:                               end)
adamc@1236:               | Lvar _ => raise Undetermined
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@1244:                                                 val r = ref (Node {Id = nodeId (),
adamc@1244:                                                                    Rep = ref NONE,
adamc@1215:                                                                    Cons = ref SM.empty,
adamc@1215:                                                                    Variety = Dt0 f,
adamc@1245:                                                                    Known = ref true,
adamc@1245:                                                                    Ge = ref NONE})
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@1244:                             val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                 Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1215:                                                 Variety = Dt1 (f, r),
adamc@1245:                                                 Known = ref (!(#Known (unNode r))),
adamc@1245:                                                 Ge = ref NONE})
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@1244:                             val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                 Rep = ref NONE,
adamc@1215:                                                 Cons = cons,
adamc@1215:                                                 Variety = Nothing,
adamc@1245:                                                 Known = ref (!(#Known (unNode r))),
adamc@1245:                                                 Ge = ref NONE})
adamc@1215: 
adamc@1244:                             val r'' = ref (Node {Id = nodeId (),
adamc@1244:                                                  Rep = ref NONE,
adamc@1215:                                                  Cons = #Cons (unNode r),
adamc@1215:                                                  Variety = Dt1 (f, r'),
adamc@1245:                                                  Known = #Known (unNode r),
adamc@1245:                                                  Ge = ref NONE})
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:                       | _ => 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@1244:                             val r = ref (Node {Id = nodeId (),
adamc@1244:                                                Rep = ref NONE,
adamc@1215:                                                Cons = ref SM.empty,
adamc@1215:                                                Variety = Nothing,
adamc@1245:                                                Known = ref false,
adamc@1245:                                                Ge = ref NONE})
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@1244:                             val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                 Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1221:                                                 Variety = Recrd (ref xes, true),
adamc@1245:                                                 Known = ref false,
adamc@1245:                                                 Ge = ref NONE})
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@1244:                                   val r = ref (Node {Id = nodeId (),
adamc@1244:                                                      Rep = ref NONE,
adamc@1215:                                                      Cons = ref SM.empty,
adamc@1215:                                                      Variety = Nothing,
adamc@1245:                                                      Known = ref (!(#Known (unNode r))),
adamc@1245:                                                      Ge = ref NONE})
adamc@1215:                               in
adamc@1215:                                  xes := SM.insert (!xes, f, r);
adamc@1215:                                  r
adamc@1215:                               end)
adamc@1215:                       | Nothing =>
adamc@1215:                         let
adamc@1244:                             val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                 Rep = ref NONE,
adamc@1215:                                                 Cons = ref SM.empty,
adamc@1215:                                                 Variety = Nothing,
adamc@1245:                                                 Known = ref (!(#Known (unNode r))),
adamc@1245:                                                 Ge = ref NONE})
adamc@1215:                                      
adamc@1244:                             val r'' = ref (Node {Id = nodeId (),
adamc@1244:                                                  Rep = ref NONE,
adamc@1215:                                                  Cons = #Cons (unNode r),
adamc@1221:                                                  Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
adamc@1245:                                                  Known = #Known (unNode r),
adamc@1245:                                                  Ge = ref NONE})
adamc@1215:                         in
adamc@1215:                             #Rep (unNode r) := SOME r'';
adamc@1215:                             r'
adamc@1215:                         end
adamc@1215:                       | _ => raise Contradiction                             
adamc@1215:                 end
adamc@1208:     in
adamc@1215:         rep e
adamc@1208:     end
adamc@1208: 
adamc@1226: fun p_repOf db e = p_rep (representative (db, e))
adamc@1226: 
adamc@1215: fun assert (db, a) =
adamc@1243:     let
adamc@1243:         fun markEq (r1, r2) =
adamc@1215:             let
adamc@1243:                 val r1 = repOf r1
adamc@1243:                 val r2 = repOf r2
adamc@1215:             in
adamc@1243:                 if r1 = r2 then
adamc@1243:                     ()
adamc@1243:                 else case (#Variety (unNode r1), #Variety (unNode r2)) of
adamc@1243:                          (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
adamc@1243:                                                    ()
adamc@1243:                                                else
adamc@1243:                                                    raise Contradiction
adamc@1243:                        | (Dt0 f1, Dt0 f2) => if f1 = f2 then
adamc@1243:                                                  ()
adamc@1243:                                              else
adamc@1243:                                                  raise Contradiction
adamc@1243:                        | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
adamc@1243:                                                              markEq (r1, r2)
adamc@1243:                                                          else
adamc@1243:                                                              raise Contradiction
adamc@1243:                        | (Recrd (xes1, _), Recrd (xes2, _)) =>
adamc@1243:                          let
adamc@1243:                              fun unif (xes1, xes2) =
adamc@1243:                                  SM.appi (fn (x, r1) =>
adamc@1243:                                              case SM.find (!xes2, x) of
adamc@1243:                                                  NONE => xes2 := SM.insert (!xes2, x, r1)
adamc@1243:                                                | SOME r2 => markEq (r1, r2)) (!xes1)
adamc@1243:                          in
adamc@1243:                              unif (xes1, xes2);
adamc@1243:                              unif (xes2, xes1)
adamc@1243:                          end
adamc@1243:                        | (Nothing, _) => mergeNodes (r1, r2)
adamc@1243:                        | (_, Nothing) => mergeNodes (r2, r1)
adamc@1243:                        | _ => raise Contradiction
adamc@1215:             end
adamc@1243: 
adamc@1243:         and mergeNodes (r1, r2) =
adamc@1243:             (#Rep (unNode r1) := SOME r2;
adamc@1243:              if !(#Known (unNode r1)) then
adamc@1243:                  markKnown r2
adamc@1243:              else
adamc@1243:                  ();
adamc@1243:              if !(#Known (unNode r2)) then
adamc@1243:                  markKnown r1
adamc@1243:              else
adamc@1243:                  ();
adamc@1243:              #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
adamc@1243: 
adamc@1245:              case !(#Ge (unNode r1)) of
adamc@1245:                  NONE => ()
adamc@1245:                | SOME n1 =>
adamc@1245:                  case !(#Ge (unNode r2)) of
adamc@1245:                      NONE => #Ge (unNode r2) := SOME n1
adamc@1245:                    | SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));
adamc@1245: 
adamc@1243:              compactFuncs ())
adamc@1243: 
adamc@1243:         and compactFuncs () =
adamc@1215:             let
adamc@1243:                 fun loop funcs =
adamc@1243:                     case funcs of
adamc@1243:                         [] => []
adamc@1243:                       | (fr as ((f, rs), r)) :: rest =>
adamc@1243:                         let
adamc@1243:                             val rest = List.filter (fn ((f' : string, rs'), r') =>
adamc@1243:                                                        if f' = f
adamc@1243:                                                           andalso ListPair.allEq (fn (r1, r2) =>
adamc@1243:                                                                                      repOf r1 = repOf r2)
adamc@1243:                                                                                  (rs, rs') then
adamc@1243:                                                            (markEq (r, r');
adamc@1243:                                                             false)
adamc@1243:                                                        else
adamc@1243:                                                            true) rest
adamc@1243:                         in
adamc@1243:                             fr :: loop rest
adamc@1243:                         end
adamc@1215:             in
adamc@1243:                 #Funcs db := loop (!(#Funcs db))
adamc@1243:             end
adamc@1243:     in
adamc@1243:         case a of
adamc@1243:             ACond _ => ()
adamc@1243:           | AReln x =>
adamc@1243:             case x of
adamc@1243:                 (Known, [e]) =>
adamc@1243:                 ((*Print.prefaces "Before" [("e", p_exp e),
adamc@1243:                                             ("db", p_database db)];*)
adamc@1243:                  markKnown (representative (db, e))(*;
adamc@1243:                                                         Print.prefaces "After" [("e", p_exp e),
adamc@1243:                                                                                 ("db", p_database db)]*))
adamc@1243:               | (PCon0 f, [e]) =>
adamc@1243:                 let
adamc@1243:                     val r = representative (db, e)
adamc@1243:                 in
adamc@1243:                     case #Variety (unNode r) of
adamc@1243:                         Dt0 f' => if f = f' then
adamc@1243:                                       ()
adamc@1243:                                   else
adamc@1243:                                       raise Contradiction
adamc@1243:                       | Nothing =>
adamc@1243:                         (case SM.find (!(#Con0s db), f) of
adamc@1243:                              SOME r' => markEq (r, r')
adamc@1243:                            | NONE =>
adamc@1243:                              let
adamc@1244:                                  val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                      Rep = ref NONE,
adamc@1243:                                                      Cons = ref SM.empty,
adamc@1243:                                                      Variety = Dt0 f,
adamc@1245:                                                      Known = ref false,
adamc@1245:                                                      Ge = ref NONE})
adamc@1243:                              in
adamc@1243:                                  #Rep (unNode r) := SOME r';
adamc@1243:                                  #Con0s db := SM.insert (!(#Con0s db), f, r')
adamc@1243:                              end)
adamc@1243:                       | _ => raise Contradiction
adamc@1243:                 end
adamc@1243:               | (PCon1 f, [e]) =>
adamc@1243:                 let
adamc@1243:                     val r = representative (db, e)
adamc@1243:                 in
adamc@1243:                     case #Variety (unNode r) of
adamc@1243:                         Dt1 (f', e') => if f = f' then
adamc@1243:                                             ()
adamc@1243:                                         else
adamc@1243:                                             raise Contradiction
adamc@1243:                       | Nothing =>
adamc@1243:                         let
adamc@1244:                             val r'' = ref (Node {Id = nodeId (),
adamc@1244:                                                  Rep = ref NONE,
adamc@1243:                                                  Cons = ref SM.empty,
adamc@1243:                                                  Variety = Nothing,
adamc@1245:                                                  Known = ref (!(#Known (unNode r))),
adamc@1245:                                                  Ge = ref NONE})
adamc@1214: 
adamc@1244:                             val r' = ref (Node {Id = nodeId (),
adamc@1244:                                                 Rep = ref NONE,
adamc@1243:                                                 Cons = ref SM.empty,
adamc@1243:                                                 Variety = Dt1 (f, r''),
adamc@1245:                                                 Known = #Known (unNode r),
adamc@1245:                                                 Ge = ref NONE})
adamc@1243:                         in
adamc@1243:                             #Rep (unNode r) := SOME r'
adamc@1243:                         end
adamc@1243:                       | _ => raise Contradiction
adamc@1243:                 end
adamc@1243:               | (Eq, [e1, e2]) =>
adamc@1215:                 markEq (representative (db, e1), representative (db, e2))
adamc@1245:               | (Ge, [e1, e2]) =>
adamc@1245:                 let
adamc@1245:                     val r1 = representative (db, e1)
adamc@1245:                     val r2 = representative (db, e2)
adamc@1245:                 in
adamc@1245:                     case !(#Ge (unNode (repOf r2))) of
adamc@1245:                         NONE => ()
adamc@1245:                       | SOME n2 =>
adamc@1245:                         case !(#Ge (unNode (repOf r1))) of
adamc@1245:                             NONE => #Ge (unNode (repOf r1)) := SOME n2
adamc@1245:                           | SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
adamc@1245:                 end
adamc@1243:               | _ => ()
adamc@1243:     end
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@1245:           | (Ge, [e1, e2]) =>
adamc@1245:             let
adamc@1245:                 val r1 = representative (db, e1)
adamc@1245:                 val r2 = representative (db, e2)
adamc@1245:             in
adamc@1245:                 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
adamc@1245:                     (SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
adamc@1245:                   | _ => false
adamc@1245:             end
adamc@1215:           | _ => false
adamc@1212: 
adamc@1238: fun builtFrom (db, {UseKnown = uk, 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@1238:                 (uk andalso !(#Known (unNode d)))
adamc@1238:                 orelse 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:                          | Nothing => false
adamc@1218:             end
adamc@1238: 
adamc@1238:         fun decomp e =
adamc@1238:             case e of
adamc@1238:                 Func (Other _, es) => List.all decomp es
adamc@1238:               | _ => loop (representative (db, e))
adamc@1218:     in
adamc@1238:         decomp d
adamc@1218:     end
adamc@1218: 
adamc@1208: end
adamc@1208: 
adamc@1226: val tabs = ref (SM.empty : (string list * string list list) SM.map)
adamc@1226: 
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@1227:          (print (name ^ ": ");
adamc@1227:           app (fn String s => print s
adamc@1227:                 | _ => print "???") chs;
adamc@1227:           print "\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@1243:        | SqTrue
adamc@1243:        | SqFalse
adamc@1206:        | Field of string * string
adamc@1239:        | Computed of 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@1245:        | Unmodeled
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@1243:       | Exp (ECase (e, [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _),
adamc@1243:                          (EPrim (Prim.String "TRUE"), _)),
adamc@1243:                         ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _),
adamc@1243:                          (EPrim (Prim.String "FALSE"), _))], _), _) :: chs =>
adamc@1243:         SOME (e, chs)
adamc@1243:                           
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@1245: val unmodeled = altL [const "COUNT(*)",
adamc@1245:                       const "CURRENT_TIMESTAMP"]
adamc@1245: 
adamc@1204: fun sqexp chs =
adamc@1206:     log "sqexp"
adamc@1207:     (altL [wrap prim SqConst,
adamc@1243:            wrap (const "TRUE") (fn () => SqTrue),
adamc@1243:            wrap (const "FALSE") (fn () => SqFalse),
adamc@1211:            wrap field Field,
adamc@1239:            wrap uw_ident Computed,
adamc@1207:            wrap known SqKnown,
adamc@1211:            wrap func SqFunc,
adamc@1245:            wrap unmodeled (fn () => Unmodeled),
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@1239: val sitem = alt (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1239:                       (fn (e, ((), s)) => SqExp (e, s)))
adamc@1239:                 (wrap field SqField)
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@1227: type query1 = {Select : sitem list,
adamc@1227:               From : (string * string) list,
adamc@1227:               Where : sqexp option}
adamc@1227: 
adamc@1227: val query1 = log "query1"
adamc@1207:                 (wrap (follow (follow select from) (opt wher))
adamc@1207:                       (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201: 
adamc@1227: datatype query =
adamc@1227:          Query1 of query1
adamc@1227:        | Union of query * query
adamc@1227: 
adamc@1239: val orderby = log "orderby"
adamc@1239:               (wrap (follow (ws (const "ORDER BY "))
adamc@1243:                             (follow (list sqexp)
adamc@1243:                                     (opt (ws (const "DESC")))))
adamc@1243:                     ignore)
adamc@1239: 
adamc@1227: fun query chs = log "query"
adamc@1239:                 (wrap
adamc@1239:                      (follow
adamc@1239:                           (alt (wrap (follow (const "((")
adamc@1239:                                              (follow query
adamc@1239:                                                      (follow (const ") UNION (")
adamc@1239:                                                              (follow query (const "))")))))
adamc@1239:                                      (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
adamc@1239:                                (wrap query1 Query1))
adamc@1239:                           (opt orderby))
adamc@1239:                      #1)
adamc@1227:                 chs
adamc@1227: 
adamc@1220: datatype dml =
adamc@1220:          Insert of string * (string * sqexp) list
adamc@1221:        | Delete of string * sqexp
adamc@1223:        | Update of string * (string * sqexp) list * 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@1223: val setting = log "setting"
adamc@1223:               (wrap (follow uw_ident (follow (const " = ") sqexp))
adamc@1223:                (fn (f, ((), e)) => (f, e)))
adamc@1223: 
adamc@1223: val update = log "update"
adamc@1223:                  (wrap (follow (const "UPDATE ")
adamc@1223:                                (follow uw_ident
adamc@1223:                                        (follow (const " AS T_T SET ")
adamc@1223:                                                (follow (list setting)
adamc@1223:                                                        (follow (ws (const "WHERE "))
adamc@1223:                                                                sqexp)))))
adamc@1223:                        (fn ((), (tab, ((), (fs, ((), e))))) =>
adamc@1223:                            (tab, fs, e)))
adamc@1223: 
adamc@1220: val dml = log "dml"
adamc@1221:               (altL [wrap insert Insert,
adamc@1223:                      wrap delete Delete,
adamc@1223:                      wrap update Update])
adamc@1220: 
adamc@1236: type check = exp * ErrorMsg.span
adamc@1236: 
adamc@1236: structure St :> sig
adamc@1236:     val reset : unit -> unit
adamc@1236: 
adamc@1236:     type stashed
adamc@1236:     val stash : unit -> stashed
adamc@1236:     val reinstate : stashed -> unit
adamc@1236: 
adamc@1236:     val nextVar : unit -> int
adamc@1236: 
adamc@1236:     val assert : atom list -> unit
adamc@1236: 
adamc@1236:     val addPath : check -> unit
adamc@1236: 
adamc@1236:     val allowSend : atom list * exp list -> unit
adamc@1238:     val send : bool -> check -> unit
adamc@1236: 
adamc@1236:     val allowInsert : atom list -> unit
adamc@1236:     val insert : ErrorMsg.span -> unit
adamc@1236: 
adamc@1236:     val allowDelete : atom list -> unit
adamc@1236:     val delete : ErrorMsg.span -> unit
adamc@1236: 
adamc@1236:     val allowUpdate : atom list -> unit
adamc@1236:     val update : ErrorMsg.span -> unit
adamc@1236: 
adamc@1236:     val havocReln : reln -> unit
adamc@1245:     val havocCookie : string -> unit
adamc@1238: 
adamc@1238:     val debug : unit -> unit
adamc@1236: end = struct
adamc@1236: 
adamc@1236: val hnames = ref 1
adamc@1236: 
adamc@1244: type hyps = int * atom list * bool ref
adamc@1236: 
adamc@1236: val db = Cc.database ()
adamc@1244: val path = ref ([] : ((int * atom list) * check) option ref list)
adamc@1244: val hyps = ref (0, [] : atom list, ref false)
adamc@1236: val nvar = ref 0
adamc@1236: 
adamc@1244: fun setHyps (n', hs) =
adamc@1236:     let
adamc@1244:         val (n, _, _) = !hyps
adamc@1236:     in
adamc@1236:         if n' = n then
adamc@1236:             ()
adamc@1236:         else
adamc@1244:             (hyps := (n', hs, ref false);
adamc@1236:              Cc.clear db;
adamc@1236:              app (fn a => Cc.assert (db, a)) hs)
adamc@1236:     end    
adamc@1236: 
adamc@1244: fun useKeys () =
adamc@1244:     let
adamc@1244:         val changed = ref false
adamc@1244: 
adamc@1244:         fun findKeys (hyps, acc) =
adamc@1244:             case hyps of
adamc@1244:                 [] => acc
adamc@1244:               | (a as AReln (Sql tab, [r1])) :: hyps =>
adamc@1244:                 (case SM.find (!tabs, tab) of
adamc@1244:                      NONE => findKeys (hyps, a :: acc)
adamc@1244:                    | SOME (_, []) => findKeys (hyps, a :: acc)
adamc@1244:                    | SOME (_, ks) =>
adamc@1244:                      let
adamc@1244:                          fun finder (hyps, acc) =
adamc@1244:                              case hyps of
adamc@1244:                                  [] => acc
adamc@1244:                                | (a as AReln (Sql tab', [r2])) :: hyps =>
adamc@1244:                                  if tab' = tab andalso
adamc@1244:                                     List.exists (List.all (fn f =>
adamc@1244:                                                               let
adamc@1244:                                                                   val r =
adamc@1244:                                                                       Cc.check (db,
adamc@1244:                                                                                 AReln (Eq, [Proj (r1, f),
adamc@1244:                                                                                             Proj (r2, f)]))
adamc@1244:                                                               in
adamc@1244:                                                                   (*Print.prefaces "Fs"
adamc@1244:                                                                                    [("tab",
adamc@1244:                                                                                      Print.PD.string tab),
adamc@1244:                                                                                     ("r1",
adamc@1244:                                                                                      p_exp (Proj (r1, f))),
adamc@1244:                                                                                     ("r2",
adamc@1244:                                                                                      p_exp (Proj (r2, f))),
adamc@1244:                                                                                     ("r",
adamc@1244:                                                                                      Print.PD.string
adamc@1244:                                                                                          (Bool.toString r))];*)
adamc@1244:                                                                   r
adamc@1244:                                                               end)) ks then
adamc@1244:                                      (changed := true;
adamc@1244:                                       Cc.assert (db, AReln (Eq, [r1, r2]));
adamc@1244:                                       finder (hyps, acc))
adamc@1244:                                  else
adamc@1244:                                      finder (hyps, a :: acc)
adamc@1244:                                | a :: hyps => finder (hyps, a :: acc)
adamc@1244: 
adamc@1244:                          val hyps = finder (hyps, [])
adamc@1244:                      in
adamc@1244:                          findKeys (hyps, acc)
adamc@1244:                      end)
adamc@1244:               | a :: hyps => findKeys (hyps, a :: acc)
adamc@1244: 
adamc@1244:         fun loop hs =
adamc@1244:             let
adamc@1244:                 val hs = findKeys (hs, [])
adamc@1244:             in
adamc@1244:                 if !changed then
adamc@1244:                     (changed := false;
adamc@1244:                      loop hs)
adamc@1244:                 else
adamc@1244:                     ()
adamc@1244:             end
adamc@1244: 
adamc@1244:         val (_, hs, _) = !hyps
adamc@1244:     in
adamc@1244:         (*print "findKeys\n";*)
adamc@1244:         loop hs
adamc@1244:     end
adamc@1244: 
adamc@1244: fun complete () =
adamc@1244:     let
adamc@1244:         val (_, _, bf) = !hyps
adamc@1244:     in
adamc@1244:         if !bf then
adamc@1244:             ()
adamc@1244:         else
adamc@1244:             (bf := true;
adamc@1244:              useKeys ())
adamc@1244:     end
adamc@1244: 
adamc@1244: type stashed = int * ((int * atom list) * check) option ref list * (int * atom list)
adamc@1244: fun stash () = (!nvar, !path, (#1 (!hyps), #2 (!hyps)))
adamc@1236: fun reinstate (nv, p, h) =
adamc@1236:     (nvar := nv;
adamc@1236:      path := p;
adamc@1236:      setHyps h)
adamc@1236: 
adamc@1236: fun nextVar () =
adamc@1236:     let
adamc@1236:         val n = !nvar
adamc@1236:     in
adamc@1236:         nvar := n + 1;
adamc@1236:         n
adamc@1236:     end
adamc@1236: 
adamc@1236: fun assert ats =
adamc@1236:     let
adamc@1236:         val n = !hnames
adamc@1244:         val (_, hs, _) = !hyps
adamc@1236:     in
adamc@1236:         hnames := n + 1;
adamc@1244:         hyps := (n, ats @ hs, ref false);
adamc@1236:         app (fn a => Cc.assert (db, a)) ats
adamc@1236:     end
adamc@1236: 
adamc@1244: fun addPath c = path := ref (SOME ((#1 (!hyps), #2 (!hyps)), c)) :: !path
adamc@1236: 
adamc@1236: val sendable = ref ([] : (atom list * exp list) list)
adamc@1236: 
adamc@1238: fun checkGoals goals k =
adamc@1238:     let
adamc@1238:         fun checkGoals goals unifs =
adamc@1238:             case goals of
adamc@1238:                 [] => k unifs
adamc@1238:               | AReln (Sql tab, [Lvar lv]) :: goals =>
adamc@1238:                 let
adamc@1238:                     val saved = stash ()
adamc@1244:                     val (_, hyps, _) = !hyps
adamc@1236: 
adamc@1238:                     fun tryAll unifs hyps =
adamc@1238:                         case hyps of
adamc@1238:                             [] => false
adamc@1238:                           | AReln (Sql tab', [e]) :: hyps =>
adamc@1238:                             (tab' = tab andalso
adamc@1238:                              checkGoals goals (IM.insert (unifs, lv, e)))
adamc@1238:                             orelse tryAll unifs hyps
adamc@1238:                           | _ :: hyps => tryAll unifs hyps
adamc@1238:                 in
adamc@1238:                     tryAll unifs hyps
adamc@1238:                 end
adamc@1243:               | (g as AReln (r, es)) :: goals =>
adamc@1244:                 (complete ();
adamc@1245:                  (if Cc.check (db, AReln (r, map (simplify unifs) es)) then
adamc@1245:                       true
adamc@1245:                   else
adamc@1245:                       ((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
adamc@1245:                        false))
adamc@1244:                  andalso checkGoals goals unifs)
adamc@1238:               | ACond _ :: _ => false
adamc@1238:     in
adamc@1238:         checkGoals goals IM.empty
adamc@1238:     end
adamc@1236: 
adamc@1238: fun buildable uk (e, loc) =
adamc@1238:     let
adamc@1238:         fun doPols pols acc =
adamc@1236:             case pols of
adamc@1236:                 [] => ((*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
adamc@1236:                                                    ("Derived", p_exp e),
adamc@1236:                                                    ("Hyps", Print.p_list p_atom (#2 (!hyps)))];*)
adamc@1238:                        Cc.builtFrom (db, {UseKnown = uk, Base = acc, Derived = e}))
adamc@1236:               | (goals, es) :: pols =>
adamc@1238:                 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
adamc@1238:                 orelse doPols pols acc
adamc@1236:     in
adamc@1238:         if doPols (!sendable) [] then
adamc@1238:             ()
adamc@1238:         else
adamc@1238:             let
adamc@1244:                 val (_, hs, _) = !hyps
adamc@1238:             in
adamc@1238:                 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1245:                 Print.prefaces "Situation" [("User learns", p_exp e),
adamc@1245:                                             ("Hypotheses", Print.p_list p_atom hs)(*,
adamc@1244:                                             ("E-graph", Cc.p_database db)*)]
adamc@1238:             end
adamc@1236:     end       
adamc@1236: 
adamc@1236: fun checkPaths () =
adamc@1236:     let
adamc@1244:         val (n, hs, _) = !hyps
adamc@1244:         val hs = (n, hs)
adamc@1236:     in
adamc@1236:         app (fn r =>
adamc@1236:                 case !r of
adamc@1236:                     NONE => ()
adamc@1236:                   | SOME (hs, e) =>
adamc@1236:                     (r := NONE;
adamc@1236:                      setHyps hs;
adamc@1238:                      buildable true e)) (!path);
adamc@1236:         setHyps hs
adamc@1236:     end
adamc@1236: 
adamc@1238: fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
adamc@1243:                                            ("exps", Print.p_list p_exp (#2 v))];*)
adamc@1238:                    sendable := v :: !sendable)
adamc@1236: 
adamc@1238: fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*)
adamc@1244:                         complete ();
adamc@1238:                         checkPaths ();
adamc@1238:                         if isKnown e then
adamc@1238:                             ()
adamc@1238:                         else
adamc@1238:                             buildable uk (e, loc))
adamc@1236: 
adamc@1236: fun doable pols (loc : ErrorMsg.span) =
adamc@1236:     let
adamc@1236:         val pols = !pols
adamc@1236:     in
adamc@1244:         complete ();
adamc@1236:         if List.exists (fn goals =>
adamc@1238:                            if checkGoals goals (fn _ => true) then
adamc@1238:                                ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
adamc@1238:                                                         ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
adamc@1238:                                 true)
adamc@1238:                            else
adamc@1238:                                ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals),
adamc@1238:                                                            ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
adamc@1238:                                 false)) pols then
adamc@1236:             ()
adamc@1236:         else
adamc@1236:             let
adamc@1244:                 val (_, hs, _) = !hyps
adamc@1236:             in
adamc@1236:                 ErrorMsg.errorAt loc "The database update policy may be violated here.";
adamc@1245:                 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
adamc@1245:                                             ("E-graph", Cc.p_database db)*)]
adamc@1236:             end
adamc@1236:     end
adamc@1236: 
adamc@1236: val insertable = ref ([] : atom list list)
adamc@1236: fun allowInsert v = insertable := v :: !insertable
adamc@1236: val insert = doable insertable
adamc@1236: 
adamc@1236: val updatable = ref ([] : atom list list)
adamc@1236: fun allowUpdate v = updatable := v :: !updatable
adamc@1236: val update = doable updatable
adamc@1236: 
adamc@1236: val deletable = ref ([] : atom list list)
adamc@1236: fun allowDelete v = deletable := v :: !deletable
adamc@1236: val delete = doable deletable
adamc@1236: 
adamc@1238: fun reset () = (Cc.clear db;
adamc@1238:                 path := [];
adamc@1244:                 hyps := (0, [], ref false);
adamc@1238:                 nvar := 0;
adamc@1238:                 sendable := [];
adamc@1238:                 insertable := [];
adamc@1238:                 updatable := [];
adamc@1238:                 deletable := [])
adamc@1238: 
adamc@1236: fun havocReln r =
adamc@1236:     let
adamc@1236:         val n = !hnames
adamc@1244:         val (_, hs, _) = !hyps
adamc@1236:     in
adamc@1236:         hnames := n + 1;
adamc@1244:         hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
adamc@1236:     end
adamc@1236: 
adamc@1245: fun havocCookie cname =
adamc@1245:     let
adamc@1245:         val cname = "cookie/" ^ cname
adamc@1245:         val n = !hnames
adamc@1245:         val (_, hs, _) = !hyps
adamc@1245:     in
adamc@1245:         hnames := n + 1;
adamc@1245:         hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
adamc@1245:     end
adamc@1245: 
adamc@1238: fun debug () =
adamc@1238:     let
adamc@1244:         val (_, hs, _) = !hyps
adamc@1238:     in
adamc@1238:         Print.preface ("Hyps", Print.p_list p_atom hs)
adamc@1238:     end
adamc@1238: 
adamc@1236: end
adamc@1236: 
adamc@1236: 
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@1241: fun deinj env e =
adamc@1241:     case #1 e of
adamc@1241:         ERel n => SOME (List.nth (env, n))
adamc@1241:       | EField (e, f) =>
adamc@1241:         (case deinj env e of
adamc@1241:              NONE => NONE
adamc@1241:            | SOME e => SOME (Proj (e, f)))
adamc@1241:       | _ => NONE
adamc@1241: 
adamc@1220: fun expIn rv env rvOf =
adamc@1220:     let
adamc@1236:         fun expIn e =
adamc@1220:             let
adamc@1236:                 fun default () = inl (rv ())
adamc@1220:             in
adamc@1220:                 case e of
adamc@1236:                     SqConst p => inl (Const p)
adamc@1243:                   | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
adamc@1243:                   | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
adamc@1236:                   | Field (v, f) => inl (Proj (rvOf v, f))
adamc@1239:                   | Computed _ => default ()
adamc@1220:                   | Binop (bo, e1, e2) =>
adamc@1220:                     let
adamc@1236:                         val e1 = expIn e1
adamc@1236:                         val e2 = expIn e2
adamc@1220:                     in
adamc@1236:                         inr (case (bo, e1, e2) of
adamc@1236:                                  (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1243:                                | (Props f, v1, v2) =>
adamc@1243:                                  let
adamc@1243:                                      fun pin v =
adamc@1243:                                          case v of
adamc@1243:                                              inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
adamc@1243:                                            | inr p => p
adamc@1243:                                  in
adamc@1243:                                      f (pin v1, pin v2)
adamc@1243:                                  end
adamc@1236:                                | _ => Unknown)
adamc@1220:                     end
adamc@1220:                   | SqKnown e =>
adamc@1236:                     (case expIn e of
adamc@1236:                          inl e => inr (Reln (Known, [e]))
adamc@1236:                        | _ => inr Unknown)
adamc@1220:                   | Inj e =>
adamc@1241:                     inl (case deinj env e of
adamc@1241:                              NONE => rv ()
adamc@1241:                            | SOME e => e)
adamc@1220:                   | SqFunc (f, e) =>
adamc@1236:                     (case expIn e of
adamc@1236:                          inl e => inl (Func (Other f, [e]))
adamc@1220:                        | _ => default ())
adamc@1220:                      
adamc@1245:                   | Unmodeled => default ()
adamc@1220:             end
adamc@1220:     in
adamc@1220:         expIn
adamc@1220:     end
adamc@1216: 
adamc@1236: fun decomp {Save = save, Restore = restore, Add = add} =
adamc@1216:     let
adamc@1236:         fun go p k =
adamc@1236:             case p of
adamc@1238:                 True => (k () handle Cc.Contradiction => ())
adamc@1236:               | False => ()
adamc@1236:               | Unknown => ()
adamc@1236:               | And (p1, p2) => go p1 (fn () => go p2 k)
adamc@1236:               | Or (p1, p2) =>
adamc@1236:                 let
adamc@1236:                     val saved = save ()
adamc@1236:                 in
adamc@1236:                     go p1 k;
adamc@1236:                     restore saved;
adamc@1236:                     go p2 k
adamc@1236:                 end
adamc@1236:               | Reln x => (add (AReln x); k ())
adamc@1236:               | Cond x => (add (ACond x); k ())
adamc@1236:     in
adamc@1236:         go
adamc@1236:     end
adamc@1236: 
adamc@1236: datatype queryMode =
adamc@1238:          SomeCol of {New : (string * exp) option, Old : (string * exp) option, Outs : exp list} -> unit
adamc@1236:        | AllCols of exp -> unit
adamc@1236: 
adamc@1236: type 'a doQuery = {
adamc@1236:      Env : exp list,
adamc@1236:      NextVar : unit -> exp,
adamc@1236:      Add : atom -> unit,
adamc@1236:      Save : unit -> 'a,
adamc@1236:      Restore : 'a -> unit,
adamc@1241:      UsedExp : bool * exp -> unit,
adamc@1236:      Cont : queryMode
adamc@1236: }
adamc@1236: 
adamc@1241: fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
adamc@1236:     let
adamc@1241:         fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"
adamc@1216:     in
adamc@1216:         case parse query e of
adamc@1216:             NONE => default ()
adamc@1227:           | SOME q =>
adamc@1216:             let
adamc@1236:                 fun doQuery q =
adamc@1227:                     case q of
adamc@1227:                         Query1 r =>
adamc@1227:                         let
adamc@1238:                             val new = ref NONE
adamc@1238:                             val old = ref NONE
adamc@1238: 
adamc@1238:                             val rvs = map (fn (tab, v) =>
adamc@1238:                                               let
adamc@1238:                                                   val nv = #NextVar arg ()
adamc@1238:                                               in
adamc@1238:                                                   case v of
adamc@1238:                                                       "New" => new := SOME (tab, nv)
adamc@1238:                                                     | "Old" => old := SOME (tab, nv)
adamc@1238:                                                     | _ => ();
adamc@1238:                                                   (v, nv)
adamc@1238:                                               end) (#From r)
adamc@1214: 
adamc@1227:                             fun rvOf v =
adamc@1227:                                 case List.find (fn (v', _) => v' = v) rvs of
adamc@1227:                                     NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1227:                                   | SOME (_, e) => e
adamc@1214: 
adamc@1236:                             val expIn = expIn (#NextVar arg) (#Env arg) rvOf
adamc@1236: 
adamc@1236:                             val saved = #Save arg ()
adamc@1236:                             fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
adamc@1236: 
adamc@1227:                             fun usedFields e =
adamc@1227:                                 case e of
adamc@1227:                                     SqConst _ => []
adamc@1243:                                   | SqTrue => []
adamc@1243:                                   | SqFalse => []
adamc@1241:                                   | Field (v, f) => [(false, Proj (rvOf v, f))]
adamc@1239:                                   | Computed _ => []
adamc@1241:                                   | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
adamc@1227:                                   | SqKnown _ => []
adamc@1241:                                   | Inj e =>
adamc@1241:                                     (case deinj (#Env arg) e of
adamc@1241:                                          NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
adamc@1241:                                                   [])
adamc@1241:                                        | SOME e => [(true, e)])
adamc@1227:                                   | SqFunc (_, e) => usedFields e
adamc@1245:                                   | Unmodeled => []
adamc@1214: 
adamc@1236:                             fun doUsed () = case #Where r of
adamc@1236:                                                 NONE => ()
adamc@1236:                                               | SOME e =>
adamc@1241:                                                 app (#UsedExp arg) (usedFields e)
adamc@1211: 
adamc@1236:                             fun normal' () =
adamc@1236:                                 case #Cont arg of
adamc@1236:                                     SomeCol k =>
adamc@1227:                                     let
adamc@1236:                                         val sis = map (fn si =>
adamc@1236:                                                           case si of
adamc@1236:                                                               SqField (v, f) => Proj (rvOf v, f)
adamc@1236:                                                             | SqExp (e, f) =>
adamc@1236:                                                               case expIn e of
adamc@1236:                                                                   inr _ => #NextVar arg ()
adamc@1236:                                                                 | inl e => e) (#Select r)
adamc@1227:                                     in
adamc@1238:                                         k {New = !new, Old = !old, Outs = sis}
adamc@1227:                                     end
adamc@1236:                                   | AllCols k =>
adamc@1227:                                     let
adamc@1236:                                         val (ts, es) =
adamc@1236:                                             foldl (fn (si, (ts, es)) =>
adamc@1227:                                                       case si of
adamc@1227:                                                           SqField (v, f) =>
adamc@1227:                                                           let
adamc@1227:                                                               val fs = getOpt (SM.find (ts, v), SM.empty)
adamc@1227:                                                           in
adamc@1236:                                                               (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es)
adamc@1227:                                                           end
adamc@1227:                                                         | SqExp (e, f) =>
adamc@1227:                                                           let
adamc@1236:                                                               val e =
adamc@1236:                                                                   case expIn e of
adamc@1236:                                                                       inr _ => #NextVar arg ()
adamc@1236:                                                                     | inl e => e
adamc@1227:                                                           in
adamc@1236:                                                               (ts, SM.insert (es, f, e))
adamc@1227:                                                           end)
adamc@1236:                                                   (SM.empty, SM.empty) (#Select r)
adamc@1227:                                     in
adamc@1236:                                         k (Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
adamc@1236:                                                      (SM.listItemsi ts)
adamc@1236:                                                  @ SM.listItemsi es))
adamc@1227:                                     end
adamc@1227: 
adamc@1236:                             fun doWhere final =
adamc@1236:                                 (addFrom ();
adamc@1236:                                  case #Where r of
adamc@1236:                                      NONE => (doUsed (); final ())
adamc@1236:                                    | SOME e =>
adamc@1243:                                      let
adamc@1243:                                          val p = case expIn e of
adamc@1243:                                                      inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
adamc@1243:                                                    | inr p => p
adamc@1243: 
adamc@1243:                                          val saved = #Save arg ()
adamc@1243:                                      in
adamc@1243:                                          decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
adamc@1243:                                                 p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
adamc@1243:                                          #Restore arg saved
adamc@1243:                                      end)
adamc@1236:                                 handle Cc.Contradiction => ()
adamc@1236: 
adamc@1236:                             fun normal () = doWhere normal'
adamc@1227:                         in
adamc@1236:                             (case #Select r of
adamc@1236:                                  [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1236:                                  (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1236:                                       Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1236:                                       (case #Cont arg of
adamc@1236:                                            SomeCol _ => ()
adamc@1236:                                          | AllCols k =>
adamc@1236:                                            let
adamc@1236:                                                fun answer e = k (Recd [(f, e)])
adamc@1236: 
adamc@1236:                                                val saved = #Save arg ()
adamc@1238:                                                val () = (answer (Func (DtCon0 "Basis.bool.False", [])))
adamc@1238:                                                         handle Cc.Contradiction => ()
adamc@1236:                                            in
adamc@1238:                                                #Restore arg saved;
adamc@1238:                                                (*print "True time!\n";*)
adamc@1236:                                                doWhere (fn () => answer (Func (DtCon0 "Basis.bool.True", [])));
adamc@1236:                                                #Restore arg saved
adamc@1236:                                            end)
adamc@1236:                                     | _ => normal ())
adamc@1236:                                | _ => normal ())
adamc@1236:                             before #Restore arg saved
adamc@1227:                         end
adamc@1227:                       | Union (q1, q2) =>
adamc@1220:                         let
adamc@1236:                             val saved = #Save arg ()
adamc@1220:                         in
adamc@1236:                             doQuery q1;
adamc@1236:                             #Restore arg saved;
adamc@1236:                             doQuery q2;
adamc@1236:                             #Restore arg saved
adamc@1220:                         end
adamc@1216:             in
adamc@1236:                 doQuery q
adamc@1216:             end
adamc@1220:     end
adamc@1220: 
adamc@1211: fun evalPat env e (pt, _) =
adamc@1211:     case pt of
adamc@1236:         PWild => env
adamc@1236:       | PVar _ => e :: env
adamc@1236:       | PPrim _ => env
adamc@1236:       | PCon (_, pc, NONE) => (St.assert [AReln (PCon0 (patCon pc), [e])]; env)
adamc@1211:       | PCon (_, pc, SOME pt) =>
adamc@1211:         let
adamc@1236:             val env = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211:         in
adamc@1236:             St.assert [AReln (PCon1 (patCon pc), [e])];
adamc@1236:             env
adamc@1211:         end
adamc@1211:       | PRecord xpts =>
adamc@1236:         foldl (fn ((x, pt, _), env) => evalPat env (Proj (e, x)) pt) env xpts
adamc@1236:       | PNone _ => (St.assert [AReln (PCon0 "None", [e])]; env)
adamc@1211:       | PSome (_, pt) =>
adamc@1211:         let
adamc@1236:             val env = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211:         in
adamc@1236:             St.assert [AReln (PCon1 "Some", [e])];
adamc@1236:             env
adamc@1211:         end
adamc@1211: 
adamc@1236: fun evalExp env (e as (_, loc)) k =
adamc@1236:     let
adamc@1238:         (*val () = St.debug ()*)
adamc@1236:         (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
adamc@1211: 
adamc@1236:         fun default () = k (Var (St.nextVar ()))
adamc@1234: 
adamc@1234:         fun doFfi (m, s, es) =
adamc@1234:             if m = "Basis" andalso SS.member (writers, s) then
adamc@1234:                 let
adamc@1236:                     fun doArgs es =
adamc@1236:                         case es of
adamc@1245:                             [] =>
adamc@1245:                             (if s = "set_cookie" then
adamc@1245:                                  case es of
adamc@1245:                                      [_, cname, _, _, _] =>
adamc@1245:                                      (case #1 cname of
adamc@1245:                                           EPrim (Prim.String cname) =>
adamc@1245:                                           St.havocCookie cname
adamc@1245:                                         | _ => ())
adamc@1245:                                    | _ => ()
adamc@1245:                              else
adamc@1245:                                  ();
adamc@1245:                              k (Recd []))
adamc@1236:                           | e :: es =>
adamc@1238:                             evalExp env e (fn e => (St.send true (e, loc); doArgs es))
adamc@1234:                 in
adamc@1236:                     doArgs es
adamc@1234:                 end
adamc@1234:             else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1234:                 default ()
adamc@1234:             else
adamc@1234:                 let
adamc@1236:                     fun doArgs (es, acc) =
adamc@1236:                         case es of
adamc@1236:                             [] => k (Func (Other (m ^ "." ^ s), rev acc))
adamc@1236:                           | e :: es =>
adamc@1236:                             evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1234:                 in
adamc@1236:                     doArgs (es, [])
adamc@1234:                 end            
adamc@1200:     in
adamc@1200:         case #1 e of
adamc@1236:             EPrim p => k (Const p)
adamc@1236:           | ERel n => k (List.nth (env, n))
adamc@1200:           | ENamed _ => default ()
adamc@1236:           | ECon (_, pc, NONE) => k (Func (DtCon0 (patCon pc), []))
adamc@1236:           | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
adamc@1236:           | ENone _ => k (Func (DtCon0 "None", []))
adamc@1236:           | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
adamc@1200:           | EFfi _ => default ()
adamc@1213: 
adamc@1234:           | EFfiApp x => doFfi x
adamc@1234:           | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
adamc@1213: 
adamc@1236:           | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
adamc@1213: 
adamc@1200:           | EAbs _ => default ()
adamc@1236:           | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
adamc@1236:           | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
adamc@1200:           | ERecord xets =>
adamc@1200:             let
adamc@1236:                 fun doFields (xes, acc) =
adamc@1236:                     case xes of
adamc@1236:                         [] => k (Recd (rev acc))
adamc@1236:                       | (x, e, _) :: xes =>
adamc@1236:                         evalExp env e (fn e => doFields (xes, (x, e) :: acc))
adamc@1200:             in
adamc@1236:                 doFields (xets, [])
adamc@1200:             end
adamc@1236:           | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
adamc@1218:           | ECase (e, pes, {result = res, ...}) =>
adamc@1236:             evalExp env e (fn e =>
adamc@1218:                               let
adamc@1236:                                   val () = St.addPath (e, loc)
adamc@1218:                               in
adamc@1236:                                   app (fn (p, pe) =>
adamc@1236:                                           let
adamc@1236:                                               val saved = St.stash ()
adamc@1236:                                           in
adamc@1238:                                               let
adamc@1238:                                                   val env = evalPat env e p
adamc@1238:                                               in
adamc@1238:                                                   evalExp env pe k;
adamc@1238:                                                   St.reinstate saved
adamc@1238:                                               end
adamc@1238:                                               handle Cc.Contradiction => St.reinstate saved
adamc@1236:                                           end) pes
adamc@1238:                               end)
adamc@1200:           | EStrcat (e1, e2) =>
adamc@1236:             evalExp env e1 (fn e1 =>
adamc@1236:                 evalExp env e2 (fn e2 =>
adamc@1236:                                    k (Func (Other "cat", [e1, e2]))))
adamc@1238:           | EError (e, _) => evalExp env e (fn e => St.send true (e, loc))
adamc@1200:           | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1236:             evalExp env b (fn b =>
adamc@1238:                               (St.send true (b, loc);
adamc@1236:                                evalExp env m
adamc@1238:                                (fn m => St.send true (m, loc))))
adamc@1200:           | ERedirect (e, _) =>
adamc@1238:             evalExp env e (fn e => St.send true (e, loc))
adamc@1200:           | EWrite e =>
adamc@1238:             evalExp env e (fn e => (St.send true (e, loc);
adamc@1236:                                     k (Recd [])))
adamc@1200:           | ESeq (e1, e2) =>
adamc@1236:             evalExp env e1 (fn _ => evalExp env e2 k)
adamc@1200:           | ELet (_, _, e1, e2) =>
adamc@1236:             evalExp env e1 (fn e1 => evalExp (e1 :: env) e2 k)
adamc@1200:           | EClosure (n, es) =>
adamc@1200:             let
adamc@1236:                 fun doArgs (es, acc) =
adamc@1236:                     case es of
adamc@1236:                         [] => k (Func (Other ("Cl" ^ Int.toString n), rev acc))
adamc@1236:                       | e :: es =>
adamc@1236:                         evalExp env e (fn e => doArgs (es, e :: acc))
adamc@1200:             in
adamc@1236:                 doArgs (es, [])
adamc@1200:             end
adamc@1200: 
adamc@1235:           | EQuery {query = q, body = b, initial = i, state = state, ...} =>
adamc@1238:             evalExp env i (fn i =>
adamc@1238:                               let
adamc@1238:                                   val saved = St.stash ()
adamc@1200: 
adamc@1238:                                   val () = (k i)
adamc@1238:                                       handle Cc.Contradiction => ()
adamc@1238:                                   val () = St.reinstate saved
adamc@1238: 
adamc@1238:                                   val r = Var (St.nextVar ())
adamc@1238:                                   val acc = Var (St.nextVar ())
adamc@1242: 
adamc@1242:                                   val touched = MonoUtil.Exp.fold {typ = fn (_, touched) => touched,
adamc@1242:                                                                    exp = fn (e, touched) =>
adamc@1242:                                                                             case e of
adamc@1242:                                                                                 EDml e =>
adamc@1242:                                                                                 (case parse dml e of
adamc@1242:                                                                                      NONE => touched
adamc@1242:                                                                                    | SOME c =>
adamc@1242:                                                                                      case c of
adamc@1242:                                                                                          Insert _ => touched
adamc@1242:                                                                                        | Delete (tab, _) =>
adamc@1242:                                                                                          SS.add (touched, tab)
adamc@1242:                                                                                        | Update (tab, _, _) =>
adamc@1242:                                                                                          SS.add (touched, tab))
adamc@1242:                                                                               | _ => touched}
adamc@1242:                                                                   SS.empty b
adamc@1238:                               in
adamc@1242:                                   SS.app (St.havocReln o Sql) touched;
adamc@1242: 
adamc@1242:                                   doQuery {Env = env,
adamc@1242:                                            NextVar = Var o St.nextVar,
adamc@1242:                                            Add = fn a => St.assert [a],
adamc@1242:                                            Save = St.stash,
adamc@1242:                                            Restore = St.reinstate,
adamc@1242:                                            UsedExp = fn (b, e) => St.send b (e, loc),
adamc@1242:                                            Cont = AllCols (fn x =>
adamc@1242:                                                               (St.assert [AReln (Eq, [r, x])];
adamc@1242:                                                                evalExp (acc :: r :: env) b k))} q
adamc@1238:                               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@1236:                          val new = St.nextVar ()
adamc@1220: 
adamc@1236:                          val expIn = expIn (Var o St.nextVar) env
adamc@1236:                                            (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [1]")
adamc@1220: 
adamc@1236:                          val es = map (fn (x, e) =>
adamc@1236:                                           case expIn e of
adamc@1236:                                               inl e => (x, e)
adamc@1236:                                             | inr _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT [2]")
adamc@1236:                                   es
adamc@1220: 
adamc@1236:                          val saved = St.stash ()
adamc@1220:                      in
adamc@1236:                          St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
adamc@1236:                          St.insert loc;
adamc@1236:                          St.reinstate saved;
adamc@1236:                          k (Recd [])
adamc@1221:                      end
adamc@1221:                    | Delete (tab, e) =>
adamc@1221:                      let
adamc@1236:                          val old = St.nextVar ()
adamc@1236:                                    
adamc@1236:                          val expIn = expIn (Var o St.nextVar) env
adamc@1236:                                            (fn "T" => Var old
adamc@1236:                                              | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221: 
adamc@1236:                          val p = case expIn e of
adamc@1236:                                      inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" 
adamc@1236:                                    | inr p => p
adamc@1236:                                                           
adamc@1236:                          val saved = St.stash ()
adamc@1221:                      in
adamc@1238:                          St.assert [AReln (Sql (tab ^ "$Old"), [Var old])];
adamc@1236:                          decomp {Save = St.stash,
adamc@1236:                                  Restore = St.reinstate,
adamc@1236:                                  Add = fn a => St.assert [a]} p
adamc@1236:                                 (fn () => (St.delete loc;
adamc@1236:                                            St.reinstate saved;
adamc@1236:                                            St.havocReln (Sql tab);
adamc@1236:                                            k (Recd []))
adamc@1236:                                     handle Cc.Contradiction => ())
adamc@1223:                      end
adamc@1223:                    | Update (tab, fs, e) =>
adamc@1223:                      let
adamc@1236:                          val new = St.nextVar ()
adamc@1236:                          val old = St.nextVar ()
adamc@1223: 
adamc@1236:                          val expIn = expIn (Var o St.nextVar) env
adamc@1236:                                            (fn "T" => Var old
adamc@1236:                                              | _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1223: 
adamc@1236:                          val fs = map
adamc@1236:                                       (fn (x, e) =>
adamc@1236:                                           (x, case expIn e of
adamc@1236:                                                   inl e => e
adamc@1236:                                                 | inr _ => raise Fail
adamc@1236:                                                                      ("Iflow.evalExp: Selecting "
adamc@1236:                                                                       ^ "boolean expression")))
adamc@1236:                                       fs
adamc@1223: 
adamc@1226:                          val fs' = case SM.find (!tabs, tab) of
adamc@1224:                                        NONE => raise Fail "Iflow.evalExp: Updating unknown table"
adamc@1226:                                      | SOME (fs', _) => fs'
adamc@1224: 
adamc@1224:                          val fs = foldl (fn (f, fs) =>
adamc@1224:                                             if List.exists (fn (f', _) => f' = f) fs then
adamc@1224:                                                 fs
adamc@1224:                                             else
adamc@1224:                                                 (f, Proj (Var old, f)) :: fs) fs fs'
adamc@1224: 
adamc@1236:                          val p = case expIn e of
adamc@1236:                                            inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" 
adamc@1236:                                          | inr p => p
adamc@1236:                          val saved = St.stash ()
adamc@1223:                      in
adamc@1236:                          St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
adamc@1238:                                     AReln (Sql (tab ^ "$Old"), [Var old])];
adamc@1236:                          decomp {Save = St.stash,
adamc@1236:                                  Restore = St.reinstate,
adamc@1236:                                  Add = fn a => St.assert [a]} p
adamc@1236:                                 (fn () => (St.update loc;
adamc@1236:                                            St.reinstate saved;
adamc@1236:                                            St.havocReln (Sql tab);
adamc@1236:                                            k (Recd []))
adamc@1236:                                     handle Cc.Contradiction => ())
adamc@1220:                      end)
adamc@1220:                      
adamc@1229:           | ENextval (EPrim (Prim.String seq), _) =>
adamc@1229:             let
adamc@1236:                 val nv = St.nextVar ()
adamc@1229:             in
adamc@1236:                 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
adamc@1236:                 k (Var nv)
adamc@1229:             end
adamc@1200:           | ENextval _ => default ()
adamc@1200:           | ESetval _ => default ()
adamc@1200: 
adamc@1238:           | EUnurlify ((EFfiApp ("Basis", "get_cookie", [(EPrim (Prim.String cname), _)]), _), _, _) =>
adamc@1217:             let
adamc@1238:                 val e = Var (St.nextVar ())
adamc@1245:                 val e' = Func (Other ("cookie/" ^ cname), [])
adamc@1217:             in
adamc@1245:                 St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
adamc@1238:                 k e
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@1236:         val () = St.reset ()
adamc@1236: 
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@1236:         fun decl (d, _) =
adamc@1200:             case d of
adamc@1226:                 DTable (tab, fs, pk, _) =>
adamc@1226:                 let
adamc@1226:                     val ks =
adamc@1226:                         case #1 pk of
adamc@1226:                             EPrim (Prim.String s) =>
adamc@1226:                             (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
adamc@1226:                                  [] => []
adamc@1226:                                | pk => [pk])
adamc@1226:                           | _ => []
adamc@1226:                 in
adamc@1226:                     if size tab >= 3 then
adamc@1236:                         tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
adamc@1236:                                            (map #1 fs,
adamc@1236:                                             map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
adamc@1236:                                                               ^ String.extract (s, 4, NONE))) ks))
adamc@1226:                     else
adamc@1226:                         raise Fail "Table name does not begin with uw_"
adamc@1226:                 end
adamc@1238:               | DVal (x, n, _, e, _) =>
adamc@1200:                 let
adamc@1238:                     (*val () = print ("\n=== " ^ x ^ " ===\n\n");*)
adamc@1238: 
adamc@1207:                     val isExptd = IS.member (exptd, n)
adamc@1207: 
adamc@1236:                     val saved = St.stash ()
adamc@1236: 
adamc@1236:                     fun deAbs (e, env, ps) =
adamc@1200:                         case #1 e of
adamc@1236:                             EAbs (_, _, _, e) =>
adamc@1236:                             let
adamc@1236:                                 val nv = Var (St.nextVar ())
adamc@1236:                             in
adamc@1236:                                 deAbs (e, nv :: env,
adamc@1236:                                        if isExptd then
adamc@1236:                                            AReln (Known, [nv]) :: ps
adamc@1236:                                        else
adamc@1236:                                            ps)
adamc@1236:                             end
adamc@1236:                           | _ => (e, env, ps)
adamc@1200: 
adamc@1236:                     val (e, env, ps) = deAbs (e, [], [])
adamc@1200:                 in
adamc@1236:                     St.assert ps;
adamc@1236:                     (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
adamc@1236:                     St.reinstate saved
adamc@1200:                 end
adamc@1202: 
adamc@1220:               | DPolicy pol =>
adamc@1218:                 let
adamc@1236:                     val rvN = ref 0
adamc@1236:                     fun rv () =
adamc@1236:                         let
adamc@1236:                             val n = !rvN
adamc@1236:                         in
adamc@1236:                             rvN := n + 1;
adamc@1236:                             Lvar n
adamc@1236:                         end
adamc@1236: 
adamc@1236:                     val atoms = ref ([] : atom list)
adamc@1236:                     fun doQ k = doQuery {Env = [],
adamc@1236:                                          NextVar = rv,
adamc@1236:                                          Add = fn a => atoms := a :: !atoms,
adamc@1236:                                          Save = fn () => !atoms,
adamc@1236:                                          Restore = fn ls => atoms := ls,
adamc@1236:                                          UsedExp = fn _ => (),
adamc@1238:                                          Cont = SomeCol (fn r => k (rev (!atoms), r))}
adamc@1238: 
adamc@1238:                     fun untab tab = List.filter (fn AReln (Sql tab', _) => tab' <> tab
adamc@1238:                                                   | _ => true)
adamc@1218:                 in
adamc@1220:                     case pol of
adamc@1220:                         PolClient e =>
adamc@1238:                         doQ (fn (ats, {Outs = es, ...}) => St.allowSend (ats, es)) e
adamc@1220:                       | PolInsert e =>
adamc@1238:                         doQ (fn (ats, {New = SOME (tab, new), ...}) =>
adamc@1238:                                 St.allowInsert (AReln (Sql (tab ^ "$New"), [new]) :: untab tab ats)
adamc@1238:                               | _ => raise Fail "Iflow: No New in mayInsert policy") e
adamc@1221:                       | PolDelete e =>
adamc@1238:                         doQ (fn (ats, {Old = SOME (tab, old), ...}) =>
adamc@1238:                                 St.allowDelete (AReln (Sql (tab ^ "$Old"), [old]) :: untab tab ats)
adamc@1238:                               | _ => raise Fail "Iflow: No Old in mayDelete policy") e
adamc@1223:                       | PolUpdate e =>
adamc@1238:                         doQ (fn (ats, {New = SOME (tab, new), Old = SOME (_, old), ...}) =>
adamc@1238:                                 St.allowUpdate (AReln (Sql (tab ^ "$Old"), [old])
adamc@1238:                                                 :: AReln (Sql (tab ^ "$New"), [new])
adamc@1238:                                                 :: untab tab ats)
adamc@1238:                               | _ => raise Fail "Iflow: No New or Old in mayUpdate policy") e
adamc@1229:                       | PolSequence e =>
adamc@1229:                         (case #1 e of
adamc@1229:                              EPrim (Prim.String seq) =>
adamc@1229:                              let
adamc@1236:                                  val p = AReln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
adamc@1229:                                  val outs = [Lvar 0]
adamc@1229:                              in
adamc@1236:                                  St.allowSend ([p], outs)
adamc@1229:                              end
adamc@1236:                            | _ => ())
adamc@1218:                 end
adamc@1214:                                         
adamc@1236:               | _ => ()
adamc@1200:     in
adamc@1236:         app decl file
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