• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
          • Defstobj
          • Defabsstobj
          • Stobj-table
          • Preservation-thms
          • Nested-stobjs
          • Defrstobj
          • User-stobjs-modified-warnings
          • With-global-stobj
          • Stobj-example-1
          • Defrstobj
          • Stobj-example-3
          • Stobj-example-1-proofs
          • With-local-stobj
          • Stobj-example-1-defuns
          • Declare-stobjs
          • Trans-eval-and-stobjs
          • With-local-state
          • Stobj-example-2
          • Stobj-example-1-implementation
          • Swap-stobjs
            • Resize-list
            • Nth-aliases-table
            • Trans-eval-and-locally-bound-stobjs
            • Std/stobjs
            • Count-keys
            • Update-nth-array
          • State
          • Memoize
          • Mbe
          • Io
          • Defpkg
          • Apply$
          • Mutual-recursion
          • Loop$
          • Programming-with-state
          • Arrays
          • Characters
          • Time$
          • Loop$-primer
          • Fast-alists
          • Defmacro
          • Defconst
          • Evaluation
          • Guard
          • Equality-variants
          • Compilation
          • Hons
          • ACL2-built-ins
          • Developers-guide
          • System-attachments
          • Advanced-features
          • Set-check-invariant-risk
          • Numbers
          • Irrelevant-formals
          • Efficiency
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Stobj
    • ACL2-built-ins

    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.