1 (* From the SML
/NJ benchmark suite
. *)
4 * Manipulations over terms
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
21 structure Terms
:TERMS
=
26 | Prop
of { name
: string, props
: (term
* term
) list ref
} * term list
28 type head
= { name
: string, props
: (term
* term
) list ref
}
30 val lemmas
= ref ([] : head list
)
32 (* replacement for property lists
*)
34 fun headname
{name
= n
, props
=p
} = n
;
37 let fun get_rec ((hd1
as {name
=n
,...})::hdl
) =
38 if n
= name
then hd1
else get_rec hdl
40 let val entry
= {name
= name
, props
= ref
[]} in
41 lemmas
:= entry
:: !lemmas
;
49 fun add_lemma (Prop(_
, [(left
as Prop({props
=r
,...},_
)), right
])) =
50 r
:= (left
, right
) :: !r
55 exception failure
of string;
57 datatype binding
= Bind
of int * term
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
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
)
81 fun unify (term1
, term2
) = unify1 (term1
, term2
, [])
82 and unify1 (term1
, term2
, unify_subst
) =
85 ((if get_binding v unify_subst
= term1
89 Bind(v
,term1
)::unify_subst
)
90 |
Prop (head2
,argl2
) =>
93 |
Prop (head1
,argl1
) =>
94 if head1
=head2
then unify1_lst (argl1
, argl2
, unify_subst
)
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
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
)
109 rewrite_with_lemmas (term
, rest
)
120 datatype cterm
= CVar
of int | CProp
of string * cterm list
;
122 fun cterm_to_term (CVar v
) = Var v
123 |
cterm_to_term (CProp(p
, l
)) = Prop(get p
, map cterm_to_term l
)
125 fun add t
= add_lemma (cterm_to_term t
)
130 [CProp ("compile",[CVar
5]),
133 [CProp ("codegen",[CProp ("optimize",[CVar
5]), CProp ("nil",[])])])]));
136 [CProp ("eqp",[CVar
23, CVar
24]),
137 CProp ("equal",[CProp ("fix",[CVar
23]), CProp ("fix",[CVar
24])])]));
140 [CProp ("gt",[CVar
23, CVar
24]), CProp ("lt",[CVar
24, CVar
23])]));
143 [CProp ("le",[CVar
23, CVar
24]), CProp ("ge",[CVar
24, CVar
23])]));
146 [CProp ("ge",[CVar
23, CVar
24]), CProp ("le",[CVar
24, CVar
23])]));
149 [CProp ("boolean",[CVar
23]),
152 [CProp ("equal",[CVar
23, CProp ("true",[])]),
153 CProp ("equal",[CVar
23, CProp ("false",[])])])]));
156 [CProp ("iff",[CVar
23, CVar
24]),
159 [CProp ("implies",[CVar
23, CVar
24]),
160 CProp ("implies",[CVar
24, CVar
23])])]));
163 [CProp ("even1",[CVar
23]),
166 [CProp ("zerop",[CVar
23]), CProp ("true",[]),
167 CProp ("odd",[CProp ("sub1",[CVar
23])])])]));
170 [CProp ("countps_",[CVar
11, CVar
15]),
171 CProp ("countps_loop",[CVar
11, CVar
15, CProp ("zero",[])])]));
174 [CProp ("fact_",[CVar
8]),
175 CProp ("fact_loop",[CVar
8, CProp ("one",[])])]));
178 [CProp ("reverse_",[CVar
23]),
179 CProp ("reverse_loop",[CVar
23, CProp ("nil",[])])]));
182 [CProp ("divides",[CVar
23, CVar
24]),
183 CProp ("zerop",[CProp ("remainder",[CVar
24, CVar
23])])]));
186 [CProp ("assume_true",[CVar
21, CVar
0]),
187 CProp ("cons",[CProp ("cons",[CVar
21, CProp ("true",[])]), CVar
0])]));
190 [CProp ("assume_false",[CVar
21, CVar
0]),
191 CProp ("cons",[CProp ("cons",[CVar
21, CProp ("false",[])]), CVar
0])]));
194 [CProp ("tautology_checker",[CVar
23]),
195 CProp ("tautologyp",[CProp ("normalize",[CVar
23]), CProp ("nil",[])])]));
198 [CProp ("falsify",[CVar
23]),
199 CProp ("falsify1",[CProp ("normalize",[CVar
23]), CProp ("nil",[])])]));
202 [CProp ("prime",[CVar
23]),
205 [CProp ("not",[CProp ("zerop",[CVar
23])]),
208 [CProp ("equal",[CVar
23, CProp ("add1",[CProp ("zero",[])])])]),
209 CProp ("prime1",[CVar
23, CProp ("sub1",[CVar
23])])])]));
212 [CProp ("and",[CVar
15, CVar
16]),
216 CProp ("if",[CVar
16, CProp ("true",[]), CProp ("false",[])]),
217 CProp ("false",[])])]));
220 [CProp ("or",[CVar
15, CVar
16]),
223 [CVar
15, CProp ("true",[]),
224 CProp ("if",[CVar
16, CProp ("true",[]), CProp ("false",[])]),
225 CProp ("false",[])])]));
228 [CProp ("not",[CVar
15]),
229 CProp ("if",[CVar
15, CProp ("false",[]), CProp ("true",[])])]));
232 [CProp ("implies",[CVar
15, CVar
16]),
236 CProp ("if",[CVar
16, CProp ("true",[]), CProp ("false",[])]),
237 CProp ("true",[])])]));
240 [CProp ("fix",[CVar
23]),
241 CProp ("if",[CProp ("numberp",[CVar
23]), CVar
23, CProp ("zero",[])])]));
244 [CProp ("if",[CProp ("if",[CVar
0, CVar
1, CVar
2]), CVar
3, CVar
4]),
247 [CVar
0, CProp ("if",[CVar
1, CVar
3, CVar
4]),
248 CProp ("if",[CVar
2, CVar
3, CVar
4])])]));
251 [CProp ("zerop",[CVar
23]),
254 [CProp ("equal",[CVar
23, CProp ("zero",[])]),
255 CProp ("not",[CProp ("numberp",[CVar
23])])])]));
258 [CProp ("plus",[CProp ("plus",[CVar
23, CVar
24]), CVar
25]),
259 CProp ("plus",[CVar
23, CProp ("plus",[CVar
24, CVar
25])])]));
262 [CProp ("equal",[CProp ("plus",[CVar
0, CVar
1]), CProp ("zero",[])]),
263 CProp ("and",[CProp ("zerop",[CVar
0]), CProp ("zerop",[CVar
1])])]));
265 ("equal",[CProp ("difference",[CVar
23, CVar
23]), CProp ("zero",[])]));
270 [CProp ("plus",[CVar
0, CVar
1]), CProp ("plus",[CVar
0, CVar
2])]),
271 CProp ("equal",[CProp ("fix",[CVar
1]), CProp ("fix",[CVar
2])])]));
275 ("equal",[CProp ("zero",[]), CProp ("difference",[CVar
23, CVar
24])]),
276 CProp ("not",[CProp ("gt",[CVar
24, CVar
23])])]));
279 [CProp ("equal",[CVar
23, CProp ("difference",[CVar
23, CVar
24])]),
282 [CProp ("numberp",[CVar
23]),
285 [CProp ("equal",[CVar
23, CProp ("zero",[])]),
286 CProp ("zerop",[CVar
24])])])]));
291 [CProp ("plus_tree",[CProp ("append",[CVar
23, CVar
24])]), CVar
0]),
294 [CProp ("meaning",[CProp ("plus_tree",[CVar
23]), CVar
0]),
295 CProp ("meaning",[CProp ("plus_tree",[CVar
24]), CVar
0])])]));
300 [CProp ("plus_tree",[CProp ("plus_fringe",[CVar
23])]), CVar
0]),
301 CProp ("fix",[CProp ("meaning",[CVar
23, CVar
0])])]));
304 [CProp ("append",[CProp ("append",[CVar
23, CVar
24]), CVar
25]),
305 CProp ("append",[CVar
23, CProp ("append",[CVar
24, CVar
25])])]));
308 [CProp ("reverse",[CProp ("append",[CVar
0, CVar
1])]),
310 ("append",[CProp ("reverse",[CVar
1]), CProp ("reverse",[CVar
0])])]));
313 [CProp ("times",[CVar
23, CProp ("plus",[CVar
24, CVar
25])]),
316 [CProp ("times",[CVar
23, CVar
24]),
317 CProp ("times",[CVar
23, CVar
25])])]));
320 [CProp ("times",[CProp ("times",[CVar
23, CVar
24]), CVar
25]),
321 CProp ("times",[CVar
23, CProp ("times",[CVar
24, CVar
25])])]));
325 ("equal",[CProp ("times",[CVar
23, CVar
24]), CProp ("zero",[])]),
326 CProp ("or",[CProp ("zerop",[CVar
23]), CProp ("zerop",[CVar
24])])]));
329 [CProp ("exec",[CProp ("append",[CVar
23, CVar
24]), CVar
15, CVar
4]),
331 ("exec",[CVar
24, CProp ("exec",[CVar
23, CVar
15, CVar
4]), CVar
4])]));
334 [CProp ("mc_flatten",[CVar
23, CVar
24]),
335 CProp ("append",[CProp ("flatten",[CVar
23]), CVar
24])]));
338 [CProp ("member",[CVar
23, CProp ("append",[CVar
0, CVar
1])]),
341 [CProp ("member",[CVar
23, CVar
0]),
342 CProp ("member",[CVar
23, CVar
1])])]));
345 [CProp ("member",[CVar
23, CProp ("reverse",[CVar
24])]),
346 CProp ("member",[CVar
23, CVar
24])]));
349 [CProp ("length",[CProp ("reverse",[CVar
23])]),
350 CProp ("length",[CVar
23])]));
353 [CProp ("member",[CVar
0, CProp ("intersect",[CVar
1, CVar
2])]),
356 [CProp ("member",[CVar
0, CVar
1]), CProp ("member",[CVar
0, CVar
2])])]));
358 ("equal",[CProp ("nth",[CProp ("zero",[]), CVar
8]), CProp ("zero",[])]));
361 [CProp ("exp",[CVar
8, CProp ("plus",[CVar
9, CVar
10])]),
364 [CProp ("exp",[CVar
8, CVar
9]), CProp ("exp",[CVar
8, CVar
10])])]));
367 [CProp ("exp",[CVar
8, CProp ("times",[CVar
9, CVar
10])]),
368 CProp ("exp",[CProp ("exp",[CVar
8, CVar
9]), CVar
10])]));
371 [CProp ("reverse_loop",[CVar
23, CVar
24]),
372 CProp ("append",[CProp ("reverse",[CVar
23]), CVar
24])]));
375 [CProp ("reverse_loop",[CVar
23, CProp ("nil",[])]),
376 CProp ("reverse",[CVar
23])]));
379 [CProp ("count_list",[CVar
25, CProp ("sort_lp",[CVar
23, CVar
24])]),
382 [CProp ("count_list",[CVar
25, CVar
23]),
383 CProp ("count_list",[CVar
25, CVar
24])])]));
388 [CProp ("append",[CVar
0, CVar
1]), CProp ("append",[CVar
0, CVar
2])]),
389 CProp ("equal",[CVar
1, CVar
2])]));
394 [CProp ("remainder",[CVar
23, CVar
24]),
395 CProp ("times",[CVar
24, CProp ("quotient",[CVar
23, CVar
24])])]),
396 CProp ("fix",[CVar
23])]));
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])]));
406 [CProp ("big_plus",[CVar
23, CVar
24, CVar
8, CVar
1]), CVar
1]),
412 [CProp ("power_eval",[CVar
23, CVar
1]),
413 CProp ("power_eval",[CVar
24, CVar
1])])])]));
416 [CProp ("remainder",[CVar
24, CProp ("one",[])]), CProp ("zero",[])]));
419 [CProp ("lt",[CProp ("remainder",[CVar
23, CVar
24]), CVar
24]),
420 CProp ("not",[CProp ("zerop",[CVar
24])])]));
422 ("equal",[CProp ("remainder",[CVar
23, CVar
23]), CProp ("zero",[])]));
425 [CProp ("lt",[CProp ("quotient",[CVar
8, CVar
9]), CVar
8]),
428 [CProp ("not",[CProp ("zerop",[CVar
8])]),
431 [CProp ("zerop",[CVar
9]),
432 CProp ("not",[CProp ("equal",[CVar
9, CProp ("one",[])])])])])]));
435 [CProp ("lt",[CProp ("remainder",[CVar
23, CVar
24]), CVar
23]),
438 [CProp ("not",[CProp ("zerop",[CVar
24])]),
439 CProp ("not",[CProp ("zerop",[CVar
23])]),
440 CProp ("not",[CProp ("lt",[CVar
23, CVar
24])])])]));
443 [CProp ("power_eval",[CProp ("power_rep",[CVar
8, CVar
1]), CVar
1]),
444 CProp ("fix",[CVar
8])]));
451 [CProp ("power_rep",[CVar
8, CVar
1]),
452 CProp ("power_rep",[CVar
9, CVar
1]), CProp ("zero",[]),
455 CProp ("plus",[CVar
8, CVar
9])]));
458 [CProp ("gcd",[CVar
23, CVar
24]), CProp ("gcd",[CVar
24, CVar
23])]));
461 [CProp ("nth",[CProp ("append",[CVar
0, CVar
1]), CVar
8]),
464 [CProp ("nth",[CVar
0, CVar
8]),
467 [CVar
1, CProp ("difference",[CVar
8, CProp ("length",[CVar
0])])])])]));
470 [CProp ("difference",[CProp ("plus",[CVar
23, CVar
24]), CVar
23]),
471 CProp ("fix",[CVar
24])]));
474 [CProp ("difference",[CProp ("plus",[CVar
24, CVar
23]), CVar
23]),
475 CProp ("fix",[CVar
24])]));
480 [CProp ("plus",[CVar
23, CVar
24]), CProp ("plus",[CVar
23, CVar
25])]),
481 CProp ("difference",[CVar
24, CVar
25])]));
484 [CProp ("times",[CVar
23, CProp ("difference",[CVar
2, CVar
22])]),
487 [CProp ("times",[CVar
2, CVar
23]),
488 CProp ("times",[CVar
22, CVar
23])])]));
491 [CProp ("remainder",[CProp ("times",[CVar
23, CVar
25]), CVar
25]),
492 CProp ("zero",[])]));
497 [CProp ("plus",[CVar
1, CProp ("plus",[CVar
0, CVar
2])]), CVar
0]),
498 CProp ("plus",[CVar
1, CVar
2])]));
503 [CProp ("add1",[CProp ("plus",[CVar
24, CVar
25])]), CVar
25]),
504 CProp ("add1",[CVar
24])]));
509 [CProp ("plus",[CVar
23, CVar
24]), CProp ("plus",[CVar
23, CVar
25])]),
510 CProp ("lt",[CVar
24, CVar
25])]));
515 [CProp ("times",[CVar
23, CVar
25]),
516 CProp ("times",[CVar
24, CVar
25])]),
519 [CProp ("not",[CProp ("zerop",[CVar
25])]),
520 CProp ("lt",[CVar
23, CVar
24])])]));
523 [CProp ("lt",[CVar
24, CProp ("plus",[CVar
23, CVar
24])]),
524 CProp ("not",[CProp ("zerop",[CVar
23])])]));
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])])]));
534 [CProp ("value",[CProp ("normalize",[CVar
23]), CVar
0]),
535 CProp ("value",[CVar
23, CVar
0])]));
540 [CProp ("flatten",[CVar
23]),
541 CProp ("cons",[CVar
24, CProp ("nil",[])])]),
544 [CProp ("nlistp",[CVar
23]), CProp ("equal",[CVar
23, CVar
24])])]));
547 [CProp ("listp",[CProp ("gother",[CVar
23])]),
548 CProp ("listp",[CVar
23])]));
551 [CProp ("samefringe",[CVar
23, CVar
24]),
553 ("equal",[CProp ("flatten",[CVar
23]), CProp ("flatten",[CVar
24])])]));
558 [CProp ("greatest_factor",[CVar
23, CVar
24]), CProp ("zero",[])]),
563 [CProp ("zerop",[CVar
24]),
564 CProp ("equal",[CVar
24, CProp ("one",[])])]),
565 CProp ("equal",[CVar
23, CProp ("zero",[])])])]));
570 [CProp ("greatest_factor",[CVar
23, CVar
24]), CProp ("one",[])]),
571 CProp ("equal",[CVar
23, CProp ("one",[])])]));
574 [CProp ("numberp",[CProp ("greatest_factor",[CVar
23, CVar
24])]),
581 [CProp ("zerop",[CVar
24]),
582 CProp ("equal",[CVar
24, CProp ("one",[])])]),
583 CProp ("not",[CProp ("numberp",[CVar
23])])])])]));
586 [CProp ("times_list",[CProp ("append",[CVar
23, CVar
24])]),
589 [CProp ("times_list",[CVar
23]), CProp ("times_list",[CVar
24])])]));
592 [CProp ("prime_list",[CProp ("append",[CVar
23, CVar
24])]),
595 [CProp ("prime_list",[CVar
23]), CProp ("prime_list",[CVar
24])])]));
598 [CProp ("equal",[CVar
25, CProp ("times",[CVar
22, CVar
25])]),
601 [CProp ("numberp",[CVar
25]),
604 [CProp ("equal",[CVar
25, CProp ("zero",[])]),
605 CProp ("equal",[CVar
22, CProp ("one",[])])])])]));
608 [CProp ("ge",[CVar
23, CVar
24]),
609 CProp ("not",[CProp ("lt",[CVar
23, CVar
24])])]));
612 [CProp ("equal",[CVar
23, CProp ("times",[CVar
23, CVar
24])]),
615 [CProp ("equal",[CVar
23, CProp ("zero",[])]),
618 [CProp ("numberp",[CVar
23]),
619 CProp ("equal",[CVar
24, CProp ("one",[])])])])]));
622 [CProp ("remainder",[CProp ("times",[CVar
24, CVar
23]), CVar
24]),
623 CProp ("zero",[])]));
626 [CProp ("equal",[CProp ("times",[CVar
0, CVar
1]), CProp ("one",[])]),
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",[])])])]));
638 [CProp ("length",[CProp ("delete",[CVar
23, CVar
11])]),
639 CProp ("length",[CVar
11])]),
640 CProp ("member",[CVar
23, CVar
11])]));
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])]));
662 CProp ("cons",[CVar
4, CProp ("cons",[CVar
5, CVar
6])])])])])])])
663 , CProp ("plus",[CProp ("six",[]), CProp ("length",[CVar
6])])]));
668 [CProp ("add1",[CProp ("add1",[CVar
23])]), CProp ("two",[])]),
669 CProp ("fix",[CVar
23])]));
674 [CProp ("plus",[CVar
23, CProp ("plus",[CVar
23, CVar
24])]),
677 ("plus",[CVar
23, CProp ("quotient",[CVar
24, CProp ("two",[])])])]));
680 [CProp ("sigma",[CProp ("zero",[]), CVar
8]),
683 [CProp ("times",[CVar
8, CProp ("add1",[CVar
8])]), CProp ("two",[])])]));
686 [CProp ("plus",[CVar
23, CProp ("add1",[CVar
24])]),
689 [CProp ("numberp",[CVar
24]),
690 CProp ("add1",[CProp ("plus",[CVar
23, CVar
24])]),
691 CProp ("add1",[CVar
23])])]));
696 [CProp ("difference",[CVar
23, CVar
24]),
697 CProp ("difference",[CVar
25, CVar
24])]),
700 [CProp ("lt",[CVar
23, CVar
24]),
701 CProp ("not",[CProp ("lt",[CVar
24, CVar
25])]),
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])])])])])
712 [CProp ("plus_tree",[CProp ("delete",[CVar
23, CVar
24])]), CVar
0]),
715 [CProp ("member",[CVar
23, CVar
24]),
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])])]));
723 [CProp ("times",[CVar
23, CProp ("add1",[CVar
24])]),
726 [CProp ("numberp",[CVar
24]),
729 [CVar
23, CProp ("times",[CVar
23, CVar
24]),
730 CProp ("fix",[CVar
23])])])]));
733 [CProp ("nth",[CProp ("nil",[]), CVar
8]),
735 ("if",[CProp ("zerop",[CVar
8]), CProp ("nil",[]), CProp ("zero",[])])]));
738 [CProp ("last",[CProp ("append",[CVar
0, CVar
1])]),
741 [CProp ("listp",[CVar
1]), CProp ("last",[CVar
1]),
744 [CProp ("listp",[CVar
0]),
745 CProp ("cons",[CProp ("car",[CProp ("last",[CVar
0])]), CVar
1]),
749 [CProp ("equal",[CProp ("lt",[CVar
23, CVar
24]), CVar
25]),
752 [CProp ("lt",[CVar
23, CVar
24]),
753 CProp ("equal",[CProp ("true",[]), CVar
25]),
754 CProp ("equal",[CProp ("false",[]), CVar
25])])]));
757 [CProp ("assignment",[CVar
23, CProp ("append",[CVar
0, CVar
1])]),
760 [CProp ("assignedp",[CVar
23, CVar
0]),
761 CProp ("assignment",[CVar
23, CVar
0]),
762 CProp ("assignment",[CVar
23, CVar
1])])]));
765 [CProp ("car",[CProp ("gother",[CVar
23])]),
768 [CProp ("listp",[CVar
23]),
769 CProp ("car",[CProp ("flatten",[CVar
23])]), CProp ("zero",[])])]));
772 [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar
23])])]),
775 [CProp ("listp",[CVar
23]),
776 CProp ("cdr",[CProp ("flatten",[CVar
23])]),
777 CProp ("cons",[CProp ("zero",[]), CProp ("nil",[])])])]));
780 [CProp ("quotient",[CProp ("times",[CVar
24, CVar
23]), CVar
24]),
783 [CProp ("zerop",[CVar
24]), CProp ("zero",[]),
784 CProp ("fix",[CVar
23])])]));
787 [CProp ("get",[CVar
9, CProp ("set",[CVar
8, CVar
21, CVar
12])]),
790 [CProp ("eqp",[CVar
9, CVar
8]), CVar
21,
791 CProp ("get",[CVar
9, CVar
12])])])))
803 val tautp
: term
-> bool
806 structure Boyer
: BOYER
=
812 | mem
x (y
::L
) = x
=y
orelse mem x L
817 headname head
= "true" orelse mem x lst
821 and falsep (x
, lst
) =
824 headname head
= "false" orelse mem x lst
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
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
)
844 fun tautp x
= tautologyp(rewrite x
, [], []);
850 val doit
: unit
-> unit
851 val testit
: TextIO.outstream
-> unit
855 structure Main
: BMARK
=
867 [Prop (get
"plus",[Var
0, Var
1]),
868 Prop (get
"plus",[Var
2, Prop (get
"zero",[])])])])),
874 [Prop (get
"times",[Var
0, Var
1]),
875 Prop (get
"plus",[Var
2, Var
3])])])),
883 [Prop (get
"append",[Var
0, Var
1]),
884 Prop (get
"nil",[])])])])),
888 [Prop (get
"plus",[Var
0, Var
1]),
889 Prop (get
"difference",[Var
23, Var
24])])),
893 [Prop (get
"remainder",[Var
0, Var
1]),
894 Prop (get
"member",[Var
0, Prop (get
"length",[Var
1])])]))]
901 [Prop (get
"implies",[Var
23, Var
24]),
904 [Prop (get
"implies",[Var
24, Var
25]),
907 [Prop (get
"implies",[Var
25, Var
20]),
908 Prop (get
"implies",[Var
20, Var
22])])])]),
909 Prop (get
"implies",[Var
23, Var
22])])
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")
915 fun doit () = (tautp (apply_subst subst term
); ())