|
|
|---|
|
|
|
|---|
An example illustrating ACL2 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 !>