		Search-engine friendly clone of the ACL2 documentation.

State-global-let*

Bind state global variables

See programming-with-state for requisite background on programming with the ACL2 state.

Example Forms:
(state-global-let*
 ((inhibit-output-lst *valid-output-names*))
 (thm (equal x x)))

(state-global-let*
 ((fmt-hard-right-margin 1000 set-fmt-hard-right-margin)
  (fmt-soft-right-margin 1000 set-fmt-soft-right-margin))
 (mini-proveall))

General Form:
(state-global-let* ((var1 form1) ; or (var1 form1 set-var1)
                    ...
                    (vark formk) ; or (vark formk set-vark)
                   )
                   body)

where: each vari is a variable; each formi is an expression whose value is a single ordinary object (i.e. not multiple values, and not state or any other stobj); set-vari, if supplied, is a function or macro such that (set-vari _ state) returns state; and body is an expression that evaluates to an error-triple. Each formi is evaluated in order, starting with form1, and with each such binding the state global variable vari is bound to the value of formi, sequentially in the style of let*. More precisely, the meaning of this form is to perform the following actions, in order.

Set (in order) the global values of the indicated state global variables vari to the values of formi. Exception: This is skipped when vari is a built-in state global and formi is (f-get-global 'vari state).
Execute body.
Restore the vari to their previous values.
Return the error-triple produced by body, where state reflects the modifications of the preceding step.

The restoration is guaranteed even in the face of aborts. The ``bound'' variables may initially be unbound in state and restoration means to make them unbound again.

Still referring to the General Form above, we next discuss how the values are set and restored. Let old-vali be the value of state global variable vari at the time vari is about to be assigned the value of formi. We say that a “setter is supplied” for vari if set-vari is supplied, either explicitly as in the General Form above, or implicitly by being associated with vari in the value of the constant, *state-global-let*-untouchable-alist* (whose definition appears at the end of this topic). If no setter is supplied then vari is set or restored to a value <val> by evaluating (f-put-global 'vari <val> state). However, if a setter set-vari is supplied, then the form evaluated will instead be (set-vari <val> state). Having a setter supplied is particularly useful if vari is untouchable, since the call above of f-put-global is illegal. However, the use of *state-global-let*-untouchable-alist* (mentioned above) avoids the need for supplying set-vari explicitly for certain built-in untouchable state global variables, vari.

Note that the scope of the bindings of a state-global-let* form is the body of that form. This may seem obvious, but to drive the point home, let's consider the following example (see set-print-base and see set-print-radix).

ACL2 !>(state-global-let* ((print-base 16 set-print-base)
                           (print-radix t set-print-radix))
                          (mv nil 10 state))
 10
ACL2 !>

Why wasn't the result printed as #xA? The reason is that the result was printed after evaluation of the entire form had completed. If you want to see #xA, do the printing in the scope of the bindings, for example as follows.

ACL2 !>(state-global-let* ((print-base 16 set-print-base)
                           (print-radix t set-print-radix))
                          (pprogn (fms "~x0~%"
                                       (list (cons #\0 10))
                                       *standard-co* state nil)
                                  (mv nil 10 state)))

#xA
 10
ACL2 !>

Finally, as promised above, here is the definition of the constant that maps certain built-in untouchable variables to setters.

Definition: *state-global-let*-untouchable-alist*

(defconst *state-global-let*-untouchable-alist*
  '((abbrev-evisc-tuple . set-abbrev-evisc-tuple-state)
    (compiler-enabled . set-compiler-enabled)
    (current-package . set-current-package-state)
    (fmt-hard-right-margin . set-fmt-hard-right-margin)
    (fmt-soft-right-margin . set-fmt-soft-right-margin)
    (gag-mode-evisc-tuple . set-gag-mode-evisc-tuple-state)
    (inhibit-output-lst . set-inhibit-output-lst-state)
    (inhibited-summary-types . set-inhibited-summary-types-state)
    (ld-evisc-tuple . set-ld-evisc-tuple-state)
    (ppr-flat-right-margin . set-ppr-flat-right-margin)
    (print-base . set-print-base)
    (print-case . set-print-case)
    (print-length . set-print-length)
    (print-level . set-print-level)
    (print-lines . set-print-lines)
    (print-right-margin . set-print-right-margin)
    (proofs-co . set-proofs-co-state)
    (serialize-character . set-serialize-character)
    (serialize-character-system . set-serialize-character-system)
    (standard-co . set-standard-co-state)
    (temp-touchable-fns . set-temp-touchable-fns)
    (temp-touchable-vars . set-temp-touchable-vars)
    (term-evisc-tuple . set-term-evisc-tuple-state)))