(* Simplifications on statements and characters *)

open Format
open Misc
open Ast
open Stmt

(* Conversions between characters and statements *)

let dummy_statement =
  Edecision {next=NSdefault; utterance=""}

let stmt_of_character c = Ecase("state", c, dummy_statement)

module IntSet = Set.Make(struct type t = int let compare = compare end)

let all_states c =
  let allstates = ref IntSet.empty in
  List.iter
    (fun (lbls, stmt) ->
      List.iter (fun lbl -> allstates := IntSet.add lbl !allstates) lbls)
    c;
  IntSet.elements !allstates

let character_of_stmt allstates s =
  [allstates, s]

(* Simplification of a character *)

let simpl_char c =
  let emptyenv = Env.empty() in
  let c' = 
    List.map
      (fun (states, stmt) ->
        (states,
         Stmt.simpl (Env.set_possible_values emptyenv "state" states) stmt))
      c in
(***
  print_string "*** First simplification:"; print_newline();
  pretty_character c'; print_newline();
***)
  let rec add_rule (lbls, stmt as lbls_stmt) = function
    [] -> [lbls_stmt]
  | (lbls', stmt' as lbls_stmt') :: rem ->
      if Stmt.same_stmt stmt' stmt
      then (lbls @ lbls', stmt) :: rem
      else lbls_stmt' :: add_rule lbls_stmt rem in
  let normal_character = List.fold_right add_rule (List.rev c') [] in
  Results.record_attempt normal_character;
(***
  print_string "*** Normal character:"; print_newline();
  pretty_character normal_character; print_newline();
***)
  (* Now try to simplify the character as a whole statement *)
  let stmt_character =
    character_of_stmt !Env.all_states
      (Stmt.simpl (Env.init()) (stmt_of_character normal_character)) in
  Results.record_attempt stmt_character
(***
  print_string "*** One-statement character:"; print_newline();
  pretty_character stmt_character; print_newline()
***)
(***
  print_string "*** Best character found so far:"; print_newline();
  pretty_character !best_character; print_newline()
***)

(* Find all variables occurring in a character *)

let rec find_cond_variables = function
    Cequals(v, n) ->
      if not (List.mem v !Env.all_variables)
      then Env.all_variables := v :: !Env.all_variables
  | Cor cl -> List.iter find_cond_variables cl
  | Cand cl -> List.iter find_cond_variables cl

let rec find_stmt_variables = function
    Eif(cond, ifso, ifnot) ->
      find_cond_variables cond;
      find_stmt_variables ifso; find_stmt_variables ifnot
  | Edecision d -> ()
  | Ecase(v, arms, default) ->
      if not (List.mem v !Env.all_variables)
      then Env.all_variables := v :: !Env.all_variables;
      find_arms_variables arms; find_stmt_variables default

and find_arms_variables arms =
  List.iter (fun (lbls, stmt) -> find_stmt_variables stmt) arms

let find_all_variables = find_arms_variables

(* Iterate simpl_char a few times, catching all exceptions and returning
   the best character found so far *)

let simpl_character c =
  Env.all_variables := ["state"]; find_all_variables c;
  Env.all_states := all_states c;
  try
    simpl_char c;
    let c1 = Results.get_best_character() in
    if c1 != c then begin
      simpl_char c1;
      let c2 = Results.get_best_character() in
      if c2 != c1 then begin
        simpl_char c2;
        let c3 = Results.get_best_character() in
          if c3 != c2 then simpl_char c3
      end
    end
  with Timeout -> raise Timeout | x -> ()