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