Lines Matching refs:fp
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)