src/floating-point/machine_ieeeLib.sml

48    fun mk_fp_to_float fp fp_ty float_ty pre_k t t_ty w_ty =
50          val fp_to_float = fp ^ "_to_float"
67    fun mk_float_to_fp fp fp_ty float_ty t_ty w_ty =
69          val float_to_fp = "float_to_" ^ fp
79    fun mk_fp_to_real fp float_to_real fp_to_float fp_ty =
81          val fp_to_real = fp ^ "_to_real"
89    fun mk_fp_to_value fp float_value fp_to_float fp_ty =
91          val fp_to_value = fp ^ "_to_value"
99    fun mk_real_to_fp fp real_to_float float_to_fp fp_ty =
101          val real_to_fp = "real_to_" ^ fp
110    fun mk_real_to_fp_with_flags fp real_to_float_with_flags float_to_fp fp_ty =
112          val real_to_fp = "real_to_" ^ fp ^ "_with_flags"
123    fun mk_int_to_fp fp real_to_fp fp_ty =
127          val s = "int_to_" ^ fp
135    fun mk_fp_to_int fp fp_to_float fp_ty float_ty =
139          val s = fp ^ "_to_int"
281    fun encoding_thms (fp, fp_to_float_def, float_to_fp_def) =
286             Q.store_thm (fp ^ "_to_float_11",
293             Q.store_thm ("float_to_" ^ fp ^ "_11",
300             Q.store_thm ("float_to_" ^ fp ^ "_" ^ fp ^ "_to_float",
306             Q.store_thm (fp ^ "_to_float_float_to_" ^ fp,
313             Q.store_thm(fp ^ "_nchotomy",
320             Q.store_thm("float_" ^ fp ^ "_nchotomy",
369    fun fp_to_float_n2w (fp, t, w, fp_to_float_def) =
374          Q.store_thm (fp ^ "_to_float_n2w",
388    fun mk_machine (fp, t, w, a) =
390 (* e.g. val fp = "fp16" and t = 10 and w = 5 and a = SOME "half" *)
405           mk_fp_to_float fp fp_ty float_ty pre_k t t_ty w_ty
407           mk_float_to_fp fp fp_ty float_ty t_ty w_ty
409           mk_fp_to_real fp float_to_real fp_to_float fp_ty
411           mk_fp_to_value fp float_value fp_to_float fp_ty
413           mk_real_to_fp fp real_to_float float_to_fp fp_ty
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
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")
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")
434           lift1b (fp ^ "_isSignallingNan", "float_is_signalling")
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")
440            lift1b (fp ^ "_isSubnormal", "float_is_subnormal")
441         val fp_isfinite_def = lift1b (fp ^ "_isFinite", "float_is_finite")
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")
457           lift2 true (fp ^ "_add_with_flags", "float_add")
459           lift2 true (fp ^ "_sub_with_flags", "float_sub")
461           lift2 true (fp ^ "_mul_with_flags", "float_mul")
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")
469            lift2b (fp ^ "_greaterThan", "float_greater_than")
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")
475           lift3 true (fp ^ "_mul_add_with_flags", "float_mul_add")
477           lift3 true (fp ^ "_mul_sub_with_flags", "float_mul_sub")
481            encoding_thms (fp, fp_to_float_def, float_to_fp_def)
485         val fp_to_float_n2w = fp_to_float_n2w (fp, t, w, fp_to_float_def)