1structure binary_ieeeSyntax :> binary_ieeeSyntax = 2struct 3 4open Abbrev HolKernel 5open realSyntax fcpSyntax wordsSyntax binary_ieeeTheory 6 7val ERR = Feedback.mk_HOL_ERR "binary_ieeeSyntax" 8 9(* ------------------------------------------------------------------------- *) 10 11val float_value_ty = 12 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float_value", Args = []} 13 14val rounding_ty = 15 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "rounding", Args = []} 16 17val flags_ty = 18 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "flags", Args = []} 19 20val float_compare_ty = 21 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float_compare", Args = []} 22 23fun mk_float_ty (t, w) = 24 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "float", Args = [t, w]} 25 26fun mk_fp_op_ty (t, w) = 27 Type.mk_thy_type {Thy = "binary_ieee", Tyop = "fp_op", Args = [t, w]} 28 29fun dest_float_ty ty = 30 case Type.dest_thy_type ty of 31 {Thy = "binary_ieee", Args = [t, w], Tyop = "float"} => (t, w) 32 | _ => raise ERR "dest_float_ty" "" 33 34fun dest_fp_op_ty ty = 35 case Type.dest_thy_type ty of 36 {Thy = "binary_ieee", Args = [t, w], Tyop = "fp_op"} => (t, w) 37 | _ => raise ERR "dest_fp_op_ty" "" 38 39val mk_ifloat_ty = 40 mk_float_ty o 41 (fcpSyntax.mk_int_numeric_type ## fcpSyntax.mk_int_numeric_type) 42 43val dest_ifloat_ty = 44 (fcpSyntax.dest_int_numeric_type ## fcpSyntax.dest_int_numeric_type) o 45 dest_float_ty 46 47fun mk_floating_point (s, e, f) = 48 TypeBase.mk_record 49 (mk_float_ty (wordsSyntax.dim_of f, wordsSyntax.dim_of e), 50 [("Sign", s), ("Exponent", e), ("Significand", f)]) 51 52fun dest_floating_point tm = 53 case Lib.with_exn TypeBase.dest_record tm (ERR "dest_floating_point" "") of 54 (_, [("Sign", s), ("Exponent", e), ("Significand", f)]) => (s, e, f) 55 | _ => raise ERR "dest_floating_point" "" 56 57fun float_of_triple ((t, w), (s, e, f)) = 58 mk_floating_point 59 (wordsSyntax.mk_wordii (if s then 1 else 0, 1), 60 wordsSyntax.mk_wordi (e, w), 61 wordsSyntax.mk_wordi (f, t)) 62 63local 64 val sz = Arbnum.toInt o wordsSyntax.size_of 65in 66 fun triple_of_float tm = 67 let 68 val (s, e, f) = dest_floating_point tm 69 in 70 ((sz f, sz e), 71 (wordsSyntax.uint_of_word s = 1, 72 wordsSyntax.dest_word_literal e, 73 wordsSyntax.dest_word_literal f)) 74 end 75end 76 77fun mk_float_var tw = fn v => Term.mk_var (v, mk_float_ty tw) 78fun mk_ifloat_var tw = fn v => Term.mk_var (v, mk_ifloat_ty tw) 79 80fun is_pure_real_literal tm = 81 case Lib.total realSyntax.dest_injected tm of 82 SOME a => numSyntax.is_numeral a 83 | NONE => false 84 85fun is_ground_real tm = 86 case Lib.total realSyntax.dest_div tm of 87 SOME (a, b) => realSyntax.is_real_literal a andalso is_pure_real_literal b 88 | NONE => realSyntax.is_real_literal tm 89 90(* ------------------------------------------------------------------------- *) 91 92val monop = HolKernel.syntax_fns1 "binary_ieee" 93val binop = HolKernel.syntax_fns2 "binary_ieee" 94val triop = HolKernel.syntax_fns3 "binary_ieee" 95val quadop = HolKernel.syntax_fns4 "binary_ieee" 96 97fun syntax_fns x = HolKernel.syntax_fns x "binary_ieee" 98 99val tw_monop = 100 syntax_fns 101 {n = 1, 102 dest = 103 fn tm1 => fn e => fn tm2 => 104 let 105 val ty = boolSyntax.dest_itself (HolKernel.dest_monop tm1 e tm2) 106 val (t, w) = pairSyntax.dest_prod ty 107 in 108 (fcpSyntax.dest_int_numeric_type t, 109 fcpSyntax.dest_int_numeric_type w) 110 end, 111 make = 112 fn tm1 => fn (t, w) => 113 let 114 val t_ty = fcpSyntax.mk_int_numeric_type t 115 val w_ty = fcpSyntax.mk_int_numeric_type w 116 val p_ty = pairSyntax.mk_prod (t_ty, w_ty) 117 in 118 boolSyntax.mk_icomb (tm1, boolSyntax.mk_itself p_ty) 119 end} 120 121val etw_monop = 122 syntax_fns 123 {n = 1, 124 dest = 125 fn tm1 => fn e => fn tm2 => 126 let 127 val (t1, t2) = 128 pairSyntax.dest_pair (HolKernel.dest_monop tm1 e tm2) 129 val t = boolSyntax.dest_itself t2 130 val w = wordsSyntax.size_of t1 131 in 132 (wordsSyntax.uint_of_word t1, 133 fcpSyntax.dest_int_numeric_type t, 134 Arbnum.toInt w) 135 end, 136 make = 137 fn tm1 => fn (i, t, w) => 138 let 139 val t1 = wordsSyntax.mk_wordii (i, w) 140 val t2 = boolSyntax.mk_itself (fcpSyntax.mk_int_numeric_type t) 141 in 142 boolSyntax.mk_icomb (tm1, pairSyntax.mk_pair (t1, t2)) 143 end} 144 145val tw_binop = 146 syntax_fns 147 {n = 2, 148 dest = 149 fn tm1 => fn e => fn tm2 => 150 let 151 val (a, b) = HolKernel.dest_binop tm1 e tm2 152 val (ty1, ty2) = dest_float_ty (Term.type_of tm2) 153 in 154 (a, b, ty1, ty2) 155 end, 156 make = 157 fn tm1 => fn (tm2, tm3, t, w) => 158 Term.inst [``:'w`` |-> w, ``:'t`` |-> t] 159 (HolKernel.mk_binop tm1 (tm2, tm3))} 160 161val tw_triop = 162 syntax_fns 163 {n = 3, 164 dest = 165 fn tm1 => fn e => fn tm2 => 166 let 167 val (a, b, c) = HolKernel.dest_triop tm1 e tm2 168 val (ty1, ty2) = dest_float_ty (Term.type_of tm2) 169 in 170 (a, b, c, ty1, ty2) 171 end, 172 make = 173 fn tm1 => fn (tm2, tm3, tm4, t, w) => 174 Term.inst [``:'w`` |-> w, ``:'t`` |-> t] 175 (HolKernel.mk_triop tm1 (tm2, tm3, tm4))} 176 177(* ------------------------------------------------------------------------- *) 178 179fun const (s, ty) = Term.mk_thy_const {Ty = ty, Thy = "binary_ieee", Name = s} 180 181val infinity_tm = const ("Infinity", ``:binary_ieee$float_value``) 182val nan_tm = const ("NaN", ``:binary_ieee$float_value``) 183 184val (roundTiesToEven_tm, roundTowardPositive_tm, roundTowardNegative_tm, 185 roundTowardZero_tm) = 186 Lib.quadruple_of_list (TypeBase.constructors_of ``:binary_ieee$rounding``) 187 188val (LT_tm, EQ_tm, GT_tm, UN_tm) = 189 Lib.quadruple_of_list 190 (TypeBase.constructors_of ``:binary_ieee$float_compare``) 191 192(* ------------------------------------------------------------------------- *) 193 194val (float_tm, mk_float, dest_float, is_float) = monop "Float" 195 196val (float_sign_tm, mk_float_sign, dest_float_sign, is_float_sign) = 197 monop "float_Sign" 198 199val (float_exponent_tm, mk_float_exponent, dest_float_exponent, 200 is_float_exponent) = monop "float_Exponent" 201 202val (float_significand_tm, mk_float_significand, dest_float_significand, 203 is_float_significand) = monop "float_Significand" 204 205val (float_to_real_tm, mk_float_to_real, dest_float_to_real, is_float_to_real) = 206 monop "float_to_real" 207 208val (float_value_tm, mk_float_value, dest_float_value, is_float_value) = 209 monop "float_value" 210 211val (float_is_nan_tm, mk_float_is_nan, dest_float_is_nan, is_float_is_nan) = 212 monop "float_is_nan" 213 214val (float_is_signalling_tm, mk_float_is_signalling, dest_float_is_signalling, 215 is_float_is_signalling) = monop "float_is_signalling" 216 217val (float_is_infinite_tm, mk_float_is_infinite, dest_float_is_infinite, 218 is_float_is_infinite) = monop "float_is_infinite" 219 220val (float_is_normal_tm, mk_float_is_normal, dest_float_is_normal, 221 is_float_is_normal) = monop "float_is_normal" 222 223val (float_is_subnormal_tm, mk_float_is_subnormal, dest_float_is_subnormal, 224 is_float_is_subnormal) = monop "float_is_subnormal" 225 226val (float_is_zero_tm, mk_float_is_zero, dest_float_is_zero, is_float_is_zero) = 227 monop "float_is_zero" 228 229val (float_is_finite_tm, mk_float_is_finite, dest_float_is_finite, 230 is_float_is_finite) = monop "float_is_finite" 231 232val (float_is_integral_tm, mk_float_is_integral, dest_float_is_integral, 233 is_float_is_integral) = monop "float_is_integral" 234 235val (float_negate_tm, mk_float_negate, dest_float_negate, is_float_negate) = 236 monop "float_negate" 237 238val (float_abs_tm, mk_float_abs, dest_float_abs, is_float_abs) = 239 monop "float_abs" 240 241val (float_plus_infinity_tm, mk_float_plus_infinity, dest_float_plus_infinity, 242 is_float_plus_infinity) = monop "float_plus_infinity" 243 244val (float_plus_zero_tm, mk_float_plus_zero, dest_float_plus_zero, 245 is_float_plus_zero) = monop "float_plus_zero" 246 247val (float_top_tm, mk_float_top, dest_float_top, is_float_top) = 248 monop "float_top" 249 250val (float_plus_min_tm, mk_float_plus_min, dest_float_plus_min, 251 is_float_plus_min) = monop "float_plus_min" 252 253val (float_minus_infinity_tm, mk_float_minus_infinity, 254 dest_float_minus_infinity, is_float_minus_infinity) = 255 monop "float_minus_infinity" 256 257val (float_minus_zero_tm, mk_float_minus_zero, dest_float_minus_zero, 258 is_float_minus_zero) = monop "float_minus_zero" 259 260val (float_bottom_tm, mk_float_bottom, dest_float_bottom, is_float_bottom) = 261 monop "float_bottom" 262 263val (float_minus_min_tm, mk_float_minus_min, dest_float_minus_min, 264 is_float_minus_min) = monop "float_minus_min" 265 266val (float_some_qnan_tm, mk_float_some_qnan, dest_float_some_qnan, 267 is_float_some_qnan) = monop "float_some_qnan" 268 269val (largest_tm, mk_largest, dest_largest, is_largest) = monop "largest" 270 271val (threshold_tm, mk_threshold, dest_threshold, is_threshold) = 272 monop "threshold" 273 274val (ulp_tm, mk_ulp, dest_ulp, is_ulp) = monop "ulp" 275 276val (ULP_tm, mk_ULP, dest_ULP, is_ULP) = monop "ULP" 277 278val (integral_round_tm, mk_integral_round, dest_integral_round, 279 is_integral_round) = binop "integral_round" 280 281val (float_to_int_tm, mk_float_to_int, dest_float_to_int, 282 is_float_to_int) = binop "float_to_int" 283 284val (float_round_to_integral_tm, mk_float_round_to_integral, 285 dest_float_round_to_integral, is_float_round_to_integral) = 286 binop "float_round_to_integral" 287 288val (float_sqrt_tm, mk_float_sqrt, dest_float_sqrt, is_float_sqrt) = 289 binop "float_sqrt" 290 291val (float_add_tm, mk_float_add, dest_float_add, is_float_add) = 292 triop "float_add" 293 294val (float_sub_tm, mk_float_sub, dest_float_sub, is_float_sub) = 295 triop "float_sub" 296 297val (float_mul_tm, mk_float_mul, dest_float_mul, is_float_mul) = 298 triop "float_mul" 299 300val (float_div_tm, mk_float_div, dest_float_div, is_float_div) = 301 triop "float_div" 302 303val (float_compare_tm, mk_float_compare, dest_float_compare, is_float_compare) = 304 binop "float_compare" 305 306val (float_less_than_tm, mk_float_less_than, dest_float_less_than, 307 is_float_less_than) = 308 binop "float_less_than" 309 310val (float_greater_than_tm, mk_float_greater_than, dest_float_greater_than, 311 is_float_greater_than) = 312 binop "float_greater_than" 313 314val (float_less_equal_tm, mk_float_less_equal, dest_float_less_equal, 315 is_float_less_equal) = 316 binop "float_less_equal" 317 318val (float_greater_equal_tm, mk_float_greater_equal, dest_float_greater_equal, 319 is_float_greater_equal) = 320 binop "float_greater_equal" 321 322val (float_equal_tm, mk_float_equal, dest_float_equal, is_float_equal) = 323 binop "float_equal" 324 325val (float_mul_add_tm, mk_float_mul_add, dest_float_mul_add, is_float_mul_add) = 326 quadop "float_mul_add" 327 328val (float_mul_sub_tm, mk_float_mul_sub, dest_float_mul_sub, is_float_mul_sub) = 329 quadop "float_mul_sub" 330 331(* ------------------------------------------------------------------------- *) 332 333val (round_tm, mk_round, dest_round, is_round) = tw_binop "round" 334 335val (float_round_tm, mk_float_round, dest_float_round, is_float_round) = 336 tw_triop "float_round" 337 338val (float_round_with_flags_tm, mk_float_round_with_flags, 339 dest_float_round_with_flags, is_float_round_with_flags) = 340 tw_triop "float_round_with_flags" 341 342val (real_to_float_tm, mk_real_to_float, dest_real_to_float, is_real_to_float) = 343 binop "real_to_float" 344 345val (real_to_float_with_flags_tm, mk_real_to_float_with_flags, 346 dest_real_to_float_with_flags, is_real_to_float_with_flags) = 347 binop "real_to_float_with_flags" 348 349(* ------------------------------------------------------------------------- *) 350 351val (_, mk_int_float_plus_infinity, dest_int_float_plus_infinity, 352 is_int_float_plus_infinity) = tw_monop "float_plus_infinity" 353 354val (_, mk_int_float_plus_zero, dest_int_float_plus_zero, 355 is_int_float_plus_zero) = tw_monop "float_plus_zero" 356 357val (_, mk_int_float_top, dest_int_float_top, is_int_float_top) = 358 tw_monop "float_top" 359 360val (_, mk_int_float_plus_min, dest_int_float_plus_min, is_int_float_plus_min) = 361 tw_monop "float_plus_min" 362 363val (_, mk_int_float_minus_infinity, 364 dest_int_float_minus_infinity, is_int_float_minus_infinity) = 365 tw_monop "float_minus_infinity" 366 367val (_, mk_int_float_minus_zero, dest_int_float_minus_zero, 368 is_int_float_minus_zero) = tw_monop "float_minus_zero" 369 370val (_, mk_int_float_bottom, dest_int_float_bottom, is_int_float_bottom) = 371 tw_monop "float_bottom" 372 373val (_, mk_int_float_minus_min, dest_int_float_minus_min, 374 is_int_float_minus_min) = tw_monop "float_minus_min" 375 376val (_, mk_int_float_some_qnan, dest_int_float_some_qnan, 377 is_int_float_some_qnan) = tw_monop "float_some_qnan" 378 379val (_, mk_int_largest, dest_int_largest, is_int_largest) = tw_monop "largest" 380 381val (_, mk_int_threshold, dest_int_threshold, is_int_threshold) = 382 tw_monop "threshold" 383 384val (_, mk_int_ulp, dest_int_ulp, is_int_ulp) = tw_monop "ulp" 385 386val (_, mk_int_ULP, dest_int_ULP, is_int_ULP) = etw_monop "ULP" 387 388end 389