Mercurial > urweb

annotate src/iflow.sml @ 1206:772760df4c4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing more of WHERE
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Apr 2010 17:44:12 -0400
parents 7cd11380cdf1
children ae3036773768
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@1202 32 structure IM = IntBinaryMap
adamc@1202 33
adamc@1200 34 structure SS = BinarySetFn(struct
adamc@1200 35 type ord_key = string
adamc@1200 36 val compare = String.compare
adamc@1200 37 end)
adamc@1200 38
adamc@1200 39 val writers = ["htmlifyInt_w",
adamc@1200 40 "htmlifyFloat_w",
adamc@1200 41 "htmlifyString_w",
adamc@1200 42 "htmlifyBool_w",
adamc@1200 43 "htmlifyTime_w",
adamc@1200 44 "attrifyInt_w",
adamc@1200 45 "attrifyFloat_w",
adamc@1200 46 "attrifyString_w",
adamc@1200 47 "attrifyChar_w",
adamc@1200 48 "urlifyInt_w",
adamc@1200 49 "urlifyFloat_w",
adamc@1200 50 "urlifyString_w",
adamc@1200 51 "urlifyBool_w"]
adamc@1200 52
adamc@1200 53 val writers = SS.addList (SS.empty, writers)
adamc@1200 54
adamc@1200 55 type lvar = int
adamc@1200 56
adamc@1200 57 datatype exp =
adamc@1200 58 Const of Prim.t
adamc@1200 59 | Var of int
adamc@1200 60 | Lvar of lvar
adamc@1200 61 | Func of string * exp list
adamc@1200 62 | Recd of (string * exp) list
adamc@1200 63 | Proj of exp * string
adamc@1200 64 | Finish
adamc@1200 65
adamc@1200 66 datatype reln =
adamc@1200 67 Sql of string
adamc@1200 68 | Eq
adamc@1200 69
adamc@1200 70 datatype prop =
adamc@1200 71 True
adamc@1200 72 | False
adamc@1200 73 | Unknown
adamc@1200 74 | And of prop * prop
adamc@1200 75 | Or of prop * prop
adamc@1200 76 | Reln of reln * exp list
adamc@1200 77 | Select of int * lvar * lvar * prop * exp
adamc@1200 78
adamc@1200 79 local
adamc@1202 80 val count = ref 1
adamc@1200 81 in
adamc@1200 82 fun newLvar () =
adamc@1200 83 let
adamc@1200 84 val n = !count
adamc@1200 85 in
adamc@1200 86 count := n + 1;
adamc@1200 87 n
adamc@1200 88 end
adamc@1200 89 end
adamc@1200 90
adamc@1200 91 fun subExp (v, lv) =
adamc@1200 92 let
adamc@1200 93 fun sub e =
adamc@1200 94 case e of
adamc@1200 95 Const _ => e
adamc@1200 96 | Var v' => if v' = v then Lvar lv else e
adamc@1200 97 | Lvar _ => e
adamc@1200 98 | Func (f, es) => Func (f, map sub es)
adamc@1200 99 | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
adamc@1200 100 | Proj (e, s) => Proj (sub e, s)
adamc@1200 101 | Finish => Finish
adamc@1200 102 in
adamc@1200 103 sub
adamc@1200 104 end
adamc@1200 105
adamc@1200 106 fun subProp (v, lv) =
adamc@1200 107 let
adamc@1200 108 fun sub p =
adamc@1200 109 case p of
adamc@1200 110 True => p
adamc@1200 111 | False => p
adamc@1200 112 | Unknown => p
adamc@1200 113 | And (p1, p2) => And (sub p1, sub p2)
adamc@1200 114 | Or (p1, p2) => Or (sub p1, sub p2)
adamc@1200 115 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
adamc@1200 116 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
adamc@1200 117 in
adamc@1200 118 sub
adamc@1200 119 end
adamc@1200 120
adamc@1200 121 fun isKnown e =
adamc@1200 122 case e of
adamc@1200 123 Const _ => true
adamc@1200 124 | Func (_, es) => List.all isKnown es
adamc@1200 125 | Recd xes => List.all (isKnown o #2) xes
adamc@1200 126 | Proj (e, _) => isKnown e
adamc@1200 127 | _ => false
adamc@1200 128
adamc@1200 129 fun isFinish e =
adamc@1200 130 case e of
adamc@1200 131 Finish => true
adamc@1200 132 | _ => false
adamc@1200 133
adamc@1200 134 fun simplify e =
adamc@1200 135 case e of
adamc@1200 136 Const _ => e
adamc@1200 137 | Var _ => e
adamc@1200 138 | Lvar _ => e
adamc@1200 139 | Func (f, es) =>
adamc@1200 140 let
adamc@1200 141 val es = map simplify es
adamc@1200 142 in
adamc@1200 143 if List.exists isFinish es then
adamc@1200 144 Finish
adamc@1200 145 else
adamc@1200 146 Func (f, es)
adamc@1200 147 end
adamc@1200 148 | Recd xes =>
adamc@1200 149 let
adamc@1200 150 val xes = map (fn (x, e) => (x, simplify e)) xes
adamc@1200 151 in
adamc@1200 152 if List.exists (isFinish o #2) xes then
adamc@1200 153 Finish
adamc@1200 154 else
adamc@1200 155 Recd xes
adamc@1200 156 end
adamc@1200 157 | Proj (e, s) =>
adamc@1200 158 (case simplify e of
adamc@1200 159 Recd xes =>
adamc@1200 160 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
adamc@1200 161 | e' =>
adamc@1200 162 if isFinish e' then
adamc@1200 163 Finish
adamc@1200 164 else
adamc@1200 165 Proj (e', s))
adamc@1200 166 | Finish => Finish
adamc@1200 167
adamc@1202 168 fun decomp fals or =
adamc@1200 169 let
adamc@1200 170 fun decomp p k =
adamc@1200 171 case p of
adamc@1200 172 True => k []
adamc@1202 173 | False => fals
adamc@1200 174 | Unknown => k []
adamc@1200 175 | And (p1, p2) =>
adamc@1200 176 decomp p1 (fn ps1 =>
adamc@1200 177 decomp p2 (fn ps2 =>
adamc@1200 178 k (ps1 @ ps2)))
adamc@1200 179 | Or (p1, p2) =>
adamc@1200 180 or (decomp p1 k, fn () => decomp p2 k)
adamc@1200 181 | Reln x => k [x]
adamc@1200 182 | Select _ => k []
adamc@1200 183 in
adamc@1200 184 decomp
adamc@1200 185 end
adamc@1200 186
adamc@1202 187 val unif = ref (IM.empty : exp IM.map)
adamc@1200 188
adamc@1203 189 fun reset () = unif := IM.empty
adamc@1203 190 fun save () = !unif
adamc@1203 191 fun restore x = unif := x
adamc@1203 192
adamc@1202 193 fun lvarIn lv =
adamc@1202 194 let
adamc@1202 195 fun lvi e =
adamc@1202 196 case e of
adamc@1202 197 Const _ => false
adamc@1202 198 | Var _ => false
adamc@1202 199 | Lvar lv' => lv' = lv
adamc@1202 200 | Func (_, es) => List.exists lvi es
adamc@1202 201 | Recd xes => List.exists (lvi o #2) xes
adamc@1202 202 | Proj (e, _) => lvi e
adamc@1202 203 | Finish => false
adamc@1202 204 in
adamc@1202 205 lvi
adamc@1202 206 end
adamc@1202 207
adamc@1202 208 fun eq' (e1, e2) =
adamc@1202 209 case (e1, e2) of
adamc@1202 210 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1202 211 | (Var n1, Var n2) => n1 = n2
adamc@1202 212
adamc@1202 213 | (Lvar n1, _) =>
adamc@1202 214 (case IM.find (!unif, n1) of
adamc@1202 215 SOME e1 => eq' (e1, e2)
adamc@1202 216 | NONE =>
adamc@1202 217 case e2 of
adamc@1202 218 Lvar n2 =>
adamc@1202 219 (case IM.find (!unif, n2) of
adamc@1202 220 SOME e2 => eq' (e1, e2)
adamc@1202 221 | NONE => n1 = n2
adamc@1202 222 orelse (unif := IM.insert (!unif, n1, e2);
adamc@1202 223 true))
adamc@1202 224 | _ =>
adamc@1202 225 if lvarIn n1 e2 then
adamc@1202 226 false
adamc@1202 227 else
adamc@1202 228 (unif := IM.insert (!unif, n1, e2);
adamc@1202 229 true))
adamc@1202 230
adamc@1202 231 | (_, Lvar n2) =>
adamc@1202 232 (case IM.find (!unif, n2) of
adamc@1202 233 SOME e2 => eq' (e1, e2)
adamc@1202 234 | NONE =>
adamc@1202 235 if lvarIn n2 e1 then
adamc@1202 236 false
adamc@1202 237 else
adamc@1202 238 (unif := IM.insert (!unif, n2, e1);
adamc@1202 239 true))
adamc@1202 240
adamc@1202 241 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1202 242 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1202 243 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1202 244 | (Finish, Finish) => true
adamc@1202 245 | _ => false
adamc@1202 246
adamc@1202 247 fun eq (e1, e2) =
adamc@1202 248 let
adamc@1203 249 val saved = save ()
adamc@1202 250 in
adamc@1202 251 if eq' (simplify e1, simplify e2) then
adamc@1202 252 true
adamc@1202 253 else
adamc@1203 254 (restore saved;
adamc@1202 255 false)
adamc@1202 256 end
adamc@1202 257
adamc@1202 258 exception Imply of prop * prop
adamc@1202 259
adamc@1202 260 fun rimp ((r1, es1), (r2, es2)) =
adamc@1202 261 case (r1, r2) of
adamc@1202 262 (Sql r1', Sql r2') =>
adamc@1202 263 r1' = r2' andalso
adamc@1202 264 (case (es1, es2) of
adamc@1202 265 ([Recd xes1], [Recd xes2]) =>
adamc@1202 266 let
adamc@1203 267 val saved = save ()
adamc@1202 268 in
adamc@1202 269 if List.all (fn (f, e2) =>
adamc@1203 270 case ListUtil.search (fn (f', e1) => if f' = f then SOME e1 else NONE) xes1 of
adamc@1203 271 NONE => true
adamc@1203 272 | SOME e1 => eq (e1, e2)) xes2 then
adamc@1202 273 true
adamc@1202 274 else
adamc@1203 275 (restore saved;
adamc@1202 276 false)
adamc@1202 277 end
adamc@1202 278 | _ => false)
adamc@1202 279 | (Eq, Eq) =>
adamc@1202 280 (case (es1, es2) of
adamc@1202 281 ([x1, y1], [x2, y2]) =>
adamc@1202 282 let
adamc@1203 283 val saved = save ()
adamc@1202 284 in
adamc@1202 285 if eq (x1, x2) andalso eq (y1, y2) then
adamc@1202 286 true
adamc@1202 287 else
adamc@1203 288 (restore saved;
adamc@1202 289 (*raise Imply (Reln (Eq, es1), Reln (Eq, es2));*)
adamc@1202 290 eq (x1, y2) andalso eq (y1, x2))
adamc@1202 291 end
adamc@1202 292 | _ => false)
adamc@1202 293 | _ => false
adamc@1202 294
adamc@1202 295 fun imply (p1, p2) =
adamc@1203 296 (reset ();
adamc@1202 297 (*raise (Imply (p1, p2));*)
adamc@1202 298 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1202 299 (fn hyps =>
adamc@1202 300 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1202 301 (fn goals =>
adamc@1202 302 let
adamc@1202 303 fun gls goals onFail =
adamc@1202 304 case goals of
adamc@1202 305 [] => true
adamc@1202 306 | g :: goals =>
adamc@1202 307 let
adamc@1202 308 fun hps hyps =
adamc@1202 309 case hyps of
adamc@1202 310 [] => onFail ()
adamc@1202 311 | h :: hyps =>
adamc@1202 312 let
adamc@1203 313 val saved = save ()
adamc@1202 314 in
adamc@1202 315 if rimp (h, g) then
adamc@1202 316 let
adamc@1203 317 val changed = IM.numItems (!unif) <> IM.numItems saved
adamc@1202 318 in
adamc@1203 319 gls goals (fn () => (restore saved;
adamc@1202 320 changed andalso hps hyps))
adamc@1202 321 end
adamc@1202 322 else
adamc@1202 323 hps hyps
adamc@1202 324 end
adamc@1202 325 in
adamc@1202 326 hps hyps
adamc@1202 327 end
adamc@1202 328 in
adamc@1202 329 gls goals (fn () => false)
adamc@1202 330 end)))
adamc@1202 331
adamc@1200 332
adamc@1200 333 fun patCon pc =
adamc@1200 334 case pc of
adamc@1200 335 PConVar n => "C" ^ Int.toString n
adamc@1200 336 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 337
adamc@1202 338
adamc@1200 339
adamc@1200 340 datatype chunk =
adamc@1200 341 String of string
adamc@1200 342 | Exp of Mono.exp
adamc@1200 343
adamc@1200 344 fun chunkify e =
adamc@1200 345 case #1 e of
adamc@1200 346 EPrim (Prim.String s) => [String s]
adamc@1200 347 | EStrcat (e1, e2) => chunkify e1 @ chunkify e2
adamc@1200 348 | _ => [Exp e]
adamc@1200 349
adamc@1201 350 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 351
adamc@1201 352 fun always v chs = SOME (v, chs)
adamc@1201 353
adamc@1202 354 fun parse p s =
adamc@1202 355 case p (chunkify s) of
adamc@1201 356 SOME (v, []) => SOME v
adamc@1201 357 | _ => NONE
adamc@1201 358
adamc@1201 359 fun const s chs =
adamc@1201 360 case chs of
adamc@1201 361 String s' :: chs => if String.isPrefix s s' then
adamc@1201 362 SOME ((), if size s = size s' then
adamc@1201 363 chs
adamc@1201 364 else
adamc@1201 365 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 366 else
adamc@1201 367 NONE
adamc@1201 368 | _ => NONE
adamc@1201 369
adamc@1201 370 fun follow p1 p2 chs =
adamc@1201 371 case p1 chs of
adamc@1201 372 NONE => NONE
adamc@1201 373 | SOME (v1, chs) =>
adamc@1201 374 case p2 chs of
adamc@1201 375 NONE => NONE
adamc@1201 376 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 377
adamc@1201 378 fun wrap p f chs =
adamc@1201 379 case p chs of
adamc@1201 380 NONE => NONE
adamc@1201 381 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 382
adamc@1201 383 fun alt p1 p2 chs =
adamc@1201 384 case p1 chs of
adamc@1201 385 NONE => p2 chs
adamc@1201 386 | v => v
adamc@1201 387
adamc@1204 388 fun opt p chs =
adamc@1204 389 case p chs of
adamc@1204 390 NONE => SOME (NONE, chs)
adamc@1204 391 | SOME (v, chs) => SOME (SOME v, chs)
adamc@1204 392
adamc@1201 393 fun skip cp chs =
adamc@1201 394 case chs of
adamc@1201 395 String "" :: chs => skip cp chs
adamc@1201 396 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 397 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 398 else
adamc@1201 399 SOME ((), chs)
adamc@1201 400 | _ => SOME ((), chs)
adamc@1201 401
adamc@1201 402 fun keep cp chs =
adamc@1201 403 case chs of
adamc@1201 404 String "" :: chs => keep cp chs
adamc@1201 405 | String s :: chs' =>
adamc@1201 406 let
adamc@1201 407 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 408 in
adamc@1201 409 if Substring.isEmpty befor then
adamc@1201 410 NONE
adamc@1201 411 else
adamc@1201 412 SOME (Substring.string befor,
adamc@1201 413 if Substring.isEmpty after then
adamc@1201 414 chs'
adamc@1201 415 else
adamc@1201 416 String (Substring.string after) :: chs')
adamc@1201 417 end
adamc@1201 418 | _ => NONE
adamc@1201 419
adamc@1204 420 fun ws p = wrap (follow (skip (fn ch => ch = #" "))
adamc@1204 421 (follow p (skip (fn ch => ch = #" ")))) (#1 o #2)
adamc@1204 422
adamc@1206 423 val debug = ref false
adamc@1206 424
adamc@1204 425 fun log name p chs =
adamc@1206 426 (if !debug then
adamc@1206 427 case chs of
adamc@1206 428 String s :: [] => print (name ^ ": " ^ s ^ "\n")
adamc@1206 429 | _ => print (name ^ ": blocked!\n")
adamc@1206 430 else
adamc@1206 431 ();
adamc@1204 432 p chs)
adamc@1201 433
adamc@1201 434 fun list p chs =
adamc@1201 435 (alt (wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1201 436 (fn (v, ((), ls)) => v :: ls))
adamc@1201 437 (alt (wrap (ws p) (fn v => [v]))
adamc@1201 438 (always []))) chs
adamc@1201 439
adamc@1201 440 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 441
adamc@1201 442 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
adamc@1201 443 String.extract (s, 2, NONE)
adamc@1201 444 else
adamc@1201 445 raise Fail "Iflow: Bad table variable")
adamc@1201 446 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then
adamc@1201 447 String.extract (s, 3, NONE)
adamc@1201 448 else
adamc@1201 449 raise Fail "Iflow: Bad uw_* variable")
adamc@1201 450
adamc@1201 451 val sitem = wrap (follow t_ident
adamc@1201 452 (follow (const ".")
adamc@1201 453 uw_ident))
adamc@1201 454 (fn (t, ((), f)) => (t, f))
adamc@1201 455
adamc@1206 456 datatype Rel =
adamc@1206 457 Exps of exp * exp -> prop
adamc@1206 458 | Props of prop * prop -> prop
adamc@1206 459
adamc@1204 460 datatype sqexp =
adamc@1206 461 SqConst of Prim.t
adamc@1206 462 | Field of string * string
adamc@1206 463 | Binop of Rel * sqexp * sqexp
adamc@1204 464
adamc@1206 465 val sqbrel = alt (wrap (const "=") (fn () => Exps (fn (e1, e2) => Reln (Eq, [e1, e2]))))
adamc@1206 466 (alt (wrap (const "AND") (fn () => Props And))
adamc@1206 467 (wrap (const "OR") (fn () => Props Or)))
adamc@1204 468
adamc@1204 469 datatype ('a, 'b) sum = inl of 'a | inr of 'b
adamc@1204 470
adamc@1206 471 fun int chs =
adamc@1206 472 case chs of
adamc@1206 473 String s :: chs' =>
adamc@1206 474 let
adamc@1206 475 val (befor, after) = Substring.splitl Char.isDigit (Substring.full s)
adamc@1206 476 in
adamc@1206 477 if Substring.isEmpty befor then
adamc@1206 478 NONE
adamc@1206 479 else case Int64.fromString (Substring.string befor) of
adamc@1206 480 NONE => NONE
adamc@1206 481 | SOME n => SOME (n, if Substring.isEmpty after then
adamc@1206 482 chs'
adamc@1206 483 else
adamc@1206 484 String (Substring.string after) :: chs')
adamc@1206 485 end
adamc@1206 486 | _ => NONE
adamc@1206 487
adamc@1206 488 val prim = wrap (follow (wrap int Prim.Int) (opt (const "::int8"))) #1
adamc@1206 489
adamc@1204 490 fun sqexp chs =
adamc@1206 491 log "sqexp"
adamc@1206 492 (alt
adamc@1206 493 (wrap prim SqConst)
adamc@1206 494 (alt
adamc@1206 495 (wrap sitem Field)
adamc@1206 496 (wrap
adamc@1206 497 (follow (ws (const "("))
adamc@1206 498 (follow (wrap
adamc@1206 499 (follow sqexp
adamc@1206 500 (alt
adamc@1206 501 (wrap
adamc@1206 502 (follow (ws sqbrel)
adamc@1206 503 (ws sqexp))
adamc@1206 504 inl)
adamc@1206 505 (always (inr ()))))
adamc@1206 506 (fn (e1, sm) =>
adamc@1206 507 case sm of
adamc@1206 508 inl (bo, e2) => Binop (bo, e1, e2)
adamc@1206 509 | inr () => e1))
adamc@1206 510 (const ")")))
adamc@1206 511 (fn ((), (e, ())) => e))))
adamc@1206 512 chs
adamc@1206 513
adamc@1201 514 val select = wrap (follow (const "SELECT ") (list sitem))
adamc@1201 515 (fn ((), ls) => ls)
adamc@1201 516
adamc@1201 517 val fitem = wrap (follow uw_ident
adamc@1201 518 (follow (const " AS ")
adamc@1201 519 t_ident))
adamc@1201 520 (fn (t, ((), f)) => (t, f))
adamc@1201 521
adamc@1201 522 val from = wrap (follow (const "FROM ") (list fitem))
adamc@1201 523 (fn ((), ls) => ls)
adamc@1201 524
adamc@1204 525 val wher = wrap (follow (ws (const "WHERE ")) sqexp)
adamc@1204 526 (fn ((), ls) => ls)
adamc@1204 527
adamc@1204 528 val query = wrap (follow (follow select from) (opt wher))
adamc@1204 529 (fn ((fs, ts), wher) => {Select = fs, From = ts, Where = wher})
adamc@1201 530
adamc@1202 531 fun queryProp rv oe e =
adamc@1202 532 case parse query e of
adamc@1204 533 NONE => (print "Crap\n"; Unknown)
adamc@1201 534 | SOME r =>
adamc@1202 535 let
adamc@1202 536 val p =
adamc@1202 537 foldl (fn ((t, v), p) =>
adamc@1202 538 And (p,
adamc@1202 539 Reln (Sql t,
adamc@1202 540 [Recd (foldl (fn ((v', f), fs) =>
adamc@1202 541 if v' = v then
adamc@1202 542 (f, Proj (Proj (Lvar rv, v), f)) :: fs
adamc@1202 543 else
adamc@1202 544 fs) [] (#Select r))])))
adamc@1202 545 True (#From r)
adamc@1205 546
adamc@1205 547 fun expIn e =
adamc@1205 548 case e of
adamc@1206 549 SqConst p => inl (Const p)
adamc@1206 550 | Field (v, f) => inl (Proj (Proj (Lvar rv, v), f))
adamc@1205 551 | Binop (bo, e1, e2) =>
adamc@1206 552 inr (case (bo, expIn e1, expIn e2) of
adamc@1206 553 (Exps f, inl e1, inl e2) => f (e1, e2)
adamc@1206 554 | (Props f, inr p1, inr p2) => f (p1, p2)
adamc@1206 555 | _ => Unknown)
adamc@1205 556
adamc@1205 557 val p = case #Where r of
adamc@1205 558 NONE => p
adamc@1205 559 | SOME e =>
adamc@1205 560 case expIn e of
adamc@1205 561 inr p' => And (p, p')
adamc@1205 562 | _ => p
adamc@1202 563 in
adamc@1202 564 case oe of
adamc@1202 565 NONE => p
adamc@1202 566 | SOME oe =>
adamc@1205 567 And (p, foldl (fn ((v, f), p) =>
adamc@1205 568 Or (p,
adamc@1205 569 Reln (Eq, [oe, Proj (Proj (Lvar rv, v), f)])))
adamc@1205 570 False (#Select r))
adamc@1202 571 end
adamc@1200 572
adamc@1202 573 fun evalExp env (e as (_, loc), st as (nv, p, sent)) =
adamc@1200 574 let
adamc@1200 575 fun default () =
adamc@1200 576 (Var nv, (nv+1, p, sent))
adamc@1200 577
adamc@1200 578 fun addSent (p, e, sent) =
adamc@1200 579 if isKnown e then
adamc@1200 580 sent
adamc@1200 581 else
adamc@1202 582 (loc, e, p) :: sent
adamc@1200 583 in
adamc@1200 584 case #1 e of
adamc@1200 585 EPrim p => (Const p, st)
adamc@1200 586 | ERel n => (List.nth (env, n), st)
adamc@1200 587 | ENamed _ => default ()
adamc@1200 588 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200 589 | ECon (_, pc, SOME e) =>
adamc@1200 590 let
adamc@1200 591 val (e, st) = evalExp env (e, st)
adamc@1200 592 in
adamc@1200 593 (Func (patCon pc, [e]), st)
adamc@1200 594 end
adamc@1200 595 | ENone _ => (Func ("None", []), st)
adamc@1200 596 | ESome (_, e) =>
adamc@1200 597 let
adamc@1200 598 val (e, st) = evalExp env (e, st)
adamc@1200 599 in
adamc@1200 600 (Func ("Some", [e]), st)
adamc@1200 601 end
adamc@1200 602 | EFfi _ => default ()
adamc@1200 603 | EFfiApp (m, s, es) =>
adamc@1200 604 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 605 let
adamc@1200 606 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 607 in
adamc@1200 608 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200 609 end
adamc@1200 610 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 611 default ()
adamc@1200 612 else
adamc@1200 613 let
adamc@1200 614 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 615 in
adamc@1200 616 (Func (m ^ "." ^ s, es), st)
adamc@1200 617 end
adamc@1200 618 | EApp _ => default ()
adamc@1200 619 | EAbs _ => default ()
adamc@1200 620 | EUnop (s, e1) =>
adamc@1200 621 let
adamc@1200 622 val (e1, st) = evalExp env (e1, st)
adamc@1200 623 in
adamc@1200 624 (Func (s, [e1]), st)
adamc@1200 625 end
adamc@1200 626 | EBinop (s, e1, e2) =>
adamc@1200 627 let
adamc@1200 628 val (e1, st) = evalExp env (e1, st)
adamc@1200 629 val (e2, st) = evalExp env (e2, st)
adamc@1200 630 in
adamc@1200 631 (Func (s, [e1, e2]), st)
adamc@1200 632 end
adamc@1200 633 | ERecord xets =>
adamc@1200 634 let
adamc@1200 635 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 636 let
adamc@1200 637 val (e, st) = evalExp env (e, st)
adamc@1200 638 in
adamc@1200 639 ((x, e), st)
adamc@1200 640 end) st xets
adamc@1200 641 in
adamc@1200 642 (Recd xes, st)
adamc@1200 643 end
adamc@1200 644 | EField (e, s) =>
adamc@1200 645 let
adamc@1200 646 val (e, st) = evalExp env (e, st)
adamc@1200 647 in
adamc@1200 648 (Proj (e, s), st)
adamc@1200 649 end
adamc@1200 650 | ECase _ => default ()
adamc@1200 651 | EStrcat (e1, e2) =>
adamc@1200 652 let
adamc@1200 653 val (e1, st) = evalExp env (e1, st)
adamc@1200 654 val (e2, st) = evalExp env (e2, st)
adamc@1200 655 in
adamc@1200 656 (Func ("cat", [e1, e2]), st)
adamc@1200 657 end
adamc@1200 658 | EError _ => (Finish, st)
adamc@1200 659 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 660 let
adamc@1200 661 val (b, st) = evalExp env (b, st)
adamc@1200 662 val (m, st) = evalExp env (m, st)
adamc@1200 663 in
adamc@1200 664 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200 665 end
adamc@1200 666 | ERedirect (e, _) =>
adamc@1200 667 let
adamc@1200 668 val (e, st) = evalExp env (e, st)
adamc@1200 669 in
adamc@1200 670 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 671 end
adamc@1200 672 | EWrite e =>
adamc@1200 673 let
adamc@1200 674 val (e, st) = evalExp env (e, st)
adamc@1200 675 in
adamc@1200 676 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 677 end
adamc@1200 678 | ESeq (e1, e2) =>
adamc@1200 679 let
adamc@1200 680 val (_, st) = evalExp env (e1, st)
adamc@1200 681 in
adamc@1200 682 evalExp env (e2, st)
adamc@1200 683 end
adamc@1200 684 | ELet (_, _, e1, e2) =>
adamc@1200 685 let
adamc@1200 686 val (e1, st) = evalExp env (e1, st)
adamc@1200 687 in
adamc@1200 688 evalExp (e1 :: env) (e2, st)
adamc@1200 689 end
adamc@1200 690 | EClosure (n, es) =>
adamc@1200 691 let
adamc@1200 692 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 693 in
adamc@1200 694 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200 695 end
adamc@1200 696
adamc@1200 697 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 698 let
adamc@1200 699 val (_, st) = evalExp env (q, st)
adamc@1200 700 val (i, st) = evalExp env (i, st)
adamc@1200 701
adamc@1200 702 val r = #1 st
adamc@1200 703 val acc = #1 st + 1
adamc@1200 704 val st' = (#1 st + 2, #2 st, #3 st)
adamc@1200 705
adamc@1200 706 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 707
adamc@1200 708 val r' = newLvar ()
adamc@1200 709 val acc' = newLvar ()
adamc@1202 710 val qp = queryProp r' NONE q
adamc@1200 711
adamc@1200 712 val doSubExp = subExp (r, r') o subExp (acc, acc')
adamc@1200 713 val doSubProp = subProp (r, r') o subProp (acc, acc')
adamc@1200 714
adamc@1200 715 val p = doSubProp (#2 st')
adamc@1200 716 val p = And (p, qp)
adamc@1200 717 val p = Select (r, r', acc', p, doSubExp b)
adamc@1200 718 in
adamc@1202 719 (Var r, (#1 st + 1, And (#2 st, p), map (fn (loc, e, p) => (loc,
adamc@1202 720 doSubExp e,
adamc@1202 721 And (qp, doSubProp p))) (#3 st')))
adamc@1200 722 end
adamc@1200 723 | EDml _ => default ()
adamc@1200 724 | ENextval _ => default ()
adamc@1200 725 | ESetval _ => default ()
adamc@1200 726
adamc@1200 727 | EUnurlify _ => default ()
adamc@1200 728 | EJavaScript _ => default ()
adamc@1200 729 | ESignalReturn _ => default ()
adamc@1200 730 | ESignalBind _ => default ()
adamc@1200 731 | ESignalSource _ => default ()
adamc@1200 732 | EServerCall _ => default ()
adamc@1200 733 | ERecv _ => default ()
adamc@1200 734 | ESleep _ => default ()
adamc@1200 735 | ESpawn _ => default ()
adamc@1200 736 end
adamc@1200 737
adamc@1200 738 fun check file =
adamc@1200 739 let
adamc@1202 740 fun decl ((d, _), (vals, pols)) =
adamc@1200 741 case d of
adamc@1200 742 DVal (x, _, _, e, _) =>
adamc@1200 743 let
adamc@1200 744 fun deAbs (e, env, nv) =
adamc@1200 745 case #1 e of
adamc@1200 746 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
adamc@1200 747 | _ => (e, env, nv)
adamc@1200 748
adamc@1202 749 val (e, env, nv) = deAbs (e, [], 1)
adamc@1200 750
adamc@1200 751 val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
adamc@1200 752 in
adamc@1202 753 ((x, e, p, sent) :: vals, pols)
adamc@1200 754 end
adamc@1202 755
adamc@1202 756 | DPolicy (PolQuery e) => (vals, queryProp 0 (SOME (Var 0)) e :: pols)
adamc@1202 757
adamc@1202 758 | _ => (vals, pols)
adamc@1202 759
adamc@1203 760 val () = reset ()
adamc@1202 761
adamc@1202 762 val (vals, pols) = foldl decl ([], []) file
adamc@1200 763 in
adamc@1202 764 app (fn (name, _, _, sent) =>
adamc@1202 765 app (fn (loc, e, p) =>
adamc@1202 766 let
adamc@1202 767 val p = And (p, Reln (Eq, [Var 0, e]))
adamc@1202 768 in
adamc@1202 769 if List.exists (fn pol => imply (p, pol)) pols then
adamc@1202 770 ()
adamc@1202 771 else
adamc@1202 772 ErrorMsg.errorAt loc "The information flow policy may be violated here."
adamc@1202 773 end) sent) vals
adamc@1200 774 end
adamc@1200 775
adamc@1200 776 end