src/Tools/float.ML
changeset 23297 06f108974fa1
parent 23261 85f27f79232f
child 23520 483fe92f00c1
equal deleted inserted replaced
23296:25f28f9c28a3 23297:06f108974fa1
    25 structure Float : FLOAT =
    25 structure Float : FLOAT =
    26 struct
    26 struct
    27 
    27 
    28 type float = integer * integer;
    28 type float = integer * integer;
    29 
    29 
    30 val zero = (Integer.zero, Integer.zero);
    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.cmp (b1, b2) = LESS then
    34     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    34     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
    35   else
    35   else
    52 fun eq (r, s) = cmp (r, s) = EQUAL;
    52 fun eq (r, s) = cmp (r, s) = EQUAL;
    53 
    53 
    54 fun min r s = case cmp (r, s) of LESS => r | _ => s;
    54 fun min r s = case cmp (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 cmp (r, s) of LESS => s | _ => r;
    56 
    56 
    57 fun positive_part (a, b) = (Integer.max Integer.zero a, b);
    57 fun positive_part (a, b) = (Integer.max 0 a, b);
    58 fun negative_part (a, b) = (Integer.min Integer.zero a, b);
    58 fun negative_part (a, b) = (Integer.min 0 a, b);
    59 
    59 
    60 end;
    60 end;