REMOVE-UNTOUCHABLE

remove names from lists of untouchable symbols 
Major Section:  SWITCHES-PARAMETERS-AND-MODES

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.

Examples:
(remove-untouchable my-var nil)
(remove-untouchable set-mem t)


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).