author | wenzelm |
Tue, 18 Sep 2007 16:08:00 +0200 | |
changeset 24630 | 351a308ab58d |
parent 24584 | 01e83ffa6c54 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/integer.ML |
23251 | 2 |
ID: $Id$ |
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
5 |
Unbounded integers. |
|
6 |
*) |
|
7 |
||
8 |
signature INTEGER = |
|
9 |
sig |
|
23520 | 10 |
val sign: int -> order |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
11 |
val sum: int list -> int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
12 |
val div_mod: int -> int -> int * int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
13 |
val square: int -> int |
23251 | 14 |
val pow: int -> int -> int (* exponent -> base -> result *) |
15 |
val gcd: int -> int -> int |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
16 |
val gcds: int list -> int |
23251 | 17 |
val lcm: int -> int -> int |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
18 |
val lcms: int list -> int |
23251 | 19 |
end; |
20 |
||
21 |
structure Integer : INTEGER = |
|
22 |
struct |
|
23 |
||
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
24 |
fun sign x = int_ord (x, 0); |
23251 | 25 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
26 |
fun sum xs = fold (curry op +) xs 0; |
23251 | 27 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
28 |
fun div_mod x y = IntInf.divMod (x, y); |
23251 | 29 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
30 |
fun square x = x * x; |
23251 | 31 |
|
32 |
fun pow k l = |
|
33 |
let |
|
23520 | 34 |
fun pw 0 _ = 1 |
35 |
| pw 1 l = l |
|
36 |
| pw k l = |
|
37 |
let |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
38 |
val (k', r) = div_mod k 2; |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
39 |
val l' = pw k' (l * l); |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
40 |
in if r = 0 then l' else l' * l end; |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
41 |
in |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
42 |
if k < 0 |
23251 | 43 |
then error "pow: negative exponent" |
23520 | 44 |
else pw k l |
23251 | 45 |
end; |
46 |
||
47 |
fun gcd x y = |
|
48 |
let |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
49 |
fun gxd x y = if y = 0 then x else gxd y (x mod y) |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
50 |
in if x < y then gxd y x else gxd x y end; |
23251 | 51 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
52 |
fun gcds xs = fold gcd xs 0; |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
53 |
|
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
54 |
fun lcm x y = (x * y) div (gcd x y); |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
55 |
fun lcms xs = fold lcm xs 1; |
23251 | 56 |
|
57 |
end; |
|
58 |