1open HolKernel Parse boolLib bossLib 2open intLib binary_ieeeSyntax binary_ieeeLib machine_ieeeTheory 3open testutils 4 5(* 6fun printn s = print (s ^ "\n") 7fun die s = ( printn s; raise ERR "" "" ) 8val die = printn 9*) 10 11val () = show_tags := true 12 13(* ------------------------------------------------------------------------ *) 14 15local 16 val s_t = ``1w:word1`` 17 val s_f = ``0w:word1`` 18 fun s_tf b = if b then s_t else s_f 19in 20 fun float_constants ty = 21 let 22 val p as (t, w) = dest_float_ty ty 23 val itself = boolSyntax.mk_itself (pairSyntax.mk_prod p) 24 fun mk_lit (s, e, f) = 25 mk_floating_point 26 (s_tf s, wordsSyntax.mk_n2w (numLib.term_of_int e, w), 27 wordsSyntax.mk_n2w (numLib.term_of_int f, t)) 28 in 29 mk_float_some_qnan (Term.mk_var ("fp_op", mk_fp_op_ty (t, w))) :: 30 List.map (fn f => f itself) 31 [ mk_float_plus_zero, mk_float_minus_zero, 32 mk_float_plus_min, mk_float_top, mk_float_bottom, 33 mk_float_plus_infinity, mk_float_minus_infinity] @ 34 List.map mk_lit 35 [(false, 512, 0), 36 (false, 12, 123456)] 37 end 38end 39 40val round_constants = 41 [roundTiesToEven_tm, roundTowardPositive_tm, roundTowardNegative_tm, 42 roundTowardZero_tm] 43 44val round_constants = 45 [roundTiesToEven_tm, roundTowardZero_tm] 46 47fun has_tags tags thm = 48 case Tag.dest_tag (Thm.tag thm) of 49 (ts, []) => Lib.set_eq ts tags 50 | _ => false 51 52fun pr_term tm = 53 ( print "\n"; Lib.with_flag (show_types, true) print_term tm; print "\n" ) 54 55fun ok_result1 tm = 56 tm = boolSyntax.T orelse 57 tm = boolSyntax.F orelse 58 tm = nan_tm orelse 59 tm = infinity_tm orelse 60 (case Lib.total dest_float tm of 61 SOME r => is_ground_real r 62 | NONE => false) orelse 63 is_ground_real tm 64 65fun ok_float tm = 66 is_float_plus_infinity tm orelse 67 is_float_minus_infinity tm orelse 68 is_float_some_qnan tm orelse 69 Lib.can dest_floating_point tm 70 71fun ok_result2 tm = 72 case Lib.total pairSyntax.dest_pair tm of 73 SOME (_, t) => ok_float t 74 | NONE => ok_float tm 75 76fun ok_order_result tm = 77 tm = boolSyntax.T orelse 78 tm = boolSyntax.F orelse 79 tm = EQ_tm orelse 80 tm = GT_tm orelse 81 tm = LT_tm orelse 82 tm = UN_tm 83 84fun test_monops ty = 85 let 86 val cs = float_constants ty 87 in 88 print "\nChecking type: " 89 ; print_type ty 90 ; List.app 91 (fn (name, monop) => 92 ( print ("\n\nTesting operation: " ^ name ^ "\n") 93 ; List.app 94 (fn a => 95 let 96 val tm = 97 monop a handle e as HOL_ERR _ => (pr_term a; raise e) 98 val e1 = EVAL tm 99 val r = rhs (concl e1) 100 in 101 if ok_result1 r orelse ok_result2 r orelse 102 Lib.mem name ["float_negate", "float_abs"] andalso 103 is_float_some_qnan a 104 then print "." 105 else ( print "\n" 106 ; print_thm e1 107 ; print "\n" 108 ; die "test_monops failed" 109 ) 110 end) cs)) 111 [("float_negate", mk_float_negate), 112 ("float_abs", mk_float_abs), 113 ("float_value", mk_float_value), 114 ("float_is_nan", mk_float_is_nan), 115 ("float_is_signalling", mk_float_is_signalling), 116 ("float_is_infinite", mk_float_is_infinite), 117 ("float_is_finite", mk_float_is_finite), 118 ("float_is_normal", mk_float_is_normal), 119 ("float_is_subnormal", mk_float_is_subnormal), 120 ("float_is_zero", mk_float_is_zero) 121 ] 122 ; print "\nDone.\n" 123 end 124 125fun test_binops ty = 126 let 127 val cs = float_constants ty 128 in 129 print "\nChecking type: " 130 ; print_type ty 131 ; List.app 132 (fn (name, binop) => 133 ( print ("\n\nTesting operation: " ^ name ^ "\n") 134 ; List.app 135 (fn mode => 136 ( print "\nMode: "; print_term mode; print "\n" 137 ; List.app 138 (fn a => 139 List.app 140 (fn b => 141 let 142 val tm = binop (mode, a, b) 143 handle e as HOL_ERR _ => 144 ( pr_term mode 145 ; pr_term a 146 ; pr_term b 147 ; raise e 148 ) 149 val e1 = EVAL tm 150 val r = rhs (concl e1) 151 in 152 if ok_result2 r 153 then print "." 154 else ( print "\n" 155 ; print_thm e1 156 ; print "\n" 157 ; die "test_binops failed" 158 ) 159 end) cs) cs)) round_constants)) 160 [("float_add", mk_float_add), ("float_sub", mk_float_sub), 161 ("float_mul", mk_float_mul), ("float_div", mk_float_div) 162 ] 163 ; print "\nDone.\n" 164 end 165 166fun test_orderings ty = 167 let 168 val cs = float_constants ty 169 in 170 print "\nChecking type: " 171 ; print_type ty 172 ; List.app 173 (fn (name, binop) => 174 ( print ("\n\nTesting operation: " ^ name ^ "\n") 175 ; List.app 176 (fn a => 177 List.app 178 (fn b => 179 let 180 val tm = binop (a, b) 181 handle e as HOL_ERR _ => 182 ( pr_term a 183 ; pr_term b 184 ; raise e 185 ) 186 val e1 = EVAL tm 187 val r = rhs (concl e1) 188 in 189 if ok_order_result r 190 then print "." 191 else ( print "\n" 192 ; print_thm e1 193 ; print "\n" 194 ; die "test_orderings failed" 195 ) 196 end) cs) cs)) 197 [("float_less_than", mk_float_less_than), 198 ("float_less_equal", mk_float_less_equal), 199 ("float_greater_than", mk_float_greater_than), 200 ("float_greater_equal", mk_float_greater_equal), 201 ("float_equal", mk_float_equal), 202 ("float_compare", mk_float_compare)] 203 ; print "\nDone.\n" 204 end 205 206(* ------------------------------------------------------------------------ *) 207 208(* start tests *) 209val tt = Timer.startRealTimer () 210 211val () = test_monops ``:half`` 212val () = test_binops ``:half`` 213val () = test_orderings ``:half`` 214 215val () = test_monops ``:single`` 216val () = test_binops ``:single`` 217val () = test_orderings ``:single`` 218 219val elapsed = Timer.checkRealTimer tt; 220 221val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^ "\n") 222 223(* ------------------------------------------------------------------------ *) 224 225val _ = OS.Process.exit OS.Process.success 226