7 datatype nat = Zero_nat | Suc of nat;
9 fun plus_nat (Suc m) n = plus_nat m (Suc n)
10 | plus_nat Zero_nat n = n;
12 fun op_eq_nat Zero_nat (Suc m) = false
13 | op_eq_nat (Suc n) Zero_nat = false
14 | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m
15 | op_eq_nat Zero_nat Zero_nat = true;
19 structure Code_Generator =
22 type 'a eq = {op_eq : 'a -> 'a -> bool};
23 fun op_eq (A_:'a eq) = #op_eq A_;
25 end; (*struct Code_Generator*)
30 datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 |
31 Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
32 NibbleC | NibbleD | NibbleE | NibbleF;
34 datatype char = Char of nibble * nibble;
36 fun zip xs (y :: ys) =
37 (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
40 fun null (x :: xs) = false
43 fun op_eq_nibble Nibble0 Nibble0 = true
44 | op_eq_nibble Nibble1 Nibble1 = true
45 | op_eq_nibble Nibble2 Nibble2 = true
46 | op_eq_nibble Nibble3 Nibble3 = true
47 | op_eq_nibble Nibble4 Nibble4 = true
48 | op_eq_nibble Nibble5 Nibble5 = true
49 | op_eq_nibble Nibble6 Nibble6 = true
50 | op_eq_nibble Nibble7 Nibble7 = true
51 | op_eq_nibble Nibble8 Nibble8 = true
52 | op_eq_nibble Nibble9 Nibble9 = true
53 | op_eq_nibble NibbleA NibbleA = true
54 | op_eq_nibble NibbleB NibbleB = true
55 | op_eq_nibble NibbleC NibbleC = true
56 | op_eq_nibble NibbleD NibbleD = true
57 | op_eq_nibble NibbleE NibbleE = true
58 | op_eq_nibble NibbleF NibbleF = true
59 | op_eq_nibble Nibble0 Nibble1 = false
60 | op_eq_nibble Nibble0 Nibble2 = false
61 | op_eq_nibble Nibble0 Nibble3 = false
62 | op_eq_nibble Nibble0 Nibble4 = false
63 | op_eq_nibble Nibble0 Nibble5 = false
64 | op_eq_nibble Nibble0 Nibble6 = false
65 | op_eq_nibble Nibble0 Nibble7 = false
66 | op_eq_nibble Nibble0 Nibble8 = false
67 | op_eq_nibble Nibble0 Nibble9 = false
68 | op_eq_nibble Nibble0 NibbleA = false
69 | op_eq_nibble Nibble0 NibbleB = false
70 | op_eq_nibble Nibble0 NibbleC = false
71 | op_eq_nibble Nibble0 NibbleD = false
72 | op_eq_nibble Nibble0 NibbleE = false
73 | op_eq_nibble Nibble0 NibbleF = false
74 | op_eq_nibble Nibble1 Nibble2 = false
75 | op_eq_nibble Nibble1 Nibble3 = false
76 | op_eq_nibble Nibble1 Nibble4 = false
77 | op_eq_nibble Nibble1 Nibble5 = false
78 | op_eq_nibble Nibble1 Nibble6 = false
79 | op_eq_nibble Nibble1 Nibble7 = false
80 | op_eq_nibble Nibble1 Nibble8 = false
81 | op_eq_nibble Nibble1 Nibble9 = false
82 | op_eq_nibble Nibble1 NibbleA = false
83 | op_eq_nibble Nibble1 NibbleB = false
84 | op_eq_nibble Nibble1 NibbleC = false
85 | op_eq_nibble Nibble1 NibbleD = false
86 | op_eq_nibble Nibble1 NibbleE = false
87 | op_eq_nibble Nibble1 NibbleF = false
88 | op_eq_nibble Nibble2 Nibble3 = false
89 | op_eq_nibble Nibble2 Nibble4 = false
90 | op_eq_nibble Nibble2 Nibble5 = false
91 | op_eq_nibble Nibble2 Nibble6 = false
92 | op_eq_nibble Nibble2 Nibble7 = false
93 | op_eq_nibble Nibble2 Nibble8 = false
94 | op_eq_nibble Nibble2 Nibble9 = false
95 | op_eq_nibble Nibble2 NibbleA = false
96 | op_eq_nibble Nibble2 NibbleB = false
97 | op_eq_nibble Nibble2 NibbleC = false
98 | op_eq_nibble Nibble2 NibbleD = false
99 | op_eq_nibble Nibble2 NibbleE = false
100 | op_eq_nibble Nibble2 NibbleF = false
101 | op_eq_nibble Nibble3 Nibble4 = false
102 | op_eq_nibble Nibble3 Nibble5 = false
103 | op_eq_nibble Nibble3 Nibble6 = false
104 | op_eq_nibble Nibble3 Nibble7 = false
105 | op_eq_nibble Nibble3 Nibble8 = false
106 | op_eq_nibble Nibble3 Nibble9 = false
107 | op_eq_nibble Nibble3 NibbleA = false
108 | op_eq_nibble Nibble3 NibbleB = false
109 | op_eq_nibble Nibble3 NibbleC = false
110 | op_eq_nibble Nibble3 NibbleD = false
111 | op_eq_nibble Nibble3 NibbleE = false
112 | op_eq_nibble Nibble3 NibbleF = false
113 | op_eq_nibble Nibble4 Nibble5 = false
114 | op_eq_nibble Nibble4 Nibble6 = false
115 | op_eq_nibble Nibble4 Nibble7 = false
116 | op_eq_nibble Nibble4 Nibble8 = false
117 | op_eq_nibble Nibble4 Nibble9 = false
118 | op_eq_nibble Nibble4 NibbleA = false
119 | op_eq_nibble Nibble4 NibbleB = false
120 | op_eq_nibble Nibble4 NibbleC = false
121 | op_eq_nibble Nibble4 NibbleD = false
122 | op_eq_nibble Nibble4 NibbleE = false
123 | op_eq_nibble Nibble4 NibbleF = false
124 | op_eq_nibble Nibble5 Nibble6 = false
125 | op_eq_nibble Nibble5 Nibble7 = false
126 | op_eq_nibble Nibble5 Nibble8 = false
127 | op_eq_nibble Nibble5 Nibble9 = false
128 | op_eq_nibble Nibble5 NibbleA = false
129 | op_eq_nibble Nibble5 NibbleB = false
130 | op_eq_nibble Nibble5 NibbleC = false
131 | op_eq_nibble Nibble5 NibbleD = false
132 | op_eq_nibble Nibble5 NibbleE = false
133 | op_eq_nibble Nibble5 NibbleF = false
134 | op_eq_nibble Nibble6 Nibble7 = false
135 | op_eq_nibble Nibble6 Nibble8 = false
136 | op_eq_nibble Nibble6 Nibble9 = false
137 | op_eq_nibble Nibble6 NibbleA = false
138 | op_eq_nibble Nibble6 NibbleB = false
139 | op_eq_nibble Nibble6 NibbleC = false
140 | op_eq_nibble Nibble6 NibbleD = false
141 | op_eq_nibble Nibble6 NibbleE = false
142 | op_eq_nibble Nibble6 NibbleF = false
143 | op_eq_nibble Nibble7 Nibble8 = false
144 | op_eq_nibble Nibble7 Nibble9 = false
145 | op_eq_nibble Nibble7 NibbleA = false
146 | op_eq_nibble Nibble7 NibbleB = false
147 | op_eq_nibble Nibble7 NibbleC = false
148 | op_eq_nibble Nibble7 NibbleD = false
149 | op_eq_nibble Nibble7 NibbleE = false
150 | op_eq_nibble Nibble7 NibbleF = false
151 | op_eq_nibble Nibble8 Nibble9 = false
152 | op_eq_nibble Nibble8 NibbleA = false
153 | op_eq_nibble Nibble8 NibbleB = false
154 | op_eq_nibble Nibble8 NibbleC = false
155 | op_eq_nibble Nibble8 NibbleD = false
156 | op_eq_nibble Nibble8 NibbleE = false
157 | op_eq_nibble Nibble8 NibbleF = false
158 | op_eq_nibble Nibble9 NibbleA = false
159 | op_eq_nibble Nibble9 NibbleB = false
160 | op_eq_nibble Nibble9 NibbleC = false
161 | op_eq_nibble Nibble9 NibbleD = false
162 | op_eq_nibble Nibble9 NibbleE = false
163 | op_eq_nibble Nibble9 NibbleF = false
164 | op_eq_nibble NibbleA NibbleB = false
165 | op_eq_nibble NibbleA NibbleC = false
166 | op_eq_nibble NibbleA NibbleD = false
167 | op_eq_nibble NibbleA NibbleE = false
168 | op_eq_nibble NibbleA NibbleF = false
169 | op_eq_nibble NibbleB NibbleC = false
170 | op_eq_nibble NibbleB NibbleD = false
171 | op_eq_nibble NibbleB NibbleE = false
172 | op_eq_nibble NibbleB NibbleF = false
173 | op_eq_nibble NibbleC NibbleD = false
174 | op_eq_nibble NibbleC NibbleE = false
175 | op_eq_nibble NibbleC NibbleF = false
176 | op_eq_nibble NibbleD NibbleE = false
177 | op_eq_nibble NibbleD NibbleF = false
178 | op_eq_nibble NibbleE NibbleF = false
179 | op_eq_nibble Nibble1 Nibble0 = false
180 | op_eq_nibble Nibble2 Nibble0 = false
181 | op_eq_nibble Nibble3 Nibble0 = false
182 | op_eq_nibble Nibble4 Nibble0 = false
183 | op_eq_nibble Nibble5 Nibble0 = false
184 | op_eq_nibble Nibble6 Nibble0 = false
185 | op_eq_nibble Nibble7 Nibble0 = false
186 | op_eq_nibble Nibble8 Nibble0 = false
187 | op_eq_nibble Nibble9 Nibble0 = false
188 | op_eq_nibble NibbleA Nibble0 = false
189 | op_eq_nibble NibbleB Nibble0 = false
190 | op_eq_nibble NibbleC Nibble0 = false
191 | op_eq_nibble NibbleD Nibble0 = false
192 | op_eq_nibble NibbleE Nibble0 = false
193 | op_eq_nibble NibbleF Nibble0 = false
194 | op_eq_nibble Nibble2 Nibble1 = false
195 | op_eq_nibble Nibble3 Nibble1 = false
196 | op_eq_nibble Nibble4 Nibble1 = false
197 | op_eq_nibble Nibble5 Nibble1 = false
198 | op_eq_nibble Nibble6 Nibble1 = false
199 | op_eq_nibble Nibble7 Nibble1 = false
200 | op_eq_nibble Nibble8 Nibble1 = false
201 | op_eq_nibble Nibble9 Nibble1 = false
202 | op_eq_nibble NibbleA Nibble1 = false
203 | op_eq_nibble NibbleB Nibble1 = false
204 | op_eq_nibble NibbleC Nibble1 = false
205 | op_eq_nibble NibbleD Nibble1 = false
206 | op_eq_nibble NibbleE Nibble1 = false
207 | op_eq_nibble NibbleF Nibble1 = false
208 | op_eq_nibble Nibble3 Nibble2 = false
209 | op_eq_nibble Nibble4 Nibble2 = false
210 | op_eq_nibble Nibble5 Nibble2 = false
211 | op_eq_nibble Nibble6 Nibble2 = false
212 | op_eq_nibble Nibble7 Nibble2 = false
213 | op_eq_nibble Nibble8 Nibble2 = false
214 | op_eq_nibble Nibble9 Nibble2 = false
215 | op_eq_nibble NibbleA Nibble2 = false
216 | op_eq_nibble NibbleB Nibble2 = false
217 | op_eq_nibble NibbleC Nibble2 = false
218 | op_eq_nibble NibbleD Nibble2 = false
219 | op_eq_nibble NibbleE Nibble2 = false
220 | op_eq_nibble NibbleF Nibble2 = false
221 | op_eq_nibble Nibble4 Nibble3 = false
222 | op_eq_nibble Nibble5 Nibble3 = false
223 | op_eq_nibble Nibble6 Nibble3 = false
224 | op_eq_nibble Nibble7 Nibble3 = false
225 | op_eq_nibble Nibble8 Nibble3 = false
226 | op_eq_nibble Nibble9 Nibble3 = false
227 | op_eq_nibble NibbleA Nibble3 = false
228 | op_eq_nibble NibbleB Nibble3 = false
229 | op_eq_nibble NibbleC Nibble3 = false
230 | op_eq_nibble NibbleD Nibble3 = false
231 | op_eq_nibble NibbleE Nibble3 = false
232 | op_eq_nibble NibbleF Nibble3 = false
233 | op_eq_nibble Nibble5 Nibble4 = false
234 | op_eq_nibble Nibble6 Nibble4 = false
235 | op_eq_nibble Nibble7 Nibble4 = false
236 | op_eq_nibble Nibble8 Nibble4 = false
237 | op_eq_nibble Nibble9 Nibble4 = false
238 | op_eq_nibble NibbleA Nibble4 = false
239 | op_eq_nibble NibbleB Nibble4 = false
240 | op_eq_nibble NibbleC Nibble4 = false
241 | op_eq_nibble NibbleD Nibble4 = false
242 | op_eq_nibble NibbleE Nibble4 = false
243 | op_eq_nibble NibbleF Nibble4 = false
244 | op_eq_nibble Nibble6 Nibble5 = false
245 | op_eq_nibble Nibble7 Nibble5 = false
246 | op_eq_nibble Nibble8 Nibble5 = false
247 | op_eq_nibble Nibble9 Nibble5 = false
248 | op_eq_nibble NibbleA Nibble5 = false
249 | op_eq_nibble NibbleB Nibble5 = false
250 | op_eq_nibble NibbleC Nibble5 = false
251 | op_eq_nibble NibbleD Nibble5 = false
252 | op_eq_nibble NibbleE Nibble5 = false
253 | op_eq_nibble NibbleF Nibble5 = false
254 | op_eq_nibble Nibble7 Nibble6 = false
255 | op_eq_nibble Nibble8 Nibble6 = false
256 | op_eq_nibble Nibble9 Nibble6 = false
257 | op_eq_nibble NibbleA Nibble6 = false
258 | op_eq_nibble NibbleB Nibble6 = false
259 | op_eq_nibble NibbleC Nibble6 = false
260 | op_eq_nibble NibbleD Nibble6 = false
261 | op_eq_nibble NibbleE Nibble6 = false
262 | op_eq_nibble NibbleF Nibble6 = false
263 | op_eq_nibble Nibble8 Nibble7 = false
264 | op_eq_nibble Nibble9 Nibble7 = false
265 | op_eq_nibble NibbleA Nibble7 = false
266 | op_eq_nibble NibbleB Nibble7 = false
267 | op_eq_nibble NibbleC Nibble7 = false
268 | op_eq_nibble NibbleD Nibble7 = false
269 | op_eq_nibble NibbleE Nibble7 = false
270 | op_eq_nibble NibbleF Nibble7 = false
271 | op_eq_nibble Nibble9 Nibble8 = false
272 | op_eq_nibble NibbleA Nibble8 = false
273 | op_eq_nibble NibbleB Nibble8 = false
274 | op_eq_nibble NibbleC Nibble8 = false
275 | op_eq_nibble NibbleD Nibble8 = false
276 | op_eq_nibble NibbleE Nibble8 = false
277 | op_eq_nibble NibbleF Nibble8 = false
278 | op_eq_nibble NibbleA Nibble9 = false
279 | op_eq_nibble NibbleB Nibble9 = false
280 | op_eq_nibble NibbleC Nibble9 = false
281 | op_eq_nibble NibbleD Nibble9 = false
282 | op_eq_nibble NibbleE Nibble9 = false
283 | op_eq_nibble NibbleF Nibble9 = false
284 | op_eq_nibble NibbleB NibbleA = false
285 | op_eq_nibble NibbleC NibbleA = false
286 | op_eq_nibble NibbleD NibbleA = false
287 | op_eq_nibble NibbleE NibbleA = false
288 | op_eq_nibble NibbleF NibbleA = false
289 | op_eq_nibble NibbleC NibbleB = false
290 | op_eq_nibble NibbleD NibbleB = false
291 | op_eq_nibble NibbleE NibbleB = false
292 | op_eq_nibble NibbleF NibbleB = false
293 | op_eq_nibble NibbleD NibbleC = false
294 | op_eq_nibble NibbleE NibbleC = false
295 | op_eq_nibble NibbleF NibbleC = false
296 | op_eq_nibble NibbleE NibbleD = false
297 | op_eq_nibble NibbleF NibbleD = false
298 | op_eq_nibble NibbleF NibbleE = false;
300 fun op_eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) =
301 op_eq_nibble nibble1 nibble1' andalso op_eq_nibble nibble2 nibble2';
303 val eq_char = {op_eq = op_eq_char} : char Code_Generator.eq;
305 fun list_all p (x :: xs) = p x andalso list_all p xs
306 | list_all p [] = true;
308 fun size_list (a :: lista) =
309 Nat.plus_nat (size_list lista) (Nat.Suc Nat.Zero_nat)
310 | size_list [] = Nat.Zero_nat;
312 fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
313 | list_all2 p xs [] = null xs
314 | list_all2 p [] ys = null ys
315 | list_all2 p xs ys =
316 Nat.op_eq_nat (size_list xs) (size_list ys) andalso
317 list_all (fn a as (aa, b) => p aa b) (zip xs ys);
319 fun op_eq_list A_ [] [] = true
320 | op_eq_list A_ (a :: lista) (a' :: list') =
321 Code_Generator.op_eq A_ a a' andalso op_eq_list A_ lista list'
322 | op_eq_list A_ [] (a :: b) = false
323 | op_eq_list A_ (a :: b) [] = false;
330 datatype monotype = Mono of List.char list * monotype list;
332 fun op_eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
333 List.op_eq_list List.eq_char tyco1 tyco2 andalso
334 List.list_all2 op_eq_monotype typargs1 typargs2;
336 end; (*struct Codegen*)