open Misc;;
open Syntax;;
open Econd;;

type clause = econd * new_state * string;;
(* an extended condition and the corresponding decision *)

let rec affirm = function
  | And l -> Eand (list_rmap affirm l)
  | Or l -> Eor (list_rmap affirm l)
  | Equals (v, i) -> Ein (v, Iset.Pos [i])
;;

let rec negate = function
  | And l -> Eor (list_rmap negate l)
  | Or l -> Eand (list_rmap negate l)
  | Equals (v, i) -> Ein (v, Iset.Neg [i])
;;

let add_cond c = function
  | (Eand cl,x,y) -> (Eand (c::cl),x,y)
  | (cc,x,y) -> (Eand [c;cc],x,y)
;;

let rec get_clauses_stm = function
  | If (cond, stm1, [], stm2)
     -> let cs1 = get_clauses_stm stm1 in
        let cond1 = affirm cond in
        let l1 = list_rmap (add_cond cond1) cs1 in
        let cs2 = get_clauses_stm stm2 in
        let cond2 = negate cond in
        let l2 = list_rmap (add_cond cond2) cs2 in
        l1 @@ l2

  | If (cond, stm1, (Elseif (cc, ss))::eis, stm2)
     -> get_clauses_stm (If (cond, stm1, [], (If (cc, ss, eis, stm2))))

  | Decision (st, msg) -> [ (Eand [], st, msg) ]

  | Case (v, arms, default)
     -> let cases = ref [] in
        let f =
          function Arm (is, stm) ->
            let cs = get_clauses_stm stm in
            let cond = Ein (v, Iset.Pos is) in
            cases := is @@ !cases;
            list_rmap (add_cond cond) cs
        in
        let resl1 = list_rmap f arms in    (* side effect on [cases] *)
        let dcond = Ein (v, Iset.Neg !cases) in
        let cs2 = get_clauses_stm default in
        let res2 = list_rmap (add_cond dcond) cs2 in
        List.concat (res2::resl1)
;;

let get_clauses_rule (Rule (ss, stm)) =
  let cs = get_clauses_stm stm in
  list_rmap (add_cond (Ein ("state", Iset.Pos ss))) cs
;;

let get_clauses chr =
  let css = list_rmap get_clauses_rule chr in
  List.concat css
;;

let underise c =
  match c with
  | (cond, None, msg) -> c
  | (cond, Some st, msg)
     -> if possible_values "state" cond = Iset.Pos [st]
        then (cond, None, msg)
        else c
;;

let add_clause c = function
  | (Eor cl,x,y) -> (Eor (c::cl),x,y)
  | (cc,x,y) -> (Eor [c;cc],x,y)
;;

let regroup cs =
  let compare (cond1,st1,msg1) (cond2,st2,msg2) = (st1,msg1) < (st2,msg2) in
  let cs = Sort.list compare cs in
  let rec loop accu ((cond,st,msg) as cur) = function
    | [] -> cur::accu
    | ((cond3,st3,msg3) as c3) :: cs3
       -> if (st3, msg3) = (st, msg)
          then loop accu (add_clause cond3 cur) cs3
          else loop (cur::accu) c3 cs3
  in
  match cs with
  | [] -> []
  | h::t -> loop [] h t
;;

let matches n stm = function
  | (cond2, Some n2, stm2) -> n = n2 && stm = stm2
  | _ -> false
;;

let covered ((cond,st,stm) as s) cs =
  match possible_values "state" cond with
  | Iset.Pos states
      -> List.for_all (fun n -> List.exists (matches n stm) cs) states
  | _ -> false
;;

let explode ((cond,st,stm) as x) =
  match possible_values "state" cond with
  | Iset.Pos states
     -> let f n = (Eand [Ein ("state", Iset.Pos [n]); cond], Some n, stm) in
        list_rmap f states
  | _ -> [x]
;;

let deunderise cs =
  let rec loop accu = function
    | [] -> accu
    | c::cs1
       -> if covered c cs then loop ((explode c) @@ accu) cs1
          else loop (c :: accu) cs1
  in
  loop [] cs
;;

let minimize l = list_rmap (fun (a,b,c) -> (minimize_econd a, b, c)) l;;

let remove_useless l = List.filter (fun (a,b,c) -> a <> Efalse) l;;

let decompose c =
  remove_useless
    (minimize
      (regroup
        (deunderise
          (minimize
            (regroup (list_rmap underise (minimize (get_clauses c))))))))
;;