(*  Title:      Tools/integer.ML

     ID:         $Id$

     Author:     Florian Haftmann, TU Muenchen

 Unbounded integers.

 *)

 signature INTEGER =

 sig

   eqtype int

   val zero: int

   val one: int

   val two: int

   val int: Int.int -> int

   val machine_int: int -> Int.int

   val string_of_int: int -> string

   val int_of_string: string -> int option

   val eq: int * int -> bool

   val ord: int * int -> order

   val le: int -> int -> bool

   val lt: int -> int -> bool

   val signabs: int -> order * int

   val sign: int -> order

   val abs: int -> int

   val min: int -> int -> int

   val max: int -> int -> int

   val inc: int -> int

   val add: int -> int -> int

   val sub: int -> int -> int

   val mult: int -> int -> int

   val divmod: int -> int -> int * int

   val div: int -> int -> int

   val mod: int -> int -> int

   val neg: int -> int

   val exp: int -> int

   val log: int -> int

   val pow: int -> int -> int (* exponent -> base -> result *)

   val gcd: int -> int -> int

   val lcm: int -> int -> int

 end;

 structure Integer : INTEGER =

 struct

 open IntInf;

 val int = fromInt;

 val zero = int 0;

 val one = int 1;

 val two = int 2;

 val machine_int = toInt;

 val string_of_int = toString;

 val int_of_string = fromString;

 val eq = op = : int * int -> bool;

 val ord = compare;

 val le = curry (op <=);

 val lt = curry (op <);

 fun sign k = ord (k, zero);

 fun signabs k = (ord (k, zero), abs k);

 val min = curry min;

 val max = curry max;

 val inc = curry (op +) one;

 val add = curry (op +);

 val sub = curry (op -);

 val mult = curry ( op * );

 val divmod = curry divMod;

 nonfix div val div = curry div;

 nonfix mod val mod = curry mod;

 val neg = ~;

 fun pow k l =

   let

     fun pw 0 _ = 1

       | pw 1 l = l

       | pw k l =

           let

             val (k', r) = divmod k 2;

             val l' = pw k' (mult l l);

           in if r = 0 then l' else mult l' l end;

   in if k < zero

     then error "pow: negative exponent"

     else pw k l

   end;

 fun exp k = pow k two;

 val log = int o log2;

 fun gcd x y =

   let

     fun gxd x y = if y = zero then x else gxd y (mod x y)

   in if lt x y then gxd y x else gxd x y end;

 fun lcm x y = div (mult x y) (gcd x y);

 end;

 type integer = Integer.int;

 infix 7 *%;

 infix 6 +% -%;

 infix 4 =% <% <=% >% >=% <>%;

 fun a +% b = Integer.add a b;

 fun a -% b = Integer.sub a b;

 fun a *% b = Integer.mult a b;

 fun a =% b = Integer.eq (a, b);

 fun a <% b = Integer.lt a b;

 fun a <=% b = Integer.le a b;

 fun a >% b = b <% a;

 fun a >=% b = b <=% a;

 fun a <>% b = not (a =% b);