formal_lp/old/arith/misc.hl

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