src/Tools/float.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24630 351a308ab58d
child 30161 c26e515f1c29
permissions -rw-r--r--
simplified interfaces for outer syntax;
     1 (*  Title:      Tools/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 = int * int
    11   val zero: float
    12   val eq: float * float -> bool
    13   val ord: float * float -> order
    14   val sign: 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 = int * int;
    29 
    30 val zero: float = (0, 0);
    31 
    32 fun add (a1, b1) (a2, b2) =
    33   if b1 < b2 then
    34     (a1 + a2 * Integer.square (b2 - b1), b1)
    35   else
    36     (a1 * Integer.square (b1 - b2) + a2, b2);
    37 
    38 fun sub (a1, b1) (a2, b2) =
    39   if b1 < b2 then
    40     (a1 - a2 * Integer.square (b2 - b1), b1)
    41   else
    42     (a1 * Integer.square (b1 - b2) - a2, b2);
    43 
    44 fun neg (a, b) = (~ a, b);
    45 
    46 fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
    47 
    48 fun sign (a, b) = Integer.sign a;
    49 
    50 fun ord (r, s) = sign (sub r s);
    51 
    52 fun eq (r, s) = ord (r, s) = EQUAL;
    53 
    54 fun min r s = case ord (r, s) of LESS => r | _ => s;
    55 fun max r s = case ord (r, s) of LESS => s | _ => r;
    56 
    57 fun positive_part (a, b) = (Int.max (0, a), b);
    58 fun negative_part (a, b) = (Int.min (0, a), b);
    59 
    60 end;