With-current-package
To bind the current-package
Evaluation of a form (with-current-package "pkg" form)
causes form to be evaluated with the current-package bound to
"pkg".
Example and WARNING. The current-package is not modified until
after the form is read! Consider the following log that was produced when the
value of the current-package was the default, "ACL2".
ACL2 !>(with-current-package "ACL2-USER"
(value (cw "~x0~%" 'abcd)))
ACL2::ABCD
NIL
ACL2 !>
We see that the call of cw did its printing relative to the
"ACL2-USER" package, producing output "ACL2::ABCD". This
illustrates that the form was read with respect to package
"ACL2" but that its evaluation took place with respect to
package "ACL2-USER".
General Form:
(with-current-package str form)
where str evaluates to a nonempty string that represents the desired
package (see current-package) and form evaluates to an error-triple.
Evaluation of (with-current-package str form) first switches to the
indicated package, as with (in-package str), and evaluates form,
after which the current-package is restored to the value it had before that
evaluation of with-current-package. The implementation is designed so
that the current-package is restored even when the evaluation of form
causes an error.
The following example drives home the behavior of
with-current-package; explanation follows.
ACL2 !>'common-lisp::defun
DEFUN
ACL2 !>'acl2-user::defun
DEFUN
ACL2 !>(with-current-package
"ACL2-USER"
(er-progn (set-current-package "ACL2-PC" state)
(value (cw "~x0~%" 'defun))))
COMMON-LISP::DEFUN
NIL
ACL2 !>
The symbol common-lisp::defun is imported from the
"COMMON-LISP" package into both the "ACL2" package and, as shown
in the first two evaluation results above, the "ACL2-USER" package.
But it's not imported into the "ACL2-PC" package. The call above of
with-current-package reads 'defun into the current package,
"ACL2". Then for evaluation the package changes to "ACL2-USER";
then the package is changed again to "ACL2-PC" before evaluating the
cw call in that package, necessitating the "COMMON-LISP::"
prefix since the defun symbol in that cw call is not in the
"ACL2-PC" package. But notice that the prompt comes back as "ACL2
!>", indicating that we are back in the "ACL2" package. The
original package is restored after the with-current-package call
completes evaluation, even when the current-package is changed during
evaluation.
The form (with-current-package str ev) is an event form if
ev is an event form; thus, it may occur in books as well as encapsulate and progn events. See embedded-event-form. But
in an event context, str must be a string, not merely an
expression that evaluates to a string.
Finally, note that Lisp compilers may vary in how they handle functions
defined within the scope of with-current-package. If you find an example
of slower execution caused by using with-current-package, please feel
free to send it to the ACL2 implementors.
