src/Tools/float.ML
author wenzelm
Wed, 26 Sep 2007 19:18:01 +0200
changeset 24726 fcf13a91cda2
parent 24630 351a308ab58d
child 30161 c26e515f1c29
permissions -rw-r--r--
Attrib.eval_thms; Syntax.parse/check;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 23520
diff changeset
     1
(*  Title:      Tools/float.ML
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     2
    ID:         $Id$
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     3
    Author:     Steven Obua, Florian Haftmann, TU Muenchen
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     4
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     5
Implementation of real numbers as mantisse-exponent pairs.
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     6
*)
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     7
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     8
signature FLOAT =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
     9
sig
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    10
  type float = int * int
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    11
  val zero: float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    12
  val eq: float * float -> bool
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    13
  val ord: float * float -> order
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    14
  val sign: float -> order
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    15
  val min: float -> float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    16
  val max: float -> float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    17
  val add: float -> float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    18
  val sub: float -> float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    19
  val neg: float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    20
  val mult: float -> float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    21
  val positive_part: float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    22
  val negative_part: float -> float
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    23
end;
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    24
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    25
structure Float : FLOAT =
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    26
struct
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    27
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    28
type float = int * int;
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    29
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
    30
val zero: float = (0, 0);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    31
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    32
fun add (a1, b1) (a2, b2) =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    33
  if b1 < b2 then
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    34
    (a1 + a2 * Integer.square (b2 - b1), b1)
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    35
  else
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    36
    (a1 * Integer.square (b1 - b2) + a2, b2);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    37
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    38
fun sub (a1, b1) (a2, b2) =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    39
  if b1 < b2 then
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    40
    (a1 - a2 * Integer.square (b2 - b1), b1)
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    41
  else
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    42
    (a1 * Integer.square (b1 - b2) - a2, b2);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    43
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    44
fun neg (a, b) = (~ a, b);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    45
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    46
fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    47
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    48
fun sign (a, b) = Integer.sign a;
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    49
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    50
fun ord (r, s) = sign (sub r s);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    51
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    52
fun eq (r, s) = ord (r, s) = EQUAL;
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    53
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    54
fun min r s = case ord (r, s) of LESS => r | _ => s;
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
    55
fun max r s = case ord (r, s) of LESS => s | _ => r;
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    56
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    57
fun positive_part (a, b) = (Int.max (0, a), b);
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    58
fun negative_part (a, b) = (Int.min (0, a), b);
23251
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    59
471b576aad25 moved generic algebra modules
haftmann
parents:
diff changeset
    60
end;