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
|
|
10 |
type float = Intt.int * Intt.int
|
|
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 |
|
|
28 |
type float = Intt.int * Intt.int;
|
|
29 |
|
|
30 |
val zero = (Intt.zero, Intt.zero);
|
|
31 |
|
|
32 |
fun add (a1, b1) (a2, b2) =
|
|
33 |
if Intt.cmp (b1, b2) = LESS then
|
|
34 |
(Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
|
|
35 |
else
|
|
36 |
(Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
|
|
37 |
|
|
38 |
fun sub (a1, b1) (a2, b2) =
|
|
39 |
if Intt.cmp (b1, b2) = LESS then
|
|
40 |
(Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
|
|
41 |
else
|
|
42 |
(Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
|
|
43 |
|
|
44 |
fun neg (a, b) = (Intt.neg a, b);
|
|
45 |
|
|
46 |
fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2);
|
|
47 |
|
|
48 |
fun cmp_zero (a, b) = Intt.cmp_zero a;
|
|
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 |
|
|
57 |
fun positive_part (a, b) = (Intt.max Intt.zero a, b);
|
|
58 |
fun negative_part (a, b) = (Intt.min Intt.zero a, b);
|
|
59 |
|
|
60 |
end;
|