1 (* Title: Pure/General/int.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Unbounded integers. |
|
6 *) |
|
7 |
|
8 signature INTT = |
|
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 cmp_zero: int -> order |
|
22 val min: int -> int -> int |
|
23 val max: int -> int -> int |
|
24 val inc: int -> int |
|
25 val add: int -> int -> int |
|
26 val sub: int -> int -> int |
|
27 val mult: int -> int -> int |
|
28 val divmod: int -> int -> int * int |
|
29 val div: int -> int -> int |
|
30 val mod: int -> int -> int |
|
31 val neg: int -> int |
|
32 val exp: int -> int |
|
33 val log: int -> int |
|
34 val pow: int -> int -> int (* exponent -> base -> result *) |
|
35 end; |
|
36 |
|
37 structure Intt: INTT = |
|
38 struct |
|
39 |
|
40 open IntInf; |
|
41 |
|
42 val int = fromInt; |
|
43 |
|
44 val zero = int 0; |
|
45 val one = int 1; |
|
46 val two = int 2; |
|
47 |
|
48 val machine_int = toInt; |
|
49 val string_of_int = toString; |
|
50 val int_of_string = fromString; |
|
51 |
|
52 val eq = op = : int * int -> bool; |
|
53 val cmp = compare; |
|
54 val le = curry (op <=); |
|
55 val cmp_zero = curry cmp zero; |
|
56 |
|
57 val min = curry min; |
|
58 val max = curry max; |
|
59 |
|
60 val inc = curry (op +) one; |
|
61 |
|
62 val add = curry (op +); |
|
63 val sub = curry (op -); |
|
64 val mult = curry ( op * ); |
|
65 val divmod = curry divMod; |
|
66 nonfix div val div = curry div; |
|
67 nonfix mod val mod = curry mod; |
|
68 val neg = ~; |
|
69 |
|
70 fun pow k l = |
|
71 let |
|
72 fun pw 0 = 1 |
|
73 | pw k = mult l (pw (sub k 1)); |
|
74 in if k < zero |
|
75 then error "pow: negative exponent" |
|
76 else pw k |
|
77 end; |
|
78 |
|
79 fun exp k = pow k two; |
|
80 val log = int o log2; |
|
81 |
|
82 end; |
|