Mercurial > urweb
changeset 1231:5fa8ae2a34e3
Avoid pointless rebuilding of hypothesis E-graphs
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 13 Apr 2010 09:25:45 -0400 |
| parents | 8768145eed1e |
| children | efbefd6e3f6c |
| files | src/iflow.sml |
| diffstat | 1 files changed, 98 insertions(+), 90 deletions(-) [+] |
line wrap: on
line diff
--- a/src/iflow.sml Tue Apr 13 09:17:52 2010 -0400 +++ b/src/iflow.sml Tue Apr 13 09:25:45 2010 -0400 @@ -959,84 +959,86 @@ val tabs = ref (SM.empty : (string list * string list list) SM.map) -fun imply (hyps, goals, outs) = +fun ccOf hyps = + let + val cc = Cc.database () + val () = app (fn a => Cc.assert (cc, a)) hyps + + (* Take advantage of table key information *) + fun findKeys hyps = + case hyps of + [] => () + | AReln (Sql tab, [r1]) :: hyps => + (case SM.find (!tabs, tab) of + NONE => findKeys hyps + | SOME (_, []) => findKeys hyps + | SOME (_, ks) => + let + fun finder hyps = + case hyps of + [] => () + | AReln (Sql tab', [r2]) :: hyps => + (if tab' = tab andalso + List.exists (List.all (fn f => + let + val r = + Cc.check (cc, + AReln (Eq, [Proj (r1, f), + Proj (r2, f)])) + in + (*Print.prefaces "Fs" + [("tab", + Print.PD.string tab), + ("r1", + p_exp (Proj (r1, f))), + ("r2", + p_exp (Proj (r2, f))), + ("r", + Print.PD.string + (Bool.toString r))];*) + r + end)) ks then + ((*Print.prefaces "Key match" [("tab", Print.PD.string tab), + ("r1", p_exp r1), + ("r2", p_exp r2), + ("rp1", Cc.p_repOf cc r1), + ("rp2", Cc.p_repOf cc r2)];*) + Cc.assert (cc, AReln (Eq, [r1, r2]))) + else + (); + finder hyps) + | _ :: hyps => finder hyps + in + finder hyps; + findKeys hyps + end) + | _ :: hyps => findKeys hyps + in + findKeys hyps; + cc + end + +fun imply (cc, hyps, goals, outs) = let fun gls goals onFail acc = case goals of [] => - (let - val cc = Cc.database () - val () = app (fn a => Cc.assert (cc, a)) hyps - - (* Take advantage of table key information *) - fun findKeys hyps = - case hyps of - [] => () - | AReln (Sql tab, [r1]) :: hyps => - (case SM.find (!tabs, tab) of - NONE => findKeys hyps - | SOME (_, []) => findKeys hyps - | SOME (_, ks) => - let - fun finder hyps = - case hyps of - [] => () - | AReln (Sql tab', [r2]) :: hyps => - (if tab' = tab andalso - List.exists (List.all (fn f => - let - val r = - Cc.check (cc, - AReln (Eq, [Proj (r1, f), - Proj (r2, f)])) - in - (*Print.prefaces "Fs" - [("tab", - Print.PD.string tab), - ("r1", - p_exp (Proj (r1, f))), - ("r2", - p_exp (Proj (r2, f))), - ("r", - Print.PD.string - (Bool.toString r))];*) - r - end)) ks then - ((*Print.prefaces "Key match" [("tab", Print.PD.string tab), - ("r1", p_exp r1), - ("r2", p_exp r2), - ("rp1", Cc.p_repOf cc r1), - ("rp2", Cc.p_repOf cc r2)];*) - Cc.assert (cc, AReln (Eq, [r1, r2]))) - else - (); - finder hyps) - | _ :: hyps => finder hyps - in - finder hyps; - findKeys hyps - end) - | _ :: hyps => findKeys hyps - in - findKeys hyps; - - (*Print.preface ("db", Cc.p_database cc);*) - (List.all (fn a => - if Cc.check (cc, a) then - true - else - ((*Print.prefaces "Can't prove" - [("a", p_atom a), - ("hyps", Print.p_list p_atom hyps), - ("db", Cc.p_database cc)];*) - false)) acc - andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true) - andalso (case outs of - NONE => true - | SOME outs => Cc.builtFrom (cc, {Derived = Var 0, - Base = outs}))) - handle Cc.Contradiction => false - end handle Cc.Undetermined => false) + ((List.all (fn a => + if Cc.check (cc, a) then + true + else + ((*Print.prefaces "Can't prove" + [("a", p_atom a), + ("hyps", Print.p_list p_atom hyps), + ("db", Cc.p_database cc)];*) + false)) acc + andalso ((*Print.preface ("Finding", Cc.p_database cc);*) true) + andalso (case outs of + NONE => true + | SOME outs => Cc.builtFrom (cc, {Derived = Var 0, + Base = outs}))) + handle Cc.Contradiction => false + | Cc.Undetermined => false) orelse onFail () | (g as AReln (Sql gf, [ge])) :: goals => let @@ -1073,7 +1075,7 @@ (*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps), ("goals", Print.p_list p_atom goals)];*) gls goals (fn () => false) [] - end handle Cc.Contradiction => true + end fun patCon pc = case pc of @@ -2471,16 +2473,20 @@ app (fn (loc, p) => if decompH p (fn hyps => - List.exists (fn p' => - if decompG p' - (fn goals => imply (hyps, goals, NONE)) then - ((*reset (); - Print.prefaces "Match" [("hyp", p_prop p), - ("goal", p_prop p')];*) - true) - else - false) - pols) then + let + val cc = ccOf hyps + in + List.exists (fn p' => + if decompG p' + (fn goals => imply (cc, hyps, goals, NONE)) then + ((*reset (); + Print.prefaces "Match" [("hyp", p_prop p), + ("goal", p_prop p')];*) + true) + else + false) + pols + end handle Cc.Contradiction => true) then () else (ErrorMsg.errorAt loc "The information flow policy may be violated here."; @@ -2495,6 +2501,8 @@ if decompH p (fn hyps => let + val cc = ccOf hyps + val avail = foldl (fn (AReln (Sql tab, _), avail) => SS.add (avail, tab) | (_, avail) => avail) SS.empty hyps @@ -2502,7 +2510,7 @@ case pols of [] => decompG g - (fn goals => imply (hyps, goals, SOME outs)) + (fn goals => imply (cc, hyps, goals, SOME outs)) | (g1, outs1) :: pols => let val g1 = bumpLvarsP (maxLv + 1) g1 @@ -2524,10 +2532,11 @@ end in (fl <> Control Where - andalso imply (hyps, [AReln (Known, [Var 0])], SOME [Var 0])) + andalso imply (cc, hyps, [AReln (Known, [Var 0])], SOME [Var 0])) orelse List.exists (fn (p', outs) => decompG p' - (fn goals => imply (hyps, goals, SOME outs))) + (fn goals => imply (cc, hyps, goals, + SOME outs))) client orelse tryCombos (0, client, True, []) orelse (reset (); @@ -2538,7 +2547,7 @@ | Data => " (returned data value)"), Print.p_list p_atom hyps); false) - end) then + end handle Cc.Contradiction => true) then () else ErrorMsg.errorAt loc "The information flow policy may be violated here." @@ -2577,4 +2586,3 @@ end end -