Pl
Print the rules for the given name or term
Examples:
:pl foo ; prints rules that rewrite some call of foo
:pl quote ; prints rules that rewrite quoted constants
:pl (+ x y) ; prints rules that rewrite (+ x y)
:pl '(4 1 2 3) ; prints rules that rewrite '(4 1 2 3)
Also see pl2, which restricts output to rules that you specify for a
given term.
Pl takes one argument, which should be a symbol or a term.
First suppose that the argument is a symbol. Then it should be the symbol
quote, a function symbol, or else a macro alias for a function
symbol (see macro-aliases-table), which is treated as the corresponding
function symbol. When the argument to pl is quote, pl displays
the rules that rewrite quoted constants, i.e., the :rewrite-quoted-constant rules. Otherwise, :pl displays rules that apply
to terms whose top function symbol is the one specified, specifically, rules
of class :rewrite, :definition, :meta,
:linear, :type-prescription, :forward-chaining, :elim, and :induction. For each
class, rules are displayed in order from the most recently submitted rule to
the oldest, with two exceptions: :rewrite, :definition, and
:meta rules are considered as one ``class'' for this purpose; and only
the current (most recent) :elim rule is displayed.
Otherwise the argument should be a term. Note that the term may have
user-level syntax (that is, it may be an untranslated term; see term),
for example one that is obtained from the theorem prover's output; in
particular, macro calls are permitted. When supplied a term, :pl
displays rules that are (possibly) applicable to the given term, in order (as
above, most recent rule first) for each of these four cases: first
:rewrite-quoted-constant, :rewrite and :definition rules, then :meta rules, then :linear rules, and
finally :type-prescription rules. Each rule is displayed with
additional information, such as the hypotheses that remain after applying some
simple techniques to discharge them that are likely to apply in any
context. (Those techniques include type-reasoning, forward-chaining, and some attempts to deal with free-variables
including handling of binding hypotheses, syntaxp and bind-free.)
It is important to remember that rules displayed as ``applicable'' by
pl may in fact not be used because of logical requirements, like
failure to relieve the hypotheses in the context in which the target occurs,
or because of heuristics such as those controlled by the :loop-stopper.
A reminder of this can sometimes be seen in the output of pl. For
example, if the list of un-discharged hypotheses contains nil then the
hypotheses of this instance the rule are known, by trivial means, to be
unsatisfiable.
Similarly, :rewrite-quoted-constant rules of form [2] are
not actually applied unless a certain computation produces a quoted constant.
For example,
ACL2 !>(include-book "demos/rewrite-quoted-constant-examples" :dir :system)
includes a form [2] rule, named form-2-rule, which will rewrite
any quoted constant occurring a position admitting set-equalp as a
congruence. The rule will apply the function drop-dups-and-sort to the
constant and replace the constant by the result — if the result is a
quoted constant. That function coerces the constant to a true-listp,
drops duplicate elements, and sorts the list. Thus, '(3 1 1 2 . 77) in a
set-equalp occurrence would be rewritten to '(1 2 3). However, that
replacement is only made if (drop-dups-and-sort '(3 1 1 2 . 77)) is
rewritten to a quoted constant.
ACL2 !>:pl '(3 1 1 2 . 77)
will include an entry for form-2-rule, but the entry reads:
New term: (DROP-DUPS-AND-SORT '(3 1 1 2 . 77))
Hypotheses: <none>
Equiv: SET-EQUALP
Substitution: ((LST '(3 1 1 2 . 77)))
WARNING: The new term above is only used if it rewrites to a quoted
constant!
How might the replacement not be made? One way is if
drop-dups-and-sort and its executable-counterpart are both
disabled and there are no :rewrite rules about that function.
Note that for :meta rules, only those are displayed that meet
two conditions: the application of the metafunction returns a term different
from the input term, and if there is a hypothesis metafunction then it also
returns a term. (A subtlety: In the case of extended metafunctions (see extended-metafunctions), a trivial metafunction context is used for the
application of the metafunction.)
Note that some rule classes are not handled by :pl. In particular, if
you want to see all :clause-processor rules, issue the command
:print-clause-processor-rules, and for trusted clause-processors,
(table trusted-cl-proc-table); see clause-processor and see define-trusted-clause-processor.
