Mercurial > urweb

annotate src/iflow.sml @ 1217:4d206e603300

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Abstract type for evalExp state; handle WHERE conditions soundly
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 10:24:13 -0400
parents 09caa8c780e5
children 48d2ca496d2c
rev   line source
adamc@1200 1 (* Copyright (c) 2010, Adam Chlipala
adamc@1200 2 * All rights reserved.
adamc@1200 3 *
adamc@1200 4 * Redistribution and use in source and binary forms, with or without
adamc@1200 5 * modification, are permitted provided that the following conditions are met:
adamc@1200 6 *
adamc@1200 7 * - Redistributions of source code must retain the above copyright notice,
adamc@1200 8 * this list of conditions and the following disclaimer.
adamc@1200 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@1200 10 * this list of conditions and the following disclaimer in the documentation
adamc@1200 11 * and/or other materials provided with the distribution.
adamc@1200 12 * - The names of contributors may not be used to endorse or promote products
adamc@1200 13 * derived from this software without specific prior written permission.
adamc@1200 14 *
adamc@1200 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@1200 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@1200 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@1200 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@1200 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@1200 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@1200 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@1200 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@1200 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@1200 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@1200 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@1200 26 *)
adamc@1200 27
adamc@1200 28 structure Iflow :> IFLOW = struct
adamc@1200 29
adamc@1200 30 open Mono
adamc@1200 31
adamc@1207 32 structure IS = IntBinarySet
adamc@1202 33 structure IM = IntBinaryMap
adamc@1202 34
adamc@1215 35 structure SK = struct
adamc@1215 36 type ord_key = string
adamc@1215 37 val compare = String.compare
adamc@1215 38 end
adamc@1215 39
adamc@1215 40 structure SS = BinarySetFn(SK)
adamc@1215 41 structure SM = BinaryMapFn(SK)
adamc@1200 42
adamc@1200 43 val writers = ["htmlifyInt_w",
adamc@1200 44 "htmlifyFloat_w",
adamc@1200 45 "htmlifyString_w",
adamc@1200 46 "htmlifyBool_w",
adamc@1200 47 "htmlifyTime_w",
adamc@1200 48 "attrifyInt_w",
adamc@1200 49 "attrifyFloat_w",
adamc@1200 50 "attrifyString_w",
adamc@1200 51 "attrifyChar_w",
adamc@1200 52 "urlifyInt_w",
adamc@1200 53 "urlifyFloat_w",
adamc@1200 54 "urlifyString_w",
adamc@1213 55 "urlifyBool_w",
adamc@1213 56 "set_cookie"]
adamc@1200 57
adamc@1200 58 val writers = SS.addList (SS.empty, writers)
adamc@1200 59
adamc@1200 60 type lvar = int
adamc@1200 61
adamc@1215 62 datatype func =
adamc@1215 63 DtCon0 of string
adamc@1215 64 | DtCon1 of string
adamc@1215 65 | UnCon of string
adamc@1215 66 | Other of string
adamc@1215 67
adamc@1200 68 datatype exp =
adamc@1200 69 Const of Prim.t
adamc@1200 70 | Var of int
adamc@1200 71 | Lvar of lvar
adamc@1215 72 | Func of func * exp list
adamc@1200 73 | Recd of (string * exp) list
adamc@1200 74 | Proj of exp * string
adamc@1200 75 | Finish
adamc@1200 76
adamc@1200 77 datatype reln =
adamc@1207 78 Known
adamc@1207 79 | Sql of string
adamc@1215 80 | PCon0 of string
adamc@1215 81 | PCon1 of string
adamc@1200 82 | Eq
adamc@1210 83 | Ne
adamc@1210 84 | Lt
adamc@1210 85 | Le
adamc@1210 86 | Gt
adamc@1210 87 | Ge
adamc@1200 88
adamc@1200 89 datatype prop =
adamc@1200 90 True
adamc@1200 91 | False
adamc@1200 92 | Unknown
adamc@1200 93 | And of prop * prop
adamc@1200 94 | Or of prop * prop
adamc@1200 95 | Reln of reln * exp list
adamc@1212 96 | Cond of exp * prop
adamc@1200 97
adamc@1215 98 val unif = ref (IM.empty : exp IM.map)
adamc@1215 99
adamc@1215 100 fun reset () = unif := IM.empty
adamc@1215 101 fun save () = !unif
adamc@1215 102 fun restore x = unif := x
adamc@1215 103
adamc@1200 104 local
adamc@1207 105 open Print
adamc@1207 106 val string = PD.string
adamc@1207 107 in
adamc@1207 108
adamc@1215 109 fun p_func f =
adamc@1215 110 string (case f of
adamc@1215 111 DtCon0 s => s
adamc@1215 112 | DtCon1 s => s
adamc@1215 113 | UnCon s => "un" ^ s
adamc@1215 114 | Other s => s)
adamc@1215 115
adamc@1207 116 fun p_exp e =
adamc@1207 117 case e of
adamc@1207 118 Const p => Prim.p_t p
adamc@1207 119 | Var n => string ("x" ^ Int.toString n)
adamc@1215 120 | Lvar n =>
adamc@1215 121 (case IM.find (!unif, n) of
adamc@1215 122 NONE => string ("X" ^ Int.toString n)
adamc@1215 123 | SOME e => p_exp e)
adamc@1215 124 | Func (f, es) => box [p_func f,
adamc@1215 125 string "(",
adamc@1207 126 p_list p_exp es,
adamc@1207 127 string ")"]
adamc@1207 128 | Recd xes => box [string "{",
adamc@1210 129 p_list (fn (x, e) => box [string x,
adamc@1207 130 space,
adamc@1207 131 string "=",
adamc@1207 132 space,
adamc@1207 133 p_exp e]) xes,
adamc@1207 134 string "}"]
adamc@1207 135 | Proj (e, x) => box [p_exp e,
adamc@1207 136 string ("." ^ x)]
adamc@1207 137 | Finish => string "FINISH"
adamc@1207 138
adamc@1210 139 fun p_bop s es =
adamc@1210 140 case es of
adamc@1210 141 [e1, e2] => box [p_exp e1,
adamc@1210 142 space,
adamc@1210 143 string s,
adamc@1210 144 space,
adamc@1210 145 p_exp e2]
adamc@1210 146 | _ => raise Fail "Iflow.p_bop"
adamc@1210 147
adamc@1207 148 fun p_reln r es =
adamc@1207 149 case r of
adamc@1207 150 Known =>
adamc@1207 151 (case es of
adamc@1207 152 [e] => box [string "known(",
adamc@1207 153 p_exp e,
adamc@1207 154 string ")"]
adamc@1207 155 | _ => raise Fail "Iflow.p_reln: Known")
adamc@1207 156 | Sql s => box [string (s ^ "("),
adamc@1207 157 p_list p_exp es,
adamc@1207 158 string ")"]
adamc@1215 159 | PCon0 s => box [string (s ^ "("),
adamc@1215 160 p_list p_exp es,
adamc@1215 161 string ")"]
adamc@1215 162 | PCon1 s => box [string (s ^ "("),
adamc@1211 163 p_list p_exp es,
adamc@1211 164 string ")"]
adamc@1210 165 | Eq => p_bop "=" es
adamc@1210 166 | Ne => p_bop "<>" es
adamc@1210 167 | Lt => p_bop "<" es
adamc@1210 168 | Le => p_bop "<=" es
adamc@1210 169 | Gt => p_bop ">" es
adamc@1210 170 | Ge => p_bop ">=" es
adamc@1207 171
adamc@1207 172 fun p_prop p =
adamc@1207 173 case p of
adamc@1207 174 True => string "True"
adamc@1207 175 | False => string "False"
adamc@1207 176 | Unknown => string "??"
adamc@1207 177 | And (p1, p2) => box [string "(",
adamc@1207 178 p_prop p1,
adamc@1207 179 string ")",
adamc@1207 180 space,
adamc@1207 181 string "&&",
adamc@1207 182 space,
adamc@1207 183 string "(",
adamc@1207 184 p_prop p2,
adamc@1207 185 string ")"]
adamc@1207 186 | Or (p1, p2) => box [string "(",
adamc@1207 187 p_prop p1,
adamc@1207 188 string ")",
adamc@1207 189 space,
adamc@1207 190 string "||",
adamc@1207 191 space,
adamc@1207 192 string "(",
adamc@1207 193 p_prop p2,
adamc@1207 194 string ")"]
adamc@1207 195 | Reln (r, es) => p_reln r es
adamc@1212 196 | Cond (e, p) => box [string "(",
adamc@1212 197 p_exp e,
adamc@1212 198 space,
adamc@1212 199 string "==",
adamc@1212 200 space,
adamc@1212 201 p_prop p,
adamc@1212 202 string ")"]
adamc@1207 203
adamc@1207 204 end
adamc@1207 205
adamc@1207 206 local
adamc@1202 207 val count = ref 1
adamc@1200 208 in
adamc@1200 209 fun newLvar () =
adamc@1200 210 let
adamc@1200 211 val n = !count
adamc@1200 212 in
adamc@1200 213 count := n + 1;
adamc@1200 214 n
adamc@1200 215 end
adamc@1200 216 end
adamc@1200 217
adamc@1200 218 fun isKnown e =
adamc@1200 219 case e of
adamc@1200 220 Const _ => true
adamc@1200 221 | Func (_, es) => List.all isKnown es
adamc@1200 222 | Recd xes => List.all (isKnown o #2) xes
adamc@1200 223 | Proj (e, _) => isKnown e
adamc@1200 224 | _ => false
adamc@1200 225
adamc@1200 226 fun isFinish e =
adamc@1200 227 case e of
adamc@1200 228 Finish => true
adamc@1200 229 | _ => false
adamc@1200 230
adamc@1200 231 fun simplify e =
adamc@1200 232 case e of
adamc@1200 233 Const _ => e
adamc@1200 234 | Var _ => e
adamc@1208 235 | Lvar n =>
adamc@1208 236 (case IM.find (!unif, n) of
adamc@1208 237 NONE => e
adamc@1208 238 | SOME e => simplify e)
adamc@1215 239 | Func (f, es) => Func (f, map simplify es)
adamc@1215 240 | Recd xes => Recd (map (fn (x, e) => (x, simplify e)) xes)
adamc@1215 241 | Proj (e, s) => Proj (simplify e, s)
adamc@1200 242 | Finish => Finish
adamc@1200 243
adamc@1212 244 datatype atom =
adamc@1212 245 AReln of reln * exp list
adamc@1212 246 | ACond of exp * prop
adamc@1212 247
adamc@1212 248 fun p_atom a =
adamc@1212 249 p_prop (case a of
adamc@1212 250 AReln x => Reln x
adamc@1212 251 | ACond x => Cond x)
adamc@1212 252
adamc@1202 253 fun lvarIn lv =
adamc@1202 254 let
adamc@1202 255 fun lvi e =
adamc@1202 256 case e of
adamc@1202 257 Const _ => false
adamc@1202 258 | Var _ => false
adamc@1202 259 | Lvar lv' => lv' = lv
adamc@1202 260 | Func (_, es) => List.exists lvi es
adamc@1202 261 | Recd xes => List.exists (lvi o #2) xes
adamc@1202 262 | Proj (e, _) => lvi e
adamc@1202 263 | Finish => false
adamc@1202 264 in
adamc@1202 265 lvi
adamc@1202 266 end
adamc@1202 267
adamc@1212 268 fun lvarInP lv =
adamc@1212 269 let
adamc@1212 270 fun lvi p =
adamc@1212 271 case p of
adamc@1212 272 True => false
adamc@1212 273 | False => false
adamc@1212 274 | Unknown => true
adamc@1212 275 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 276 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 277 | Reln (_, es) => List.exists (lvarIn lv) es
adamc@1212 278 | Cond (e, p) => lvarIn lv e orelse lvi p
adamc@1212 279 in
adamc@1212 280 lvi
adamc@1212 281 end
adamc@1212 282
adamc@1212 283 fun varIn lv =
adamc@1212 284 let
adamc@1212 285 fun lvi e =
adamc@1212 286 case e of
adamc@1212 287 Const _ => false
adamc@1212 288 | Lvar _ => false
adamc@1212 289 | Var lv' => lv' = lv
adamc@1212 290 | Func (_, es) => List.exists lvi es
adamc@1212 291 | Recd xes => List.exists (lvi o #2) xes
adamc@1212 292 | Proj (e, _) => lvi e
adamc@1212 293 | Finish => false
adamc@1212 294 in
adamc@1212 295 lvi
adamc@1212 296 end
adamc@1212 297
adamc@1212 298 fun varInP lv =
adamc@1212 299 let
adamc@1212 300 fun lvi p =
adamc@1212 301 case p of
adamc@1212 302 True => false
adamc@1212 303 | False => false
adamc@1212 304 | Unknown => false
adamc@1212 305 | And (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 306 | Or (p1, p2) => lvi p1 orelse lvi p2
adamc@1212 307 | Reln (_, es) => List.exists (varIn lv) es
adamc@1212 308 | Cond (e, p) => varIn lv e orelse lvi p
adamc@1212 309 in
adamc@1212 310 lvi
adamc@1212 311 end
adamc@1212 312
adamc@1202 313 fun eq' (e1, e2) =
adamc@1202 314 case (e1, e2) of
adamc@1202 315 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202 316 | (Var n1, Var n2) => n1 = n2
adamc@1202 317
adamc@1202 318 | (Lvar n1, _) =>
adamc@1202 319 (case IM.find (!unif, n1) of
adamc@1202 320 SOME e1 => eq' (e1, e2)
adamc@1202 321 | NONE =>
adamc@1202 322 case e2 of
adamc@1202 323 Lvar n2 =>
adamc@1202 324 (case IM.find (!unif, n2) of
adamc@1202 325 SOME e2 => eq' (e1, e2)
adamc@1202 326 | NONE => n1 = n2
adamc@1208 327 orelse (unif := IM.insert (!unif, n2, e1);
adamc@1202 328 true))
adamc@1202 329 | _ =>
adamc@1202 330 if lvarIn n1 e2 then
adamc@1202 331 false
adamc@1202 332 else
adamc@1202 333 (unif := IM.insert (!unif, n1, e2);
adamc@1202 334 true))
adamc@1202 335
adamc@1202 336 | (_, Lvar n2) =>
adamc@1202 337 (case IM.find (!unif, n2) of
adamc@1202 338 SOME e2 => eq' (e1, e2)
adamc@1202 339 | NONE =>
adamc@1202 340 if lvarIn n2 e1 then
adamc@1202 341 false
adamc@1202 342 else
adamc@1213 343 ((*Print.prefaces "unif" [("n2", Print.PD.string (Int.toString n2)),
adamc@1213 344 ("e1", p_exp e1)];*)
adamc@1213 345 unif := IM.insert (!unif, n2, e1);
adamc@1202 346 true))
adamc@1202 347
adamc@1202 348 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202 349 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202 350 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202 351 | (Finish, Finish) => true
adamc@1202 352 | _ => false
adamc@1202 353
adamc@1202 354 fun eq (e1, e2) =
adamc@1202 355 let
adamc@1203 356 val saved = save ()
adamc@1202 357 in
adamc@1202 358 if eq' (simplify e1, simplify e2) then
adamc@1202 359 true
adamc@1202 360 else
adamc@1203 361 (restore saved;
adamc@1202 362 false)
adamc@1202 363 end
adamc@1202 364
adamc@1208 365 val debug = ref false
adamc@1208 366
adamc@1211 367 fun eeq (e1, e2) =
adamc@1211 368 case (e1, e2) of
adamc@1211 369 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1211 370 | (Var n1, Var n2) => n1 = n2
adamc@1211 371 | (Lvar n1, Lvar n2) => n1 = n2
adamc@1211 372 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eeq (es1, es2)
adamc@1211 373 | (Recd xes1, Recd xes2) => length xes1 = length xes2 andalso
adamc@1211 374 List.all (fn (x2, e2) =>
adamc@1211 375 List.exists (fn (x1, e1) => x1 = x2 andalso eeq (e1, e2)) xes2) xes1
adamc@1211 376 | (Proj (e1, x1), Proj (e2, x2)) => eeq (e1, e2) andalso x1 = x2
adamc@1211 377 | (Finish, Finish) => true
adamc@1211 378 | _ => false
adamc@1211 379
adamc@1208 380 (* Congruence closure *)
adamc@1208 381 structure Cc :> sig
adamc@1215 382 type database
adamc@1215 383 type representative
adamc@1215 384
adamc@1215 385 exception Contradiction
adamc@1215 386 exception Undetermined
adamc@1215 387
adamc@1215 388 val database : unit -> database
adamc@1215 389 val representative : database * exp -> representative
adamc@1215 390
adamc@1215 391 val assert : database * atom -> unit
adamc@1215 392 val check : database * atom -> bool
adamc@1215 393
adamc@1215 394 val p_database : database Print.printer
adamc@1208 395 end = struct
adamc@1208 396
adamc@1215 397 exception Contradiction
adamc@1215 398 exception Undetermined
adamc@1208 399
adamc@1215 400 structure CM = BinaryMapFn(struct
adamc@1215 401 type ord_key = Prim.t
adamc@1215 402 val compare = Prim.compare
adamc@1215 403 end)
adamc@1208 404
adamc@1215 405 datatype node = Node of {Rep : node ref option ref,
adamc@1215 406 Cons : node ref SM.map ref,
adamc@1215 407 Variety : variety,
adamc@1215 408 Known : bool ref}
adamc@1208 409
adamc@1215 410 and variety =
adamc@1215 411 Dt0 of string
adamc@1215 412 | Dt1 of string * node ref
adamc@1215 413 | Prim of Prim.t
adamc@1215 414 | Recrd of node ref SM.map ref
adamc@1215 415 | VFinish
adamc@1215 416 | Nothing
adamc@1208 417
adamc@1215 418 type representative = node ref
adamc@1215 419
adamc@1215 420 val finish = ref (Node {Rep = ref NONE,
adamc@1215 421 Cons = ref SM.empty,
adamc@1215 422 Variety = VFinish,
adamc@1215 423 Known = ref false})
adamc@1215 424
adamc@1215 425 type database = {Vars : representative IM.map ref,
adamc@1215 426 Consts : representative CM.map ref,
adamc@1215 427 Con0s : representative SM.map ref,
adamc@1215 428 Records : (representative SM.map * representative) list ref,
adamc@1215 429 Funcs : ((string * representative list) * representative) list ref }
adamc@1215 430
adamc@1215 431 fun database () = {Vars = ref IM.empty,
adamc@1215 432 Consts = ref CM.empty,
adamc@1215 433 Con0s = ref SM.empty,
adamc@1215 434 Records = ref [],
adamc@1215 435 Funcs = ref []}
adamc@1215 436
adamc@1215 437 fun unNode n =
adamc@1215 438 case !n of
adamc@1215 439 Node r => r
adamc@1215 440
adamc@1215 441 open Print
adamc@1215 442 val string = PD.string
adamc@1215 443 val newline = PD.newline
adamc@1215 444
adamc@1215 445 fun p_rep n =
adamc@1215 446 case !(#Rep (unNode n)) of
adamc@1215 447 SOME n => p_rep n
adamc@1215 448 | NONE =>
adamc@1215 449 case #Variety (unNode n) of
adamc@1215 450 Nothing => string ("?" ^ Int.toString (Unsafe.cast n))
adamc@1215 451 | Dt0 s => string ("Dt0(" ^ s ^ ")")
adamc@1215 452 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
adamc@1215 453 space,
adamc@1215 454 p_rep n,
adamc@1215 455 string ")"]
adamc@1215 456 | Prim p => Prim.p_t p
adamc@1215 457 | Recrd (ref m) => box [string "{",
adamc@1215 458 p_list (fn (x, n) => box [string x,
adamc@1215 459 space,
adamc@1215 460 string "=",
adamc@1215 461 space,
adamc@1215 462 p_rep n]) (SM.listItemsi m),
adamc@1215 463 string "}"]
adamc@1215 464 | VFinish => string "FINISH"
adamc@1215 465
adamc@1215 466 fun p_database (db : database) =
adamc@1215 467 box [string "Vars:",
adamc@1215 468 newline,
adamc@1215 469 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
adamc@1215 470 space,
adamc@1215 471 string "=",
adamc@1215 472 space,
adamc@1215 473 p_rep n]) (IM.listItemsi (!(#Vars db)))]
adamc@1215 474
adamc@1215 475 fun repOf (n : representative) : representative =
adamc@1215 476 case !(#Rep (unNode n)) of
adamc@1215 477 NONE => n
adamc@1215 478 | SOME r =>
adamc@1215 479 let
adamc@1215 480 val r = repOf r
adamc@1215 481 in
adamc@1215 482 #Rep (unNode n) := SOME r;
adamc@1215 483 r
adamc@1215 484 end
adamc@1215 485
adamc@1215 486 fun markKnown r =
adamc@1215 487 (#Known (unNode r) := true;
adamc@1215 488 case #Variety (unNode r) of
adamc@1215 489 Dt1 (_, r) => markKnown r
adamc@1215 490 | Recrd xes => SM.app markKnown (!xes)
adamc@1215 491 | _ => ())
adamc@1215 492
adamc@1215 493 fun representative (db : database, e) =
adamc@1208 494 let
adamc@1215 495 fun rep e =
adamc@1215 496 case e of
adamc@1215 497 Const p => (case CM.find (!(#Consts db), p) of
adamc@1215 498 SOME r => repOf r
adamc@1215 499 | NONE =>
adamc@1215 500 let
adamc@1215 501 val r = ref (Node {Rep = ref NONE,
adamc@1215 502 Cons = ref SM.empty,
adamc@1215 503 Variety = Prim p,
adamc@1215 504 Known = ref false})
adamc@1215 505 in
adamc@1215 506 #Consts db := CM.insert (!(#Consts db), p, r);
adamc@1215 507 r
adamc@1215 508 end)
adamc@1215 509 | Var n => (case IM.find (!(#Vars db), n) of
adamc@1215 510 SOME r => repOf r
adamc@1215 511 | NONE =>
adamc@1215 512 let
adamc@1215 513 val r = ref (Node {Rep = ref NONE,
adamc@1215 514 Cons = ref SM.empty,
adamc@1215 515 Variety = Nothing,
adamc@1215 516 Known = ref false})
adamc@1215 517 in
adamc@1215 518 #Vars db := IM.insert (!(#Vars db), n, r);
adamc@1215 519 r
adamc@1215 520 end)
adamc@1215 521 | Lvar n =>
adamc@1215 522 (case IM.find (!unif, n) of
adamc@1215 523 NONE => raise Undetermined
adamc@1215 524 | SOME e => rep e)
adamc@1215 525 | Func (DtCon0 f, []) => (case SM.find (!(#Con0s db), f) of
adamc@1215 526 SOME r => repOf r
adamc@1215 527 | NONE =>
adamc@1215 528 let
adamc@1215 529 val r = ref (Node {Rep = ref NONE,
adamc@1215 530 Cons = ref SM.empty,
adamc@1215 531 Variety = Dt0 f,
adamc@1215 532 Known = ref false})
adamc@1215 533 in
adamc@1215 534 #Con0s db := SM.insert (!(#Con0s db), f, r);
adamc@1215 535 r
adamc@1215 536 end)
adamc@1215 537 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
adamc@1215 538 | Func (DtCon1 f, [e]) =>
adamc@1215 539 let
adamc@1215 540 val r = rep e
adamc@1215 541 in
adamc@1215 542 case SM.find (!(#Cons (unNode r)), f) of
adamc@1215 543 SOME r => repOf r
adamc@1215 544 | NONE =>
adamc@1215 545 let
adamc@1215 546 val r' = ref (Node {Rep = ref NONE,
adamc@1215 547 Cons = ref SM.empty,
adamc@1215 548 Variety = Dt1 (f, r),
adamc@1216 549 Known = #Known (unNode r)})
adamc@1215 550 in
adamc@1215 551 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
adamc@1215 552 r'
adamc@1215 553 end
adamc@1215 554 end
adamc@1215 555 | Func (DtCon1 _, _) => raise Fail "Iflow.rep: DtCon1"
adamc@1215 556 | Func (UnCon f, [e]) =>
adamc@1215 557 let
adamc@1215 558 val r = rep e
adamc@1215 559 in
adamc@1215 560 case #Variety (unNode r) of
adamc@1215 561 Dt1 (f', n) => if f' = f then
adamc@1215 562 repOf n
adamc@1215 563 else
adamc@1215 564 raise Contradiction
adamc@1215 565 | Nothing =>
adamc@1215 566 let
adamc@1215 567 val cons = ref SM.empty
adamc@1215 568 val r' = ref (Node {Rep = ref NONE,
adamc@1215 569 Cons = cons,
adamc@1215 570 Variety = Nothing,
adamc@1216 571 Known = #Known (unNode r)})
adamc@1215 572
adamc@1215 573 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 574 Cons = #Cons (unNode r),
adamc@1215 575 Variety = Dt1 (f, r'),
adamc@1215 576 Known = #Known (unNode r)})
adamc@1215 577 in
adamc@1215 578 cons := SM.insert (!cons, f, r'');
adamc@1215 579 #Rep (unNode r) := SOME r'';
adamc@1215 580 r'
adamc@1215 581 end
adamc@1215 582 | VFinish => r
adamc@1215 583 | _ => raise Contradiction
adamc@1215 584 end
adamc@1215 585 | Func (UnCon _, _) => raise Fail "Iflow.rep: UnCon"
adamc@1215 586 | Func (Other f, es) =>
adamc@1215 587 let
adamc@1215 588 val rs = map rep es
adamc@1215 589 in
adamc@1215 590 case List.find (fn (x : string * representative list, _) => x = (f, rs)) (!(#Funcs db)) of
adamc@1215 591 NONE =>
adamc@1215 592 let
adamc@1215 593 val r = ref (Node {Rep = ref NONE,
adamc@1215 594 Cons = ref SM.empty,
adamc@1215 595 Variety = Nothing,
adamc@1215 596 Known = ref false})
adamc@1215 597 in
adamc@1215 598 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
adamc@1215 599 r
adamc@1215 600 end
adamc@1215 601 | SOME (_, r) => repOf r
adamc@1215 602 end
adamc@1215 603 | Recd xes =>
adamc@1215 604 let
adamc@1215 605 val xes = map (fn (x, e) => (x, rep e)) xes
adamc@1215 606 val len = length xes
adamc@1215 607 in
adamc@1215 608 case List.find (fn (xes', _) =>
adamc@1215 609 SM.numItems xes' = len
adamc@1215 610 andalso List.all (fn (x, n) =>
adamc@1215 611 case SM.find (xes', x) of
adamc@1215 612 NONE => false
adamc@1215 613 | SOME n' => n = repOf n') xes)
adamc@1215 614 (!(#Records db)) of
adamc@1215 615 SOME (_, r) => repOf r
adamc@1215 616 | NONE =>
adamc@1215 617 let
adamc@1215 618 val xes = foldl SM.insert' SM.empty xes
adamc@1215 619
adamc@1215 620 val r' = ref (Node {Rep = ref NONE,
adamc@1215 621 Cons = ref SM.empty,
adamc@1215 622 Variety = Recrd (ref xes),
adamc@1215 623 Known = ref false})
adamc@1215 624 in
adamc@1215 625 #Records db := (xes, r') :: (!(#Records db));
adamc@1215 626 r'
adamc@1215 627 end
adamc@1215 628 end
adamc@1215 629 | Proj (e, f) =>
adamc@1215 630 let
adamc@1215 631 val r = rep e
adamc@1215 632 in
adamc@1215 633 case #Variety (unNode r) of
adamc@1215 634 Recrd xes =>
adamc@1215 635 (case SM.find (!xes, f) of
adamc@1215 636 SOME r => repOf r
adamc@1216 637 | NONE => let
adamc@1215 638 val r = ref (Node {Rep = ref NONE,
adamc@1215 639 Cons = ref SM.empty,
adamc@1215 640 Variety = Nothing,
adamc@1216 641 Known = #Known (unNode r)})
adamc@1215 642 in
adamc@1215 643 xes := SM.insert (!xes, f, r);
adamc@1215 644 r
adamc@1215 645 end)
adamc@1215 646 | Nothing =>
adamc@1215 647 let
adamc@1215 648 val r' = ref (Node {Rep = ref NONE,
adamc@1215 649 Cons = ref SM.empty,
adamc@1215 650 Variety = Nothing,
adamc@1216 651 Known = #Known (unNode r)})
adamc@1215 652
adamc@1215 653 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 654 Cons = #Cons (unNode r),
adamc@1215 655 Variety = Recrd (ref (SM.insert (SM.empty, f, r'))),
adamc@1215 656 Known = #Known (unNode r)})
adamc@1215 657 in
adamc@1215 658 #Rep (unNode r) := SOME r'';
adamc@1215 659 r'
adamc@1215 660 end
adamc@1215 661 | VFinish => r
adamc@1215 662 | _ => raise Contradiction
adamc@1215 663 end
adamc@1215 664 | Finish => finish
adamc@1208 665 in
adamc@1215 666 rep e
adamc@1208 667 end
adamc@1208 668
adamc@1215 669 fun assert (db, a) =
adamc@1215 670 case a of
adamc@1215 671 ACond _ => ()
adamc@1215 672 | AReln x =>
adamc@1215 673 case x of
adamc@1215 674 (Known, [e]) => markKnown (representative (db, e))
adamc@1215 675 | (PCon0 f, [e]) =>
adamc@1215 676 let
adamc@1215 677 val r = representative (db, e)
adamc@1215 678 in
adamc@1215 679 case #Variety (unNode r) of
adamc@1215 680 Dt0 f' => if f = f' then
adamc@1215 681 ()
adamc@1215 682 else
adamc@1215 683 raise Contradiction
adamc@1215 684 | Nothing =>
adamc@1215 685 let
adamc@1215 686 val r' = ref (Node {Rep = ref NONE,
adamc@1215 687 Cons = ref SM.empty,
adamc@1215 688 Variety = Dt0 f,
adamc@1215 689 Known = ref false})
adamc@1215 690 in
adamc@1215 691 #Rep (unNode r) := SOME r'
adamc@1215 692 end
adamc@1215 693 | _ => raise Contradiction
adamc@1215 694 end
adamc@1215 695 | (PCon1 f, [e]) =>
adamc@1215 696 let
adamc@1215 697 val r = representative (db, e)
adamc@1215 698 in
adamc@1215 699 case #Variety (unNode r) of
adamc@1215 700 Dt1 (f', e') => if f = f' then
adamc@1215 701 ()
adamc@1215 702 else
adamc@1215 703 raise Contradiction
adamc@1215 704 | Nothing =>
adamc@1215 705 let
adamc@1215 706 val r'' = ref (Node {Rep = ref NONE,
adamc@1215 707 Cons = ref SM.empty,
adamc@1215 708 Variety = Nothing,
adamc@1215 709 Known = ref false})
adamc@1214 710
adamc@1215 711 val r' = ref (Node {Rep = ref NONE,
adamc@1215 712 Cons = ref SM.empty,
adamc@1215 713 Variety = Dt1 (f, r''),
adamc@1215 714 Known = ref false})
adamc@1215 715 in
adamc@1215 716 #Rep (unNode r) := SOME r'
adamc@1215 717 end
adamc@1215 718 | _ => raise Contradiction
adamc@1215 719 end
adamc@1215 720 | (Eq, [e1, e2]) =>
adamc@1215 721 let
adamc@1215 722 fun markEq (r1, r2) =
adamc@1215 723 if r1 = r2 then
adamc@1215 724 ()
adamc@1215 725 else case (#Variety (unNode r1), #Variety (unNode r2)) of
adamc@1215 726 (Prim p1, Prim p2) => if Prim.equal (p1, p2) then
adamc@1215 727 ()
adamc@1215 728 else
adamc@1215 729 raise Contradiction
adamc@1215 730 | (Dt0 f1, Dt0 f2) => if f1 = f2 then
adamc@1215 731 ()
adamc@1215 732 else
adamc@1215 733 raise Contradiction
adamc@1215 734 | (Dt1 (f1, r1), Dt1 (f2, r2)) => if f1 = f2 then
adamc@1215 735 markEq (r1, r2)
adamc@1215 736 else
adamc@1215 737 raise Contradiction
adamc@1215 738 | (Recrd xes1, Recrd xes2) =>
adamc@1215 739 let
adamc@1215 740 fun unif (xes1, xes2) =
adamc@1215 741 SM.appi (fn (x, r1) =>
adamc@1215 742 case SM.find (xes2, x) of
adamc@1215 743 NONE => ()
adamc@1215 744 | SOME r2 => markEq (r1, r2)) xes1
adamc@1215 745 in
adamc@1215 746 unif (!xes1, !xes2);
adamc@1215 747 unif (!xes2, !xes1)
adamc@1215 748 end
adamc@1215 749 | (VFinish, VFinish) => ()
adamc@1215 750 | (Nothing, _) =>
adamc@1215 751 (#Rep (unNode r1) := SOME r2;
adamc@1215 752 if !(#Known (unNode r1)) andalso not (!(#Known (unNode r2))) then
adamc@1215 753 markKnown r2
adamc@1215 754 else
adamc@1215 755 ();
adamc@1215 756 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
adamc@1215 757 compactFuncs ())
adamc@1215 758 | (_, Nothing) =>
adamc@1215 759 (#Rep (unNode r2) := SOME r1;
adamc@1215 760 if !(#Known (unNode r2)) andalso not (!(#Known (unNode r1))) then
adamc@1215 761 markKnown r1
adamc@1215 762 else
adamc@1215 763 ();
adamc@1215 764 #Cons (unNode r1) := SM.unionWith #1 (!(#Cons (unNode r1)), !(#Cons (unNode r2)));
adamc@1215 765 compactFuncs ())
adamc@1215 766 | _ => raise Contradiction
adamc@1214 767
adamc@1215 768 and compactFuncs () =
adamc@1214 769 let
adamc@1215 770 fun loop funcs =
adamc@1215 771 case funcs of
adamc@1215 772 [] => []
adamc@1215 773 | (fr as ((f, rs), r)) :: rest =>
adamc@1215 774 let
adamc@1215 775 val rest = List.filter (fn ((f' : string, rs'), r') =>
adamc@1215 776 if f' = f
adamc@1215 777 andalso ListPair.allEq (fn (r1, r2) =>
adamc@1215 778 repOf r1 = repOf r2)
adamc@1215 779 (rs, rs') then
adamc@1215 780 (markEq (r, r');
adamc@1215 781 false)
adamc@1215 782 else
adamc@1215 783 true) rest
adamc@1215 784 in
adamc@1215 785 fr :: loop rest
adamc@1215 786 end
adamc@1214 787 in
adamc@1215 788 #Funcs db := loop (!(#Funcs db))
adamc@1214 789 end
adamc@1215 790 in
adamc@1215 791 markEq (representative (db, e1), representative (db, e2))
adamc@1215 792 end
adamc@1215 793 | _ => ()
adamc@1214 794
adamc@1215 795 fun check (db, a) =
adamc@1215 796 case a of
adamc@1215 797 ACond _ => false
adamc@1215 798 | AReln x =>
adamc@1215 799 case x of
adamc@1215 800 (Known, [e]) => !(#Known (unNode (representative (db, e))))
adamc@1215 801 | (PCon0 f, [e]) =>
adamc@1215 802 (case #Variety (unNode (representative (db, e))) of
adamc@1215 803 Dt0 f' => f' = f
adamc@1215 804 | _ => false)
adamc@1215 805 | (PCon1 f, [e]) =>
adamc@1215 806 (case #Variety (unNode (representative (db, e))) of
adamc@1215 807 Dt1 (f', _) => f' = f
adamc@1215 808 | _ => false)
adamc@1215 809 | (Eq, [e1, e2]) =>
adamc@1214 810 let
adamc@1215 811 val r1 = representative (db, e1)
adamc@1215 812 val r2 = representative (db, e2)
adamc@1214 813 in
adamc@1215 814 repOf r1 = repOf r2
adamc@1214 815 end
adamc@1215 816 | _ => false
adamc@1212 817
adamc@1208 818 end
adamc@1208 819
adamc@1215 820 fun decomp fals or =
adamc@1215 821 let
adamc@1215 822 fun decomp p k =
adamc@1215 823 case p of
adamc@1215 824 True => k []
adamc@1215 825 | False => fals
adamc@1215 826 | Unknown => k []
adamc@1215 827 | And (p1, p2) =>
adamc@1215 828 decomp p1 (fn ps1 =>
adamc@1215 829 decomp p2 (fn ps2 =>
adamc@1215 830 k (ps1 @ ps2)))
adamc@1215 831 | Or (p1, p2) =>
adamc@1215 832 or (decomp p1 k, fn () => decomp p2 k)
adamc@1215 833 | Reln x => k [AReln x]
adamc@1215 834 | Cond x => k [ACond x]
adamc@1215 835 in
adamc@1215 836 decomp
adamc@1215 837 end
adamc@1202 838
adamc@1202 839 fun imply (p1, p2) =
adamc@1217 840 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1217 841 (fn hyps =>
adamc@1217 842 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1217 843 (fn goals =>
adamc@1217 844 let
adamc@1217 845 fun gls goals onFail acc =
adamc@1217 846 case goals of
adamc@1217 847 [] =>
adamc@1217 848 (let
adamc@1217 849 val cc = Cc.database ()
adamc@1217 850 val () = app (fn a => Cc.assert (cc, a)) hyps
adamc@1217 851 in
adamc@1217 852 (List.all (fn a =>
adamc@1217 853 if Cc.check (cc, a) then
adamc@1217 854 true
adamc@1217 855 else
adamc@1217 856 ((*Print.prefaces "Can't prove"
adamc@1217 857 [("a", p_atom a),
adamc@1217 858 ("hyps", Print.p_list p_atom hyps),
adamc@1217 859 ("db", Cc.p_database cc)];*)
adamc@1217 860 false)) acc)
adamc@1217 861 handle Cc.Contradiction => false
adamc@1217 862 end handle Cc.Undetermined => false)
adamc@1217 863 orelse onFail ()
adamc@1217 864 | (g as AReln (Sql gf, [ge])) :: goals =>
adamc@1217 865 let
adamc@1217 866 fun hps hyps =
adamc@1217 867 case hyps of
adamc@1217 868 [] => gls goals onFail (g :: acc)
adamc@1217 869 | (h as AReln (Sql hf, [he])) :: hyps =>
adamc@1217 870 if gf = hf then
adamc@1217 871 let
adamc@1217 872 val saved = save ()
adamc@1217 873 in
adamc@1217 874 if eq (ge, he) then
adamc@1217 875 let
adamc@1217 876 val changed = IM.numItems (!unif)
adamc@1217 877 <> IM.numItems saved
adamc@1217 878 in
adamc@1217 879 gls goals (fn () => (restore saved;
adamc@1217 880 changed
adamc@1217 881 andalso hps hyps))
adamc@1217 882 acc
adamc@1217 883 end
adamc@1215 884 else
adamc@1217 885 hps hyps
adamc@1217 886 end
adamc@1217 887 else
adamc@1217 888 hps hyps
adamc@1217 889 | _ :: hyps => hps hyps
adamc@1217 890 in
adamc@1217 891 hps hyps
adamc@1217 892 end
adamc@1217 893 | g :: goals => gls goals onFail (g :: acc)
adamc@1217 894 in
adamc@1217 895 reset ();
adamc@1217 896 (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
adamc@1217 897 ("goals", Print.p_list p_atom goals)];*)
adamc@1217 898 gls goals (fn () => false) []
adamc@1217 899 end handle Cc.Contradiction => true))
adamc@1200 900
adamc@1200 901 fun patCon pc =
adamc@1200 902 case pc of
adamc@1200 903 PConVar n => "C" ^ Int.toString n
adamc@1200 904 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 905
adamc@1200 906 datatype chunk =
adamc@1200 907 String of string
adamc@1200 908 | Exp of Mono.exp
adamc@1200 909
adamc@1200 910 fun chunkify e =
adamc@1200 911 case #1 e of
adamc@1200 912 EPrim (Prim.String s) => [String s]
adamc@1207 913 | EStrcat (e1, e2) =>
adamc@1207 914 let
adamc@1207 915 val chs1 = chunkify e1
adamc@1207 916 val chs2 = chunkify e2
adamc@1207 917 in
adamc@1207 918 case chs2 of
adamc@1207 919 String s2 :: chs2' =>
adamc@1207 920 (case List.last chs1 of
adamc@1207 921 String s1 => List.take (chs1, length chs1 - 1) @ String (s1 ^ s2) :: chs2'
adamc@1207 922 | _ => chs1 @ chs2)
adamc@1207 923 | _ => chs1 @ chs2
adamc@1207 924 end
adamc@1200 925 | _ => [Exp e]
adamc@1200 926
adamc@1201 927 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 928
adamc@1201 929 fun always v chs = SOME (v, chs)
adamc@1201 930
adamc@1202 931 fun parse p s =
adamc@1202 932 case p (chunkify s) of
adamc@1201 933 SOME (v, []) => SOME v
adamc@1201 934 | _ => NONE
adamc@1201 935
adamc@1201 936 fun const s chs =
adamc@1201 937 case chs of
adamc@1201 938 String s' :: chs => if String.isPrefix s s' then
adamc@1201 939 SOME ((), if size s = size s' then
adamc@1201 940 chs
adamc@1201 941 else
adamc@1201 942 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 943 else
adamc@1201 944 NONE
adamc@1201 945 | _ => NONE
adamc@1201 946
adamc@1201 947 fun follow p1 p2 chs =
adamc@1201 948 case p1 chs of
adamc@1201 949 NONE => NONE
adamc@1201 950 | SOME (v1, chs) =>
adamc@1201 951 case p2 chs of
adamc@1201 952 NONE => NONE
adamc@1201 953 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 954
adamc@1201 955 fun wrap p f chs =
adamc@1201 956 case p chs of
adamc@1201 957 NONE => NONE
adamc@1201 958 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 959
adamc@1209 960 fun wrapP p f chs =
adamc@1209 961 case p chs of
adamc@1209 962 NONE => NONE
adamc@1209 963 | SOME (v, chs) =>
adamc@1209 964 case f v of
adamc@1209 965 NONE => NONE
adamc@1209 966 | SOME r => SOME (r, chs)
adamc@1209 967
adamc@1201 968 fun alt p1 p2 chs =
adamc@1201 969 case p1 chs of
adamc@1201 970 NONE => p2 chs
adamc@1201 971 | v => v
adamc@1201 972
adamc@1207 973 fun altL ps =
adamc@1207 974 case rev ps of
adamc@1207 975 [] => (fn _ => NONE)
adamc@1207 976 | p :: ps =>
adamc@1207 977 foldl (fn (p1, p2) => alt p1 p2) p ps
adamc@1207 978
adamc@1204 979 fun opt p chs =
adamc@1204 980 case p chs of
adamc@1204 981 NONE => SOME (NONE, chs)
adamc@1204 982 | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204 983
adamc@1201 984 fun skip cp chs =
adamc@1201 985 case chs of
adamc@1201 986 String "" :: chs => skip cp chs
adamc@1201 987 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 988 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 989 else
adamc@1201 990 SOME ((), chs)
adamc@1201 991 | _ => SOME ((), chs)
adamc@1201 992
adamc@1201 993 fun keep cp chs =
adamc@1201 994 case chs of
adamc@1201 995 String "" :: chs => keep cp chs
adamc@1201 996 | String s :: chs' =>
adamc@1201 997 let
adamc@1201 998 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 999 in
adamc@1201 1000 if Substring.isEmpty befor then
adamc@1201 1001 NONE
adamc@1201 1002 else
adamc@1201 1003 SOME (Substring.string befor,
adamc@1201 1004 if Substring.isEmpty after then
adamc@1201 1005 chs'
adamc@1201 1006 else
adamc@1201 1007 String (Substring.string after) :: chs')
adamc@1201 1008 end
adamc@1201 1009 | _ => NONE
adamc@1201 1010
adamc@1204 1011 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204 1012 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204 1013
adamc@1204 1014 fun log name p chs =
adamc@1206 1015 (if !debug then
adamc@1206 1016 case chs of
adamc@1207 1017 String s :: _ => print (name ^ ": " ^ s ^ "\n")
adamc@1206 1018 | _ => print (name ^ ": blocked!\n")
adamc@1206 1019 else
adamc@1206 1020 ();
adamc@1204 1021 p chs)
adamc@1201 1022
adamc@1201 1023 fun list p chs =
adamc@1207 1024 altL [wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1207 1025 (fn (v, ((), ls)) => v :: ls),
adamc@1207 1026 wrap (ws p) (fn v => [v]),
adamc@1207 1027 always []] chs
adamc@1201 1028
adamc@1201 1029 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 1030
adamc@1211 1031 val t_ident = wrapP ident (fn s => if String.isPrefix "T_" s then
adamc@1211 1032 SOME (String.extract (s, 2, NONE))
adamc@1201 1033 else
adamc@1211 1034 NONE)
adamc@1211 1035 val uw_ident = wrapP ident (fn s => if String.isPrefix "uw_" s andalso size s >= 4 then
adamc@1211 1036 SOME (str (Char.toUpper (String.sub (s, 3)))
adamc@1211 1037 ^ String.extract (s, 4, NONE))
adamc@1211 1038 else
adamc@1211 1039 NONE)
adamc@1201 1040
adamc@1211 1041 val field = wrap (follow t_ident
adamc@1201 1042 (follow (const ".")
adamc@1201 1043 uw_ident))
adamc@1201 1044 (fn (t, ((), f)) => (t, f))
adamc@1201 1045
adamc@1206 1046 datatype Rel =
adamc@1206 1047 Exps of exp * exp -> prop
adamc@1206 1048 | Props of prop * prop -> prop
adamc@1206 1049
adamc@1204 1050 datatype sqexp =
adamc@1206 1051 SqConst of Prim.t
adamc@1206 1052 | Field of string * string
adamc@1206 1053 | Binop of Rel * sqexp * sqexp
adamc@1207 1054 | SqKnown of sqexp
adamc@1207 1055 | Inj of Mono.exp
adamc@1211 1056 | SqFunc of string * sqexp
adamc@1211 1057 | Count
adamc@1204 1058
adamc@1210 1059 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
adamc@1210 1060
adamc@1210 1061 val sqbrel = altL [cmp "=" Eq,
adamc@1210 1062 cmp "<>" Ne,
adamc@1210 1063 cmp "<=" Le,
adamc@1210 1064 cmp "<" Lt,
adamc@1210 1065 cmp ">=" Ge,
adamc@1210 1066 cmp ">" Gt,
adamc@1207 1067 wrap (const "AND") (fn () => Props And),
adamc@1207 1068 wrap (const "OR") (fn () => Props Or)]
adamc@1204 1069
adamc@1204 1070 datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204 1071
adamc@1209 1072 fun string chs =
adamc@1206 1073 case chs of
adamc@1209 1074 String s :: chs =>
adamc@1209 1075 if size s >= 2 andalso String.sub (s, 0) = #"'" then
adamc@1209 1076 let
adamc@1209 1077 fun loop (cs, acc) =
adamc@1209 1078 case cs of
adamc@1209 1079 [] => NONE
adamc@1209 1080 | c :: cs =>
adamc@1209 1081 if c = #"'" then
adamc@1209 1082 SOME (String.implode (rev acc), cs)
adamc@1209 1083 else if c = #"\\" then
adamc@1209 1084 case cs of
adamc@1209 1085 c :: cs => loop (cs, c :: acc)
adamc@1209 1086 | _ => raise Fail "Iflow.string: Unmatched backslash escape"
adamc@1209 1087 else
adamc@1209 1088 loop (cs, c :: acc)
adamc@1209 1089 in
adamc@1209 1090 case loop (String.explode (String.extract (s, 1, NONE)), []) of
adamc@1209 1091 NONE => NONE
adamc@1209 1092 | SOME (s, []) => SOME (s, chs)
adamc@1209 1093 | SOME (s, cs) => SOME (s, String (String.implode cs) :: chs)
adamc@1209 1094 end
adamc@1209 1095 else
adamc@1209 1096 NONE
adamc@1209 1097 | _ => NONE
adamc@1206 1098
adamc@1209 1099 val prim =
adamc@1209 1100 altL [wrap (follow (wrapP (follow (keep Char.isDigit) (follow (const ".") (keep Char.isDigit)))
adamc@1209 1101 (fn (x, ((), y)) => Option.map Prim.Float (Real64.fromString (x ^ "." ^ y))))
adamc@1209 1102 (opt (const "::float8"))) #1,
adamc@1209 1103 wrap (follow (wrapP (keep Char.isDigit)
adamc@1209 1104 (Option.map Prim.Int o Int64.fromString))
adamc@1209 1105 (opt (const "::int8"))) #1,
adamc@1209 1106 wrap (follow (opt (const "E")) (follow string (opt (const "::text"))))
adamc@1209 1107 (Prim.String o #1 o #2)]
adamc@1206 1108
adamc@1207 1109 fun known' chs =
adamc@1207 1110 case chs of
adamc@1207 1111 Exp (EFfi ("Basis", "sql_known"), _) :: chs => SOME ((), chs)
adamc@1207 1112 | _ => NONE
adamc@1207 1113
adamc@1207 1114 fun sqlify chs =
adamc@1207 1115 case chs of
adamc@1207 1116 Exp (EFfiApp ("Basis", f, [e]), _) :: chs =>
adamc@1207 1117 if String.isPrefix "sqlify" f then
adamc@1207 1118 SOME (e, chs)
adamc@1207 1119 else
adamc@1207 1120 NONE
adamc@1207 1121 | _ => NONE
adamc@1207 1122
adamc@1211 1123 fun constK s = wrap (const s) (fn () => s)
adamc@1211 1124
adamc@1211 1125 val funcName = altL [constK "COUNT",
adamc@1211 1126 constK "MIN",
adamc@1211 1127 constK "MAX",
adamc@1211 1128 constK "SUM",
adamc@1211 1129 constK "AVG"]
adamc@1211 1130
adamc@1204 1131 fun sqexp chs =
adamc@1206 1132 log "sqexp"
adamc@1207 1133 (altL [wrap prim SqConst,
adamc@1211 1134 wrap field Field,
adamc@1207 1135 wrap known SqKnown,
adamc@1211 1136 wrap func SqFunc,
adamc@1211 1137 wrap (const "COUNT(*)") (fn () => Count),
adamc@1207 1138 wrap sqlify Inj,
adamc@1211 1139 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
adamc@1211 1140 (follow (keep (fn ch => ch <> #")")) (const ")")))))
adamc@1211 1141 (fn ((), (e, _)) => e),
adamc@1207 1142 wrap (follow (ws (const "("))
adamc@1207 1143 (follow (wrap
adamc@1207 1144 (follow sqexp
adamc@1207 1145 (alt
adamc@1207 1146 (wrap
adamc@1207 1147 (follow (ws sqbrel)
adamc@1207 1148 (ws sqexp))
adamc@1207 1149 inl)
adamc@1207 1150 (always (inr ()))))
adamc@1207 1151 (fn (e1, sm) =>
adamc@1207 1152 case sm of
adamc@1207 1153 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1207 1154 | inr () => e1))
adamc@1207 1155 (const ")")))
adamc@1207 1156 (fn ((), (e, ())) => e)])
adamc@1207 1157 chs
adamc@1206 1158
adamc@1207 1159 and known chs = wrap (follow known' (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 1160 (fn ((), ((), (e, ()))) => e) chs
adamc@1211 1161
adamc@1211 1162 and func chs = wrap (follow funcName (follow (const "(") (follow sqexp (const ")"))))
adamc@1211 1163 (fn (f, ((), (e, ()))) => (f, e)) chs
adamc@1211 1164
adamc@1211 1165 datatype sitem =
adamc@1211 1166 SqField of string * string
adamc@1211 1167 | SqExp of sqexp * string
adamc@1211 1168
adamc@1211 1169 val sitem = alt (wrap field SqField)
adamc@1211 1170 (wrap (follow sqexp (follow (const " AS ") uw_ident))
adamc@1211 1171 (fn (e, ((), s)) => SqExp (e, s)))
adamc@1207 1172
adamc@1207 1173 val select = log "select"
adamc@1207 1174 (wrap (follow (const "SELECT ") (list sitem))
adamc@1207 1175 (fn ((), ls) => ls))
adamc@1201 1176
adamc@1201 1177 val fitem = wrap (follow uw_ident
adamc@1201 1178 (follow (const " AS ")
adamc@1201 1179 t_ident))
adamc@1201 1180 (fn (t, ((), f)) => (t, f))
adamc@1201 1181
adamc@1207 1182 val from = log "from"
adamc@1207 1183 (wrap (follow (const "FROM ") (list fitem))
adamc@1207 1184 (fn ((), ls) => ls))
adamc@1201 1185
adamc@1204 1186 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204 1187 (fn ((), ls) => ls)
adamc@1204 1188
adamc@1207 1189 val query = log "query"
adamc@1207 1190 (wrap (follow (follow select from) (opt wher))
adamc@1207 1191 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher}))
adamc@1201 1192
adamc@1215 1193 fun removeDups (ls : (string * string) list) =
adamc@1211 1194 case ls of
adamc@1211 1195 [] => []
adamc@1211 1196 | x :: ls =>
adamc@1211 1197 let
adamc@1211 1198 val ls = removeDups ls
adamc@1211 1199 in
adamc@1211 1200 if List.exists (fn x' => x' = x) ls then
adamc@1211 1201 ls
adamc@1211 1202 else
adamc@1211 1203 x :: ls
adamc@1211 1204 end
adamc@1211 1205
adamc@1212 1206 datatype queryMode =
adamc@1212 1207 SomeCol of exp
adamc@1212 1208 | AllCols of exp
adamc@1212 1209
adamc@1216 1210 exception Default
adamc@1216 1211
adamc@1214 1212 fun queryProp env rvN rv oe e =
adamc@1216 1213 let
adamc@1216 1214 fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
adamc@1216 1215 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
adamc@1217 1216 (rvN, Unknown, Unknown, []))
adamc@1216 1217 in
adamc@1216 1218 case parse query e of
adamc@1216 1219 NONE => default ()
adamc@1216 1220 | SOME r =>
adamc@1216 1221 let
adamc@1216 1222 val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
adamc@1216 1223 let
adamc@1216 1224 val (rvN, e) = rv rvN
adamc@1216 1225 in
adamc@1216 1226 ((v, e), rvN)
adamc@1216 1227 end) rvN (#From r)
adamc@1214 1228
adamc@1216 1229 fun rvOf v =
adamc@1216 1230 case List.find (fn (v', _) => v' = v) rvs of
adamc@1216 1231 NONE => raise Fail "Iflow.queryProp: Bad table variable"
adamc@1216 1232 | SOME (_, e) => e
adamc@1214 1233
adamc@1216 1234 fun usedFields e =
adamc@1216 1235 case e of
adamc@1216 1236 SqConst _ => []
adamc@1216 1237 | Field (v, f) => [(v, f)]
adamc@1216 1238 | Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
adamc@1216 1239 | SqKnown _ => []
adamc@1216 1240 | Inj _ => []
adamc@1216 1241 | SqFunc (_, e) => usedFields e
adamc@1216 1242 | Count => []
adamc@1214 1243
adamc@1216 1244 val p =
adamc@1216 1245 foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
adamc@1211 1246
adamc@1216 1247 fun expIn e =
adamc@1216 1248 case e of
adamc@1216 1249 SqConst p => inl (Const p)
adamc@1216 1250 | Field (v, f) => inl (Proj (rvOf v, f))
adamc@1216 1251 | Binop (bo, e1, e2) =>
adamc@1216 1252 inr (case (bo, expIn e1, expIn e2) of
adamc@1216 1253 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1216 1254 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1216 1255 | _ => Unknown)
adamc@1216 1256 | SqKnown e =>
adamc@1216 1257 inr (case expIn e of
adamc@1216 1258 inl e => Reln (Known, [e])
adamc@1216 1259 | _ => Unknown)
adamc@1216 1260 | Inj e =>
adamc@1216 1261 let
adamc@1216 1262 fun deinj (e, _) =
adamc@1216 1263 case e of
adamc@1216 1264 ERel n => List.nth (env, n)
adamc@1216 1265 | EField (e, f) => Proj (deinj e, f)
adamc@1216 1266 | _ => raise Fail "Iflow: non-variable injected into query"
adamc@1216 1267 in
adamc@1216 1268 inl (deinj e)
adamc@1216 1269 end
adamc@1216 1270 | SqFunc (f, e) =>
adamc@1216 1271 inl (case expIn e of
adamc@1216 1272 inl e => Func (Other f, [e])
adamc@1216 1273 | _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
adamc@1216 1274 | Count => raise Default
adamc@1205 1275
adamc@1216 1276 val p = case #Where r of
adamc@1216 1277 NONE => p
adamc@1216 1278 | SOME e =>
adamc@1216 1279 case expIn e of
adamc@1216 1280 inr p' => And (p, p')
adamc@1216 1281 | _ => p
adamc@1210 1282
adamc@1216 1283 fun normal () =
adamc@1217 1284 (And (p, case oe of
adamc@1216 1285 SomeCol oe =>
adamc@1216 1286 foldl (fn (si, p) =>
adamc@1216 1287 let
adamc@1216 1288 val p' = case si of
adamc@1216 1289 SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
adamc@1216 1290 | SqExp (e, f) =>
adamc@1216 1291 case expIn e of
adamc@1216 1292 inr _ => Unknown
adamc@1216 1293 | inl e => Reln (Eq, [oe, e])
adamc@1216 1294 in
adamc@1216 1295 Or (p, p')
adamc@1216 1296 end)
adamc@1216 1297 False (#Select r)
adamc@1216 1298 | AllCols oe =>
adamc@1216 1299 foldl (fn (si, p) =>
adamc@1216 1300 let
adamc@1216 1301 val p' = case si of
adamc@1216 1302 SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
adamc@1216 1303 Proj (rvOf v, f)])
adamc@1216 1304 | SqExp (e, f) =>
adamc@1216 1305 case expIn e of
adamc@1216 1306 inr p => Cond (Proj (oe, f), p)
adamc@1216 1307 | inl e => Reln (Eq, [Proj (oe, f), e])
adamc@1216 1308 in
adamc@1216 1309 And (p, p')
adamc@1216 1310 end)
adamc@1216 1311 True (#Select r)),
adamc@1217 1312 True)
adamc@1217 1313
adamc@1217 1314 val (p, wp) =
adamc@1217 1315 case #Select r of
adamc@1217 1316 [SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
adamc@1217 1317 (case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
adamc@1217 1318 Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
adamc@1217 1319 let
adamc@1217 1320 val oe = case oe of
adamc@1217 1321 SomeCol oe => oe
adamc@1217 1322 | AllCols oe => Proj (oe, f)
adamc@1217 1323 in
adamc@1217 1324 (Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
adamc@1217 1325 And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
adamc@1217 1326 p)),
adamc@1217 1327 Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]))
adamc@1217 1328 end
adamc@1217 1329 | _ => normal ())
adamc@1217 1330 | _ => normal ()
adamc@1216 1331 in
adamc@1217 1332 (rvN, p, wp, case #Where r of
adamc@1217 1333 NONE => []
adamc@1217 1334 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
adamc@1216 1335 end
adamc@1216 1336 handle Default => default ()
adamc@1216 1337 end
adamc@1200 1338
adamc@1211 1339 fun evalPat env e (pt, _) =
adamc@1211 1340 case pt of
adamc@1211 1341 PWild => (env, True)
adamc@1211 1342 | PVar _ => (e :: env, True)
adamc@1211 1343 | PPrim _ => (env, True)
adamc@1215 1344 | PCon (_, pc, NONE) => (env, Reln (PCon0 (patCon pc), [e]))
adamc@1211 1345 | PCon (_, pc, SOME pt) =>
adamc@1211 1346 let
adamc@1215 1347 val (env, p) = evalPat env (Func (UnCon (patCon pc), [e])) pt
adamc@1211 1348 in
adamc@1215 1349 (env, And (p, Reln (PCon1 (patCon pc), [e])))
adamc@1211 1350 end
adamc@1211 1351 | PRecord xpts =>
adamc@1211 1352 foldl (fn ((x, pt, _), (env, p)) =>
adamc@1211 1353 let
adamc@1211 1354 val (env, p') = evalPat env (Proj (e, x)) pt
adamc@1211 1355 in
adamc@1211 1356 (env, And (p', p))
adamc@1211 1357 end) (env, True) xpts
adamc@1215 1358 | PNone _ => (env, Reln (PCon0 "None", [e]))
adamc@1211 1359 | PSome (_, pt) =>
adamc@1211 1360 let
adamc@1215 1361 val (env, p) = evalPat env (Func (UnCon "Some", [e])) pt
adamc@1211 1362 in
adamc@1215 1363 (env, And (p, Reln (PCon1 "Some", [e])))
adamc@1211 1364 end
adamc@1211 1365
adamc@1211 1366 fun peq (p1, p2) =
adamc@1211 1367 case (p1, p2) of
adamc@1211 1368 (True, True) => true
adamc@1211 1369 | (False, False) => true
adamc@1211 1370 | (Unknown, Unknown) => true
adamc@1211 1371 | (And (x1, y1), And (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1372 | (Or (x1, y1), Or (x2, y2)) => peq (x1, x2) andalso peq (y1, y2)
adamc@1211 1373 | (Reln (r1, es1), Reln (r2, es2)) => r1 = r2 andalso ListPair.allEq eeq (es1, es2)
adamc@1212 1374 | (Cond (e1, p1), Cond (e2, p2)) => eeq (e1, e2) andalso peq (p1, p2)
adamc@1211 1375 | _ => false
adamc@1211 1376
adamc@1211 1377 fun removeRedundant p1 =
adamc@1211 1378 let
adamc@1211 1379 fun rr p2 =
adamc@1211 1380 if peq (p1, p2) then
adamc@1211 1381 True
adamc@1211 1382 else
adamc@1211 1383 case p2 of
adamc@1211 1384 And (x, y) => And (rr x, rr y)
adamc@1211 1385 | Or (x, y) => Or (rr x, rr y)
adamc@1211 1386 | _ => p2
adamc@1211 1387 in
adamc@1211 1388 rr
adamc@1211 1389 end
adamc@1211 1390
adamc@1217 1391 structure St :> sig
adamc@1217 1392 type t
adamc@1217 1393 val create : {Var : int,
adamc@1217 1394 Ambient : prop} -> t
adamc@1217 1395
adamc@1217 1396 val curVar : t -> int
adamc@1217 1397 val nextVar : t -> t * int
adamc@1217 1398
adamc@1217 1399 val ambient : t -> prop
adamc@1217 1400 val setAmbient : t * prop -> t
adamc@1217 1401
adamc@1217 1402 type check = ErrorMsg.span * exp * prop
adamc@1217 1403
adamc@1217 1404 val path : t -> check list
adamc@1217 1405 val addPath : t * check -> t
adamc@1217 1406
adamc@1217 1407 val sent : t -> check list
adamc@1217 1408 val addSent : t * check -> t
adamc@1217 1409 val setSent : t * check list -> t
adamc@1217 1410 end = struct
adamc@1217 1411
adamc@1217 1412 type check = ErrorMsg.span * exp * prop
adamc@1217 1413
adamc@1217 1414 type t = {Var : int,
adamc@1217 1415 Ambient : prop,
adamc@1217 1416 Path : check list,
adamc@1217 1417 Sent : check list}
adamc@1217 1418
adamc@1217 1419 fun create {Var = v, Ambient = p} = {Var = v,
adamc@1217 1420 Ambient = p,
adamc@1217 1421 Path = [],
adamc@1217 1422 Sent = []}
adamc@1217 1423
adamc@1217 1424 fun curVar (t : t) = #Var t
adamc@1217 1425 fun nextVar (t : t) = ({Var = #Var t + 1,
adamc@1217 1426 Ambient = #Ambient t,
adamc@1217 1427 Path = #Path t,
adamc@1217 1428 Sent = #Sent t}, #Var t)
adamc@1217 1429
adamc@1217 1430 fun ambient (t : t) = #Ambient t
adamc@1217 1431 fun setAmbient (t : t, p) = {Var = #Var t,
adamc@1217 1432 Ambient = p,
adamc@1217 1433 Path = #Path t,
adamc@1217 1434 Sent = #Sent t}
adamc@1217 1435
adamc@1217 1436 fun path (t : t) = #Path t
adamc@1217 1437 fun addPath (t : t, c) = {Var = #Var t,
adamc@1217 1438 Ambient = #Ambient t,
adamc@1217 1439 Path = c :: #Path t,
adamc@1217 1440 Sent = #Sent t}
adamc@1217 1441
adamc@1217 1442 fun sent (t : t) = #Sent t
adamc@1217 1443 fun addSent (t : t, c) = {Var = #Var t,
adamc@1217 1444 Ambient = #Ambient t,
adamc@1217 1445 Path = #Path t,
adamc@1217 1446 Sent = c :: #Sent t}
adamc@1217 1447 fun setSent (t : t, cs) = {Var = #Var t,
adamc@1217 1448 Ambient = #Ambient t,
adamc@1217 1449 Path = #Path t,
adamc@1217 1450 Sent = cs}
adamc@1217 1451
adamc@1217 1452 end
adamc@1217 1453
adamc@1217 1454 fun evalExp env (e as (_, loc), st) =
adamc@1200 1455 let
adamc@1200 1456 fun default () =
adamc@1217 1457 let
adamc@1217 1458 val (st, nv) = St.nextVar st
adamc@1217 1459 in
adamc@1217 1460 (Var nv, st)
adamc@1217 1461 end
adamc@1200 1462
adamc@1217 1463 fun addSent (p, e, st) =
adamc@1200 1464 if isKnown e then
adamc@1217 1465 st
adamc@1200 1466 else
adamc@1217 1467 St.addSent (st, (loc, e, p))
adamc@1200 1468 in
adamc@1200 1469 case #1 e of
adamc@1200 1470 EPrim p => (Const p, st)
adamc@1200 1471 | ERel n => (List.nth (env, n), st)
adamc@1200 1472 | ENamed _ => default ()
adamc@1215 1473 | ECon (_, pc, NONE) => (Func (DtCon0 (patCon pc), []), st)
adamc@1200 1474 | ECon (_, pc, SOME e) =>
adamc@1200 1475 let
adamc@1200 1476 val (e, st) = evalExp env (e, st)
adamc@1200 1477 in
adamc@1215 1478 (Func (DtCon1 (patCon pc), [e]), st)
adamc@1200 1479 end
adamc@1215 1480 | ENone _ => (Func (DtCon0 "None", []), st)
adamc@1200 1481 | ESome (_, e) =>
adamc@1200 1482 let
adamc@1200 1483 val (e, st) = evalExp env (e, st)
adamc@1200 1484 in
adamc@1215 1485 (Func (DtCon1 "Some", [e]), st)
adamc@1200 1486 end
adamc@1200 1487 | EFfi _ => default ()
adamc@1213 1488
adamc@1200 1489 | EFfiApp (m, s, es) =>
adamc@1200 1490 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 1491 let
adamc@1200 1492 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1493 in
adamc@1217 1494 (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es)
adamc@1200 1495 end
adamc@1200 1496 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 1497 default ()
adamc@1200 1498 else
adamc@1200 1499 let
adamc@1200 1500 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1501 in
adamc@1215 1502 (Func (Other (m ^ "." ^ s), es), st)
adamc@1200 1503 end
adamc@1213 1504
adamc@1213 1505 | EApp (e1, e2) =>
adamc@1213 1506 let
adamc@1213 1507 val (e1, st) = evalExp env (e1, st)
adamc@1213 1508 in
adamc@1213 1509 case e1 of
adamc@1213 1510 Finish => (Finish, st)
adamc@1213 1511 | _ => default ()
adamc@1213 1512 end
adamc@1213 1513
adamc@1200 1514 | EAbs _ => default ()
adamc@1200 1515 | EUnop (s, e1) =>
adamc@1200 1516 let
adamc@1200 1517 val (e1, st) = evalExp env (e1, st)
adamc@1200 1518 in
adamc@1215 1519 (Func (Other s, [e1]), st)
adamc@1200 1520 end
adamc@1200 1521 | EBinop (s, e1, e2) =>
adamc@1200 1522 let
adamc@1200 1523 val (e1, st) = evalExp env (e1, st)
adamc@1200 1524 val (e2, st) = evalExp env (e2, st)
adamc@1200 1525 in
adamc@1215 1526 (Func (Other s, [e1, e2]), st)
adamc@1200 1527 end
adamc@1200 1528 | ERecord xets =>
adamc@1200 1529 let
adamc@1200 1530 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 1531 let
adamc@1200 1532 val (e, st) = evalExp env (e, st)
adamc@1200 1533 in
adamc@1200 1534 ((x, e), st)
adamc@1200 1535 end) st xets
adamc@1200 1536 in
adamc@1200 1537 (Recd xes, st)
adamc@1200 1538 end
adamc@1200 1539 | EField (e, s) =>
adamc@1200 1540 let
adamc@1200 1541 val (e, st) = evalExp env (e, st)
adamc@1200 1542 in
adamc@1200 1543 (Proj (e, s), st)
adamc@1200 1544 end
adamc@1211 1545 | ECase (e, pes, _) =>
adamc@1211 1546 let
adamc@1211 1547 val (e, st) = evalExp env (e, st)
adamc@1217 1548 val (st, r) = St.nextVar st
adamc@1217 1549 val orig = St.ambient st
adamc@1211 1550
adamc@1211 1551 val st = foldl (fn ((pt, pe), st) =>
adamc@1211 1552 let
adamc@1211 1553 val (env, pp) = evalPat env e pt
adamc@1217 1554 val (pe, st') = evalExp env (pe, St.setAmbient (st, And (orig, pp)))
adamc@1216 1555 (*val () = Print.prefaces "Case" [("loc", Print.PD.string
adamc@1216 1556 (ErrorMsg.spanToString (#2 pt))),
adamc@1216 1557 ("env", Print.p_list p_exp env),
adamc@1216 1558 ("sent", Print.p_list_sep Print.PD.newline
adamc@1216 1559 (fn (loc, e, p) =>
adamc@1216 1560 Print.box [Print.PD.string
adamc@1216 1561 (ErrorMsg.spanToString loc),
adamc@1216 1562 Print.PD.string ":",
adamc@1216 1563 Print.space,
adamc@1216 1564 p_exp e,
adamc@1216 1565 Print.space,
adamc@1216 1566 Print.PD.string "in",
adamc@1216 1567 Print.space,
adamc@1216 1568 p_prop p])
adamc@1216 1569 (List.take (#3 st', length (#3 st')
adamc@1216 1570 - length (#3 st))))]*)
adamc@1211 1571
adamc@1217 1572 val this = And (removeRedundant orig (St.ambient st'),
adamc@1217 1573 Reln (Eq, [Var r, pe]))
adamc@1211 1574 in
adamc@1217 1575 St.setAmbient (st', Or (St.ambient st, this))
adamc@1217 1576 end) (St.setAmbient (st, False)) pes
adamc@1211 1577 in
adamc@1217 1578 (Var r, St.setAmbient (st, And (orig, St.ambient st)))
adamc@1211 1579 end
adamc@1200 1580 | EStrcat (e1, e2) =>
adamc@1200 1581 let
adamc@1200 1582 val (e1, st) = evalExp env (e1, st)
adamc@1200 1583 val (e2, st) = evalExp env (e2, st)
adamc@1200 1584 in
adamc@1215 1585 (Func (Other "cat", [e1, e2]), st)
adamc@1200 1586 end
adamc@1200 1587 | EError _ => (Finish, st)
adamc@1200 1588 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 1589 let
adamc@1200 1590 val (b, st) = evalExp env (b, st)
adamc@1200 1591 val (m, st) = evalExp env (m, st)
adamc@1200 1592 in
adamc@1217 1593 (Finish, addSent (St.ambient st, b, addSent (St.ambient st, m, st)))
adamc@1200 1594 end
adamc@1200 1595 | ERedirect (e, _) =>
adamc@1200 1596 let
adamc@1200 1597 val (e, st) = evalExp env (e, st)
adamc@1200 1598 in
adamc@1217 1599 (Finish, addSent (St.ambient st, e, st))
adamc@1200 1600 end
adamc@1200 1601 | EWrite e =>
adamc@1200 1602 let
adamc@1200 1603 val (e, st) = evalExp env (e, st)
adamc@1200 1604 in
adamc@1217 1605 (Recd [], addSent (St.ambient st, e, st))
adamc@1200 1606 end
adamc@1200 1607 | ESeq (e1, e2) =>
adamc@1200 1608 let
adamc@1200 1609 val (_, st) = evalExp env (e1, st)
adamc@1200 1610 in
adamc@1200 1611 evalExp env (e2, st)
adamc@1200 1612 end
adamc@1200 1613 | ELet (_, _, e1, e2) =>
adamc@1200 1614 let
adamc@1200 1615 val (e1, st) = evalExp env (e1, st)
adamc@1200 1616 in
adamc@1200 1617 evalExp (e1 :: env) (e2, st)
adamc@1200 1618 end
adamc@1200 1619 | EClosure (n, es) =>
adamc@1200 1620 let
adamc@1200 1621 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 1622 in
adamc@1215 1623 (Func (Other ("Cl" ^ Int.toString n), es), st)
adamc@1200 1624 end
adamc@1200 1625
adamc@1200 1626 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 1627 let
adamc@1200 1628 val (_, st) = evalExp env (q, st)
adamc@1200 1629 val (i, st) = evalExp env (i, st)
adamc@1200 1630
adamc@1217 1631 val (st', r) = St.nextVar st
adamc@1217 1632 val (st', acc) = St.nextVar st'
adamc@1200 1633
adamc@1200 1634 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 1635
adamc@1217 1636 val (st', qp, qwp, used) =
adamc@1214 1637 queryProp env
adamc@1217 1638 st' (fn st' =>
adamc@1217 1639 let
adamc@1217 1640 val (st', rv) = St.nextVar st'
adamc@1217 1641 in
adamc@1217 1642 (st', Var rv)
adamc@1217 1643 end)
adamc@1214 1644 (AllCols (Var r)) q
adamc@1200 1645
adamc@1217 1646 val p' = And (qp, St.ambient st')
adamc@1200 1647
adamc@1217 1648 val (st, res) = if varInP acc (St.ambient st') then
adamc@1217 1649 let
adamc@1217 1650 val (st, r) = St.nextVar st
adamc@1217 1651 in
adamc@1217 1652 (st, Var r)
adamc@1217 1653 end
adamc@1217 1654 else
adamc@1217 1655 let
adamc@1217 1656 val (st, out) = St.nextVar st'
adamc@1217 1657
adamc@1217 1658 val p = Or (Reln (Eq, [Var out, i]),
adamc@1217 1659 And (Reln (Eq, [Var out, b]),
adamc@1217 1660 p'))
adamc@1217 1661 in
adamc@1217 1662 (St.setAmbient (st, p), Var out)
adamc@1217 1663 end
adamc@1210 1664
adamc@1217 1665 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (St.sent st')
adamc@1212 1666
adamc@1217 1667 val p' = And (p', qwp)
adamc@1210 1668 val sent = map (fn e => (loc, e, p')) used @ sent
adamc@1200 1669 in
adamc@1217 1670 (res, St.setSent (st, sent))
adamc@1200 1671 end
adamc@1200 1672 | EDml _ => default ()
adamc@1200 1673 | ENextval _ => default ()
adamc@1200 1674 | ESetval _ => default ()
adamc@1200 1675
adamc@1213 1676 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
adamc@1217 1677 let
adamc@1217 1678 val (st, nv) = St.nextVar st
adamc@1217 1679 in
adamc@1217 1680 (Var nv, St.setAmbient (st, And (St.ambient st, Reln (Known, [Var nv]))))
adamc@1217 1681 end
adamc@1213 1682
adamc@1200 1683 | EUnurlify _ => default ()
adamc@1200 1684 | EJavaScript _ => default ()
adamc@1200 1685 | ESignalReturn _ => default ()
adamc@1200 1686 | ESignalBind _ => default ()
adamc@1200 1687 | ESignalSource _ => default ()
adamc@1200 1688 | EServerCall _ => default ()
adamc@1200 1689 | ERecv _ => default ()
adamc@1200 1690 | ESleep _ => default ()
adamc@1200 1691 | ESpawn _ => default ()
adamc@1200 1692 end
adamc@1200 1693
adamc@1200 1694 fun check file =
adamc@1200 1695 let
adamc@1213 1696 val file = MonoReduce.reduce file
adamc@1213 1697 val file = MonoOpt.optimize file
adamc@1213 1698 val file = Fuse.fuse file
adamc@1213 1699 val file = MonoOpt.optimize file
adamc@1216 1700 val file = MonoShake.shake file
adamc@1213 1701 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
adamc@1213 1702
adamc@1207 1703 val exptd = foldl (fn ((d, _), exptd) =>
adamc@1207 1704 case d of
adamc@1207 1705 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
adamc@1207 1706 | _ => exptd) IS.empty file
adamc@1207 1707
adamc@1202 1708 fun decl ((d, _), (vals, pols)) =
adamc@1200 1709 case d of
adamc@1207 1710 DVal (_, n, _, e, _) =>
adamc@1200 1711 let
adamc@1207 1712 val isExptd = IS.member (exptd, n)
adamc@1207 1713
adamc@1207 1714 fun deAbs (e, env, nv, p) =
adamc@1200 1715 case #1 e of
adamc@1207 1716 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1,
adamc@1207 1717 if isExptd then
adamc@1207 1718 And (p, Reln (Known, [Var nv]))
adamc@1207 1719 else
adamc@1207 1720 p)
adamc@1207 1721 | _ => (e, env, nv, p)
adamc@1200 1722
adamc@1207 1723 val (e, env, nv, p) = deAbs (e, [], 1, True)
adamc@1200 1724
adamc@1217 1725 val (_, st) = evalExp env (e, St.create {Var = nv,
adamc@1217 1726 Ambient = p})
adamc@1200 1727 in
adamc@1217 1728 (St.sent st @ vals, pols)
adamc@1200 1729 end
adamc@1202 1730
adamc@1216 1731 | DPolicy (PolClient e) => (vals, #2 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
adamc@1214 1732 (SomeCol (Var 0)) e) :: pols)
adamc@1214 1733
adamc@1202 1734 | _ => (vals, pols)
adamc@1202 1735
adamc@1203 1736 val () = reset ()
adamc@1202 1737
adamc@1202 1738 val (vals, pols) = foldl decl ([], []) file
adamc@1200 1739 in
adamc@1207 1740 app (fn (loc, e, p) =>
adamc@1207 1741 let
adamc@1213 1742 fun doOne e =
adamc@1213 1743 let
adamc@1213 1744 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1213 1745 in
adamc@1213 1746 if List.exists (fn pol => if imply (p, pol) then
adamc@1213 1747 (if !debug then
adamc@1213 1748 Print.prefaces "Match"
adamc@1213 1749 [("Hyp", p_prop p),
adamc@1213 1750 ("Goal", p_prop pol)]
adamc@1213 1751 else
adamc@1213 1752 ();
adamc@1213 1753 true)
adamc@1213 1754 else
adamc@1213 1755 false) pols then
adamc@1213 1756 ()
adamc@1213 1757 else
adamc@1213 1758 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
adamc@1216 1759 Print.preface ("The state satisifies this predicate:", p_prop p))
adamc@1213 1760 end
adamc@1213 1761
adamc@1213 1762 fun doAll e =
adamc@1213 1763 case e of
adamc@1213 1764 Const _ => ()
adamc@1213 1765 | Var _ => doOne e
adamc@1213 1766 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
adamc@1216 1767 | Func (UnCon _, [_]) => doOne e
adamc@1215 1768 | Func (_, es) => app doAll es
adamc@1213 1769 | Recd xes => app (doAll o #2) xes
adamc@1213 1770 | Proj _ => doOne e
adamc@1213 1771 | Finish => ()
adamc@1207 1772 in
adamc@1213 1773 doAll e
adamc@1207 1774 end) vals
adamc@1200 1775 end
adamc@1200 1776
adamc@1213 1777 val check = fn file =>
adamc@1213 1778 let
adamc@1213 1779 val oldInline = Settings.getMonoInline ()
adamc@1213 1780 in
adamc@1213 1781 (Settings.setMonoInline (case Int.maxInt of
adamc@1213 1782 NONE => 1000000
adamc@1213 1783 | SOME n => n);
adamc@1213 1784 check file;
adamc@1213 1785 Settings.setMonoInline oldInline)
adamc@1213 1786 handle ex => (Settings.setMonoInline oldInline;
adamc@1213 1787 raise ex)
adamc@1213 1788 end
adamc@1213 1789
adamc@1200 1790 end
adamc@1213 1791