Mercurial > urweb

comparison src/iflow.sml @ 1232:efbefd6e3f6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
When applying multiple policies at once, filter the policy set at the beginning, removing unmatchable policies
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 09:31:04 -0400
parents 5fa8ae2a34e3
children 8d1d2f7163c2
comparison
equal deleted inserted replaced
1231:5fa8ae2a34e3 1232:efbefd6e3f6c
2501 if decompH p 2501 if decompH p
2502 (fn hyps => 2502 (fn hyps =>
2503 let 2503 let
2504 val cc = ccOf hyps 2504 val cc = ccOf hyps
2505 2505
2506 val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab) 2506 fun relevant () =
2507 | (_, avail) => avail) SS.empty hyps 2507 let
2508 val avail = foldl (fn (AReln (Sql tab, _), avail) =>
2509 SS.add (avail, tab)
2510 | (_, avail) => avail) SS.empty hyps
2511 in
2512 List.filter
2513 (fn (g1, _) =>
2514 decompG g1
2515 (List.all (fn AReln (Sql tab, _) =>
2516 SS.member (avail, tab)
2517 | _ => true))) client
2518 end
2508 2519
2509 fun tryCombos (maxLv, pols, g, outs) = 2520 fun tryCombos (maxLv, pols, g, outs) =
2510 case pols of 2521 case pols of
2511 [] => 2522 [] =>
2512 decompG g 2523 decompG g
2515 let 2526 let
2516 val g1 = bumpLvarsP (maxLv + 1) g1 2527 val g1 = bumpLvarsP (maxLv + 1) g1
2517 val outs1 = map (bumpLvars (maxLv + 1)) outs1 2528 val outs1 = map (bumpLvars (maxLv + 1)) outs1
2518 fun skip () = tryCombos (maxLv, pols, g, outs) 2529 fun skip () = tryCombos (maxLv, pols, g, outs)
2519 in 2530 in
2520 if decompG g1 2531 skip ()
2521 (List.all (fn AReln (Sql tab, _) => 2532 orelse tryCombos (Int.max (maxLv,
2522 SS.member (avail, tab) 2533 maxLvarP g1),
2523 | _ => true)) then 2534 pols,
2524 skip () 2535 And (g1, g),
2525 orelse tryCombos (Int.max (maxLv, 2536 outs1 @ outs)
2526 maxLvarP g1),
2527 pols,
2528 And (g1, g),
2529 outs1 @ outs)
2530 else
2531 skip ()
2532 end 2537 end
2533 in 2538 in
2534 (fl <> Control Where 2539 (fl <> Control Where
2535 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0])) 2540 andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0]))
2536 orelse List.exists (fn (p', outs) => 2541 orelse List.exists (fn (p', outs) =>
2537 decompG p' 2542 decompG p'
2538 (fn goals => imply (cc, hyps, goals, 2543 (fn goals => imply (cc, hyps, goals,
2539 SOME outs))) 2544 SOME outs)))
2540 client 2545 client
2541 orelse tryCombos (0, client, True, []) 2546 orelse tryCombos (0, relevant (), True, [])
2542 orelse (reset (); 2547 orelse (reset ();
2543 Print.preface ("Untenable hypotheses" 2548 Print.preface ("Untenable hypotheses"
2544 ^ (case fl of 2549 ^ (case fl of
2545 Control Where => " (WHERE clause)" 2550 Control Where => " (WHERE clause)"
2546 | Control Case => " (case discriminee)" 2551 | Control Case => " (case discriminee)"