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


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;
