Swap-stobjs
Swap two congruent stobjs
See stobj for relevant background on single-threaded
objects.
The macro call (swap-stobjs st1 st2) is allowed exactly when st1
and st2 are congruent stobjs. The logical meaning is simply to
return the two stobjs in reverse order, (list st2 st1):
Macro: swap-stobjs
(defmacro swap-stobjs (x y)
(cons 'mv (cons y (cons x 'nil))))
However, for purposes of tracking single-threadedness, the result (mv
st2 st1) of (swap-stobjs st1 st2) is treated as a list of new values
for the stobjs st1 and st2, respectively. That is, after this call
of swap-stobjs, the new value of stobj st1 is considered to be the
old value of st2, and the new value of stobj st2 is considered to be
the old value of st1. This is illustrated by the following example.
(defstobj st1 fld1)
(defstobj st2 fld2 :congruent-to st1)
(defstobj st3 fld3 :congruent-to st1)
(defun foo (st1 st2)
(declare (xargs :stobjs (st1 st2)))
(swap-stobjs st1 st2))
; Initialize:
(update-fld1 3 st1)
(update-fld2 4 st2)
; Swap:
(foo st1 st2)
; Check that the swap took place:
(assert-event (equal (fld2 st2) 3))
(assert-event (equal (fld1 st1) 4))
The example above is essentially the first of several that may be found in
the community-book, books/system/tests/swap-stobjs.lisp. Those
examples illustrate that swap-stobjs has the expected effect even when
stobjs are involved that are bound by with-local-stobj or stobj-let. It also explains subtle interaction with trans-eval. For
another example, see books/demos/swap-stobj-fields.lisp
