ARRAYS-EXAMPLE

an example illustrating ACL2 arrays
Major Section:  ARRAYS

The example below illustrates the use of ACL2 arrays. It is not, of course, a substitute for the detailed explanations provided elsewhere (see arrays, including subtopics).

ACL2 !>(defun defarray (name size initial-element)
         (compress1 name
                    (cons (list :HEADER
                                :DIMENSIONS (list size)
                                :MAXIMUM-LENGTH (1+ size)
                                :DEFAULT initial-element
                                :NAME name)
                          nil)))

Since DEFARRAY is non-recursive, its admission is trivial.  We observe
that the type of DEFARRAY is described by the theorem
(AND (CONSP (DEFARRAY NAME SIZE INITIAL-ELEMENT))
     (TRUE-LISTP (DEFARRAY NAME SIZE INITIAL-ELEMENT))).
We used the :type-prescription rule COMPRESS1.

Summary
Form:  ( DEFUN DEFARRAY ...)
Rules: ((:TYPE-PRESCRIPTION COMPRESS1))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.02, other: 0.00)
 DEFARRAY
ACL2 !>(assign my-ar (defarray 'a1 5 17))
 ((:HEADER :DIMENSIONS (5)
           :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
ACL2 !>(aref1 'a1 (@ my-ar) 3)
17
ACL2 !>(aref1 'a1 (@ my-ar) 8)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol AREF1,
which is
(AND (ARRAY1P NAME L) (INTEGERP N) (>= N 0) (< N (CAR (DIMENSIONS NAME L)))),
is violated by the arguments in the call (AREF1 'A1 '(#) 8).

ACL2 !>(assign my-ar (aset1 'a1 (@ my-ar) 3 'xxx))
 ((3 . XXX)
  (:HEADER :DIMENSIONS (5)
           :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
ACL2 !>(aref1 'a1 (@ my-ar) 3)
XXX
ACL2 !>(aset1 'a1 (@ my-ar) 3 'yyy) ; BAD: (@ my-ar) now points to
                                    ;      an old copy of the array!
((3 . YYY)
 (3 . XXX)
 (:HEADER :DIMENSIONS (5)
          :MAXIMUM-LENGTH 6 :DEFAULT 17 :NAME A1))
ACL2 !>(aref1 'a1 (@ my-ar) 3) ; Because of "BAD" above, the array
                               ; access is done using assoc rather
                               ; than Lisp aref, hence is slower;
                               ; but the answer is still correct,
                               ; reflecting the value in (@ my-ar),
                               ; which was not changed above.


**********************************************************
Slow Array Access!  A call of AREF1 on an array named
A1 is being executed slowly.  See :DOC slow-array-warning
**********************************************************

XXX
ACL2 !>