		Search-engine friendly clone of the ACL2 documentation.

Std/stobjs

Defstobj-clone

Create a new stobj that is :congruent-to an existing (concrete or abstract) stobj, and can be given to functions that operate on the old stobj.

Defstobj-clone lets you easily introduce a new stobj that is :congruent-to an existing stobj. This allows you to have two (or more) copies of a stobj that coexist simultaneously.

Basic Example

If you want to write an algorithm that operates on two bit arrays, you might clone the bitarr to get a second stobj, bitarr2. A minimal way to do this is:

(defstobj-clone bitarr2 bitarr :suffix "2")

This introduces:

A new stobj, bitarr2, which is congruent to bitarr, and
New functions that are basically renamed bitarr operations. In particular, whereas bitarr has operations like get-bit and set-bit, we'll get new functions named get-bit2 and set-bit2.

Usually you can just ignore these new functions. They are added only because of the way that ACL2 stobj definition works and, strictly speaking, are not really necessary for anything else because you can still use the original stobj's functions on the new stobj.

Ignoring the new functions is particularly useful when you have already built up more complex functionality on top of a stobj. That is, if you've implemented functions like clear-range and invert-range or similar, you can just use these on bitarr2 without reimplementing them.

Renaming Accessors

On the other hand, it may occasionally be useful for code clarity to rename the new functions in some semantically meaningful way. For instance, if your cloned bit array will be used as a seen table, it may be convenient to use operations like set-seen instead of set-bit.

To support using such semantically meaningful names, defstobj-clone has a variety of options. Here is a contrived example that uses all of them:

(defstobj-clone fancy-bitarr bitarr
  :strsubst (("GET" . "FETCH")     ;; Substring replacements to make
             ("SET" . "INSTALL"))  ;;   (capitalized per symbol names)
  :prefix "MY-"                      ;; Name prefix to add
  :suffix "-FOR-JUSTICE"             ;; Name suffix to add
  :pkg acl2::rewrite                   ;; Package for new symbols
                                       ;;   default: new stobj name
  )

The result is to define new analogues of the bitarr functions with the following names:

bitarrp       -->  fancy-bitarrp
create-bitarr -->  create-fancy-bitarr
bits-length   -->  my-bits-length-for-justice
get-bit       -->  my-fetch-bit-for-justice
set-bit       -->  my-install-bit-for-justice
resize-bits   -->  my-resize-bits-for-justice

Alternate Syntax for Abstract Stobjs

For an abstract stobj, the accessors/updaters are known as "exports". Another way to specifying their names in the new stobj is to provide the :exports argument, which should be a list of symbols corresponding to the exported functions from the original abstract stobj. When this is provided, the other keyword arguments are unused. For example:

(defstobj-clone xx-bitarr bitarr
  :exports (xx-size xx-nth !xx-nth xx-resize))

Defines a new xx-bitarr stobj with:

bitarrp       --> xx-bitarrp
create-bitarr --> create-xx-bitarr
bits-length   --> xx-size
get-bit       --> xx-nth
set-bit       --> !xx-nth
resize-bits   --> xx-resize