src/Tools/float.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 30161 c26e515f1c29
child 67560 0fa87bd86566
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     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 fun eq (r, s) = ord (r, s) = EQUAL;
    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;