1open HolKernel Parse boolLib bossLib
2open machine_ieeeLib;
3
4val () = new_theory "machine_ieee";
5
6(* ------------------------------------------------------------------------
7   Bit-vector Encodings
8   ------------------------------------------------------------------------ *)
9
10(* 16-bit, 32-bit and 64-bit encodings *)
11
12val thms = (List.concat o List.map machine_ieeeLib.mk_fp_encoding)
13   [("fp16", 10, 5, SOME "half"),
14    ("fp32", 23, 8, SOME "single"),
15    ("fp64", 52, 11, SOME "double")];
16
17(* ------------------------------------------------------------------------
18   Encoding conversions
19   ------------------------------------------------------------------------ *)
20
21val convert_def = Define`
22  convert (to_float: 'a word -> ('b, 'c) float)
23          (from_float: ('d, 'e) float -> 'f word) from_real_with_flags
24          (m: rounding) w =
25  let f = to_float w in
26  case float_value f of
27     Float r => from_real_with_flags m r
28   | NaN => (check_for_signalling [f], from_float (@fp. float_is_nan fp))
29   | Infinity =>
30       (clear_flags,
31        from_float (if f.Sign = 0w then
32                      float_plus_infinity (:'d # 'e)
33                    else
34                      float_minus_infinity (:'d # 'e)))`
35
36(* These can only set InvalidOp *)
37
38val fp16_to_fp32_with_flags_def = Define`
39  fp16_to_fp32_with_flags =
40  convert fp16_to_float float_to_fp32 real_to_fp32_with_flags roundTiesToEven`
41
42val fp16_to_fp64_with_flags_def = Define`
43  fp16_to_fp64_with_flags =
44  convert fp16_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven`
45
46val fp32_to_fp64_with_flags_def = Define`
47  fp32_to_fp64_with_flags =
48  convert fp32_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven`
49
50(* These can set InvalidOp, Overflow, Precision and Underflow_* *)
51
52val fp64_to_fp32_with_flags_def = Define`
53  fp64_to_fp32_with_flags =
54  convert fp64_to_float float_to_fp32 real_to_fp32_with_flags`
55
56val fp64_to_fp16_with_flags_def = Define`
57  fp64_to_fp16_with_flags =
58  convert fp64_to_float float_to_fp16 real_to_fp16_with_flags`
59
60val fp32_to_fp16_with_flags_def = Define`
61  fp32_to_fp16_with_flags =
62  convert fp32_to_float float_to_fp16 real_to_fp16_with_flags`
63
64(* Versions without flags *)
65
66val fp16_to_fp32_def = Define `fp16_to_fp32 = SND o fp16_to_fp32_with_flags`
67val fp16_to_fp64_def = Define `fp16_to_fp64 = SND o fp16_to_fp64_with_flags`
68val fp32_to_fp64_def = Define `fp32_to_fp64 = SND o fp32_to_fp64_with_flags`
69
70val fp64_to_fp32_def = Define `fp64_to_fp32 m = SND o fp64_to_fp32_with_flags m`
71val fp64_to_fp16_def = Define `fp64_to_fp16 m = SND o fp64_to_fp16_with_flags m`
72val fp32_to_fp16_def = Define `fp32_to_fp16 m = SND o fp32_to_fp16_with_flags m`
73
74(* ------------------------------------------------------------------------
75   Support 64-bit native evaluation
76   (Controlled by the trace "native IEEE". Off by default.)
77   ------------------------------------------------------------------------ *)
78
79val () = Theory.quote_adjoin_to_theory
80`val sqrt_CONV: Conv.conv ref
81val add_CONV: Conv.conv ref
82val sub_CONV: Conv.conv ref
83val mul_CONV: Conv.conv ref
84val div_CONV: Conv.conv ref
85val compare_CONV: Conv.conv ref
86val eq_CONV: Conv.conv ref
87val lt_CONV: Conv.conv ref
88val le_CONV: Conv.conv ref
89val gt_CONV: Conv.conv ref
90val ge_CONV: Conv.conv ref`
91`val native_eval = ref false(* off by default *)
92val () = Feedback.register_btrace ("native IEEE", native_eval)
93val sqrt_CONV = ref Conv.NO_CONV
94val add_CONV = ref Conv.NO_CONV
95val sub_CONV = ref Conv.NO_CONV
96val mul_CONV = ref Conv.NO_CONV
97val div_CONV = ref Conv.NO_CONV
98val compare_CONV = ref Conv.NO_CONV
99val eq_CONV = ref Conv.NO_CONV
100val lt_CONV = ref Conv.NO_CONV
101val le_CONV = ref Conv.NO_CONV
102val gt_CONV = ref Conv.NO_CONV
103val ge_CONV = ref Conv.NO_CONV
104fun native cnv1 s =
105  let
106    val cnv2 =
107      Conv.QCHANGED_CONV
108        (Rewrite.PURE_REWRITE_CONV [DB.fetch "machine_ieee" ("fp64_" ^  s)])
109  in
110    fn tm => (if !native_eval then !cnv1 else cnv2) tm
111  end
112fun mk s = Term.prim_mk_const {Name = "fp64_" ^ s, Thy = "machine_ieee"}
113val () = computeLib.add_convs
114  [(mk "sqrt", 2, native sqrt_CONV "sqrt"),
115   (mk "add", 3, native add_CONV "add"),
116   (mk "sub", 3, native sub_CONV "sub"),
117   (mk "mul", 3, native mul_CONV "mul"),
118   (mk "div", 3, native div_CONV "div"),
119   (mk "compare", 2, native compare_CONV "compare"),
120   (mk "equal", 2, native eq_CONV "equal"),
121   (mk "lessThan", 2, native lt_CONV "lessThan"),
122   (mk "lessEqual", 2, native le_CONV "lessEqual"),
123   (mk "greaterThan", 2, native gt_CONV "greaterThan"),
124   (mk "greaterEqual", 2, native ge_CONV "greaterEqual")
125  ]`
126
127val () = export_theory ()
128