Major Section: EVENTS
This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization for a general discussion of memoization and the related features of hash consing and applicative hash tables.
Examples: (memoize 'foo) ; remember the values of calls ; of foo (memoize 'foo :condition t) ; same as above (memoize 'foo :condition '(test x)) ; memoize for args satisfying ; condition (memoize 'foo :condition 'test-fn) ; memoize for args satisfying ; test-fn (memoize 'foo :inline nil) ; do not inline the definition ; of foo
fn
evaluates to a user-defined function symbol;
condition
is either t
(the default)
or 't
or else evaluates to an expression whose free variables
are among the formal parameters of fn
; condition-fn
is
either nil
(the default) or else evaluates to a legal function
symbol. Further restrictions are discussed below.
Generally fn
must evaluate to a defined function symbol whose
guard
s have been verified. However, this value can be the
name of a macro that is associated with such a function symbol;
see macro-aliases-table. That associated function symbol is the
one called ``memoized'' in the discussion below, but we make no more
mention of this subtlety.
It is illegal to memoize a function that is already memoized. To turn off memoization, see unmemoize.
In the most common case, memoize
takes a single argument, which
evaluates to a function symbol. We call this function symbol the
``memoized function'' because ``memos'' are saved and re-used, in
the following sense. When a call of the memoized function is
evaluated, the result is ``memoized'' by associating the call's
arguments with that result, in a suitable table. But first an
attempt is made to avoid such evaluation, by doing a lookup in that
table on the given arguments for the result, as stored for a
previous call on those arguments. If such a result is found, then
it is returned without further computation. This paragraph also
applies if :condition
is supplied but is t
or 't
.
If in addition :condition-fn
is supplied, but :condition
is
not, then the result of evaluating :condition-fn
must be a
defined function symbol whose guards have been verified and
whose formal parameter list is the same as for the function being
memoized. Such a ``condition function'' will be run whenever the
memoized function is called, on the same parameters, and the lookup
or table store described above are only performed if the result from
the condition function call is non-nil
.
If however :condition
is supplied, then an attempt will be made
to define a condition function whose guard and formal
parameters list are the same as those of the memoized function, and
whose body is the result, r
, of evaluating the given
condition
. The name of that condition function is the result of
evaluating :condition-fn
if supplied, else is the result of
concatenating the string "-MEMOIZE-CONDITION"
to the end of
the name of the memoized function. The condition function will be
defined with guard verification turned off, but that definition
will be followed immediately by a verify-guards
event; and
this is where the optional :hints
and :otf-flg
are attached.
At evaluation time the condition function is used as described in
the preceding paragraph; so in effect, the condition (r
, above)
is evaluated, with its variables bound to the corresponding actuals
of the memoized function call, and the memoized function attempts a
lookup or table store if and only if the result of that evaluation
is non-nil
.
Calls of this macro generate events of the form
(table memoize-table fn (list condition-fn inline))
. When
successful, the returned value is of the form
(mv nil function-symbol state)
.
When :inline
has value nil
, then memoize
does not use
the definitional body of fn
in the body of the new, memoized
definition of fn
. Instead, memoize
lays down a call to the
symbol-function
for fn
that was in effect prior to
memoization. Use value t
for :inline
to avoid memoizing
recursive calls to fn
directly from within fn
.
If :trace
has a non-nil
value, then memoize
also traces
in a traditional Lisp style. If :trace
has value notinline
or notinline
, then a corresponding declaration is added at the
beginning of the new definition of fn
.
Memoize
works for functions that have stobj arguments or
return stobj values. However, in some cases the memoized
version of the function may execute much less inefficiently than the
unmemoized version.
Memoize
causes an error if fn
uses state
as an
explicit parameter.