Mercurial > urweb

annotate src/iflow.sml @ 1245:5c2555dfce8f

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