Ur/Web: src/iflow.sml annotate

annotate src/iflow.sml @ 1282:a9a500d22ebc

Roll back WHERE checking

author	Adam Chlipala <adam@chlipala.net>
date	Tue, 27 Jul 2010 14:04:09 -0400
parents	60e19545841b
children	acabf3935060

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

Mercurial > urweb

annotate src/iflow.sml @ 1282:a9a500d22ebc