1 structure ROOT = |
1 structure Classes = |
2 struct |
|
3 |
|
4 structure Nat = |
|
5 struct |
2 struct |
6 |
3 |
7 datatype nat = Zero_nat | Suc of nat; |
4 datatype nat = Zero_nat | Suc of nat; |
8 |
5 |
9 end; (*struct Nat*) |
|
10 |
|
11 structure Integer = |
|
12 struct |
|
13 |
|
14 datatype bit = B0 | B1; |
6 datatype bit = B0 | B1; |
15 |
7 |
16 datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; |
8 fun nat_aux i n = |
|
9 (if IntInf.<= (i, (0 : IntInf.int)) then n |
|
10 else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n)); |
17 |
11 |
18 fun pred (Bit (k, B0)) = Bit (pred k, B1) |
12 fun nat i = nat_aux i Zero_nat; |
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 |
|
77 fun nat_aux n i = |
|
78 (if less_eq_int i (Number_of_int Pls) then n |
|
79 else nat_aux (Nat.Suc n) |
|
80 (minus_int i (Number_of_int (Bit (Pls, B1))))); |
|
81 |
|
82 fun nat i = nat_aux Nat.Zero_nat i; |
|
83 |
|
84 end; (*struct Integer*) |
|
85 |
|
86 structure Classes = |
|
87 struct |
|
88 |
13 |
89 type 'a semigroup = {mult : 'a -> 'a -> 'a}; |
14 type 'a semigroup = {mult : 'a -> 'a -> 'a}; |
90 fun mult (A_:'a semigroup) = #mult A_; |
15 fun mult (A_:'a semigroup) = #mult A_; |
91 |
16 |
92 type 'a monoidl = |
17 type 'a monoidl = |
93 {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a}; |
18 {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a}; |
94 fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_; |
19 fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_; |
95 fun neutral (A_:'a monoidl) = #neutral A_; |
20 fun neutral (A_:'a monoidl) = #neutral A_; |
96 |
21 |
97 type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a}; |
22 type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a}; |
98 fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; |
23 fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_; |
99 fun inverse (A_:'a group) = #inverse A_; |
24 fun inverse (A_:'a group) = #inverse A_; |
100 |
25 |
101 fun inverse_int i = Integer.uminus_int i; |
26 fun inverse_int i = IntInf.~ i; |
102 |
27 |
103 val neutral_int : Integer.int = Integer.Number_of_int Integer.Pls; |
28 val neutral_int : IntInf.int = (0 : IntInf.int); |
104 |
29 |
105 fun mult_int i j = Integer.plus_int i j; |
30 fun mult_int i j = IntInf.+ (i, j); |
106 |
31 |
107 val semigroup_int = {mult = mult_int} : Integer.int semigroup; |
32 val semigroup_int = {mult = mult_int} : IntInf.int semigroup; |
108 |
33 |
109 val monoidl_int = |
34 val monoidl_int = |
110 {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} : |
35 {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} : |
111 Integer.int monoidl; |
36 IntInf.int monoidl; |
112 |
37 |
113 val group_int = |
38 val group_int = |
114 {Classes__group_monoidl = monoidl_int, inverse = inverse_int} : |
39 {Classes__monoidl_group = monoidl_int, inverse = inverse_int} : |
115 Integer.int group; |
40 IntInf.int group; |
116 |
41 |
117 fun pow_nat B_ (Nat.Suc n) x = |
42 fun pow_nat B_ (Suc n) x = |
118 mult (monoidl_semigroup B_) x (pow_nat B_ n x) |
43 mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x) |
119 | pow_nat B_ Nat.Zero_nat x = neutral B_; |
44 | pow_nat B_ Zero_nat x = neutral (monoidl_group B_); |
120 |
45 |
121 fun pow_int A_ k x = |
46 fun pow_int A_ k x = |
122 (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k |
47 (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x |
123 then pow_nat (group_monoidl A_) (Integer.nat k) x |
48 else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x)); |
124 else inverse A_ |
|
125 (pow_nat (group_monoidl A_) |
|
126 (Integer.nat (Integer.uminus_int k)) x)); |
|
127 |
49 |
128 val example : Integer.int = |
50 val example : IntInf.int = |
129 pow_int group_int |
51 pow_int group_int (10 : IntInf.int) (~2 : IntInf.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))); |
|
138 |
52 |
139 end; (*struct Classes*) |
53 end; (*struct Classes*) |
140 |
|
141 end; (*struct ROOT*) |
|