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
with signature ((set-vari * state) => 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, then meaning of
this form is to set (in order) the global values of the indicated state
global variables vari to the values of formi using f-put-global, execute body, restore the vari to their previous
values (but see the discussion of setters below), and return the triple
produced by body (with its state as modified by the restoration). 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, let old-vali be the value
of state global variable vari at the time vari is about to be
assigned the value of formi. If set-vari is not supplied, then as
suggested above, the following form is evaluated at the conclusion of the
evaluation of the state-global-let* form, whether or not an error has
occurred: (f-put-global 'vari 'old-vali state). However, if
set-vari is supplied, it is a function symbol that we may call a
“setter”, and the form evaluated will instead be (set-vari
'old-vali state). This capability is particularly useful if vari is
untouchable (see push-untouchable), since the above call of f-put-global is illegal.
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 !>
