• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/system
      • Std/basic
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
        • Stobj-updater-independence
        • Def-1d-arr
        • Defstobj-clone
        • Def-2d-arr
          • Defabsstobj-events
          • Bitarr
          • Natarr
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Std/stobjs

    Def-2d-arr

    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) stobj array.

    Example

    The following defines a two-dimensional array of integers named intmatrix.

    (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

    Keyword Options

    :prefix
    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.
    :pred
    Specifies an element recognizer function. This can be used to restrict the types of elements that 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 a single element's type. It primarily affects memory efficienty and performance. If provided, it must sensibly agree with the given :pred.
    :fix
    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 array.
    :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.

    Advanced/Obscure Options

    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.