1(* ------------------------------------------------------------------------ 2 Conversions for evaluating IEEE-754 operations. 3 The evaluation of rounding (to zero and nearest) uses a certification 4 approach, with calculations performed over rational numbers at the ML level. 5 (Rounding to +/-INF is not currently supported.) 6 ------------------------------------------------------------------------ *) 7structure binary_ieeeLib :> binary_ieeeLib = 8struct 9 10open HolKernel Parse boolLib bossLib 11open realLib wordsLib binary_ieeeSyntax 12 13structure Parse = 14struct 15 open Parse 16 val (Type, Term) = 17 parse_from_grammars binary_ieeeTheory.binary_ieee_grammars 18end 19open Parse 20 21val ERR = Feedback.mk_HOL_ERR "binary_ieeeLib" 22 23val lhsc = boolSyntax.lhs o Thm.concl 24val rhsc = boolSyntax.rhs o Thm.concl 25 26(* ------------------------------------------------------------------------ 27 real_to_arbrat 28 arbrat_to_real 29 ------------------------------------------------------------------------ *) 30 31local 32 fun real_to_pos_arbrat tm = 33 case Lib.total realSyntax.dest_injected tm of 34 SOME a => Arbrat.fromNat (numLib.dest_numeral a) 35 | NONE => raise ERR "real_to_pos_arbrat" "" 36 fun real_to_signed_arbrat tm = 37 case Lib.total realSyntax.dest_negated tm of 38 SOME a => Arbrat.negate (real_to_pos_arbrat a) 39 | NONE => real_to_pos_arbrat tm 40in 41 fun real_to_arbrat tm = 42 case Lib.total realSyntax.dest_div tm of 43 SOME (a, b) => 44 Arbrat./ (real_to_signed_arbrat a, real_to_signed_arbrat b) 45 | NONE => real_to_signed_arbrat tm 46 fun arbrat_to_real r = 47 let 48 val n = realSyntax.term_of_int (Arbrat.numerator r) 49 val d = Arbrat.denominator r 50 in 51 if d = Arbnum.one 52 then n 53 else realSyntax.mk_div (n, realSyntax.term_of_int (Arbint.fromNat d)) 54 end 55end 56 57(* ------------------------------------------------------------------------ 58 float_to_real 59 real_to_float 60 ------------------------------------------------------------------------ *) 61 62local 63 fun is_negative_rat r = Arbrat.< (r, Arbrat.zero) 64 val nfloor = Arbint.toNat o Arbrat.floor 65 fun lg2 n = if n = Arbnum.zero then Arbnum.zero else Arbnum.log2 n 66 fun pow2 n = Arbnum.pow (Arbnum.two, n) 67 fun dimword w = pow2 (Arbnum.fromInt w) 68 fun uint_max w = Arbnum.less1 (dimword w) 69 fun int_max w = Arbnum.less1 (dimword (w - 1)) 70 fun frac i = Arbrat.- (Arbrat.two, Arbrat.inv (Arbrat.fromNat (dimword i))) 71 val diff = Arbrat.abs o Arbrat.- 72 fun evenfloat (s: bool, e: Arbnum.num, f) = Arbnum.mod2 f = Arbnum.zero 73 fun negativefloat (s: bool, e: Arbnum.num, f: Arbnum.num) = s 74 val positivefloat = not o negativefloat 75 fun real_to_float0 (t, w) = 76 let 77 val tt = Arbnum.fromInt t 78 val ulp = Arbrat./ (Arbrat.two, 79 Arbrat.fromNat (pow2 (Arbnum.+ (int_max w, tt)))) 80 val d = pow2 (Arbnum.less1 tt) 81 val c = pow2 tt 82 fun exponent n = lg2 (Arbnum.div (n, d)) 83 fun fraction e n = Arbnum.- (Arbnum.div (n, pow2 (Arbnum.less1 e)), c) 84 in 85 fn r => 86 let 87 val s = is_negative_rat r 88 val n = nfloor (Arbrat./ (Arbrat.abs r, ulp)) 89 val e = exponent n 90 in 91 if e = Arbnum.zero 92 then (s, e, n) 93 else (s, e, fraction e n) 94 end 95 end 96 fun nextfloat (t, w) = 97 let 98 val mt = Arbnum.less1 (dimword t) 99 val mw = Arbnum.less2 (dimword w) 100 in 101 fn (s: bool, e, f) => 102 if e = Arbnum.zero andalso f = Arbnum.zero 103 then (s, e, Arbnum.one) 104 else if Arbnum.< (f, mt) 105 then (s, e, Arbnum.plus1 f) 106 else if Arbnum.< (e, mw) 107 then (s, Arbnum.plus1 e, Arbnum.zero) 108 else (s, e, f) 109 end 110in 111 datatype float = posInf | negInf | Float of bool * Arbnum.num * Arbnum.num 112 fun float_to_real (t, w) = 113 let 114 val i = Arbrat.fromNat (pow2 (int_max w)) 115 val j = Arbrat./ (Arbrat.two, i) 116 val d = Arbrat.fromNat (dimword t) 117 in 118 fn (s, e, f) => 119 let 120 val f' = Arbrat./ (Arbrat.fromNat f, d) 121 val r = 122 if e = Arbnum.zero 123 then Arbrat.* (j, f') 124 else let 125 val e2 = Arbrat./ (Arbrat.fromNat (pow2 e), i) 126 in 127 Arbrat.* (e2, Arbrat.+ (Arbrat.one, f')) 128 end 129 in 130 if s then Arbrat.negate r else r 131 end 132 end 133 fun real_to_float ((t, w), mode) = 134 let 135 val real_to_float0 = real_to_float0 (t, w) 136 val float_to_real = float_to_real (t, w) 137 val nextfloat = nextfloat (t, w) 138 val p = int_max w 139 val f = uint_max t 140 val m = Arbnum.less1 (uint_max w) 141 val n = Arbrat./ (Arbrat.fromNat (pow2 m), Arbrat.fromNat (pow2 p)) 142 val largest = Arbrat.* (n, frac t) 143 val threshold = Arbrat.* (n, frac (t + 1)) 144 val nlargest = Arbrat.negate largest 145 val nthreshold = Arbrat.negate threshold 146 val top = Float (false, m, f) 147 val bottom = Float (true, m, f) 148 in 149 if mode = binary_ieeeSyntax.roundTiesToEven_tm 150 then fn x => 151 let 152 val r = real_to_arbrat x 153 in 154 if Arbrat.<= (r, nthreshold) 155 then negInf 156 else if Arbrat.>= (r, threshold) 157 then posInf 158 else let 159 val fp = real_to_float0 r 160 val fpr = float_to_real fp 161 in 162 Float 163 (if fpr = r 164 then fp 165 else let 166 val nfp = nextfloat fp 167 val nfpr = float_to_real nfp 168 val fp_diff = diff (fpr, r) 169 val nfp_diff = diff (nfpr, r) 170 in 171 if fp_diff = nfp_diff 172 then if evenfloat fp 173 then fp 174 else nfp 175 else if Arbrat.< (fp_diff, nfp_diff) 176 then fp 177 else nfp 178 end) 179 end 180 end 181 else if mode = binary_ieeeSyntax.roundTowardPositive_tm 182 then fn x => 183 let 184 val r = real_to_arbrat x 185 in 186 if Arbrat.< (r, nlargest) 187 then bottom 188 else if Arbrat.> (r, largest) 189 then posInf 190 else let 191 val fp = real_to_float0 r 192 in 193 if float_to_real fp = r orelse negativefloat fp 194 then Float fp 195 else Float (nextfloat fp) 196 end 197 end 198 else if mode = binary_ieeeSyntax.roundTowardNegative_tm 199 then fn x => 200 let 201 val r = real_to_arbrat x 202 in 203 if Arbrat.< (r, nlargest) 204 then negInf 205 else if Arbrat.> (r, largest) 206 then top 207 else let 208 val fp = real_to_float0 r 209 in 210 if float_to_real fp = r orelse positivefloat fp 211 then Float fp 212 else Float (nextfloat fp) 213 end 214 end 215 else if mode = binary_ieeeSyntax.roundTowardZero_tm 216 then fn x => 217 let 218 val r = real_to_arbrat x 219 in 220 if Arbrat.< (r, nlargest) 221 then bottom 222 else if Arbrat.> (r, largest) 223 then top 224 else Float (real_to_float0 r) 225 end 226 else raise ERR "real_to_float" "unknown mode" 227 end 228end 229 230(* ------------------------------------------------------------------------ 231 REAL_REDUCE_CONV - based on realSimps.real_compset 232 ULP_CONV - evaluates ground ``ULP (n2w a, (:n))`` 233 largest_CONV - evaluates ground ``largest (:m # n)`` 234 threshold_CONV - evaluates ground ``threshold (:m # n)`` 235 float_value_CONV - evaluates ground ``float_value f`` 236 ------------------------------------------------------------------------ *) 237 238val float_datatype_rwts = 239 #rewrs (TypeBase.simpls_of ``:('a, 'b) float``) @ 240 #rewrs (TypeBase.simpls_of ``:flags``) @ 241 #rewrs (TypeBase.simpls_of ``:rounding``) 242 243val FLOAT_DATATYPE_CONV = 244 REWRITE_CONV (combinTheory.K_THM :: float_datatype_rwts) 245 246val REAL_REDUCE_CONV = computeLib.CBV_CONV (realSimps.real_compset()) 247 248fun memo_conv is_tm cnv0 s = 249 let 250 val rwts = ref ([]: thm list) 251 val cnv = ref (fn _: term => raise Conv.UNCHANGED) 252 val err = ERR (s ^ "_CONV") "" 253 in 254 fn tm => 255 if is_tm tm 256 then !cnv tm 257 handle Conv.UNCHANGED => 258 let 259 val thm = cnv0 tm 260 in 261 rwts := thm :: !rwts 262 ; cnv := PURE_ONCE_REWRITE_CONV (!rwts) 263 ; thm 264 end 265 else raise err 266 end 267 268local 269 val SZ_CONV = Conv.DEPTH_CONV wordsLib.SIZES_CONV THENC REAL_REDUCE_CONV 270 fun RWT_CONV rwt = Conv.REWR_CONV rwt THENC SZ_CONV 271in 272 val ULP_CONV = 273 memo_conv binary_ieeeSyntax.is_int_ULP 274 (Conv.REWR_CONV binary_ieeeTheory.ULP_def 275 THENC Conv.DEPTH_CONV wordsLib.word_EQ_CONV 276 THENC PURE_REWRITE_CONV [wordsTheory.w2n_n2w] 277 THENC SZ_CONV) 278 "ULP" 279 val largest_CONV = 280 memo_conv binary_ieeeSyntax.is_int_largest 281 (RWT_CONV binary_ieeeTheory.largest) "largest" 282 val threshold_CONV = 283 memo_conv binary_ieeeSyntax.is_int_threshold 284 (RWT_CONV binary_ieeeTheory.threshold) "threshold" 285end 286 287val float_value_CONV0 = 288 Conv.REWR_CONV binary_ieeeTheory.float_value_def 289 THENC Conv.RATOR_CONV FLOAT_DATATYPE_CONV 290 THENC wordsLib.WORD_CONV 291 THENC TRY_CONV 292 (Conv.RAND_CONV 293 (Conv.REWR_CONV binary_ieeeTheory.float_to_real_def 294 THENC FLOAT_DATATYPE_CONV 295 THENC wordsLib.WORD_CONV 296 THENC REAL_REDUCE_CONV)) 297 298val float_value_CONV = 299 Conv.CHANGED_CONV (PURE_ONCE_REWRITE_CONV [binary_ieeeTheory.float_values]) 300 ORELSEC float_value_CONV0 301 302(* ------------------------------------------------------------------------ 303 round_CONV - evaluates ground ``round mode r`` 304 float_round_CONV - evaluates ground ``float_round mode toneg r`` 305 ------------------------------------------------------------------------ *) 306 307local 308 val mk_real = realSyntax.term_of_int o Arbint.fromInt 309 val mk_tw = boolSyntax.mk_itself o pairSyntax.mk_prod 310 val mk_large = binary_ieeeSyntax.mk_largest o mk_tw 311 val mk_neg_large = realSyntax.mk_negated o mk_large 312 val mk_threshold = binary_ieeeSyntax.mk_threshold o mk_tw 313 val mk_neg_threshold = realSyntax.mk_negated o mk_threshold 314 val mk_ulp = binary_ieeeSyntax.mk_ulp o mk_tw 315 fun mk_ULP (e, t) = 316 binary_ieeeSyntax.mk_ULP (pairSyntax.mk_pair (e, boolSyntax.mk_itself t)) 317 fun mk_abs_diff (x, r) = realSyntax.mk_absval (realSyntax.mk_minus (x, r)) 318 fun mk_abs_diff_lt (x, r, u) = realSyntax.mk_less (mk_abs_diff (x, r), u) 319 val cond_mk_absval = fn true => realSyntax.mk_absval | _ => Lib.I 320 fun mk_abs_leq (b1, r, b2, x) = 321 realSyntax.mk_leq (cond_mk_absval b1 r, cond_mk_absval b2 x) 322 fun mk_abs_lt (r, x) = realSyntax.mk_less (cond_mk_absval true r, x) 323 fun mk_times2 r = realSyntax.mk_mult (mk_real 2, r) 324 fun mk_times4 r = realSyntax.mk_mult (mk_real 4, r) 325 fun ties_thm (rx2_thm, u_thm, y) = 326 boolSyntax.mk_imp 327 (boolSyntax.mk_eq (lhsc rx2_thm, lhsc u_thm), 328 boolSyntax.mk_neg 329 (wordsSyntax.mk_word_lsb 330 (binary_ieeeSyntax.mk_float_significand y))) 331 |> (Conv.LAND_CONV 332 (Conv.FORK_CONV (Conv.REWR_CONV rx2_thm, Conv.REWR_CONV u_thm)) 333 THENC EVAL) 334 |> Drule.EQT_ELIM 335 val twm_map = 336 ref (Redblackmap.mkDict 337 (Lib.pair_compare (Lib.pair_compare (Type.compare, Type.compare), 338 Term.compare)) 339 : ((hol_type * hol_type) * term, 340 (term -> float) * conv) Redblackmap.dict) 341 fun lookup (x as (tw as (t, w), mode)) = 342 case Redblackmap.peek (!twm_map, x) of 343 SOME y => y 344 | NONE => 345 let 346 val tn = fcpSyntax.dest_int_numeric_type t 347 val wn = fcpSyntax.dest_int_numeric_type w 348 val f = real_to_float ((tn, wn), mode) 349 val thm = if mode = binary_ieeeSyntax.roundTiesToEven_tm 350 then threshold_CONV (mk_threshold tw) 351 else largest_CONV (mk_large tw) 352 val y = (f, Conv.REWR_CONV thm) 353 val () = twm_map := Redblackmap.insert (!twm_map, x, y) 354 in 355 y 356 end 357 val toPosInf0 = 358 Drule.MATCH_MP binary_ieeeTheory.round_roundTiesToEven_plus_infinity 359 val toNegInf0 = 360 Drule.MATCH_MP binary_ieeeTheory.round_roundTiesToEven_minus_infinity 361 val toPosInf1 = 362 Drule.MATCH_MP binary_ieeeTheory.round_roundTowardPositive_plus_infinity 363 val toNegInf1 = 364 Drule.MATCH_MP binary_ieeeTheory.round_roundTowardNegative_minus_infinity 365 val toBot0 = 366 Drule.MATCH_MP binary_ieeeTheory.round_roundTowardZero_bottom 367 val toTop0 = 368 Drule.MATCH_MP binary_ieeeTheory.round_roundTowardZero_top 369 val err = ERR "round_CONV" 370 fun EQT_REDUCE cnv = Drule.EQT_ELIM o (cnv THENC REAL_REDUCE_CONV) 371 val EXPONENT_ULP_CONV = Conv.RAND_CONV FLOAT_DATATYPE_CONV THENC ULP_CONV 372 val ulp_conv = 373 Conv.LAND_CONV (Conv.REWR_CONV binary_ieeeTheory.ulp_def THENC ULP_CONV) 374 THENC REAL_REDUCE_CONV 375 val f_word_conv = Conv.LAND_CONV FLOAT_DATATYPE_CONV THENC wordsLib.WORD_CONV 376 val ties_to_even = 377 Drule.EQT_ELIM o 378 (Conv.FORK_CONV (Conv.FORK_CONV (f_word_conv, Conv.RAND_CONV f_word_conv), 379 REAL_REDUCE_CONV) 380 THENC REWRITE_CONV []) 381 val conj_assoc_rule = PURE_ONCE_REWRITE_RULE [GSYM CONJ_ASSOC] 382 fun ties_to_even_thm (y, r, x) = 383 let 384 val f = binary_ieeeSyntax.mk_float_significand y 385 val f0 = boolSyntax.mk_eq 386 (f, wordsSyntax.mk_n2w (``0n``, wordsSyntax.dim_of f)) 387 val e = binary_ieeeSyntax.mk_float_exponent y 388 val e0 = boolSyntax.mk_eq 389 (e, wordsSyntax.mk_n2w (``1n``, wordsSyntax.dim_of e)) 390 val e1 = boolSyntax.mk_neg e0 391 val rx = mk_abs_leq (true, r, true, x) 392 val c = boolSyntax.mk_conj (f0, e1) 393 in 394 mlibUseful.INL (ties_to_even (boolSyntax.mk_imp (c, rx))) 395 handle HOL_ERR {origin_function = "EQT_ELIM", ...} => 396 mlibUseful.INR 397 (conj_assoc_rule 398 (ties_to_even (boolSyntax.mk_conj (c, boolSyntax.mk_neg rx)))) 399 end 400 val lt_thm = 401 Drule.MATCH_MP (realLib.REAL_ARITH ``(a <= b = F) ==> b < a: real``) 402 val le_thm = 403 Drule.MATCH_MP (realLib.REAL_ARITH ``(a < b = F) ==> b <= a: real``) 404 fun mk_w (n, ty) = wordsSyntax.mk_n2w (numLib.mk_numeral n, ty) 405 fun float_of_triple ((t, w), (s, e, f)) = 406 binary_ieeeSyntax.mk_floating_point 407 (wordsSyntax.mk_wordii (if s then 1 else 0, 1), mk_w (e, w), mk_w (f, t)) 408 (* 409 fun EQ_ELIM thm = 410 mlibUseful.INL (Drule.EQT_ELIM thm) 411 handle HOL_ERR _ => mlibUseful.INR (Drule.EQF_ELIM thm) 412 *) 413in 414 exception PlusMinusZero of Thm.thm 415 fun round_CONV tm = 416 let 417 val (mode, x, t, w) = binary_ieeeSyntax.dest_round tm 418 val tw = (t, w) 419 val (r2f, cnv) = lookup (tw, mode) 420 in 421 (* 422 val Float (sef as (s, _, _)) = r2f x 423 val SOME l_thm = 424 Lib.total 425 (EQT_REDUCE (Conv.RAND_CONV cnv)) 426 (mk_abs_leq (true, x, false, mk_large tw)) 427 *) 428 case r2f x of 429 Float (sef as (s, _, _)) => 430 if mode = binary_ieeeSyntax.roundTiesToEven_tm 431 then let 432 val u_thm = 433 ulp_conv 434 (realSyntax.mk_less 435 (mk_ulp tw, 436 realSyntax.mk_mult 437 (``2r``, realSyntax.mk_absval x))) 438 val u_thm = 439 Drule.EQT_ELIM u_thm 440 handle HOL_ERR _ => raise PlusMinusZero (le_thm u_thm) 441 val t_thm = 442 (EQT_REDUCE (Conv.RAND_CONV cnv)) 443 (mk_abs_lt (x, mk_threshold tw)) 444 val y = float_of_triple (tw, sef) 445 val r_thm = 446 float_value_CONV (binary_ieeeSyntax.mk_float_value y) 447 val r = binary_ieeeSyntax.dest_float (rhsc r_thm) 448 val u = mk_ULP (binary_ieeeSyntax.mk_float_exponent y, t) 449 val U_thm = EXPONENT_ULP_CONV u 450 in 451 case ties_to_even_thm (y, r, x) of 452 mlibUseful.INL s_thm => 453 let 454 val rx2 = mk_times2 (mk_abs_diff (r, x)) 455 val rx2_thm = REAL_REDUCE_CONV rx2 456 val rx2_u_thm = 457 EQT_REDUCE 458 (Conv.LAND_CONV (Conv.REWR_CONV rx2_thm) 459 THENC Conv.RAND_CONV 460 (Conv.REWR_CONV U_thm)) 461 (realSyntax.mk_leq (rx2, u)) 462 val tie_thm = ties_thm (rx2_thm, U_thm, y) 463 val thm = 464 Drule.LIST_CONJ 465 [r_thm, s_thm, rx2_u_thm, tie_thm, 466 u_thm, t_thm] 467 in 468 MATCH_MP 469 binary_ieeeTheory.round_roundTiesToEven thm 470 end 471 | mlibUseful.INR s_thm => 472 let 473 val rx4 = mk_times4 (mk_abs_diff (r, x)) 474 val rx4_thm = REAL_REDUCE_CONV rx4 475 val rx4_u_thm = 476 EQT_REDUCE 477 (Conv.LAND_CONV (Conv.REWR_CONV rx4_thm) 478 THENC Conv.RAND_CONV 479 (Conv.REWR_CONV U_thm)) 480 (realSyntax.mk_leq (rx4, u)) 481 val thm = 482 Drule.LIST_CONJ 483 [r_thm, s_thm, rx4_u_thm, u_thm, t_thm] 484 in 485 MATCH_MP 486 binary_ieeeTheory.round_roundTiesToEven0 thm 487 end 488 end 489 else if mode = binary_ieeeSyntax.roundTowardPositive_tm 490 then raise err "roundTowardPositive: not implemented" 491 else if mode = binary_ieeeSyntax.roundTowardNegative_tm 492 then raise err "roundTowardNegative: not implemented" 493 else if mode = binary_ieeeSyntax.roundTowardZero_tm 494 then 495 case Lib.total 496 (EQT_REDUCE (Conv.RAND_CONV cnv)) 497 (mk_abs_leq (true, x, false, mk_large tw)) of 498 SOME l_thm => 499 let 500 val u_thm = 501 ulp_conv (mk_abs_leq (false, mk_ulp tw, true, x)) 502 val u_thm = 503 Drule.EQT_ELIM u_thm 504 handle HOL_ERR _ => 505 raise PlusMinusZero (lt_thm u_thm) 506 val y = float_of_triple (tw, sef) 507 val r_thm = 508 float_value_CONV 509 (binary_ieeeSyntax.mk_float_value y) 510 val r = binary_ieeeSyntax.dest_float (rhsc r_thm) 511 val u = 512 mk_ULP (binary_ieeeSyntax.mk_float_exponent y, t) 513 val d_thm = 514 EQT_REDUCE (Conv.RAND_CONV EXPONENT_ULP_CONV) 515 (mk_abs_diff_lt (r, x, u)) 516 val a_thm = EQT_REDUCE Conv.ALL_CONV 517 (mk_abs_leq (true, r, true, x)) 518 val thm = Drule.LIST_CONJ 519 [r_thm, d_thm, a_thm, u_thm, l_thm] 520 in 521 MATCH_MP binary_ieeeTheory.round_roundTowardZero thm 522 end 523 | NONE => 524 if s then 525 let 526 val lt = 527 realSyntax.mk_less (x, mk_neg_large tw) 528 val thm = 529 EQT_REDUCE 530 (Conv.RAND_CONV (Conv.RAND_CONV cnv)) lt 531 in 532 toBot0 thm 533 end 534 else let 535 val lt = realSyntax.mk_less (mk_large tw, x) 536 val thm = EQT_REDUCE (Conv.LAND_CONV cnv) lt 537 in 538 toTop0 thm 539 end 540 else raise err "unknown mode" 541 | posInf => 542 if mode = binary_ieeeSyntax.roundTiesToEven_tm 543 then let 544 val le = realSyntax.mk_leq (mk_threshold tw, x) 545 val thm = EQT_REDUCE (Conv.LAND_CONV cnv) le 546 in 547 toPosInf0 thm 548 end 549 else if mode = binary_ieeeSyntax.roundTowardPositive_tm 550 then let 551 val lt = realSyntax.mk_less (mk_large tw, x) 552 val thm = EQT_REDUCE (Conv.LAND_CONV cnv) lt 553 in 554 toPosInf1 thm 555 end 556 else raise err "+inf" 557 | negInf => 558 if mode = binary_ieeeSyntax.roundTiesToEven_tm 559 then let 560 val le = realSyntax.mk_leq (x, mk_neg_threshold tw) 561 val thm = 562 EQT_REDUCE (Conv.RAND_CONV (Conv.RAND_CONV cnv)) le 563 in 564 toNegInf0 thm 565 end 566 else if mode = binary_ieeeSyntax.roundTowardNegative_tm 567 then let 568 val lt = realSyntax.mk_less (x, mk_neg_large tw) 569 val thm = 570 EQT_REDUCE (Conv.RAND_CONV (Conv.RAND_CONV cnv)) lt 571 in 572 toNegInf1 thm 573 end 574 else raise err "+inf" 575 end 576end 577 578local 579 datatype round_result = 580 NotZero of Thm.thm 581 | Limit of Thm.thm 582 | Zero of Thm.thm 583 fun mk_neq_zero tm ty = 584 boolSyntax.mk_neg 585 (boolSyntax.mk_eq (tm, wordsSyntax.mk_n2w (numSyntax.zero_tm, ty))) 586 fun try_round tm = 587 let 588 val thm = round_CONV tm 589 val y = rhsc thm 590 in 591 if binary_ieeeSyntax.is_float_plus_infinity y 592 then Limit (Drule.MATCH_MP 593 binary_ieeeTheory.float_round_plus_infinity thm) 594 else if binary_ieeeSyntax.is_float_minus_infinity y 595 then Limit (Drule.MATCH_MP 596 binary_ieeeTheory.float_round_minus_infinity thm) 597 else if binary_ieeeSyntax.is_float_top y 598 then Limit (Drule.MATCH_MP binary_ieeeTheory.float_round_top thm) 599 else if binary_ieeeSyntax.is_float_bottom y 600 then Limit (Drule.MATCH_MP binary_ieeeTheory.float_round_bottom thm) 601 else NotZero thm 602 end 603 handle PlusMinusZero thm => Zero thm 604 val err = ERR "float_round_CONV" 605 val rule = REWRITE_RULE [binary_ieeeTheory.float_minus_zero, 606 binary_ieeeTheory.float_plus_zero_def] 607 val rule = rule ## rule 608 val toEven = rule (binary_ieeeTheory.round_roundTiesToEven_is_minus_zero, 609 binary_ieeeTheory.round_roundTiesToEven_is_plus_zero) 610 val toZero = rule (binary_ieeeTheory.round_roundTowardZero_is_minus_zero, 611 binary_ieeeTheory.round_roundTowardZero_is_plus_zero) 612 fun rnd_zero_thms toneg mode = 613 (if toneg = boolSyntax.T then fst 614 else if toneg = boolSyntax.F then snd 615 else raise err "+/- 0") 616 (if mode = binary_ieeeSyntax.roundTiesToEven_tm 617 then toEven 618 else if mode = binary_ieeeSyntax.roundTowardPositive_tm 619 then raise err "roundTowardPositive: not implemented" 620 else if mode = binary_ieeeSyntax.roundTowardNegative_tm 621 then raise err "roundTowardNegative: not implemented" 622 else if mode = binary_ieeeSyntax.roundTowardZero_tm 623 then toZero 624 else raise err "unknown mode") 625in 626 fun float_round_CONV tm = 627 let 628 val (mode, toneg, x, t, w) = binary_ieeeSyntax.dest_float_round tm 629 in 630 case try_round (binary_ieeeSyntax.mk_round (mode, x, t, w)) of 631 NotZero rnd_thm => 632 let 633 val (_, e, f) = 634 binary_ieeeSyntax.dest_floating_point (rhsc rnd_thm) 635 val not_zero_tm = 636 boolSyntax.mk_disj (mk_neq_zero e w, mk_neq_zero f t) 637 val not_zero_thm = 638 Drule.EQT_ELIM (wordsLib.WORD_EVAL_CONV not_zero_tm) 639 in 640 Drule.MATCH_MP binary_ieeeTheory.float_round_non_zero 641 (Thm.CONJ rnd_thm not_zero_thm) 642 |> Thm.SPEC toneg 643 end 644 | Limit thm => Thm.SPEC toneg thm 645 | Zero thm => Drule.MATCH_MP (rnd_zero_thms toneg mode) thm 646 end 647end 648 649local 650 val cnv = round_CONV 651in 652 fun round_CONV tm = 653 cnv tm handle PlusMinusZero _ => raise ERR "round_CONV" "+/- 0" 654end 655 656(* ------------------------------------------------------------------------- 657 float_round_with_flags_CONV 658 ------------------------------------------------------------------------- *) 659 660local 661 val conv = 662 REAL_REDUCE_CONV 663 THENC FLOAT_DATATYPE_CONV 664 THENC REWRITE_CONV [binary_ieeeTheory.float_components] 665 THENC wordsLib.WORD_EVAL_CONV 666 THENC float_round_CONV 667 fun round_conv tm = 668 (if binary_ieeeSyntax.is_float_round tm then conv else NO_CONV) tm 669in 670 val float_round_with_flags_CONV = 671 Conv.REWR_CONV binary_ieeeTheory.float_round_with_flags_def 672 THENC Conv.RAND_CONV REAL_REDUCE_CONV 673 THENC Conv.DEPTH_CONV round_conv 674end 675 676(* ------------------------------------------------------------------------ 677 infinity_intro_CONV - if possible, convert ground FP term to 678 float_plus_infinity or float_minus_infinity 679 680 For example: 681 682 infinity_intro_CONV 683 ``<|Sign := 0w; Exponent := 31w; Significand := 0w|> : (10, 5) float`` 684 685 gives 686 687 |- <|Sign := 0w; Exponent := 31w; Significand := 0w|> = 688 float_plus_infinity (:10 # 5) 689 690 ------------------------------------------------------------------------ *) 691 692local 693 fun pow2exp i = Arbnum.pow (Arbnum.two, Arbnum.fromInt i) 694 fun mod2exp (w, i) = Arbnum.mod (w, pow2exp i) 695 fun eq_thm (n, i, v) = 696 Drule.EQT_ELIM 697 (wordsLib.WORD_EVAL_CONV 698 (boolSyntax.mk_eq (wordsSyntax.mk_wordi (n, i), v))) 699 val uint_max = wordsSyntax.mk_word_T o fcpSyntax.mk_int_numeric_type 700 val plus = GSYM binary_ieeeTheory.float_plus_infinity_def 701 val minus = GSYM binary_ieeeTheory.float_minus_infinity 702in 703 fun infinity_intro_CONV tm = 704 let 705 val ((t, w), (s, e, f)) = binary_ieeeSyntax.triple_of_float tm 706 in 707 if mod2exp (f, t) = Arbnum.zero andalso 708 mod2exp (e, w) = Arbnum.less1 (pow2exp w) 709 then let 710 val thm = if s then minus else plus 711 val e_thm = eq_thm (e, w, uint_max w) 712 val f_thm = eq_thm (f, t, wordsSyntax.mk_wordii (0, t)) 713 in 714 (Conv.RAND_CONV 715 (Conv.FORK_CONV 716 (Conv.RAND_CONV (Conv.REWR_CONV e_thm), 717 Conv.RATOR_CONV 718 (Conv.RAND_CONV 719 (Conv.RAND_CONV (Conv.REWR_CONV f_thm))))) 720 THENC Conv.REWR_CONV thm) tm 721 end 722 else raise ERR "emax_intro_CONV" "not emax term" 723 end 724end 725 726(* ------------------------------------------------------------------------ 727 float_add_CONV 728 float_sub_CONV 729 float_mul_CONV 730 float_div_CONV 731 732 For example, float_add_CONV converts ground 733 734 ``float_add mode a b`` 735 736 to one of 737 738 ``float_round mode toneg (ra + rb)`` 739 ``float_some_qnan (:10 # 5)`` 740 ``float_plus_infinity (:10 # 5)`` 741 ``float_minus_infinity (:10 # 5)`` 742 743 The latter two cases only apply when either ``a`` or ``b`` is the same 744 infinity term. Missing cases are handled by adding further rewrites to 745 the_compset. 746 ------------------------------------------------------------------------ *) 747 748local 749 val rwt = boolTheory.IMP_CLAUSES |> Drule.SPEC_ALL |> Drule.CONJUNCTS |> hd 750 fun is_nan_thm thm = 751 case Lib.total boolSyntax.dest_eq (Thm.concl thm) of 752 SOME (_, r) => r = binary_ieeeSyntax.nan_tm 753 | _ => false 754 fun float_x_CONV (name, compute, dest, nan, float_finite, 755 plus_infinity_finite, minus_infinity_finite, 756 finite_plus_infinity, finite_minus_infinity) = 757 let 758 val err = ERR ("float_" ^ name ^ "_CONV") "" 759 fun float_nan (mode, x, y, thm) = 760 nan 761 |> Drule.ISPECL [mode, x, y] 762 |> Conv.CONV_RULE 763 (Conv.LAND_CONV (REWRITE_CONV [thm]) THENC Conv.REWR_CONV rwt) 764 val cnv = PURE_ONCE_REWRITE_CONV [compute] 765 in 766 fn tm => 767 cnv tm 768 handle Conv.UNCHANGED => 769 let 770 val (mode, x, y) = dest tm 771 fun mtch_spec thm1 thm2 = 772 if is_nan_thm thm2 773 then float_nan (mode, x, y, thm2) 774 else (Thm.SPEC mode (Drule.MATCH_MP thm1 thm2) 775 handle HOL_ERR _ => raise err) 776 val vx = binary_ieeeSyntax.mk_float_value x 777 val vy = binary_ieeeSyntax.mk_float_value y 778 in 779 if binary_ieeeSyntax.is_float_plus_infinity x 780 then mtch_spec plus_infinity_finite (float_value_CONV vy) 781 else if binary_ieeeSyntax.is_float_minus_infinity x 782 then mtch_spec minus_infinity_finite (float_value_CONV vy) 783 else if binary_ieeeSyntax.is_float_plus_infinity y 784 then mtch_spec finite_plus_infinity (float_value_CONV vx) 785 else if binary_ieeeSyntax.is_float_minus_infinity y 786 then mtch_spec finite_minus_infinity (float_value_CONV vx) 787 else 788 let 789 val vx_thm = float_value_CONV vx 790 in 791 if rhsc vx_thm = binary_ieeeSyntax.nan_tm 792 then float_nan (mode, x, y, vx_thm) 793 else let 794 val vy_thm = float_value_CONV vy 795 in 796 if rhsc vy_thm = binary_ieeeSyntax.nan_tm 797 then float_nan (mode, x, y, vy_thm) 798 else 799 mtch_spec float_finite (Thm.CONJ vx_thm vy_thm) 800 end 801 end 802 end 803 end 804in 805 val float_add_CONV = 806 float_x_CONV 807 ("add", 808 binary_ieeeTheory.float_add_compute, 809 binary_ieeeSyntax.dest_float_add, 810 binary_ieeeTheory.float_add_nan, 811 binary_ieeeTheory.float_add_finite, 812 binary_ieeeTheory.float_add_plus_infinity_finite, 813 binary_ieeeTheory.float_add_minus_infinity_finite, 814 binary_ieeeTheory.float_add_finite_plus_infinity, 815 binary_ieeeTheory.float_add_finite_minus_infinity) 816 val float_sub_CONV = 817 float_x_CONV 818 ("sub", 819 binary_ieeeTheory.float_sub_compute, 820 binary_ieeeSyntax.dest_float_sub, 821 binary_ieeeTheory.float_sub_nan, 822 binary_ieeeTheory.float_sub_finite, 823 binary_ieeeTheory.float_sub_plus_infinity_finite, 824 binary_ieeeTheory.float_sub_minus_infinity_finite, 825 binary_ieeeTheory.float_sub_finite_plus_infinity, 826 binary_ieeeTheory.float_sub_finite_minus_infinity) 827 val float_mul_CONV = 828 float_x_CONV 829 ("mul", 830 binary_ieeeTheory.float_mul_compute, 831 binary_ieeeSyntax.dest_float_mul, 832 binary_ieeeTheory.float_mul_nan, 833 binary_ieeeTheory.float_mul_finite, 834 binary_ieeeTheory.float_mul_plus_infinity_finite, 835 binary_ieeeTheory.float_mul_minus_infinity_finite, 836 binary_ieeeTheory.float_mul_finite_plus_infinity, 837 binary_ieeeTheory.float_mul_finite_minus_infinity) 838 val float_div_CONV = 839 float_x_CONV 840 ("div", 841 binary_ieeeTheory.float_div_compute, 842 binary_ieeeSyntax.dest_float_div, 843 binary_ieeeTheory.float_div_nan, 844 binary_ieeeTheory.float_div_finite, 845 binary_ieeeTheory.float_div_plus_infinity_finite, 846 binary_ieeeTheory.float_div_minus_infinity_finite, 847 binary_ieeeTheory.float_div_finite_plus_infinity, 848 binary_ieeeTheory.float_div_finite_minus_infinity) 849end 850 851(* ------------------------------------------------------------------------ 852 float_equal_CONV 853 float_less_than_CONV 854 float_less_equal_CONV 855 float_greater_than_CONV 856 float_greater_equal_CONV 857 ------------------------------------------------------------------------ *) 858 859local 860 val cmp = realSimps.real_compset () 861 val () = computeLib.add_thms 862 ([pairTheory.pair_CASE_def, 863 pairTheory.FST, pairTheory.SND] @ 864 #rewrs (TypeBase.simpls_of ``:float_value``)) cmp 865 val float_compare_CONV = 866 Conv.REWR_CONV binary_ieeeTheory.float_compare_def 867 THENC Conv.LAND_CONV (Conv.BINOP_CONV float_value_CONV) 868 THENC computeLib.CBV_CONV cmp 869 val FLOAT_COMPARE_CONV = 870 REWRITE_CONV (#rewrs (TypeBase.simpls_of ``:float_compare``)) 871 val cnv1 = Conv.LAND_CONV float_compare_CONV THENC FLOAT_COMPARE_CONV 872 val cnv2 = 873 Conv.RATOR_CONV 874 (Conv.RATOR_CONV 875 (Conv.RATOR_CONV 876 (Conv.RATOR_CONV 877 (Conv.RAND_CONV float_compare_CONV)))) 878 THENC FLOAT_COMPARE_CONV 879in 880 val compare_CONV = float_compare_CONV 881 val equal_CONV = 882 Conv.REWR_CONV binary_ieeeTheory.float_equal_def THENC cnv1 883 val less_than_CONV = 884 Conv.REWR_CONV binary_ieeeTheory.float_less_than_def THENC cnv1 885 val less_equal_CONV = 886 Conv.REWR_CONV binary_ieeeTheory.float_less_equal_def THENC cnv2 887 val greater_than_CONV = 888 Conv.REWR_CONV binary_ieeeTheory.float_greater_than_def THENC cnv1 889 val greater_equal_CONV = 890 Conv.REWR_CONV binary_ieeeTheory.float_greater_equal_def THENC cnv2 891end 892 893(* ------------------------------------------------------------------------ 894 Add rewrites and conversions to compsets 895 ------------------------------------------------------------------------ *) 896 897(* Evaluation conversions *) 898 899fun round_after cnv = cnv THENC TRY_CONV float_round_with_flags_CONV 900 901val add_CONV = round_after float_add_CONV 902val sub_CONV = round_after float_sub_CONV 903val mul_CONV = round_after float_mul_CONV 904val div_CONV = 905 round_after 906 (float_div_CONV THENC wordsLib.WORD_EVAL_CONV THENC REAL_REDUCE_CONV) 907 908(* the following could benefit from a more efficient LCF custom conversion *) 909 910val sqrt_CONV = 911 round_after (Conv.REWR_CONV binary_ieeeTheory.float_sqrt_def THENC EVAL) 912 913val mul_add_CONV = 914 round_after (Conv.REWR_CONV binary_ieeeTheory.float_mul_add_def THENC EVAL) 915 916val mul_sub_CONV = 917 round_after (Conv.REWR_CONV binary_ieeeTheory.float_mul_sub_def THENC EVAL) 918 919val ieee_rewrites = 920 let 921 open binary_ieeeTheory 922 val sr = SIMP_RULE (srw_ss()) 923 val sr0 = sr [] 924 val spc = Drule.GEN_ALL o sr0 o 925 Q.SPEC `<| Sign := s; Exponent := e; Significand := f |>` 926 in 927 [float_to_real, spc float_value_def, float_tests, ulp_def, 928 infinity_properties, some_nan_properties, float_infinity_negate_abs, 929 spc float_negate_def, spc float_abs_def, float_plus_zero_def, 930 sr0 float_top_def, float_plus_min_def, float_minus_min_def, 931 float_minus_zero, sr [float_top_def, float_negate_def] float_bottom_def, 932 float_components, float_round_to_integral_compute, float_to_int_def, 933 real_to_float_def, real_to_float_with_flags_def, float_is_signalling_def, 934 check_for_signalling_def, clear_flags_def, invalidop_flags_def, 935 dividezero_flags_def 936 ] @ 937 List.take (Drule.CONJUNCTS float_values, 3) @ float_datatype_rwts 938 end 939 940val float_Sign_fupd_tm = 941 Term.mk_thy_const 942 {Ty = ``:(word1 -> word1) -> ('t, 'w) float -> ('t, 'w) float``, 943 Thy = "binary_ieee", 944 Name = "float_Sign_fupd"} 945 946fun add_ieee_to_compset cmp = 947 let 948 open computeLib 949 in 950 add_thms ieee_rewrites cmp 951 ; List.app (fn a => add_conv a cmp) 952 [ 953 (float_Sign_fupd_tm, 2, infinity_intro_CONV), 954 (binary_ieeeSyntax.ULP_tm, 1, ULP_CONV), 955 (binary_ieeeSyntax.largest_tm, 1, largest_CONV), 956 (binary_ieeeSyntax.threshold_tm, 1, threshold_CONV), 957 (binary_ieeeSyntax.round_tm, 2, round_CONV), 958 (binary_ieeeSyntax.float_sqrt_tm, 2, sqrt_CONV), 959 (binary_ieeeSyntax.float_add_tm, 3, add_CONV), 960 (binary_ieeeSyntax.float_sub_tm, 3, sub_CONV), 961 (binary_ieeeSyntax.float_mul_tm, 3, mul_CONV), 962 (binary_ieeeSyntax.float_div_tm, 3, div_CONV), 963 (binary_ieeeSyntax.float_mul_add_tm, 4, mul_add_CONV), 964 (binary_ieeeSyntax.float_mul_sub_tm, 4, mul_sub_CONV), 965 (binary_ieeeSyntax.float_round_tm, 3, float_round_CONV), 966 (binary_ieeeSyntax.float_round_with_flags_tm, 3, 967 float_round_with_flags_CONV), 968 (binary_ieeeSyntax.float_compare_tm, 2, compare_CONV), 969 (binary_ieeeSyntax.float_equal_tm, 2, equal_CONV), 970 (binary_ieeeSyntax.float_less_than_tm, 2, less_than_CONV), 971 (binary_ieeeSyntax.float_less_equal_tm, 2, less_equal_CONV), 972 (binary_ieeeSyntax.float_greater_than_tm, 2, greater_than_CONV), 973 (binary_ieeeSyntax.float_greater_equal_tm, 2, greater_equal_CONV) 974 ] 975 end 976 977val () = add_ieee_to_compset computeLib.the_compset 978 979(* ------------------------------------------------------------------------ *) 980 981end 982