flet-patch.lisp in order to fix some
problems with FLET
in ACL2 Version 3.4 (actually also in Version 3.3, where ACL2 support
for FLET was 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 flet expressions, which we
have also fixed: this form failed before the fix.
:trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)