Mercurial > urweb

annotate src/iflow.sml @ 1243:e754dc92c47c

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