Defines a abstract-stobj for a two-dimensional array.
Def-2d-arr produces an abstract-stobj with associated
get2/set2, nrows/ncols, resize-rows/resize-cols
functions. Logically the stobj looks like a list of lists. But for execution,
these functions are stobj array operations that manipulate a (one-dimensional)
The following defines a two-dimensional array of integers named
(def-2d-arr intmatrix ;; Stobj name
:prefix imx ;; Base name for accessor functions (optional)
:pred integerp ;; Element type recognizer (optional)
:type-decl integer ;; Element type-spec (optional)
:fix ifix ;; Element fixing function (optional)
:default-val 0 ;; Element default value (for resizing)
:parents (my-algorithm)) ;; XDOC parent topics
- This is used for name generation. For example, by using imx above, we
will get functions named imx-nrows, imx-ncols, imx-resize-rows,
imx-resize-cols, imx-get2, and imx-set2. If you don't provide a
custom prefix we just use the stobj name.
- Specifies an element recognizer function. This can be used to restrict the
types of elements that can be put into the array.
- 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.
- This provides a Common Lisp ACL2::type-spec declaration for a single
element's type. It primarily affects memory efficienty and performance. If
provided, it must sensibly agree with the given :pred.
- Optional, requires a compatible :pred. This alters the logical
definition of the get2 function so that it always produces a result of the
correct type. For instance, by using :fix ifix above, imx-get2
will (logically) return the ifix of the element at that position in the
- :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.
In certain cases, you may want to use a stronger type-decl than your
pred really allows. For instance, you might want Common Lisp to know that
your array really contains fixnums, but logically just imagine that the array
contains arbitrary integers (and hence avoid the difficulty of bounds checking
when using the array).
The options :elt-guard, :elt-okp, and :xvar can be used to
customize the set function to accomplish this. See for instance s61v
in std/stobjs/tests/2d-arr.lisp for an example.