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