src/Tools/float.ML
changeset 23520 483fe92f00c1
parent 23297 06f108974fa1
child 24584 01e83ffa6c54
equal deleted inserted replaced
23519:a4ffa756d8eb 23520:483fe92f00c1
     8 signature FLOAT =
     8 signature FLOAT =
     9 sig
     9 sig
    10   type float = integer * integer
    10   type float = integer * integer
    11   val zero: float
    11   val zero: float
    12   val eq: float * float -> bool
    12   val eq: float * float -> bool
    13   val cmp: float * float -> order
    13   val ord: float * float -> order
    14   val cmp_zero: float -> order
    14   val sign: float -> order
    15   val min: float -> float -> float
    15   val min: float -> float -> float
    16   val max: float -> float -> float
    16   val max: float -> float -> float
    17   val add: float -> float -> float
    17   val add: float -> float -> float
    18   val sub: float -> float -> float
    18   val sub: float -> float -> float
    19   val neg: float -> float
    19   val neg: float -> float
    28 type float = integer * integer;
    28 type float = integer * integer;
    29 
    29 
    30 val zero: float = (0, 0);
    30 val zero: float = (0, 0);
    31 
    31 
    32 fun add (a1, b1) (a2, b2) =
    32 fun add (a1, b1) (a2, b2) =
    33   if Integer.cmp (b1, b2) = LESS then
    33   if Integer.ord (b1, b2) = LESS then
    34     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    34     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    35   else
    35   else
    36     (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
    36     (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
    37 
    37 
    38 fun sub (a1, b1) (a2, b2) =
    38 fun sub (a1, b1) (a2, b2) =
    39   if Integer.cmp (b1, b2) = LESS then
    39   if Integer.ord (b1, b2) = LESS then
    40     (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
    40     (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
    41   else
    41   else
    42     (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
    42     (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
    43 
    43 
    44 fun neg (a, b) = (Integer.neg a, b);
    44 fun neg (a, b) = (Integer.neg a, b);
    45 
    45 
    46 fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
    46 fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
    47 
    47 
    48 fun cmp_zero (a, b) = Integer.cmp_zero a;
    48 fun sign (a, b) = Integer.sign a;
    49 
    49 
    50 fun cmp (r, s) = cmp_zero (sub r s);
    50 fun ord (r, s) = sign (sub r s);
    51 
    51 
    52 fun eq (r, s) = cmp (r, s) = EQUAL;
    52 fun eq (r, s) = ord (r, s) = EQUAL;
    53 
    53 
    54 fun min r s = case cmp (r, s) of LESS => r | _ => s;
    54 fun min r s = case ord (r, s) of LESS => r | _ => s;
    55 fun max r s = case cmp (r, s) of LESS => s | _ => r;
    55 fun max r s = case ord (r, s) of LESS => s | _ => r;
    56 
    56 
    57 fun positive_part (a, b) = (Integer.max 0 a, b);
    57 fun positive_part (a, b) = (Integer.max 0 a, b);
    58 fun negative_part (a, b) = (Integer.min 0 a, b);
    58 fun negative_part (a, b) = (Integer.min 0 a, b);
    59 
    59 
    60 end;
    60 end;