src/Tools/float.ML
changeset 23251 471b576aad25
child 23261 85f27f79232f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/float.ML	Tue Jun 05 15:17:02 2007 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +(*  Title:      Pure/General/float.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua, Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Implementation of real numbers as mantisse-exponent pairs.
     1.9 +*)
    1.10 +
    1.11 +signature FLOAT =
    1.12 +sig
    1.13 +  type float = Intt.int * Intt.int
    1.14 +  val zero: float
    1.15 +  val eq: float * float -> bool
    1.16 +  val cmp: float * float -> order
    1.17 +  val cmp_zero: float -> order
    1.18 +  val min: float -> float -> float
    1.19 +  val max: float -> float -> float
    1.20 +  val add: float -> float -> float
    1.21 +  val sub: float -> float -> float
    1.22 +  val neg: float -> float
    1.23 +  val mult: float -> float -> float
    1.24 +  val positive_part: float -> float
    1.25 +  val negative_part: float -> float
    1.26 +end;
    1.27 +
    1.28 +structure Float : FLOAT =
    1.29 +struct
    1.30 +
    1.31 +type float = Intt.int * Intt.int;
    1.32 +
    1.33 +val zero = (Intt.zero, Intt.zero);
    1.34 +
    1.35 +fun add (a1, b1) (a2, b2) =
    1.36 +  if Intt.cmp (b1, b2) = LESS then
    1.37 +    (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    1.38 +  else
    1.39 +    (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    1.40 +
    1.41 +fun sub (a1, b1) (a2, b2) =
    1.42 +  if Intt.cmp (b1, b2) = LESS then
    1.43 +    (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
    1.44 +  else
    1.45 +    (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
    1.46 +
    1.47 +fun neg (a, b) = (Intt.neg a, b);
    1.48 +
    1.49 +fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2);
    1.50 +
    1.51 +fun cmp_zero (a, b) = Intt.cmp_zero a;
    1.52 +
    1.53 +fun cmp (r, s) = cmp_zero (sub r s);
    1.54 +
    1.55 +fun eq (r, s) = cmp (r, s) = EQUAL;
    1.56 +
    1.57 +fun min r s = case cmp (r, s) of LESS => r | _ => s;
    1.58 +fun max r s = case cmp (r, s) of LESS => s | _ => r;
    1.59 +
    1.60 +fun positive_part (a, b) = (Intt.max Intt.zero a, b);
    1.61 +fun negative_part (a, b) = (Intt.min Intt.zero a, b);
    1.62 +
    1.63 +end;