formal_ineqs/misc/misc.hl

   1 (* =========================================================== *)\r
   2 (* Miscellaneous functions                                     *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 #load "unix.cma";;\r
   8 \r
   9 module Arith_misc = struct\r
  10 \r
  11 (* A little faster version of PROVE_HYP *)\r
  12 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;\r
  13 \r
  14 (* A faster version of BETA_RULE *)\r
  15 let MY_BETA_RULE th =\r
  16   let rec beta tm =\r
  17     let op, arg = dest_comb tm in\r
  18       if is_comb op then\r
  19         let op_th = AP_THM (beta op) arg in\r
  20         let beta_th = BETA_CONV (rand (concl op_th)) in\r
  21           TRANS op_th beta_th\r
  22       else\r
  23         BETA_CONV tm in\r
  24     EQ_MP (beta (concl th)) th;;\r
  25 \r
  26 \r
  27 (* Applies f to arg n times and returns the total execution time *)\r
  28 let test n f arg =\r
  29   let start = Unix.gettimeofday() in\r
  30     for i = 1 to n do\r
  31       let _ = f arg in ()\r
  32     done;\r
  33   Unix.gettimeofday() -. start;;\r
  34 \r
  35 (* Generates a power function for the given binary operation *)\r
  36 let gen_pow op id n x =\r
  37   let ( * ) = op in\r
  38   let rec pow n =\r
  39     if n <= 0 then id\r
  40     else if n = 1 then x\r
  41     else if n land 1 = 1 then\r
  42       x * pow (n - 1)\r
  43     else\r
  44       let t = pow (n lsr 1) in\r
  45         t * t in\r
  46     pow n;;\r
  47 \r
  48 let rec shape_list n list =\r
  49   if length list <= n then [list]\r
  50   else\r
  51     let l1, l2 = chop_list n list in\r
  52       l1 :: shape_list n l2;;\r
  53           \r
  54 (* map2 which works for lists of any size (no requirement |l1| = |l2|) *)\r
  55 let rec my_map2 f l1 l2 =\r
  56   match l1 with\r
  57     | [] -> []\r
  58     | (h1::t1) ->\r
  59         (match l2 with\r
  60            | [] -> []\r
  61            | (h2::t2) -> (f h1 h2) :: my_map2 f t1 t2);;\r
  62   \r
  63 end;;\r