Check-vars-not-free
Avoid variable capture in macro calls
Check-vars-not-free is a macro that is useful for avoiding
capture of variables in macro calls. We explain using a running example,
after which we give a precise explanation (at the end of this documentation
topic). These definitions are rather contrived but are designed to illustrate
how check-vars-not-free can be useful.
(defmacro has-length (x n)
`(let ((k (len ,x)))
(equal k ,n)))
(defun f1 (u v)
(and (natp v)
(has-length u (* 2 v))))
(defun f2 (lst k)
(and (natp k)
(has-length lst (* 2 k))))
One might expect f1 and f2 to be the same function, since the
only change seems to be from the choices of formal parameters. However,
consider these evaluations.
ACL2 !>(f1 '(a b c d e f) 3)
T
ACL2 !>(f2 '(a b c d e f) 3)
NIL
ACL2 !>
The problem becomes clear if we expand the macro call in the body of
f2.
ACL2 !>:trans1 (has-length lst (* 2 k))
(LET ((K (LEN LST))) (EQUAL K (* 2 K)))
ACL2 !>
We see that when expanding the call of the macro has-length in the
body of f2, the substitution of (* 2 k) for ,n causes k to
be``captured'' by the binding of k to (len lst).
The macro check-vars-not-free is designed to enforce that no such
capture takes place. An improved definition of has-length is as
follows, since it insists that the variable k must not appear in the term
that replaces ,n.
(defmacro has-length (x n)
`(let ((k (len ,x)))
(equal k (check-vars-not-free (k) ,n))))
Now, the attempt to define f2 as above causes an error.
ACL2 !>(defun f2 (lst k)
(and (natp k)
(has-length lst (* 2 k))))
ACL2 Error in ( DEFUN F2 ...): CHECK-VARS-NOT-FREE failed:
It is forbidden to use K in (BINARY-* '2 K). Note: this error occurred
in the context (CHECK-VARS-NOT-FREE (K) (* 2 K)).
Summary
Form: ( DEFUN F2 ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2 Error in ( DEFUN F2 ...): See :DOC failure.
******** FAILED ********
ACL2 !>
The error message shows that the check performed by
check-vars-not-free has failed, because the variable k occurs in the
expression (* 2 k). More precisely, what is checked is that k does
not occur in the translation to a term of the expression (* 2 k),
namely, (binary-* '2 k).
The general form of a call of check-vars-not-free is
(check-vars-not-free (var_1 ... var_n) expr)
where var_1, ..., var_n are variables and expr is an
expression. This call is equivalent to expr — indeed, there is no
effect on the code generated when using this call in place of expr
— but ACL2 requires that the indicated variables do not occur free in
the translation of expr to a term.
