src/Pure/General/integer.ML

export get_names (formerly names);
moved pervasive theory = ThyInfo.get_theory to pure_setup.ML;
removed unused pretty_theory;
use OuterSyntax.load_thy instead of backpatched ThyLoad.load_thy;

(*  Title:      Tools/integer.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

Unbounded integers.
*)

signature INTEGER =
sig
  val sign: int -> order
  val sum: int list -> int
  val div_mod: int -> int -> int * int
  val square: int -> int
  val pow: int -> int -> int (* exponent -> base -> result *)
  val gcd: int -> int -> int
  val gcds: int list -> int
  val lcm: int -> int -> int
  val lcms: int list -> int
end;

structure Integer : INTEGER =
struct

fun sign x = int_ord (x, 0);

fun sum xs = fold (curry op +) xs 0;

fun div_mod x y = IntInf.divMod (x, y);

fun square x = x * x;

fun pow k l =
  let
    fun pw 0 _ = 1
      | pw 1 l = l
      | pw k l =
          let
            val (k', r) = div_mod k 2;
            val l' = pw k' (l * l);
          in if r = 0 then l' else l' * l end;
  in
    if k < 0
    then error "pow: negative exponent"
    else pw k l
  end;

fun gcd x y =
  let
    fun gxd x y = if y = 0 then x else gxd y (x mod y)
  in if x < y then gxd y x else gxd x y end;

fun gcds xs = fold gcd xs 0;

fun lcm x y = (x * y) div (gcd x y);
fun lcms xs = fold lcm xs 1;

end;