module W = Words
module B = BalancedWords

let rec word_size w = match w with
  | W.Eps -> 1
  | W.Snoc(w',_) -> 1 + word_size w'

let rec size t = match t with
  | B.B2_e -> 1
  | B.B2_ab (u,v,pu,pv) | B.B2_ba (u,v,pu,pv) ->
      1 + word_size u + word_size v + size pu + size pv

(* Solution JCF *)
type sol = E | AB of sol * sol | BA of sol * sol

(* start cherche une solution pour un mot complet *)
let rec start = function
  | W.Eps -> E
  | W.Snoc(w, W.Coq_a) -> let u,w' = endsB w in AB (u, start w')
  | W.Snoc(w, W.Coq_b) -> let u,w' = endsA w in BA (u, start w')

(* endsA cherche une solution suivie d'un A, le consomme et retourne
   la solution et le reste du mot *)
and endsA = function
  | W.Eps -> assert false
  | W.Snoc(w, W.Coq_a) -> E, w
  | W.Snoc(w, W.Coq_b) ->
      let u,w' = endsA w in let v,w'' = endsA w' in BA (u,v), w''

(* endsA cherche une solution suivie d'un B, le consomme et retourne
   la solution et le reste du mot *)
and endsB = function
  | W.Eps -> assert false
  | W.Snoc(w, W.Coq_b) -> E, w
  | W.Snoc(w, W.Coq_a) ->
      let u,w' = endsB w in let v,w'' = endsB w' in AB (u,v), w''

(***********************************************************)

(* untyping f *)
let ign f x = ignore (f x)

(* Words.word -> unit *)
let i_ivt_b1 = ign Exo_inter.coq_B1_compl
let i_ivt_b2 = ign Exo_inter.coq_B2_compl
let i_ind_b1 = ign Exo_induc_fct.coq_B1_completeness
let i_ind_b2 = ign Exo_induc_fct.coq_B2_completeness
let i_start = ign start

type algo_name=  Ivt_b1 | Ivt_b2 | Ind_b1 | Ind_b2 | Start

let fn_of_algo_name = function
  | Ivt_b1 -> i_ivt_b1
  | Ivt_b2 -> i_ivt_b2
  | Ind_b1 -> i_ind_b1
  | Ind_b2 -> i_ind_b2
  | Start -> i_start

let string_of_algo_name = function
  | Ivt_b1 -> "ivt B1"
  | Ivt_b2 -> "ivt B2"
  | Ind_b1 -> "ind B1"
  | Ind_b2 -> "ind B2"
  | Start ->  "direct"

type balanced = W.coq_V array

let an_bn half_size =
  let a = Array.make (2 * half_size) W.Coq_b in
  for i = 0 to half_size-1 do a.(i) <- W.Coq_a done;
  a

let bn_an half_size =
  let a = Array.make (2 * half_size) W.Coq_a in
  for i = 0 to half_size-1 do a.(i) <- W.Coq_b done;
  a

let ab_n half_size =
  let a = Array.make (2 * half_size) W.Coq_b in
  for i = 0 to half_size-1 do a.(2*i) <- W.Coq_a done;
  a

let ba_n half_size =
  let a = Array.make (2 * half_size) W.Coq_b in
  for i = 0 to half_size-1 do a.(2*i + 1) <- W.Coq_a done;
  a

let word_of_array a =
  let w = ref W.Eps in
  for i = 0 to Array.length a - 1 do w := W.Snoc(!w,a.(i)) done;
  !w

(* int -> W.word *)
let w_an_bn n = word_of_array (an_bn n)
let w_bn_an n = word_of_array (bn_an n)
let w_ab_n n = word_of_array (ab_n n)
let w_ba_n n = word_of_array (ba_n n)

type mkword_name = Mk_an_bn | Mk_bn_an | Mk_ab_n | Mk_ba_n

let mkword_of_name = function
  | Mk_an_bn -> w_an_bn
  | Mk_bn_an -> w_bn_an
  | Mk_ab_n -> w_ab_n
  | Mk_ba_n -> w_ba_n

let string_of_mkword = function
  | Mk_an_bn -> "an bn"
  | Mk_bn_an -> "bn an"
  | Mk_ab_n -> "(ab)n"
  | Mk_ba_n -> "(ba)n"

(* *)

(* Random permutation applied to a word of the form a------ab------b *) 

