author  wenzelm 
Sun, 08 Jul 2007 19:51:58 +0200  
changeset 23655  d2d1138e0ddc 
parent 23520  483fe92f00c1 
child 24584  01e83ffa6c54 
permissions  rwrr 
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 

23298
404988d8b1e0
eqtype int  explicitly encourage overloaded equality;
wenzelm
parents:
23251
diff
changeset

10 
eqtype int 
23251  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 

23520  19 
val ord: int * int > order 
23251  20 
val le: int > int > bool 
21 
val lt: int > int > bool 

23520  22 
val signabs: int > order * int 
23 
val sign: int > order 

24 
val abs: int > int 

23251  25 
val min: int > int > int 
26 
val max: int > int > int 

27 
val inc: int > int 

28 
val add: int > int > int 

29 
val sub: int > int > int 

30 
val mult: int > int > int 

31 
val divmod: int > int > int * int 

32 
val div: int > int > int 

33 
val mod: int > int > int 

34 
val neg: int > int 

35 
val exp: int > int 

36 
val log: int > int 

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

38 
val gcd: int > int > int 

39 
val lcm: int > int > int 

40 
end; 

41 

42 
structure Integer : INTEGER = 

43 
struct 

44 

45 
open IntInf; 

46 

47 
val int = fromInt; 

48 

49 
val zero = int 0; 

50 
val one = int 1; 

51 
val two = int 2; 

52 

53 
val machine_int = toInt; 

54 
val string_of_int = toString; 

55 
val int_of_string = fromString; 

56 

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

23520  58 
val ord = compare; 
23251  59 
val le = curry (op <=); 
60 
val lt = curry (op <); 

23520  61 

62 
fun sign k = ord (k, zero); 

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

23251  64 

65 
val min = curry min; 

66 
val max = curry max; 

67 

68 
val inc = curry (op +) one; 

69 

70 
val add = curry (op +); 

71 
val sub = curry (op ); 

72 
val mult = curry ( op * ); 

73 
val divmod = curry divMod; 

74 
nonfix div val div = curry div; 

75 
nonfix mod val mod = curry mod; 

76 
val neg = ~; 

77 

78 
fun pow k l = 

79 
let 

23520  80 
fun pw 0 _ = 1 
81 
 pw 1 l = l 

82 
 pw k l = 

83 
let 

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

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

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

23251  87 
in if k < zero 
88 
then error "pow: negative exponent" 

23520  89 
else pw k l 
23251  90 
end; 
91 

92 
fun exp k = pow k two; 

93 
val log = int o log2; 

94 

95 
fun gcd x y = 

96 
let 

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

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

99 

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

101 

102 
end; 

103 

104 
type integer = Integer.int; 

105 

106 
infix 7 *%; 

23298
404988d8b1e0
eqtype int  explicitly encourage overloaded equality;
wenzelm
parents:
23251
diff
changeset

107 
infix 6 +% %; 
23251  108 
infix 4 =% <% <=% >% >=% <>%; 
109 

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

23298
404988d8b1e0
eqtype int  explicitly encourage overloaded equality;
wenzelm
parents:
23251
diff
changeset

111 
fun a % b = Integer.sub a b; 
23251  112 
fun a *% b = Integer.mult a b; 
113 
fun a =% b = Integer.eq (a, b); 

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

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

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

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

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