machine_ieeeScript.sml

1Theory machine_ieee
2Ancestors
3  binary_ieee
4Libs
5  machine_ieeeLib
6
7(* ------------------------------------------------------------------------
8   Bit-vector Encodings
9   ------------------------------------------------------------------------ *)
10
11(* 16-bit, 32-bit and 64-bit encodings *)
12
13val thms = (List.concat o List.map machine_ieeeLib.mk_fp_encoding)
14   [("fp16", 10, 5, SOME "half"),
15    ("fp32", 23, 8, SOME "single"),
16    ("fp64", 52, 11, SOME "double")];
17
18(* ------------------------------------------------------------------------
19   Encoding conversions
20   ------------------------------------------------------------------------ *)
21
22Definition convert_def:
23  convert (to_float: 'a word -> ('b, 'c) float)
24          (from_float: ('d, 'e) float -> 'f word) from_real_with_flags
25          (m: rounding) w =
26  let f = to_float w in
27  case float_value f of
28     Float r => from_real_with_flags m r
29   | NaN => (check_for_signalling [f], from_float (@fp. float_is_nan fp))
30   | Infinity =>
31       (clear_flags,
32        from_float (if f.Sign = 0w then
33                      float_plus_infinity (:'d # 'e)
34                    else
35                      float_minus_infinity (:'d # 'e)))
36End
37
38(* These can only set InvalidOp *)
39
40Definition fp16_to_fp32_with_flags_def:
41  fp16_to_fp32_with_flags =
42  convert fp16_to_float float_to_fp32 real_to_fp32_with_flags roundTiesToEven
43End
44
45Definition fp16_to_fp64_with_flags_def:
46  fp16_to_fp64_with_flags =
47  convert fp16_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven
48End
49
50Definition fp32_to_fp64_with_flags_def:
51  fp32_to_fp64_with_flags =
52  convert fp32_to_float float_to_fp64 real_to_fp64_with_flags roundTiesToEven
53End
54
55(* These can set InvalidOp, Overflow, Precision and Underflow_* *)
56
57Definition fp64_to_fp32_with_flags_def:
58  fp64_to_fp32_with_flags =
59  convert fp64_to_float float_to_fp32 real_to_fp32_with_flags
60End
61
62Definition fp64_to_fp16_with_flags_def:
63  fp64_to_fp16_with_flags =
64  convert fp64_to_float float_to_fp16 real_to_fp16_with_flags
65End
66
67Definition fp32_to_fp16_with_flags_def:
68  fp32_to_fp16_with_flags =
69  convert fp32_to_float float_to_fp16 real_to_fp16_with_flags
70End
71
72(* Versions without flags *)
73
74Definition fp16_to_fp32_def:   fp16_to_fp32 = SND o fp16_to_fp32_with_flags
75End
76Definition fp16_to_fp64_def:   fp16_to_fp64 = SND o fp16_to_fp64_with_flags
77End
78Definition fp32_to_fp64_def:   fp32_to_fp64 = SND o fp32_to_fp64_with_flags
79End
80
81Definition fp64_to_fp32_def:   fp64_to_fp32 m = SND o fp64_to_fp32_with_flags m
82End
83Definition fp64_to_fp16_def:   fp64_to_fp16 m = SND o fp64_to_fp16_with_flags m
84End
85Definition fp32_to_fp16_def:   fp32_to_fp16 m = SND o fp32_to_fp16_with_flags m
86End