src/Pure/General/integer.ML
changeset 24633 0a3a02066244
child 28308 d4396a28fb29
equal deleted inserted replaced
24632:779fc4fcbf8b 24633:0a3a02066244
       
     1 (*  Title:      Tools/integer.ML
       
     2     ID:         $Id$
       
     3     Author:     Florian Haftmann, TU Muenchen
       
     4 
       
     5 Unbounded integers.
       
     6 *)
       
     7 
       
     8 signature INTEGER =
       
     9 sig
       
    10   val sign: int -> order
       
    11   val sum: int list -> int
       
    12   val div_mod: int -> int -> int * int
       
    13   val square: int -> int
       
    14   val pow: int -> int -> int (* exponent -> base -> result *)
       
    15   val gcd: int -> int -> int
       
    16   val gcds: int list -> int
       
    17   val lcm: int -> int -> int
       
    18   val lcms: int list -> int
       
    19 end;
       
    20 
       
    21 structure Integer : INTEGER =
       
    22 struct
       
    23 
       
    24 fun sign x = int_ord (x, 0);
       
    25 
       
    26 fun sum xs = fold (curry op +) xs 0;
       
    27 
       
    28 fun div_mod x y = IntInf.divMod (x, y);
       
    29 
       
    30 fun square x = x * x;
       
    31 
       
    32 fun pow k l =
       
    33   let
       
    34     fun pw 0 _ = 1
       
    35       | pw 1 l = l
       
    36       | pw k l =
       
    37           let
       
    38             val (k', r) = div_mod k 2;
       
    39             val l' = pw k' (l * l);
       
    40           in if r = 0 then l' else l' * l end;
       
    41   in
       
    42     if k < 0
       
    43     then error "pow: negative exponent"
       
    44     else pw k l
       
    45   end;
       
    46 
       
    47 fun gcd x y =
       
    48   let
       
    49     fun gxd x y = if y = 0 then x else gxd y (x mod y)
       
    50   in if x < y then gxd y x else gxd x y end;
       
    51 
       
    52 fun gcds xs = fold gcd xs 0;
       
    53 
       
    54 fun lcm x y = (x * y) div (gcd x y);
       
    55 fun lcms xs = fold lcm xs 1;
       
    56 
       
    57 end;
       
    58