1 needs "../formal_lp/arith/float.hl";;
2 needs "../formal_lp/arith/arith_hash_rat.hl";;
6 let rec float_interval_test pp expr x_th =
10 let ltm, r_tm = dest_comb expr in
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
24 failwith ("Unknown operation: " ^ (fst o dest_const) op)
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
30 mk_float_interval_num (dest_numeral r_tm);;
33 let rec rat_arith_test expr x_th =
37 let ltm, r_tm = dest_comb expr in
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
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
52 failwith ("Unknown operation: " ^ (fst o dest_const) op) in
55 AP_TERM ltm (NUMERAL_TO_NUM_CONV r_tm);;
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`;;
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.)))));;
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;;
83 let x2_th = float_interval_div pp int1 int3;;
84 let x3_th = float_interval_div pp int234451 int1234567;;
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;;
92 10, min_exp = 20: 0.180
93 100, min_exp = 20: 0.144 *)
95 100, min_exp = 20: 0.116 *)
97 8, min_exp = 20: 0.060 *)
99 float_interval_test pp expr3 x_th;;
100 test 1 (float_interval_test pp expr3) x_th;;
102 float_interval_test pp eps_expr x_th;;
104 let th1 = float_interval_test pp expr3 x_th;;
105 let th2 = float_interval_sub pp th1 x2_th;;
108 float_interval_test pp expr3 x1_th;;
109 float_interval_test pp expr3 x2_th;;
110 float_interval_test pp expr3 x3_th;;
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`;;
117 rat_arith_test expr1 y1_th;;
118 float_interval_test pp expr1 x1_th;;
120 rat_arith_test expr2 y1_th;;
121 float_interval_test pp expr2 x1_th;;
123 rat_arith_test expr1 y2_th;;
124 float_interval_test pp expr1 x2_th;;
126 rat_arith_test expr2 y2_th;;
127 float_interval_test pp expr2 x2_th;;
129 rat_arith_test expr1 y3_th;;
130 float_interval_test pp expr1 x3_th;;
132 rat_arith_test expr2 y3_th;;
133 float_interval_test pp expr2 x3_th;;
139 test 100 (rat_arith_test expr1) y1_th;;
141 test 100 (float_interval_test pp expr1) x1_th;;
144 test 100 (rat_arith_test expr2) y1_th;;
146 test 100 (float_interval_test pp expr2) x1_th;;
149 test 100 (rat_arith_test expr1) y2_th;;
151 test 100 (float_interval_test pp expr1) x2_th;;
154 test 100 (rat_arith_test expr2) y2_th;;
156 test 100 (float_interval_test pp expr2) x2_th;;
159 test 10 (rat_arith_test expr1) y3_th;;
161 test 10 (float_interval_test pp expr1) x3_th;;
164 test 100 (rat_arith_test expr2) y3_th;;
166 test 100 (float_interval_test pp expr2) x3_th;;