author | wenzelm |
Wed, 26 Sep 2007 19:18:01 +0200 | |
changeset 24726 | fcf13a91cda2 |
parent 24630 | 351a308ab58d |
child 30161 | c26e515f1c29 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/float.ML |
23251 | 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 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
10 |
type float = int * int |
23251 | 11 |
val zero: float |
12 |
val eq: float * float -> bool |
|
23520 | 13 |
val ord: float * float -> order |
14 |
val sign: float -> order |
|
23251 | 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 |
||
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
28 |
type float = int * int; |
23251 | 29 |
|
23297 | 30 |
val zero: float = (0, 0); |
23251 | 31 |
|
32 |
fun add (a1, b1) (a2, b2) = |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
33 |
if b1 < b2 then |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
34 |
(a1 + a2 * Integer.square (b2 - b1), b1) |
23251 | 35 |
else |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
36 |
(a1 * Integer.square (b1 - b2) + a2, b2); |
23251 | 37 |
|
38 |
fun sub (a1, b1) (a2, b2) = |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
39 |
if b1 < b2 then |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
40 |
(a1 - a2 * Integer.square (b2 - b1), b1) |
23251 | 41 |
else |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
42 |
(a1 * Integer.square (b1 - b2) - a2, b2); |
23251 | 43 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
44 |
fun neg (a, b) = (~ a, b); |
23251 | 45 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
46 |
fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2); |
23251 | 47 |
|
23520 | 48 |
fun sign (a, b) = Integer.sign a; |
23251 | 49 |
|
23520 | 50 |
fun ord (r, s) = sign (sub r s); |
23251 | 51 |
|
23520 | 52 |
fun eq (r, s) = ord (r, s) = EQUAL; |
23251 | 53 |
|
23520 | 54 |
fun min r s = case ord (r, s) of LESS => r | _ => s; |
55 |
fun max r s = case ord (r, s) of LESS => s | _ => r; |
|
23251 | 56 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
57 |
fun positive_part (a, b) = (Int.max (0, a), b); |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
58 |
fun negative_part (a, b) = (Int.min (0, a), b); |
23251 | 59 |
|
60 |
end; |