Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* From the SML/NJ benchmark suite. *) |
2 | (* terms.sml: | |
3 | * | |
4 | * Manipulations over terms | |
5 | *) | |
6 | ||
7 | signature TERMS = | |
8 | sig | |
9 | type head; | |
10 | datatype term = | |
11 | Var of int | |
12 | | Prop of head * term list; | |
13 | datatype binding = Bind of int * term; | |
14 | val get: string -> head | |
15 | and headname: head -> string | |
16 | and add_lemma: term -> unit | |
17 | and apply_subst: binding list -> term -> term | |
18 | and rewrite: term -> term | |
19 | end; | |
20 | ||
21 | structure Terms:TERMS = | |
22 | struct | |
23 | ||
24 | datatype term | |
25 | = Var of int | |
26 | | Prop of { name: string, props: (term * term) list ref } * term list | |
27 | ||
28 | type head = { name: string, props: (term * term) list ref } | |
29 | ||
30 | val lemmas = ref ([] : head list) | |
31 | ||
32 | (* replacement for property lists *) | |
33 | ||
34 | fun headname {name = n, props=p} = n; | |
35 | ||
36 | fun get name = | |
37 | let fun get_rec ((hd1 as {name=n,...})::hdl) = | |
38 | if n = name then hd1 else get_rec hdl | |
39 | | get_rec [] = | |
40 | let val entry = {name = name, props = ref []} in | |
41 | lemmas := entry :: !lemmas; | |
42 | entry | |
43 | end | |
44 | in | |
45 | get_rec (!lemmas) | |
46 | end | |
47 | ; | |
48 | ||
49 | fun add_lemma (Prop(_, [(left as Prop({props=r,...},_)), right])) = | |
50 | r := (left, right) :: !r | |
51 | ; | |
52 | ||
53 | (* substitutions *) | |
54 | ||
55 | exception failure of string; | |
56 | ||
57 | datatype binding = Bind of int * term | |
58 | ; | |
59 | ||
60 | fun get_binding v = | |
61 | let fun get_rec [] = raise (failure "unbound") | |
62 | | get_rec (Bind(w,t)::rest) = | |
63 | if v = w then t else get_rec rest | |
64 | in | |
65 | get_rec | |
66 | end | |
67 | ; | |
68 | ||
69 | fun apply_subst alist = | |
70 | let fun as_rec (term as Var v) = | |
71 | ((get_binding v alist) handle failure _ => term) | |
72 | | as_rec (Prop (head,argl)) = | |
73 | Prop (head, map as_rec argl) | |
74 | in | |
75 | as_rec | |
76 | end | |
77 | ; | |
78 | ||
79 | exception Unify; | |
80 | ||
81 | fun unify (term1, term2) = unify1 (term1, term2, []) | |
82 | and unify1 (term1, term2, unify_subst) = | |
83 | (case term2 of | |
84 | Var v => | |
85 | ((if get_binding v unify_subst = term1 | |
86 | then unify_subst | |
87 | else raise Unify) | |
88 | handle failure _ => | |
89 | Bind(v,term1)::unify_subst) | |
90 | | Prop (head2,argl2) => | |
91 | case term1 of | |
92 | Var _ => raise Unify | |
93 | | Prop (head1,argl1) => | |
94 | if head1=head2 then unify1_lst (argl1, argl2, unify_subst) | |
95 | else raise Unify) | |
96 | and unify1_lst ([], [], unify_subst) = unify_subst | |
97 | | unify1_lst (h1::r1, h2::r2, unify_subst) = | |
98 | unify1_lst(r1, r2, unify1(h1, h2, unify_subst)) | |
99 | | unify1_lst _ = raise Unify | |
100 | ; | |
101 | ||
102 | fun rewrite (term as Var _) = term | |
103 | | rewrite (Prop ((head as {props=p,...}), argl)) = | |
104 | rewrite_with_lemmas (Prop (head, map rewrite argl), !p) | |
105 | and rewrite_with_lemmas (term, []) = term | |
106 | | rewrite_with_lemmas (term, (t1,t2)::rest) = | |
107 | rewrite (apply_subst (unify (term, t1)) t2) | |
108 | handle unify => | |
109 | rewrite_with_lemmas (term, rest) | |
110 | ; | |
111 | end; | |
112 | (* rules.sml: | |
113 | *) | |
114 | ||
115 | structure Rules = | |
116 | struct | |
117 | ||
118 | open Terms; | |
119 | ||
120 | datatype cterm = CVar of int | CProp of string * cterm list; | |
121 | ||
122 | fun cterm_to_term (CVar v) = Var v | |
123 | | cterm_to_term (CProp(p, l)) = Prop(get p, map cterm_to_term l) | |
124 | ||
125 | fun add t = add_lemma (cterm_to_term t) | |
126 | ||
127 | val _ = ( | |
128 | add (CProp | |
129 | ("equal", | |
130 | [CProp ("compile",[CVar 5]), | |
131 | CProp | |
132 | ("reverse", | |
133 | [CProp ("codegen",[CProp ("optimize",[CVar 5]), CProp ("nil",[])])])])); | |
134 | add (CProp | |
135 | ("equal", | |
136 | [CProp ("eqp",[CVar 23, CVar 24]), | |
137 | CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 24])])])); | |
138 | add (CProp | |
139 | ("equal", | |
140 | [CProp ("gt",[CVar 23, CVar 24]), CProp ("lt",[CVar 24, CVar 23])])); | |
141 | add (CProp | |
142 | ("equal", | |
143 | [CProp ("le",[CVar 23, CVar 24]), CProp ("ge",[CVar 24, CVar 23])])); | |
144 | add (CProp | |
145 | ("equal", | |
146 | [CProp ("ge",[CVar 23, CVar 24]), CProp ("le",[CVar 24, CVar 23])])); | |
147 | add (CProp | |
148 | ("equal", | |
149 | [CProp ("boolean",[CVar 23]), | |
150 | CProp | |
151 | ("or", | |
152 | [CProp ("equal",[CVar 23, CProp ("true",[])]), | |
153 | CProp ("equal",[CVar 23, CProp ("false",[])])])])); | |
154 | add (CProp | |
155 | ("equal", | |
156 | [CProp ("iff",[CVar 23, CVar 24]), | |
157 | CProp | |
158 | ("and", | |
159 | [CProp ("implies",[CVar 23, CVar 24]), | |
160 | CProp ("implies",[CVar 24, CVar 23])])])); | |
161 | add (CProp | |
162 | ("equal", | |
163 | [CProp ("even1",[CVar 23]), | |
164 | CProp | |
165 | ("if", | |
166 | [CProp ("zerop",[CVar 23]), CProp ("true",[]), | |
167 | CProp ("odd",[CProp ("sub1",[CVar 23])])])])); | |
168 | add (CProp | |
169 | ("equal", | |
170 | [CProp ("countps_",[CVar 11, CVar 15]), | |
171 | CProp ("countps_loop",[CVar 11, CVar 15, CProp ("zero",[])])])); | |
172 | add (CProp | |
173 | ("equal", | |
174 | [CProp ("fact_",[CVar 8]), | |
175 | CProp ("fact_loop",[CVar 8, CProp ("one",[])])])); | |
176 | add (CProp | |
177 | ("equal", | |
178 | [CProp ("reverse_",[CVar 23]), | |
179 | CProp ("reverse_loop",[CVar 23, CProp ("nil",[])])])); | |
180 | add (CProp | |
181 | ("equal", | |
182 | [CProp ("divides",[CVar 23, CVar 24]), | |
183 | CProp ("zerop",[CProp ("remainder",[CVar 24, CVar 23])])])); | |
184 | add (CProp | |
185 | ("equal", | |
186 | [CProp ("assume_true",[CVar 21, CVar 0]), | |
187 | CProp ("cons",[CProp ("cons",[CVar 21, CProp ("true",[])]), CVar 0])])); | |
188 | add (CProp | |
189 | ("equal", | |
190 | [CProp ("assume_false",[CVar 21, CVar 0]), | |
191 | CProp ("cons",[CProp ("cons",[CVar 21, CProp ("false",[])]), CVar 0])])); | |
192 | add (CProp | |
193 | ("equal", | |
194 | [CProp ("tautology_checker",[CVar 23]), | |
195 | CProp ("tautologyp",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])])); | |
196 | add (CProp | |
197 | ("equal", | |
198 | [CProp ("falsify",[CVar 23]), | |
199 | CProp ("falsify1",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])])); | |
200 | add (CProp | |
201 | ("equal", | |
202 | [CProp ("prime",[CVar 23]), | |
203 | CProp | |
204 | ("and", | |
205 | [CProp ("not",[CProp ("zerop",[CVar 23])]), | |
206 | CProp | |
207 | ("not", | |
208 | [CProp ("equal",[CVar 23, CProp ("add1",[CProp ("zero",[])])])]), | |
209 | CProp ("prime1",[CVar 23, CProp ("sub1",[CVar 23])])])])); | |
210 | add (CProp | |
211 | ("equal", | |
212 | [CProp ("and",[CVar 15, CVar 16]), | |
213 | CProp | |
214 | ("if", | |
215 | [CVar 15, | |
216 | CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]), | |
217 | CProp ("false",[])])])); | |
218 | add (CProp | |
219 | ("equal", | |
220 | [CProp ("or",[CVar 15, CVar 16]), | |
221 | CProp | |
222 | ("if", | |
223 | [CVar 15, CProp ("true",[]), | |
224 | CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]), | |
225 | CProp ("false",[])])])); | |
226 | add (CProp | |
227 | ("equal", | |
228 | [CProp ("not",[CVar 15]), | |
229 | CProp ("if",[CVar 15, CProp ("false",[]), CProp ("true",[])])])); | |
230 | add (CProp | |
231 | ("equal", | |
232 | [CProp ("implies",[CVar 15, CVar 16]), | |
233 | CProp | |
234 | ("if", | |
235 | [CVar 15, | |
236 | CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]), | |
237 | CProp ("true",[])])])); | |
238 | add (CProp | |
239 | ("equal", | |
240 | [CProp ("fix",[CVar 23]), | |
241 | CProp ("if",[CProp ("numberp",[CVar 23]), CVar 23, CProp ("zero",[])])])); | |
242 | add (CProp | |
243 | ("equal", | |
244 | [CProp ("if",[CProp ("if",[CVar 0, CVar 1, CVar 2]), CVar 3, CVar 4]), | |
245 | CProp | |
246 | ("if", | |
247 | [CVar 0, CProp ("if",[CVar 1, CVar 3, CVar 4]), | |
248 | CProp ("if",[CVar 2, CVar 3, CVar 4])])])); | |
249 | add (CProp | |
250 | ("equal", | |
251 | [CProp ("zerop",[CVar 23]), | |
252 | CProp | |
253 | ("or", | |
254 | [CProp ("equal",[CVar 23, CProp ("zero",[])]), | |
255 | CProp ("not",[CProp ("numberp",[CVar 23])])])])); | |
256 | add (CProp | |
257 | ("equal", | |
258 | [CProp ("plus",[CProp ("plus",[CVar 23, CVar 24]), CVar 25]), | |
259 | CProp ("plus",[CVar 23, CProp ("plus",[CVar 24, CVar 25])])])); | |
260 | add (CProp | |
261 | ("equal", | |
262 | [CProp ("equal",[CProp ("plus",[CVar 0, CVar 1]), CProp ("zero",[])]), | |
263 | CProp ("and",[CProp ("zerop",[CVar 0]), CProp ("zerop",[CVar 1])])])); | |
264 | add (CProp | |
265 | ("equal",[CProp ("difference",[CVar 23, CVar 23]), CProp ("zero",[])])); | |
266 | add (CProp | |
267 | ("equal", | |
268 | [CProp | |
269 | ("equal", | |
270 | [CProp ("plus",[CVar 0, CVar 1]), CProp ("plus",[CVar 0, CVar 2])]), | |
271 | CProp ("equal",[CProp ("fix",[CVar 1]), CProp ("fix",[CVar 2])])])); | |
272 | add (CProp | |
273 | ("equal", | |
274 | [CProp | |
275 | ("equal",[CProp ("zero",[]), CProp ("difference",[CVar 23, CVar 24])]), | |
276 | CProp ("not",[CProp ("gt",[CVar 24, CVar 23])])])); | |
277 | add (CProp | |
278 | ("equal", | |
279 | [CProp ("equal",[CVar 23, CProp ("difference",[CVar 23, CVar 24])]), | |
280 | CProp | |
281 | ("and", | |
282 | [CProp ("numberp",[CVar 23]), | |
283 | CProp | |
284 | ("or", | |
285 | [CProp ("equal",[CVar 23, CProp ("zero",[])]), | |
286 | CProp ("zerop",[CVar 24])])])])); | |
287 | add (CProp | |
288 | ("equal", | |
289 | [CProp | |
290 | ("meaning", | |
291 | [CProp ("plus_tree",[CProp ("append",[CVar 23, CVar 24])]), CVar 0]), | |
292 | CProp | |
293 | ("plus", | |
294 | [CProp ("meaning",[CProp ("plus_tree",[CVar 23]), CVar 0]), | |
295 | CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])])); | |
296 | add (CProp | |
297 | ("equal", | |
298 | [CProp | |
299 | ("meaning", | |
300 | [CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]), CVar 0]), | |
301 | CProp ("fix",[CProp ("meaning",[CVar 23, CVar 0])])])); | |
302 | add (CProp | |
303 | ("equal", | |
304 | [CProp ("append",[CProp ("append",[CVar 23, CVar 24]), CVar 25]), | |
305 | CProp ("append",[CVar 23, CProp ("append",[CVar 24, CVar 25])])])); | |
306 | add (CProp | |
307 | ("equal", | |
308 | [CProp ("reverse",[CProp ("append",[CVar 0, CVar 1])]), | |
309 | CProp | |
310 | ("append",[CProp ("reverse",[CVar 1]), CProp ("reverse",[CVar 0])])])); | |
311 | add (CProp | |
312 | ("equal", | |
313 | [CProp ("times",[CVar 23, CProp ("plus",[CVar 24, CVar 25])]), | |
314 | CProp | |
315 | ("plus", | |
316 | [CProp ("times",[CVar 23, CVar 24]), | |
317 | CProp ("times",[CVar 23, CVar 25])])])); | |
318 | add (CProp | |
319 | ("equal", | |
320 | [CProp ("times",[CProp ("times",[CVar 23, CVar 24]), CVar 25]), | |
321 | CProp ("times",[CVar 23, CProp ("times",[CVar 24, CVar 25])])])); | |
322 | add (CProp | |
323 | ("equal", | |
324 | [CProp | |
325 | ("equal",[CProp ("times",[CVar 23, CVar 24]), CProp ("zero",[])]), | |
326 | CProp ("or",[CProp ("zerop",[CVar 23]), CProp ("zerop",[CVar 24])])])); | |
327 | add (CProp | |
328 | ("equal", | |
329 | [CProp ("exec",[CProp ("append",[CVar 23, CVar 24]), CVar 15, CVar 4]), | |
330 | CProp | |
331 | ("exec",[CVar 24, CProp ("exec",[CVar 23, CVar 15, CVar 4]), CVar 4])])); | |
332 | add (CProp | |
333 | ("equal", | |
334 | [CProp ("mc_flatten",[CVar 23, CVar 24]), | |
335 | CProp ("append",[CProp ("flatten",[CVar 23]), CVar 24])])); | |
336 | add (CProp | |
337 | ("equal", | |
338 | [CProp ("member",[CVar 23, CProp ("append",[CVar 0, CVar 1])]), | |
339 | CProp | |
340 | ("or", | |
341 | [CProp ("member",[CVar 23, CVar 0]), | |
342 | CProp ("member",[CVar 23, CVar 1])])])); | |
343 | add (CProp | |
344 | ("equal", | |
345 | [CProp ("member",[CVar 23, CProp ("reverse",[CVar 24])]), | |
346 | CProp ("member",[CVar 23, CVar 24])])); | |
347 | add (CProp | |
348 | ("equal", | |
349 | [CProp ("length",[CProp ("reverse",[CVar 23])]), | |
350 | CProp ("length",[CVar 23])])); | |
351 | add (CProp | |
352 | ("equal", | |
353 | [CProp ("member",[CVar 0, CProp ("intersect",[CVar 1, CVar 2])]), | |
354 | CProp | |
355 | ("and", | |
356 | [CProp ("member",[CVar 0, CVar 1]), CProp ("member",[CVar 0, CVar 2])])])); | |
357 | add (CProp | |
358 | ("equal",[CProp ("nth",[CProp ("zero",[]), CVar 8]), CProp ("zero",[])])); | |
359 | add (CProp | |
360 | ("equal", | |
361 | [CProp ("exp",[CVar 8, CProp ("plus",[CVar 9, CVar 10])]), | |
362 | CProp | |
363 | ("times", | |
364 | [CProp ("exp",[CVar 8, CVar 9]), CProp ("exp",[CVar 8, CVar 10])])])); | |
365 | add (CProp | |
366 | ("equal", | |
367 | [CProp ("exp",[CVar 8, CProp ("times",[CVar 9, CVar 10])]), | |
368 | CProp ("exp",[CProp ("exp",[CVar 8, CVar 9]), CVar 10])])); | |
369 | add (CProp | |
370 | ("equal", | |
371 | [CProp ("reverse_loop",[CVar 23, CVar 24]), | |
372 | CProp ("append",[CProp ("reverse",[CVar 23]), CVar 24])])); | |
373 | add (CProp | |
374 | ("equal", | |
375 | [CProp ("reverse_loop",[CVar 23, CProp ("nil",[])]), | |
376 | CProp ("reverse",[CVar 23])])); | |
377 | add (CProp | |
378 | ("equal", | |
379 | [CProp ("count_list",[CVar 25, CProp ("sort_lp",[CVar 23, CVar 24])]), | |
380 | CProp | |
381 | ("plus", | |
382 | [CProp ("count_list",[CVar 25, CVar 23]), | |
383 | CProp ("count_list",[CVar 25, CVar 24])])])); | |
384 | add (CProp | |
385 | ("equal", | |
386 | [CProp | |
387 | ("equal", | |
388 | [CProp ("append",[CVar 0, CVar 1]), CProp ("append",[CVar 0, CVar 2])]), | |
389 | CProp ("equal",[CVar 1, CVar 2])])); | |
390 | add (CProp | |
391 | ("equal", | |
392 | [CProp | |
393 | ("plus", | |
394 | [CProp ("remainder",[CVar 23, CVar 24]), | |
395 | CProp ("times",[CVar 24, CProp ("quotient",[CVar 23, CVar 24])])]), | |
396 | CProp ("fix",[CVar 23])])); | |
397 | add (CProp | |
398 | ("equal", | |
399 | [CProp | |
400 | ("power_eval",[CProp ("big_plus",[CVar 11, CVar 8, CVar 1]), CVar 1]), | |
401 | CProp ("plus",[CProp ("power_eval",[CVar 11, CVar 1]), CVar 8])])); | |
402 | add (CProp | |
403 | ("equal", | |
404 | [CProp | |
405 | ("power_eval", | |
406 | [CProp ("big_plus",[CVar 23, CVar 24, CVar 8, CVar 1]), CVar 1]), | |
407 | CProp | |
408 | ("plus", | |
409 | [CVar 8, | |
410 | CProp | |
411 | ("plus", | |
412 | [CProp ("power_eval",[CVar 23, CVar 1]), | |
413 | CProp ("power_eval",[CVar 24, CVar 1])])])])); | |
414 | add (CProp | |
415 | ("equal", | |
416 | [CProp ("remainder",[CVar 24, CProp ("one",[])]), CProp ("zero",[])])); | |
417 | add (CProp | |
418 | ("equal", | |
419 | [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 24]), | |
420 | CProp ("not",[CProp ("zerop",[CVar 24])])])); | |
421 | add (CProp | |
422 | ("equal",[CProp ("remainder",[CVar 23, CVar 23]), CProp ("zero",[])])); | |
423 | add (CProp | |
424 | ("equal", | |
425 | [CProp ("lt",[CProp ("quotient",[CVar 8, CVar 9]), CVar 8]), | |
426 | CProp | |
427 | ("and", | |
428 | [CProp ("not",[CProp ("zerop",[CVar 8])]), | |
429 | CProp | |
430 | ("or", | |
431 | [CProp ("zerop",[CVar 9]), | |
432 | CProp ("not",[CProp ("equal",[CVar 9, CProp ("one",[])])])])])])); | |
433 | add (CProp | |
434 | ("equal", | |
435 | [CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 23]), | |
436 | CProp | |
437 | ("and", | |
438 | [CProp ("not",[CProp ("zerop",[CVar 24])]), | |
439 | CProp ("not",[CProp ("zerop",[CVar 23])]), | |
440 | CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])])])); | |
441 | add (CProp | |
442 | ("equal", | |
443 | [CProp ("power_eval",[CProp ("power_rep",[CVar 8, CVar 1]), CVar 1]), | |
444 | CProp ("fix",[CVar 8])])); | |
445 | add (CProp | |
446 | ("equal", | |
447 | [CProp | |
448 | ("power_eval", | |
449 | [CProp | |
450 | ("big_plus", | |
451 | [CProp ("power_rep",[CVar 8, CVar 1]), | |
452 | CProp ("power_rep",[CVar 9, CVar 1]), CProp ("zero",[]), | |
453 | CVar 1]), | |
454 | CVar 1]), | |
455 | CProp ("plus",[CVar 8, CVar 9])])); | |
456 | add (CProp | |
457 | ("equal", | |
458 | [CProp ("gcd",[CVar 23, CVar 24]), CProp ("gcd",[CVar 24, CVar 23])])); | |
459 | add (CProp | |
460 | ("equal", | |
461 | [CProp ("nth",[CProp ("append",[CVar 0, CVar 1]), CVar 8]), | |
462 | CProp | |
463 | ("append", | |
464 | [CProp ("nth",[CVar 0, CVar 8]), | |
465 | CProp | |
466 | ("nth", | |
467 | [CVar 1, CProp ("difference",[CVar 8, CProp ("length",[CVar 0])])])])])); | |
468 | add (CProp | |
469 | ("equal", | |
470 | [CProp ("difference",[CProp ("plus",[CVar 23, CVar 24]), CVar 23]), | |
471 | CProp ("fix",[CVar 24])])); | |
472 | add (CProp | |
473 | ("equal", | |
474 | [CProp ("difference",[CProp ("plus",[CVar 24, CVar 23]), CVar 23]), | |
475 | CProp ("fix",[CVar 24])])); | |
476 | add (CProp | |
477 | ("equal", | |
478 | [CProp | |
479 | ("difference", | |
480 | [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]), | |
481 | CProp ("difference",[CVar 24, CVar 25])])); | |
482 | add (CProp | |
483 | ("equal", | |
484 | [CProp ("times",[CVar 23, CProp ("difference",[CVar 2, CVar 22])]), | |
485 | CProp | |
486 | ("difference", | |
487 | [CProp ("times",[CVar 2, CVar 23]), | |
488 | CProp ("times",[CVar 22, CVar 23])])])); | |
489 | add (CProp | |
490 | ("equal", | |
491 | [CProp ("remainder",[CProp ("times",[CVar 23, CVar 25]), CVar 25]), | |
492 | CProp ("zero",[])])); | |
493 | add (CProp | |
494 | ("equal", | |
495 | [CProp | |
496 | ("difference", | |
497 | [CProp ("plus",[CVar 1, CProp ("plus",[CVar 0, CVar 2])]), CVar 0]), | |
498 | CProp ("plus",[CVar 1, CVar 2])])); | |
499 | add (CProp | |
500 | ("equal", | |
501 | [CProp | |
502 | ("difference", | |
503 | [CProp ("add1",[CProp ("plus",[CVar 24, CVar 25])]), CVar 25]), | |
504 | CProp ("add1",[CVar 24])])); | |
505 | add (CProp | |
506 | ("equal", | |
507 | [CProp | |
508 | ("lt", | |
509 | [CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]), | |
510 | CProp ("lt",[CVar 24, CVar 25])])); | |
511 | add (CProp | |
512 | ("equal", | |
513 | [CProp | |
514 | ("lt", | |
515 | [CProp ("times",[CVar 23, CVar 25]), | |
516 | CProp ("times",[CVar 24, CVar 25])]), | |
517 | CProp | |
518 | ("and", | |
519 | [CProp ("not",[CProp ("zerop",[CVar 25])]), | |
520 | CProp ("lt",[CVar 23, CVar 24])])])); | |
521 | add (CProp | |
522 | ("equal", | |
523 | [CProp ("lt",[CVar 24, CProp ("plus",[CVar 23, CVar 24])]), | |
524 | CProp ("not",[CProp ("zerop",[CVar 23])])])); | |
525 | add (CProp | |
526 | ("equal", | |
527 | [CProp | |
528 | ("gcd", | |
529 | [CProp ("times",[CVar 23, CVar 25]), | |
530 | CProp ("times",[CVar 24, CVar 25])]), | |
531 | CProp ("times",[CVar 25, CProp ("gcd",[CVar 23, CVar 24])])])); | |
532 | add (CProp | |
533 | ("equal", | |
534 | [CProp ("value",[CProp ("normalize",[CVar 23]), CVar 0]), | |
535 | CProp ("value",[CVar 23, CVar 0])])); | |
536 | add (CProp | |
537 | ("equal", | |
538 | [CProp | |
539 | ("equal", | |
540 | [CProp ("flatten",[CVar 23]), | |
541 | CProp ("cons",[CVar 24, CProp ("nil",[])])]), | |
542 | CProp | |
543 | ("and", | |
544 | [CProp ("nlistp",[CVar 23]), CProp ("equal",[CVar 23, CVar 24])])])); | |
545 | add (CProp | |
546 | ("equal", | |
547 | [CProp ("listp",[CProp ("gother",[CVar 23])]), | |
548 | CProp ("listp",[CVar 23])])); | |
549 | add (CProp | |
550 | ("equal", | |
551 | [CProp ("samefringe",[CVar 23, CVar 24]), | |
552 | CProp | |
553 | ("equal",[CProp ("flatten",[CVar 23]), CProp ("flatten",[CVar 24])])])); | |
554 | add (CProp | |
555 | ("equal", | |
556 | [CProp | |
557 | ("equal", | |
558 | [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("zero",[])]), | |
559 | CProp | |
560 | ("and", | |
561 | [CProp | |
562 | ("or", | |
563 | [CProp ("zerop",[CVar 24]), | |
564 | CProp ("equal",[CVar 24, CProp ("one",[])])]), | |
565 | CProp ("equal",[CVar 23, CProp ("zero",[])])])])); | |
566 | add (CProp | |
567 | ("equal", | |
568 | [CProp | |
569 | ("equal", | |
570 | [CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("one",[])]), | |
571 | CProp ("equal",[CVar 23, CProp ("one",[])])])); | |
572 | add (CProp | |
573 | ("equal", | |
574 | [CProp ("numberp",[CProp ("greatest_factor",[CVar 23, CVar 24])]), | |
575 | CProp | |
576 | ("not", | |
577 | [CProp | |
578 | ("and", | |
579 | [CProp | |
580 | ("or", | |
581 | [CProp ("zerop",[CVar 24]), | |
582 | CProp ("equal",[CVar 24, CProp ("one",[])])]), | |
583 | CProp ("not",[CProp ("numberp",[CVar 23])])])])])); | |
584 | add (CProp | |
585 | ("equal", | |
586 | [CProp ("times_list",[CProp ("append",[CVar 23, CVar 24])]), | |
587 | CProp | |
588 | ("times", | |
589 | [CProp ("times_list",[CVar 23]), CProp ("times_list",[CVar 24])])])); | |
590 | add (CProp | |
591 | ("equal", | |
592 | [CProp ("prime_list",[CProp ("append",[CVar 23, CVar 24])]), | |
593 | CProp | |
594 | ("and", | |
595 | [CProp ("prime_list",[CVar 23]), CProp ("prime_list",[CVar 24])])])); | |
596 | add (CProp | |
597 | ("equal", | |
598 | [CProp ("equal",[CVar 25, CProp ("times",[CVar 22, CVar 25])]), | |
599 | CProp | |
600 | ("and", | |
601 | [CProp ("numberp",[CVar 25]), | |
602 | CProp | |
603 | ("or", | |
604 | [CProp ("equal",[CVar 25, CProp ("zero",[])]), | |
605 | CProp ("equal",[CVar 22, CProp ("one",[])])])])])); | |
606 | add (CProp | |
607 | ("equal", | |
608 | [CProp ("ge",[CVar 23, CVar 24]), | |
609 | CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])])); | |
610 | add (CProp | |
611 | ("equal", | |
612 | [CProp ("equal",[CVar 23, CProp ("times",[CVar 23, CVar 24])]), | |
613 | CProp | |
614 | ("or", | |
615 | [CProp ("equal",[CVar 23, CProp ("zero",[])]), | |
616 | CProp | |
617 | ("and", | |
618 | [CProp ("numberp",[CVar 23]), | |
619 | CProp ("equal",[CVar 24, CProp ("one",[])])])])])); | |
620 | add (CProp | |
621 | ("equal", | |
622 | [CProp ("remainder",[CProp ("times",[CVar 24, CVar 23]), CVar 24]), | |
623 | CProp ("zero",[])])); | |
624 | add (CProp | |
625 | ("equal", | |
626 | [CProp ("equal",[CProp ("times",[CVar 0, CVar 1]), CProp ("one",[])]), | |
627 | CProp | |
628 | ("and", | |
629 | [CProp ("not",[CProp ("equal",[CVar 0, CProp ("zero",[])])]), | |
630 | CProp ("not",[CProp ("equal",[CVar 1, CProp ("zero",[])])]), | |
631 | CProp ("numberp",[CVar 0]), CProp ("numberp",[CVar 1]), | |
632 | CProp ("equal",[CProp ("sub1",[CVar 0]), CProp ("zero",[])]), | |
633 | CProp ("equal",[CProp ("sub1",[CVar 1]), CProp ("zero",[])])])])); | |
634 | add (CProp | |
635 | ("equal", | |
636 | [CProp | |
637 | ("lt", | |
638 | [CProp ("length",[CProp ("delete",[CVar 23, CVar 11])]), | |
639 | CProp ("length",[CVar 11])]), | |
640 | CProp ("member",[CVar 23, CVar 11])])); | |
641 | add (CProp | |
642 | ("equal", | |
643 | [CProp ("sort2",[CProp ("delete",[CVar 23, CVar 11])]), | |
644 | CProp ("delete",[CVar 23, CProp ("sort2",[CVar 11])])])); | |
645 | add (CProp ("equal",[CProp ("dsort",[CVar 23]), CProp ("sort2",[CVar 23])])); | |
646 | add (CProp | |
647 | ("equal", | |
648 | [CProp | |
649 | ("length", | |
650 | [CProp | |
651 | ("cons", | |
652 | [CVar 0, | |
653 | CProp | |
654 | ("cons", | |
655 | [CVar 1, | |
656 | CProp | |
657 | ("cons", | |
658 | [CVar 2, | |
659 | CProp | |
660 | ("cons", | |
661 | [CVar 3, | |
662 | CProp ("cons",[CVar 4, CProp ("cons",[CVar 5, CVar 6])])])])])])]) | |
663 | , CProp ("plus",[CProp ("six",[]), CProp ("length",[CVar 6])])])); | |
664 | add (CProp | |
665 | ("equal", | |
666 | [CProp | |
667 | ("difference", | |
668 | [CProp ("add1",[CProp ("add1",[CVar 23])]), CProp ("two",[])]), | |
669 | CProp ("fix",[CVar 23])])); | |
670 | add (CProp | |
671 | ("equal", | |
672 | [CProp | |
673 | ("quotient", | |
674 | [CProp ("plus",[CVar 23, CProp ("plus",[CVar 23, CVar 24])]), | |
675 | CProp ("two",[])]), | |
676 | CProp | |
677 | ("plus",[CVar 23, CProp ("quotient",[CVar 24, CProp ("two",[])])])])); | |
678 | add (CProp | |
679 | ("equal", | |
680 | [CProp ("sigma",[CProp ("zero",[]), CVar 8]), | |
681 | CProp | |
682 | ("quotient", | |
683 | [CProp ("times",[CVar 8, CProp ("add1",[CVar 8])]), CProp ("two",[])])])); | |
684 | add (CProp | |
685 | ("equal", | |
686 | [CProp ("plus",[CVar 23, CProp ("add1",[CVar 24])]), | |
687 | CProp | |
688 | ("if", | |
689 | [CProp ("numberp",[CVar 24]), | |
690 | CProp ("add1",[CProp ("plus",[CVar 23, CVar 24])]), | |
691 | CProp ("add1",[CVar 23])])])); | |
692 | add (CProp | |
693 | ("equal", | |
694 | [CProp | |
695 | ("equal", | |
696 | [CProp ("difference",[CVar 23, CVar 24]), | |
697 | CProp ("difference",[CVar 25, CVar 24])]), | |
698 | CProp | |
699 | ("if", | |
700 | [CProp ("lt",[CVar 23, CVar 24]), | |
701 | CProp ("not",[CProp ("lt",[CVar 24, CVar 25])]), | |
702 | CProp | |
703 | ("if", | |
704 | [CProp ("lt",[CVar 25, CVar 24]), | |
705 | CProp ("not",[CProp ("lt",[CVar 24, CVar 23])]), | |
706 | CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 25])])])])]) | |
707 | ); | |
708 | add (CProp | |
709 | ("equal", | |
710 | [CProp | |
711 | ("meaning", | |
712 | [CProp ("plus_tree",[CProp ("delete",[CVar 23, CVar 24])]), CVar 0]), | |
713 | CProp | |
714 | ("if", | |
715 | [CProp ("member",[CVar 23, CVar 24]), | |
716 | CProp | |
717 | ("difference", | |
718 | [CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0]), | |
719 | CProp ("meaning",[CVar 23, CVar 0])]), | |
720 | CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])])); | |
721 | add (CProp | |
722 | ("equal", | |
723 | [CProp ("times",[CVar 23, CProp ("add1",[CVar 24])]), | |
724 | CProp | |
725 | ("if", | |
726 | [CProp ("numberp",[CVar 24]), | |
727 | CProp | |
728 | ("plus", | |
729 | [CVar 23, CProp ("times",[CVar 23, CVar 24]), | |
730 | CProp ("fix",[CVar 23])])])])); | |
731 | add (CProp | |
732 | ("equal", | |
733 | [CProp ("nth",[CProp ("nil",[]), CVar 8]), | |
734 | CProp | |
735 | ("if",[CProp ("zerop",[CVar 8]), CProp ("nil",[]), CProp ("zero",[])])])); | |
736 | add (CProp | |
737 | ("equal", | |
738 | [CProp ("last",[CProp ("append",[CVar 0, CVar 1])]), | |
739 | CProp | |
740 | ("if", | |
741 | [CProp ("listp",[CVar 1]), CProp ("last",[CVar 1]), | |
742 | CProp | |
743 | ("if", | |
744 | [CProp ("listp",[CVar 0]), | |
745 | CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]), CVar 1]), | |
746 | CVar 1])])])); | |
747 | add (CProp | |
748 | ("equal", | |
749 | [CProp ("equal",[CProp ("lt",[CVar 23, CVar 24]), CVar 25]), | |
750 | CProp | |
751 | ("if", | |
752 | [CProp ("lt",[CVar 23, CVar 24]), | |
753 | CProp ("equal",[CProp ("true",[]), CVar 25]), | |
754 | CProp ("equal",[CProp ("false",[]), CVar 25])])])); | |
755 | add (CProp | |
756 | ("equal", | |
757 | [CProp ("assignment",[CVar 23, CProp ("append",[CVar 0, CVar 1])]), | |
758 | CProp | |
759 | ("if", | |
760 | [CProp ("assignedp",[CVar 23, CVar 0]), | |
761 | CProp ("assignment",[CVar 23, CVar 0]), | |
762 | CProp ("assignment",[CVar 23, CVar 1])])])); | |
763 | add (CProp | |
764 | ("equal", | |
765 | [CProp ("car",[CProp ("gother",[CVar 23])]), | |
766 | CProp | |
767 | ("if", | |
768 | [CProp ("listp",[CVar 23]), | |
769 | CProp ("car",[CProp ("flatten",[CVar 23])]), CProp ("zero",[])])])); | |
770 | add (CProp | |
771 | ("equal", | |
772 | [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]), | |
773 | CProp | |
774 | ("if", | |
775 | [CProp ("listp",[CVar 23]), | |
776 | CProp ("cdr",[CProp ("flatten",[CVar 23])]), | |
777 | CProp ("cons",[CProp ("zero",[]), CProp ("nil",[])])])])); | |
778 | add (CProp | |
779 | ("equal", | |
780 | [CProp ("quotient",[CProp ("times",[CVar 24, CVar 23]), CVar 24]), | |
781 | CProp | |
782 | ("if", | |
783 | [CProp ("zerop",[CVar 24]), CProp ("zero",[]), | |
784 | CProp ("fix",[CVar 23])])])); | |
785 | add (CProp | |
786 | ("equal", | |
787 | [CProp ("get",[CVar 9, CProp ("set",[CVar 8, CVar 21, CVar 12])]), | |
788 | CProp | |
789 | ("if", | |
790 | [CProp ("eqp",[CVar 9, CVar 8]), CVar 21, | |
791 | CProp ("get",[CVar 9, CVar 12])])]))) | |
792 | ||
793 | end; (* Rules *) | |
794 | ||
795 | (* boyer.sml: | |
796 | * | |
797 | * Tautology checker | |
798 | *) | |
799 | ||
800 | signature BOYER = | |
801 | sig | |
802 | include TERMS | |
803 | val tautp: term -> bool | |
804 | end | |
805 | ||
806 | structure Boyer: BOYER = | |
807 | struct | |
808 | ||
809 | open Terms | |
810 | ||
811 | fun mem x [] = false | |
812 | | mem x (y::L) = x=y orelse mem x L | |
813 | ||
814 | fun truep (x, lst) = | |
815 | case x of | |
816 | Prop(head, _) => | |
817 | headname head = "true" orelse mem x lst | |
818 | | _ => | |
819 | mem x lst | |
820 | ||
821 | and falsep (x, lst) = | |
822 | case x of | |
823 | Prop(head, _) => | |
824 | headname head = "false" orelse mem x lst | |
825 | | _ => | |
826 | mem x lst | |
827 | ||
828 | fun tautologyp (x, true_lst, false_lst) = | |
829 | if truep (x, true_lst) then true else | |
830 | if falsep (x, false_lst) then false else | |
831 | (case x of | |
832 | Var _ => false | |
833 | | Prop (head,[test, yes, no]) => | |
834 | if headname head = "if" then | |
835 | if truep (test, true_lst) then | |
836 | tautologyp (yes, true_lst, false_lst) | |
837 | else if falsep (test, false_lst) then | |
838 | tautologyp (no, true_lst, false_lst) | |
839 | else tautologyp (yes, test::true_lst, false_lst) andalso | |
840 | tautologyp (no, true_lst, test::false_lst) | |
841 | else | |
842 | false) | |
843 | ||
844 | fun tautp x = tautologyp(rewrite x, [], []); | |
845 | ||
846 | end; (* Boyer *) | |
847 | ||
848 | signature BMARK = | |
849 | sig | |
850 | val doit : unit -> unit | |
851 | val testit : TextIO.outstream -> unit | |
852 | end; | |
853 | ||
854 | (* the benchmark *) | |
855 | structure Main : BMARK = | |
856 | struct | |
857 | ||
858 | open Terms; | |
859 | open Boyer; | |
860 | ||
861 | val subst = | |
862 | [Bind(23, | |
863 | Prop | |
864 | (get "f", | |
865 | [Prop | |
866 | (get "plus", | |
867 | [Prop (get "plus",[Var 0, Var 1]), | |
868 | Prop (get "plus",[Var 2, Prop (get "zero",[])])])])), | |
869 | Bind(24, | |
870 | Prop | |
871 | (get "f", | |
872 | [Prop | |
873 | (get "times", | |
874 | [Prop (get "times",[Var 0, Var 1]), | |
875 | Prop (get "plus",[Var 2, Var 3])])])), | |
876 | Bind(25, | |
877 | Prop | |
878 | (get "f", | |
879 | [Prop | |
880 | (get "reverse", | |
881 | [Prop | |
882 | (get "append", | |
883 | [Prop (get "append",[Var 0, Var 1]), | |
884 | Prop (get "nil",[])])])])), | |
885 | Bind(20, | |
886 | Prop | |
887 | (get "equal", | |
888 | [Prop (get "plus",[Var 0, Var 1]), | |
889 | Prop (get "difference",[Var 23, Var 24])])), | |
890 | Bind(22, | |
891 | Prop | |
892 | (get "lt", | |
893 | [Prop (get "remainder",[Var 0, Var 1]), | |
894 | Prop (get "member",[Var 0, Prop (get "length",[Var 1])])]))] | |
895 | ||
896 | val term = | |
897 | Prop | |
898 | (get "implies", | |
899 | [Prop | |
900 | (get "and", | |
901 | [Prop (get "implies",[Var 23, Var 24]), | |
902 | Prop | |
903 | (get "and", | |
904 | [Prop (get "implies",[Var 24, Var 25]), | |
905 | Prop | |
906 | (get "and", | |
907 | [Prop (get "implies",[Var 25, Var 20]), | |
908 | Prop (get "implies",[Var 20, Var 22])])])]), | |
909 | Prop (get "implies",[Var 23, Var 22])]) | |
910 | ||
911 | fun testit outstrm = if tautp (apply_subst subst term) | |
912 | then TextIO.output (outstrm, "Proved!\n") | |
913 | else TextIO.output (outstrm, "Cannot prove!\n") | |
914 | ||
915 | fun doit () = (tautp (apply_subst subst term); ()) | |
916 | ||
917 | end; (* Main *) | |
918 | ||
919 | structure Main = | |
920 | struct | |
921 | val doit = | |
922 | fn n => | |
923 | let | |
924 | fun loop n = | |
925 | if n = 0 | |
926 | then () | |
927 | else (Main.doit (); | |
928 | loop(n-1)) | |
929 | in loop n | |
930 | end | |
931 | end; |