23251
|
1 |
(* Title: Pure/General/float.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Steven Obua, Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Implementation of real numbers as mantisse-exponent pairs.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature FLOAT =
|
|
9 |
sig
|
23261
|
10 |
type float = integer * integer
|
23251
|
11 |
val zero: float
|
|
12 |
val eq: float * float -> bool
|
|
13 |
val cmp: float * float -> order
|
|
14 |
val cmp_zero: float -> order
|
|
15 |
val min: float -> float -> float
|
|
16 |
val max: float -> float -> float
|
|
17 |
val add: float -> float -> float
|
|
18 |
val sub: float -> float -> float
|
|
19 |
val neg: float -> float
|
|
20 |
val mult: float -> float -> float
|
|
21 |
val positive_part: float -> float
|
|
22 |
val negative_part: float -> float
|
|
23 |
end;
|
|
24 |
|
|
25 |
structure Float : FLOAT =
|
|
26 |
struct
|
|
27 |
|
23261
|
28 |
type float = integer * integer;
|
23251
|
29 |
|
23261
|
30 |
val zero = (Integer.zero, Integer.zero);
|
23251
|
31 |
|
|
32 |
fun add (a1, b1) (a2, b2) =
|
23261
|
33 |
if Integer.cmp (b1, b2) = LESS then
|
|
34 |
(a1 +% a2 *% Integer.exp (b2 -% b1), b1)
|
23251
|
35 |
else
|
23261
|
36 |
(a1 *% Integer.exp (b1 -% b2) +% a2, b2);
|
23251
|
37 |
|
|
38 |
fun sub (a1, b1) (a2, b2) =
|
23261
|
39 |
if Integer.cmp (b1, b2) = LESS then
|
|
40 |
(a1 -% a2 *% Integer.exp (b2 -% b1), b1)
|
23251
|
41 |
else
|
23261
|
42 |
(a1 *% Integer.exp (b1 -% b2) -% a2, b2);
|
23251
|
43 |
|
23261
|
44 |
fun neg (a, b) = (Integer.neg a, b);
|
23251
|
45 |
|
23261
|
46 |
fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
|
23251
|
47 |
|
23261
|
48 |
fun cmp_zero (a, b) = Integer.cmp_zero a;
|
23251
|
49 |
|
|
50 |
fun cmp (r, s) = cmp_zero (sub r s);
|
|
51 |
|
|
52 |
fun eq (r, s) = cmp (r, s) = EQUAL;
|
|
53 |
|
|
54 |
fun min r s = case cmp (r, s) of LESS => r | _ => s;
|
|
55 |
fun max r s = case cmp (r, s) of LESS => s | _ => r;
|
|
56 |
|
23261
|
57 |
fun positive_part (a, b) = (Integer.max Integer.zero a, b);
|
|
58 |
fun negative_part (a, b) = (Integer.min Integer.zero a, b);
|
23251
|
59 |
|
|
60 |
end;
|