comparison src/iflow.sml @ 1293:acabf3935060

tryDml
author Adam Chlipala <adam@chlipala.net>
date Sun, 05 Sep 2010 14:00:57 -0400
parents a9a500d22ebc
children 02fc16faecf3
comparison
equal deleted inserted replaced
1292:a671c986f517 1293:acabf3935060
2038 val acc = Var (St.nextVar ()) 2038 val acc = Var (St.nextVar ())
2039 2039
2040 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st, 2040 val (ts, cs) = MonoUtil.Exp.fold {typ = fn (_, st) => st,
2041 exp = fn (e, st as (cs, ts)) => 2041 exp = fn (e, st as (cs, ts)) =>
2042 case e of 2042 case e of
2043 EDml e => 2043 EDml (e, _) =>
2044 (case parse dml e of 2044 (case parse dml e of
2045 NONE => st 2045 NONE => st
2046 | SOME c => 2046 | SOME c =>
2047 case c of 2047 case c of
2048 Insert _ => st 2048 Insert _ => st
2078 Restore = St.reinstate, 2078 Restore = St.reinstate,
2079 Cont = AllCols (fn x => 2079 Cont = AllCols (fn x =>
2080 (St.assert [AReln (Eq, [r, x])]; 2080 (St.assert [AReln (Eq, [r, x])];
2081 evalExp (acc :: r :: env) b k))} q 2081 evalExp (acc :: r :: env) b k))} q
2082 end) 2082 end)
2083 | EDml e => 2083 | EDml (e, _) =>
2084 (case parse dml e of 2084 (case parse dml e of
2085 NONE => (print ("Warning: Information flow checker can't parse DML command at " 2085 NONE => (print ("Warning: Information flow checker can't parse DML command at "
2086 ^ ErrorMsg.spanToString loc ^ "\n"); 2086 ^ ErrorMsg.spanToString loc ^ "\n");
2087 default ()) 2087 default ())
2088 | SOME d => 2088 | SOME d =>
2398 | EQuery {exps, tables, state, query, body, initial} => 2398 | EQuery {exps, tables, state, query, body, initial} =>
2399 (EQuery {exps = exps, tables = tables, state = state, 2399 (EQuery {exps = exps, tables = tables, state = state,
2400 query = doExp env query, 2400 query = doExp env query,
2401 body = doExp (Unknown :: Unknown :: env) body, 2401 body = doExp (Unknown :: Unknown :: env) body,
2402 initial = doExp env initial}, loc) 2402 initial = doExp env initial}, loc)
2403 | EDml e1 => 2403 | EDml (e1, mode) =>
2404 (case parse dml e1 of 2404 (case parse dml e1 of
2405 NONE => () 2405 NONE => ()
2406 | SOME c => 2406 | SOME c =>
2407 case c of 2407 case c of
2408 Insert _ => () 2408 Insert _ => ()
2409 | Delete (tab, _) => 2409 | Delete (tab, _) =>
2410 tables := SS.add (!tables, tab) 2410 tables := SS.add (!tables, tab)
2411 | Update (tab, _, _) => 2411 | Update (tab, _, _) =>
2412 tables := SS.add (!tables, tab); 2412 tables := SS.add (!tables, tab);
2413 (EDml (doExp env e1), loc)) 2413 (EDml (doExp env e1, mode), loc))
2414 | ENextval e1 => (ENextval (doExp env e1), loc) 2414 | ENextval e1 => (ENextval (doExp env e1), loc)
2415 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc) 2415 | ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
2416 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc) 2416 | EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
2417 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc) 2417 | EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
2418 | ESignalReturn _ => e 2418 | ESignalReturn _ => e