(* =========================================================== *)
(* Miscellaneous functions                                     *)
(* Author: Alexey Solovyev                                     *)
(* Date: 2012-10-27                                            *)
(* =========================================================== *)

module Arith_misc = struct

(* A little faster version of PROVE_HYP *)
let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;

(* A faster version of BETA_RULE *)
let MY_BETA_RULE th =
  let rec beta tm =
    let op, arg = dest_comb tm in
      if is_comb op then
        let op_th = AP_THM (beta op) arg in
        let beta_th = BETA_CONV (rand (concl op_th)) in
          TRANS op_th beta_th
      else
        BETA_CONV tm in
    EQ_MP (beta (concl th)) th;;


(* Applies f to arg n times and returns the total execution time *)
let test n f arg =
  let start = Sys.time() in
    for i = 1 to n do
      let _ = f arg in ()
    done;
  Sys.time() -. start;;

(* Generates a power function for the given binary operation *)
let gen_pow op id n x =
  let ( * ) = op in
  let rec pow n =
    if n <= 0 then id
    else if n = 1 then x
    else if n land 1 = 1 then
      x * pow (n - 1)
    else
      let t = pow (n lsr 1) in
        t * t in
    pow n;;

let rec shape_list n list =
  if length list <= n then [list]
  else
    let l1, l2 = chop_list n list in
      l1 :: shape_list n l2;;

(* map2 which works for lists of any size (no requirement |l1| = |l2|) *)
let rec my_map2 f l1 l2 =
  match l1 with
    | [] -> []
    | (h1::t1) ->
        (match l2 with
           | [] -> []
           | (h2::t2) -> (f h1 h2) :: my_map2 f t1 t2);;

end;;