Trans-eval-and-stobjs
How user-defined stobjs are handled by trans-eval
See trans-eval for basic background on the relatively
advanced system utility, trans-eval. In this topic we discuss how
trans-eval handles user-defined stobjs.
A field of the ACL2 state, the user-stobj-alist, is an
association list (alist) that maps each user-defined stobj name to its
current value. Trans-eval evaluates with respect to this alist, so that
any time a variable (which must be a stobj name) is to be evaluated, its value
is looked up in that alist.
For example, suppose that you evaluate the following forms in the top-level
ACL2 loop.
(defstobj st fld)
(fld st)
To evaluate the expression, (fld st), ACL2 calls trans-eval
— or more accurately its variant, trans-eval-default-warning
— on that expression. (We generally consider all such variants to be
the same as trans-eval for purposes of this documentation topic.)
Although st has the syntax of a global variable, it is bound in the
user-stobj-alist. Here we see trans-eval in action.
ACL2 !>(trace$ trans-eval-default-warning)
((TRANS-EVAL-DEFAULT-WARNING))
ACL2 !>(fld st)
1> (TRANS-EVAL-DEFAULT-WARNING (FLD ST)
TOP-LEVEL |*the-live-state*| T)
<1 (TRANS-EVAL-DEFAULT-WARNING NIL ((NIL))
|*the-live-state*|)
NIL
ACL2 !>
This call of trans-eval (or more accurately,
trans-eval-default-warning) invokes an ACL2 evaluator (ev form alist
state ...), by calling it on the form (fld st) and an alist that binds
the variable st to its value in the user-stobj-alist component of
the ACL2 state. We may refer to this value as the ``global value of''
st.
We can of course update this stobj.
ACL2 !>(update-fld 3 st)
1> (TRANS-EVAL-DEFAULT-WARNING (UPDATE-FLD 3 ST)
TOP-LEVEL |*the-live-state*| T)
<1 (TRANS-EVAL-DEFAULT-WARNING NIL ((ST) . REPLACED-ST)
|*the-live-state*|)
<st>
ACL2 !>(fld st) ; check that the update occurred
1> (TRANS-EVAL-DEFAULT-WARNING (FLD ST)
TOP-LEVEL |*the-live-state*| T)
<1 (TRANS-EVAL-DEFAULT-WARNING NIL ((NIL) . 3)
|*the-live-state*|)
3
ACL2 !>
We see above that the global value of st was indeed updated by
evaluating the update-fld call. That is: the value of st in the
user-stobj-alist of the ACL2 state was updated by calling trans-eval on the expression, (update-fld 3 st). More generally: as
trans-eval returns, it updates the user-stobj-alist of the ACL2
state according to all stobj values that have been returned.
