Mercurial > urweb

comparison src/iflow.sml @ 1246:fd4028a594a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better handling of DELETE and UPDATE
author Adam Chlipala <adamc@hcoop.net>
date Sun, 18 Apr 2010 14:52:13 -0400
parents 5c2555dfce8f
children 0c643f51fbc0
comparison
equal deleted inserted replaced
1245:5c2555dfce8f 1246:fd4028a594a9
796 let 796 let
797 val d = repOf d 797 val d = repOf d
798 in 798 in
799 (uk andalso !(#Known (unNode d))) 799 (uk andalso !(#Known (unNode d)))
800 orelse List.exists (fn b => repOf b = d) bs 800 orelse List.exists (fn b => repOf b = d) bs
801 orelse case #Variety (unNode d) of 801 orelse (case #Variety (unNode d) of
802 Dt0 _ => true 802 Dt0 _ => true
803 | Dt1 (_, d) => loop d 803 | Dt1 (_, d) => loop d
804 | Prim _ => true 804 | Prim _ => true
805 | Recrd (xes, _) => List.all loop (SM.listItems (!xes)) 805 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
806 | Nothing => false 806 | Nothing => false)
807 end 807 end
808 808
809 fun decomp e = 809 fun decomp e =
810 case e of 810 case e of
811 Func (Other _, es) => List.all decomp es 811 Func (Other _, es) => List.all decomp es
1294 finder (hyps, a :: acc) 1294 finder (hyps, a :: acc)
1295 | a :: hyps => finder (hyps, a :: acc) 1295 | a :: hyps => finder (hyps, a :: acc)
1296 1296
1297 val hyps = finder (hyps, []) 1297 val hyps = finder (hyps, [])
1298 in 1298 in
1299 findKeys (hyps, acc) 1299 findKeys (hyps, a :: acc)
1300 end) 1300 end)
1301 | a :: hyps => findKeys (hyps, a :: acc) 1301 | a :: hyps => findKeys (hyps, a :: acc)
1302 1302
1303 fun loop hs = 1303 fun loop hs =
1304 let 1304 let
1311 () 1311 ()
1312 end 1312 end
1313 1313
1314 val (_, hs, _) = !hyps 1314 val (_, hs, _) = !hyps
1315 in 1315 in
1316 (*print "findKeys\n";*) 1316 (*print "useKeys\n";*)
1317 loop hs 1317 loop hs
1318 end 1318 end
1319 1319
1320 fun complete () = 1320 fun complete () =
1321 let 1321 let
1409 let 1409 let
1410 val (_, hs, _) = !hyps 1410 val (_, hs, _) = !hyps
1411 in 1411 in
1412 ErrorMsg.errorAt loc "The information flow policy may be violated here."; 1412 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
1413 Print.prefaces "Situation" [("User learns", p_exp e), 1413 Print.prefaces "Situation" [("User learns", p_exp e),
1414 ("Hypotheses", Print.p_list p_atom hs)(*, 1414 ("Hypotheses", Print.p_list p_atom hs),
1415 ("E-graph", Cc.p_database db)*)] 1415 ("E-graph", Cc.p_database db)]
1416 end 1416 end
1417 end 1417 end
1418 1418
1419 fun checkPaths () = 1419 fun checkPaths () =
1420 let 1420 let
1421 val (n, hs, _) = !hyps 1421 val (n, hs, _) = !hyps
1422 val hs = (n, hs) 1422 val hs = (n, hs)
1452 if checkGoals goals (fn _ => true) then 1452 if checkGoals goals (fn _ => true) then
1453 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals), 1453 ((*Print.prefaces "Match" [("goals", Print.p_list p_atom goals),
1454 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*) 1454 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*)
1455 true) 1455 true)
1456 else 1456 else
1457 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals), 1457 ((*Print.prefaces "No match" [("goals", Print.p_list p_atom goals)(*,
1458 ("hyps", Print.p_list p_atom (#2 (!hyps)))];*) 1458 ("hyps", Print.p_list p_atom (#2 (!hyps)))*)];*)
1459 false)) pols then 1459 false)) pols then
1460 () 1460 ()
1461 else 1461 else
1462 let 1462 let
1463 val (_, hs, _) = !hyps 1463 val (_, hs, _) = !hyps
2003 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean" 2003 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
2004 | inr p => p 2004 | inr p => p
2005 2005
2006 val saved = St.stash () 2006 val saved = St.stash ()
2007 in 2007 in
2008 St.assert [AReln (Sql (tab ^ "$Old"), [Var old])]; 2008 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
2009 AReln (Sql (tab), [Var old])];
2009 decomp {Save = St.stash, 2010 decomp {Save = St.stash,
2010 Restore = St.reinstate, 2011 Restore = St.reinstate,
2011 Add = fn a => St.assert [a]} p 2012 Add = fn a => St.assert [a]} p
2012 (fn () => (St.delete loc; 2013 (fn () => (St.delete loc;
2013 St.reinstate saved; 2014 St.reinstate saved;
2047 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean" 2048 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
2048 | inr p => p 2049 | inr p => p
2049 val saved = St.stash () 2050 val saved = St.stash ()
2050 in 2051 in
2051 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]), 2052 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
2052 AReln (Sql (tab ^ "$Old"), [Var old])]; 2053 AReln (Sql (tab ^ "$Old"), [Var old]),
2054 AReln (Sql tab, [Var old])];
2053 decomp {Save = St.stash, 2055 decomp {Save = St.stash,
2054 Restore = St.reinstate, 2056 Restore = St.reinstate,
2055 Add = fn a => St.assert [a]} p 2057 Add = fn a => St.assert [a]} p
2056 (fn () => (St.update loc; 2058 (fn () => (St.update loc;
2057 St.reinstate saved; 2059 St.reinstate saved;