haftmann@23251: (*  Title:      Pure/General/float.ML
haftmann@23251:     ID:         $Id$
haftmann@23251:     Author:     Steven Obua, Florian Haftmann, TU Muenchen
haftmann@23251: 
haftmann@23251: Implementation of real numbers as mantisse-exponent pairs.
haftmann@23251: *)
haftmann@23251: 
haftmann@23251: signature FLOAT =
haftmann@23251: sig
haftmann@23261:   type float = integer * integer
haftmann@23251:   val zero: float
haftmann@23251:   val eq: float * float -> bool
haftmann@23251:   val cmp: float * float -> order
haftmann@23251:   val cmp_zero: float -> order
haftmann@23251:   val min: float -> float -> float
haftmann@23251:   val max: float -> float -> float
haftmann@23251:   val add: float -> float -> float
haftmann@23251:   val sub: float -> float -> float
haftmann@23251:   val neg: float -> float
haftmann@23251:   val mult: float -> float -> float
haftmann@23251:   val positive_part: float -> float
haftmann@23251:   val negative_part: float -> float
haftmann@23251: end;
haftmann@23251: 
haftmann@23251: structure Float : FLOAT =
haftmann@23251: struct
haftmann@23251: 
haftmann@23261: type float = integer * integer;
haftmann@23251: 
wenzelm@23297: val zero: float = (0, 0);
haftmann@23251: 
haftmann@23251: fun add (a1, b1) (a2, b2) =
haftmann@23261:   if Integer.cmp (b1, b2) = LESS then
haftmann@23261:     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
haftmann@23251:   else
haftmann@23261:     (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
haftmann@23251: 
haftmann@23251: fun sub (a1, b1) (a2, b2) =
haftmann@23261:   if Integer.cmp (b1, b2) = LESS then
haftmann@23261:     (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
haftmann@23251:   else
haftmann@23261:     (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
haftmann@23251: 
haftmann@23261: fun neg (a, b) = (Integer.neg a, b);
haftmann@23251: 
haftmann@23261: fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
haftmann@23251: 
haftmann@23261: fun cmp_zero (a, b) = Integer.cmp_zero a;
haftmann@23251: 
haftmann@23251: fun cmp (r, s) = cmp_zero (sub r s);
haftmann@23251: 
haftmann@23251: fun eq (r, s) = cmp (r, s) = EQUAL;
haftmann@23251: 
haftmann@23251: fun min r s = case cmp (r, s) of LESS => r | _ => s;
haftmann@23251: fun max r s = case cmp (r, s) of LESS => s | _ => r;
haftmann@23251: 
wenzelm@23297: fun positive_part (a, b) = (Integer.max 0 a, b);
wenzelm@23297: fun negative_part (a, b) = (Integer.min 0 a, b);
haftmann@23251: 
haftmann@23251: end;