src/Tools/float.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (7 weeks ago)
changeset 69981 3dced198b9ec
parent 67560 0fa87bd86566
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/float.ML
     2     Author:     Steven Obua, Florian Haftmann, TU Muenchen
     3 
     4 Implementation of real numbers as mantisse-exponent pairs.
     5 *)
     6 
     7 signature FLOAT =
     8 sig
     9   type float = int * int
    10   val zero: float
    11   val eq: float * float -> bool
    12   val ord: float * float -> order
    13   val sign: float -> order
    14   val min: float -> float -> float
    15   val max: float -> float -> float
    16   val add: float -> float -> float
    17   val sub: float -> float -> float
    18   val neg: float -> float
    19   val mult: float -> float -> float
    20   val positive_part: float -> float
    21   val negative_part: float -> float
    22 end;
    23 
    24 structure Float : FLOAT =
    25 struct
    26 
    27 type float = int * int;
    28 
    29 val zero: float = (0, 0);
    30 
    31 fun add (a1, b1) (a2, b2) =
    32   if b1 < b2 then
    33     (a1 + a2 * Integer.square (b2 - b1), b1)
    34   else
    35     (a1 * Integer.square (b1 - b2) + a2, b2);
    36 
    37 fun sub (a1, b1) (a2, b2) =
    38   if b1 < b2 then
    39     (a1 - a2 * Integer.square (b2 - b1), b1)
    40   else
    41     (a1 * Integer.square (b1 - b2) - a2, b2);
    42 
    43 fun neg (a, b) = (~ a, b);
    44 
    45 fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
    46 
    47 fun sign (a, b) = Integer.sign a;
    48 
    49 fun ord (r, s) = sign (sub r s);
    50 
    51 val eq = is_equal o ord;
    52 
    53 fun min r s = case ord (r, s) of LESS => r | _ => s;
    54 fun max r s = case ord (r, s) of LESS => s | _ => r;
    55 
    56 fun positive_part (a, b) = (Int.max (0, a), b);
    57 fun negative_part (a, b) = (Int.min (0, a), b);
    58 
    59 end;