|
|
|---|
|
|
|
|---|
Special records designed for array-like usage.
Loading the library:
(include-book "data-structures/memories" :dir :system)
Memories are specialized records that are designed for array-like usage. Memories have a fixed size, and elements are accessed by the natural numbers 0, 1, ..., size-1, where size is the maximum size of the memory.
Unlike arrays, memories are based on trees. As a result, loading and storing into memories is slower than array access in a typical programming language, and requires an O(log_2 n) search for the right element. However, there are benefits to this system as well. We populate the tree structure as needed when writes occur, allowing us to conceptually represent very large arrays so long as we use them sparesely. Hence, memories are well suited for uses such as simulating the memory systems of processors or virtual machines with many gigabytes of memory, only some of which is used during simulation.
Memories are as easy to reason about as records (see misc/records.lisp) and we provide the same core 'record theorems' about them. However, the load and store operations on memories are guarded more strongly than the records book, in order to achieve efficiency.
See also ACL2::arrays and ACL2::stobjs for more efficient
implementations of small arrays. The records book,