Mercurial > urweb

comparison src/iflow.sml @ 1230:8768145eed1e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Havoc relations that have been updated
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:17:52 -0400
parents a2cd6664f57f
children 5fa8ae2a34e3
comparison
equal deleted inserted replaced
1229:a2cd6664f57f 1230:8768145eed1e
1982 Delete = #Delete t, 1982 Delete = #Delete t,
1983 Update = c :: #Update t} 1983 Update = c :: #Update t}
1984 1984
1985 end 1985 end
1986 1986
1987 fun havocReln r =
1988 let
1989 fun hr p =
1990 case p of
1991 True => p
1992 | False => p
1993 | Unknown => p
1994 | And (p1, p2) => And (hr p1, hr p2)
1995 | Or (p1, p2) => Or (hr p1, hr p2)
1996 | Reln (r', _) => if r' = r then True else p
1997 | Cond (e, p) => Cond (e, hr p)
1998 in
1999 hr
2000 end
2001
1987 fun evalExp env (e as (_, loc), st) = 2002 fun evalExp env (e as (_, loc), st) =
1988 let 2003 let
1989 fun default () = 2004 fun default () =
1990 let 2005 let
1991 val (st, nv) = St.nextVar st 2006 val (st, nv) = St.nextVar st
2257 | (inr p, st) => (p, st) 2272 | (inr p, st) => (p, st)
2258 2273
2259 val p = And (p, 2274 val p = And (p,
2260 And (Reln (Sql "$Old", [Var old]), 2275 And (Reln (Sql "$Old", [Var old]),
2261 Reln (Sql tab, [Var old]))) 2276 Reln (Sql tab, [Var old])))
2277
2278 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
2262 in 2279 in
2263 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p)))) 2280 (Recd [], St.addDelete (st, (loc, And (St.ambient st, p))))
2264 end 2281 end
2265 | Update (tab, fs, e) => 2282 | Update (tab, fs, e) =>
2266 let 2283 let
2306 2323
2307 val p = And (p, 2324 val p = And (p,
2308 And (Reln (Sql (tab ^ "$New"), [Recd fs]), 2325 And (Reln (Sql (tab ^ "$New"), [Recd fs]),
2309 And (Reln (Sql "$Old", [Var old]), 2326 And (Reln (Sql "$Old", [Var old]),
2310 Reln (Sql tab, [Var old])))) 2327 Reln (Sql tab, [Var old]))))
2328
2329 val st = St.setAmbient (st, havocReln (Sql tab) (St.ambient st))
2311 in 2330 in
2312 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p)))) 2331 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
2313 end) 2332 end)
2314 2333
2315 | ENextval (EPrim (Prim.String seq), _) => 2334 | ENextval (EPrim (Prim.String seq), _) =>