Remove-untouchable
Remove names from lists of untouchable symbols
Untouchables are functions that cannot be called or as state
global variables (see programming-with-state) that cannot be modified
or unbound.
Example Forms:
(remove-untouchable my-var nil) ; then state global my-var is not untouchable
(remove-untouchable set-mem t) ; then function set-mem is not untouchable
Also see push-untouchable.
This documentation topic is directed at those who build systems on top of
ACL2. We first describe a means for modifying state to remove some
untouchables. Then we describe the remove-untouchable event. Both
require an active trust tag (see defttag).
We begin by discussing untouchable state global variables
temp-touchable-vars and temp-touchable-fns, which initially have
value nil. These can often be used in place of remove-untouchable.
When the value is t, no variable (respectively, no function or macro) is
treated as untouchable, regardless of the set of initial untouchables or the
remove-untouchable or push-untouchable events that have
been admitted. Otherwise the value of each of these two variables is a symbol-listp, and no member of this list is treated as an untouchable
variable (in the case of temp-touchable-vars) or as an untouchable
function or macro (in the case of temp-touchable-fns). These two state
global variables can be set by set-temp-touchable-vars and
set-temp-touchable-fns, respectively, provided there is an active trust
tag (see defttag). Here is an illustrative example. This macro
executes the indicated forms in a context where there are no untouchable
variables, but requires an active trust tag when invoked.
(defmacro with-all-touchable (&rest forms)
`(progn!
:state-global-bindings
((temp-touchable-vars t set-temp-touchable-vars))
(progn! ,@forms)))
An equivalent version, which however is not recommended since state-global-let* may have surprising behavior in raw Lisp, is as
follows.
(defmacro with-all-touchable (&rest forms)
`(progn!
(state-global-let*
((temp-touchable-vars t set-temp-touchable-vars))
(progn! ,@forms))))
Finally, the value t for temp-touchable-vars removes the
requirement that built-in state globals cannot be made unbound (with
makunbound-global).
We now turn to the remove-untouchable event, in case the approach
above is for some reason not adequate. This event is illegal by default,
since it can be used to provide access to ACL2 internal functions and data
structures that are intentionally made untouchable for the user. If you want
to call it, you must first create an active trust tag; see defttag.
General Form:
(remove-untouchable name{s} fn-p)
where name{s} is a non-nil symbol or a non-nil true list of
symbols, and fn-p is any value (but generally nil or t). If
name{s} is a symbol it is treated as the singleton list containing that
symbol. The effect of this event is to remove the given symbols from the list
of ``untouchable variables'' in the current world if fn-p is nil,
else to remove the symbols into the list of ``untouchable functions''. This
event is redundant if no symbol listed is a member of the appropriate
untouchables list (variables or functions).
