23251

1 
(* Title: Pure/General/int.ML


2 
ID: $Id$


3 
Author: Florian Haftmann, TU Muenchen


4 


5 
Unbounded integers.


6 
*)


7 


8 
signature INTEGER =


9 
sig


10 
type int


11 
val zero: int


12 
val one: int


13 
val two: int


14 
val int: Int.int > int


15 
val machine_int: int > Int.int


16 
val string_of_int: int > string


17 
val int_of_string: string > int option


18 
val eq: int * int > bool


19 
val cmp: int * int > order


20 
val le: int > int > bool


21 
val lt: int > int > bool


22 
val cmp_zero: int > order


23 
val min: int > int > int


24 
val max: int > int > int


25 
val inc: int > int


26 
val add: int > int > int


27 
val sub: int > int > int


28 
val mult: int > int > int


29 
val divmod: int > int > int * int


30 
val div: int > int > int


31 
val mod: int > int > int


32 
val neg: int > int


33 
val signabs: int > bool * int


34 
val exp: int > int


35 
val log: int > int


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


37 
val gcd: int > int > int


38 
val lcm: int > int > int


39 
end;


40 


41 
structure Integer : INTEGER =


42 
struct


43 


44 
open IntInf;


45 


46 
val int = fromInt;


47 


48 
val zero = int 0;


49 
val one = int 1;


50 
val two = int 2;


51 


52 
val machine_int = toInt;


53 
val string_of_int = toString;


54 
val int_of_string = fromString;


55 


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


57 
val cmp = compare;


58 
val le = curry (op <=);


59 
val lt = curry (op <);


60 
fun cmp_zero k = cmp (k, zero);


61 


62 
val min = curry min;


63 
val max = curry max;


64 


65 
val inc = curry (op +) one;


66 


67 
val add = curry (op +);


68 
val sub = curry (op );


69 
val mult = curry ( op * );


70 
val divmod = curry divMod;


71 
nonfix div val div = curry div;


72 
nonfix mod val mod = curry mod;


73 
val neg = ~;


74 


75 
fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);


76 


77 
fun pow k l =


78 
let


79 
fun pw 0 = 1


80 
 pw k = mult l (pw (sub k 1));


81 
in if k < zero


82 
then error "pow: negative exponent"


83 
else pw k


84 
end;


85 


86 
fun exp k = pow k two;


87 
val log = int o log2;


88 


89 
fun gcd x y =


90 
let


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


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


93 


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


95 


96 
end;


97 


98 
type integer = Integer.int;


99 


100 
infix 7 *%;


101 
infix 6 +% %;


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


103 


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


105 
fun a % b = a +% Integer.neg b;


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


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


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


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


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


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


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


113 


114 
structure Intt = Integer; (*FIXME*)


115 
val gcd = uncurry Integer.gcd; (*FIXME*)


116 
val lcm = uncurry Integer.lcm; (*FIXME*)
