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@1200: structure SS = BinarySetFn(struct
adamc@1200:                            type ord_key = string
adamc@1200:                            val compare = String.compare
adamc@1200:                            end)
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@1200:                "urlifyBool_w"]
adamc@1200: 
adamc@1200: val writers = SS.addList (SS.empty, writers)
adamc@1200: 
adamc@1200: type lvar = int
adamc@1200: 
adamc@1200: datatype exp =
adamc@1200:          Const of Prim.t
adamc@1200:        | Var of int
adamc@1200:        | Lvar of lvar
adamc@1200:        | Func of string * exp list
adamc@1200:        | Recd of (string * exp) list
adamc@1200:        | Proj of exp * string
adamc@1200:        | Finish
adamc@1200: 
adamc@1200: datatype reln =
adamc@1207:          Known
adamc@1207:        | Sql of string
adamc@1211:        | DtCon 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@1200:        | Select of int * lvar * lvar * prop * exp
adamc@1200: 
adamc@1200: local
adamc@1207:     open Print
adamc@1207:     val string = PD.string
adamc@1207: in
adamc@1207: 
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@1207:       | Lvar n => string ("X" ^ Int.toString n)
adamc@1207:       | Func (f, es) => box [string (f ^ "("),
adamc@1207:                              p_list p_exp es,
adamc@1207:                              string ")"]
adamc@1207:       | Recd xes => box [string "{",
adamc@1210:                          p_list (fn (x, e) => box [string x,
adamc@1207:                                                    space,
adamc@1207:                                                    string "=",
adamc@1207:                                                    space,
adamc@1207:                                                    p_exp e]) xes,
adamc@1207:                          string "}"]
adamc@1207:       | Proj (e, x) => box [p_exp e,
adamc@1207:                             string ("." ^ x)]
adamc@1207:       | Finish => string "FINISH"
adamc@1207: 
adamc@1210: fun p_bop s es =
adamc@1210:     case es of
adamc@1210:         [e1, e2] => box [p_exp e1,
adamc@1210:                          space,
adamc@1210:                          string s,
adamc@1210:                          space,
adamc@1210:                          p_exp e2]
adamc@1210:       | _ => raise Fail "Iflow.p_bop"
adamc@1210: 
adamc@1207: fun p_reln r es =
adamc@1207:     case r of
adamc@1207:         Known =>
adamc@1207:         (case es of
adamc@1207:              [e] => box [string "known(",
adamc@1207:                          p_exp e,
adamc@1207:                          string ")"]
adamc@1207:            | _ => raise Fail "Iflow.p_reln: Known")
adamc@1207:       | Sql s => box [string (s ^ "("),
adamc@1207:                       p_list p_exp es,
adamc@1207:                       string ")"]
adamc@1211:       | DtCon 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@1207:       | Select (n1, n2, n3, p, e) => box [string ("select(x" ^ Int.toString n1
adamc@1207:                                                   ^ ",X" ^ Int.toString n2
adamc@1207:                                                   ^ ",X" ^ Int.toString n3
adamc@1207:                                                   ^ "){"),
adamc@1207:                                           p_prop p,
adamc@1207:                                           string "}{",
adamc@1207:                                           p_exp e,
adamc@1207:                                           string "}"]
adamc@1207: 
adamc@1207: end
adamc@1207: 
adamc@1207: local
adamc@1202:     val count = ref 1
adamc@1200: in
adamc@1200: fun newLvar () =
adamc@1200:     let
adamc@1200:         val n = !count
adamc@1200:     in
adamc@1200:         count := n + 1;
adamc@1200:         n
adamc@1200:     end
adamc@1200: end
adamc@1200: 
adamc@1200: fun subExp (v, lv) =
adamc@1200:     let
adamc@1200:         fun sub e =
adamc@1200:             case e of
adamc@1200:                 Const _ => e
adamc@1200:               | Var v' => if v' = v then Lvar lv else e
adamc@1200:               | Lvar _ => e
adamc@1200:               | Func (f, es) => Func (f, map sub es)
adamc@1200:               | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
adamc@1200:               | Proj (e, s) => Proj (sub e, s)
adamc@1200:               | Finish => Finish
adamc@1200:     in
adamc@1200:         sub
adamc@1200:     end
adamc@1200: 
adamc@1200: fun subProp (v, lv) =
adamc@1200:     let
adamc@1200:         fun sub p =
adamc@1200:             case p of
adamc@1200:                 True => p
adamc@1200:               | False => p
adamc@1200:               | Unknown => p
adamc@1200:               | And (p1, p2) => And (sub p1, sub p2)
adamc@1200:               | Or (p1, p2) => Or (sub p1, sub p2)
adamc@1200:               | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
adamc@1200:               | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
adamc@1200:     in
adamc@1200:         sub
adamc@1200:     end
adamc@1200: 
adamc@1200: fun isKnown e =
adamc@1200:     case e of
adamc@1200:         Const _ => true
adamc@1200:       | Func (_, es) => List.all isKnown es
adamc@1200:       | Recd xes => List.all (isKnown o #2) xes
adamc@1200:       | Proj (e, _) => isKnown e
adamc@1200:       | _ => false
adamc@1200: 
adamc@1200: fun isFinish e =
adamc@1200:     case e of
adamc@1200:         Finish => true
adamc@1200:       | _ => false
adamc@1200: 
adamc@1208: val unif = ref (IM.empty : exp IM.map)
adamc@1208: 
adamc@1208: fun reset () = unif := IM.empty
adamc@1208: fun save () = !unif
adamc@1208: fun restore x = unif := x
adamc@1208: 
adamc@1200: fun simplify e =
adamc@1200:     case e of
adamc@1200:         Const _ => e
adamc@1200:       | Var _ => e
adamc@1208:       | Lvar n =>
adamc@1208:         (case IM.find (!unif, n) of
adamc@1208:              NONE => e
adamc@1208:            | SOME e => simplify e)
adamc@1200:       | Func (f, es) =>
adamc@1200:         let
adamc@1200:             val es = map simplify es
adamc@1211: 
adamc@1211:             fun default () = Func (f, es)
adamc@1200:         in
adamc@1200:             if List.exists isFinish es then
adamc@1200:                 Finish
adamc@1211:             else if String.isPrefix "un" f then
adamc@1211:                 case es of
adamc@1211:                     [Func (f', [e])] => if f' = String.extract (f, 2, NONE) then
adamc@1211:                                             e
adamc@1211:                                         else
adamc@1211:                                             default ()
adamc@1211:                   | _ => default ()
adamc@1200:             else
adamc@1211:                 default ()
adamc@1200:         end
adamc@1200:       | Recd xes =>
adamc@1200:         let
adamc@1200:             val xes = map (fn (x, e) => (x, simplify e)) xes
adamc@1200:         in
adamc@1200:             if List.exists (isFinish o #2) xes then
adamc@1200:                 Finish
adamc@1200:             else
adamc@1200:                 Recd xes
adamc@1200:         end
adamc@1200:       | Proj (e, s) =>
adamc@1200:         (case simplify e of
adamc@1200:              Recd xes =>
adamc@1200:              getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
adamc@1200:            | e' =>
adamc@1200:              if isFinish e' then
adamc@1200:                  Finish
adamc@1200:              else
adamc@1200:                  Proj (e', s))
adamc@1200:       | Finish => Finish
adamc@1200: 
adamc@1202: fun decomp fals or =
adamc@1200:     let
adamc@1200:         fun decomp p k =
adamc@1200:             case p of
adamc@1200:                 True => k []
adamc@1202:               | False => fals
adamc@1200:               | Unknown => k []
adamc@1200:               | And (p1, p2) => 
adamc@1200:                 decomp p1 (fn ps1 =>
adamc@1200:                               decomp p2 (fn ps2 =>
adamc@1200:                                             k (ps1 @ ps2)))
adamc@1200:               | Or (p1, p2) =>
adamc@1200:                 or (decomp p1 k, fn () => decomp p2 k)
adamc@1200:               | Reln x => k [x]
adamc@1200:               | Select _ => k []
adamc@1200:     in
adamc@1200:         decomp
adamc@1200:     end
adamc@1200: 
adamc@1202: fun lvarIn lv =
adamc@1202:     let
adamc@1202:         fun lvi e =
adamc@1202:             case e of
adamc@1202:                 Const _ => false
adamc@1202:               | Var _ => false
adamc@1202:               | Lvar lv' => lv' = lv
adamc@1202:               | Func (_, es) => List.exists lvi es
adamc@1202:               | Recd xes => List.exists (lvi o #2) xes
adamc@1202:               | Proj (e, _) => lvi e
adamc@1202:               | Finish => false
adamc@1202:     in
adamc@1202:         lvi
adamc@1202:     end
adamc@1202: 
adamc@1202: fun eq' (e1, e2) =
adamc@1202:     case (e1, e2) of
adamc@1202:         (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202:       | (Var n1, Var n2) => n1 = n2
adamc@1202: 
adamc@1202:       | (Lvar n1, _) =>
adamc@1202:         (case IM.find (!unif, n1) of
adamc@1202:              SOME e1 => eq' (e1, e2)
adamc@1202:            | NONE =>
adamc@1202:              case e2 of
adamc@1202:                  Lvar n2 =>
adamc@1202:                  (case IM.find (!unif, n2) of
adamc@1202:                       SOME e2 => eq' (e1, e2)
adamc@1202:                     | NONE => n1 = n2
adamc@1208:                               orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202:                                       true))
adamc@1202:                | _ =>
adamc@1202:                  if lvarIn n1 e2 then
adamc@1202:                      false
adamc@1202:                  else
adamc@1202:                      (unif := IM.insert (!unif, n1, e2);
adamc@1202:                       true))
adamc@1202: 
adamc@1202:       | (_, Lvar n2) =>
adamc@1202:         (case IM.find (!unif, n2) of
adamc@1202:              SOME e2 => eq' (e1, e2)
adamc@1202:            | NONE =>
adamc@1202:              if lvarIn n2 e1 then
adamc@1202:                  false
adamc@1202:              else
adamc@1202:                  (unif := IM.insert (!unif, n2, e1);
adamc@1202:                   true))
adamc@1202:                                        
adamc@1202:       | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202:       | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202:       | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202:       | (Finish, Finish) => true
adamc@1202:       | _ => false
adamc@1202: 
adamc@1202: fun eq (e1, e2) =
adamc@1202:     let
adamc@1203:         val saved = save ()
adamc@1202:     in
adamc@1202:         if eq' (simplify e1, simplify e2) then
adamc@1202:             true
adamc@1202:         else
adamc@1203:             (restore saved;
adamc@1202:              false)
adamc@1202:     end
adamc@1202: 
adamc@1208: val debug = ref false
adamc@1208: 
adamc@1211: fun eeq (e1, e2) =
adamc@1211:     case (e1, e2) of
adamc@1211:         (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211:       | (Var n1, Var n2) => n1 = n2
adamc@1211:       | (Lvar n1, Lvar n2) => n1 = n2
adamc@1211:       | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211:       | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211:                                   List.all (fn (x2, e2) =>
adamc@1211:                                                List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211:       | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211:       | (Finish, Finish) => true
adamc@1211:       | _ => false
adamc@1211:              
adamc@1208: (* Congruence closure *)
adamc@1208: structure Cc :> sig
adamc@1208:     type t
adamc@1208:     val empty : t
adamc@1208:     val assert : t * exp * exp -> t
adamc@1208:     val query : t * exp * exp -> bool
adamc@1208:     val allPeers : t * exp -> exp list
adamc@1208: end = struct
adamc@1208: 
adamc@1211: fun eq (e1, e2) = eeq (simplify e1, simplify e2)
adamc@1208: 
adamc@1208: type t = (exp * exp) list
adamc@1208: 
adamc@1208: val empty = []
adamc@1208: 
adamc@1208: fun lookup (t, e) =
adamc@1208:     case List.find (fn (e', _) => eq (e', e)) t of
adamc@1208:         NONE => e
adamc@1208:       | SOME (_, e2) => lookup (t, e2)
adamc@1208: 
adamc@1208: fun assert (t, e1, e2) =
adamc@1208:     let
adamc@1208:         val r1 = lookup (t, e1)
adamc@1208:         val r2 = lookup (t, e2)
adamc@1208:     in
adamc@1208:         if eq (r1, r2) then
adamc@1208:             t
adamc@1208:         else
adamc@1208:             (r1, r2) :: t
adamc@1208:     end
adamc@1208: 
adamc@1208: open Print
adamc@1208: 
adamc@1208: fun query (t, e1, e2) =
adamc@1208:     (if !debug then
adamc@1208:          prefaces "CC query" [("e1", p_exp (simplify e1)),
adamc@1208:                               ("e2", p_exp (simplify e2)),
adamc@1208:                               ("t", p_list (fn (e1, e2) => box [p_exp (simplify e1),
adamc@1208:                                                                 space,
adamc@1208:                                                                 PD.string "->",
adamc@1208:                                                                 space,
adamc@1208:                                                                 p_exp (simplify e2)]) t)]
adamc@1208:      else
adamc@1208:          ();
adamc@1208:      eq (lookup (t, e1), lookup (t, e2)))
adamc@1208: 
adamc@1208: fun allPeers (t, e) =
adamc@1208:     let
adamc@1208:         val r = lookup (t, e)
adamc@1208:     in
adamc@1208:         r :: List.mapPartial (fn (e1, e2) =>
adamc@1208:                                  let
adamc@1208:                                      val r' = lookup (t, e2)
adamc@1208:                                  in
adamc@1208:                                      if eq (r, r') then
adamc@1208:                                          SOME e1
adamc@1208:                                      else
adamc@1208:                                          NONE
adamc@1208:                                  end) t
adamc@1208:     end
adamc@1208: 
adamc@1208: end
adamc@1208: 
adamc@1208: fun rimp cc ((r1, es1), (r2, es2)) =
adamc@1202:     case (r1, r2) of
adamc@1202:         (Sql r1', Sql r2') =>
adamc@1202:         r1' = r2' andalso
adamc@1202:         (case (es1, es2) of
adamc@1202:              ([Recd xes1], [Recd xes2]) =>
adamc@1202:              let
adamc@1203:                  val saved = save ()
adamc@1202:              in
adamc@1202:                  if List.all (fn (f, e2) =>
adamc@1203:                                  case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
adamc@1203:                                      NONE => true
adamc@1203:                                    | SOME e1 => eq (e1, e2)) xes2 then
adamc@1202:                      true
adamc@1202:                  else
adamc@1203:                      (restore saved;
adamc@1202:                       false)
adamc@1202:              end
adamc@1202:            | _ => false)
adamc@1202:       | (Eq, Eq) =>
adamc@1202:         (case (es1, es2) of
adamc@1202:              ([x1, y1], [x2, y2]) =>
adamc@1202:              let
adamc@1203:                  val saved = save ()
adamc@1202:              in
adamc@1202:                  if eq (x1, x2) andalso eq (y1, y2) then
adamc@1202:                      true
adamc@1202:                  else
adamc@1203:                      (restore saved;
adamc@1208:                       if eq (x1, y2) andalso eq (y1, x2) then
adamc@1208:                           true
adamc@1208:                       else
adamc@1208:                           (restore saved;
adamc@1208:                            false))
adamc@1202:              end
adamc@1202:            | _ => false)
adamc@1207:       | (Known, Known) =>
adamc@1207:         (case (es1, es2) of
adamc@1208:              ([Var v], [e2]) =>
adamc@1207:              let
adamc@1208:                  fun matches e =
adamc@1208:                      case e of
adamc@1208:                          Var v' => v' = v
adamc@1208:                        | Proj (e, _) => matches e
adamc@1211:                        | Func (f, [e]) => String.isPrefix "un" f andalso matches e
adamc@1207:                        | _ => false
adamc@1207:              in
adamc@1208:                  List.exists matches (Cc.allPeers (cc, e2))
adamc@1207:              end
adamc@1207:            | _ => false)
adamc@1202:       | _ => false
adamc@1202: 
adamc@1202: fun imply (p1, p2) =
adamc@1208:     let
adamc@1208:         fun doOne doKnown =
adamc@1208:             decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1208:                    (fn hyps =>
adamc@1208:                        decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1208:                               (fn goals =>
adamc@1208:                                   let
adamc@1208:                                       val cc = foldl (fn (p, cc) =>
adamc@1208:                                                          case p of
adamc@1208:                                                              (Eq, [e1, e2]) => Cc.assert (cc, e1, e2)
adamc@1208:                                                            | _ => cc) Cc.empty hyps
adamc@1202: 
adamc@1208:                                       fun gls goals onFail =
adamc@1208:                                           case goals of
adamc@1208:                                               [] => true
adamc@1208:                                             | g :: goals =>
adamc@1208:                                               case (doKnown, g) of
adamc@1208:                                                   (false, (Known, _)) => gls goals onFail
adamc@1208:                                                 | _ =>
adamc@1208:                                                   let
adamc@1208:                                                       fun hps hyps =
adamc@1208:                                                           case hyps of
adamc@1208:                                                               [] => onFail ()
adamc@1208:                                                             | h :: hyps =>
adamc@1208:                                                               let
adamc@1208:                                                                   val saved = save ()
adamc@1208:                                                               in
adamc@1208:                                                                   if rimp cc (h, g) then
adamc@1208:                                                                       let
adamc@1208:                                                                           val changed = IM.numItems (!unif)
adamc@1208:                                                                                         <> IM.numItems saved
adamc@1208:                                                                       in
adamc@1208:                                                                           gls goals (fn () => (restore saved;
adamc@1208:                                                                                                changed andalso hps hyps))
adamc@1208:                                                                       end
adamc@1208:                                                                   else
adamc@1208:                                                                       hps hyps
adamc@1208:                                                               end
adamc@1208:                                                   in
adamc@1208:                                                       (case g of
adamc@1208:                                                            (Eq, [e1, e2]) => Cc.query (cc, e1, e2)
adamc@1208:                                                          | _ => false)
adamc@1208:                                                       orelse hps hyps
adamc@1208:                                                   end
adamc@1208:                                   in
adamc@1211:                                       if List.exists (fn (DtCon c1, [e]) =>
adamc@1211:                                                          List.exists (fn (DtCon c2, [e']) =>
adamc@1211:                                                                          c1 <> c2 andalso
adamc@1211:                                                                          Cc.query (cc, e, e')
adamc@1211:                                                                        | _ => false) hyps
adamc@1211:                                                          orelse List.exists (fn Func (c2, []) => c1 <> c2
adamc@1211:                                                                               | Finish => true
adamc@1211:                                                                               | _ => false)
adamc@1211:                                                                             (Cc.allPeers (cc, e))
adamc@1211:                                                        | _ => false) hyps
adamc@1211:                                          orelse gls goals (fn () => false) then
adamc@1211:                                           true
adamc@1211:                                       else
adamc@1211:                                           (Print.prefaces "Can't prove"
adamc@1211:                                                           [("hyps", Print.p_list (fn x => p_prop (Reln x)) hyps),
adamc@1211:                                                            ("goals", Print.p_list (fn x => p_prop (Reln x)) goals)];
adamc@1211:                                            false)
adamc@1208:                                   end))
adamc@1208:     in
adamc@1208:         reset ();
adamc@1208:         doOne false;
adamc@1208:         doOne true
adamc@1208:     end
adamc@1200: 
adamc@1200: fun patCon pc =
adamc@1200:     case pc of
adamc@1200:         PConVar n => "C" ^ Int.toString n
adamc@1200:       | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200: 
adamc@1202: 
adamc@1200: 
adamc@1200: datatype chunk =
adamc@1200:          String of string
adamc@1200:        | Exp of Mono.exp
adamc@1200: 
adamc@1200: fun chunkify e =
adamc@1200:     case #1 e of
adamc@1200:         EPrim (Prim.String s) => [String s]
adamc@1207:       | EStrcat (e1, e2) =>
adamc@1207:         let
adamc@1207:             val chs1 = chunkify e1
adamc@1207:             val chs2 = chunkify e2
adamc@1207:         in
adamc@1207:             case chs2 of
adamc@1207:                 String s2 :: chs2' =>
adamc@1207:                 (case List.last chs1 of
adamc@1207:                      String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207:                    | _ => chs1 @ chs2)
adamc@1207:               | _ => chs1 @ chs2
adamc@1207:         end
adamc@1200:       | _ => [Exp e]
adamc@1200: 
adamc@1201: type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201: 
adamc@1201: fun always v chs = SOME (v, chs)
adamc@1201: 
adamc@1202: fun parse p s =
adamc@1202:     case p (chunkify s) of
adamc@1201:         SOME (v, []) => SOME v
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1201: fun const s chs =
adamc@1201:     case chs of
adamc@1201:         String s' :: chs => if String.isPrefix s s' then
adamc@1201:                                 SOME ((), if size s = size s' then
adamc@1201:                                               chs
adamc@1201:                                           else
adamc@1201:                                               String (String.extract (s', size s, NONE)) :: chs)
adamc@1201:                             else
adamc@1201:                                 NONE
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1201: fun follow p1 p2 chs =
adamc@1201:     case p1 chs of
adamc@1201:         NONE => NONE
adamc@1201:       | SOME (v1, chs) =>
adamc@1201:         case p2 chs of
adamc@1201:             NONE => NONE
adamc@1201:           | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201: 
adamc@1201: fun wrap p f chs =
adamc@1201:     case p chs of
adamc@1201:         NONE => NONE
adamc@1201:       | SOME (v, chs) => SOME (f v, chs)
adamc@1201: 
adamc@1209: fun wrapP p f chs =
adamc@1209:     case p chs of
adamc@1209:         NONE => NONE
adamc@1209:       | SOME (v, chs) =>
adamc@1209:         case f v of
adamc@1209:             NONE => NONE
adamc@1209:           | SOME r => SOME (r, chs)
adamc@1209: 
adamc@1201: fun alt p1 p2 chs =
adamc@1201:     case p1 chs of
adamc@1201:         NONE => p2 chs
adamc@1201:       | v => v
adamc@1201: 
adamc@1207: fun altL ps =
adamc@1207:     case rev ps of
adamc@1207:         [] => (fn _ => NONE)
adamc@1207:       | p :: ps =>
adamc@1207:         foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207: 
adamc@1204: fun opt p chs =
adamc@1204:     case p chs of
adamc@1204:         NONE => SOME (NONE, chs)
adamc@1204:       | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204: 
adamc@1201: fun skip cp chs =
adamc@1201:     case chs of
adamc@1201:         String "" :: chs => skip cp chs
adamc@1201:       | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201:                                 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201:                             else
adamc@1201:                                 SOME ((), chs)
adamc@1201:       | _ => SOME ((), chs)
adamc@1201: 
adamc@1201: fun keep cp chs =
adamc@1201:     case chs of
adamc@1201:         String "" :: chs => keep cp chs
adamc@1201:       | String s :: chs' =>
adamc@1201:         let
adamc@1201:             val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201:         in
adamc@1201:             if Substring.isEmpty befor then
adamc@1201:                 NONE
adamc@1201:             else
adamc@1201:                 SOME (Substring.string befor,
adamc@1201:                       if Substring.isEmpty after then
adamc@1201:                           chs'
adamc@1201:                       else
adamc@1201:                           String (Substring.string after) :: chs')
adamc@1201:         end
adamc@1201:       | _ => NONE
adamc@1201: 
adamc@1204: fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204:                         (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204: 
adamc@1204: fun log name p chs =
adamc@1206:     (if !debug then
adamc@1206:          case chs of
adamc@1207:              String s :: _ => print (name ^ ": " ^ s ^ "\n")
adamc@1206:            | _ => print (name ^ ": blocked!\n")
adamc@1206:      else
adamc@1206:          ();
adamc@1204:      p chs)
adamc@1201: 
adamc@1201: fun list p chs =
adamc@1207:     altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207:                (fn (v, ((), ls)) => v :: ls),
adamc@1207:           wrap (ws p) (fn v => [v]),
adamc@1207:           always []] chs
adamc@1201: 
adamc@1201: val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201: 
adamc@1211: val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211:                                        SOME (String.extract (s, 2, NONE))
adamc@1201:                                    else
adamc@1211:                                        NONE)
adamc@1211: val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211:                                         SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211:                                               ^ String.extract (s, 4, NONE))
adamc@1211:                                     else
adamc@1211:                                         NONE)
adamc@1201: 
adamc@1211: val field = wrap (follow t_ident
adamc@1201:                          (follow (const ".")
adamc@1201:                                  uw_ident))
adamc@1201:                  (fn (t, ((), f)) => (t, f))
adamc@1201: 
adamc@1206: datatype Rel =
adamc@1206:          Exps of exp * exp -> prop
adamc@1206:        | Props of prop * prop -> prop
adamc@1206: 
adamc@1204: datatype sqexp =
adamc@1206:          SqConst of Prim.t
adamc@1206:        | Field of string * string
adamc@1206:        | Binop of Rel * sqexp * sqexp
adamc@1207:        | SqKnown of sqexp
adamc@1207:        | Inj of Mono.exp
adamc@1211:        | SqFunc of string * sqexp
adamc@1211:        | Count
adamc@1204: 
adamc@1210: fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210: 
adamc@1210: val sqbrel = altL [cmp "=" Eq,
adamc@1210:                    cmp "<>" Ne,
adamc@1210:                    cmp "<=" Le,
adamc@1210:                    cmp "<" Lt,
adamc@1210:                    cmp ">=" Ge,
adamc@1210:                    cmp ">" Gt,
adamc@1207:                    wrap (const "AND") (fn () => Props And),
adamc@1207:                    wrap (const "OR") (fn () => Props Or)]
adamc@1204: 
adamc@1204: datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204: 
adamc@1209: fun string chs =
adamc@1206:     case chs of
adamc@1209:         String s :: chs =>
adamc@1209:         if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209:             let
adamc@1209:                 fun loop (cs, acc) =
adamc@1209:                     case cs of
adamc@1209:                         [] => NONE
adamc@1209:                       | c :: cs =>
adamc@1209:                         if c = #"'" then
adamc@1209:                             SOME (String.implode (rev acc), cs)
adamc@1209:                         else if c = #"\\" then
adamc@1209:                             case cs of
adamc@1209:                                 c :: cs => loop (cs, c :: acc)
adamc@1209:                               | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209:                         else
adamc@1209:                             loop (cs, c :: acc)
adamc@1209:             in
adamc@1209:                 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209:                     NONE => NONE
adamc@1209:                   | SOME (s, []) => SOME (s, chs)
adamc@1209:                   | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209:             end
adamc@1209:         else
adamc@1209:             NONE
adamc@1209:       | _ => NONE                            
adamc@1206: 
adamc@1209: val prim =
adamc@1209:     altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209:                               (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209:                        (opt (const "::float8"))) #1,
adamc@1209:           wrap (follow (wrapP (keep Char.isDigit)
adamc@1209:                               (Option.map Prim.Int o Int64.fromString))
adamc@1209:                        (opt (const "::int8"))) #1,
adamc@1209:           wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209:                (Prim.String o #1 o #2)]
adamc@1206: 
adamc@1207: fun known' chs =
adamc@1207:     case chs of
adamc@1207:         Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207:       | _ => NONE
adamc@1207: 
adamc@1207: fun sqlify chs =
adamc@1207:     case chs of
adamc@1207:         Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207:         if String.isPrefix "sqlify" f then
adamc@1207:             SOME (e, chs)
adamc@1207:         else
adamc@1207:             NONE
adamc@1207:       | _ => NONE
adamc@1207: 
adamc@1211: fun constK s = wrap (const s) (fn () => s)
adamc@1211: 
adamc@1211: val funcName = altL [constK "COUNT",
adamc@1211:                      constK "MIN",
adamc@1211:                      constK "MAX",
adamc@1211:                      constK "SUM",
adamc@1211:                      constK "AVG"]
adamc@1211: 
adamc@1204: fun sqexp chs =
adamc@1206:     log "sqexp"
adamc@1207:     (altL [wrap prim SqConst,
adamc@1211:            wrap field Field,
adamc@1207:            wrap known SqKnown,
adamc@1211:            wrap func SqFunc,
adamc@1211:            wrap (const "COUNT(*)") (fn () => Count),
adamc@1207:            wrap sqlify Inj,
adamc@1211:            wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211:                                                                   (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211:                 (fn ((), (e, _)) => e),
adamc@1207:            wrap (follow (ws (const "("))
adamc@1207:                         (follow (wrap
adamc@1207:                                      (follow sqexp
adamc@1207:                                              (alt
adamc@1207:                                                   (wrap
adamc@1207:                                                        (follow (ws sqbrel)
adamc@1207:                                                                (ws sqexp))
adamc@1207:                                                        inl)
adamc@1207:                                                   (always (inr ()))))
adamc@1207:                                      (fn (e1, sm) =>
adamc@1207:                                          case sm of
adamc@1207:                                              inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207:                                            | inr () => e1))
adamc@1207:                                 (const ")")))
adamc@1207:                 (fn ((), (e, ())) => e)])
adamc@1207:     chs
adamc@1206: 
adamc@1207: and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211:                      (fn ((), ((), (e, ()))) => e) chs
adamc@1211:                 
adamc@1211: and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211:                     (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211: 
adamc@1211: datatype sitem =
adamc@1211:          SqField of string * string
adamc@1211:        | SqExp of sqexp * string
adamc@1211: 
adamc@1211: val sitem = alt (wrap field SqField)
adamc@1211:             (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211:              (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207: 
adamc@1207: val select = log "select"
adamc@1207:              (wrap (follow (const "SELECT ") (list sitem))
adamc@1207:                    (fn ((), ls) => ls))
adamc@1201: 
adamc@1201: val fitem = wrap (follow uw_ident
adamc@1201:                          (follow (const " AS ")
adamc@1201:                                  t_ident))
adamc@1201:                  (fn (t, ((), f)) => (t, f))
adamc@1201: 
adamc@1207: val from = log "from"
adamc@1207:            (wrap (follow (const "FROM ") (list fitem))
adamc@1207:                  (fn ((), ls) => ls))
adamc@1201: 
adamc@1204: val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204:            (fn ((), ls) => ls)
adamc@1204: 
adamc@1207: val query = log "query"
adamc@1207:                 (wrap (follow (follow select from) (opt wher))
adamc@1207:                       (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201: 
adamc@1211: fun removeDups ls =
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@1207: fun queryProp env rv oe e =
adamc@1202:     case parse query e of
adamc@1207:         NONE => (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1207:                         ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1210:                  (Unknown, []))
adamc@1201:       | SOME r =>
adamc@1202:         let
adamc@1211:             fun usedFields e =
adamc@1211:                 case e of
adamc@1211:                     SqConst _ => []
adamc@1211:                   | Field (v, f) => [(v, f)]
adamc@1211:                   | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1211:                   | SqKnown _ => []
adamc@1211:                   | Inj _ => []
adamc@1211:                   | SqFunc (_, e) => usedFields e
adamc@1211:                   | Count => []
adamc@1211: 
adamc@1211:             val allUsed = removeDups (List.mapPartial (fn SqField x => SOME x | _ => NONE) (#Select r)
adamc@1211:                                       @ (case #Where r of
adamc@1211:                                              NONE => []
adamc@1211:                                            | SOME e => usedFields e))
adamc@1211: 
adamc@1202:             val p =
adamc@1202:                 foldl (fn ((t, v), p) =>
adamc@1202:                           And (p,
adamc@1202:                                Reln (Sql t,
adamc@1202:                                      [Recd (foldl (fn ((v', f), fs) =>
adamc@1202:                                                       if v' = v then
adamc@1202:                                                           (f, Proj (Proj (Lvar rv, v), f)) :: fs
adamc@1202:                                                       else
adamc@1211:                                                           fs) [] allUsed)])))
adamc@1202:                       True (#From r)
adamc@1205: 
adamc@1205:             fun expIn e =
adamc@1205:                 case e of
adamc@1206:                     SqConst p => inl (Const p)
adamc@1206:                   | Field (v, f) => inl (Proj (Proj (Lvar rv, v), f))
adamc@1205:                   | Binop (bo, e1, e2) =>
adamc@1206:                     inr (case (bo, expIn e1, expIn e2) of
adamc@1206:                              (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1206:                            | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1206:                            | _ => Unknown)
adamc@1207:                   | SqKnown e =>
adamc@1207:                     inr (case expIn e of
adamc@1207:                              inl e => Reln (Known, [e])
adamc@1207:                            | _ => Unknown)
adamc@1207:                   | Inj e =>
adamc@1207:                     let
adamc@1207:                         fun deinj (e, _) =
adamc@1207:                             case e of
adamc@1207:                                 ERel n => List.nth (env, n)
adamc@1207:                               | EField (e, f) => Proj (deinj e, f)
adamc@1207:                               | _ => raise Fail "Iflow: non-variable injected into query"
adamc@1207:                     in
adamc@1207:                         inl (deinj e)
adamc@1207:                     end
adamc@1211:                   | SqFunc (f, e) =>
adamc@1211:                     inl (case expIn e of
adamc@1211:                          inl e => Func (f, [e])
adamc@1211:                        | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
adamc@1211:                   | Count => inl (Func ("COUNT", []))
adamc@1210: 
adamc@1205:             val p = case #Where r of
adamc@1205:                         NONE => p
adamc@1205:                       | SOME e =>
adamc@1205:                         case expIn e of
adamc@1205:                             inr p' => And (p, p')
adamc@1205:                           | _ => p
adamc@1202:         in
adamc@1210:             (case oe of
adamc@1210:                  NONE => p
adamc@1210:                | SOME oe =>
adamc@1211:                  And (p, foldl (fn (si, p) =>
adamc@1211:                                    let
adamc@1211:                                        val p' = case si of
adamc@1211:                                                     SqField (v, f) => Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])
adamc@1211:                                                   | SqExp (e, f) =>
adamc@1211:                                                     case expIn e of
adamc@1211:                                                         inr _ => Unknown
adamc@1211:                                                       | inl e => Reln (Eq, [oe, e])
adamc@1211:                                    in
adamc@1211:                                        Or (p, p')
adamc@1211:                                    end)
adamc@1210:                                False (#Select r)),
adamc@1210:              
adamc@1210:              case #Where r of
adamc@1210:                  NONE => []
adamc@1211:                | SOME e => map (fn (v, f) => Proj (Proj (Lvar rv, v), f)) (usedFields e))
adamc@1202:         end
adamc@1200: 
adamc@1211: fun evalPat env e (pt, _) =
adamc@1211:     case pt of
adamc@1211:         PWild => (env, True)
adamc@1211:       | PVar _ => (e :: env, True)
adamc@1211:       | PPrim _ => (env, True)
adamc@1211:       | PCon (_, pc, NONE) => (env, Reln (DtCon (patCon pc), [e]))
adamc@1211:       | PCon (_, pc, SOME pt) =>
adamc@1211:         let
adamc@1211:             val (env, p) = evalPat env (Func ("un" ^ patCon pc, [e])) pt
adamc@1211:         in
adamc@1211:             (env, And (p, Reln (DtCon (patCon pc), [e])))
adamc@1211:         end
adamc@1211:       | PRecord xpts =>
adamc@1211:         foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211:                   let
adamc@1211:                       val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211:                   in
adamc@1211:                       (env, And (p', p))
adamc@1211:                   end) (env, True) xpts
adamc@1211:       | PNone _ => (env, Reln (DtCon "None", [e]))
adamc@1211:       | PSome (_, pt) =>
adamc@1211:         let
adamc@1211:             val (env, p) = evalPat env (Func ("unSome", [e])) pt
adamc@1211:         in
adamc@1211:             (env, And (p, Reln (DtCon "Some", [e])))
adamc@1211:         end
adamc@1211: 
adamc@1211: fun peq (p1, p2) =
adamc@1211:     case (p1, p2) of
adamc@1211:         (True, True) => true
adamc@1211:       | (False, False) => true
adamc@1211:       | (Unknown, Unknown) => true
adamc@1211:       | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211:       | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211:       | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211:       | (Select (n1, n2, n3, p1, e1), Select (n1', n2', n3', p2, e2)) =>
adamc@1211:         n1 = n1' andalso n2 = n2' andalso n3 = n3'
adamc@1211:         andalso peq (p1, p2) andalso eeq (e1, e2)
adamc@1211:       | _ => false
adamc@1211: 
adamc@1211: fun removeRedundant p1 =
adamc@1211:     let
adamc@1211:         fun rr p2 =
adamc@1211:             if peq (p1, p2) then
adamc@1211:                 True
adamc@1211:             else
adamc@1211:                 case p2 of
adamc@1211:                     And (x, y) => And (rr x, rr y)
adamc@1211:                   | Or (x, y) => Or (rr x, rr y)
adamc@1211:                   | Select (n1, n2, n3, p, e) => Select (n1, n2, n3, rr p, e)
adamc@1211:                   | _ => p2
adamc@1211:     in
adamc@1211:         rr
adamc@1211:     end
adamc@1211: 
adamc@1202: fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
adamc@1200:     let
adamc@1200:         fun default () =
adamc@1200:             (Var nv, (nv+1, p, sent))
adamc@1200: 
adamc@1200:         fun addSent (p, e, sent) =
adamc@1200:             if isKnown e then
adamc@1200:                 sent
adamc@1200:             else
adamc@1202:                 (loc, e, p) :: sent
adamc@1200:     in
adamc@1200:         case #1 e of
adamc@1200:             EPrim p => (Const p, st)
adamc@1200:           | ERel n => (List.nth (env, n), st)
adamc@1200:           | ENamed _ => default ()
adamc@1200:           | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200:           | ECon (_, pc, SOME e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func (patCon pc, [e]), st)
adamc@1200:             end
adamc@1200:           | ENone _ => (Func ("None", []), st)
adamc@1200:           | ESome (_, e) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func ("Some", [e]), st)
adamc@1200:             end
adamc@1200:           | EFfi _ => default ()
adamc@1200:           | EFfiApp (m, s, es) =>
adamc@1200:             if m = "Basis" andalso SS.member (writers, s) then
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1200:                     (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200:                 end
adamc@1200:             else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200:                 default ()
adamc@1200:             else
adamc@1200:                 let
adamc@1200:                     val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:                 in
adamc@1200:                     (Func (m ^ "." ^ s, es), st)
adamc@1200:                 end
adamc@1200:           | EApp _ => default ()
adamc@1200:           | EAbs _ => default ()
adamc@1200:           | EUnop (s, e1) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 (Func (s, [e1]), st)
adamc@1200:             end
adamc@1200:           | EBinop (s, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1200:                 (Func (s, [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | ERecord xets =>
adamc@1200:             let
adamc@1200:                 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200:                                                       let
adamc@1200:                                                           val (e, st) = evalExp env (e, st)
adamc@1200:                                                       in
adamc@1200:                                                           ((x, e), st)
adamc@1200:                                                       end) st xets
adamc@1200:             in
adamc@1200:                 (Recd xes, st)
adamc@1200:             end
adamc@1200:           | EField (e, s) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Proj (e, s), st)
adamc@1200:             end
adamc@1211:           | ECase (e, pes, _) =>
adamc@1211:             let
adamc@1211:                 val (e, st) = evalExp env (e, st)
adamc@1211:                 val r = #1 st
adamc@1211:                 val st = (r + 1, #2 st, #3 st)
adamc@1211:                 val orig = #2 st
adamc@1211: 
adamc@1211:                 val st = foldl (fn ((pt, pe), st) =>
adamc@1211:                                    let
adamc@1211:                                        val (env, pp) = evalPat env e pt
adamc@1211:                                        val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st))
adamc@1211:                                                        
adamc@1211:                                        val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe]))
adamc@1211:                                    in
adamc@1211:                                        (#1 st', Or (#2 st, this), #3 st')
adamc@1211:                                    end) (#1 st, False, #3 st) pes
adamc@1211:             in
adamc@1211:                 (Var r, (#1 st, And (orig, #2 st), #3 st))
adamc@1211:             end
adamc@1200:           | EStrcat (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:                 val (e2, st) = evalExp env (e2, st)
adamc@1200:             in
adamc@1200:                 (Func ("cat", [e1, e2]), st)
adamc@1200:             end
adamc@1200:           | EError _ => (Finish, st)
adamc@1200:           | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200:             let
adamc@1200:                 val (b, st) = evalExp env (b, st)
adamc@1200:                 val (m, st) = evalExp env (m, st)
adamc@1200:             in
adamc@1200:                 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200:             end
adamc@1200:           | ERedirect (e, _) =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200:             end
adamc@1200:           | EWrite e =>
adamc@1200:             let
adamc@1200:                 val (e, st) = evalExp env (e, st)
adamc@1200:             in
adamc@1200:                 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200:             end
adamc@1200:           | ESeq (e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp env (e2, st)
adamc@1200:             end
adamc@1200:           | ELet (_, _, e1, e2) =>
adamc@1200:             let
adamc@1200:                 val (e1, st) = evalExp env (e1, st)
adamc@1200:             in
adamc@1200:                 evalExp (e1 :: env) (e2, st)
adamc@1200:             end
adamc@1200:           | EClosure (n, es) =>
adamc@1200:             let
adamc@1200:                 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200:             in
adamc@1200:                 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200:             end
adamc@1200: 
adamc@1200:           | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200:             let
adamc@1200:                 val (_, st) = evalExp env (q, st)
adamc@1200:                 val (i, st) = evalExp env (i, st)
adamc@1200: 
adamc@1200:                 val r = #1 st
adamc@1200:                 val acc = #1 st + 1
adamc@1200:                 val st' = (#1 st + 2, #2 st, #3 st)
adamc@1200: 
adamc@1200:                 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200: 
adamc@1200:                 val r' = newLvar ()
adamc@1200:                 val acc' = newLvar ()
adamc@1210:                 val (qp, used) = queryProp env r' NONE q
adamc@1200: 
adamc@1200:                 val doSubExp = subExp (r, r') o subExp (acc, acc')
adamc@1200:                 val doSubProp = subProp (r, r') o subProp (acc, acc')
adamc@1200: 
adamc@1200:                 val p = doSubProp (#2 st')
adamc@1210:                 val p' = And (p, qp)
adamc@1210:                 val p = Select (r, r', acc', p', doSubExp b)
adamc@1210: 
adamc@1210:                 val sent = map (fn (loc, e, p) => (loc,
adamc@1210:                                                    doSubExp e,
adamc@1210:                                                    And (qp, doSubProp p))) (#3 st')
adamc@1210:                 val sent = map (fn e => (loc, e, p')) used @ sent
adamc@1200:             in
adamc@1210:                 (Var r, (#1 st + 1, And (#2 st, p), sent))
adamc@1200:             end
adamc@1200:           | EDml _ => default ()
adamc@1200:           | ENextval _ => default ()
adamc@1200:           | ESetval _ => default ()
adamc@1200: 
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@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@1202:         fun decl ((d, _), (vals, pols)) =
adamc@1200:             case d of
adamc@1207:                 DVal (_, n, _, e, _) =>
adamc@1200:                 let
adamc@1207:                     val isExptd = IS.member (exptd, n)
adamc@1207: 
adamc@1207:                     fun deAbs (e, env, nv, p) =
adamc@1200:                         case #1 e of
adamc@1207:                             EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207:                                                         if isExptd then
adamc@1207:                                                             And (p, Reln (Known, [Var nv]))
adamc@1207:                                                         else
adamc@1207:                                                             p)
adamc@1207:                           | _ => (e, env, nv, p)
adamc@1200: 
adamc@1207:                     val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200: 
adamc@1207:                     val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
adamc@1200:                 in
adamc@1207:                     (sent @ vals, pols)
adamc@1200:                 end
adamc@1202: 
adamc@1210:               | DPolicy (PolQuery e) => (vals, #1 (queryProp [] 0 (SOME (Var 0)) e) :: pols)
adamc@1202: 
adamc@1202:               | _ => (vals, pols)
adamc@1202: 
adamc@1203:         val () = reset ()
adamc@1202: 
adamc@1202:         val (vals, pols) = foldl decl ([], []) file
adamc@1200:     in
adamc@1207:         app (fn (loc, e, p) =>
adamc@1207:                 let
adamc@1207:                     val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1207:                 in
adamc@1208:                     if List.exists (fn pol => if imply (p, pol) then
adamc@1208:                                                   (if !debug then
adamc@1208:                                                        Print.prefaces "Match"
adamc@1208:                                                        [("Hyp", p_prop p),
adamc@1208:                                                         ("Goal", p_prop pol)]
adamc@1208:                                                    else
adamc@1208:                                                        ();
adamc@1208:                                                    true)
adamc@1208:                                               else
adamc@1208:                                                   false) pols then
adamc@1207:                         ()
adamc@1207:                     else
adamc@1207:                         (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1207:                          Print.preface ("The state satisifes this predicate:", p_prop p))
adamc@1207:                 end) vals
adamc@1200:     end
adamc@1200: 
adamc@1200: end