(* Simplifications on conditions *)
open Ast
(* Simplifications of conditions *)
let sctrue = Cand []
let scfalse = Cor []
let mkor = function [c] -> c | cl -> Cor cl
let mkand = function [c] -> c | cl -> Cand cl
(* Logical implication and equivalence *)
let rec implies c1 c2 =
match (c1, c2) with
(Cequals(v1, n1), Cequals(v2, n2)) -> v1 = v2 && n1 = n2
| (_, Cor cl) -> List.exists (fun c -> implies c1 c) cl
| (Cor cl, _) -> List.for_all (fun c -> implies c c2) cl
| (_, Cand cl) -> List.for_all (fun c -> implies c1 c) cl
| (Cand cl, _) -> List.exists (fun c -> implies c c2) cl
let equiv c1 c2 = implies c1 c2 && implies c2 c1
(* Logical contradiction *)
let rec contradicts c1 c2 =
match (c1, c2) with
(Cequals(v1, n1), Cequals(v2, n2)) -> v1 = v2 && n1 <> n2
| (_, Cand cl) -> List.exists (fun c -> contradicts c1 c) cl
| (Cand cl, _) -> List.exists (fun c -> contradicts c c2) cl
| (_, Cor cl) -> List.for_all (fun c -> contradicts c1 c) cl
| (Cor cl, _) -> List.for_all (fun c -> contradicts c c2) cl
(* In an "and" list, remove all elements that are implied by other elements *)
let rec remove_implied_and = function
[] -> []
| c1 :: rem ->
let rem' = remove_implied_and rem in
if List.exists (fun c2 -> implies c2 c1) rem'
then rem'
else c1 :: List.filter (fun c2 -> not(implies c1 c2)) rem'
(* In an "or" list, remove all elements that imply other elements *)
let rec remove_implied_or = function
[] -> []
| c1 :: rem ->
let rem' = remove_implied_or rem in
if List.exists (fun c2 -> implies c1 c2) rem'
then rem'
else c1 :: List.filter (fun c2 -> not(implies c2 c1)) rem'
(* In an "and" list, detect contradictions *)
let rec contradiction_and = function
[] -> false
| c1 :: rem ->
List.exists (fun c -> contradicts c1 c) rem || contradiction_and rem
let check_contradiction = function
Cand cl when contradiction_and cl -> scfalse
| c -> c
(* In an "or" list, detect disjunctions (EQUALS v n1) | ... | (EQUALS v nk)
that are trivially true given the infos we have on n in the environment *)
let trivial_or_aux env v cl =
let cases = ref [] in
List.iter (function (Cequals(v', n)) when v = v' -> cases := n :: !cases
| _ -> ())
cl;
Env.matches_arm env v !cases
let trivial_or env = function
Cor cl ->
begin try
List.iter
(function Cequals(v, _) -> if trivial_or_aux env v cl then raise Exit
| _ -> ())
cl;
Cor cl
with Exit -> sctrue
end
| c -> c
(* In an "or" list consisting entirely of "and"s, try to factor common
clauses:
(A & B) | (A & C) | ... = A & (B | C | ...) *)
let rec intersect c1 c2 =
match c1 with
[] -> []
| c :: cl ->
if List.exists (equiv c) c2
then c :: intersect cl c2
else intersect cl c2
let rec subtract c1 c2 =
match c1 with
[] -> []
| c :: cl ->
if List.exists (equiv c) c2
then subtract cl c2
else c :: subtract cl c2
let factor_or = function
(Cand cl1) :: (_ :: _ as crem) as cl ->
begin try
let common = ref cl1 in
List.iter
(function Cand l -> common := intersect l !common
| _ -> raise Exit)
crem;
if !common = [] then raise Exit;
let newcl =
List.map (function Cand l -> mkand (subtract l !common)
| _ -> raise Exit)
cl in
mkand (mkor newcl :: !common)
with Exit ->
mkor cl
end
| cl -> mkor cl
(* In an "and" list consisting entirely of "or"s, try to factor common
clauses:
(A | B) & (A | C) & ... = A | (B & C & ...) *)
let factor_and = function
(Cor cl1) :: (_ :: _ as crem) as cl ->
begin try
let common = ref cl1 in
List.iter
(function Cor l -> common := intersect l !common
| _ -> raise Exit)
crem;
if !common = [] then raise Exit;
let newcl =
List.map (function Cor l -> mkor(subtract l !common)
| _ -> raise Exit)
cl in
mkor (mkand newcl :: !common)
with Exit ->
mkand cl
end
| cl -> mkand cl
(* Flatten ands within ands / ors within ors *)
let rec flatten_ands = function
[] -> []
| Cand cl' :: cl -> cl' @ flatten_ands cl
| c :: cl -> c :: flatten_ands cl
let rec flatten_ors = function
[] -> []
| Cor cl' :: cl -> cl' @ flatten_ors cl
| c :: cl -> c :: flatten_ors cl
(* One round of simplification *)
let rec simpl_cond env = function
Cequals(v, n) as c ->
begin match Env.equals env v n with
Env.Yes -> sctrue
| Env.No -> scfalse
| Env.Maybe -> c
end
| Cand cl ->
trivial_or env (check_contradiction(factor_and(remove_implied_and(flatten_ands(List.map (simpl_cond env) cl)))))
| Cor cl ->
trivial_or env (check_contradiction(factor_or(remove_implied_or(flatten_ors (List.map (simpl_cond env) cl)))))
(* Simplification of conditions may cause impossible "and"s to appear,
so iterate simpl_cond a few times *)
let simpl env c =
let c1 = simpl_cond env c in
if c1 = c then c else
let c2 = simpl_cond env c1 in
if c2 = c1 then c1 else
simpl_cond env c2