### USING-TABLES-EFFICIENTLY

Notes on how to use tables efficiently
```Major Section:  TABLE
```

(Thanks to Jared Davis for contributing this documentation topic, to which we have made only minor modifications.)

Suppose your book contains `table` events, or macros that expand into `table` events, of the following form:

```   (table my-table 'my-field <computation>)
```
Then `<computation>` will be evaluated twice during `certify-book` and again every time you include the book with `include-book`. In some cases this overhead can be avoided using `make-event`.

See also `books/make-event/defconst-fast.lisp` for an analogous trick involving `defconst`.

## Some Related Topics

• ### MAKE-EVENT -- evaluate (expand) a given form and then evaluate the result

As an example, suppose we want to store numbers in a table only if they satisfy some computationally expensive predicate. We'll introduce a new book, `number-table.lisp`, and create a table to store these numbers:
```  (table number-table 'data nil)
```
Instead of implementing a ``computationally expensive predicate,'' we'll write a function that just prints a message when it is called and accepts even numbers:
```(defun expensive-computation (n)
(prog2\$ (cw "Expensive computation on ~x0.~%" n)
(evenp n)))
```
Now we'll implement a macro, `add-number`, which will add its argument to the table only if it satisfies the expensive predicate:
```(defmacro add-number (n)
`(table number-table 'data
(let ((current-data
(cdr (assoc-eq 'data (table-alist 'number-table world)))))
(if (expensive-computation ,n)
(cons ,n current-data)
current-data))))
```
Finally, we'll call `add-number` a few times to finish the book.
```(add-number 1)
```
When we now invoke `(certify-book "number-table")`, we see the expensive predicate being called twice for each number: once in Step 2, the main pass, then again in Step 3, the admissibility check. Worse, the computation is performed again for each number when we use `include-book` to load `number-table`, e.g.,
```   ACL2 !>(include-book "number-table")
Expensive computation on 1.
Expensive computation on 2.
Expensive computation on 3.
```
To avoid these repeated executions, we can pull the test out of the `table` event using `make-event`. Here's an alternate implementation of `add-number` that won't repeat the computation:
```(defmacro add-number (n)
`(make-event
(if (expensive-computation ,n)
'(table number-table 'data
(cons ,n (cdr (assoc 'data
(table-alist 'number-table world)))))
'(value-triple :expensive-computation-failed))))
```
When we recertify `number-table.lisp`, we'll see the expensive computation is still called once for each number in Step 2, but is no longer called during Step 3. Similarly, the `include-book` no longer shows any calls of the expensive computation.