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 mantisseexponent 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 

23297

30 
val zero: float = (0, 0);

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 

23297

57 
fun positive_part (a, b) = (Integer.max 0 a, b);


58 
fun negative_part (a, b) = (Integer.min 0 a, b);

23251

59 


60 
end;
