src/Tools/float.ML
author haftmann
Tue Jun 05 15:17:02 2007 +0200 (2007-06-05)
changeset 23251 471b576aad25
child 23261 85f27f79232f
permissions -rw-r--r--
moved generic algebra modules
     1 (*  Title:      Pure/General/float.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, Florian Haftmann, TU Muenchen
     4 
     5 Implementation of real numbers as mantisse-exponent 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;