Major Section: SWITCHES-PARAMETERS-AND-MODES
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
In brief: The variable symbol STATE has an unusual status in ACL2.
In order to use it, you either need to issue :set-state-ok t, as
we explain below, or you need to declare it to be a stobj, as
explained elsewhere (see declare-stobjs). Now we explain in
more detail.
Because the variable symbol STATE denotes the ``current ACL2
state,'' ACL2 treats the symbol very restrictively when it occurs as
a formal parameter of a defined function. The novice user, who is
unlikely to be aware of the special status of that symbol, is
likely to be confused when error messages about STATE are printed
in response to the innocent choice of that symbol as a formal
variable. Therefore the top-level ACL2 loop can operate in a mode
in which STATE is simply disallowed as a formal parameter.
For a discussion of STATE, See state and see stobj. Roughly speaking, at
the top-level, the ``current ACL2 state'' is denoted by the variable
symbol STATE. Only the current state may be passed into a
function expecting a state as an argument. Furthermore, the name of
the formal parameter into which the current state is passed must be
STATE and nothing but the current state may be passed into a
formal of that name. Therefore, only certain access and change
functions can use that formal -- namely those with a STATE formal
-- and if any such function produces a new state it becomes the
``current state'' and must be passed along in the STATE position
thereafter. Thus, ACL2 requires that the state be single-threaded.
This, in turn, allows us to represent only one state at a time and
to produce new states from it destructively in a von Neumaneque
fashion. The syntactic restrictions on the variable STATE are
enforced by the translate mechanism (see trans and see term) when
terms are read.
To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol STATE ACL2 has a mode in which it
simply disallows the use of that symbol as a formal parameter. Use of
the symbol causes a simple error message. The system is initially
in that mode.
To get out of that mode, execute:
:set-state-ok t ;;; or, (set-state-ok t)It is not recommended that you do this until you have read the documentation of
STATE.To enter the mode in which use of state is prohibited as a formal
parameter, do:
:set-state-ok nil
The mode is stored in the defaults table, See acl2-defaults-table.
Thus, the mode may be set locally in books.
