(* Randomized equivalence test *)

open Unix
open Ast

exception Test_failed

(* Check the determinism of CASEs and of the character *)

let rec determ_stmt = function
    Eif(cond, ifso, ifnot) -> determ_stmt ifso; determ_stmt ifnot
  | Edecision d -> ()
  | Ecase(v, arms, default) ->
      determ_arms arms; determ_stmt default

and determ_arms arms =
  let cases = ref [] in
  List.iter
    (fun (lbls, stmt) ->
      List.iter (fun n -> if List.mem n !cases then raise Test_failed;
                          cases := n :: !cases)
                lbls;
      determ_stmt stmt)
    arms

let determ_character = determ_arms

(* Evaluate a statement *)

let rec eval_cond env = function
    Cequals(v, n) -> List.assoc v env = n
  | Cand l -> List.for_all (eval_cond env) l
  | Cor l -> List.exists (eval_cond env) l

let rec eval_stmt env = function
    Eif(cond, ifso, ifnot) ->
      if eval_cond env cond then eval_stmt env ifso else eval_stmt env ifnot
  | Edecision d ->
      (begin match d.next with
          NSdefault -> List.assoc "state" env
        | NSfixed n -> n
        | NSchoose n -> n
       end,
       d.utterance)
  | Ecase(v, arms, default) ->
      eval_case env (List.assoc v env) default arms

and eval_case env n default = function
    [] -> eval_stmt env default
  | (csts, stmt) :: rem ->
      if List.mem n csts
      then eval_stmt env stmt
      else eval_case env n default rem

let eval_rule env rulelist =
  let state = List.assoc "state" env in
  let rec eval_rl = function
    [] -> raise Test_failed
  | (csts, stmt) :: rem ->
      if List.mem state csts
      then eval_stmt env stmt
      else eval_rl rem in
  eval_rl rulelist

(* Determine all values of interest of all variables *)

let possible_values = (Hashtbl.create 17 : (string, int list ref) Hashtbl.t)

let add_val_aux v n =
  try
    let r = Hashtbl.find possible_values v in
    if not (List.mem n !r) then r := n :: !r
  with Not_found ->
    Hashtbl.add possible_values v (ref [n])  

let add_val v n =
  if v <> "state" then add_val_aux v n

let rec collect_cond = function
    Cequals(v, n) -> add_val v n
  | Cand cl -> List.iter collect_cond cl
  | Cor cl -> List.iter collect_cond cl

let rec collect_stmt = function
    Eif(cond, ifso, ifnot) ->
      collect_cond cond; collect_stmt ifso; collect_stmt ifnot
  | Edecision d -> ()
  | Ecase(v, cases, default) ->
      collect_cases v cases; collect_stmt default

and collect_cases v = function
    [] -> ()
  | (ns, stmt) :: rem ->
      List.iter (add_val v) ns; collect_stmt stmt; collect_cases v rem

let rec collect_states = function
    [] -> ()
  | (ns, stmt) :: rem ->
      List.iter (add_val_aux "state") ns; collect_stmt stmt; collect_states rem

let collect_possible_values rulelist1 rulelist2 =
  Hashtbl.clear possible_values;
  collect_states rulelist1;
  let st1 = !(Hashtbl.find possible_values "state") in
  collect_states rulelist2;
  let st2 = !(Hashtbl.find possible_values "state") in
  if Sort.list (<=) st1 <> Sort.list (<=) st2 then raise Test_failed;
  let res = ref [] in
  let add_one_val v rl =
    let l = if v = "state" then !rl else max_int :: !rl in
    res := (v, Array.of_list l) :: !res in
  Hashtbl.iter add_one_val possible_values;
  !res

(* Randomly assign values to variables *)

let rec variable_assignment = function
    [] -> []
  | (v, values) :: rem ->
      (v, values.(Random.int (Array.length values))) :: variable_assignment rem

(* Evaluate two characters on a random input *)

let eval_random poss_val ch1 ch2 =
  let env = variable_assignment poss_val in
  let (n1,u1 as v1) = eval_rule env ch1
  and (n2,u2 as v2) = eval_rule env ch2 in
  if v1 <> v2 then begin
(***
    List.iter (fun (v, n) -> print_string v; print_string "="; print_int n; print_string " ") env; print_newline();
    print_int n1; print_string " "; print_string u1; print_newline();
    print_int n2; print_string " "; print_string u2; print_newline();
***)
    raise Test_failed
  end

(* Main test function *)

let test_duration = ref 30.0

exception Timeout

let test ch1 ch2 =
  ignore(Sys.set_signal Sys.sigvtalrm
                        (Sys.Signal_handle (fun _ -> raise Timeout)));
  try
    ignore(Unix.setitimer Unix.ITIMER_VIRTUAL
                          {it_interval = 0.0; it_value = !test_duration});
    determ_character ch2;
    let poss_val = collect_possible_values ch1 ch2 in
    while true do eval_random poss_val ch1 ch2 done;
    true
  with exn ->
    match exn with
      Test_failed -> false
    | Timeout -> true
    | _ -> raise exn