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