|
|
|---|
|
|
|
|---|
Trans-eval deals in global stobjs.
This topic assumes familiarity with the relatively advanced utility, trans-eval. In particular, see trans-eval-and-stobjs for relevant background. It may also be helpful to see user-stobjs-modified-warnings.
A stobj may be locally bound by stobj-let or with-local-stobj. But trans-eval ignores such local bindings! The following example illustrates this point.
(defstobj st fld) (defun f (x state) (declare (xargs :stobjs state :mode :program)) (with-local-stobj st (mv-let (state local-fld st) (mv-let (erp val state) (trans-eval `(update-fld ',x st) 'f state nil) (declare (ignore erp val)) (mv state (fld st) st)) (mv state local-fld)))) ; The following returns (<state> NIL). Thus, the return value of local-fld ; indicated above, which is the value of the fld of the locally-bound st, is ; nil: trans-eval did not update the locally-bound stobj! (f 3 state) ; On the other hand the global stobj, st, was indeed updated by the call of f ; just above. (assert-event (equal (fld st) 3))
Here is another such example, this time using nested-stobjs instead of with-local-stobj.
(defstobj sub1 sub1-fld1) (defstobj top1 (top1-fld :type sub1)) (defun g (x top1 state) (declare (xargs :stobjs (top1 state) :mode :program)) (stobj-let ((sub1 (top1-fld top1))) ; bindings (sub1 state) ; producer variables (mv-let (erp val state) ; producer ; NOTE: The reference to sub1 inside the following trans-eval call is actually ; a reference to the global sub1 from the user-stobj-alist, not to the sub1 ; bound by stobj-let above. Thus, this trans-eval call updates the global ; stobj, sub1, not the locally bound sub1 that is a field of top1. (trans-eval `(update-sub1-fld1 ',x sub1) 'g state t) (declare (ignore erp val)) (mv sub1 state)) (mv top1 state) ; consumer )) (g 7 top1 state) ; The global stobj, sub1, has been updated by the call of g just above. (assert-event (equal (sub1-fld1 sub1) 7)) (g 8 top1 state) ; The global stobj, sub1, has been updated by the call of g just above. (assert-event (equal (sub1-fld1 sub1) 8)) ; Obtain the sub1 field of top1. (defun get-sub1-of-top1 (top1) (declare (xargs :stobjs top1 :mode :program)) (stobj-let ((sub1 (top1-fld top1))) ; bindings (val) ; producer variable (sub1-fld1 sub1) ; producer val ; consumer )) ; The calls of g above did not update the locally bound sub1. ; That is, they did not update the sub1 field of top1. (assert-event (equal (get-sub1-of-top1 top1) nil))