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
haftmann@23251
     1
(*  Title:      Pure/General/float.ML
haftmann@23251
     2
    ID:         $Id$
haftmann@23251
     3
    Author:     Steven Obua, Florian Haftmann, TU Muenchen
haftmann@23251
     4
haftmann@23251
     5
Implementation of real numbers as mantisse-exponent pairs.
haftmann@23251
     6
*)
haftmann@23251
     7
haftmann@23251
     8
signature FLOAT =
haftmann@23251
     9
sig
haftmann@23251
    10
  type float = Intt.int * Intt.int
haftmann@23251
    11
  val zero: float
haftmann@23251
    12
  val eq: float * float -> bool
haftmann@23251
    13
  val cmp: float * float -> order
haftmann@23251
    14
  val cmp_zero: float -> order
haftmann@23251
    15
  val min: float -> float -> float
haftmann@23251
    16
  val max: float -> float -> float
haftmann@23251
    17
  val add: float -> float -> float
haftmann@23251
    18
  val sub: float -> float -> float
haftmann@23251
    19
  val neg: float -> float
haftmann@23251
    20
  val mult: float -> float -> float
haftmann@23251
    21
  val positive_part: float -> float
haftmann@23251
    22
  val negative_part: float -> float
haftmann@23251
    23
end;
haftmann@23251
    24
haftmann@23251
    25
structure Float : FLOAT =
haftmann@23251
    26
struct
haftmann@23251
    27
haftmann@23251
    28
type float = Intt.int * Intt.int;
haftmann@23251
    29
haftmann@23251
    30
val zero = (Intt.zero, Intt.zero);
haftmann@23251
    31
haftmann@23251
    32
fun add (a1, b1) (a2, b2) =
haftmann@23251
    33
  if Intt.cmp (b1, b2) = LESS then
haftmann@23251
    34
    (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
haftmann@23251
    35
  else
haftmann@23251
    36
    (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
haftmann@23251
    37
haftmann@23251
    38
fun sub (a1, b1) (a2, b2) =
haftmann@23251
    39
  if Intt.cmp (b1, b2) = LESS then
haftmann@23251
    40
    (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1)
haftmann@23251
    41
  else
haftmann@23251
    42
    (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2);
haftmann@23251
    43
haftmann@23251
    44
fun neg (a, b) = (Intt.neg a, b);
haftmann@23251
    45
haftmann@23251
    46
fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2);
haftmann@23251
    47
haftmann@23251
    48
fun cmp_zero (a, b) = Intt.cmp_zero a;
haftmann@23251
    49
haftmann@23251
    50
fun cmp (r, s) = cmp_zero (sub r s);
haftmann@23251
    51
haftmann@23251
    52
fun eq (r, s) = cmp (r, s) = EQUAL;
haftmann@23251
    53
haftmann@23251
    54
fun min r s = case cmp (r, s) of LESS => r | _ => s;
haftmann@23251
    55
fun max r s = case cmp (r, s) of LESS => s | _ => r;
haftmann@23251
    56
haftmann@23251
    57
fun positive_part (a, b) = (Intt.max Intt.zero a, b);
haftmann@23251
    58
fun negative_part (a, b) = (Intt.min Intt.zero a, b);
haftmann@23251
    59
haftmann@23251
    60
end;