author  wenzelm 
Tue, 18 Sep 2007 16:08:00 +0200  
changeset 24630  351a308ab58d 
parent 24584  01e83ffa6c54 
child 30161  c26e515f1c29 
permissions  rwrr 
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 mantisseexponent 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; 