Ur/Web: src/iflow.sml annotate

annotate src/iflow.sml @ 1232:efbefd6e3f6c

When applying multiple policies at once, filter the policy set at the beginning, removing unmatchable policies

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 13 Apr 2010 09:31:04 -0400
parents	5fa8ae2a34e3
children	8d1d2f7163c2

rev	line source
adamc@1200	1 (* Copyright (c) 2010, Adam Chlipala
adamc@1200	2 * All rights reserved.
adamc@1200	3 *
adamc@1200	4 * Redistribution and use in source and binary forms, with or without
adamc@1200	5 * modification, are permitted provided that the following conditions are met:
adamc@1200	6 *
adamc@1200	7 * - Redistributions of source code must retain the above copyright notice,
adamc@1200	8 * this list of conditions and the following disclaimer.
adamc@1200	9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200	10 * this list of conditions and the following disclaimer in the documentation
adamc@1200	11 * and/or other materials provided with the distribution.
adamc@1200	12 * - The names of contributors may not be used to endorse or promote products
adamc@1200	13 * derived from this software without specific prior written permission.
adamc@1200	14 *
adamc@1200	15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200	16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200	17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200	18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200	19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@1200	20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200	21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200	22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200	23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200	24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200	25 * POSSIBILITY OF SUCH DAMAGE.
adamc@1200	26 *)
adamc@1200	27
adamc@1200	28 structure Iflow :> IFLOW = struct
adamc@1200	29
adamc@1200	30 open Mono
adamc@1200	31
adamc@1207	32 structure IS = IntBinarySet
adamc@1202	33 structure IM = IntBinaryMap
adamc@1202	34
adamc@1215	35 structure SK = struct
adamc@1215	36 type ord_key = string
adamc@1215	37 val compare = String.compare
adamc@1215	38 end
adamc@1215	39
adamc@1215	40 structure SS = BinarySetFn(SK)
adamc@1215	41 structure SM = BinaryMapFn(SK)
adamc@1200	42
adamc@1200	43 val writers = ["htmlifyInt_w",
adamc@1200	44 "htmlifyFloat_w",
adamc@1200	45 "htmlifyString_w",
adamc@1200	46 "htmlifyBool_w",
adamc@1200	47 "htmlifyTime_w",
adamc@1200	48 "attrifyInt_w",
adamc@1200	49 "attrifyFloat_w",
adamc@1200	50 "attrifyString_w",
adamc@1200	51 "attrifyChar_w",
adamc@1200	52 "urlifyInt_w",
adamc@1200	53 "urlifyFloat_w",
adamc@1200	54 "urlifyString_w",
adamc@1213	55 "urlifyBool_w",
adamc@1213	56 "set_cookie"]
adamc@1200	57
adamc@1200	58 val writers = SS.addList (SS.empty, writers)
adamc@1200	59
adamc@1200	60 type lvar = int
adamc@1200	61
adamc@1215	62 datatype func =
adamc@1215	63 DtCon0 of string
adamc@1215	64 \| DtCon1 of string
adamc@1215	65 \| UnCon of string
adamc@1215	66 \| Other of string
adamc@1215	67
adamc@1200	68 datatype exp =
adamc@1200	69 Const of Prim.t
adamc@1200	70 \| Var of int
adamc@1200	71 \| Lvar of lvar
adamc@1215	72 \| Func of func * exp list
adamc@1200	73 \| Recd of (string * exp) list
adamc@1200	74 \| Proj of exp * string
adamc@1200	75 \| Finish
adamc@1200	76
adamc@1200	77 datatype reln =
adamc@1207	78 Known
adamc@1207	79 \| Sql of string
adamc@1215	80 \| PCon0 of string
adamc@1215	81 \| PCon1 of string
adamc@1200	82 \| Eq
adamc@1210	83 \| Ne
adamc@1210	84 \| Lt
adamc@1210	85 \| Le
adamc@1210	86 \| Gt
adamc@1210	87 \| Ge
adamc@1200	88
adamc@1200	89 datatype prop =
adamc@1200	90 True
adamc@1200	91 \| False
adamc@1200	92 \| Unknown
adamc@1200	93 \| And of prop * prop
adamc@1200	94 \| Or of prop * prop
adamc@1200	95 \| Reln of reln * exp list
adamc@1212	96 \| Cond of exp * prop
adamc@1200	97
adamc@1215	98 val unif = ref (IM.empty : exp IM.map)
adamc@1215	99
adamc@1215	100 fun reset () = unif := IM.empty
adamc@1215	101 fun save () = !unif
adamc@1215	102 fun restore x = unif := x
adamc@1215	103
adamc@1200	104 local
adamc@1207	105 open Print
adamc@1207	106 val string = PD.string
adamc@1207	107 in
adamc@1207	108
adamc@1215	109 fun p_func f =
adamc@1215	110 string (case f of
adamc@1215	111 DtCon0 s => s
adamc@1215	112 \| DtCon1 s => s
adamc@1215	113 \| UnCon s => "un" ^ s
adamc@1215	114 \| Other s => s)
adamc@1215	115
adamc@1207	116 fun p_exp e =
adamc@1207	117 case e of
adamc@1207	118 Const p => Prim.p_t p
adamc@1207	119 \| Var n => string ("x" ^ Int.toString n)
adamc@1215	120 \| Lvar n =>
adamc@1215	121 (case IM.find (!unif, n) of
adamc@1215	122 NONE => string ("X" ^ Int.toString n)
adamc@1215	123 \| SOME e => p_exp e)
adamc@1215	124 \| Func (f, es) => box [p_func f,
adamc@1215	125 string "(",
adamc@1207	126 p_list p_exp es,
adamc@1207	127 string ")"]
adamc@1207	128 \| Recd xes => box [string "{",
adamc@1210	129 p_list (fn (x, e) => box [string x,
adamc@1207	130 space,
adamc@1207	131 string "=",
adamc@1207	132 space,
adamc@1207	133 p_exp e]) xes,
adamc@1207	134 string "}"]
adamc@1207	135 \| Proj (e, x) => box [p_exp e,
adamc@1207	136 string ("." ^ x)]
adamc@1207	137 \| Finish => string "FINISH"
adamc@1207	138
adamc@1210	139 fun p_bop s es =
adamc@1210	140 case es of
adamc@1210	141 [e1, e2] => box [p_exp e1,
adamc@1210	142 space,
adamc@1210	143 string s,
adamc@1210	144 space,
adamc@1210	145 p_exp e2]
adamc@1210	146 \| _ => raise Fail "Iflow.p_bop"
adamc@1210	147
adamc@1207	148 fun p_reln r es =
adamc@1207	149 case r of
adamc@1207	150 Known =>
adamc@1207	151 (case es of
adamc@1207	152 [e] => box [string "known(",
adamc@1207	153 p_exp e,
adamc@1207	154 string ")"]
adamc@1207	155 \| _ => raise Fail "Iflow.p_reln: Known")
adamc@1207	156 \| Sql s => box [string (s ^ "("),
adamc@1207	157 p_list p_exp es,
adamc@1207	158 string ")"]
adamc@1215	159 \| PCon0 s => box [string (s ^ "("),
adamc@1215	160 p_list p_exp es,
adamc@1215	161 string ")"]
adamc@1215	162 \| PCon1 s => box [string (s ^ "("),
adamc@1211	163 p_list p_exp es,
adamc@1211	164 string ")"]
adamc@1210	165 \| Eq => p_bop "=" es
adamc@1210	166 \| Ne => p_bop "<>" es
adamc@1210	167 \| Lt => p_bop "<" es
adamc@1210	168 \| Le => p_bop "<=" es
adamc@1210	169 \| Gt => p_bop ">" es
adamc@1210	170 \| Ge => p_bop ">=" es
adamc@1207	171
adamc@1207	172 fun p_prop p =
adamc@1207	173 case p of
adamc@1207	174 True => string "True"
adamc@1207	175 \| False => string "False"
adamc@1207	176 \| Unknown => string "??"
adamc@1207	177 \| And (p1, p2) => box [string "(",
adamc@1207	178 p_prop p1,
adamc@1207	179 string ")",
adamc@1207	180 space,
adamc@1207	181 string "&&",
adamc@1207	182 space,
adamc@1207	183 string "(",
adamc@1207	184 p_prop p2,
adamc@1207	185 string ")"]
adamc@1207	186 \| Or (p1, p2) => box [string "(",
adamc@1207	187 p_prop p1,
adamc@1207	188 string ")",
adamc@1207	189 space,
adamc@1207	190 string "\|\|",
adamc@1207	191 space,
adamc@1207	192 string "(",
adamc@1207	193 p_prop p2,
adamc@1207	194 string ")"]
adamc@1207	195 \| Reln (r, es) => p_reln r es
adamc@1212	196 \| Cond (e, p) => box [string "(",
adamc@1212	197 p_exp e,
adamc@1212	198 space,
adamc@1212	199 string "==",
adamc@1212	200 space,
adamc@1212	201 p_prop p,
adamc@1212	202 string ")"]
adamc@1207	203
adamc@1207	204 end
adamc@1207	205
adamc@1207	206 local
adamc@1202	207 val count = ref 1
adamc@1200	208 in
adamc@1200	209 fun newLvar () =
adamc@1200	210 let
adamc@1200	211 val n = !count
adamc@1200	212 in
adamc@1200	213 count := n + 1;
adamc@1200	214 n
adamc@1200	215 end
adamc@1200	216 end
adamc@1200	217
adamc@1200	218 fun isKnown e =
adamc@1200	219 case e of
adamc@1200	220 Const _ => true
adamc@1200	221 \| Func (_, es) => List.all isKnown es
adamc@1200	222 \| Recd xes => List.all (isKnown o #2) xes
adamc@1200	223 \| Proj (e, _) => isKnown e
adamc@1200	224 \| _ => false
adamc@1200	225
adamc@1200	226 fun isFinish e =
adamc@1200	227 case e of
adamc@1200	228 Finish => true
adamc@1200	229 \| _ => false
adamc@1200	230
adamc@1200	231 fun simplify e =
adamc@1200	232 case e of
adamc@1200	233 Const _ => e
adamc@1200	234 \| Var _ => e
adamc@1208	235 \| Lvar n =>
adamc@1208	236 (case IM.find (!unif, n) of
adamc@1208	237 NONE => e
adamc@1208	238 \| SOME e => simplify e)
adamc@1215	239 \| Func (f, es) => Func (f, map simplify es)
adamc@1215	240 \| Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
adamc@1215	241 \| Proj (e, s) => Proj (simplify e, s)
adamc@1200	242 \| Finish => Finish
adamc@1200	243
adamc@1212	244 datatype atom =
adamc@1212	245 AReln of reln * exp list
adamc@1212	246 \| ACond of exp * prop
adamc@1212	247
adamc@1212	248 fun p_atom a =
adamc@1212	249 p_prop (case a of
adamc@1212	250 AReln x => Reln x
adamc@1212	251 \| ACond x => Cond x)
adamc@1212	252
adamc@1202	253 fun lvarIn lv =
adamc@1202	254 let
adamc@1202	255 fun lvi e =
adamc@1202	256 case e of
adamc@1202	257 Const _ => false
adamc@1202	258 \| Var _ => false
adamc@1202	259 \| Lvar lv' => lv' = lv
adamc@1202	260 \| Func (_, es) => List.exists lvi es
adamc@1202	261 \| Recd xes => List.exists (lvi o #2) xes
adamc@1202	262 \| Proj (e, _) => lvi e
adamc@1202	263 \| Finish => false
adamc@1202	264 in
adamc@1202	265 lvi
adamc@1202	266 end
adamc@1202	267
adamc@1212	268 fun lvarInP lv =
adamc@1212	269 let
adamc@1212	270 fun lvi p =
adamc@1212	271 case p of
adamc@1212	272 True => false
adamc@1212	273 \| False => false
adamc@1212	274 \| Unknown => true
adamc@1212	275 \| And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212	276 \| Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212	277 \| Reln (_, es) => List.exists (lvarIn lv) es
adamc@1212	278 \| Cond (e, p) => lvarIn lv e orelse lvi p
adamc@1212	279 in
adamc@1212	280 lvi
adamc@1212	281 end
adamc@1212	282
adamc@1212	283 fun varIn lv =
adamc@1212	284 let
adamc@1212	285 fun lvi e =
adamc@1212	286 case e of
adamc@1212	287 Const _ => false
adamc@1212	288 \| Lvar _ => false
adamc@1212	289 \| Var lv' => lv' = lv
adamc@1212	290 \| Func (_, es) => List.exists lvi es
adamc@1212	291 \| Recd xes => List.exists (lvi o #2) xes
adamc@1212	292 \| Proj (e, _) => lvi e
adamc@1212	293 \| Finish => false
adamc@1212	294 in
adamc@1212	295 lvi
adamc@1212	296 end
adamc@1212	297
adamc@1212	298 fun varInP lv =
adamc@1212	299 let
adamc@1212	300 fun lvi p =
adamc@1212	301 case p of
adamc@1212	302 True => false
adamc@1212	303 \| False => false
adamc@1212	304 \| Unknown => false
adamc@1212	305 \| And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212	306 \| Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212	307 \| Reln (_, es) => List.exists (varIn lv) es
adamc@1212	308 \| Cond (e, p) => varIn lv e orelse lvi p
adamc@1212	309 in
adamc@1212	310 lvi
adamc@1212	311 end
adamc@1212	312
adamc@1228	313 fun bumpLvars by =
adamc@1228	314 let
adamc@1228	315 fun lvi e =
adamc@1228	316 case e of
adamc@1228	317 Const _ => e
adamc@1228	318 \| Var _ => e
adamc@1228	319 \| Lvar lv => Lvar (lv + by)
adamc@1228	320 \| Func (f, es) => Func (f, map lvi es)
adamc@1228	321 \| Recd xes => Recd (map (fn (x, e) => (x, lvi e)) xes)
adamc@1228	322 \| Proj (e, f) => Proj (lvi e, f)
adamc@1228	323 \| Finish => e
adamc@1228	324 in
adamc@1228	325 lvi
adamc@1228	326 end
adamc@1228	327
adamc@1228	328 fun bumpLvarsP by =
adamc@1228	329 let
adamc@1228	330 fun lvi p =
adamc@1228	331 case p of
adamc@1228	332 True => p
adamc@1228	333 \| False => p
adamc@1228	334 \| Unknown => p
adamc@1228	335 \| And (p1, p2) => And (lvi p1, lvi p2)
adamc@1228	336 \| Or (p1, p2) => And (lvi p1, lvi p2)
adamc@1228	337 \| Reln (r, es) => Reln (r, map (bumpLvars by) es)
adamc@1228	338 \| Cond (e, p) => Cond (bumpLvars by e, lvi p)
adamc@1228	339 in
adamc@1228	340 lvi
adamc@1228	341 end
adamc@1228	342
adamc@1228	343 fun maxLvar e =
adamc@1228	344 let
adamc@1228	345 fun lvi e =
adamc@1228	346 case e of
adamc@1228	347 Const _ => 0
adamc@1228	348 \| Var _ => 0
adamc@1228	349 \| Lvar lv => lv
adamc@1228	350 \| Func (f, es) => foldl Int.max 0 (map lvi es)
adamc@1228	351 \| Recd xes => foldl Int.max 0 (map (lvi o #2) xes)
adamc@1228	352 \| Proj (e, f) => lvi e
adamc@1228	353 \| Finish => 0
adamc@1228	354 in
adamc@1228	355 lvi e
adamc@1228	356 end
adamc@1228	357
adamc@1228	358 fun maxLvarP p =
adamc@1228	359 let
adamc@1228	360 fun lvi p =
adamc@1228	361 case p of
adamc@1228	362 True => 0
adamc@1228	363 \| False => 0
adamc@1228	364 \| Unknown => 0
adamc@1228	365 \| And (p1, p2) => Int.max (lvi p1, lvi p2)
adamc@1228	366 \| Or (p1, p2) => Int.max (lvi p1, lvi p2)
adamc@1228	367 \| Reln (r, es) => foldl Int.max 0 (map maxLvar es)
adamc@1228	368 \| Cond (e, p) => Int.max (maxLvar e, lvi p)
adamc@1228	369 in
adamc@1228	370 lvi p
adamc@1228	371 end
adamc@1228	372
adamc@1202	373 fun eq' (e1, e2) =
adamc@1202	374 case (e1, e2) of
adamc@1202	375 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202	376 \| (Var n1, Var n2) => n1 = n2
adamc@1202	377
adamc@1202	378 \| (Lvar n1, _) =>
adamc@1202	379 (case IM.find (!unif, n1) of
adamc@1202	380 SOME e1 => eq' (e1, e2)
adamc@1202	381 \| NONE =>
adamc@1202	382 case e2 of
adamc@1202	383 Lvar n2 =>
adamc@1202	384 (case IM.find (!unif, n2) of
adamc@1202	385 SOME e2 => eq' (e1, e2)
adamc@1202	386 \| NONE => n1 = n2
adamc@1208	387 orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202	388 true))
adamc@1202	389 \| _ =>
adamc@1202	390 if lvarIn n1 e2 then
adamc@1202	391 false
adamc@1202	392 else
adamc@1202	393 (unif := IM.insert (!unif, n1, e2);
adamc@1202	394 true))
adamc@1202	395
adamc@1202	396 \| (_, Lvar n2) =>
adamc@1202	397 (case IM.find (!unif, n2) of
adamc@1202	398 SOME e2 => eq' (e1, e2)
adamc@1202	399 \| NONE =>
adamc@1202	400 if lvarIn n2 e1 then
adamc@1202	401 false
adamc@1202	402 else
adamc@1213	403 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
adamc@1213	404 ("e1", p_exp e1)];*)
adamc@1213	405 unif := IM.insert (!unif, n2, e1);
adamc@1202	406 true))
adamc@1202	407
adamc@1202	408 \| (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202	409 \| (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202	410 \| (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202	411 \| (Finish, Finish) => true
adamc@1202	412 \| _ => false
adamc@1202	413
adamc@1202	414 fun eq (e1, e2) =
adamc@1202	415 let
adamc@1203	416 val saved = save ()
adamc@1202	417 in
adamc@1202	418 if eq' (simplify e1, simplify e2) then
adamc@1202	419 true
adamc@1202	420 else
adamc@1203	421 (restore saved;
adamc@1202	422 false)
adamc@1202	423 end
adamc@1202	424
adamc@1208	425 val debug = ref false
adamc@1208	426
adamc@1211	427 fun eeq (e1, e2) =
adamc@1211	428 case (e1, e2) of
adamc@1211	429 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211	430 \| (Var n1, Var n2) => n1 = n2
adamc@1211	431 \| (Lvar n1, Lvar n2) => n1 = n2
adamc@1211	432 \| (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211	433 \| (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211	434 List.all (fn (x2, e2) =>
adamc@1211	435 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211	436 \| (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211	437 \| (Finish, Finish) => true
adamc@1211	438 \| _ => false
adamc@1211	439
adamc@1208	440 (* Congruence closure *)
adamc@1208	441 structure Cc :> sig
adamc@1215	442 type database
adamc@1215	443
adamc@1215	444 exception Contradiction
adamc@1215	445 exception Undetermined
adamc@1215	446
adamc@1215	447 val database : unit -> database
adamc@1215	448
adamc@1215	449 val assert : database * atom -> unit
adamc@1215	450 val check : database * atom -> bool
adamc@1215	451
adamc@1215	452 val p_database : database Print.printer
adamc@1218	453
adamc@1218	454 val builtFrom : database * {Base : exp list, Derived : exp} -> bool
adamc@1226	455
adamc@1226	456 val p_repOf : database -> exp Print.printer
adamc@1208	457 end = struct
adamc@1208	458
adamc@1215	459 exception Contradiction
adamc@1215	460 exception Undetermined
adamc@1208	461
adamc@1215	462 structure CM = BinaryMapFn(struct
adamc@1215	463 type ord_key = Prim.t
adamc@1215	464 val compare = Prim.compare
adamc@1215	465 end)
adamc@1208	466
adamc@1215	467 datatype node = Node of {Rep : node ref option ref,
adamc@1215	468 Cons : node ref SM.map ref,
adamc@1215	469 Variety : variety,
adamc@1215	470 Known : bool ref}
adamc@1208	471
adamc@1215	472 and variety =
adamc@1215	473 Dt0 of string
adamc@1215	474 \| Dt1 of string * node ref
adamc@1215	475 \| Prim of Prim.t
adamc@1221	476 \| Recrd of node ref SM.map ref * bool
adamc@1215	477 \| Nothing
adamc@1208	478
adamc@1215	479 type representative = node ref
adamc@1215	480
adamc@1215	481 type database = {Vars : representative IM.map ref,
adamc@1215	482 Consts : representative CM.map ref,
adamc@1215	483 Con0s : representative SM.map ref,
adamc@1215	484 Records : (representative SM.map * representative) list ref,
adamc@1229	485 Funcs : ((string * representative list) * representative) list ref}
adamc@1215	486
adamc@1215	487 fun database () = {Vars = ref IM.empty,
adamc@1215	488 Consts = ref CM.empty,
adamc@1215	489 Con0s = ref SM.empty,
adamc@1215	490 Records = ref [],
adamc@1215	491 Funcs = ref []}
adamc@1215	492
adamc@1215	493 fun unNode n =
adamc@1215	494 case !n of
adamc@1215	495 Node r => r
adamc@1215	496
adamc@1215	497 open Print
adamc@1215	498 val string = PD.string
adamc@1215	499 val newline = PD.newline
adamc@1215	500
adamc@1215	501 fun p_rep n =
adamc@1215	502 case !(#Rep (unNode n)) of
adamc@1215	503 SOME n => p_rep n
adamc@1215	504 \| NONE =>
adamc@1221	505 box [string (Int.toString (Unsafe.cast n) ^ ":"),
adamc@1221	506 space,
adamc@1221	507 case #Variety (unNode n) of
adamc@1221	508 Nothing => string "?"
adamc@1221	509 \| Dt0 s => string ("Dt0(" ^ s ^ ")")
adamc@1221	510 \| Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
adamc@1221	511 space,
adamc@1221	512 p_rep n,
adamc@1221	513 string ")"]
adamc@1221	514 \| Prim p => Prim.p_t p
adamc@1221	515 \| Recrd (ref m, b) => box [string "{",
adamc@1221	516 p_list (fn (x, n) => box [string x,
adamc@1221	517 space,
adamc@1221	518 string "=",
adamc@1221	519 space,
adamc@1221	520 p_rep n]) (SM.listItemsi m),
adamc@1221	521 string "}",
adamc@1221	522 if b then
adamc@1221	523 box [space,
adamc@1221	524 string "(complete)"]
adamc@1221	525 else
adamc@1226	526 box []]]
adamc@1215	527
adamc@1215	528 fun p_database (db : database) =
adamc@1215	529 box [string "Vars:",
adamc@1215	530 newline,
adamc@1215	531 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
adamc@1215	532 space,
adamc@1215	533 string "=",
adamc@1215	534 space,
adamc@1218	535 p_rep n,
adamc@1218	536 if !(#Known (unNode n)) then
adamc@1218	537 box [space,
adamc@1218	538 string "(known)"]
adamc@1218	539 else
adamc@1218	540 box []]) (IM.listItemsi (!(#Vars db)))]
adamc@1215	541
adamc@1215	542 fun repOf (n : representative) : representative =
adamc@1215	543 case !(#Rep (unNode n)) of
adamc@1215	544 NONE => n
adamc@1215	545 \| SOME r =>
adamc@1215	546 let
adamc@1215	547 val r = repOf r
adamc@1215	548 in
adamc@1215	549 #Rep (unNode n) := SOME r;
adamc@1215	550 r
adamc@1215	551 end
adamc@1215	552
adamc@1215	553 fun markKnown r =
adamc@1221	554 let
adamc@1221	555 val r = repOf r
adamc@1221	556 in
adamc@1221	557 (Print.preface ("markKnown", p_rep r);)
adamc@1221	558 if !(#Known (unNode r)) then
adamc@1221	559 ()(TextIO.print "Already known\n")
adamc@1221	560 else
adamc@1221	561 (#Known (unNode r) := true;
adamc@1221	562 SM.app markKnown (!(#Cons (unNode r)));
adamc@1221	563 case #Variety (unNode r) of
adamc@1221	564 Dt1 (_, r) => markKnown r
adamc@1221	565 \| Recrd (xes, _) => SM.app markKnown (!xes)
adamc@1221	566 \| _ => ())
adamc@1221	567 end
adamc@1215	568
adamc@1215	569 fun representative (db : database, e) =
adamc@1208	570 let
adamc@1215	571 fun rep e =
adamc@1215	572 case e of
adamc@1215	573 Const p => (case CM.find (!(#Consts db), p) of
adamc@1215	574 SOME r => repOf r
adamc@1215	575 \| NONE =>
adamc@1215	576 let
adamc@1215	577 val r = ref (Node {Rep = ref NONE,
adamc@1215	578 Cons = ref SM.empty,
adamc@1215	579 Variety = Prim p,
adamc@1219	580 Known = ref true})
adamc@1215	581 in
adamc@1215	582 #Consts db := CM.insert (!(#Consts db), p, r);
adamc@1215	583 r
adamc@1215	584 end)
adamc@1215	585 \| Var n => (case IM.find (!(#Vars db), n) of
adamc@1215	586 SOME r => repOf r
adamc@1215	587 \| NONE =>
adamc@1215	588 let
adamc@1215	589 val r = ref (Node {Rep = ref NONE,
adamc@1215	590 Cons = ref SM.empty,
adamc@1215	591 Variety = Nothing,
adamc@1215	592 Known = ref false})
adamc@1215	593 in
adamc@1215	594 #Vars db := IM.insert (!(#Vars db), n, r);
adamc@1215	595 r
adamc@1215	596 end)
adamc@1215	597 \| Lvar n =>
adamc@1215	598 (case IM.find (!unif, n) of
adamc@1215	599 NONE => raise Undetermined
adamc@1215	600 \| SOME e => rep e)
adamc@1215	601 \| Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
adamc@1215	602 SOME r => repOf r
adamc@1215	603 \| NONE =>
adamc@1215	604 let
adamc@1215	605 val r = ref (Node {Rep = ref NONE,
adamc@1215	606 Cons = ref SM.empty,
adamc@1215	607 Variety = Dt0 f,
adamc@1218	608 Known = ref true})
adamc@1215	609 in
adamc@1215	610 #Con0s db := SM.insert (!(#Con0s db), f, r);
adamc@1215	611 r
adamc@1215	612 end)
adamc@1215	613 \| Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
adamc@1215	614 \| Func (DtCon1 f, [e]) =>
adamc@1215	615 let
adamc@1215	616 val r = rep e
adamc@1215	617 in
adamc@1215	618 case SM.find (!(#Cons (unNode r)), f) of
adamc@1215	619 SOME r => repOf r
adamc@1215	620 \| NONE =>
adamc@1215	621 let
adamc@1215	622 val r' = ref (Node {Rep = ref NONE,
adamc@1215	623 Cons = ref SM.empty,
adamc@1215	624 Variety = Dt1 (f, r),
adamc@1221	625 Known = ref (!(#Known (unNode r)))})
adamc@1215	626 in
adamc@1215	627 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
adamc@1215	628 r'
adamc@1215	629 end
adamc@1215	630 end
adamc@1215	631 \| Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
adamc@1215	632 \| Func (UnCon f, [e]) =>
adamc@1215	633 let
adamc@1215	634 val r = rep e
adamc@1215	635 in
adamc@1215	636 case #Variety (unNode r) of
adamc@1215	637 Dt1 (f', n) => if f' = f then
adamc@1215	638 repOf n
adamc@1215	639 else
adamc@1215	640 raise Contradiction
adamc@1215	641 \| Nothing =>
adamc@1215	642 let
adamc@1215	643 val cons = ref SM.empty
adamc@1215	644 val r' = ref (Node {Rep = ref NONE,
adamc@1215	645 Cons = cons,
adamc@1215	646 Variety = Nothing,
adamc@1221	647 Known = ref (!(#Known (unNode r)))})
adamc@1215	648
adamc@1215	649 val r'' = ref (Node {Rep = ref NONE,
adamc@1215	650 Cons = #Cons (unNode r),
adamc@1215	651 Variety = Dt1 (f, r'),
adamc@1215	652 Known = #Known (unNode r)})
adamc@1215	653 in
adamc@1215	654 cons := SM.insert (!cons, f, r'');
adamc@1215	655 #Rep (unNode r) := SOME r'';
adamc@1215	656 r'
adamc@1215	657 end
adamc@1215	658 \| _ => raise Contradiction
adamc@1215	659 end
adamc@1215	660 \| Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
adamc@1215	661 \| Func (Other f, es) =>
adamc@1215	662 let
adamc@1215	663 val rs = map rep es
adamc@1215	664 in
adamc@1215	665 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
adamc@1215	666 NONE =>
adamc@1215	667 let
adamc@1215	668 val r = ref (Node {Rep = ref NONE,
adamc@1215	669 Cons = ref SM.empty,
adamc@1215	670 Variety = Nothing,
adamc@1215	671 Known = ref false})
adamc@1215	672 in
adamc@1215	673 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
adamc@1215	674 r
adamc@1215	675 end
adamc@1215	676 \| SOME (_, r) => repOf r
adamc@1215	677 end
adamc@1215	678 \| Recd xes =>
adamc@1215	679 let
adamc@1215	680 val xes = map (fn (x, e) => (x, rep e)) xes
adamc@1215	681 val len = length xes
adamc@1215	682 in
adamc@1215	683 case List.find (fn (xes', _) =>
adamc@1215	684 SM.numItems xes' = len
adamc@1215	685 andalso List.all (fn (x, n) =>
adamc@1215	686 case SM.find (xes', x) of
adamc@1215	687 NONE => false
adamc@1215	688 \| SOME n' => n = repOf n') xes)
adamc@1215	689 (!(#Records db)) of
adamc@1215	690 SOME (_, r) => repOf r
adamc@1215	691 \| NONE =>
adamc@1215	692 let
adamc@1215	693 val xes = foldl SM.insert' SM.empty xes
adamc@1215	694
adamc@1215	695 val r' = ref (Node {Rep = ref NONE,
adamc@1215	696 Cons = ref SM.empty,
adamc@1221	697 Variety = Recrd (ref xes, true),
adamc@1215	698 Known = ref false})
adamc@1215	699 in
adamc@1215	700 #Records db := (xes, r') :: (!(#Records db));
adamc@1215	701 r'
adamc@1215	702 end
adamc@1215	703 end
adamc@1215	704 \| Proj (e, f) =>
adamc@1215	705 let
adamc@1215	706 val r = rep e
adamc@1215	707 in
adamc@1215	708 case #Variety (unNode r) of
adamc@1221	709 Recrd (xes, _) =>
adamc@1215	710 (case SM.find (!xes, f) of
adamc@1215	711 SOME r => repOf r
adamc@1216	712 \| NONE => let
adamc@1215	713 val r = ref (Node {Rep = ref NONE,
adamc@1215	714 Cons = ref SM.empty,
adamc@1215	715 Variety = Nothing,
adamc@1221	716 Known = ref (!(#Known (unNode r)))})
adamc@1215	717 in
adamc@1215	718 xes := SM.insert (!xes, f, r);
adamc@1215	719 r
adamc@1215	720 end)
adamc@1215	721 \| Nothing =>
adamc@1215	722 let
adamc@1215	723 val r' = ref (Node {Rep = ref NONE,
adamc@1215	724 Cons = ref SM.empty,
adamc@1215	725 Variety = Nothing,
adamc@1221	726 Known = ref (!(#Known (unNode r)))})
adamc@1215	727
adamc@1215	728 val r'' = ref (Node {Rep = ref NONE,
adamc@1215	729 Cons = #Cons (unNode r),
adamc@1221	730 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
adamc@1215	731 Known = #Known (unNode r)})
adamc@1215	732 in
adamc@1215	733 #Rep (unNode r) := SOME r'';
adamc@1215	734 r'
adamc@1215	735 end
adamc@1215	736 \| _ => raise Contradiction
adamc@1215	737 end
adamc@1226	738 \| Finish => raise Contradiction
adamc@1208	739 in
adamc@1215	740 rep e
adamc@1208	741 end
adamc@1208	742
adamc@1226	743 fun p_repOf db e = p_rep (representative (db, e))
adamc@1226	744
adamc@1215	745 fun assert (db, a) =
adamc@1215	746 case a of
adamc@1215	747 ACond _ => ()
adamc@1215	748 \| AReln x =>
adamc@1215	749 case x of
adamc@1221	750 (Known, [e]) =>
adamc@1221	751 ((*Print.prefaces "Before" [("e", p_exp e),
adamc@1221	752 ("db", p_database db)];*)
adamc@1221	753 markKnown (representative (db, e))(*;
adamc@1221	754 Print.prefaces "After" [("e", p_exp e),
adamc@1221	755 ("db", p_database db)]*))
adamc@1215	756 \| (PCon0 f, [e]) =>
adamc@1215	757 let
adamc@1215	758 val r = representative (db, e)
adamc@1215	759 in
adamc@1215	760 case #Variety (unNode r) of
adamc@1215	761 Dt0 f' => if f = f' then
adamc@1215	762 ()
adamc@1215	763 else
adamc@1215	764 raise Contradiction
adamc@1215	765 \| Nothing =>
adamc@1215	766 let
adamc@1215	767 val r' = ref (Node {Rep = ref NONE,
adamc@1215	768 Cons = ref SM.empty,
adamc@1215	769 Variety = Dt0 f,
adamc@1215	770 Known = ref false})
adamc@1215	771 in
adamc@1215	772 #Rep (unNode r) := SOME r'
adamc@1215	773 end
adamc@1215	774 \| _ => raise Contradiction
adamc@1215	775 end
adamc@1215	776 \| (PCon1 f, [e]) =>
adamc@1215	777 let
adamc@1215	778 val r = representative (db, e)
adamc@1215	779 in
adamc@1215	780 case #Variety (unNode r) of
adamc@1215	781 Dt1 (f', e') => if f = f' then
adamc@1215	782 ()
adamc@1215	783 else
adamc@1215	784 raise Contradiction
adamc@1215	785 \| Nothing =>
adamc@1215	786 let
adamc@1215	787 val r'' = ref (Node {Rep = ref NONE,
adamc@1215	788 Cons = ref SM.empty,
adamc@1215	789 Variety = Nothing,
adamc@1215	790 Known = ref false})
adamc@1214	791
adamc@1215	792 val r' = ref (Node {Rep = ref NONE,
adamc@1215	793 Cons = ref SM.empty,
adamc@1215	794 Variety = Dt1 (f, r''),
adamc@1215	795 Known = ref false})
adamc@1215	796 in
adamc@1215	797 #Rep (unNode r) := SOME r'
adamc@1215	798 end
adamc@1215	799 \| _ => raise Contradiction
adamc@1215	800 end
adamc@1215	801 \| (Eq, [e1, e2]) =>
adamc@1215	802 let
adamc@1215	803 fun markEq (r1, r2) =
adamc@1226	804 let
adamc@1226	805 val r1 = repOf r1
adamc@1226	806 val r2 = repOf r2
adamc@1226	807 in
adamc@1226	808 if r1 = r2 then
adamc@1226	809 ()
adamc@1226	810 else case (#Variety (unNode r1), #Variety (unNode r2)) of
adamc@1226	811 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
adamc@1226	812 ()
adamc@1226	813 else
adamc@1226	814 raise Contradiction
adamc@1226	815 \| (Dt0 f1, Dt0 f2) => if f1 = f2 then
adamc@1226	816 ()
adamc@1226	817 else
adamc@1226	818 raise Contradiction
adamc@1226	819 \| (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
adamc@1226	820 markEq (r1, r2)
adamc@1226	821 else
adamc@1226	822 raise Contradiction
adamc@1226	823 \| (Recrd (xes1, _), Recrd (xes2, _)) =>
adamc@1226	824 let
adamc@1226	825 fun unif (xes1, xes2) =
adamc@1226	826 SM.appi (fn (x, r1) =>
adamc@1226	827 case SM.find (!xes2, x) of
adamc@1226	828 NONE => xes2 := SM.insert (!xes2, x, r1)
adamc@1226	829 \| SOME r2 => markEq (r1, r2)) (!xes1)
adamc@1226	830 in
adamc@1226	831 unif (xes1, xes2);
adamc@1226	832 unif (xes2, xes1)
adamc@1226	833 end
adamc@1226	834 \| (Nothing, _) => mergeNodes (r1, r2)
adamc@1226	835 \| (_, Nothing) => mergeNodes (r2, r1)
adamc@1226	836 \| _ => raise Contradiction
adamc@1226	837 end
adamc@1214	838
adamc@1218	839 and mergeNodes (r1, r2) =
adamc@1218	840 (#Rep (unNode r1) := SOME r2;
adamc@1218	841 if !(#Known (unNode r1)) then
adamc@1218	842 markKnown r2
adamc@1218	843 else
adamc@1218	844 ();
adamc@1218	845 if !(#Known (unNode r2)) then
adamc@1218	846 markKnown r1
adamc@1218	847 else
adamc@1218	848 ();
adamc@1218	849 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
adamc@1229	850
adamc@1218	851 compactFuncs ())
adamc@1218	852
adamc@1215	853 and compactFuncs () =
adamc@1214	854 let
adamc@1215	855 fun loop funcs =
adamc@1215	856 case funcs of
adamc@1215	857 [] => []
adamc@1215	858 \| (fr as ((f, rs), r)) :: rest =>
adamc@1215	859 let
adamc@1215	860 val rest = List.filter (fn ((f' : string, rs'), r') =>
adamc@1215	861 if f' = f
adamc@1215	862 andalso ListPair.allEq (fn (r1, r2) =>
adamc@1215	863 repOf r1 = repOf r2)
adamc@1215	864 (rs, rs') then
adamc@1215	865 (markEq (r, r');
adamc@1215	866 false)
adamc@1215	867 else
adamc@1215	868 true) rest
adamc@1215	869 in
adamc@1215	870 fr :: loop rest
adamc@1215	871 end
adamc@1214	872 in
adamc@1215	873 #Funcs db := loop (!(#Funcs db))
adamc@1214	874 end
adamc@1215	875 in
adamc@1215	876 markEq (representative (db, e1), representative (db, e2))
adamc@1215	877 end
adamc@1215	878 \| _ => ()
adamc@1214	879
adamc@1215	880 fun check (db, a) =
adamc@1215	881 case a of
adamc@1215	882 ACond _ => false
adamc@1215	883 \| AReln x =>
adamc@1215	884 case x of
adamc@1221	885 (Known, [e]) =>
adamc@1221	886 let
adamc@1221	887 fun isKnown r =
adamc@1221	888 let
adamc@1221	889 val r = repOf r
adamc@1221	890 in
adamc@1221	891 !(#Known (unNode r))
adamc@1221	892 orelse case #Variety (unNode r) of
adamc@1221	893 Dt1 (_, r) => isKnown r
adamc@1221	894 \| Recrd (xes, true) => List.all isKnown (SM.listItems (!xes))
adamc@1221	895 \| _ => false
adamc@1221	896 end
adamc@1221	897
adamc@1221	898 val r = representative (db, e)
adamc@1221	899 in
adamc@1221	900 isKnown r
adamc@1221	901 end
adamc@1215	902 \| (PCon0 f, [e]) =>
adamc@1215	903 (case #Variety (unNode (representative (db, e))) of
adamc@1215	904 Dt0 f' => f' = f
adamc@1215	905 \| _ => false)
adamc@1215	906 \| (PCon1 f, [e]) =>
adamc@1215	907 (case #Variety (unNode (representative (db, e))) of
adamc@1215	908 Dt1 (f', _) => f' = f
adamc@1215	909 \| _ => false)
adamc@1215	910 \| (Eq, [e1, e2]) =>
adamc@1214	911 let
adamc@1215	912 val r1 = representative (db, e1)
adamc@1215	913 val r2 = representative (db, e2)
adamc@1214	914 in
adamc@1215	915 repOf r1 = repOf r2
adamc@1214	916 end
adamc@1215	917 \| _ => false
adamc@1212	918
adamc@1218	919 fun builtFrom (db, {Base = bs, Derived = d}) =
adamc@1218	920 let
adamc@1218	921 val bs = map (fn b => representative (db, b)) bs
adamc@1218	922
adamc@1218	923 fun loop d =
adamc@1218	924 let
adamc@1218	925 val d = repOf d
adamc@1218	926 in
adamc@1218	927 List.exists (fn b => repOf b = d) bs
adamc@1218	928 orelse case #Variety (unNode d) of
adamc@1218	929 Dt0 _ => true
adamc@1218	930 \| Dt1 (_, d) => loop d
adamc@1218	931 \| Prim _ => true
adamc@1221	932 \| Recrd (xes, _) => List.all loop (SM.listItems (!xes))
adamc@1218	933 \| Nothing => false
adamc@1218	934 end
adamc@1218	935 in
adamc@1218	936 loop (representative (db, d))
adamc@1218	937 end
adamc@1218	938
adamc@1208	939 end
adamc@1208	940
adamc@1215	941 fun decomp fals or =
adamc@1215	942 let
adamc@1215	943 fun decomp p k =
adamc@1215	944 case p of
adamc@1215	945 True => k []
adamc@1215	946 \| False => fals
adamc@1215	947 \| Unknown => k []
adamc@1215	948 \| And (p1, p2) =>
adamc@1215	949 decomp p1 (fn ps1 =>
adamc@1215	950 decomp p2 (fn ps2 =>
adamc@1215	951 k (ps1 @ ps2)))
adamc@1215	952 \| Or (p1, p2) =>
adamc@1215	953 or (decomp p1 k, fn () => decomp p2 k)
adamc@1215	954 \| Reln x => k [AReln x]
adamc@1215	955 \| Cond x => k [ACond x]
adamc@1215	956 in
adamc@1215	957 decomp
adamc@1215	958 end
adamc@1202	959
adamc@1226	960 val tabs = ref (SM.empty : (string list * string list list) SM.map)
adamc@1226	961
adamc@1231	962 fun ccOf hyps =
adamc@1231	963 let
adamc@1231	964 val cc = Cc.database ()
adamc@1231	965 val () = app (fn a => Cc.assert (cc, a)) hyps
adamc@1231	966
adamc@1231	967 (* Take advantage of table key information *)
adamc@1231	968 fun findKeys hyps =
adamc@1231	969 case hyps of
adamc@1231	970 [] => ()
adamc@1231	971 \| AReln (Sql tab, [r1]) :: hyps =>
adamc@1231	972 (case SM.find (!tabs, tab) of
adamc@1231	973 NONE => findKeys hyps
adamc@1231	974 \| SOME (_, []) => findKeys hyps
adamc@1231	975 \| SOME (_, ks) =>
adamc@1231	976 let
adamc@1231	977 fun finder hyps =
adamc@1231	978 case hyps of
adamc@1231	979 [] => ()
adamc@1231	980 \| AReln (Sql tab', [r2]) :: hyps =>
adamc@1231	981 (if tab' = tab andalso
adamc@1231	982 List.exists (List.all (fn f =>
adamc@1231	983 let
adamc@1231	984 val r =
adamc@1231	985 Cc.check (cc,
adamc@1231	986 AReln (Eq, [Proj (r1, f),
adamc@1231	987 Proj (r2, f)]))
adamc@1231	988 in
adamc@1231	989 (*Print.prefaces "Fs"
adamc@1231	990 [("tab",
adamc@1231	991 Print.PD.string tab),
adamc@1231	992 ("r1",
adamc@1231	993 p_exp (Proj (r1, f))),
adamc@1231	994 ("r2",
adamc@1231	995 p_exp (Proj (r2, f))),
adamc@1231	996 ("r",
adamc@1231	997 Print.PD.string
adamc@1231	998 (Bool.toString r))];*)
adamc@1231	999 r
adamc@1231	1000 end)) ks then
adamc@1231	1001 ((*Print.prefaces "Key match" [("tab", Print.PD.string tab),
adamc@1231	1002 ("r1", p_exp r1),
adamc@1231	1003 ("r2", p_exp r2),
adamc@1231	1004 ("rp1", Cc.p_repOf cc r1),
adamc@1231	1005 ("rp2", Cc.p_repOf cc r2)];*)
adamc@1231	1006 Cc.assert (cc, AReln (Eq, [r1, r2])))
adamc@1231	1007 else
adamc@1231	1008 ();
adamc@1231	1009 finder hyps)
adamc@1231	1010 \| _ :: hyps => finder hyps
adamc@1231	1011 in
adamc@1231	1012 finder hyps;
adamc@1231	1013 findKeys hyps
adamc@1231	1014 end)
adamc@1231	1015 \| _ :: hyps => findKeys hyps
adamc@1231	1016 in
adamc@1231	1017 findKeys hyps;
adamc@1231	1018 cc
adamc@1231	1019 end
adamc@1231	1020
adamc@1231	1021 fun imply (cc, hyps, goals, outs) =
adamc@1218	1022 let
adamc@1218	1023 fun gls goals onFail acc =
adamc@1218	1024 case goals of
adamc@1218	1025 [] =>
adamc@1231	1026 ((List.all (fn a =>
adamc@1231	1027 if Cc.check (cc, a) then
adamc@1231	1028 true
adamc@1231	1029 else
adamc@1231	1030 ((*Print.prefaces "Can't prove"
adamc@1231	1031 [("a", p_atom a),
adamc@1231	1032 ("hyps", Print.p_list p_atom hyps),
adamc@1231	1033 ("db", Cc.p_database cc)];*)
adamc@1231	1034 false)) acc
adamc@1231	1035 andalso ((Print.preface ("Finding", Cc.p_database cc);) true)
adamc@1231	1036 andalso (case outs of
adamc@1231	1037 NONE => true
adamc@1231	1038 \| SOME outs => Cc.builtFrom (cc, {Derived = Var 0,
adamc@1231	1039 Base = outs})))
adamc@1231	1040 handle Cc.Contradiction => false
adamc@1231	1041 \| Cc.Undetermined => false)
adamc@1218	1042 orelse onFail ()
adamc@1218	1043 \| (g as AReln (Sql gf, [ge])) :: goals =>
adamc@1218	1044 let
adamc@1218	1045 fun hps hyps =
adamc@1218	1046 case hyps of
adamc@1218	1047 [] => gls goals onFail (g :: acc)
adamc@1218	1048 \| (h as AReln (Sql hf, [he])) :: hyps =>
adamc@1218	1049 if gf = hf then
adamc@1218	1050 let
adamc@1218	1051 val saved = save ()
adamc@1218	1052 in
adamc@1218	1053 if eq (ge, he) then
adamc@1218	1054 let
adamc@1218	1055 val changed = IM.numItems (!unif)
adamc@1218	1056 <> IM.numItems saved
adamc@1218	1057 in
adamc@1218	1058 gls goals (fn () => (restore saved;
adamc@1218	1059 changed
adamc@1218	1060 andalso hps hyps))
adamc@1218	1061 acc
adamc@1218	1062 end
adamc@1218	1063 else
adamc@1218	1064 hps hyps
adamc@1218	1065 end
adamc@1218	1066 else
adamc@1218	1067 hps hyps
adamc@1218	1068 \| _ :: hyps => hps hyps
adamc@1218	1069 in
adamc@1218	1070 hps hyps
adamc@1218	1071 end
adamc@1218	1072 \| g :: goals => gls goals onFail (g :: acc)
adamc@1218	1073 in
adamc@1218	1074 reset ();
adamc@1218	1075 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
adamc@1223	1076 ("goals", Print.p_list p_atom goals)];*)
adamc@1218	1077 gls goals (fn () => false) []
adamc@1231	1078 end
adamc@1200	1079
adamc@1200	1080 fun patCon pc =
adamc@1200	1081 case pc of
adamc@1200	1082 PConVar n => "C" ^ Int.toString n
adamc@1200	1083 \| PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200	1084
adamc@1200	1085 datatype chunk =
adamc@1200	1086 String of string
adamc@1200	1087 \| Exp of Mono.exp
adamc@1200	1088
adamc@1200	1089 fun chunkify e =
adamc@1200	1090 case #1 e of
adamc@1200	1091 EPrim (Prim.String s) => [String s]
adamc@1207	1092 \| EStrcat (e1, e2) =>
adamc@1207	1093 let
adamc@1207	1094 val chs1 = chunkify e1
adamc@1207	1095 val chs2 = chunkify e2
adamc@1207	1096 in
adamc@1207	1097 case chs2 of
adamc@1207	1098 String s2 :: chs2' =>
adamc@1207	1099 (case List.last chs1 of
adamc@1207	1100 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207	1101 \| _ => chs1 @ chs2)
adamc@1207	1102 \| _ => chs1 @ chs2
adamc@1207	1103 end
adamc@1200	1104 \| _ => [Exp e]
adamc@1200	1105
adamc@1201	1106 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201	1107
adamc@1201	1108 fun always v chs = SOME (v, chs)
adamc@1201	1109
adamc@1202	1110 fun parse p s =
adamc@1202	1111 case p (chunkify s) of
adamc@1201	1112 SOME (v, []) => SOME v
adamc@1201	1113 \| _ => NONE
adamc@1201	1114
adamc@1201	1115 fun const s chs =
adamc@1201	1116 case chs of
adamc@1201	1117 String s' :: chs => if String.isPrefix s s' then
adamc@1201	1118 SOME ((), if size s = size s' then
adamc@1201	1119 chs
adamc@1201	1120 else
adamc@1201	1121 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201	1122 else
adamc@1201	1123 NONE
adamc@1201	1124 \| _ => NONE
adamc@1201	1125
adamc@1201	1126 fun follow p1 p2 chs =
adamc@1201	1127 case p1 chs of
adamc@1201	1128 NONE => NONE
adamc@1201	1129 \| SOME (v1, chs) =>
adamc@1201	1130 case p2 chs of
adamc@1201	1131 NONE => NONE
adamc@1201	1132 \| SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201	1133
adamc@1201	1134 fun wrap p f chs =
adamc@1201	1135 case p chs of
adamc@1201	1136 NONE => NONE
adamc@1201	1137 \| SOME (v, chs) => SOME (f v, chs)
adamc@1201	1138
adamc@1209	1139 fun wrapP p f chs =
adamc@1209	1140 case p chs of
adamc@1209	1141 NONE => NONE
adamc@1209	1142 \| SOME (v, chs) =>
adamc@1209	1143 case f v of
adamc@1209	1144 NONE => NONE
adamc@1209	1145 \| SOME r => SOME (r, chs)
adamc@1209	1146
adamc@1201	1147 fun alt p1 p2 chs =
adamc@1201	1148 case p1 chs of
adamc@1201	1149 NONE => p2 chs
adamc@1201	1150 \| v => v
adamc@1201	1151
adamc@1207	1152 fun altL ps =
adamc@1207	1153 case rev ps of
adamc@1207	1154 [] => (fn _ => NONE)
adamc@1207	1155 \| p :: ps =>
adamc@1207	1156 foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207	1157
adamc@1204	1158 fun opt p chs =
adamc@1204	1159 case p chs of
adamc@1204	1160 NONE => SOME (NONE, chs)
adamc@1204	1161 \| SOME (v, chs) => SOME (SOME v, chs)
adamc@1204	1162
adamc@1201	1163 fun skip cp chs =
adamc@1201	1164 case chs of
adamc@1201	1165 String "" :: chs => skip cp chs
adamc@1201	1166 \| String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201	1167 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201	1168 else
adamc@1201	1169 SOME ((), chs)
adamc@1201	1170 \| _ => SOME ((), chs)
adamc@1201	1171
adamc@1201	1172 fun keep cp chs =
adamc@1201	1173 case chs of
adamc@1201	1174 String "" :: chs => keep cp chs
adamc@1201	1175 \| String s :: chs' =>
adamc@1201	1176 let
adamc@1201	1177 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201	1178 in
adamc@1201	1179 if Substring.isEmpty befor then
adamc@1201	1180 NONE
adamc@1201	1181 else
adamc@1201	1182 SOME (Substring.string befor,
adamc@1201	1183 if Substring.isEmpty after then
adamc@1201	1184 chs'
adamc@1201	1185 else
adamc@1201	1186 String (Substring.string after) :: chs')
adamc@1201	1187 end
adamc@1201	1188 \| _ => NONE
adamc@1201	1189
adamc@1204	1190 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204	1191 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204	1192
adamc@1204	1193 fun log name p chs =
adamc@1206	1194 (if !debug then
adamc@1227	1195 (print (name ^ ": ");
adamc@1227	1196 app (fn String s => print s
adamc@1227	1197 \| _ => print "???") chs;
adamc@1227	1198 print "\n")
adamc@1206	1199 else
adamc@1206	1200 ();
adamc@1204	1201 p chs)
adamc@1201	1202
adamc@1201	1203 fun list p chs =
adamc@1207	1204 altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207	1205 (fn (v, ((), ls)) => v :: ls),
adamc@1207	1206 wrap (ws p) (fn v => [v]),
adamc@1207	1207 always []] chs
adamc@1201	1208
adamc@1201	1209 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201	1210
adamc@1211	1211 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211	1212 SOME (String.extract (s, 2, NONE))
adamc@1201	1213 else
adamc@1211	1214 NONE)
adamc@1211	1215 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211	1216 SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211	1217 ^ String.extract (s, 4, NONE))
adamc@1211	1218 else
adamc@1211	1219 NONE)
adamc@1201	1220
adamc@1211	1221 val field = wrap (follow t_ident
adamc@1201	1222 (follow (const ".")
adamc@1201	1223 uw_ident))
adamc@1201	1224 (fn (t, ((), f)) => (t, f))
adamc@1201	1225
adamc@1206	1226 datatype Rel =
adamc@1206	1227 Exps of exp * exp -> prop
adamc@1206	1228 \| Props of prop * prop -> prop
adamc@1206	1229
adamc@1204	1230 datatype sqexp =
adamc@1206	1231 SqConst of Prim.t
adamc@1206	1232 \| Field of string * string
adamc@1206	1233 \| Binop of Rel * sqexp * sqexp
adamc@1207	1234 \| SqKnown of sqexp
adamc@1207	1235 \| Inj of Mono.exp
adamc@1211	1236 \| SqFunc of string * sqexp
adamc@1211	1237 \| Count
adamc@1204	1238
adamc@1210	1239 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210	1240
adamc@1210	1241 val sqbrel = altL [cmp "=" Eq,
adamc@1210	1242 cmp "<>" Ne,
adamc@1210	1243 cmp "<=" Le,
adamc@1210	1244 cmp "<" Lt,
adamc@1210	1245 cmp ">=" Ge,
adamc@1210	1246 cmp ">" Gt,
adamc@1207	1247 wrap (const "AND") (fn () => Props And),
adamc@1207	1248 wrap (const "OR") (fn () => Props Or)]
adamc@1204	1249
adamc@1204	1250 datatype ('a, 'b) sum = inl of 'a \| inr of 'b
adamc@1204	1251
adamc@1209	1252 fun string chs =
adamc@1206	1253 case chs of
adamc@1209	1254 String s :: chs =>
adamc@1209	1255 if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209	1256 let
adamc@1209	1257 fun loop (cs, acc) =
adamc@1209	1258 case cs of
adamc@1209	1259 [] => NONE
adamc@1209	1260 \| c :: cs =>
adamc@1209	1261 if c = #"'" then
adamc@1209	1262 SOME (String.implode (rev acc), cs)
adamc@1209	1263 else if c = #"\\" then
adamc@1209	1264 case cs of
adamc@1209	1265 c :: cs => loop (cs, c :: acc)
adamc@1209	1266 \| _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209	1267 else
adamc@1209	1268 loop (cs, c :: acc)
adamc@1209	1269 in
adamc@1209	1270 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209	1271 NONE => NONE
adamc@1209	1272 \| SOME (s, []) => SOME (s, chs)
adamc@1209	1273 \| SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209	1274 end
adamc@1209	1275 else
adamc@1209	1276 NONE
adamc@1209	1277 \| _ => NONE
adamc@1206	1278
adamc@1209	1279 val prim =
adamc@1209	1280 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209	1281 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209	1282 (opt (const "::float8"))) #1,
adamc@1209	1283 wrap (follow (wrapP (keep Char.isDigit)
adamc@1209	1284 (Option.map Prim.Int o Int64.fromString))
adamc@1209	1285 (opt (const "::int8"))) #1,
adamc@1209	1286 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209	1287 (Prim.String o #1 o #2)]
adamc@1206	1288
adamc@1207	1289 fun known' chs =
adamc@1207	1290 case chs of
adamc@1207	1291 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207	1292 \| _ => NONE
adamc@1207	1293
adamc@1207	1294 fun sqlify chs =
adamc@1207	1295 case chs of
adamc@1207	1296 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207	1297 if String.isPrefix "sqlify" f then
adamc@1207	1298 SOME (e, chs)
adamc@1207	1299 else
adamc@1207	1300 NONE
adamc@1207	1301 \| _ => NONE
adamc@1207	1302
adamc@1211	1303 fun constK s = wrap (const s) (fn () => s)
adamc@1211	1304
adamc@1211	1305 val funcName = altL [constK "COUNT",
adamc@1211	1306 constK "MIN",
adamc@1211	1307 constK "MAX",
adamc@1211	1308 constK "SUM",
adamc@1211	1309 constK "AVG"]
adamc@1211	1310
adamc@1204	1311 fun sqexp chs =
adamc@1206	1312 log "sqexp"
adamc@1207	1313 (altL [wrap prim SqConst,
adamc@1211	1314 wrap field Field,
adamc@1207	1315 wrap known SqKnown,
adamc@1211	1316 wrap func SqFunc,
adamc@1211	1317 wrap (const "COUNT(*)") (fn () => Count),
adamc@1207	1318 wrap sqlify Inj,
adamc@1211	1319 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211	1320 (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211	1321 (fn ((), (e, _)) => e),
adamc@1207	1322 wrap (follow (ws (const "("))
adamc@1207	1323 (follow (wrap
adamc@1207	1324 (follow sqexp
adamc@1207	1325 (alt
adamc@1207	1326 (wrap
adamc@1207	1327 (follow (ws sqbrel)
adamc@1207	1328 (ws sqexp))
adamc@1207	1329 inl)
adamc@1207	1330 (always (inr ()))))
adamc@1207	1331 (fn (e1, sm) =>
adamc@1207	1332 case sm of
adamc@1207	1333 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207	1334 \| inr () => e1))
adamc@1207	1335 (const ")")))
adamc@1207	1336 (fn ((), (e, ())) => e)])
adamc@1207	1337 chs
adamc@1206	1338
adamc@1207	1339 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211	1340 (fn ((), ((), (e, ()))) => e) chs
adamc@1211	1341
adamc@1211	1342 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211	1343 (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211	1344
adamc@1211	1345 datatype sitem =
adamc@1211	1346 SqField of string * string
adamc@1211	1347 \| SqExp of sqexp * string
adamc@1211	1348
adamc@1211	1349 val sitem = alt (wrap field SqField)
adamc@1211	1350 (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211	1351 (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207	1352
adamc@1207	1353 val select = log "select"
adamc@1207	1354 (wrap (follow (const "SELECT ") (list sitem))
adamc@1207	1355 (fn ((), ls) => ls))
adamc@1201	1356
adamc@1201	1357 val fitem = wrap (follow uw_ident
adamc@1201	1358 (follow (const " AS ")
adamc@1201	1359 t_ident))
adamc@1201	1360 (fn (t, ((), f)) => (t, f))
adamc@1201	1361
adamc@1207	1362 val from = log "from"
adamc@1207	1363 (wrap (follow (const "FROM ") (list fitem))
adamc@1207	1364 (fn ((), ls) => ls))
adamc@1201	1365
adamc@1204	1366 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204	1367 (fn ((), ls) => ls)
adamc@1204	1368
adamc@1227	1369 type query1 = {Select : sitem list,
adamc@1227	1370 From : (string * string) list,
adamc@1227	1371 Where : sqexp option}
adamc@1227	1372
adamc@1227	1373 val query1 = log "query1"
adamc@1207	1374 (wrap (follow (follow select from) (opt wher))
adamc@1207	1375 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201	1376
adamc@1227	1377 datatype query =
adamc@1227	1378 Query1 of query1
adamc@1227	1379 \| Union of query * query
adamc@1227	1380
adamc@1227	1381 fun query chs = log "query"
adamc@1227	1382 (alt (wrap (follow (const "((")
adamc@1227	1383 (follow query
adamc@1227	1384 (follow (const ") UNION (")
adamc@1227	1385 (follow query (const "))")))))
adamc@1227	1386 (fn ((), (q1, ((), (q2, ())))) => Union (q1, q2)))
adamc@1227	1387 (wrap query1 Query1))
adamc@1227	1388 chs
adamc@1227	1389
adamc@1220	1390 datatype dml =
adamc@1220	1391 Insert of string * (string * sqexp) list
adamc@1221	1392 \| Delete of string * sqexp
adamc@1223	1393 \| Update of string * (string * sqexp) list * sqexp
adamc@1220	1394
adamc@1220	1395 val insert = log "insert"
adamc@1220	1396 (wrapP (follow (const "INSERT INTO ")
adamc@1220	1397 (follow uw_ident
adamc@1220	1398 (follow (const " (")
adamc@1220	1399 (follow (list uw_ident)
adamc@1220	1400 (follow (const ") VALUES (")
adamc@1220	1401 (follow (list sqexp)
adamc@1220	1402 (const ")")))))))
adamc@1220	1403 (fn ((), (tab, ((), (fs, ((), (es, ())))))) =>
adamc@1221	1404 (SOME (tab, ListPair.zipEq (fs, es)))
adamc@1220	1405 handle ListPair.UnequalLengths => NONE))
adamc@1220	1406
adamc@1221	1407 val delete = log "delete"
adamc@1221	1408 (wrap (follow (const "DELETE FROM ")
adamc@1221	1409 (follow uw_ident
adamc@1221	1410 (follow (const " AS T_T WHERE ")
adamc@1221	1411 sqexp)))
adamc@1221	1412 (fn ((), (tab, ((), es))) => (tab, es)))
adamc@1221	1413
adamc@1223	1414 val setting = log "setting"
adamc@1223	1415 (wrap (follow uw_ident (follow (const " = ") sqexp))
adamc@1223	1416 (fn (f, ((), e)) => (f, e)))
adamc@1223	1417
adamc@1223	1418 val update = log "update"
adamc@1223	1419 (wrap (follow (const "UPDATE ")
adamc@1223	1420 (follow uw_ident
adamc@1223	1421 (follow (const " AS T_T SET ")
adamc@1223	1422 (follow (list setting)
adamc@1223	1423 (follow (ws (const "WHERE "))
adamc@1223	1424 sqexp)))))
adamc@1223	1425 (fn ((), (tab, ((), (fs, ((), e))))) =>
adamc@1223	1426 (tab, fs, e)))
adamc@1223	1427
adamc@1220	1428 val dml = log "dml"
adamc@1221	1429 (altL [wrap insert Insert,
adamc@1223	1430 wrap delete Delete,
adamc@1223	1431 wrap update Update])
adamc@1220	1432
adamc@1215	1433 fun removeDups (ls : (string * string) list) =
adamc@1211	1434 case ls of
adamc@1211	1435 [] => []
adamc@1211	1436 \| x :: ls =>
adamc@1211	1437 let
adamc@1211	1438 val ls = removeDups ls
adamc@1211	1439 in
adamc@1211	1440 if List.exists (fn x' => x' = x) ls then
adamc@1211	1441 ls
adamc@1211	1442 else
adamc@1211	1443 x :: ls
adamc@1211	1444 end
adamc@1211	1445
adamc@1212	1446 datatype queryMode =
adamc@1218	1447 SomeCol
adamc@1212	1448 \| AllCols of exp
adamc@1212	1449
adamc@1220	1450 fun expIn rv env rvOf =
adamc@1220	1451 let
adamc@1220	1452 fun expIn (e, rvN) =
adamc@1220	1453 let
adamc@1220	1454 fun default () =
adamc@1220	1455 let
adamc@1229	1456 val (rvN, e') = rv rvN
adamc@1220	1457 in
adamc@1229	1458 (inl e', rvN)
adamc@1220	1459 end
adamc@1220	1460 in
adamc@1220	1461 case e of
adamc@1220	1462 SqConst p => (inl (Const p), rvN)
adamc@1220	1463 \| Field (v, f) => (inl (Proj (rvOf v, f)), rvN)
adamc@1220	1464 \| Binop (bo, e1, e2) =>
adamc@1220	1465 let
adamc@1220	1466 val (e1, rvN) = expIn (e1, rvN)
adamc@1220	1467 val (e2, rvN) = expIn (e2, rvN)
adamc@1220	1468 in
adamc@1220	1469 (inr (case (bo, e1, e2) of
adamc@1220	1470 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1220	1471 \| (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1220	1472 \| _ => Unknown), rvN)
adamc@1220	1473 end
adamc@1220	1474 \| SqKnown e =>
adamc@1220	1475 (case expIn (e, rvN) of
adamc@1220	1476 (inl e, rvN) => (inr (Reln (Known, [e])), rvN)
adamc@1220	1477 \| _ => (inr Unknown, rvN))
adamc@1220	1478 \| Inj e =>
adamc@1220	1479 let
adamc@1220	1480 fun deinj e =
adamc@1220	1481 case #1 e of
adamc@1220	1482 ERel n => (List.nth (env, n), rvN)
adamc@1220	1483 \| EField (e, f) =>
adamc@1220	1484 let
adamc@1220	1485 val (e, rvN) = deinj e
adamc@1220	1486 in
adamc@1220	1487 (Proj (e, f), rvN)
adamc@1220	1488 end
adamc@1220	1489 \| _ =>
adamc@1220	1490 let
adamc@1220	1491 val (rvN, e) = rv rvN
adamc@1220	1492 in
adamc@1220	1493 (e, rvN)
adamc@1220	1494 end
adamc@1220	1495
adamc@1220	1496 val (e, rvN) = deinj e
adamc@1220	1497 in
adamc@1220	1498 (inl e, rvN)
adamc@1220	1499 end
adamc@1220	1500 \| SqFunc (f, e) =>
adamc@1220	1501 (case expIn (e, rvN) of
adamc@1220	1502 (inl e, rvN) => (inl (Func (Other f, [e])), rvN)
adamc@1220	1503 \| _ => default ())
adamc@1220	1504
adamc@1220	1505 \| Count => default ()
adamc@1220	1506 end
adamc@1220	1507 in
adamc@1220	1508 expIn
adamc@1220	1509 end
adamc@1216	1510
adamc@1214	1511 fun queryProp env rvN rv oe e =
adamc@1216	1512 let
adamc@1216	1513 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1216	1514 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1227	1515 (rvN, Unknown, [], []))
adamc@1216	1516 in
adamc@1216	1517 case parse query e of
adamc@1216	1518 NONE => default ()
adamc@1227	1519 \| SOME q =>
adamc@1216	1520 let
adamc@1227	1521 fun doQuery (q, rvN) =
adamc@1227	1522 case q of
adamc@1227	1523 Query1 r =>
adamc@1227	1524 let
adamc@1227	1525 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1227	1526 let
adamc@1227	1527 val (rvN, e) = rv rvN
adamc@1227	1528 in
adamc@1227	1529 ((v, e), rvN)
adamc@1227	1530 end) rvN (#From r)
adamc@1214	1531
adamc@1227	1532 fun rvOf v =
adamc@1227	1533 case List.find (fn (v', _) => v' = v) rvs of
adamc@1227	1534 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1227	1535 \| SOME (_, e) => e
adamc@1214	1536
adamc@1227	1537 fun usedFields e =
adamc@1227	1538 case e of
adamc@1227	1539 SqConst _ => []
adamc@1227	1540 \| Field (v, f) => [(v, f)]
adamc@1227	1541 \| Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1227	1542 \| SqKnown _ => []
adamc@1227	1543 \| Inj _ => []
adamc@1227	1544 \| SqFunc (_, e) => usedFields e
adamc@1227	1545 \| Count => []
adamc@1214	1546
adamc@1227	1547 val p =
adamc@1227	1548 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1211	1549
adamc@1227	1550 val expIn = expIn rv env rvOf
adamc@1205	1551
adamc@1227	1552 val (p, rvN) = case #Where r of
adamc@1227	1553 NONE => (p, rvN)
adamc@1227	1554 \| SOME e =>
adamc@1227	1555 case expIn (e, rvN) of
adamc@1227	1556 (inr p', rvN) => (And (p, p'), rvN)
adamc@1227	1557 \| _ => (p, rvN)
adamc@1210	1558
adamc@1227	1559 fun normal () =
adamc@1227	1560 case oe of
adamc@1227	1561 SomeCol =>
adamc@1227	1562 let
adamc@1227	1563 val (sis, rvN) =
adamc@1227	1564 ListUtil.foldlMap
adamc@1227	1565 (fn (si, rvN) =>
adamc@1227	1566 case si of
adamc@1227	1567 SqField (v, f) => (Proj (rvOf v, f), rvN)
adamc@1227	1568 \| SqExp (e, f) =>
adamc@1227	1569 case expIn (e, rvN) of
adamc@1227	1570 (inr _, _) =>
adamc@1227	1571 let
adamc@1227	1572 val (rvN, e) = rv rvN
adamc@1227	1573 in
adamc@1227	1574 (e, rvN)
adamc@1227	1575 end
adamc@1227	1576 \| (inl e, rvN) => (e, rvN)) rvN (#Select r)
adamc@1227	1577 in
adamc@1227	1578 (rvN, p, True, sis)
adamc@1227	1579 end
adamc@1227	1580 \| AllCols oe =>
adamc@1227	1581 let
adamc@1227	1582 val (ts, es, rvN) =
adamc@1227	1583 foldl (fn (si, (ts, es, rvN)) =>
adamc@1227	1584 case si of
adamc@1227	1585 SqField (v, f) =>
adamc@1227	1586 let
adamc@1227	1587 val fs = getOpt (SM.find (ts, v), SM.empty)
adamc@1227	1588 in
adamc@1227	1589 (SM.insert (ts, v, SM.insert (fs, f, Proj (rvOf v, f))), es, rvN)
adamc@1227	1590 end
adamc@1227	1591 \| SqExp (e, f) =>
adamc@1227	1592 let
adamc@1227	1593 val (e, rvN) =
adamc@1227	1594 case expIn (e, rvN) of
adamc@1227	1595 (inr _, rvN) =>
adamc@1227	1596 let
adamc@1227	1597 val (rvN, e) = rv rvN
adamc@1227	1598 in
adamc@1227	1599 (e, rvN)
adamc@1227	1600 end
adamc@1227	1601 \| (inl e, rvN) => (e, rvN)
adamc@1227	1602 in
adamc@1227	1603 (ts, SM.insert (es, f, e), rvN)
adamc@1227	1604 end)
adamc@1227	1605 (SM.empty, SM.empty, rvN) (#Select r)
adamc@1227	1606
adamc@1227	1607 val p' = Reln (Eq, [oe, Recd (map (fn (t, fs) => (t, Recd (SM.listItemsi fs)))
adamc@1227	1608 (SM.listItemsi ts)
adamc@1227	1609 @ SM.listItemsi es)])
adamc@1227	1610 in
adamc@1227	1611 (rvN, And (p, p'), True, [])
adamc@1227	1612 end
adamc@1227	1613
adamc@1227	1614 val (rvN, p, wp, outs) =
adamc@1227	1615 case #Select r of
adamc@1227	1616 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1227	1617 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1227	1618 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1227	1619 (case oe of
adamc@1227	1620 SomeCol =>
adamc@1227	1621 let
adamc@1227	1622 val (rvN, oe) = rv rvN
adamc@1227	1623 in
adamc@1227	1624 (rvN,
adamc@1227	1625 Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
adamc@1227	1626 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1227	1627 p)),
adamc@1227	1628 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1227	1629 [oe])
adamc@1227	1630 end
adamc@1227	1631 \| AllCols oe =>
adamc@1227	1632 let
adamc@1227	1633 fun oeEq e = Reln (Eq, [oe, Recd [(f, e)]])
adamc@1227	1634 in
adamc@1227	1635 (rvN,
adamc@1227	1636 Or (oeEq (Func (DtCon0 "Basis.bool.False", [])),
adamc@1227	1637 And (oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1227	1638 p)),
adamc@1227	1639 oeEq (Func (DtCon0 "Basis.bool.True", [])),
adamc@1227	1640 [])
adamc@1227	1641 end)
adamc@1227	1642 \| _ => normal ())
adamc@1227	1643 \| _ => normal ()
adamc@1227	1644 in
adamc@1227	1645 (rvN, p, map (fn x => (wp, x))
adamc@1227	1646 (case #Where r of
adamc@1227	1647 NONE => []
adamc@1227	1648 \| SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e)), outs)
adamc@1227	1649 end
adamc@1227	1650 \| Union (q1, q2) =>
adamc@1220	1651 let
adamc@1227	1652 val (rvN, p1, used1, outs1) = doQuery (q1, rvN)
adamc@1227	1653 val (rvN, p2, used2, outs2) = doQuery (q2, rvN)
adamc@1220	1654 in
adamc@1227	1655 case (outs1, outs2) of
adamc@1227	1656 ([], []) => (rvN, Or (p1, p2),
adamc@1227	1657 map (fn (p, e) => (And (p1, p), e)) used1
adamc@1227	1658 @ map (fn (p, e) => (And (p2, p), e)) used2, [])
adamc@1227	1659 \| _ => default ()
adamc@1220	1660 end
adamc@1216	1661 in
adamc@1227	1662 doQuery (q, rvN)
adamc@1216	1663 end
adamc@1220	1664 end
adamc@1220	1665
adamc@1220	1666 fun insertProp rvN rv e =
adamc@1220	1667 let
adamc@1220	1668 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1220	1669 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1220	1670 Unknown)
adamc@1220	1671 in
adamc@1220	1672 case parse query e of
adamc@1227	1673 SOME (Query1 r) =>
adamc@1220	1674 let
adamc@1220	1675 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1220	1676 let
adamc@1220	1677 val (rvN, e) = rv rvN
adamc@1220	1678 in
adamc@1220	1679 ((v, e), rvN)
adamc@1220	1680 end) rvN (#From r)
adamc@1220	1681
adamc@1220	1682 fun rvOf v =
adamc@1220	1683 case List.find (fn (v', _) => v' = v) rvs of
adamc@1220	1684 NONE => raise Fail "Iflow.insertProp: Bad table variable"
adamc@1220	1685 \| SOME (_, e) => e
adamc@1220	1686
adamc@1220	1687 val p =
adamc@1220	1688 foldl (fn ((t, v), p) =>
adamc@1220	1689 let
adamc@1220	1690 val t =
adamc@1220	1691 case v of
adamc@1229	1692 "New" => t ^ "$New"
adamc@1220	1693 \| _ => t
adamc@1220	1694 in
adamc@1220	1695 And (p, Reln (Sql t, [rvOf v]))
adamc@1220	1696 end) True (#From r)
adamc@1220	1697
adamc@1220	1698 val expIn = expIn rv [] rvOf
adamc@1220	1699 in
adamc@1220	1700 case #Where r of
adamc@1220	1701 NONE => p
adamc@1220	1702 \| SOME e =>
adamc@1220	1703 case expIn (e, rvN) of
adamc@1220	1704 (inr p', _) => And (p, p')
adamc@1220	1705 \| _ => p
adamc@1220	1706 end
adamc@1227	1707 \| _ => default ()
adamc@1216	1708 end
adamc@1200	1709
adamc@1221	1710 fun deleteProp rvN rv e =
adamc@1221	1711 let
adamc@1221	1712 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1221	1713 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1221	1714 Unknown)
adamc@1221	1715 in
adamc@1221	1716 case parse query e of
adamc@1227	1717 SOME (Query1 r) =>
adamc@1221	1718 let
adamc@1221	1719 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1221	1720 let
adamc@1221	1721 val (rvN, e) = rv rvN
adamc@1221	1722 in
adamc@1221	1723 ((v, e), rvN)
adamc@1221	1724 end) rvN (#From r)
adamc@1221	1725
adamc@1221	1726 fun rvOf v =
adamc@1221	1727 case List.find (fn (v', _) => v' = v) rvs of
adamc@1221	1728 NONE => raise Fail "Iflow.deleteProp: Bad table variable"
adamc@1221	1729 \| SOME (_, e) => e
adamc@1221	1730
adamc@1221	1731 val p =
adamc@1221	1732 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1221	1733
adamc@1221	1734 val expIn = expIn rv [] rvOf
adamc@1221	1735 in
adamc@1221	1736 And (Reln (Sql "$Old", [rvOf "Old"]),
adamc@1221	1737 case #Where r of
adamc@1221	1738 NONE => p
adamc@1221	1739 \| SOME e =>
adamc@1221	1740 case expIn (e, rvN) of
adamc@1221	1741 (inr p', _) => And (p, p')
adamc@1221	1742 \| _ => p)
adamc@1221	1743 end
adamc@1227	1744 \| _ => default ()
adamc@1221	1745 end
adamc@1221	1746
adamc@1223	1747 fun updateProp rvN rv e =
adamc@1223	1748 let
adamc@1223	1749 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1223	1750 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1223	1751 Unknown)
adamc@1223	1752 in
adamc@1223	1753 case parse query e of
adamc@1227	1754 SOME (Query1 r) =>
adamc@1223	1755 let
adamc@1223	1756 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1223	1757 let
adamc@1223	1758 val (rvN, e) = rv rvN
adamc@1223	1759 in
adamc@1223	1760 ((v, e), rvN)
adamc@1223	1761 end) rvN (#From r)
adamc@1223	1762
adamc@1223	1763 fun rvOf v =
adamc@1223	1764 case List.find (fn (v', _) => v' = v) rvs of
adamc@1223	1765 NONE => raise Fail "Iflow.insertProp: Bad table variable"
adamc@1223	1766 \| SOME (_, e) => e
adamc@1223	1767
adamc@1223	1768 val p =
adamc@1223	1769 foldl (fn ((t, v), p) =>
adamc@1223	1770 let
adamc@1223	1771 val t =
adamc@1223	1772 case v of
adamc@1229	1773 "New" => t ^ "$New"
adamc@1223	1774 \| _ => t
adamc@1223	1775 in
adamc@1223	1776 And (p, Reln (Sql t, [rvOf v]))
adamc@1223	1777 end) True (#From r)
adamc@1223	1778
adamc@1223	1779 val expIn = expIn rv [] rvOf
adamc@1223	1780 in
adamc@1223	1781 And (Reln (Sql "$Old", [rvOf "Old"]),
adamc@1223	1782 case #Where r of
adamc@1223	1783 NONE => p
adamc@1223	1784 \| SOME e =>
adamc@1223	1785 case expIn (e, rvN) of
adamc@1223	1786 (inr p', _) => And (p, p')
adamc@1223	1787 \| _ => p)
adamc@1223	1788 end
adamc@1227	1789 \| _ => default ()
adamc@1223	1790 end
adamc@1223	1791
adamc@1211	1792 fun evalPat env e (pt, _) =
adamc@1211	1793 case pt of
adamc@1211	1794 PWild => (env, True)
adamc@1211	1795 \| PVar _ => (e :: env, True)
adamc@1211	1796 \| PPrim _ => (env, True)
adamc@1215	1797 \| PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
adamc@1211	1798 \| PCon (_, pc, SOME pt) =>
adamc@1211	1799 let
adamc@1215	1800 val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211	1801 in
adamc@1215	1802 (env, And (p, Reln (PCon1 (patCon pc), [e])))
adamc@1211	1803 end
adamc@1211	1804 \| PRecord xpts =>
adamc@1211	1805 foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211	1806 let
adamc@1211	1807 val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211	1808 in
adamc@1211	1809 (env, And (p', p))
adamc@1211	1810 end) (env, True) xpts
adamc@1215	1811 \| PNone _ => (env, Reln (PCon0 "None", [e]))
adamc@1211	1812 \| PSome (_, pt) =>
adamc@1211	1813 let
adamc@1215	1814 val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211	1815 in
adamc@1215	1816 (env, And (p, Reln (PCon1 "Some", [e])))
adamc@1211	1817 end
adamc@1211	1818
adamc@1211	1819 fun peq (p1, p2) =
adamc@1211	1820 case (p1, p2) of
adamc@1211	1821 (True, True) => true
adamc@1211	1822 \| (False, False) => true
adamc@1211	1823 \| (Unknown, Unknown) => true
adamc@1211	1824 \| (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211	1825 \| (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211	1826 \| (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212	1827 \| (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211	1828 \| _ => false
adamc@1211	1829
adamc@1211	1830 fun removeRedundant p1 =
adamc@1211	1831 let
adamc@1211	1832 fun rr p2 =
adamc@1211	1833 if peq (p1, p2) then
adamc@1211	1834 True
adamc@1211	1835 else
adamc@1211	1836 case p2 of
adamc@1211	1837 And (x, y) => And (rr x, rr y)
adamc@1211	1838 \| Or (x, y) => Or (rr x, rr y)
adamc@1211	1839 \| _ => p2
adamc@1211	1840 in
adamc@1211	1841 rr
adamc@1211	1842 end
adamc@1211	1843
adamc@1218	1844 datatype cflow = Case \| Where
adamc@1218	1845 datatype flow = Data \| Control of cflow
adamc@1218	1846 type check = ErrorMsg.span * exp * prop
adamc@1221	1847 type dml = ErrorMsg.span * prop
adamc@1218	1848
adamc@1217	1849 structure St :> sig
adamc@1217	1850 type t
adamc@1217	1851 val create : {Var : int,
adamc@1217	1852 Ambient : prop} -> t
adamc@1217	1853
adamc@1217	1854 val curVar : t -> int
adamc@1217	1855 val nextVar : t -> t * int
adamc@1217	1856
adamc@1217	1857 val ambient : t -> prop
adamc@1217	1858 val setAmbient : t * prop -> t
adamc@1217	1859
adamc@1218	1860 val paths : t -> (check * cflow) list
adamc@1218	1861 val addPath : t * (check * cflow) -> t
adamc@1218	1862 val addPaths : t * (check * cflow) list -> t
adamc@1218	1863 val clearPaths : t -> t
adamc@1218	1864 val setPaths : t * (check * cflow) list -> t
adamc@1217	1865
adamc@1218	1866 val sent : t -> (check * flow) list
adamc@1218	1867 val addSent : t * (check * flow) -> t
adamc@1218	1868 val setSent : t * (check * flow) list -> t
adamc@1220	1869
adamc@1221	1870 val inserted : t -> dml list
adamc@1221	1871 val addInsert : t * dml -> t
adamc@1221	1872
adamc@1221	1873 val deleted : t -> dml list
adamc@1221	1874 val addDelete : t * dml -> t
adamc@1223	1875
adamc@1223	1876 val updated : t -> dml list
adamc@1223	1877 val addUpdate : t * dml -> t
adamc@1217	1878 end = struct
adamc@1217	1879
adamc@1217	1880 type t = {Var : int,
adamc@1217	1881 Ambient : prop,
adamc@1218	1882 Path : (check * cflow) list,
adamc@1220	1883 Sent : (check * flow) list,
adamc@1221	1884 Insert : dml list,
adamc@1223	1885 Delete : dml list,
adamc@1223	1886 Update : dml list}
adamc@1217	1887
adamc@1217	1888 fun create {Var = v, Ambient = p} = {Var = v,
adamc@1217	1889 Ambient = p,
adamc@1217	1890 Path = [],
adamc@1220	1891 Sent = [],
adamc@1221	1892 Insert = [],
adamc@1223	1893 Delete = [],
adamc@1223	1894 Update = []}
adamc@1217	1895
adamc@1217	1896 fun curVar (t : t) = #Var t
adamc@1217	1897 fun nextVar (t : t) = ({Var = #Var t + 1,
adamc@1217	1898 Ambient = #Ambient t,
adamc@1217	1899 Path = #Path t,
adamc@1220	1900 Sent = #Sent t,
adamc@1221	1901 Insert = #Insert t,
adamc@1223	1902 Delete = #Delete t,
adamc@1223	1903 Update = #Update t}, #Var t)
adamc@1217	1904
adamc@1217	1905 fun ambient (t : t) = #Ambient t
adamc@1217	1906 fun setAmbient (t : t, p) = {Var = #Var t,
adamc@1217	1907 Ambient = p,
adamc@1217	1908 Path = #Path t,
adamc@1220	1909 Sent = #Sent t,
adamc@1221	1910 Insert = #Insert t,
adamc@1223	1911 Delete = #Delete t,
adamc@1223	1912 Update = #Update t}
adamc@1217	1913
adamc@1218	1914 fun paths (t : t) = #Path t
adamc@1217	1915 fun addPath (t : t, c) = {Var = #Var t,
adamc@1217	1916 Ambient = #Ambient t,
adamc@1217	1917 Path = c :: #Path t,
adamc@1220	1918 Sent = #Sent t,
adamc@1221	1919 Insert = #Insert t,
adamc@1223	1920 Delete = #Delete t,
adamc@1223	1921 Update = #Update t}
adamc@1218	1922 fun addPaths (t : t, cs) = {Var = #Var t,
adamc@1218	1923 Ambient = #Ambient t,
adamc@1218	1924 Path = cs @ #Path t,
adamc@1220	1925 Sent = #Sent t,
adamc@1221	1926 Insert = #Insert t,
adamc@1223	1927 Delete = #Delete t,
adamc@1223	1928 Update = #Update t}
adamc@1218	1929 fun clearPaths (t : t) = {Var = #Var t,
adamc@1218	1930 Ambient = #Ambient t,
adamc@1218	1931 Path = [],
adamc@1220	1932 Sent = #Sent t,
adamc@1221	1933 Insert = #Insert t,
adamc@1223	1934 Delete = #Delete t,
adamc@1223	1935 Update = #Update t}
adamc@1218	1936 fun setPaths (t : t, cs) = {Var = #Var t,
adamc@1218	1937 Ambient = #Ambient t,
adamc@1218	1938 Path = cs,
adamc@1220	1939 Sent = #Sent t,
adamc@1221	1940 Insert = #Insert t,
adamc@1223	1941 Delete = #Delete t,
adamc@1223	1942 Update = #Update t}
adamc@1217	1943
adamc@1217	1944 fun sent (t : t) = #Sent t
adamc@1217	1945 fun addSent (t : t, c) = {Var = #Var t,
adamc@1217	1946 Ambient = #Ambient t,
adamc@1217	1947 Path = #Path t,
adamc@1220	1948 Sent = c :: #Sent t,
adamc@1221	1949 Insert = #Insert t,
adamc@1223	1950 Delete = #Delete t,
adamc@1223	1951 Update = #Update t}
adamc@1217	1952 fun setSent (t : t, cs) = {Var = #Var t,
adamc@1217	1953 Ambient = #Ambient t,
adamc@1217	1954 Path = #Path t,
adamc@1220	1955 Sent = cs,
adamc@1221	1956 Insert = #Insert t,
adamc@1223	1957 Delete = #Delete t,
adamc@1223	1958 Update = #Update t}
adamc@1220	1959
adamc@1220	1960 fun inserted (t : t) = #Insert t
adamc@1220	1961 fun addInsert (t : t, c) = {Var = #Var t,
adamc@1220	1962 Ambient = #Ambient t,
adamc@1220	1963 Path = #Path t,
adamc@1220	1964 Sent = #Sent t,
adamc@1221	1965 Insert = c :: #Insert t,
adamc@1223	1966 Delete = #Delete t,
adamc@1223	1967 Update = #Update t}
adamc@1221	1968
adamc@1221	1969 fun deleted (t : t) = #Delete t
adamc@1221	1970 fun addDelete (t : t, c) = {Var = #Var t,
adamc@1221	1971 Ambient = #Ambient t,
adamc@1221	1972 Path = #Path t,
adamc@1221	1973 Sent = #Sent t,
adamc@1221	1974 Insert = #Insert t,
adamc@1223	1975 Delete = c :: #Delete t,
adamc@1223	1976 Update = #Update t}
adamc@1223	1977
adamc@1223	1978 fun updated (t : t) = #Update t
adamc@1223	1979 fun addUpdate (t : t, c) = {Var = #Var t,
adamc@1223	1980 Ambient = #Ambient t,
adamc@1223	1981 Path = #Path t,
adamc@1223	1982 Sent = #Sent t,
adamc@1223	1983 Insert = #Insert t,
adamc@1223	1984 Delete = #Delete t,
adamc@1223	1985 Update = c :: #Update t}
adamc@1217	1986
adamc@1217	1987 end
adamc@1217	1988
adamc@1230	1989 fun havocReln r =
adamc@1230	1990 let
adamc@1230	1991 fun hr p =
adamc@1230	1992 case p of
adamc@1230	1993 True => p
adamc@1230	1994 \| False => p
adamc@1230	1995 \| Unknown => p
adamc@1230	1996 \| And (p1, p2) => And (hr p1, hr p2)
adamc@1230	1997 \| Or (p1, p2) => Or (hr p1, hr p2)
adamc@1230	1998 \| Reln (r', _) => if r' = r then True else p
adamc@1230	1999 \| Cond (e, p) => Cond (e, hr p)
adamc@1230	2000 in
adamc@1230	2001 hr
adamc@1230	2002 end
adamc@1230	2003
adamc@1217	2004 fun evalExp env (e as (_, loc), st) =
adamc@1200	2005 let
adamc@1200	2006 fun default () =
adamc@1217	2007 let
adamc@1217	2008 val (st, nv) = St.nextVar st
adamc@1217	2009 in
adamc@1229	2010 (*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
adamc@1229	2011 ("nv", p_exp (Var nv))];*)
adamc@1217	2012 (Var nv, st)
adamc@1217	2013 end
adamc@1200	2014
adamc@1217	2015 fun addSent (p, e, st) =
adamc@1218	2016 let
adamc@1218	2017 val st = if isKnown e then
adamc@1218	2018 st
adamc@1218	2019 else
adamc@1218	2020 St.addSent (st, ((loc, e, p), Data))
adamc@1218	2021
adamc@1218	2022 val st = foldl (fn ((c, fl), st) => St.addSent (st, (c, Control fl))) st (St.paths st)
adamc@1218	2023 in
adamc@1218	2024 St.clearPaths st
adamc@1218	2025 end
adamc@1200	2026 in
adamc@1200	2027 case #1 e of
adamc@1200	2028 EPrim p => (Const p, st)
adamc@1200	2029 \| ERel n => (List.nth (env, n), st)
adamc@1200	2030 \| ENamed _ => default ()
adamc@1215	2031 \| ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
adamc@1200	2032 \| ECon (_, pc, SOME e) =>
adamc@1200	2033 let
adamc@1200	2034 val (e, st) = evalExp env (e, st)
adamc@1200	2035 in
adamc@1215	2036 (Func (DtCon1 (patCon pc), [e]), st)
adamc@1200	2037 end
adamc@1215	2038 \| ENone _ => (Func (DtCon0 "None", []), st)
adamc@1200	2039 \| ESome (_, e) =>
adamc@1200	2040 let
adamc@1200	2041 val (e, st) = evalExp env (e, st)
adamc@1200	2042 in
adamc@1215	2043 (Func (DtCon1 "Some", [e]), st)
adamc@1200	2044 end
adamc@1200	2045 \| EFfi _ => default ()
adamc@1213	2046
adamc@1200	2047 \| EFfiApp (m, s, es) =>
adamc@1200	2048 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200	2049 let
adamc@1200	2050 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200	2051 in
adamc@1217	2052 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
adamc@1200	2053 end
adamc@1200	2054 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200	2055 default ()
adamc@1200	2056 else
adamc@1200	2057 let
adamc@1200	2058 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200	2059 in
adamc@1215	2060 (Func (Other (m ^ "." ^ s), es), st)
adamc@1200	2061 end
adamc@1213	2062
adamc@1213	2063 \| EApp (e1, e2) =>
adamc@1213	2064 let
adamc@1213	2065 val (e1, st) = evalExp env (e1, st)
adamc@1213	2066 in
adamc@1213	2067 case e1 of
adamc@1213	2068 Finish => (Finish, st)
adamc@1213	2069 \| _ => default ()
adamc@1213	2070 end
adamc@1213	2071
adamc@1200	2072 \| EAbs _ => default ()
adamc@1200	2073 \| EUnop (s, e1) =>
adamc@1200	2074 let
adamc@1200	2075 val (e1, st) = evalExp env (e1, st)
adamc@1200	2076 in
adamc@1215	2077 (Func (Other s, [e1]), st)
adamc@1200	2078 end
adamc@1200	2079 \| EBinop (s, e1, e2) =>
adamc@1200	2080 let
adamc@1200	2081 val (e1, st) = evalExp env (e1, st)
adamc@1200	2082 val (e2, st) = evalExp env (e2, st)
adamc@1200	2083 in
adamc@1215	2084 (Func (Other s, [e1, e2]), st)
adamc@1200	2085 end
adamc@1200	2086 \| ERecord xets =>
adamc@1200	2087 let
adamc@1200	2088 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200	2089 let
adamc@1200	2090 val (e, st) = evalExp env (e, st)
adamc@1200	2091 in
adamc@1200	2092 ((x, e), st)
adamc@1200	2093 end) st xets
adamc@1200	2094 in
adamc@1200	2095 (Recd xes, st)
adamc@1200	2096 end
adamc@1200	2097 \| EField (e, s) =>
adamc@1200	2098 let
adamc@1200	2099 val (e, st) = evalExp env (e, st)
adamc@1200	2100 in
adamc@1200	2101 (Proj (e, s), st)
adamc@1200	2102 end
adamc@1218	2103 \| ECase (e, pes, {result = res, ...}) =>
adamc@1211	2104 let
adamc@1211	2105 val (e, st) = evalExp env (e, st)
adamc@1217	2106 val (st, r) = St.nextVar st
adamc@1217	2107 val orig = St.ambient st
adamc@1218	2108 val origPaths = St.paths st
adamc@1211	2109
adamc@1218	2110 val st = St.addPath (st, ((loc, e, orig), Case))
adamc@1218	2111
adamc@1218	2112 val (st, paths) =
adamc@1218	2113 foldl (fn ((pt, pe), (st, paths)) =>
adamc@1218	2114 let
adamc@1218	2115 val (env, pp) = evalPat env e pt
adamc@1218	2116 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
adamc@1218	2117
adamc@1218	2118 val this = And (removeRedundant orig (St.ambient st'),
adamc@1218	2119 Reln (Eq, [Var r, pe]))
adamc@1218	2120 in
adamc@1218	2121 (St.setPaths (St.setAmbient (st', Or (St.ambient st, this)), origPaths),
adamc@1218	2122 St.paths st' @ paths)
adamc@1218	2123 end) (St.setAmbient (st, False), []) pes
adamc@1218	2124
adamc@1218	2125 val st = case #1 res of
adamc@1218	2126 TRecord [] => St.setPaths (st, origPaths)
adamc@1218	2127 \| _ => St.setPaths (st, paths)
adamc@1211	2128 in
adamc@1217	2129 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
adamc@1211	2130 end
adamc@1200	2131 \| EStrcat (e1, e2) =>
adamc@1200	2132 let
adamc@1200	2133 val (e1, st) = evalExp env (e1, st)
adamc@1200	2134 val (e2, st) = evalExp env (e2, st)
adamc@1200	2135 in
adamc@1215	2136 (Func (Other "cat", [e1, e2]), st)
adamc@1200	2137 end
adamc@1200	2138 \| EError _ => (Finish, st)
adamc@1200	2139 \| EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200	2140 let
adamc@1200	2141 val (b, st) = evalExp env (b, st)
adamc@1200	2142 val (m, st) = evalExp env (m, st)
adamc@1200	2143 in
adamc@1217	2144 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
adamc@1200	2145 end
adamc@1200	2146 \| ERedirect (e, _) =>
adamc@1200	2147 let
adamc@1200	2148 val (e, st) = evalExp env (e, st)
adamc@1200	2149 in
adamc@1217	2150 (Finish, addSent (St.ambient st, e, st))
adamc@1200	2151 end
adamc@1200	2152 \| EWrite e =>
adamc@1200	2153 let
adamc@1200	2154 val (e, st) = evalExp env (e, st)
adamc@1200	2155 in
adamc@1217	2156 (Recd [], addSent (St.ambient st, e, st))
adamc@1200	2157 end
adamc@1200	2158 \| ESeq (e1, e2) =>
adamc@1200	2159 let
adamc@1200	2160 val (_, st) = evalExp env (e1, st)
adamc@1200	2161 in
adamc@1200	2162 evalExp env (e2, st)
adamc@1200	2163 end
adamc@1200	2164 \| ELet (_, _, e1, e2) =>
adamc@1200	2165 let
adamc@1200	2166 val (e1, st) = evalExp env (e1, st)
adamc@1200	2167 in
adamc@1200	2168 evalExp (e1 :: env) (e2, st)
adamc@1200	2169 end
adamc@1200	2170 \| EClosure (n, es) =>
adamc@1200	2171 let
adamc@1200	2172 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200	2173 in
adamc@1215	2174 (Func (Other ("Cl" ^ Int.toString n), es), st)
adamc@1200	2175 end
adamc@1200	2176
adamc@1200	2177 \| EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200	2178 let
adamc@1200	2179 val (_, st) = evalExp env (q, st)
adamc@1200	2180 val (i, st) = evalExp env (i, st)
adamc@1200	2181
adamc@1217	2182 val (st', r) = St.nextVar st
adamc@1217	2183 val (st', acc) = St.nextVar st'
adamc@1200	2184
adamc@1200	2185 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200	2186
adamc@1227	2187 val (st', qp, used, _) =
adamc@1214	2188 queryProp env
adamc@1217	2189 st' (fn st' =>
adamc@1217	2190 let
adamc@1217	2191 val (st', rv) = St.nextVar st'
adamc@1217	2192 in
adamc@1217	2193 (st', Var rv)
adamc@1217	2194 end)
adamc@1214	2195 (AllCols (Var r)) q
adamc@1200	2196
adamc@1217	2197 val p' = And (qp, St.ambient st')
adamc@1200	2198
adamc@1217	2199 val (st, res) = if varInP acc (St.ambient st') then
adamc@1217	2200 let
adamc@1217	2201 val (st, r) = St.nextVar st
adamc@1217	2202 in
adamc@1217	2203 (st, Var r)
adamc@1217	2204 end
adamc@1217	2205 else
adamc@1217	2206 let
adamc@1217	2207 val (st, out) = St.nextVar st'
adamc@1217	2208
adamc@1217	2209 val p = Or (Reln (Eq, [Var out, i]),
adamc@1217	2210 And (Reln (Eq, [Var out, b]),
adamc@1217	2211 p'))
adamc@1217	2212 in
adamc@1217	2213 (St.setAmbient (st, p), Var out)
adamc@1217	2214 end
adamc@1210	2215
adamc@1218	2216 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
adamc@1212	2217
adamc@1227	2218 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used
adamc@1200	2219 in
adamc@1218	2220 (res, St.addPaths (St.setSent (st, sent), paths))
adamc@1200	2221 end
adamc@1220	2222 \| EDml e =>
adamc@1220	2223 (case parse dml e of
adamc@1220	2224 NONE => (print ("Warning: Information flow checker can't parse DML command at "
adamc@1220	2225 ^ ErrorMsg.spanToString loc ^ "\n");
adamc@1220	2226 default ())
adamc@1220	2227 \| SOME d =>
adamc@1220	2228 case d of
adamc@1220	2229 Insert (tab, es) =>
adamc@1220	2230 let
adamc@1220	2231 val (st, new) = St.nextVar st
adamc@1220	2232
adamc@1220	2233 fun rv st =
adamc@1220	2234 let
adamc@1220	2235 val (st, n) = St.nextVar st
adamc@1220	2236 in
adamc@1220	2237 (st, Var n)
adamc@1220	2238 end
adamc@1220	2239
adamc@1223	2240 val expIn = expIn rv env (fn _ => raise Fail "Iflow.evalExp: Bad field expression in INSERT")
adamc@1220	2241
adamc@1220	2242 val (es, st) = ListUtil.foldlMap
adamc@1220	2243 (fn ((x, e), st) =>
adamc@1220	2244 let
adamc@1220	2245 val (e, st) = case expIn (e, st) of
adamc@1220	2246 (inl e, st) => (e, st)
adamc@1220	2247 \| (inr _, _) => raise Fail
adamc@1220	2248 ("Iflow.evalExp: Selecting "
adamc@1220	2249 ^ "boolean expression")
adamc@1220	2250 in
adamc@1220	2251 ((x, e), st)
adamc@1220	2252 end)
adamc@1220	2253 st es
adamc@1220	2254 in
adamc@1220	2255 (Recd [], St.addInsert (st, (loc, And (St.ambient st,
adamc@1229	2256 Reln (Sql (tab ^ "$New"), [Recd es])))))
adamc@1221	2257 end
adamc@1221	2258 \| Delete (tab, e) =>
adamc@1221	2259 let
adamc@1221	2260 val (st, old) = St.nextVar st
adamc@1221	2261
adamc@1221	2262 fun rv st =
adamc@1221	2263 let
adamc@1221	2264 val (st, n) = St.nextVar st
adamc@1221	2265 in
adamc@1221	2266 (st, Var n)
adamc@1221	2267 end
adamc@1221	2268
adamc@1221	2269 val expIn = expIn rv env (fn "T" => Var old
adamc@1221	2270 \| _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
adamc@1221	2271
adamc@1221	2272 val (p, st) = case expIn (e, st) of
adamc@1221	2273 (inl e, _) => raise Fail "Iflow.evalExp: DELETE with non-boolean"
adamc@1221	2274 \| (inr p, st) => (p, st)
adamc@1221	2275
adamc@1221	2276 val p = And (p,
adamc@1221	2277 And (Reln (Sql "$Old", [Var old]),
adamc@1221	2278 Reln (Sql tab, [Var old])))
adamc@1230	2279
adamc@1230	2280 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
adamc@1221	2281 in
adamc@1221	2282 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
adamc@1223	2283 end
adamc@1223	2284 \| Update (tab, fs, e) =>
adamc@1223	2285 let
adamc@1223	2286 val (st, new) = St.nextVar st
adamc@1223	2287 val (st, old) = St.nextVar st
adamc@1223	2288
adamc@1223	2289 fun rv st =
adamc@1223	2290 let
adamc@1223	2291 val (st, n) = St.nextVar st
adamc@1223	2292 in
adamc@1223	2293 (st, Var n)
adamc@1223	2294 end
adamc@1223	2295
adamc@1223	2296 val expIn = expIn rv env (fn "T" => Var old
adamc@1223	2297 \| _ => raise Fail "Iflow.evalExp: Bad field expression in UPDATE")
adamc@1223	2298
adamc@1223	2299 val (fs, st) = ListUtil.foldlMap
adamc@1223	2300 (fn ((x, e), st) =>
adamc@1223	2301 let
adamc@1223	2302 val (e, st) = case expIn (e, st) of
adamc@1223	2303 (inl e, st) => (e, st)
adamc@1223	2304 \| (inr _, _) => raise Fail
adamc@1223	2305 ("Iflow.evalExp: Selecting "
adamc@1223	2306 ^ "boolean expression")
adamc@1223	2307 in
adamc@1223	2308 ((x, e), st)
adamc@1223	2309 end)
adamc@1223	2310 st fs
adamc@1223	2311
adamc@1226	2312 val fs' = case SM.find (!tabs, tab) of
adamc@1224	2313 NONE => raise Fail "Iflow.evalExp: Updating unknown table"
adamc@1226	2314 \| SOME (fs', _) => fs'
adamc@1224	2315
adamc@1224	2316 val fs = foldl (fn (f, fs) =>
adamc@1224	2317 if List.exists (fn (f', _) => f' = f) fs then
adamc@1224	2318 fs
adamc@1224	2319 else
adamc@1224	2320 (f, Proj (Var old, f)) :: fs) fs fs'
adamc@1224	2321
adamc@1223	2322 val (p, st) = case expIn (e, st) of
adamc@1223	2323 (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
adamc@1223	2324 \| (inr p, st) => (p, st)
adamc@1223	2325
adamc@1223	2326 val p = And (p,
adamc@1229	2327 And (Reln (Sql (tab ^ "$New"), [Recd fs]),
adamc@1223	2328 And (Reln (Sql "$Old", [Var old]),
adamc@1223	2329 Reln (Sql tab, [Var old]))))
adamc@1230	2330
adamc@1230	2331 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
adamc@1223	2332 in
adamc@1223	2333 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
adamc@1220	2334 end)
adamc@1220	2335
adamc@1229	2336 \| ENextval (EPrim (Prim.String seq), _) =>
adamc@1229	2337 let
adamc@1229	2338 val (st, nv) = St.nextVar st
adamc@1229	2339 in
adamc@1229	2340 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv]))))
adamc@1229	2341 end
adamc@1200	2342 \| ENextval _ => default ()
adamc@1200	2343 \| ESetval _ => default ()
adamc@1200	2344
adamc@1213	2345 \| EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1217	2346 let
adamc@1217	2347 val (st, nv) = St.nextVar st
adamc@1217	2348 in
adamc@1217	2349 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
adamc@1217	2350 end
adamc@1213	2351
adamc@1200	2352 \| EUnurlify _ => default ()
adamc@1200	2353 \| EJavaScript _ => default ()
adamc@1200	2354 \| ESignalReturn _ => default ()
adamc@1200	2355 \| ESignalBind _ => default ()
adamc@1200	2356 \| ESignalSource _ => default ()
adamc@1200	2357 \| EServerCall _ => default ()
adamc@1200	2358 \| ERecv _ => default ()
adamc@1200	2359 \| ESleep _ => default ()
adamc@1200	2360 \| ESpawn _ => default ()
adamc@1200	2361 end
adamc@1200	2362
adamc@1200	2363 fun check file =
adamc@1200	2364 let
adamc@1213	2365 val file = MonoReduce.reduce file
adamc@1213	2366 val file = MonoOpt.optimize file
adamc@1213	2367 val file = Fuse.fuse file
adamc@1213	2368 val file = MonoOpt.optimize file
adamc@1216	2369 val file = MonoShake.shake file
adamc@1213	2370 (val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file))
adamc@1213	2371
adamc@1207	2372 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207	2373 case d of
adamc@1207	2374 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207	2375 \| _ => exptd) IS.empty file
adamc@1207	2376
adamc@1223	2377 fun decl ((d, _), (vals, inserts, deletes, updates, client, insert, delete, update)) =
adamc@1200	2378 case d of
adamc@1226	2379 DTable (tab, fs, pk, _) =>
adamc@1226	2380 let
adamc@1226	2381 val ks =
adamc@1226	2382 case #1 pk of
adamc@1226	2383 EPrim (Prim.String s) =>
adamc@1226	2384 (case String.tokens (fn ch => ch = #"," orelse ch = #" ") s of
adamc@1226	2385 [] => []
adamc@1226	2386 \| pk => [pk])
adamc@1226	2387 \| _ => []
adamc@1226	2388 in
adamc@1226	2389 if size tab >= 3 then
adamc@1226	2390 (tabs := SM.insert (!tabs, String.extract (tab, 3, NONE),
adamc@1226	2391 (map #1 fs,
adamc@1226	2392 map (map (fn s => str (Char.toUpper (String.sub (s, 3)))
adamc@1226	2393 ^ String.extract (s, 4, NONE))) ks));
adamc@1226	2394 (vals, inserts, deletes, updates, client, insert, delete, update))
adamc@1226	2395 else
adamc@1226	2396 raise Fail "Table name does not begin with uw_"
adamc@1226	2397 end
adamc@1224	2398 \| DVal (_, n, _, e, _) =>
adamc@1200	2399 let
adamc@1207	2400 val isExptd = IS.member (exptd, n)
adamc@1207	2401
adamc@1207	2402 fun deAbs (e, env, nv, p) =
adamc@1200	2403 case #1 e of
adamc@1207	2404 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207	2405 if isExptd then
adamc@1207	2406 And (p, Reln (Known, [Var nv]))
adamc@1207	2407 else
adamc@1207	2408 p)
adamc@1207	2409 \| _ => (e, env, nv, p)
adamc@1200	2410
adamc@1207	2411 val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200	2412
adamc@1217	2413 val (_, st) = evalExp env (e, St.create {Var = nv,
adamc@1217	2414 Ambient = p})
adamc@1200	2415 in
adamc@1223	2416 (St.sent st @ vals, St.inserted st @ inserts, St.deleted st @ deletes, St.updated st @ updates,
adamc@1223	2417 client, insert, delete, update)
adamc@1200	2418 end
adamc@1202	2419
adamc@1220	2420 \| DPolicy pol =>
adamc@1218	2421 let
adamc@1220	2422 fun rv rvN = (rvN + 1, Lvar rvN)
adamc@1218	2423 in
adamc@1220	2424 case pol of
adamc@1220	2425 PolClient e =>
adamc@1220	2426 let
adamc@1227	2427 val (_, p, _, outs) = queryProp [] 0 rv SomeCol e
adamc@1220	2428 in
adamc@1223	2429 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
adamc@1220	2430 end
adamc@1220	2431 \| PolInsert e =>
adamc@1220	2432 let
adamc@1220	2433 val p = insertProp 0 rv e
adamc@1220	2434 in
adamc@1223	2435 (vals, inserts, deletes, updates, client, p :: insert, delete, update)
adamc@1221	2436 end
adamc@1221	2437 \| PolDelete e =>
adamc@1221	2438 let
adamc@1221	2439 val p = deleteProp 0 rv e
adamc@1221	2440 in
adamc@1223	2441 (vals, inserts, deletes, updates, client, insert, p :: delete, update)
adamc@1223	2442 end
adamc@1223	2443 \| PolUpdate e =>
adamc@1223	2444 let
adamc@1223	2445 val p = updateProp 0 rv e
adamc@1223	2446 in
adamc@1223	2447 (vals, inserts, deletes, updates, client, insert, delete, p :: update)
adamc@1220	2448 end
adamc@1229	2449 \| PolSequence e =>
adamc@1229	2450 (case #1 e of
adamc@1229	2451 EPrim (Prim.String seq) =>
adamc@1229	2452 let
adamc@1229	2453 val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
adamc@1229	2454 val outs = [Lvar 0]
adamc@1229	2455 in
adamc@1229	2456 (vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
adamc@1229	2457 end
adamc@1229	2458 \| _ => (vals, inserts, deletes, updates, client, insert, delete, update))
adamc@1218	2459 end
adamc@1214	2460
adamc@1223	2461 \| _ => (vals, inserts, deletes, updates, client, insert, delete, update)
adamc@1202	2462
adamc@1203	2463 val () = reset ()
adamc@1202	2464
adamc@1223	2465 val (vals, inserts, deletes, updates, client, insert, delete, update) =
adamc@1223	2466 foldl decl ([], [], [], [], [], [], [], []) file
adamc@1220	2467
adamc@1224	2468
adamc@1220	2469 val decompH = decomp true (fn (e1, e2) => e1 andalso e2 ())
adamc@1220	2470 val decompG = decomp false (fn (e1, e2) => e1 orelse e2 ())
adamc@1221	2471
adamc@1221	2472 fun doDml (cmds, pols) =
adamc@1221	2473 app (fn (loc, p) =>
adamc@1221	2474 if decompH p
adamc@1221	2475 (fn hyps =>
adamc@1231	2476 let
adamc@1231	2477 val cc = ccOf hyps
adamc@1231	2478 in
adamc@1231	2479 List.exists (fn p' =>
adamc@1231	2480 if decompG p'
adamc@1231	2481 (fn goals => imply (cc, hyps, goals, NONE)) then
adamc@1231	2482 ((*reset ();
adamc@1231	2483 Print.prefaces "Match" [("hyp", p_prop p),
adamc@1231	2484 ("goal", p_prop p')];*)
adamc@1231	2485 true)
adamc@1231	2486 else
adamc@1231	2487 false)
adamc@1231	2488 pols
adamc@1231	2489 end handle Cc.Contradiction => true) then
adamc@1221	2490 ()
adamc@1221	2491 else
adamc@1221	2492 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1221	2493 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
adamc@1200	2494 in
adamc@1218	2495 app (fn ((loc, e, p), fl) =>
adamc@1207	2496 let
adamc@1213	2497 fun doOne e =
adamc@1213	2498 let
adamc@1213	2499 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213	2500 in
adamc@1220	2501 if decompH p
adamc@1220	2502 (fn hyps =>
adamc@1228	2503 let
adamc@1231	2504 val cc = ccOf hyps
adamc@1231	2505
adamc@1232	2506 fun relevant () =
adamc@1232	2507 let
adamc@1232	2508 val avail = foldl (fn (AReln (Sql tab, _), avail) =>
adamc@1232	2509 SS.add (avail, tab)
adamc@1232	2510 \| (_, avail) => avail) SS.empty hyps
adamc@1232	2511 in
adamc@1232	2512 List.filter
adamc@1232	2513 (fn (g1, _) =>
adamc@1232	2514 decompG g1
adamc@1232	2515 (List.all (fn AReln (Sql tab, _) =>
adamc@1232	2516 SS.member (avail, tab)
adamc@1232	2517 \| _ => true))) client
adamc@1232	2518 end
adamc@1228	2519
adamc@1228	2520 fun tryCombos (maxLv, pols, g, outs) =
adamc@1228	2521 case pols of
adamc@1228	2522 [] =>
adamc@1228	2523 decompG g
adamc@1231	2524 (fn goals => imply (cc, hyps, goals, SOME outs))
adamc@1228	2525 \| (g1, outs1) :: pols =>
adamc@1228	2526 let
adamc@1228	2527 val g1 = bumpLvarsP (maxLv + 1) g1
adamc@1228	2528 val outs1 = map (bumpLvars (maxLv + 1)) outs1
adamc@1228	2529 fun skip () = tryCombos (maxLv, pols, g, outs)
adamc@1228	2530 in
adamc@1232	2531 skip ()
adamc@1232	2532 orelse tryCombos (Int.max (maxLv,
adamc@1232	2533 maxLvarP g1),
adamc@1232	2534 pols,
adamc@1232	2535 And (g1, g),
adamc@1232	2536 outs1 @ outs)
adamc@1228	2537 end
adamc@1228	2538 in
adamc@1228	2539 (fl <> Control Where
adamc@1231	2540 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
adamc@1228	2541 orelse List.exists (fn (p', outs) =>
adamc@1228	2542 decompG p'
adamc@1231	2543 (fn goals => imply (cc, hyps, goals,
adamc@1231	2544 SOME outs)))
adamc@1228	2545 client
adamc@1232	2546 orelse tryCombos (0, relevant (), True, [])
adamc@1228	2547 orelse (reset ();
adamc@1229	2548 Print.preface ("Untenable hypotheses"
adamc@1229	2549 ^ (case fl of
adamc@1229	2550 Control Where => " (WHERE clause)"
adamc@1229	2551 \| Control Case => " (case discriminee)"
adamc@1229	2552 \| Data => " (returned data value)"),
adamc@1228	2553 Print.p_list p_atom hyps);
adamc@1228	2554 false)
adamc@1231	2555 end handle Cc.Contradiction => true) then
adamc@1213	2556 ()
adamc@1213	2557 else
adamc@1228	2558 ErrorMsg.errorAt loc "The information flow policy may be violated here."
adamc@1213	2559 end
adamc@1213	2560
adamc@1213	2561 fun doAll e =
adamc@1213	2562 case e of
adamc@1213	2563 Const _ => ()
adamc@1213	2564 \| Var _ => doOne e
adamc@1213	2565 \| Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1216	2566 \| Func (UnCon _, [_]) => doOne e
adamc@1215	2567 \| Func (_, es) => app doAll es
adamc@1213	2568 \| Recd xes => app (doAll o #2) xes
adamc@1213	2569 \| Proj _ => doOne e
adamc@1213	2570 \| Finish => ()
adamc@1207	2571 in
adamc@1213	2572 doAll e
adamc@1220	2573 end) vals;
adamc@1220	2574
adamc@1221	2575 doDml (inserts, insert);
adamc@1223	2576 doDml (deletes, delete);
adamc@1223	2577 doDml (updates, update)
adamc@1200	2578 end
adamc@1200	2579
adamc@1213	2580 val check = fn file =>
adamc@1213	2581 let
adamc@1213	2582 val oldInline = Settings.getMonoInline ()
adamc@1213	2583 in
adamc@1213	2584 (Settings.setMonoInline (case Int.maxInt of
adamc@1213	2585 NONE => 1000000
adamc@1213	2586 \| SOME n => n);
adamc@1213	2587 check file;
adamc@1213	2588 Settings.setMonoInline oldInline)
adamc@1213	2589 handle ex => (Settings.setMonoInline oldInline;
adamc@1213	2590 raise ex)
adamc@1213	2591 end
adamc@1213	2592
adamc@1200	2593 end

Mercurial > urweb

annotate src/iflow.sml @ 1232:efbefd6e3f6c