9 end; (*struct Nat*) |
9 end; (*struct Nat*) |
10 |
10 |
11 structure Integer = |
11 structure Integer = |
12 struct |
12 struct |
13 |
13 |
|
14 datatype bit = B0 | B1; |
|
15 |
|
16 datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; |
|
17 |
|
18 fun pred (Bit (k, B0)) = Bit (pred k, B1) |
|
19 | pred (Bit (k, B1)) = Bit (k, B0) |
|
20 | pred Min = Bit (Min, B0) |
|
21 | pred Pls = Min; |
|
22 |
|
23 fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) |
|
24 | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) |
|
25 | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) |
|
26 | uminus_int Min = Bit (Pls, B1) |
|
27 | uminus_int Pls = Pls; |
|
28 |
|
29 fun succ (Bit (k, B0)) = Bit (k, B1) |
|
30 | succ (Bit (k, B1)) = Bit (succ k, B0) |
|
31 | succ Min = Pls |
|
32 | succ Pls = Bit (Pls, B1); |
|
33 |
|
34 fun plus_int (Number_of_int v) (Number_of_int w) = |
|
35 Number_of_int (plus_int v w) |
|
36 | plus_int k Min = pred k |
|
37 | plus_int k Pls = k |
|
38 | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) |
|
39 | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) |
|
40 | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) |
|
41 | plus_int Min k = pred k |
|
42 | plus_int Pls k = k; |
|
43 |
|
44 fun minus_int (Number_of_int v) (Number_of_int w) = |
|
45 Number_of_int (plus_int v (uminus_int w)) |
|
46 | minus_int z w = plus_int z (uminus_int w); |
|
47 |
|
48 fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l |
|
49 | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2 |
|
50 | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2 |
|
51 | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2 |
|
52 | less_eq_int (Bit (k, v)) Min = less_eq_int k Min |
|
53 | less_eq_int (Bit (k, B1)) Pls = less_int k Pls |
|
54 | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls |
|
55 | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k |
|
56 | less_eq_int Min (Bit (k, B0)) = less_int Min k |
|
57 | less_eq_int Min Min = true |
|
58 | less_eq_int Min Pls = true |
|
59 | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k |
|
60 | less_eq_int Pls Min = false |
|
61 | less_eq_int Pls Pls = true |
|
62 and less_int (Number_of_int k) (Number_of_int l) = less_int k l |
|
63 | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2 |
|
64 | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2 |
|
65 | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2 |
|
66 | less_int (Bit (k, B1)) Min = less_int k Min |
|
67 | less_int (Bit (k, B0)) Min = less_eq_int k Min |
|
68 | less_int (Bit (k, v)) Pls = less_int k Pls |
|
69 | less_int Min (Bit (k, v)) = less_int Min k |
|
70 | less_int Min Min = false |
|
71 | less_int Min Pls = true |
|
72 | less_int Pls (Bit (k, B1)) = less_eq_int Pls k |
|
73 | less_int Pls (Bit (k, B0)) = less_int Pls k |
|
74 | less_int Pls Min = false |
|
75 | less_int Pls Pls = false; |
|
76 |
14 fun nat_aux n i = |
77 fun nat_aux n i = |
15 (if IntInf.<= (i, (0 : IntInf.int)) then n |
78 (if less_eq_int i (Number_of_int Pls) then n |
16 else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int)))); |
79 else nat_aux (Nat.Suc n) |
|
80 (minus_int i (Number_of_int (Bit (Pls, B1))))); |
17 |
81 |
18 fun nat i = nat_aux Nat.Zero_nat i; |
82 fun nat i = nat_aux Nat.Zero_nat i; |
19 |
83 |
20 end; (*struct Integer*) |
84 end; (*struct Integer*) |
21 |
85 |
32 |
96 |
33 type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a}; |
97 type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a}; |
34 fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; |
98 fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; |
35 fun inverse (A_:'a group) = #inverse A_; |
99 fun inverse (A_:'a group) = #inverse A_; |
36 |
100 |
37 fun inverse_int i = IntInf.~ i; |
101 fun inverse_int i = Integer.uminus_int i; |
38 |
102 |
39 val neutral_int : IntInf.int = (0 : IntInf.int); |
103 val neutral_int : Integer.int = Integer.Number_of_int Integer.Pls; |
40 |
104 |
41 fun mult_int i j = IntInf.+ (i, j); |
105 fun mult_int i j = Integer.plus_int i j; |
42 |
106 |
43 val semigroup_int = {mult = mult_int} : IntInf.int semigroup; |
107 val semigroup_int = {mult = mult_int} : Integer.int semigroup; |
44 |
108 |
45 val monoidl_int = |
109 val monoidl_int = |
46 {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} : |
110 {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} : |
47 IntInf.int monoidl; |
111 Integer.int monoidl; |
48 |
112 |
49 val group_int = |
113 val group_int = |
50 {Classes__group_monoidl = monoidl_int, inverse = inverse_int} : |
114 {Classes__group_monoidl = monoidl_int, inverse = inverse_int} : |
51 IntInf.int group; |
115 Integer.int group; |
52 |
116 |
53 fun pow_nat A_ (Nat.Suc n) x = |
117 fun pow_nat B_ (Nat.Suc n) x = |
54 mult (monoidl_semigroup A_) x (pow_nat A_ n x) |
118 mult (monoidl_semigroup B_) x (pow_nat B_ n x) |
55 | pow_nat A_ Nat.Zero_nat x = neutral A_; |
119 | pow_nat B_ Nat.Zero_nat x = neutral B_; |
56 |
120 |
57 fun pow_int A_ k x = |
121 fun pow_int A_ k x = |
58 (if IntInf.<= ((0 : IntInf.int), k) |
122 (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k |
59 then pow_nat (group_monoidl A_) (Integer.nat k) x |
123 then pow_nat (group_monoidl A_) (Integer.nat k) x |
60 else inverse A_ |
124 else inverse A_ |
61 (pow_nat (group_monoidl A_) (Integer.nat (IntInf.~ k)) x)); |
125 (pow_nat (group_monoidl A_) |
|
126 (Integer.nat (Integer.uminus_int k)) x)); |
62 |
127 |
63 val example : IntInf.int = |
128 val example : Integer.int = |
64 pow_int group_int (10 : IntInf.int) (~2 : IntInf.int); |
129 pow_int group_int |
|
130 (Integer.Number_of_int |
|
131 (Integer.Bit |
|
132 (Integer.Bit |
|
133 (Integer.Bit |
|
134 (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0), |
|
135 Integer.B1), |
|
136 Integer.B0))) |
|
137 (Integer.Number_of_int (Integer.Bit (Integer.Min, Integer.B0))); |
65 |
138 |
66 end; (*struct Classes*) |
139 end; (*struct Classes*) |
67 |
140 |
68 end; (*struct ROOT*) |
141 end; (*struct ROOT*) |