formal_lp/old/arith/float_test.hl

   1 needs "../formal_lp/arith/float.hl";;
   2 needs "../formal_lp/arith/arith_hash_rat.hl";;
   3
   4
   5
   6 let rec float_interval_test pp expr x_th =
   7   if is_var expr then
   8     x_th
   9   else
  10     let ltm, r_tm = dest_comb expr in
  11       if is_comb ltm then
  12         let op, l_tm = dest_comb ltm in
  13         let l_th = float_interval_test pp l_tm x_th in
  14         let r_th = float_interval_test pp r_tm x_th in
  15           if op = plus_op_real then
  16             float_interval_add pp l_th r_th
  17           else if op = mul_op_real then
  18             float_interval_mul pp l_th r_th
  19           else if op = div_op_real then
  20             float_interval_div pp l_th r_th
  21           else if op = minus_op_real then
  22             float_interval_sub pp l_th r_th
  23           else
  24             failwith ("Unknown operation: " ^ (fst o dest_const) op)
  25       else
  26         if ltm = neg_op_real then
  27           let r_th = float_interval_test pp r_tm x_th in
  28             float_interval_neg r_th
  29         else
  30           mk_float_interval_num (dest_numeral r_tm);;
  31
  32
  33 let rec rat_arith_test expr x_th =
  34   if is_var expr then
  35     x_th
  36   else
  37     let ltm, r_tm = dest_comb expr in
  38       if is_comb ltm then
  39         let op, l_tm = dest_comb ltm in
  40         let l_th = rat_arith_test l_tm x_th in
  41         let r_th = rat_arith_test r_tm x_th in
  42         let th0 = MK_COMB (AP_TERM op l_th, r_th) in
  43         let rtm = rand(concl th0) in
  44         let th1 =
  45           if op = plus_op_real then
  46             my_real_rat_add_conv rtm
  47           else if op = mul_op_real then
  48             my_real_rat_mul_conv rtm
  49           else if op = div_op_real then
  50             my_real_rat_div_conv rtm
  51           else
  52             failwith ("Unknown operation: " ^ (fst o dest_const) op) in
  53           TRANS th0 th1
  54       else
  55         AP_TERM ltm (NUMERAL_TO_NUM_CONV r_tm);;
  56
  57
  58
  59
  60
  61 let expr1 = `&1 + x + x*x / &2 + x*x*x / &6 + x*x*x*x / &24 + x*x*x*x*x / &120 + x*x*x*x*x*x / &720`;;
  62 let expr2 = `&1 + x*(&1 + x*(&1 / &2 + x*(&1 / &6 + x*(&1 / &24 + x*(&1 / &120 + x / &720)))))`;;
  63 let expr3 = `&1 + x*x*(--(&1 / &2) + x*x*(&1 / &24 + x*x*(--(&1 / &720) + x*x*(&1 / &40320 + x*x*(--(&1 / &3628800) + x*x / &479001600)))))`;;
  64 let eps_expr = `x*x*x*x*x*x*x*x*x*x*x*x*x*x / &87178291200`;;
  65
  66
  67 let f x =
  68   1. +. x*.x*.(~-. 0.5 +. x*.x*.(1. /. 24. +. x*.x*.(~-.1. /. 720. +. x*.x*.(1. /. 40320. +. x*.x*.(~-. 1. /. 3628800. +. x*.x /. 479001600.)))));;
  69
  70 f 1.230959417;;
  71
  72
  73
  74 let int1 = mk_float_interval_small_num 1 and
  75     int3 = mk_float_interval_small_num 3 and
  76     int234451 = mk_float_interval_small_num 234451 and
  77     int1234567 = mk_float_interval_small_num 1234567;;
  78
  79
  80 let pp = 10;;
  81
  82 let x1_th = int1;;
  83 let x2_th = float_interval_div pp int1 int3;;
  84 let x3_th = float_interval_div pp int234451 int1234567;;
  85
  86 let x_th =
  87   let n = mk_float_interval_num (Num.num_of_string "1230959417") in
  88   let d = mk_float_interval_num (Num.num_of_string "1000000000") in
  89     float_interval_div pp n d;;
  90
  91 (* pp = 11:
  92    10, min_exp = 20: 0.180
  93    100, min_exp = 20: 0.144 *)
  94 (* pp = 6:
  95    100, min_exp = 20: 0.116 *)
  96 (* pp = 5:
  97    8, min_exp = 20: 0.060 *)
  98
  99 float_interval_test pp expr3 x_th;;
 100 test 1 (float_interval_test pp expr3) x_th;;
 101
 102 float_interval_test pp eps_expr x_th;;
 103
 104 let th1 = float_interval_test pp expr3 x_th;;
 105 let th2 = float_interval_sub pp th1 x2_th;;
 106
 107
 108 float_interval_test pp expr3 x1_th;;
 109 float_interval_test pp expr3 x2_th;;
 110 float_interval_test pp expr3 x3_th;;
 111
 112
 113 let y1_th = REPLACE_NUMERALS_CONV `&1`;;
 114 let y2_th = REPLACE_NUMERALS_CONV `&1 / &3`;;
 115 let y3_th = REPLACE_NUMERALS_CONV `&234451 / &1234567`;;
 116
 117 rat_arith_test expr1 y1_th;;
 118 float_interval_test pp expr1 x1_th;;
 119
 120 rat_arith_test expr2 y1_th;;
 121 float_interval_test pp expr2 x1_th;;
 122
 123 rat_arith_test expr1 y2_th;;
 124 float_interval_test pp expr1 x2_th;;
 125
 126 rat_arith_test expr2 y2_th;;
 127 float_interval_test pp expr2 x2_th;;
 128
 129 rat_arith_test expr1 y3_th;;
 130 float_interval_test pp expr1 x3_th;;
 131
 132 rat_arith_test expr2 y3_th;;
 133 float_interval_test pp expr2 x3_th;;
 134
 135
 136
 137
 138 (* 4: 0.624 *)
 139 test 100 (rat_arith_test expr1) y1_th;;
 140 (* 4: 2.028 *)
 141 test 100 (float_interval_test pp expr1) x1_th;;
 142
 143 (* 4: 0.496 *)
 144 test 100 (rat_arith_test expr2) y1_th;;
 145 (* 4: 1.756 *)
 146 test 100 (float_interval_test pp expr2) x1_th;;
 147
 148 (* 4: 1.012 *)
 149 test 100 (rat_arith_test expr1) y2_th;;
 150 (* 4: 4.252 *)
 151 test 100 (float_interval_test pp expr1) x2_th;;
 152
 153 (* 4: 0.760 *)
 154 test 100 (rat_arith_test expr2) y2_th;;
 155 (* 4: 2.460 *)
 156 test 100 (float_interval_test pp expr2) x2_th;;
 157
 158 (* 4: 5.732 *)
 159 test 10 (rat_arith_test expr1) y3_th;;
 160 (* 4: 0.468 *)
 161 test 10 (float_interval_test pp expr1) x3_th;;
 162
 163 (* 4: 1.504 *)
 164 test 100 (rat_arith_test expr2) y3_th;;
 165 (* 4: 0.244 *)
 166 test 100 (float_interval_test pp expr2) x3_th;;