1(* -------------------------------------------------------------------------
2   Floating-point
3   ------------------------------------------------------------------------- *)
4
5structure FP64 :> FP =
6struct
7
8   structure R = Real
9   structure P = PackRealLittle (* must be little-endian structure *)
10
11   type ieee_flags = {DivideByZero: bool,
12                      InvalidOp: bool,
13                      Overflow: bool,
14                      Precision: bool,
15                      Underflow: bool}
16
17   local
18     val bytes = Word8Vector.length (P.toBytes R.posInf)
19   in
20     val size = 8 * bytes
21     val byte = Word8.fromLargeInt o BitsN.toNat o L3.uncurry BitsN.bits
22     fun unbyte b = BitsN.fromNat (Word8.toLargeInt b, 8)
23     fun fromBits w =
24       ( IntInf.toInt (BitsN.size w) = size orelse
25         raise Fail ("fromBits: not " ^ Int.toString size ^ "-bit word")
26       ; (P.fromBytes o Word8Vector.fromList)
27           (List.tabulate
28             (bytes, fn i => let
29                                val j = 8 * IntInf.fromInt i
30                             in
31                                byte ((j + 7, j), w)
32                             end))
33       )
34     fun toBits r =
35       let
36         val v = P.toBytes r
37         val l = List.tabulate
38                   (bytes, fn i => unbyte (Word8Vector.sub (v, bytes - 1 - i)))
39       in
40         BitsN.concat l
41       end
42   end
43
44   val posInf = toBits R.posInf
45   val negInf = toBits R.negInf
46   val posZero = toBits (Option.valOf (R.fromString "0.0"))
47   val negZero = toBits (Option.valOf (R.fromString "-0.0"))
48   val qNan = BitsN.fromInt (0x7FF8000000000000, 64)
49   val sNan = BitsN.fromInt (0x7FF0000000000001, 64)
50
51   fun withMode m f x =
52     let
53       val m0 = IEEEReal.getRoundingMode ()
54     in
55        IEEEReal.setRoundingMode m
56      ; f x before IEEEReal.setRoundingMode m0
57     end
58
59   fun toInt (m, w) =
60     let
61       val r = fromBits w
62     in
63       if R.isFinite r then SOME (R.toLargeInt m r) else NONE
64     end
65
66   fun fromInt (m, i) = toBits (withMode m R.fromLargeInt i)
67   val fromString = Option.map toBits o R.fromString
68
69   val isNan = R.isNan o fromBits
70   val isFinite = R.isFinite o fromBits
71   val isNormal = R.isNormal o fromBits
72   fun isSignallingNan a = isNan a andalso not (BitsN.bit (a, 51))
73   fun isSubnormal a = R.class (fromBits a) = IEEEReal.SUBNORMAL
74   fun isIntegral a =
75     let
76       val r = fromBits a
77     in
78       R.isFinite r andalso R.== (R.realTrunc r, r)
79     end
80
81   local
82     val dummy_flags =
83       {DivideByZero = false, InvalidOp = false, Overflow = false,
84        Precision = false, Underflow = false}
85     fun fromBits2 (a, b) = (fromBits a, fromBits b)
86     fun fpOp from f (m, a) =
87       ((fn a => (dummy_flags, toBits a)) o withMode m f o from) a
88     fun fpOp0 f = toBits o f o fromBits
89     val fpOp1 = fpOp fromBits
90     val fpOp2 = fpOp fromBits2
91     val fpOp3 = fpOp (fn (a, (b, c)) => (fromBits a, fromBits b, fromBits c))
92     val sign_bit = BitsN.#>> (BitsN.B (1, IntInf.fromInt size), 1)
93     val comp_sign_bit = BitsN.~ sign_bit
94   in
95     val abs = fpOp0 R.abs
96     val neg = fpOp0 R.~
97     val sqrt = fpOp1 R.Math.sqrt
98
99     val add = fpOp2 R.+
100     val mul = fpOp2 R.*
101     val sub = fpOp2 R.-
102     val op div = fpOp2 R./
103
104     val equal = R.== o fromBits2
105     val compare = R.compareReal o fromBits2
106     val greaterThan = R.> o fromBits2
107     val greaterEqual = R.>= o fromBits2
108     val lessThan = R.< o fromBits2
109     val lessEqual = R.<= o fromBits2
110
111     val mul_add = fpOp3 R.*+
112     val mul_sub = fpOp3 R.*-
113
114     val roundToIntegral =
115       fn (IEEEReal.TO_NEGINF, a) => fpOp0 R.realFloor a
116        | (IEEEReal.TO_POSINF, a) => fpOp0 R.realCeil a
117        | (IEEEReal.TO_ZERO, a) => fpOp0 R.realTrunc a
118        | (IEEEReal.TO_NEAREST, a) => fpOp0 R.realRound a
119   end
120
121end (* functor FP *)
122