Major Section: ACL2-BUILT-INS
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 (see error-triples). 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, then instead the form evaluated will 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 !>
