Mercurial > urweb

annotate src/iflow.sml @ 1244:1eedc9086e6c

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