Major Section: SWITCHES-PARAMETERS-AND-MODES
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 removing restrictions related to
so-called ``untouchables'': functions (or macros) that cannot be called, or
state global variables that cannot be modified or unbound, without
intervention that requires an active trust tag (see defttag). Then we
describe the remove-untouchable event.
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 :doc doc-string)
where name{s} is a non-nil symbol or a non-nil true list of symbols,
fn-p is any value (but generally nil or t), and doc-string
is an optional documentation string not beginning with
``:Doc-Section ...''. 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).
