|
15178
|
1 |
structure FloatArith =
|
|
|
2 |
struct
|
|
|
3 |
|
|
|
4 |
type float = IntInf.int * IntInf.int
|
|
|
5 |
|
|
|
6 |
val izero = IntInf.fromInt 0
|
|
|
7 |
fun imul a b = IntInf.* (a,b)
|
|
|
8 |
fun isub a b = IntInf.- (a,b)
|
|
|
9 |
fun iadd a b = IntInf.+ (a,b)
|
|
|
10 |
|
|
|
11 |
val floatzero = (izero, izero)
|
|
|
12 |
|
|
|
13 |
fun positive_part (a,b) =
|
|
|
14 |
(if IntInf.< (a,izero) then izero else a, b)
|
|
|
15 |
|
|
|
16 |
fun negative_part (a,b) =
|
|
|
17 |
(if IntInf.< (a,izero) then a else izero, b)
|
|
|
18 |
|
|
|
19 |
fun is_negative (a,b) =
|
|
|
20 |
if IntInf.< (a, izero) then true else false
|
|
|
21 |
|
|
|
22 |
fun is_positive (a,b) =
|
|
|
23 |
if IntInf.< (izero, a) then true else false
|
|
|
24 |
|
|
|
25 |
fun is_zero (a,b) =
|
|
|
26 |
if a = izero then true else false
|
|
|
27 |
|
|
|
28 |
fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
|
|
|
29 |
|
|
|
30 |
fun add (a1, b1) (a2, b2) =
|
|
15189
|
31 |
if IntInf.< (b1, b2) then
|
|
15178
|
32 |
(iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
|
|
|
33 |
else
|
|
|
34 |
(iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
|
|
|
35 |
|
|
|
36 |
fun sub (a1, b1) (a2, b2) =
|
|
15189
|
37 |
if IntInf.< (b1, b2) then
|
|
15178
|
38 |
(isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
|
|
|
39 |
else
|
|
|
40 |
(isub (imul a1 (ipow2 (isub b1 b2))) a2, b2)
|
|
|
41 |
|
|
|
42 |
fun neg (a, b) = (IntInf.~ a, b)
|
|
|
43 |
|
|
|
44 |
fun is_equal a b = is_zero (sub a b)
|
|
|
45 |
|
|
|
46 |
fun is_less a b = is_negative (sub a b)
|
|
|
47 |
|
|
|
48 |
fun max a b = if is_less a b then b else a
|
|
|
49 |
|
|
|
50 |
fun min a b = if is_less a b then a else b
|
|
|
51 |
|
|
|
52 |
fun abs a = if is_negative a then neg a else a
|
|
|
53 |
|
|
|
54 |
fun mul (a1, b1) (a2, b2) = (imul a1 a2, iadd b1 b2)
|
|
|
55 |
|
|
|
56 |
end;
|