author | haftmann |
Thu, 28 Jun 2007 19:09:43 +0200 | |
changeset 23517 | 93d1ad7662a9 |
parent 23298 | 404988d8b1e0 |
child 23520 | 483fe92f00c1 |
permissions | -rw-r--r-- |
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 |
|
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 |
||
23517 | 46 |
type integer = int; |
47 |
||
23251 | 48 |
val int = fromInt; |
49 |
||
50 |
val zero = int 0; |
|
51 |
val one = int 1; |
|
52 |
val two = int 2; |
|
53 |
||
54 |
val machine_int = toInt; |
|
55 |
val string_of_int = toString; |
|
56 |
val int_of_string = fromString; |
|
57 |
||
58 |
val eq = op = : int * int -> bool; |
|
59 |
val cmp = compare; |
|
60 |
val le = curry (op <=); |
|
61 |
val lt = curry (op <); |
|
62 |
fun cmp_zero k = cmp (k, zero); |
|
63 |
||
64 |
val min = curry min; |
|
65 |
val max = curry max; |
|
66 |
||
67 |
val inc = curry (op +) one; |
|
68 |
||
69 |
val add = curry (op +); |
|
70 |
val sub = curry (op -); |
|
71 |
val mult = curry ( op * ); |
|
72 |
val divmod = curry divMod; |
|
73 |
nonfix div val div = curry div; |
|
74 |
nonfix mod val mod = curry mod; |
|
75 |
val neg = ~; |
|
76 |
||
77 |
fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k); |
|
78 |
||
79 |
fun pow k l = |
|
80 |
let |
|
81 |
fun pw 0 = 1 |
|
82 |
| pw k = mult l (pw (sub k 1)); |
|
83 |
in if k < zero |
|
84 |
then error "pow: negative exponent" |
|
85 |
else pw k |
|
86 |
end; |
|
87 |
||
88 |
fun exp k = pow k two; |
|
89 |
val log = int o log2; |
|
90 |
||
91 |
fun gcd x y = |
|
92 |
let |
|
93 |
fun gxd x y = if y = zero then x else gxd y (mod x y) |
|
94 |
in if lt x y then gxd y x else gxd x y end; |
|
95 |
||
96 |
fun lcm x y = div (mult x y) (gcd x y); |
|
97 |
||
98 |
end; |
|
99 |
||
100 |
type integer = Integer.int; |
|
101 |
||
102 |
infix 7 *%; |
|
23298
404988d8b1e0
eqtype int -- explicitly encourage overloaded equality;
wenzelm
parents:
23251
diff
changeset
|
103 |
infix 6 +% -%; |
23251 | 104 |
infix 4 =% <% <=% >% >=% <>%; |
105 |
||
106 |
fun a +% b = Integer.add a b; |
|
23298
404988d8b1e0
eqtype int -- explicitly encourage overloaded equality;
wenzelm
parents:
23251
diff
changeset
|
107 |
fun a -% b = Integer.sub a b; |
23251 | 108 |
fun a *% b = Integer.mult a b; |
109 |
fun a =% b = Integer.eq (a, b); |
|
110 |
fun a <% b = Integer.lt a b; |
|
111 |
fun a <=% b = Integer.le a b; |
|
112 |
fun a >% b = b <% a; |
|
113 |
fun a >=% b = b <=% a; |
|
114 |
fun a <>% b = not (a =% b); |