• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
          • Slow-array-warning
          • Compress1
          • Aset1
            • Aset1-trusted
          • Aref1
          • Flush-compress
          • Aset2
          • Compress2
          • Header
          • Aref2
          • Maximum-length
          • Dimensions
          • Default
          • Aset1-trusted
          • Arrays-example
          • Array2p
          • Array1p
          • Maybe-flush-and-compress1
        • 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
  • Arrays
  • ACL2-built-ins

Aset1

Set the elements of a 1-dimensional array

Example Form:
(aset1 'delta1 a (+ i k) 27)

General Form:
(aset1 name alist index val)

where name is a symbol, alist is a 1-dimensional array named name, index is a legal index into alist, and val is an arbitrary object. See arrays for details. Roughly speaking this function ``modifies'' alist so that the value associated with index is val. More precisely, it returns a new array, alist', of the same name and dimension as alist that, under aref1, is everywhere equal to alist except at index where the result is val. That is, (aref1 name alist' i) is (aref1 name alist i) for all legal indices i except index, where (aref1 name alist' i) is val.

In order to ``modify'' alist, aset1 conses a new pair onto the front. If the length of the resulting alist exceeds the :maximum-length entry in the array header, aset1 compresses the array as with compress1.

It is generally expected that the ``semantic value'' of name will be alist (see arrays). This function operates in virtually constant time whether this condition is true or not (unless the compress1 operation is required). But the value returned by this function cannot be used efficiently by subsequent aset1 operations unless alist is the semantic value of name when aset1 is executed. Thus, if the condition is not true, aset1 prints a slow array warning to the comment window. See slow-array-warning.

Note that aset1 is marked as having invariant-risk, which can affect the execution of :program-mode functions. To get around this problem (but only with great care!), see aset1-trusted.

Function: aset1

(defun
     aset1 (name l n val)
     (declare (xargs :guard (and (array1p name l)
                                 (integerp n)
                                 (>= n 0)
                                 (< n (car (dimensions name l))))))
     (let ((l (cons (cons n val) l)))
          (cond ((> (length l) (maximum-length name l))
                 (compress1 name l))
                (t l))))

Subtopics

Aset1-trusted
Set the elements of a 1-dimensional array without invariant-risk