(* 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