src/Pure/General/integer.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/integer.ML	Tue Sep 18 18:05:34 2007 +0200
@@ -0,0 +1,58 @@
+(*  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;
+