24633

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 
