1structure machine_ieeeLib :> machine_ieeeLib = 2struct 3 4open HolKernel Parse boolLib bossLib 5open realSyntax intrealSyntax wordsLib binary_ieeeSyntax 6 7structure Parse = 8struct 9 open Parse 10 val (Type, Term) = parse_from_grammars binary_ieeeTheory.binary_ieee_grammars 11end 12open Parse 13 14val ERR = Feedback.mk_HOL_ERR "machine_ieeeLib" 15 16(* ------------------------------------------------------------------------ 17 mk_fp_encoding (prefix, significand_width, exponent_width) 18 19 Generate definitions & theorems for bit-vector encodings of fixed size FP 20 ------------------------------------------------------------------------ *) 21 22local 23 infix 0 == 24 infix 8 & 25 infixr 5 @@ o' ** 26 open binary_ieeeSyntax 27 val op & = Term.mk_comb 28 val op == = boolSyntax.mk_eq 29 val op @@ = wordsSyntax.mk_word_concat 30 val op o' = combinSyntax.mk_o 31 val op ** = pairSyntax.mk_prod 32 val i2t = numLib.term_of_int 33 val mk_w = wordsSyntax.mk_word_type 34 val real_ty = realSyntax.real_ty 35 val value_ty = binary_ieeeSyntax.float_value_ty 36 val mode = Term.mk_var ("mode", rounding_ty) 37 fun dest_float_ty ty = 38 case Lib.total Type.dest_type ty of 39 SOME ("float", [t, w]) => t ** w 40 | _ => raise ERR "dest_float_ty" "not a float type" 41 val get_function = 42 fst o boolSyntax.strip_comb o boolSyntax.lhs o 43 snd o boolSyntax.strip_forall o List.hd o boolSyntax.strip_conj o 44 Thm.concl 45 fun mk_I_hashhash f = 46 pairSyntax.mk_pair_map 47 (Term.inst [alpha |-> flags_ty] combinSyntax.I_tm, f) 48 fun mk_fp_to_float fp fp_ty float_ty pre_k t t_ty w_ty = 49 let 50 val fp_to_float = fp ^ "_to_float" 51 val fp_to_float_var = Term.mk_var (fp_to_float, fp_ty --> float_ty) 52 val w = Term.mk_var ("w", fp_ty) 53 val s = i2t pre_k 54 val float = 55 TypeBase.mk_record (float_ty, 56 [("Sign", wordsSyntax.mk_word_extract (s, s, w, ``:1``)), 57 ("Exponent", wordsSyntax.mk_word_extract 58 (i2t (pre_k - 1), i2t t, w, w_ty)), 59 ("Significand", wordsSyntax.mk_word_extract 60 (i2t (t - 1), i2t 0, w, t_ty))]) 61 val def = 62 Definition.new_definition (fp_to_float ^ "_def", 63 fp_to_float_var & w == float) 64 in 65 (get_function def, def) 66 end 67 fun mk_float_to_fp fp fp_ty float_ty t_ty w_ty = 68 let 69 val float_to_fp = "float_to_" ^ fp 70 val float_to_fp_var = Term.mk_var (float_to_fp, float_ty --> fp_ty) 71 val x = Term.mk_var ("x", float_ty) 72 val def = 73 Definition.new_definition (float_to_fp ^ "_def", 74 float_to_fp_var & x == 75 mk_float_sign x @@ mk_float_exponent x @@ mk_float_significand x) 76 in 77 (get_function def, def) 78 end 79 fun mk_fp_to_real fp float_to_real fp_to_float fp_ty = 80 let 81 val fp_to_real = fp ^ "_to_real" 82 val fp_to_real_var = Term.mk_var (fp_to_real, fp_ty --> real_ty) 83 val def = 84 Definition.new_definition (fp_to_real ^ "_def", 85 fp_to_real_var == float_to_real o' fp_to_float) 86 in 87 (get_function def, def) 88 end 89 fun mk_fp_to_value fp float_value fp_to_float fp_ty = 90 let 91 val fp_to_value = fp ^ "_to_value" 92 val fp_to_value_var = Term.mk_var (fp_to_value, fp_ty --> value_ty) 93 val def = 94 Definition.new_definition (fp_to_value ^ "_def", 95 fp_to_value_var == float_value o' fp_to_float) 96 in 97 (get_function def, def) 98 end 99 fun mk_real_to_fp fp real_to_float float_to_fp fp_ty = 100 let 101 val real_to_fp = "real_to_" ^ fp 102 val real_to_fp_var = 103 Term.mk_var (real_to_fp, rounding_ty --> real_ty --> fp_ty) 104 val def = 105 Definition.new_definition (real_to_fp ^ "_def", 106 real_to_fp_var & mode == float_to_fp o' real_to_float & mode) 107 in 108 (get_function def, def) 109 end 110 fun mk_real_to_fp_with_flags fp real_to_float_with_flags float_to_fp fp_ty = 111 let 112 val real_to_fp = "real_to_" ^ fp ^ "_with_flags" 113 val real_to_fp_var = 114 Term.mk_var 115 (real_to_fp, rounding_ty --> real_ty --> flags_ty ** fp_ty) 116 val def = 117 Definition.new_definition (real_to_fp ^ "_def", 118 real_to_fp_var & mode == 119 mk_I_hashhash float_to_fp o' real_to_float_with_flags & mode) 120 in 121 (get_function def, def) 122 end 123 fun mk_int_to_fp fp real_to_fp fp_ty = 124 let 125 val ty = rounding_ty --> intSyntax.int_ty --> fp_ty 126 val a = Term.mk_var ("a", intSyntax.int_ty) 127 val s = "int_to_" ^ fp 128 val v = Term.mk_var (s, ty) 129 in 130 Definition.new_definition (s ^ "_def", 131 v & mode & a == 132 real_to_fp & mode & (intrealSyntax.real_of_int_tm & a)) 133 end 134 val int_option_ty = optionSyntax.mk_option intSyntax.int_ty 135 fun mk_fp_to_int fp fp_to_float fp_ty float_ty = 136 let 137 val ty1 = rounding_ty --> fp_ty --> int_option_ty 138 val ty2 = rounding_ty --> float_ty --> int_option_ty 139 val s = fp ^ "_to_int" 140 val v = Term.mk_var (s, ty1) 141 val float_to_int = Term.mk_const ("float_to_int", ty2) 142 in 143 Definition.new_definition (s ^ "_def", 144 v & mode == (float_to_int & mode) o' fp_to_float) 145 end 146 fun lift1 float_to_fp fp_to_float fp_ty float_ty with_flags has_flags = 147 let 148 val ty1 = 149 if with_flags then fp_ty --> flags_ty ** fp_ty else fp_ty --> fp_ty 150 val ty2 = if has_flags then float_ty --> flags_ty ** float_ty 151 else float_ty --> float_ty 152 val snd_tm = Term.inst [alpha |-> flags_ty, beta |-> float_ty] 153 pairSyntax.snd_tm 154 in 155 fn (s, f) => 156 let 157 val (v, tm) = 158 (Term.mk_var (s, ty1), Term.mk_const (f, ty2)) 159 handle HOL_ERR _ => 160 (Term.mk_var (s, rounding_ty --> ty1) & mode, 161 Term.mk_const (f, rounding_ty --> ty2) & mode) 162 val def = 163 Definition.new_definition (s ^ "_def", 164 v == (if with_flags then 165 mk_I_hashhash float_to_fp o' tm o' fp_to_float 166 else if has_flags then 167 float_to_fp o' snd_tm o' tm o' fp_to_float 168 else float_to_fp o' tm o' fp_to_float)) 169 in 170 def 171 end 172 end 173 fun lift1b fp_to_float fp_ty float_ty = 174 let 175 val ty1 = fp_ty --> Type.bool 176 val ty2 = float_ty --> Type.bool 177 in 178 fn (s, f) => 179 let 180 val (v, tm) = (Term.mk_var (s, ty1), Term.mk_const (f, ty2)) 181 val def = 182 Definition.new_definition (s ^ "_def", 183 v == tm o' fp_to_float) 184 in 185 def 186 end 187 end 188 fun lift1c float_to_fp fp_ty float_ty = 189 let 190 val dim_ty = dest_float_ty float_ty 191 val ty = Type.mk_type ("itself", [dim_ty]) --> float_ty 192 val a = boolSyntax.mk_itself dim_ty 193 in 194 fn (s, f) => 195 let 196 val v = Term.mk_var (s, fp_ty) 197 val tm = Term.mk_const (f, ty) & a 198 val def = 199 Definition.new_definition (s ^ "_def", v == float_to_fp & tm) 200 in 201 def 202 end 203 end 204 fun lift2 float_to_fp fp_to_float fp_ty float_ty with_flags = 205 let 206 val ty1 = 207 if with_flags then 208 rounding_ty --> fp_ty --> fp_ty --> flags_ty ** fp_ty 209 else rounding_ty --> fp_ty --> fp_ty --> fp_ty 210 val ty2 = 211 rounding_ty --> float_ty --> float_ty --> flags_ty ** float_ty 212 val a = Term.mk_var ("a", fp_ty) 213 val b = Term.mk_var ("b", fp_ty) 214 val snd_tm = Term.inst [alpha |-> flags_ty, beta |-> float_ty] 215 pairSyntax.snd_tm 216 in 217 fn (s, f) => 218 let 219 val v = Term.mk_var (s, ty1) 220 val tm = Term.mk_const (f, ty2) 221 val x = tm & mode & (fp_to_float & a) & (fp_to_float & b) 222 val def = 223 Definition.new_definition (s ^ "_def", 224 v & mode & a & b == 225 (if with_flags then 226 mk_I_hashhash float_to_fp & x 227 else float_to_fp & (snd_tm & x))) 228 in 229 def 230 end 231 end 232 fun lift2b fp_to_float fp_ty float_ty res_ty = 233 let 234 val ty1 = fp_ty --> fp_ty --> res_ty 235 val ty2 = float_ty --> float_ty --> res_ty 236 val a = Term.mk_var ("a", fp_ty) 237 val b = Term.mk_var ("b", fp_ty) 238 in 239 fn (s, f) => 240 let 241 val v = Term.mk_var (s, ty1) 242 val tm = Term.mk_const (f, ty2) 243 val def = 244 Definition.new_definition (s ^ "_def", 245 v & a & b == 246 tm & (fp_to_float & a) & (fp_to_float & b)) 247 in 248 def 249 end 250 end 251 fun lift3 float_to_fp fp_to_float fp_ty float_ty with_flags = 252 let 253 val ty1 = 254 if with_flags then 255 rounding_ty --> fp_ty --> fp_ty --> fp_ty --> flags_ty ** fp_ty 256 else rounding_ty --> fp_ty --> fp_ty --> fp_ty --> fp_ty 257 val ty2 = rounding_ty --> float_ty --> float_ty --> float_ty --> 258 flags_ty ** float_ty 259 val a = Term.mk_var ("a", fp_ty) 260 val b = Term.mk_var ("b", fp_ty) 261 val c = Term.mk_var ("c", fp_ty) 262 val snd_tm = Term.inst [alpha |-> flags_ty, beta |-> float_ty] 263 pairSyntax.snd_tm 264 in 265 fn (s, f) => 266 let 267 val v = Term.mk_var (s, ty1) 268 val tm = Term.mk_const (f, ty2) 269 val x = tm & mode & (fp_to_float & a) & (fp_to_float & b) & 270 (fp_to_float & c) 271 val def = 272 Definition.new_definition (s ^ "_def", 273 v & mode & a & b & c == 274 (if with_flags then 275 mk_I_hashhash float_to_fp & x 276 else float_to_fp & (snd_tm & x))) 277 in 278 def 279 end 280 end 281 fun encoding_thms (fp, fp_to_float_def, float_to_fp_def) = 282 let 283 val fp_to_float = get_function fp_to_float_def 284 val float_to_fp = get_function float_to_fp_def 285 val fp_to_float_11 = 286 Q.store_thm (fp ^ "_to_float_11", 287 `!x y. (^fp_to_float x = ^fp_to_float y) = (x = y)`, 288 srw_tac [wordsLib.WORD_BIT_EQ_ss] 289 [fp_to_float_def, binary_ieeeTheory.float_component_equality] 290 >> decide_tac 291 ) 292 val float_to_fp_11 = 293 Q.store_thm ("float_to_" ^ fp ^ "_11", 294 `!x y. (^float_to_fp x = ^float_to_fp y) = (x = y)`, 295 srw_tac [wordsLib.WORD_BIT_EQ_ss] 296 [float_to_fp_def, binary_ieeeTheory.float_component_equality] 297 >> decide_tac 298 ) 299 val float_to_fp_fp_to_float = 300 Q.store_thm ("float_to_" ^ fp ^ "_" ^ fp ^ "_to_float", 301 `!x. ^float_to_fp (^fp_to_float x) = x`, 302 srw_tac [wordsLib.WORD_EXTRACT_ss] 303 [float_to_fp_def, fp_to_float_def] 304 ) 305 val fp_to_float_float_to_fp = 306 Q.store_thm (fp ^ "_to_float_float_to_" ^ fp, 307 `!x. ^fp_to_float (^float_to_fp x) = x`, 308 rw [float_to_fp_def, fp_to_float_def, 309 binary_ieeeTheory.float_component_equality] 310 >> simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 311 ) 312 val fp_nchotomy = 313 Q.store_thm(fp ^ "_nchotomy", 314 `!x. ?y. x = ^float_to_fp y`, 315 gen_tac 316 >> qexists_tac `^fp_to_float x` 317 >> rewrite_tac [float_to_fp_fp_to_float] 318 ) 319 val float_nchotomy = 320 Q.store_thm("float_" ^ fp ^ "_nchotomy", 321 `!x. ?y. x = ^fp_to_float y`, 322 gen_tac 323 >> qexists_tac `^float_to_fp x` 324 >> rewrite_tac [fp_to_float_float_to_fp] 325 ) 326 in 327 (fp_to_float_11, float_to_fp_11, 328 float_to_fp_fp_to_float, fp_to_float_float_to_fp, 329 fp_nchotomy, float_nchotomy) 330 end 331 fun all_combs [h1] [h2] = [[h1], [h2]] 332 | all_combs (h1 :: t1) (h2 :: t2) = 333 let 334 val r = all_combs t1 t2 335 in 336 List.map (fn x => h1 :: x) r @ 337 List.map (fn x => h2 :: x) r 338 end 339 | all_combs _ _ = raise ERR "all_combs" "" 340 val get_float_to_fp = 341 boolSyntax.rator o boolSyntax.rand o boolSyntax.lhs o snd o 342 boolSyntax.strip_forall o Thm.concl 343 fun try_f f x = Option.getOpt (Lib.total f x, x) 344 val opname = fst o Term.dest_const o get_function 345 fun xop vs fp_to_float_float_to_fp = 346 let 347 val float_to_fp = get_float_to_fp fp_to_float_float_to_fp 348 val (ty1, ty2) = Type.dom_rng (Term.type_of float_to_fp) 349 val ty2 = wordsSyntax.dest_word_type ty2 350 fun f1 v = boolSyntax.mk_icomb (float_to_fp, Term.mk_var (v, ty1)) 351 fun f2 v = wordsSyntax.mk_n2w (Term.mk_var (v, numSyntax.num), ty2) 352 val l = all_combs (List.map f1 vs) (List.map f2 vs) 353 in 354 fn op_def => 355 let 356 fun f l = 357 op_def 358 |> try_f (Thm.SPEC ``mode:rounding``) 359 |> (case l of [v] => Lib.C Thm.AP_THM v | _ => Drule.ISPECL l) 360 |> REWRITE_RULE [fp_to_float_float_to_fp, combinTheory.o_THM] 361 |> Drule.GEN_ALL 362 in 363 Theory.save_thm (opname op_def, LIST_CONJ (List.map f l)) 364 end 365 end 366 val monop = xop ["a"] 367 val binop = xop ["a", "b"] 368 val triop = xop ["a", "b", "c"] 369 fun fp_to_float_n2w (fp, t, w, fp_to_float_def) = 370 let 371 open bitTheory arithmeticTheory 372 val fp_to_float = get_function fp_to_float_def 373 in 374 Q.store_thm (fp ^ "_to_float_n2w", 375 `!n. 376 ^fp_to_float (n2w n) = 377 let (q, f) = DIVMOD_2EXP ^(i2t t) n in 378 let (s, e) = DIVMOD_2EXP ^(i2t w) q in 379 <| Sign := n2w (s MOD 2); 380 Exponent := n2w e; 381 Significand := n2w f |>`, 382 lrw [fp_to_float_def, BIT_def, BITS_THM, DIVMOD_2EXP_def, 383 DIV_2EXP_def, MOD_2EXP_def, wordsTheory.word_extract_n2w, 384 DIV_1, DIV2_def, ODD_MOD2_LEM, DIV_DIV_DIV_MULT] 385 ) 386 end 387in 388 fun mk_machine (fp, t, w, a) = 389 let 390(* e.g. val fp = "fp16" and t = 10 and w = 5 and a = SOME "half" *) 391 val pre_k = t + w 392 val k = pre_k + 1 393 val t_ty = fcpSyntax.mk_int_numeric_type t 394 val w_ty = fcpSyntax.mk_int_numeric_type w 395 val fp_ty = mk_w (fcpSyntax.mk_int_numeric_type k) 396 val float_ty = Type.mk_type ("float", [t_ty, w_ty]) 397 val float_to_real = Term.mk_const ("float_to_real", float_ty --> real_ty) 398 val float_value = Term.mk_const ("float_value", float_ty --> value_ty) 399 val real_to_float = 400 Term.mk_const ("real_to_float", rounding_ty --> real_ty --> float_ty) 401 val real_to_float_with_flags = 402 Term.mk_const ("real_to_float_with_flags", 403 rounding_ty --> real_ty --> flags_ty ** float_ty) 404 val (fp_to_float, fp_to_float_def) = 405 mk_fp_to_float fp fp_ty float_ty pre_k t t_ty w_ty 406 val (float_to_fp, float_to_fp_def) = 407 mk_float_to_fp fp fp_ty float_ty t_ty w_ty 408 val (fp_to_real, fp_to_real_def) = 409 mk_fp_to_real fp float_to_real fp_to_float fp_ty 410 val (fp_to_value, fp_to_value_def) = 411 mk_fp_to_value fp float_value fp_to_float fp_ty 412 val (real_to_fp, real_to_fp_def) = 413 mk_real_to_fp fp real_to_float float_to_fp fp_ty 414 val (real_to_fp_with_flags, real_to_fp_with_flags_def) = 415 mk_real_to_fp_with_flags fp real_to_float_with_flags float_to_fp fp_ty 416 val int_to_fp_def = mk_int_to_fp fp real_to_fp fp_ty 417 val lift1 = lift1 float_to_fp fp_to_float fp_ty float_ty 418 val lift1b = lift1b fp_to_float fp_ty float_ty 419 val lift1c = lift1c float_to_fp fp_ty float_ty 420 val lift2 = lift2 float_to_fp fp_to_float fp_ty float_ty 421 val lift2c = lift2b fp_to_float fp_ty float_ty float_compare_ty 422 val lift2b = lift2b fp_to_float fp_ty float_ty Type.bool 423 val lift3 = lift3 float_to_fp fp_to_float fp_ty float_ty 424 val fp_roundToIntegral_def = 425 lift1 false false (fp ^ "_roundToIntegral", "float_round_to_integral") 426 val fp_to_int_def = mk_fp_to_int fp fp_to_float fp_ty float_ty 427 val fp_sqrt_def = lift1 false true (fp ^ "_sqrt", "float_sqrt") 428 val fp_sqrt_with_flags_def = 429 lift1 true true (fp ^ "_sqrt_with_flags", "float_sqrt") 430 val fp_negate_def = lift1 false false (fp ^ "_negate", "float_negate") 431 val fp_abs_def = lift1 false false (fp ^ "_abs", "float_abs") 432 val fp_isnan_def = lift1b (fp ^ "_isNan", "float_is_nan") 433 val fp_issignallingnan_def = 434 lift1b (fp ^ "_isSignallingNan", "float_is_signalling") 435 val fp_isintegral_def = 436 lift1b (fp ^ "_isIntegral", "float_is_integral") 437 val fp_iszero_def = lift1b (fp ^ "_isZero", "float_is_zero") 438 val fp_isnormal_def = lift1b (fp ^ "_isNormal", "float_is_normal") 439 val fp_issubnormal_def = 440 lift1b (fp ^ "_isSubnormal", "float_is_subnormal") 441 val fp_isfinite_def = lift1b (fp ^ "_isFinite", "float_is_finite") 442 val fp_isinfinite_def = 443 lift1b (fp ^ "_isInfinite", "float_is_infinite") 444 val fp_posinf_def = lift1c (fp ^ "_posInf", "float_plus_infinity") 445 val fp_neginf_def = lift1c (fp ^ "_negInf", "float_minus_infinity") 446 val fp_poszero_def = lift1c (fp ^ "_posZero", "float_plus_zero") 447 val fp_negzero_def = lift1c (fp ^ "_negZero", "float_minus_zero") 448 val fp_minpos_def = lift1c (fp ^ "_posMin", "float_plus_min") 449 val fp_minneg_def = lift1c (fp ^ "_negMin", "float_minus_min") 450 val fp_top_def = lift1c (fp ^ "_top", "float_top") 451 val fp_bottom_def = lift1c (fp ^ "_bottom", "float_bottom") 452 val fp_add_def = lift2 false (fp ^ "_add", "float_add") 453 val fp_sub_def = lift2 false (fp ^ "_sub", "float_sub") 454 val fp_mul_def = lift2 false (fp ^ "_mul", "float_mul") 455 val fp_div_def = lift2 false (fp ^ "_div", "float_div") 456 val fp_add_with_flags_def = 457 lift2 true (fp ^ "_add_with_flags", "float_add") 458 val fp_sub_with_flags_def = 459 lift2 true (fp ^ "_sub_with_flags", "float_sub") 460 val fp_mul_with_flags_def = 461 lift2 true (fp ^ "_mul_with_flags", "float_mul") 462 val fp_div_with_flags_def = 463 lift2 true (fp ^ "_div_with_flags", "float_div") 464 val fp_compare_def = lift2c (fp ^ "_compare", "float_compare") 465 val fp_equal_def = lift2b (fp ^ "_equal", "float_equal") 466 val fp_lessthan_def = lift2b (fp ^ "_lessThan", "float_less_than") 467 val fp_lessequal_def = lift2b (fp ^ "_lessEqual", "float_less_equal") 468 val fp_greaterthan_def = 469 lift2b (fp ^ "_greaterThan", "float_greater_than") 470 val fp_greaterequal_def = 471 lift2b (fp ^ "_greaterEqual", "float_greater_equal") 472 val fp_mul_add_def = lift3 false (fp ^ "_mul_add", "float_mul_add") 473 val fp_mul_sub_def = lift3 false (fp ^ "_mul_sub", "float_mul_sub") 474 val fp_mul_add_with_flags_def = 475 lift3 true (fp ^ "_mul_add_with_flags", "float_mul_add") 476 val fp_mul_sub_with_flags_def = 477 lift3 true (fp ^ "_mul_sub_with_flags", "float_mul_sub") 478 val (fp_to_float_11, float_to_fp_11, 479 float_to_fp_fp_to_float, fp_to_float_float_to_fp, 480 fp_nchotomy, float_nchotomy) = 481 encoding_thms (fp, fp_to_float_def, float_to_fp_def) 482 val monop = monop fp_to_float_float_to_fp 483 val binop = binop fp_to_float_float_to_fp 484 val triop = triop fp_to_float_float_to_fp 485 val fp_to_float_n2w = fp_to_float_n2w (fp, t, w, fp_to_float_def) 486 in 487 case a of 488 SOME name => Parse.type_abbrev (name, float_ty) 489 | NONE => () 490 ; [monop fp_sqrt_def] @ 491 List.map binop 492 [fp_add_def, fp_sub_def, fp_mul_def, fp_div_def, fp_compare_def, 493 fp_equal_def, fp_lessthan_def, fp_lessequal_def, 494 fp_greaterthan_def, fp_greaterequal_def] @ 495 [fp_to_float_float_to_fp, fp_to_float_n2w, real_to_fp_def, 496 real_to_fp_with_flags_def, int_to_fp_def, fp_posinf_def, fp_neginf_def, 497 fp_poszero_def, fp_negzero_def, fp_minpos_def, fp_minneg_def, 498 fp_top_def, fp_bottom_def, float_to_fp_fp_to_float, 499 fp_to_float_float_to_fp] @ 500 List.map monop 501 [fp_to_real_def, fp_to_value_def, fp_to_int_def, fp_abs_def, 502 fp_negate_def, fp_isnan_def, fp_issignallingnan_def, 503 fp_isintegral_def, fp_iszero_def, fp_isnormal_def, 504 fp_issubnormal_def, fp_isfinite_def, fp_isinfinite_def, 505 fp_roundToIntegral_def, fp_sqrt_with_flags_def] @ 506 List.map binop 507 [fp_add_with_flags_def, fp_sub_with_flags_def, fp_mul_with_flags_def, 508 fp_div_with_flags_def] @ 509 List.map triop 510 [fp_mul_add_def, fp_mul_sub_def, fp_mul_add_with_flags_def, 511 fp_mul_sub_with_flags_def] 512 end 513end 514 515fun mk_fp_encoding (x as (_, y, _, _)) = 516 let 517 val mtch = DB.match [Theory.current_theory()] o Thm.concl 518 fun get_thm_name thm = 519 case mtch thm of 520 [((_, name), _)] => (thm, name) 521 | _ => raise Feedback.mk_HOL_ERR "machine_ieee" "get_thm_name" "" 522 val l = 523 (List.map get_thm_name o 524 (if y = 52 then (* native *) fn l => List.drop (l, 11) else Lib.I) o 525 mk_machine) x 526 val (thms, names) = ListPair.unzip l 527 in 528 computeLib.add_persistent_funs names; thms 529 end 530 531end 532