Def-1d-arr
Defines a abstract-stobj that logically just appears to be a
typed list but is implemented as an array.
Def-1d-arr produces an abstract-stobj and associated
get, set, resize, and length functions. Logically the
stobj just looks like an (optionally) typed list. But for execution, these
functions are stobj array operations.
How is this any better than just using defstobj to define a new stobj
with an array field? With a regular defstobj, the stobj is logically
viewed as a singleton list whose car holds the contents. With
def-1d-arr this extra layer goes away: the stobj itself, rather than its
car, looks like the list of elements.
This difference is slight, but it can help to simplify reasoning, e.g., it
can make congruence-based reasoning via equivalence relations
like ACL2::list-equiv and ACL2::set-equiv easier to apply to your
array, and can also make it easier to use proof strategies like ACL2::equal-by-nths.
Example
The following defines a bit array named bitarr.
(def-1d-arr bitarr ;; Stobj name
:slotname bit ;; Base name for accessor functions
:pred bitp ;; Element type (optional)
:type-decl bit ;; Element type-spec (optional)
:fix bfix ;; Element fixing function (optional)
:default-val 0 ;; Element default value (for resizing)
:parents (std/stobjs)) ;; XDOC parent topics
Keyword Options
- :slotname and :pkg-sym
- The :slotname influences the names of the array get, set, length, and
resize functions. In the example above, using bit results in functions
named get-bit, set-bit, bits-length, and resize-bits.
Default: <arrname>val.
- The :pkg-sym, if given, determines the package in which any newly
created symbols will be interned. It defaults to the array name.
- :pred
- This can be used to restrict the types of elements that can be put into the
array. It impacts the array recognizer's definition and the guard of the array
functions. The default is nil, meaning that there are no restrictions and
any kind of element can be put into the array.
- :default-val
- This gives the default array element for resizing, i.e., the
:initially argument to the underlying stobj. This is often
necessary when you provide a restricted :pred, because the default value
needs to satisfy the predicate.
- :type-decl
- This provides a Common Lisp ACL2::type-spec declaration for the
array element's type. It primarily affects memory efficiency and performance.
It must sensibly agree with the given pred.
- :fix
- Optional, requires a compatible :pred. This alters the logical
definition of the getting function so that it always produces a result of the
correct type. For example, by using :fix bfix above, get-bit will be
defined as (bit-fix (nth i bitarr)) instead of just a call of nth.
- :parents, :short, :long
- These options are as in defxdoc. Note that you typically don't need
to give :short or :long descriptions because reasonable boilerplate
documentation can be generated automatically.
