SET-STATE-OK

allow the use of STATE as a formal parameter
Major Section:  SWITCHES-PARAMETERS-AND-MODES-OH-MY

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