Mercurial > urweb

annotate src/iflow.sml @ 1201:8793fd48968c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generating a good Iflow condition for a test query
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Apr 2010 15:17:57 -0400
parents 5eac14322548
children 509a6d7b60fb
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@1200 32 structure SS = BinarySetFn(struct
adamc@1200 33 type ord_key = string
adamc@1200 34 val compare = String.compare
adamc@1200 35 end)
adamc@1200 36
adamc@1200 37 val writers = ["htmlifyInt_w",
adamc@1200 38 "htmlifyFloat_w",
adamc@1200 39 "htmlifyString_w",
adamc@1200 40 "htmlifyBool_w",
adamc@1200 41 "htmlifyTime_w",
adamc@1200 42 "attrifyInt_w",
adamc@1200 43 "attrifyFloat_w",
adamc@1200 44 "attrifyString_w",
adamc@1200 45 "attrifyChar_w",
adamc@1200 46 "urlifyInt_w",
adamc@1200 47 "urlifyFloat_w",
adamc@1200 48 "urlifyString_w",
adamc@1200 49 "urlifyBool_w"]
adamc@1200 50
adamc@1200 51 val writers = SS.addList (SS.empty, writers)
adamc@1200 52
adamc@1200 53 type lvar = int
adamc@1200 54
adamc@1200 55 datatype exp =
adamc@1200 56 Const of Prim.t
adamc@1200 57 | Var of int
adamc@1200 58 | Lvar of lvar
adamc@1200 59 | Func of string * exp list
adamc@1200 60 | Recd of (string * exp) list
adamc@1200 61 | Proj of exp * string
adamc@1200 62 | Finish
adamc@1200 63
adamc@1200 64 datatype reln =
adamc@1200 65 Sql of string
adamc@1200 66 | Eq
adamc@1200 67
adamc@1200 68 datatype prop =
adamc@1200 69 True
adamc@1200 70 | False
adamc@1200 71 | Unknown
adamc@1200 72 | And of prop * prop
adamc@1200 73 | Or of prop * prop
adamc@1200 74 | Reln of reln * exp list
adamc@1200 75 | Select of int * lvar * lvar * prop * exp
adamc@1200 76
adamc@1200 77 local
adamc@1200 78 val count = ref 0
adamc@1200 79 in
adamc@1200 80 fun newLvar () =
adamc@1200 81 let
adamc@1200 82 val n = !count
adamc@1200 83 in
adamc@1200 84 count := n + 1;
adamc@1200 85 n
adamc@1200 86 end
adamc@1200 87 end
adamc@1200 88
adamc@1200 89 fun subExp (v, lv) =
adamc@1200 90 let
adamc@1200 91 fun sub e =
adamc@1200 92 case e of
adamc@1200 93 Const _ => e
adamc@1200 94 | Var v' => if v' = v then Lvar lv else e
adamc@1200 95 | Lvar _ => e
adamc@1200 96 | Func (f, es) => Func (f, map sub es)
adamc@1200 97 | Recd xes => Recd (map (fn (x, e) => (x, sub e)) xes)
adamc@1200 98 | Proj (e, s) => Proj (sub e, s)
adamc@1200 99 | Finish => Finish
adamc@1200 100 in
adamc@1200 101 sub
adamc@1200 102 end
adamc@1200 103
adamc@1200 104 fun subProp (v, lv) =
adamc@1200 105 let
adamc@1200 106 fun sub p =
adamc@1200 107 case p of
adamc@1200 108 True => p
adamc@1200 109 | False => p
adamc@1200 110 | Unknown => p
adamc@1200 111 | And (p1, p2) => And (sub p1, sub p2)
adamc@1200 112 | Or (p1, p2) => Or (sub p1, sub p2)
adamc@1200 113 | Reln (r, es) => Reln (r, map (subExp (v, lv)) es)
adamc@1200 114 | Select (v1, lv1, lv2, p, e) => Select (v1, lv1, lv2, sub p, subExp (v, lv) e)
adamc@1200 115 in
adamc@1200 116 sub
adamc@1200 117 end
adamc@1200 118
adamc@1200 119 fun eq' (e1, e2) =
adamc@1200 120 case (e1, e2) of
adamc@1200 121 (Const p1, Const p2) => Prim.equal (p1, p2)
adamc@1200 122 | (Var n1, Var n2) => n1 = n2
adamc@1200 123 | (Lvar n1, Lvar n2) => n1 = n2
adamc@1200 124 | (Func (f1, es1), Func (f2, es2)) => f1 = f2 andalso ListPair.allEq eq' (es1, es2)
adamc@1200 125 | (Recd xes1, Recd xes2) => ListPair.allEq (fn ((x1, e1), (x2, e2)) => x1 = x2 andalso eq' (e1, e2)) (xes1, xes2)
adamc@1200 126 | (Proj (e1, s1), Proj (e2, s2)) => eq' (e1, e2) andalso s1 = s2
adamc@1200 127 | (Finish, Finish) => true
adamc@1200 128 | _ => false
adamc@1200 129
adamc@1200 130 fun isKnown e =
adamc@1200 131 case e of
adamc@1200 132 Const _ => true
adamc@1200 133 | Func (_, es) => List.all isKnown es
adamc@1200 134 | Recd xes => List.all (isKnown o #2) xes
adamc@1200 135 | Proj (e, _) => isKnown e
adamc@1200 136 | _ => false
adamc@1200 137
adamc@1200 138 fun isFinish e =
adamc@1200 139 case e of
adamc@1200 140 Finish => true
adamc@1200 141 | _ => false
adamc@1200 142
adamc@1200 143 fun simplify e =
adamc@1200 144 case e of
adamc@1200 145 Const _ => e
adamc@1200 146 | Var _ => e
adamc@1200 147 | Lvar _ => e
adamc@1200 148 | Func (f, es) =>
adamc@1200 149 let
adamc@1200 150 val es = map simplify es
adamc@1200 151 in
adamc@1200 152 if List.exists isFinish es then
adamc@1200 153 Finish
adamc@1200 154 else
adamc@1200 155 Func (f, es)
adamc@1200 156 end
adamc@1200 157 | Recd xes =>
adamc@1200 158 let
adamc@1200 159 val xes = map (fn (x, e) => (x, simplify e)) xes
adamc@1200 160 in
adamc@1200 161 if List.exists (isFinish o #2) xes then
adamc@1200 162 Finish
adamc@1200 163 else
adamc@1200 164 Recd xes
adamc@1200 165 end
adamc@1200 166 | Proj (e, s) =>
adamc@1200 167 (case simplify e of
adamc@1200 168 Recd xes =>
adamc@1200 169 getOpt (ListUtil.search (fn (x, e') => if x = s then SOME e' else NONE) xes, Recd xes)
adamc@1200 170 | e' =>
adamc@1200 171 if isFinish e' then
adamc@1200 172 Finish
adamc@1200 173 else
adamc@1200 174 Proj (e', s))
adamc@1200 175 | Finish => Finish
adamc@1200 176
adamc@1200 177 fun eq (e1, e2) = eq' (simplify e1, simplify e2)
adamc@1200 178
adamc@1200 179 fun decomp or =
adamc@1200 180 let
adamc@1200 181 fun decomp p k =
adamc@1200 182 case p of
adamc@1200 183 True => k []
adamc@1200 184 | False => true
adamc@1200 185 | Unknown => k []
adamc@1200 186 | And (p1, p2) =>
adamc@1200 187 decomp p1 (fn ps1 =>
adamc@1200 188 decomp p2 (fn ps2 =>
adamc@1200 189 k (ps1 @ ps2)))
adamc@1200 190 | Or (p1, p2) =>
adamc@1200 191 or (decomp p1 k, fn () => decomp p2 k)
adamc@1200 192 | Reln x => k [x]
adamc@1200 193 | Select _ => k []
adamc@1200 194 in
adamc@1200 195 decomp
adamc@1200 196 end
adamc@1200 197
adamc@1200 198 fun rimp ((r1 : reln, es1), (r2, es2)) =
adamc@1200 199 r1 = r2 andalso ListPair.allEq eq (es1, es2)
adamc@1200 200
adamc@1200 201 fun imp (p1, p2) =
adamc@1200 202 decomp (fn (e1, e2) => e1 andalso e2 ()) p1
adamc@1200 203 (fn hyps =>
adamc@1200 204 decomp (fn (e1, e2) => e1 orelse e2 ()) p2
adamc@1200 205 (fn goals =>
adamc@1200 206 List.all (fn r2 => List.exists (fn r1 => rimp (r1, r2)) hyps) goals))
adamc@1200 207
adamc@1200 208 fun patCon pc =
adamc@1200 209 case pc of
adamc@1200 210 PConVar n => "C" ^ Int.toString n
adamc@1200 211 | PConFfi {mod = m, datatyp = d, con = c, ...} => m ^ "." ^ d ^ "." ^ c
adamc@1200 212
adamc@1200 213 exception Summaries of (string * exp * prop * (exp * prop) list) list
adamc@1200 214
adamc@1200 215 datatype chunk =
adamc@1200 216 String of string
adamc@1200 217 | Exp of Mono.exp
adamc@1200 218
adamc@1200 219 fun chunkify e =
adamc@1200 220 case #1 e of
adamc@1200 221 EPrim (Prim.String s) => [String s]
adamc@1200 222 | EStrcat (e1, e2) => chunkify e1 @ chunkify e2
adamc@1200 223 | _ => [Exp e]
adamc@1200 224
adamc@1201 225 type 'a parser = chunk list -> ('a * chunk list) option
adamc@1201 226
adamc@1201 227 fun always v chs = SOME (v, chs)
adamc@1201 228
adamc@1201 229 fun parse p chs =
adamc@1201 230 case p chs of
adamc@1201 231 SOME (v, []) => SOME v
adamc@1201 232 | _ => NONE
adamc@1201 233
adamc@1201 234 fun const s chs =
adamc@1201 235 case chs of
adamc@1201 236 String s' :: chs => if String.isPrefix s s' then
adamc@1201 237 SOME ((), if size s = size s' then
adamc@1201 238 chs
adamc@1201 239 else
adamc@1201 240 String (String.extract (s', size s, NONE)) :: chs)
adamc@1201 241 else
adamc@1201 242 NONE
adamc@1201 243 | _ => NONE
adamc@1201 244
adamc@1201 245 fun follow p1 p2 chs =
adamc@1201 246 case p1 chs of
adamc@1201 247 NONE => NONE
adamc@1201 248 | SOME (v1, chs) =>
adamc@1201 249 case p2 chs of
adamc@1201 250 NONE => NONE
adamc@1201 251 | SOME (v2, chs) => SOME ((v1, v2), chs)
adamc@1201 252
adamc@1201 253 fun wrap p f chs =
adamc@1201 254 case p chs of
adamc@1201 255 NONE => NONE
adamc@1201 256 | SOME (v, chs) => SOME (f v, chs)
adamc@1201 257
adamc@1201 258 fun alt p1 p2 chs =
adamc@1201 259 case p1 chs of
adamc@1201 260 NONE => p2 chs
adamc@1201 261 | v => v
adamc@1201 262
adamc@1201 263 fun skip cp chs =
adamc@1201 264 case chs of
adamc@1201 265 String "" :: chs => skip cp chs
adamc@1201 266 | String s :: chs' => if cp (String.sub (s, 0)) then
adamc@1201 267 skip cp (String (String.extract (s, 1, NONE)) :: chs')
adamc@1201 268 else
adamc@1201 269 SOME ((), chs)
adamc@1201 270 | _ => SOME ((), chs)
adamc@1201 271
adamc@1201 272 fun keep cp chs =
adamc@1201 273 case chs of
adamc@1201 274 String "" :: chs => keep cp chs
adamc@1201 275 | String s :: chs' =>
adamc@1201 276 let
adamc@1201 277 val (befor, after) = Substring.splitl cp (Substring.full s)
adamc@1201 278 in
adamc@1201 279 if Substring.isEmpty befor then
adamc@1201 280 NONE
adamc@1201 281 else
adamc@1201 282 SOME (Substring.string befor,
adamc@1201 283 if Substring.isEmpty after then
adamc@1201 284 chs'
adamc@1201 285 else
adamc@1201 286 String (Substring.string after) :: chs')
adamc@1201 287 end
adamc@1201 288 | _ => NONE
adamc@1201 289
adamc@1201 290 fun ws p = wrap (follow p (skip (fn ch => ch = #" "))) #1
adamc@1201 291
adamc@1201 292 fun list p chs =
adamc@1201 293 (alt (wrap (follow p (follow (ws (const ",")) (list p)))
adamc@1201 294 (fn (v, ((), ls)) => v :: ls))
adamc@1201 295 (alt (wrap (ws p) (fn v => [v]))
adamc@1201 296 (always []))) chs
adamc@1201 297
adamc@1201 298 val ident = keep (fn ch => Char.isAlphaNum ch orelse ch = #"_")
adamc@1201 299
adamc@1201 300 val t_ident = wrap ident (fn s => if String.isPrefix "T_" s then
adamc@1201 301 String.extract (s, 2, NONE)
adamc@1201 302 else
adamc@1201 303 raise Fail "Iflow: Bad table variable")
adamc@1201 304 val uw_ident = wrap ident (fn s => if String.isPrefix "uw_" s then
adamc@1201 305 String.extract (s, 3, NONE)
adamc@1201 306 else
adamc@1201 307 raise Fail "Iflow: Bad uw_* variable")
adamc@1201 308
adamc@1201 309 val sitem = wrap (follow t_ident
adamc@1201 310 (follow (const ".")
adamc@1201 311 uw_ident))
adamc@1201 312 (fn (t, ((), f)) => (t, f))
adamc@1201 313
adamc@1201 314 val select = wrap (follow (const "SELECT ") (list sitem))
adamc@1201 315 (fn ((), ls) => ls)
adamc@1201 316
adamc@1201 317 val fitem = wrap (follow uw_ident
adamc@1201 318 (follow (const " AS ")
adamc@1201 319 t_ident))
adamc@1201 320 (fn (t, ((), f)) => (t, f))
adamc@1201 321
adamc@1201 322 val from = wrap (follow (const "FROM ") (list fitem))
adamc@1201 323 (fn ((), ls) => ls)
adamc@1201 324
adamc@1201 325 val query = wrap (follow select from)
adamc@1201 326 (fn (fs, ts) => {Select = fs, From = ts})
adamc@1201 327
adamc@1200 328 fun queryProp rv e =
adamc@1201 329 case parse query (chunkify e) of
adamc@1201 330 NONE => Unknown
adamc@1201 331 | SOME r =>
adamc@1201 332 foldl (fn ((t, v), p) =>
adamc@1201 333 And (p,
adamc@1201 334 Reln (Sql t,
adamc@1201 335 [Recd (foldl (fn ((v', f), fs) =>
adamc@1201 336 if v' = v then
adamc@1201 337 (f, Proj (Proj (Lvar rv, v), f)) :: fs
adamc@1201 338 else
adamc@1201 339 fs) [] (#Select r))])))
adamc@1201 340 True (#From r)
adamc@1200 341
adamc@1200 342 fun evalExp env (e : Mono.exp, st as (nv, p, sent)) =
adamc@1200 343 let
adamc@1200 344 fun default () =
adamc@1200 345 (Var nv, (nv+1, p, sent))
adamc@1200 346
adamc@1200 347 fun addSent (p, e, sent) =
adamc@1200 348 if isKnown e then
adamc@1200 349 sent
adamc@1200 350 else
adamc@1200 351 (e, p) :: sent
adamc@1200 352 in
adamc@1200 353 case #1 e of
adamc@1200 354 EPrim p => (Const p, st)
adamc@1200 355 | ERel n => (List.nth (env, n), st)
adamc@1200 356 | ENamed _ => default ()
adamc@1200 357 | ECon (_, pc, NONE) => (Func (patCon pc, []), st)
adamc@1200 358 | ECon (_, pc, SOME e) =>
adamc@1200 359 let
adamc@1200 360 val (e, st) = evalExp env (e, st)
adamc@1200 361 in
adamc@1200 362 (Func (patCon pc, [e]), st)
adamc@1200 363 end
adamc@1200 364 | ENone _ => (Func ("None", []), st)
adamc@1200 365 | ESome (_, e) =>
adamc@1200 366 let
adamc@1200 367 val (e, st) = evalExp env (e, st)
adamc@1200 368 in
adamc@1200 369 (Func ("Some", [e]), st)
adamc@1200 370 end
adamc@1200 371 | EFfi _ => default ()
adamc@1200 372 | EFfiApp (m, s, es) =>
adamc@1200 373 if m = "Basis" andalso SS.member (writers, s) then
adamc@1200 374 let
adamc@1200 375 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 376 in
adamc@1200 377 (Func ("unit", []), (#1 st, p, foldl (fn (e, sent) => addSent (#2 st, e, sent)) sent es))
adamc@1200 378 end
adamc@1200 379 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
adamc@1200 380 default ()
adamc@1200 381 else
adamc@1200 382 let
adamc@1200 383 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 384 in
adamc@1200 385 (Func (m ^ "." ^ s, es), st)
adamc@1200 386 end
adamc@1200 387 | EApp _ => default ()
adamc@1200 388 | EAbs _ => default ()
adamc@1200 389 | EUnop (s, e1) =>
adamc@1200 390 let
adamc@1200 391 val (e1, st) = evalExp env (e1, st)
adamc@1200 392 in
adamc@1200 393 (Func (s, [e1]), st)
adamc@1200 394 end
adamc@1200 395 | EBinop (s, e1, e2) =>
adamc@1200 396 let
adamc@1200 397 val (e1, st) = evalExp env (e1, st)
adamc@1200 398 val (e2, st) = evalExp env (e2, st)
adamc@1200 399 in
adamc@1200 400 (Func (s, [e1, e2]), st)
adamc@1200 401 end
adamc@1200 402 | ERecord xets =>
adamc@1200 403 let
adamc@1200 404 val (xes, st) = ListUtil.foldlMap (fn ((x, e, _), st) =>
adamc@1200 405 let
adamc@1200 406 val (e, st) = evalExp env (e, st)
adamc@1200 407 in
adamc@1200 408 ((x, e), st)
adamc@1200 409 end) st xets
adamc@1200 410 in
adamc@1200 411 (Recd xes, st)
adamc@1200 412 end
adamc@1200 413 | EField (e, s) =>
adamc@1200 414 let
adamc@1200 415 val (e, st) = evalExp env (e, st)
adamc@1200 416 in
adamc@1200 417 (Proj (e, s), st)
adamc@1200 418 end
adamc@1200 419 | ECase _ => default ()
adamc@1200 420 | EStrcat (e1, e2) =>
adamc@1200 421 let
adamc@1200 422 val (e1, st) = evalExp env (e1, st)
adamc@1200 423 val (e2, st) = evalExp env (e2, st)
adamc@1200 424 in
adamc@1200 425 (Func ("cat", [e1, e2]), st)
adamc@1200 426 end
adamc@1200 427 | EError _ => (Finish, st)
adamc@1200 428 | EReturnBlob {blob = b, mimeType = m, ...} =>
adamc@1200 429 let
adamc@1200 430 val (b, st) = evalExp env (b, st)
adamc@1200 431 val (m, st) = evalExp env (m, st)
adamc@1200 432 in
adamc@1200 433 (Finish, (#1 st, p, addSent (#2 st, b, addSent (#2 st, m, sent))))
adamc@1200 434 end
adamc@1200 435 | ERedirect (e, _) =>
adamc@1200 436 let
adamc@1200 437 val (e, st) = evalExp env (e, st)
adamc@1200 438 in
adamc@1200 439 (Finish, (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 440 end
adamc@1200 441 | EWrite e =>
adamc@1200 442 let
adamc@1200 443 val (e, st) = evalExp env (e, st)
adamc@1200 444 in
adamc@1200 445 (Func ("unit", []), (#1 st, p, addSent (#2 st, e, sent)))
adamc@1200 446 end
adamc@1200 447 | ESeq (e1, e2) =>
adamc@1200 448 let
adamc@1200 449 val (_, st) = evalExp env (e1, st)
adamc@1200 450 in
adamc@1200 451 evalExp env (e2, st)
adamc@1200 452 end
adamc@1200 453 | ELet (_, _, e1, e2) =>
adamc@1200 454 let
adamc@1200 455 val (e1, st) = evalExp env (e1, st)
adamc@1200 456 in
adamc@1200 457 evalExp (e1 :: env) (e2, st)
adamc@1200 458 end
adamc@1200 459 | EClosure (n, es) =>
adamc@1200 460 let
adamc@1200 461 val (es, st) = ListUtil.foldlMap (evalExp env) st es
adamc@1200 462 in
adamc@1200 463 (Func ("Cl" ^ Int.toString n, es), st)
adamc@1200 464 end
adamc@1200 465
adamc@1200 466 | EQuery {query = q, body = b, initial = i, ...} =>
adamc@1200 467 let
adamc@1200 468 val (_, st) = evalExp env (q, st)
adamc@1200 469 val (i, st) = evalExp env (i, st)
adamc@1200 470
adamc@1200 471 val r = #1 st
adamc@1200 472 val acc = #1 st + 1
adamc@1200 473 val st' = (#1 st + 2, #2 st, #3 st)
adamc@1200 474
adamc@1200 475 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
adamc@1200 476
adamc@1200 477 val r' = newLvar ()
adamc@1200 478 val acc' = newLvar ()
adamc@1200 479 val qp = queryProp r' q
adamc@1200 480
adamc@1200 481 val doSubExp = subExp (r, r') o subExp (acc, acc')
adamc@1200 482 val doSubProp = subProp (r, r') o subProp (acc, acc')
adamc@1200 483
adamc@1200 484 val p = doSubProp (#2 st')
adamc@1200 485 val p = And (p, qp)
adamc@1200 486 val p = Select (r, r', acc', p, doSubExp b)
adamc@1200 487 in
adamc@1200 488 (Var r, (#1 st + 1, And (#2 st, p), map (fn (e, p) => (doSubExp e, And (qp, doSubProp p))) (#3 st')))
adamc@1200 489 end
adamc@1200 490 | EDml _ => default ()
adamc@1200 491 | ENextval _ => default ()
adamc@1200 492 | ESetval _ => default ()
adamc@1200 493
adamc@1200 494 | EUnurlify _ => default ()
adamc@1200 495 | EJavaScript _ => default ()
adamc@1200 496 | ESignalReturn _ => default ()
adamc@1200 497 | ESignalBind _ => default ()
adamc@1200 498 | ESignalSource _ => default ()
adamc@1200 499 | EServerCall _ => default ()
adamc@1200 500 | ERecv _ => default ()
adamc@1200 501 | ESleep _ => default ()
adamc@1200 502 | ESpawn _ => default ()
adamc@1200 503 end
adamc@1200 504
adamc@1200 505 fun check file =
adamc@1200 506 let
adamc@1200 507 fun decl ((d, _), summaries) =
adamc@1200 508 case d of
adamc@1200 509 DVal (x, _, _, e, _) =>
adamc@1200 510 let
adamc@1200 511 fun deAbs (e, env, nv) =
adamc@1200 512 case #1 e of
adamc@1200 513 EAbs (_, _, _, e) => deAbs (e, Var nv :: env, nv + 1)
adamc@1200 514 | _ => (e, env, nv)
adamc@1200 515
adamc@1200 516 val (e, env, nv) = deAbs (e, [], 0)
adamc@1200 517
adamc@1200 518 val (e, (_, p, sent)) = evalExp env (e, (nv, True, []))
adamc@1200 519 in
adamc@1200 520 (x, e, p, sent) :: summaries
adamc@1200 521 end
adamc@1200 522 | _ => summaries
adamc@1200 523 in
adamc@1200 524 raise Summaries (foldl decl [] file)
adamc@1200 525 end
adamc@1200 526
adamc@1200 527 end