flet-patch.lispin order to fix some problems with
FLETin ACL2 Version 3.4 (actually also in Version 3.3, where ACL2 support for
FLETwas introduced). Installation instructions are at the top of the file.
Below is the documentation that may appear in the next release notes to explain this patch.
Fixed bugs in the handling of
flet expressions, one of which had the
capability of rendering ACL2 unsound. Thanks to Sol Swords for pointing out
two issues and sending examples. One example illustrated how ACL2 was in
essence throwing away outer
flet bindings when processing an inner
flet. We have exploited that example to prove a contradiction, as
follows: this book was certifiable before this fix.
(in-package "ACL2") (defun a (x) (list 'c x)) ; Example from Sol Swords, which failed to be admitted (claiming that ; function A is undefined) without the above definition of A. (defun foo1 (x y) (flet ((a (x) (list 'a x))) (flet ((b (y) (list 'b y))) (b (a (list x y)))))) (defthm not-true (equal (foo1 3 4) '(b (c (3 4)))) :hints (("Goal" :in-theory (disable (:executable-counterpart foo1)))) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :use not-true)) :rule-classes nil)Sol's second example, below, pointed to a second bug related to computing output signatures in the presence of nested
fletexpressions, which we have also fixed: this form failed before the fix.
:trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)