author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 30161  c26e515f1c29 
child 67560  0fa87bd86566 
permissions  rwrr 
24584  1 
(* Title: Tools/float.ML 
23251  2 
Author: Steven Obua, Florian Haftmann, TU Muenchen 
3 

4 
Implementation of real numbers as mantisseexponent pairs. 

5 
*) 

6 

7 
signature FLOAT = 

8 
sig 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

9 
type float = int * int 
23251  10 
val zero: float 
11 
val eq: float * float > bool 

23520  12 
val ord: float * float > order 
13 
val sign: float > order 

23251  14 
val min: float > float > float 
15 
val max: float > float > float 

16 
val add: float > float > float 

17 
val sub: float > float > float 

18 
val neg: float > float 

19 
val mult: float > float > float 

20 
val positive_part: float > float 

21 
val negative_part: float > float 

22 
end; 

23 

24 
structure Float : FLOAT = 

25 
struct 

26 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

27 
type float = int * int; 
23251  28 

23297  29 
val zero: float = (0, 0); 
23251  30 

31 
fun add (a1, b1) (a2, b2) = 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

32 
if b1 < b2 then 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

33 
(a1 + a2 * Integer.square (b2  b1), b1) 
23251  34 
else 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

35 
(a1 * Integer.square (b1  b2) + a2, b2); 
23251  36 

37 
fun sub (a1, b1) (a2, b2) = 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

38 
if b1 < b2 then 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

39 
(a1  a2 * Integer.square (b2  b1), b1) 
23251  40 
else 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

41 
(a1 * Integer.square (b1  b2)  a2, b2); 
23251  42 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

43 
fun neg (a, b) = (~ a, b); 
23251  44 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

45 
fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2); 
23251  46 

23520  47 
fun sign (a, b) = Integer.sign a; 
23251  48 

23520  49 
fun ord (r, s) = sign (sub r s); 
23251  50 

23520  51 
fun eq (r, s) = ord (r, s) = EQUAL; 
23251  52 

23520  53 
fun min r s = case ord (r, s) of LESS => r  _ => s; 
54 
fun max r s = case ord (r, s) of LESS => s  _ => r; 

23251  55 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

56 
fun positive_part (a, b) = (Int.max (0, a), b); 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset

57 
fun negative_part (a, b) = (Int.min (0, a), b); 
23251  58 

59 
end; 