src/Tools/float.ML
changeset 23520 483fe92f00c1
parent 23297 06f108974fa1
child 24584 01e83ffa6c54
     1.1 --- a/src/Tools/float.ML	Fri Jun 29 18:21:25 2007 +0200
     1.2 +++ b/src/Tools/float.ML	Fri Jun 29 21:23:05 2007 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    type float = integer * integer
     1.5    val zero: float
     1.6    val eq: float * float -> bool
     1.7 -  val cmp: float * float -> order
     1.8 -  val cmp_zero: float -> order
     1.9 +  val ord: float * float -> order
    1.10 +  val sign: float -> order
    1.11    val min: float -> float -> float
    1.12    val max: float -> float -> float
    1.13    val add: float -> float -> float
    1.14 @@ -30,13 +30,13 @@
    1.15  val zero: float = (0, 0);
    1.16  
    1.17  fun add (a1, b1) (a2, b2) =
    1.18 -  if Integer.cmp (b1, b2) = LESS then
    1.19 +  if Integer.ord (b1, b2) = LESS then
    1.20      (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    1.21    else
    1.22      (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
    1.23  
    1.24  fun sub (a1, b1) (a2, b2) =
    1.25 -  if Integer.cmp (b1, b2) = LESS then
    1.26 +  if Integer.ord (b1, b2) = LESS then
    1.27      (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
    1.28    else
    1.29      (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
    1.30 @@ -45,14 +45,14 @@
    1.31  
    1.32  fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
    1.33  
    1.34 -fun cmp_zero (a, b) = Integer.cmp_zero a;
    1.35 +fun sign (a, b) = Integer.sign a;
    1.36  
    1.37 -fun cmp (r, s) = cmp_zero (sub r s);
    1.38 +fun ord (r, s) = sign (sub r s);
    1.39  
    1.40 -fun eq (r, s) = cmp (r, s) = EQUAL;
    1.41 +fun eq (r, s) = ord (r, s) = EQUAL;
    1.42  
    1.43 -fun min r s = case cmp (r, s) of LESS => r | _ => s;
    1.44 -fun max r s = case cmp (r, s) of LESS => s | _ => r;
    1.45 +fun min r s = case ord (r, s) of LESS => r | _ => s;
    1.46 +fun max r s = case ord (r, s) of LESS => s | _ => r;
    1.47  
    1.48  fun positive_part (a, b) = (Integer.max 0 a, b);
    1.49  fun negative_part (a, b) = (Integer.min 0 a, b);