needs "arith/prove_lp.hl";;
needs "arith_test_data25.hl";;
needs "arith_test_data20.hl";;
needs "arith_test_data15.hl";;
needs "arith_test_data10.hl";;
needs "arith_test_data5.hl";;



let mul_op_num = `( * ):num->num->num` and
    mul_op_real = `( * ):real->real->real` and
    plus_op_num = `(+):num->num->num` and
    plus_op_real = `(+):real->real->real` and
    neg_op_real = `(--):real->real` and
    amp_op_real = `(&):num->real`;;


let mul_data_int = map (fun (t1,t2) -> mk_binop mul_op_real t1 t2) data;;
let add_data_int = map (fun (t1,t2) -> mk_binop plus_op_real t1 t2) data;;
let sub_data_int = map (fun (t1,t2) -> mk_binop plus_op_real t1 (mk_comb(neg_op_real, t2))) data;;


let NUM_TO_NUMERAL = rand o concl o NUM_TO_NUMERAL_CONV;;

let data2 = map (fun (t1,t2) -> (mk_comb(amp_op_real, NUM_TO_NUMERAL(rand t1)), 
				 mk_comb(amp_op_real, NUM_TO_NUMERAL(rand t2)))) data;;

let mul_data2 = map (fun (t1,t2) -> mk_binop mul_op_real t1 t2) data2;;
let add_data2 = map (fun (t1,t2) -> mk_binop plus_op_real t1 t2) data2;;
let sub_data2 = map (fun (t1,t2) -> mk_binop plus_op_real t1 (mk_comb(neg_op_real, t2))) data2;;



(**********************************)

(* data25 *)


(* 4: 10.645
   8: 3.592
 *)
test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;

(* 4: 0.208
   8: 0.132
*)
test 1 (map REAL_BITS_ADD_CONV) add_data_int;;

(* 4: 880
   8: 0.524
*)
test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;



(* 85.081 *)
test 1 (map REAL_INT_MUL_CONV) mul_data2;;

(* 0.808 *)
test 1 (map REAL_INT_ADD_CONV) add_data2;;

(* 2.588 *)
test 1 (map REAL_INT_ADD_CONV) sub_data2;;



(**********************************)

(* data20 *)


(* 4: 6.092
   8: 2.256
 *)
test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;

(* 4: 0.176
   8: 0.108
*)
test 1 (map REAL_BITS_ADD_CONV) add_data_int;;

(* 4: 0.728
   8: 0.420
*)
test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;




(* 59.160 *)
test 1 (map REAL_INT_MUL_CONV) mul_data2;;

(* 0.648 *)
test 1 (map REAL_INT_ADD_CONV) add_data2;;

(* 2.392 *)
test 1 (map REAL_INT_ADD_CONV) sub_data2;;




(**********************************)

(* data15 *)


(* 4: 3.880
   8: 1.316
 *)
test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;

(* 4: 0.112
   8: 0.096
*)
test 1 (map REAL_BITS_ADD_CONV) add_data_int;;

(* 4: 0.560
   8: 0.340
*)
test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;


(* 16.081 *)
test 1 (map REAL_INT_MUL_CONV) mul_data2;;

(* 0.492 *)
test 1 (map REAL_INT_ADD_CONV) add_data2;;

(* 1.792 *)
test 1 (map REAL_INT_ADD_CONV) sub_data2;;



(**********************************)

(* data10 *)


(* 4: 1.292
   8: 0.376
 *)
test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;

(* 4: 0.100
   8: 0.064
*)
test 1 (map REAL_BITS_ADD_CONV) add_data_int;;

(* 4: 0.328
   8: 0.220
*)
test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;



(* 7.216 *)
test 1 (map REAL_INT_MUL_CONV) mul_data2;;

(* 0.324 *)
test 1 (map REAL_INT_ADD_CONV) add_data2;;

(* 0.876 *)
test 1 (map REAL_INT_ADD_CONV) sub_data2;;




(**********************************)

(* data5 *)


(* 4: 0.428
   8: 0.148
 *)
test 1 (map REAL_BITS_MUL_CONV) mul_data_int;;

(* 4: 0.064
   8: 0.052
*)
test 1 (map REAL_BITS_ADD_CONV) add_data_int;;

(* 4: 0.192
   8: 0.132
*)
test 1 (map REAL_BITS_ADD_CONV) sub_data_int;;



(* 2.220 *)
test 1 (map REAL_INT_MUL_CONV) mul_data2;;

(* 0.188 *)
test 1 (map REAL_INT_ADD_CONV) add_data2;;

(* 0.568 *)
test 1 (map REAL_INT_ADD_CONV) sub_data2;;