		Search-engine friendly clone of the ACL2 documentation.

Flush-compress

Flush the under-the-hood array for the given name

Example Form:
(flush-compress 'my-array)

General Form:
(flush-compress name)

where name is a symbol.

Recall that (compress1 nm alist) associates an under-the-hood raw Lisp one-dimensional array of name nm with the given association list, alist, while (compress2 nm alist) is the analogous function for two-dimensional arrays; see compress1 and see compress2. The only purpose of flush-compress, which always returns nil, is to remove the association of any under-the-hood array with the given name, thus eliminating slow array accesses (see slow-array-warning). It is not necessary if the return values of compress1 and compress2 are always used as the ``current'' copy of the named array, and thus flush-compress should rarely, if ever, be needed in user applications.

Nevertheless, we provide the following contrived example to show how flush-compress can be used to good effect. Comments have been added to this log to provide explanation.

ACL2 !>(assign a (compress1 'demo
                            '((:header :dimensions (5)
                                       :maximum-length 15
                                       :default uninitialized
                                       :name demo)
                              (0 . zero)
                              (1 . one))))
 ((:HEADER :DIMENSIONS (5)
           :MAXIMUM-LENGTH
           15 :DEFAULT UNINITIALIZED :NAME DEMO)
  (0 . ZERO)
  (1 . ONE))
ACL2 !>(aref1 'demo (@ a) 0)
ZERO
; As expected, the above evaluation did not cause a slow array warning.  Now
; we associate a different under-the-hood array with the name 'demo.
ACL2 !>(compress1 'demo
                  '((:header :dimensions (5)
                             :maximum-length 15
                             :default uninitialized
                             :name demo)
                    (0 . zero)))
((:HEADER :DIMENSIONS (5)
          :MAXIMUM-LENGTH
          15 :DEFAULT UNINITIALIZED :NAME DEMO)
 (0 . ZERO))
; The following array access produces a slow array warning because (@ a) is
; no longer associated under-the-hood with the array name 'demo.
ACL2 !>(aref1 'demo (@ a) 0)

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

ZERO
; Now we associate under-the-hood, with array name 'demo, an alist equal to
; (@ a).
ACL2 !>(compress1 'demo
                  '((:header :dimensions (5)
                             :maximum-length 15
                             :default uninitialized
                             :name demo)
                    (0 . zero)
                    (1 . one)))
((:HEADER :DIMENSIONS (5)
          :MAXIMUM-LENGTH
          15 :DEFAULT UNINITIALIZED :NAME DEMO)
 (0 . ZERO)
 (1 . ONE))
; The following array access is still slow, because the under-the-hood array
; is merely associated with a copy of (@ a), not with the actual object
; (@ a).
ACL2 !>(aref1 'demo (@ a) 0)

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

ZERO
; So we might try to fix the problem by recompressing. But this doesn't
; work.  It would work, by the way, if we re-assign a:
; (assign a (compress1 'demo (@ a))).  That is why we usually will not need
; flush-compress.
ACL2 !>(compress1 'demo (@ a))
((:HEADER :DIMENSIONS (5)
          :MAXIMUM-LENGTH
          15 :DEFAULT UNINITIALIZED :NAME DEMO)
 (0 . ZERO)
 (1 . ONE))
ACL2 !>(aref1 'demo (@ a) 0)

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

ZERO
; Finally, we eliminate the warning by calling flush-compress before we call
; compress1.  The call of flush-compress removes any under-the-hood
; association of an array with the name 'demo.  Then the subsequent call of
; compress1 associates the object (@ a) with that name.  (Technical point:
; compress1 always associates the indicated name with the value that it
; returns.  in this case, what compress1 returns is (@ a), because (@ a) is
; already, logically speaking, a compressed array1p (starts with a :header
; and the natural number keys are ordered).
ACL2 !>(flush-compress 'demo)
NIL
ACL2 !>(compress1 'demo (@ a))
((:HEADER :DIMENSIONS (5)
          :MAXIMUM-LENGTH
          15 :DEFAULT UNINITIALIZED :NAME DEMO)
 (0 . ZERO)
 (1 . ONE))
ACL2 !>(aref1 'demo (@ a) 0)
ZERO
ACL2 !>

Function: flush-compress

(defun flush-compress (name)
       (declare (xargs :guard t))
       (declare (ignore name))
       nil)