formal_lp/old/arith/tests/test_nat_arith.hl

   1 needs "arith/prove_lp.hl";;
   2 needs "arith_test_data25.hl";;
   3 needs "arith_test_data20.hl";;
   4 needs "arith_test_data15.hl";;
   5 needs "arith_test_data10.hl";;
   6 needs "arith_test_data5.hl";;
   7
   8
   9
  10 let mul_op_num = `( * ):num->num->num` and
  11     mul_op_real = `( * ):real->real->real` and
  12     plus_op_num = `(+):num->num->num` and
  13     plus_op_real = `(+):real->real->real` and
  14     neg_op_real = `(--):real->real` and
  15     amp_op_real = `(&):num->real`;;
  16
  17
  18 let mul_data_int = map (fun (t1,t2) -> mk_binop mul_op_real t1 t2) data;;
  19 let add_data_int = map (fun (t1,t2) -> mk_binop plus_op_real t1 t2) data;;
  20 let sub_data_int = map (fun (t1,t2) -> mk_binop plus_op_real t1 (mk_comb(neg_op_real, t2))) data;;
  21
  22
  23 let NUM_TO_NUMERAL = rand o concl o NUM_TO_NUMERAL_CONV;;
  24
  25 let data2 = map (fun (t1,t2) -> (mk_comb(amp_op_real, NUM_TO_NUMERAL(rand t1)),
  26                                  mk_comb(amp_op_real, NUM_TO_NUMERAL(rand t2)))) data;;
  27
  28 let mul_data2 = map (fun (t1,t2) -> mk_binop mul_op_real t1 t2) data2;;
  29 let add_data2 = map (fun (t1,t2) -> mk_binop plus_op_real t1 t2) data2;;
  30 let sub_data2 = map (fun (t1,t2) -> mk_binop plus_op_real t1 (mk_comb(neg_op_real, t2))) data2;;
  31
  32
  33
  34 (**********************************)
  35
  36 (* data25 *)
  37
  38
  39 (* 4: 10.645
  40    8: 3.592
  41  *)
  42 test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;
  43
  44 (* 4: 0.208
  45    8: 0.132
  46 *)
  47 test 1 (map REAL_BITS_ADD_CONV) add_data_int;;
  48
  49 (* 4: 880
  50    8: 0.524
  51 *)
  52 test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;
  53
  54
  55
  56 (* 85.081 *)
  57 test 1 (map REAL_INT_MUL_CONV) mul_data2;;
  58
  59 (* 0.808 *)
  60 test 1 (map REAL_INT_ADD_CONV) add_data2;;
  61
  62 (* 2.588 *)
  63 test 1 (map REAL_INT_ADD_CONV) sub_data2;;
  64
  65
  66
  67 (**********************************)
  68
  69 (* data20 *)
  70
  71
  72 (* 4: 6.092
  73    8: 2.256
  74  *)
  75 test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;
  76
  77 (* 4: 0.176
  78    8: 0.108
  79 *)
  80 test 1 (map REAL_BITS_ADD_CONV) add_data_int;;
  81
  82 (* 4: 0.728
  83    8: 0.420
  84 *)
  85 test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;
  86
  87
  88
  89
  90 (* 59.160 *)
  91 test 1 (map REAL_INT_MUL_CONV) mul_data2;;
  92
  93 (* 0.648 *)
  94 test 1 (map REAL_INT_ADD_CONV) add_data2;;
  95
  96 (* 2.392 *)
  97 test 1 (map REAL_INT_ADD_CONV) sub_data2;;
  98
  99
 100
 101
 102 (**********************************)
 103
 104 (* data15 *)
 105
 106
 107 (* 4: 3.880
 108    8: 1.316
 109  *)
 110 test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;
 111
 112 (* 4: 0.112
 113    8: 0.096
 114 *)
 115 test 1 (map REAL_BITS_ADD_CONV) add_data_int;;
 116
 117 (* 4: 0.560
 118    8: 0.340
 119 *)
 120 test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;
 121
 122
 123 (* 16.081 *)
 124 test 1 (map REAL_INT_MUL_CONV) mul_data2;;
 125
 126 (* 0.492 *)
 127 test 1 (map REAL_INT_ADD_CONV) add_data2;;
 128
 129 (* 1.792 *)
 130 test 1 (map REAL_INT_ADD_CONV) sub_data2;;
 131
 132
 133
 134 (**********************************)
 135
 136 (* data10 *)
 137
 138
 139 (* 4: 1.292
 140    8: 0.376
 141  *)
 142 test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;
 143
 144 (* 4: 0.100
 145    8: 0.064
 146 *)
 147 test 1 (map REAL_BITS_ADD_CONV) add_data_int;;
 148
 149 (* 4: 0.328
 150    8: 0.220
 151 *)
 152 test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;
 153
 154
 155
 156 (* 7.216 *)
 157 test 1 (map REAL_INT_MUL_CONV) mul_data2;;
 158
 159 (* 0.324 *)
 160 test 1 (map REAL_INT_ADD_CONV) add_data2;;
 161
 162 (* 0.876 *)
 163 test 1 (map REAL_INT_ADD_CONV) sub_data2;;
 164
 165
 166
 167
 168 (**********************************)
 169
 170 (* data5 *)
 171
 172
 173 (* 4: 0.428
 174    8: 0.148
 175  *)
 176 test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;
 177
 178 (* 4: 0.064
 179    8: 0.052
 180 *)
 181 test 1 (map REAL_BITS_ADD_CONV) add_data_int;;
 182
 183 (* 4: 0.192
 184    8: 0.132
 185 *)
 186 test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;
 187
 188
 189
 190 (* 2.220 *)
 191 test 1 (map REAL_INT_MUL_CONV) mul_data2;;
 192
 193 (* 0.188 *)
 194 test 1 (map REAL_INT_ADD_CONV) add_data2;;
 195
 196 (* 0.568 *)
 197 test 1 (map REAL_INT_ADD_CONV) sub_data2;;