1functor fpSyntax (val thy: string 2 val fp: string 3 val ty: Type.hol_type) :> fpSyntax = 4struct 5 open Abbrev HolKernel 6 open machine_ieeeTheory 7 8 val monop = HolKernel.syntax_fns1 thy 9 val binop = HolKernel.syntax_fns2 thy 10 11 val (float_to_fp_tm, mk_float_to_fp, dest_float_to_fp, is_float_to_fp) = 12 monop ("float_to_" ^ fp) 13 14 val (int_to_fp_tm, mk_int_to_fp, dest_int_to_fp, is_int_to_fp) = 15 binop ("int_to_" ^ fp) 16 17 val (real_to_fp_tm, mk_real_to_fp, dest_real_to_fp, is_real_to_fp) = 18 binop ("real_to_" ^ fp) 19 20 val (real_to_fp_with_flags_tm, mk_real_to_fp_with_flags, 21 dest_real_to_fp_with_flags, is_real_to_fp_with_flags) = 22 binop ("real_to_" ^ fp ^ "_with_flags") 23 24 fun pre s = fp ^ "_" ^ s 25 26 fun const name = Term.mk_thy_const {Ty = ty, Thy = thy, Name = pre name} 27 val monop = monop o pre 28 val binop = binop o pre 29 val triop = HolKernel.syntax_fns3 thy o pre 30 val quadop = HolKernel.syntax_fns4 thy o pre 31 32 val (fp_abs_tm, mk_fp_abs, dest_fp_abs, is_fp_abs) = monop "abs" 33 val (fp_add_tm, mk_fp_add, dest_fp_add, is_fp_add) = triop "add" 34 val (fp_add_with_flags_tm, mk_fp_add_with_flags, dest_fp_add_with_flags, 35 is_fp_add_with_flags) = triop "add_with_flags" 36 val fp_bottom_tm = const "bottom" 37 val (fp_div_tm, mk_fp_div, dest_fp_div, is_fp_div) = triop "div" 38 val (fp_div_with_flags_tm, mk_fp_div_with_flags, dest_fp_div_with_flags, 39 is_fp_div_with_flags) = triop "div_with_flags" 40 val (fp_compare_tm, mk_fp_compare, dest_fp_compare, is_fp_compare) = 41 binop "compare" 42 val (fp_equal_tm, mk_fp_equal, dest_fp_equal, is_fp_equal) = binop "equal" 43 val (fp_greaterEqual_tm, mk_fp_greaterEqual, dest_fp_greaterEqual, 44 is_fp_greaterEqual) = binop "greaterEqual" 45 val (fp_greaterThan_tm, mk_fp_greaterThan, dest_fp_greaterThan, 46 is_fp_greaterThan) = binop "greaterThan" 47 val (fp_isFinite_tm, mk_fp_isFinite, dest_fp_isFinite, is_fp_isFinite) = 48 monop "isFinite" 49 val (fp_isInfinite_tm, mk_fp_isInfinite, dest_fp_isInfinite, 50 is_fp_isInfinite) = monop "isInfinite" 51 val (fp_isIntegral_tm, mk_fp_isIntegral, dest_fp_isIntegral, 52 is_fp_isIntegral) = monop "isIntegral" 53 val (fp_isNan_tm, mk_fp_isNan, dest_fp_isNan, is_fp_isNan) = monop "isNan" 54 val (fp_isNormal_tm, mk_fp_isNormal, dest_fp_isNormal, is_fp_isNormal) = 55 monop "isNormal" 56 val (fp_isSignallingNan_tm, mk_fp_isSignallingNan, dest_fp_isSignallingNan, 57 is_fp_isSignallingNan) = monop "isSignallingNan" 58 val (fp_isSubnormal_tm, mk_fp_isSubnormal, dest_fp_isSubnormal, 59 is_fp_isSubnormal) = monop "isSubnormal" 60 val (fp_isZero_tm, mk_fp_isZero, dest_fp_isZero, is_fp_isZero) = 61 monop "isZero" 62 val (fp_lessEqual_tm, mk_fp_lessEqual, dest_fp_lessEqual, is_fp_lessEqual) = 63 binop "lessEqual" 64 val (fp_lessThan_tm, mk_fp_lessThan, dest_fp_lessThan, is_fp_lessThan) = 65 binop "lessThan" 66 val (fp_mul_tm, mk_fp_mul, dest_fp_mul, is_fp_mul) = triop "mul" 67 val (fp_mul_with_flags_tm, mk_fp_mul_with_flags, dest_fp_mul_with_flags, 68 is_fp_mul_with_flags) = triop "mul_with_flags" 69 val (fp_mul_add_tm, mk_fp_mul_add, dest_fp_mul_add, is_fp_mul_add) = 70 quadop "mul_add" 71 val (fp_mul_add_with_flags_tm, mk_fp_mul_add_with_flags, 72 dest_fp_mul_add_with_flags, is_fp_mul_add_with_flags) = 73 quadop "mul_add_with_flags" 74 val (fp_mul_sub_tm, mk_fp_mul_sub, dest_fp_mul_sub, is_fp_mul_sub) = 75 quadop "mul_sub" 76 val (fp_mul_sub_with_flags_tm, mk_fp_mul_sub_with_flags, 77 dest_fp_mul_sub_with_flags, is_fp_mul_sub_with_flags) = 78 quadop "mul_sub_with_flags" 79 val fp_neginf_tm = const "negInf" 80 val fp_negmin_tm = const "negMin" 81 val fp_negzero_tm = const "negZero" 82 val (fp_negate_tm, mk_fp_negate, dest_fp_negate, is_fp_negate) = 83 monop "negate" 84 val fp_posinf_tm = const "posInf" 85 val fp_posmin_tm = const "posMin" 86 val fp_poszero_tm = const "posZero" 87 val (fp_roundToIntegral_tm, mk_fp_roundToIntegral, dest_fp_roundToIntegral, 88 is_fp_roundToIntegral) = binop "roundToIntegral" 89 val (fp_sqrt_tm, mk_fp_sqrt, dest_fp_sqrt, is_fp_sqrt) = binop "sqrt" 90 val (fp_sqrt_with_flags_tm, mk_fp_sqrt_with_flags, dest_fp_sqrt_with_flags, 91 is_fp_sqrt_with_flags) = binop "sqrt_with_flags" 92 val (fp_sub_tm, mk_fp_sub, dest_fp_sub, is_fp_sub) = triop "sub" 93 val (fp_sub_with_flags_tm, mk_fp_sub_with_flags, dest_fp_sub_with_flags, 94 is_fp_sub_with_flags) = triop "sub_with_flags" 95 val (fp_to_float_tm, mk_fp_to_float, dest_fp_to_float, is_fp_to_float) = 96 monop "to_float" 97 val (fp_to_int_tm, mk_fp_to_int, dest_fp_to_int, is_fp_to_int) = 98 binop "to_int" 99 val (fp_to_real_tm, mk_fp_to_real, dest_fp_to_real, is_fp_to_real) = 100 monop "to_real" 101 val fp_top_tm = const "top" 102end 103