Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/benchmarks/todo/vboyer/rules.sml
ViewVC logotype

Annotation of /sml/trunk/benchmarks/todo/vboyer/rules.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 193 - (view) (download)

1 : monnier 193 (* rules.sml:
2 :     *)
3 :    
4 :     structure Rules =
5 :     struct
6 :    
7 :     open Terms;
8 :    
9 :     datatype cterm = CVar of int | CProp of string * cterm list;
10 :    
11 :     fun cterm_to_term (CVar v) = Var v
12 :     | cterm_to_term (CProp(p, l)) = Prop(get p, Vector.vector(map cterm_to_term l))
13 :    
14 :     fun add t = add_lemma (cterm_to_term t)
15 :    
16 :     val _ = (
17 :     add (CProp
18 :     ("equal",
19 :     [CProp ("compile",[CVar 5]),
20 :     CProp
21 :     ("reverse",
22 :     [CProp ("codegen",[CProp ("optimize",[CVar 5]), CProp ("nil",[])])])]));
23 :     add (CProp
24 :     ("equal",
25 :     [CProp ("eqp",[CVar 23, CVar 24]),
26 :     CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 24])])]));
27 :     add (CProp
28 :     ("equal",
29 :     [CProp ("gt",[CVar 23, CVar 24]), CProp ("lt",[CVar 24, CVar 23])]));
30 :     add (CProp
31 :     ("equal",
32 :     [CProp ("le",[CVar 23, CVar 24]), CProp ("ge",[CVar 24, CVar 23])]));
33 :     add (CProp
34 :     ("equal",
35 :     [CProp ("ge",[CVar 23, CVar 24]), CProp ("le",[CVar 24, CVar 23])]));
36 :     add (CProp
37 :     ("equal",
38 :     [CProp ("boolean",[CVar 23]),
39 :     CProp
40 :     ("or",
41 :     [CProp ("equal",[CVar 23, CProp ("true",[])]),
42 :     CProp ("equal",[CVar 23, CProp ("false",[])])])]));
43 :     add (CProp
44 :     ("equal",
45 :     [CProp ("iff",[CVar 23, CVar 24]),
46 :     CProp
47 :     ("and",
48 :     [CProp ("implies",[CVar 23, CVar 24]),
49 :     CProp ("implies",[CVar 24, CVar 23])])]));
50 :     add (CProp
51 :     ("equal",
52 :     [CProp ("even1",[CVar 23]),
53 :     CProp
54 :     ("if",
55 :     [CProp ("zerop",[CVar 23]), CProp ("true",[]),
56 :     CProp ("odd",[CProp ("sub1",[CVar 23])])])]));
57 :     add (CProp
58 :     ("equal",
59 :     [CProp ("countps_",[CVar 11, CVar 15]),
60 :     CProp ("countps_loop",[CVar 11, CVar 15, CProp ("zero",[])])]));
61 :     add (CProp
62 :     ("equal",
63 :     [CProp ("fact_",[CVar 8]),
64 :     CProp ("fact_loop",[CVar 8, CProp ("one",[])])]));
65 :     add (CProp
66 :     ("equal",
67 :     [CProp ("reverse_",[CVar 23]),
68 :     CProp ("reverse_loop",[CVar 23, CProp ("nil",[])])]));
69 :     add (CProp
70 :     ("equal",
71 :     [CProp ("divides",[CVar 23, CVar 24]),
72 :     CProp ("zerop",[CProp ("remainder",[CVar 24, CVar 23])])]));
73 :     add (CProp
74 :     ("equal",
75 :     [CProp ("assume_true",[CVar 21, CVar 0]),
76 :     CProp ("cons",[CProp ("cons",[CVar 21, CProp ("true",[])]), CVar 0])]));
77 :     add (CProp
78 :     ("equal",
79 :     [CProp ("assume_false",[CVar 21, CVar 0]),
80 :     CProp ("cons",[CProp ("cons",[CVar 21, CProp ("false",[])]), CVar 0])]));
81 :     add (CProp
82 :     ("equal",
83 :     [CProp ("tautology_checker",[CVar 23]),
84 :     CProp ("tautologyp",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
85 :     add (CProp
86 :     ("equal",
87 :     [CProp ("falsify",[CVar 23]),
88 :     CProp ("falsify1",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
89 :     add (CProp
90 :     ("equal",
91 :     [CProp ("prime",[CVar 23]),
92 :     CProp
93 :     ("and",
94 :     [CProp ("not",[CProp ("zerop",[CVar 23])]),
95 :     CProp
96 :     ("not",
97 :     [CProp ("equal",[CVar 23, CProp ("add1",[CProp ("zero",[])])])]),
98 :     CProp ("prime1",[CVar 23, CProp ("sub1",[CVar 23])])])]));
99 :     add (CProp
100 :     ("equal",
101 :     [CProp ("and",[CVar 15, CVar 16]),
102 :     CProp
103 :     ("if",
104 :     [CVar 15,
105 :     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
106 :     CProp ("false",[])])]));
107 :     add (CProp
108 :     ("equal",
109 :     [CProp ("or",[CVar 15, CVar 16]),
110 :     CProp
111 :     ("if",
112 :     [CVar 15, CProp ("true",[]),
113 :     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
114 :     CProp ("false",[])])]));
115 :     add (CProp
116 :     ("equal",
117 :     [CProp ("not",[CVar 15]),
118 :     CProp ("if",[CVar 15, CProp ("false",[]), CProp ("true",[])])]));
119 :     add (CProp
120 :     ("equal",
121 :     [CProp ("implies",[CVar 15, CVar 16]),
122 :     CProp
123 :     ("if",
124 :     [CVar 15,
125 :     CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
126 :     CProp ("true",[])])]));
127 :     add (CProp
128 :     ("equal",
129 :     [CProp ("fix",[CVar 23]),
130 :     CProp ("if",[CProp ("numberp",[CVar 23]), CVar 23, CProp ("zero",[])])]));
131 :     add (CProp
132 :     ("equal",
133 :     [CProp ("if",[CProp ("if",[CVar 0, CVar 1, CVar 2]), CVar 3, CVar 4]),
134 :     CProp
135 :     ("if",
136 :     [CVar 0, CProp ("if",[CVar 1, CVar 3, CVar 4]),
137 :     CProp ("if",[CVar 2, CVar 3, CVar 4])])]));
138 :     add (CProp
139 :     ("equal",
140 :     [CProp ("zerop",[CVar 23]),
141 :     CProp
142 :     ("or",
143 :     [CProp ("equal",[CVar 23, CProp ("zero",[])]),
144 :     CProp ("not",[CProp ("numberp",[CVar 23])])])]));
145 :     add (CProp
146 :     ("equal",
147 :     [CProp ("plus",[CProp ("plus",[CVar 23, CVar 24]), CVar 25]),
148 :     CProp ("plus",[CVar 23, CProp ("plus",[CVar 24, CVar 25])])]));
149 :     add (CProp
150 :     ("equal",
151 :     [CProp ("equal",[CProp ("plus",[CVar 0, CVar 1]), CProp ("zero",[])]),
152 :     CProp ("and",[CProp ("zerop",[CVar 0]), CProp ("zerop",[CVar 1])])]));
153 :     add (CProp
154 :     ("equal",[CProp ("difference",[CVar 23, CVar 23]), CProp ("zero",[])]));
155 :     add (CProp
156 :     ("equal",
157 :     [CProp
158 :     ("equal",
159 :     [CProp ("plus",[CVar 0, CVar 1]), CProp ("plus",[CVar 0, CVar 2])]),
160 :     CProp ("equal",[CProp ("fix",[CVar 1]), CProp ("fix",[CVar 2])])]));
161 :     add (CProp
162 :     ("equal",
163 :     [CProp
164 :     ("equal",[CProp ("zero",[]), CProp ("difference",[CVar 23, CVar 24])]),
165 :     CProp ("not",[CProp ("gt",[CVar 24, CVar 23])])]));
166 :     add (CProp
167 :     ("equal",
168 :     [CProp ("equal",[CVar 23, CProp ("difference",[CVar 23, CVar 24])]),
169 :     CProp
170 :     ("and",
171 :     [CProp ("numberp",[CVar 23]),
172 :     CProp
173 :     ("or",
174 :     [CProp ("equal",[CVar 23, CProp ("zero",[])]),
175 :     CProp ("zerop",[CVar 24])])])]));
176 :     add (CProp
177 :     ("equal",
178 :     [CProp
179 :     ("meaning",
180 :     [CProp ("plus_tree",[CProp ("append",[CVar 23, CVar 24])]), CVar 0]),
181 :     CProp
182 :     ("plus",
183 :     [CProp ("meaning",[CProp ("plus_tree",[CVar 23]), CVar 0]),
184 :     CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
185 :     add (CProp
186 :     ("equal",
187 :     [CProp
188 :     ("meaning",
189 :     [CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]), CVar 0]),
190 :     CProp ("fix",[CProp ("meaning",[CVar 23, CVar 0])])]));
191 :     add (CProp
192 :     ("equal",
193 :     [CProp ("append",[CProp ("append",[CVar 23, CVar 24]), CVar 25]),
194 :     CProp ("append",[CVar 23, CProp ("append",[CVar 24, CVar 25])])]));
195 :     add (CProp
196 :     ("equal",
197 :     [CProp ("reverse",[CProp ("append",[CVar 0, CVar 1])]),
198 :     CProp
199 :     ("append",[CProp ("reverse",[CVar 1]), CProp ("reverse",[CVar 0])])]));
200 :     add (CProp
201 :     ("equal",
202 :     [CProp ("times",[CVar 23, CProp ("plus",[CVar 24, CVar 25])]),
203 :     CProp
204 :     ("plus",
205 :     [CProp ("times",[CVar 23, CVar 24]),
206 :     CProp ("times",[CVar 23, CVar 25])])]));
207 :     add (CProp
208 :     ("equal",
209 :     [CProp ("times",[CProp ("times",[CVar 23, CVar 24]), CVar 25]),
210 :     CProp ("times",[CVar 23, CProp ("times",[CVar 24, CVar 25])])]));
211 :     add (CProp
212 :     ("equal",
213 :     [CProp
214 :     ("equal",[CProp ("times",[CVar 23, CVar 24]), CProp ("zero",[])]),
215 :     CProp ("or",[CProp ("zerop",[CVar 23]), CProp ("zerop",[CVar 24])])]));
216 :     add (CProp
217 :     ("equal",
218 :     [CProp ("exec",[CProp ("append",[CVar 23, CVar 24]), CVar 15, CVar 4]),
219 :     CProp
220 :     ("exec",[CVar 24, CProp ("exec",[CVar 23, CVar 15, CVar 4]), CVar 4])]));
221 :     add (CProp
222 :     ("equal",
223 :     [CProp ("mc_flatten",[CVar 23, CVar 24]),
224 :     CProp ("append",[CProp ("flatten",[CVar 23]), CVar 24])]));
225 :     add (CProp
226 :     ("equal",
227 :     [CProp ("member",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
228 :     CProp
229 :     ("or",
230 :     [CProp ("member",[CVar 23, CVar 0]),
231 :     CProp ("member",[CVar 23, CVar 1])])]));
232 :     add (CProp
233 :     ("equal",
234 :     [CProp ("member",[CVar 23, CProp ("reverse",[CVar 24])]),
235 :     CProp ("member",[CVar 23, CVar 24])]));
236 :     add (CProp
237 :     ("equal",
238 :     [CProp ("length",[CProp ("reverse",[CVar 23])]),
239 :     CProp ("length",[CVar 23])]));
240 :     add (CProp
241 :     ("equal",
242 :     [CProp ("member",[CVar 0, CProp ("intersect",[CVar 1, CVar 2])]),
243 :     CProp
244 :     ("and",
245 :     [CProp ("member",[CVar 0, CVar 1]), CProp ("member",[CVar 0, CVar 2])])]));
246 :     add (CProp
247 :     ("equal",[CProp ("nth",[CProp ("zero",[]), CVar 8]), CProp ("zero",[])]));
248 :     add (CProp
249 :     ("equal",
250 :     [CProp ("exp",[CVar 8, CProp ("plus",[CVar 9, CVar 10])]),
251 :     CProp
252 :     ("times",
253 :     [CProp ("exp",[CVar 8, CVar 9]), CProp ("exp",[CVar 8, CVar 10])])]));
254 :     add (CProp
255 :     ("equal",
256 :     [CProp ("exp",[CVar 8, CProp ("times",[CVar 9, CVar 10])]),
257 :     CProp ("exp",[CProp ("exp",[CVar 8, CVar 9]), CVar 10])]));
258 :     add (CProp
259 :     ("equal",
260 :     [CProp ("reverse_loop",[CVar 23, CVar 24]),
261 :     CProp ("append",[CProp ("reverse",[CVar 23]), CVar 24])]));
262 :     add (CProp
263 :     ("equal",
264 :     [CProp ("reverse_loop",[CVar 23, CProp ("nil",[])]),
265 :     CProp ("reverse",[CVar 23])]));
266 :     add (CProp
267 :     ("equal",
268 :     [CProp ("count_list",[CVar 25, CProp ("sort_lp",[CVar 23, CVar 24])]),
269 :     CProp
270 :     ("plus",
271 :     [CProp ("count_list",[CVar 25, CVar 23]),
272 :     CProp ("count_list",[CVar 25, CVar 24])])]));
273 :     add (CProp
274 :     ("equal",
275 :     [CProp
276 :     ("equal",
277 :     [CProp ("append",[CVar 0, CVar 1]), CProp ("append",[CVar 0, CVar 2])]),
278 :     CProp ("equal",[CVar 1, CVar 2])]));
279 :     add (CProp
280 :     ("equal",
281 :     [CProp
282 :     ("plus",
283 :     [CProp ("remainder",[CVar 23, CVar 24]),
284 :     CProp ("times",[CVar 24, CProp ("quotient",[CVar 23, CVar 24])])]),
285 :     CProp ("fix",[CVar 23])]));
286 :     add (CProp
287 :     ("equal",
288 :     [CProp
289 :     ("power_eval",[CProp ("big_plus",[CVar 11, CVar 8, CVar 1]), CVar 1]),
290 :     CProp ("plus",[CProp ("power_eval",[CVar 11, CVar 1]), CVar 8])]));
291 :     add (CProp
292 :     ("equal",
293 :     [CProp
294 :     ("power_eval",
295 :     [CProp ("big_plus",[CVar 23, CVar 24, CVar 8, CVar 1]), CVar 1]),
296 :     CProp
297 :     ("plus",
298 :     [CVar 8,
299 :     CProp
300 :     ("plus",
301 :     [CProp ("power_eval",[CVar 23, CVar 1]),
302 :     CProp ("power_eval",[CVar 24, CVar 1])])])]));
303 :     add (CProp
304 :     ("equal",
305 :     [CProp ("remainder",[CVar 24, CProp ("one",[])]), CProp ("zero",[])]));
306 :     add (CProp
307 :     ("equal",
308 :     [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 24]),
309 :     CProp ("not",[CProp ("zerop",[CVar 24])])]));
310 :     add (CProp
311 :     ("equal",[CProp ("remainder",[CVar 23, CVar 23]), CProp ("zero",[])]));
312 :     add (CProp
313 :     ("equal",
314 :     [CProp ("lt",[CProp ("quotient",[CVar 8, CVar 9]), CVar 8]),
315 :     CProp
316 :     ("and",
317 :     [CProp ("not",[CProp ("zerop",[CVar 8])]),
318 :     CProp
319 :     ("or",
320 :     [CProp ("zerop",[CVar 9]),
321 :     CProp ("not",[CProp ("equal",[CVar 9, CProp ("one",[])])])])])]));
322 :     add (CProp
323 :     ("equal",
324 :     [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 23]),
325 :     CProp
326 :     ("and",
327 :     [CProp ("not",[CProp ("zerop",[CVar 24])]),
328 :     CProp ("not",[CProp ("zerop",[CVar 23])]),
329 :     CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])])]));
330 :     add (CProp
331 :     ("equal",
332 :     [CProp ("power_eval",[CProp ("power_rep",[CVar 8, CVar 1]), CVar 1]),
333 :     CProp ("fix",[CVar 8])]));
334 :     add (CProp
335 :     ("equal",
336 :     [CProp
337 :     ("power_eval",
338 :     [CProp
339 :     ("big_plus",
340 :     [CProp ("power_rep",[CVar 8, CVar 1]),
341 :     CProp ("power_rep",[CVar 9, CVar 1]), CProp ("zero",[]),
342 :     CVar 1]),
343 :     CVar 1]),
344 :     CProp ("plus",[CVar 8, CVar 9])]));
345 :     add (CProp
346 :     ("equal",
347 :     [CProp ("gcd",[CVar 23, CVar 24]), CProp ("gcd",[CVar 24, CVar 23])]));
348 :     add (CProp
349 :     ("equal",
350 :     [CProp ("nth",[CProp ("append",[CVar 0, CVar 1]), CVar 8]),
351 :     CProp
352 :     ("append",
353 :     [CProp ("nth",[CVar 0, CVar 8]),
354 :     CProp
355 :     ("nth",
356 :     [CVar 1, CProp ("difference",[CVar 8, CProp ("length",[CVar 0])])])])]));
357 :     add (CProp
358 :     ("equal",
359 :     [CProp ("difference",[CProp ("plus",[CVar 23, CVar 24]), CVar 23]),
360 :     CProp ("fix",[CVar 24])]));
361 :     add (CProp
362 :     ("equal",
363 :     [CProp ("difference",[CProp ("plus",[CVar 24, CVar 23]), CVar 23]),
364 :     CProp ("fix",[CVar 24])]));
365 :     add (CProp
366 :     ("equal",
367 :     [CProp
368 :     ("difference",
369 :     [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
370 :     CProp ("difference",[CVar 24, CVar 25])]));
371 :     add (CProp
372 :     ("equal",
373 :     [CProp ("times",[CVar 23, CProp ("difference",[CVar 2, CVar 22])]),
374 :     CProp
375 :     ("difference",
376 :     [CProp ("times",[CVar 2, CVar 23]),
377 :     CProp ("times",[CVar 22, CVar 23])])]));
378 :     add (CProp
379 :     ("equal",
380 :     [CProp ("remainder",[CProp ("times",[CVar 23, CVar 25]), CVar 25]),
381 :     CProp ("zero",[])]));
382 :     add (CProp
383 :     ("equal",
384 :     [CProp
385 :     ("difference",
386 :     [CProp ("plus",[CVar 1, CProp ("plus",[CVar 0, CVar 2])]), CVar 0]),
387 :     CProp ("plus",[CVar 1, CVar 2])]));
388 :     add (CProp
389 :     ("equal",
390 :     [CProp
391 :     ("difference",
392 :     [CProp ("add1",[CProp ("plus",[CVar 24, CVar 25])]), CVar 25]),
393 :     CProp ("add1",[CVar 24])]));
394 :     add (CProp
395 :     ("equal",
396 :     [CProp
397 :     ("lt",
398 :     [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
399 :     CProp ("lt",[CVar 24, CVar 25])]));
400 :     add (CProp
401 :     ("equal",
402 :     [CProp
403 :     ("lt",
404 :     [CProp ("times",[CVar 23, CVar 25]),
405 :     CProp ("times",[CVar 24, CVar 25])]),
406 :     CProp
407 :     ("and",
408 :     [CProp ("not",[CProp ("zerop",[CVar 25])]),
409 :     CProp ("lt",[CVar 23, CVar 24])])]));
410 :     add (CProp
411 :     ("equal",
412 :     [CProp ("lt",[CVar 24, CProp ("plus",[CVar 23, CVar 24])]),
413 :     CProp ("not",[CProp ("zerop",[CVar 23])])]));
414 :     add (CProp
415 :     ("equal",
416 :     [CProp
417 :     ("gcd",
418 :     [CProp ("times",[CVar 23, CVar 25]),
419 :     CProp ("times",[CVar 24, CVar 25])]),
420 :     CProp ("times",[CVar 25, CProp ("gcd",[CVar 23, CVar 24])])]));
421 :     add (CProp
422 :     ("equal",
423 :     [CProp ("value",[CProp ("normalize",[CVar 23]), CVar 0]),
424 :     CProp ("value",[CVar 23, CVar 0])]));
425 :     add (CProp
426 :     ("equal",
427 :     [CProp
428 :     ("equal",
429 :     [CProp ("flatten",[CVar 23]),
430 :     CProp ("cons",[CVar 24, CProp ("nil",[])])]),
431 :     CProp
432 :     ("and",
433 :     [CProp ("nlistp",[CVar 23]), CProp ("equal",[CVar 23, CVar 24])])]));
434 :     add (CProp
435 :     ("equal",
436 :     [CProp ("listp",[CProp ("gother",[CVar 23])]),
437 :     CProp ("listp",[CVar 23])]));
438 :     add (CProp
439 :     ("equal",
440 :     [CProp ("samefringe",[CVar 23, CVar 24]),
441 :     CProp
442 :     ("equal",[CProp ("flatten",[CVar 23]), CProp ("flatten",[CVar 24])])]));
443 :     add (CProp
444 :     ("equal",
445 :     [CProp
446 :     ("equal",
447 :     [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("zero",[])]),
448 :     CProp
449 :     ("and",
450 :     [CProp
451 :     ("or",
452 :     [CProp ("zerop",[CVar 24]),
453 :     CProp ("equal",[CVar 24, CProp ("one",[])])]),
454 :     CProp ("equal",[CVar 23, CProp ("zero",[])])])]));
455 :     add (CProp
456 :     ("equal",
457 :     [CProp
458 :     ("equal",
459 :     [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("one",[])]),
460 :     CProp ("equal",[CVar 23, CProp ("one",[])])]));
461 :     add (CProp
462 :     ("equal",
463 :     [CProp ("numberp",[CProp ("greatest_factor",[CVar 23, CVar 24])]),
464 :     CProp
465 :     ("not",
466 :     [CProp
467 :     ("and",
468 :     [CProp
469 :     ("or",
470 :     [CProp ("zerop",[CVar 24]),
471 :     CProp ("equal",[CVar 24, CProp ("one",[])])]),
472 :     CProp ("not",[CProp ("numberp",[CVar 23])])])])]));
473 :     add (CProp
474 :     ("equal",
475 :     [CProp ("times_list",[CProp ("append",[CVar 23, CVar 24])]),
476 :     CProp
477 :     ("times",
478 :     [CProp ("times_list",[CVar 23]), CProp ("times_list",[CVar 24])])]));
479 :     add (CProp
480 :     ("equal",
481 :     [CProp ("prime_list",[CProp ("append",[CVar 23, CVar 24])]),
482 :     CProp
483 :     ("and",
484 :     [CProp ("prime_list",[CVar 23]), CProp ("prime_list",[CVar 24])])]));
485 :     add (CProp
486 :     ("equal",
487 :     [CProp ("equal",[CVar 25, CProp ("times",[CVar 22, CVar 25])]),
488 :     CProp
489 :     ("and",
490 :     [CProp ("numberp",[CVar 25]),
491 :     CProp
492 :     ("or",
493 :     [CProp ("equal",[CVar 25, CProp ("zero",[])]),
494 :     CProp ("equal",[CVar 22, CProp ("one",[])])])])]));
495 :     add (CProp
496 :     ("equal",
497 :     [CProp ("ge",[CVar 23, CVar 24]),
498 :     CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])]));
499 :     add (CProp
500 :     ("equal",
501 :     [CProp ("equal",[CVar 23, CProp ("times",[CVar 23, CVar 24])]),
502 :     CProp
503 :     ("or",
504 :     [CProp ("equal",[CVar 23, CProp ("zero",[])]),
505 :     CProp
506 :     ("and",
507 :     [CProp ("numberp",[CVar 23]),
508 :     CProp ("equal",[CVar 24, CProp ("one",[])])])])]));
509 :     add (CProp
510 :     ("equal",
511 :     [CProp ("remainder",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
512 :     CProp ("zero",[])]));
513 :     add (CProp
514 :     ("equal",
515 :     [CProp ("equal",[CProp ("times",[CVar 0, CVar 1]), CProp ("one",[])]),
516 :     CProp
517 :     ("and",
518 :     [CProp ("not",[CProp ("equal",[CVar 0, CProp ("zero",[])])]),
519 :     CProp ("not",[CProp ("equal",[CVar 1, CProp ("zero",[])])]),
520 :     CProp ("numberp",[CVar 0]), CProp ("numberp",[CVar 1]),
521 :     CProp ("equal",[CProp ("sub1",[CVar 0]), CProp ("zero",[])]),
522 :     CProp ("equal",[CProp ("sub1",[CVar 1]), CProp ("zero",[])])])]));
523 :     add (CProp
524 :     ("equal",
525 :     [CProp
526 :     ("lt",
527 :     [CProp ("length",[CProp ("delete",[CVar 23, CVar 11])]),
528 :     CProp ("length",[CVar 11])]),
529 :     CProp ("member",[CVar 23, CVar 11])]));
530 :     add (CProp
531 :     ("equal",
532 :     [CProp ("sort2",[CProp ("delete",[CVar 23, CVar 11])]),
533 :     CProp ("delete",[CVar 23, CProp ("sort2",[CVar 11])])]));
534 :     add (CProp ("equal",[CProp ("dsort",[CVar 23]), CProp ("sort2",[CVar 23])]));
535 :     add (CProp
536 :     ("equal",
537 :     [CProp
538 :     ("length",
539 :     [CProp
540 :     ("cons",
541 :     [CVar 0,
542 :     CProp
543 :     ("cons",
544 :     [CVar 1,
545 :     CProp
546 :     ("cons",
547 :     [CVar 2,
548 :     CProp
549 :     ("cons",
550 :     [CVar 3,
551 :     CProp ("cons",[CVar 4, CProp ("cons",[CVar 5, CVar 6])])])])])])])
552 :     , CProp ("plus",[CProp ("six",[]), CProp ("length",[CVar 6])])]));
553 :     add (CProp
554 :     ("equal",
555 :     [CProp
556 :     ("difference",
557 :     [CProp ("add1",[CProp ("add1",[CVar 23])]), CProp ("two",[])]),
558 :     CProp ("fix",[CVar 23])]));
559 :     add (CProp
560 :     ("equal",
561 :     [CProp
562 :     ("quotient",
563 :     [CProp ("plus",[CVar 23, CProp ("plus",[CVar 23, CVar 24])]),
564 :     CProp ("two",[])]),
565 :     CProp
566 :     ("plus",[CVar 23, CProp ("quotient",[CVar 24, CProp ("two",[])])])]));
567 :     add (CProp
568 :     ("equal",
569 :     [CProp ("sigma",[CProp ("zero",[]), CVar 8]),
570 :     CProp
571 :     ("quotient",
572 :     [CProp ("times",[CVar 8, CProp ("add1",[CVar 8])]), CProp ("two",[])])]));
573 :     add (CProp
574 :     ("equal",
575 :     [CProp ("plus",[CVar 23, CProp ("add1",[CVar 24])]),
576 :     CProp
577 :     ("if",
578 :     [CProp ("numberp",[CVar 24]),
579 :     CProp ("add1",[CProp ("plus",[CVar 23, CVar 24])]),
580 :     CProp ("add1",[CVar 23])])]));
581 :     add (CProp
582 :     ("equal",
583 :     [CProp
584 :     ("equal",
585 :     [CProp ("difference",[CVar 23, CVar 24]),
586 :     CProp ("difference",[CVar 25, CVar 24])]),
587 :     CProp
588 :     ("if",
589 :     [CProp ("lt",[CVar 23, CVar 24]),
590 :     CProp ("not",[CProp ("lt",[CVar 24, CVar 25])]),
591 :     CProp
592 :     ("if",
593 :     [CProp ("lt",[CVar 25, CVar 24]),
594 :     CProp ("not",[CProp ("lt",[CVar 24, CVar 23])]),
595 :     CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 25])])])])])
596 :     );
597 :     add (CProp
598 :     ("equal",
599 :     [CProp
600 :     ("meaning",
601 :     [CProp ("plus_tree",[CProp ("delete",[CVar 23, CVar 24])]), CVar 0]),
602 :     CProp
603 :     ("if",
604 :     [CProp ("member",[CVar 23, CVar 24]),
605 :     CProp
606 :     ("difference",
607 :     [CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0]),
608 :     CProp ("meaning",[CVar 23, CVar 0])]),
609 :     CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
610 :     add (CProp
611 :     ("equal",
612 :     [CProp ("times",[CVar 23, CProp ("add1",[CVar 24])]),
613 :     CProp
614 :     ("if",
615 :     [CProp ("numberp",[CVar 24]),
616 :     CProp
617 :     ("plus",
618 :     [CVar 23, CProp ("times",[CVar 23, CVar 24]),
619 :     CProp ("fix",[CVar 23])])])]));
620 :     add (CProp
621 :     ("equal",
622 :     [CProp ("nth",[CProp ("nil",[]), CVar 8]),
623 :     CProp
624 :     ("if",[CProp ("zerop",[CVar 8]), CProp ("nil",[]), CProp ("zero",[])])]));
625 :     add (CProp
626 :     ("equal",
627 :     [CProp ("last",[CProp ("append",[CVar 0, CVar 1])]),
628 :     CProp
629 :     ("if",
630 :     [CProp ("listp",[CVar 1]), CProp ("last",[CVar 1]),
631 :     CProp
632 :     ("if",
633 :     [CProp ("listp",[CVar 0]),
634 :     CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]), CVar 1]),
635 :     CVar 1])])]));
636 :     add (CProp
637 :     ("equal",
638 :     [CProp ("equal",[CProp ("lt",[CVar 23, CVar 24]), CVar 25]),
639 :     CProp
640 :     ("if",
641 :     [CProp ("lt",[CVar 23, CVar 24]),
642 :     CProp ("equal",[CProp ("true",[]), CVar 25]),
643 :     CProp ("equal",[CProp ("false",[]), CVar 25])])]));
644 :     add (CProp
645 :     ("equal",
646 :     [CProp ("assignment",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
647 :     CProp
648 :     ("if",
649 :     [CProp ("assignedp",[CVar 23, CVar 0]),
650 :     CProp ("assignment",[CVar 23, CVar 0]),
651 :     CProp ("assignment",[CVar 23, CVar 1])])]));
652 :     add (CProp
653 :     ("equal",
654 :     [CProp ("car",[CProp ("gother",[CVar 23])]),
655 :     CProp
656 :     ("if",
657 :     [CProp ("listp",[CVar 23]),
658 :     CProp ("car",[CProp ("flatten",[CVar 23])]), CProp ("zero",[])])]));
659 :     add (CProp
660 :     ("equal",
661 :     [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]),
662 :     CProp
663 :     ("if",
664 :     [CProp ("listp",[CVar 23]),
665 :     CProp ("cdr",[CProp ("flatten",[CVar 23])]),
666 :     CProp ("cons",[CProp ("zero",[]), CProp ("nil",[])])])]));
667 :     add (CProp
668 :     ("equal",
669 :     [CProp ("quotient",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
670 :     CProp
671 :     ("if",
672 :     [CProp ("zerop",[CVar 24]), CProp ("zero",[]),
673 :     CProp ("fix",[CVar 23])])]));
674 :     add (CProp
675 :     ("equal",
676 :     [CProp ("get",[CVar 9, CProp ("set",[CVar 8, CVar 21, CVar 12])]),
677 :     CProp
678 :     ("if",
679 :     [CProp ("eqp",[CVar 9, CVar 8]), CVar 21,
680 :     CProp ("get",[CVar 9, CVar 12])])])))
681 :    
682 :     end; (* Rules *)
683 :    

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0