Major Section: EVENTS
Examples: ACL2 !>(invisible-fns-table (w state)) ((binary-+ unary--) (binary-* unary-/) (unary-- unary--) (unary-/ unary-/))Among other things, the setting above has the effect of making
unary--
``invisible'' for the purposes of applying permutative :
rewrite
rules to binary-+
trees. Also see add-invisible-fns,
see remove-invisible-fns, and see set-invisible-fns-table.See table for a general discussion of tables.
The ``invisible functions table'' is an alist with elements of the following
form, where fn
is a function symbol and the ufni
are unary function
symbols in the current ACL2 world, and k
is at least 1.
(fn ufn1 ufn2 ... ufnk)
This table thus associates with certain function symbols, e.g., fn
above, a set of unary functions, e.g., the ufni
above. The ufni
associated with fn
in the invisible functions table are said to be
``invisible with respect to fn
.'' If fn
is not the car
of any
pair in the alist
, then no function is invisible for it. Thus for
example, setting the invisible functions alist to nil
completely
eliminates the consideration of invisibility.
The notion of invisibility is involved in the use of the
:
loop-stopper
field of :
rewrite
rules to prevent the indefinite
application of permutative rewrite rules. Roughly speaking, if
rewrite rules are being used to permute arg
and (ufni arg) inside of
a nest of fn
calls, and ufni
is invisible with respect to fn
, then
arg
and (ufni arg)
are considered to have the same ``weight'' and
will be permuted so as to end up as adjacent tips in the fn
nest.
See loop-stopper.