haftmann@24584: (*  Title:      Tools/float.ML
haftmann@23251:     Author:     Steven Obua, Florian Haftmann, TU Muenchen
haftmann@23251: 
haftmann@23251: Implementation of real numbers as mantisse-exponent pairs.
haftmann@23251: *)
haftmann@23251: 
haftmann@23251: signature FLOAT =
haftmann@23251: sig
wenzelm@24630:   type float = int * int
haftmann@23251:   val zero: float
haftmann@23251:   val eq: float * float -> bool
haftmann@23520:   val ord: float * float -> order
haftmann@23520:   val sign: float -> order
haftmann@23251:   val min: float -> float -> float
haftmann@23251:   val max: float -> float -> float
haftmann@23251:   val add: float -> float -> float
haftmann@23251:   val sub: float -> float -> float
haftmann@23251:   val neg: float -> float
haftmann@23251:   val mult: float -> float -> float
haftmann@23251:   val positive_part: float -> float
haftmann@23251:   val negative_part: float -> float
haftmann@23251: end;
haftmann@23251: 
haftmann@23251: structure Float : FLOAT =
haftmann@23251: struct
haftmann@23251: 
wenzelm@24630: type float = int * int;
haftmann@23251: 
wenzelm@23297: val zero: float = (0, 0);
haftmann@23251: 
haftmann@23251: fun add (a1, b1) (a2, b2) =
wenzelm@24630:   if b1 < b2 then
wenzelm@24630:     (a1 + a2 * Integer.square (b2 - b1), b1)
haftmann@23251:   else
wenzelm@24630:     (a1 * Integer.square (b1 - b2) + a2, b2);
haftmann@23251: 
haftmann@23251: fun sub (a1, b1) (a2, b2) =
wenzelm@24630:   if b1 < b2 then
wenzelm@24630:     (a1 - a2 * Integer.square (b2 - b1), b1)
haftmann@23251:   else
wenzelm@24630:     (a1 * Integer.square (b1 - b2) - a2, b2);
haftmann@23251: 
wenzelm@24630: fun neg (a, b) = (~ a, b);
haftmann@23251: 
wenzelm@24630: fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
haftmann@23251: 
haftmann@23520: fun sign (a, b) = Integer.sign a;
haftmann@23251: 
haftmann@23520: fun ord (r, s) = sign (sub r s);
haftmann@23251: 
haftmann@23520: fun eq (r, s) = ord (r, s) = EQUAL;
haftmann@23251: 
haftmann@23520: fun min r s = case ord (r, s) of LESS => r | _ => s;
haftmann@23520: fun max r s = case ord (r, s) of LESS => s | _ => r;
haftmann@23251: 
wenzelm@24630: fun positive_part (a, b) = (Int.max (0, a), b);
wenzelm@24630: fun negative_part (a, b) = (Int.min (0, a), b);
haftmann@23251: 
haftmann@23251: end;