(* int in [i, n[ *)
let () = Random.init 123456

let rand i n = i + Random.int (n-i)

let transpose i j permut =
  let tmp = permut.(i) in
  permut.(i) <- permut.(j);
  permut.(j) <- tmp


let random_permut half_size =
  let size = 2 * half_size in
  let p = an_bn half_size in
  assert (Array.length p = size);
  for i = 0 to size-1 do
    transpose i (rand i size) p
  done;
  p

let random_balanced_word half_size =
  word_of_array (random_permut half_size)

(* *)
(* If max_overhead >= 1000000, compaction is never triggered *)
let _ = Gc.set { (Gc.get()) with Gc.max_overhead = 1000000 }

let time_of f u =
  let t0 = Unix.gettimeofday() in
  let () = f u in
  let t1 = Unix.gettimeofday() in
  t1 -. t0

let consol_time_of n f u =
  let rec sigm n a = if n = 0 then a else sigm (n-1) (a +. time_of f u) in
  sigm n 0. /. float_of_int n

let nbr_echantillons = int_of_string (Sys.argv.(5))

let results1 = Array.make nbr_echantillons 0.0
let results2 = Array.make nbr_echantillons 0.0

let crete_lg = nbr_echantillons / 20
let reste_lg = nbr_echantillons - crete_lg
let crete = Array.make (crete_lg + 1) (-10.0)
let reste = Array.make reste_lg 0.0

let par_crete x =
  let minc = crete.(1) in
  if x < minc then x
  else 
    let rec loop i =
      let j = 2 * i in
      let k = j + 1 in
      if crete_lg < j then i
      else 
	let cj = crete.(j) in
	if crete_lg < k then 
	  if x <= cj then i
	  else begin crete.(i) <- crete.(j); j end
	else 
	  let ck = crete.(k) in
	  if x <= cj && x <= ck then i
	  else 
	    if cj <= ck then (crete.(i) <- crete.(j); loop j)
	    else (crete.(i) <- crete.(k); loop k)
    in crete.(loop 1) <- x;
    minc

let ecrete arr =
  for i = 1 to crete_lg do crete.(i) <- (-10.) done;
  for i = 0 to crete_lg - 1 do ignore (par_crete arr.(i)) done ;
  for i = crete_lg to nbr_echantillons - 1 do
    reste.(i - crete_lg) <- par_crete arr.(i)
  done

let mean arr =
  (Array.fold_left (+.) 0. arr) /. (float_of_int (Array.length arr))
let max_arr arr = Array.fold_left max 0. arr
let nothing arr = 0.

let soft_mean arr =
  if Array.length arr < 20 then mean arr
  else begin ecrete arr; mean reste end

(* ((W.word -> unit) * float array) list -> int -> unit *)
let list_stats lfr n =
  for i = 0 to nbr_echantillons - 1 do 
    let u = random_balanced_word n in
    let rec upd = function
      | [] -> ()
      | (f,results) :: lfr -> results.(i) <- time_of (fn_of_algo_name f) u; upd lfr
    in upd lfr
  done;
  List.map (fun (f,r) -> r) lfr

let means lfr n = List.map soft_mean (list_stats lfr n)

let list_determ mkw lf n =
  let u = mkword_of_name mkw n in
  List.map (fun f -> consol_time_of 10 (fn_of_algo_name f) u) lf

let comp_stat sf fr1 fr2 n =
  match list_stats [fr1; fr2] n with
    | [r1; r2] -> sf r2 /. sf r1
    | _ -> assert false

type stat_pair = algo_name * float array

type com =
  | Means of stat_pair list
  | Ratio of stat_pair * stat_pair
  | Det of mkword_name * algo_name list

type revlist = Nil | Snoc of revlist * string

let list_of_revlist =
  let rec aux l = function
    | Nil -> l
    | Snoc (rl, s) -> aux (s :: l) rl in
  aux []

let gplot_genfmt_of_com_list col_abc datfic cl = 
  let gplot_fmt_line col_ord title =
    Printf.sprintf "   \"%s\" using %d:%d title '%s' with linespoints"
      datfic col_abc col_ord title in
  let gplot_fmt_of_mean col_ord (f,_) =
    gplot_fmt_line col_ord (Printf.sprintf "%s, mean" (string_of_algo_name f)) in
  let gplot_fmt_of_ratio col_ord (f1,_) (f2,_) =
    gplot_fmt_line col_ord
      (Printf.sprintf "%s / %s" (string_of_algo_name f2) (string_of_algo_name f1)) in
  let gplot_fmt_of_det col_ord mkw f =
    gplot_fmt_line col_ord
      (Printf.sprintf "%s, %s" (string_of_algo_name f) (string_of_mkword mkw)) in
  let gplot_fmt_of_com cpl = function 
    | Means (lfr) ->
	List.fold_left (fun (n,l) fr ->
			  (n+2), Snoc (l, gplot_fmt_of_mean n fr)) cpl lfr
    | Ratio (fr1, fr2) ->
	(match cpl with (n,l) -> (n+2), Snoc (l, gplot_fmt_of_ratio n fr1 fr2))
    | Det (mkw, lf) -> 
	List.fold_left (fun (n,l) f ->
			  (n+2), Snoc (l, gplot_fmt_of_det n mkw f)) cpl lf
  in match List.fold_left (gplot_fmt_of_com) (col_abc + 2, Nil) cl with
      _,l -> list_of_revlist l

let gplot_fmt_of_com_list = gplot_genfmt_of_com_list 1 
let gplot_logfmt_of_com_list = gplot_genfmt_of_com_list 2 

let write_com_list cout gplot_list datfic cl =
  let lines = gplot_list datfic cl in
  let rec loop = function
    | [] -> Printf.fprintf cout  "\n"
    | s :: l -> Printf.fprintf cout  ", \\\n%s" s; loop l in
  Printf.fprintf cout  "set size nosquare 0.9, 0.9\nplot \\\n";
  match lines with
    | [] -> assert false
    | s :: lines -> Printf.fprintf cout  "%s" s; loop lines

let write_gplot_formats datfic cl =
  let rac = Filename.chop_extension datfic in
  let cout = open_out (rac ^ ".fmt") in
  write_com_list cout gplot_fmt_of_com_list datfic cl;
  close_out cout;
  let cout = open_out (rac ^ ".logfmt") in
  write_com_list cout gplot_logfmt_of_com_list datfic cl;
  close_out cout

let com_list_of = function
  | "ivt" ->
      [Means ([Ivt_b1, results1; Ivt_b2, results2])]
  | "ind" -> 
      [Means ([Ind_b2, results1; Ind_b1, results2])]
  | "direct" -> 
      [Means ([Start, results1])]
  | "ind1" -> 
      [Means ([Ind_b1, results1])]
  | "indvt1" -> 
      [Ratio ((Ind_b1, results1), (Ivt_b1, results2))]
  | "indvt2" -> 
      [Ratio ((Ind_b2, results1), (Ivt_b2, results2))]
  | "directind" -> 
      [Ratio ((Start, results1), (Ind_b2, results2))]
  | "indabm1" -> 
      [Det (Mk_an_bn, [Ind_b1]);
       Means ([Ind_b1, results1]);
       Det (Mk_ab_n, [Ind_b1])
      ]
  | "indabm2" -> 
      [Det (Mk_an_bn, [Ind_b2]);
       Means ([Ind_b2, results2]);
       Det (Mk_ab_n, [Ind_b2])
      ]
  | "ivtabm2" -> 
      [Det (Mk_an_bn, [Ivt_b2]);
       Means ([Ivt_b2, results2]);
       Det (Mk_ab_n, [Ivt_b2])
      ]
  | "directabm" -> 
      [Det (Mk_an_bn, [Start]);
       Means ([Start, results2]);
       Det (Mk_ab_n, [Start])
      ]
  | "ivtindanbn2" -> 
      [Means ([Ivt_b2, results2]);
       Det (Mk_an_bn, [Ind_b2])
      ]
  | _ -> assert false

let com_list = com_list_of Sys.argv.(1)
let datfic = Sys.argv.(6)

let bench_com n = function
  | Means (lfr) -> means lfr n
  | Ratio (fr1, fr2) -> [comp_stat soft_mean fr1 fr2 n]
  | Det (mkw, lf) -> list_determ mkw lf n 

let rec bench_lcom n = function
  | [] -> []
  | c :: lc -> bench_com n c @ bench_lcom n lc

let from_ = int_of_string (Sys.argv.(2))
let end_ = int_of_string (Sys.argv.(3))

let rate = int_of_string (Sys.argv.(4))

let coeff = 1. +. (float_of_int rate /. 100.)
let xfrom_ = float_of_int from_
let xend_ = float_of_int end_

let heat = ()
  (*ignore (list_stats com_list from_)*)

let print_abciss n =
  Printf.printf "%d %f " n (log10 (float_of_int n))

let print_data delta =
  Printf.printf "%F %f " delta (log10 delta)

let print_bench n ldelta =
  print_abciss n;
  List.iter print_data ldelta;
  Printf.printf "\n";
  flush stdout

let print_exponent ldx olh lf =
  Printf.eprintf "exponents = ";
  let lh = match olh with
    | None -> assert false
    | Some (lh) -> lh in
  let rec loop lh lf =
    match lh, lf with
      | [], [] -> ()
      | h :: lh, f :: lf -> Printf.eprintf "%f " ((log10 f -. log10 h) /. ldx); loop lh lf
      | _, _ -> assert false
  in loop lh lf;
  Printf.eprintf "\n";
  flush stderr
  
let main () =
   write_gplot_formats datfic com_list;
  let halfway = (log10 xfrom_ +. log10 xend_ ) /. 2. in
  let rec loop x halfway_x halfway_deltas =
    let n = int_of_float x in
    let lx = log10 x in
    let ldelta = bench_lcom n com_list in
    print_bench n ldelta;
    let halfway_x,  halfway_deltas = 
      if lx <= halfway then (lx, Some (ldelta)) else (halfway_x, halfway_deltas) in
    if x >= xend_ then print_exponent (lx -. halfway_x) halfway_deltas ldelta 
    else loop (x *. coeff) halfway_x halfway_deltas in
  loop xfrom_ (log10 xfrom_) None

let _ = main ()