Mercurial > urweb
changeset 1232:efbefd6e3f6c
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 |
| files | src/iflow.sml |
| diffstat | 1 files changed, 20 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/iflow.sml Tue Apr 13 09:25:45 2010 -0400 +++ b/src/iflow.sml Tue Apr 13 09:31:04 2010 -0400 @@ -2503,8 +2503,19 @@ let val cc = ccOf hyps - val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab) - | (_, avail) => avail) SS.empty hyps + fun relevant () = + let + val avail = foldl (fn (AReln (Sql tab, _), avail) => + SS.add (avail, tab) + | (_, avail) => avail) SS.empty hyps + in + List.filter + (fn (g1, _) => + decompG g1 + (List.all (fn AReln (Sql tab, _) => + SS.member (avail, tab) + | _ => true))) client + end fun tryCombos (maxLv, pols, g, outs) = case pols of @@ -2517,18 +2528,12 @@ val outs1 = map (bumpLvars (maxLv + 1)) outs1 fun skip () = tryCombos (maxLv, pols, g, outs) in - if decompG g1 - (List.all (fn AReln (Sql tab, _) => - SS.member (avail, tab) - | _ => true)) then - skip () - orelse tryCombos (Int.max (maxLv, - maxLvarP g1), - pols, - And (g1, g), - outs1 @ outs) - else - skip () + skip () + orelse tryCombos (Int.max (maxLv, + maxLvarP g1), + pols, + And (g1, g), + outs1 @ outs) end in (fl <> Control Where @@ -2538,7 +2543,7 @@ (fn goals => imply (cc, hyps, goals, SOME outs))) client - orelse tryCombos (0, client, True, []) + orelse tryCombos (0, relevant (), True, []) orelse (reset (); Print.preface ("Untenable hypotheses" ^ (case fl of