src/Tools/float.ML
author haftmann
Tue Jun 05 19:19:30 2007 +0200 (2007-06-05)
changeset 23261 85f27f79232f
parent 23251 471b576aad25
child 23297 06f108974fa1
permissions -rw-r--r--
tuned integers
     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 = integer * integer
    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 = integer * integer;
    29 
    30 val zero = (Integer.zero, Integer.zero);
    31 
    32 fun add (a1, b1) (a2, b2) =
    33   if Integer.cmp (b1, b2) = LESS then
    34     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    35   else
    36     (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
    37 
    38 fun sub (a1, b1) (a2, b2) =
    39   if Integer.cmp (b1, b2) = LESS then
    40     (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
    41   else
    42     (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
    43 
    44 fun neg (a, b) = (Integer.neg a, b);
    45 
    46 fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
    47 
    48 fun cmp_zero (a, b) = Integer.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) = (Integer.max Integer.zero a, b);
    58 fun negative_part (a, b) = (Integer.min Integer.zero a, b);
    59 
    60 end;