Clause-processor
Make or apply a :clause-processor rule (goal-level simplifier)
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
We will introduce clause-processor rules by way of the following example.
But note that the clause-processor utility is more general than this example
may suggest; for example, the second argument of evl0 in the hypothesis
need not be the same as its second argument in the conclusion.
; Example (which we'll return to, below):
(defthm correctness-of-note-fact-clause-processor
(implies (and (pseudo-term-listp cl)
(alistp a)
(evl0 (conjoin-clauses
(note-fact-clause-processor cl term))
a))
(evl0 (disjoin cl) a))
:rule-classes :clause-processor)
We begin this documentation with an introduction, focusing on the example
above, and then conclude with a detailed general discussion of
clause-processor rules. You might find it most useful simply to look at the
examples in community books directory books/clause-processors/; see file
Readme.lsp in that directory.
Also see define-trusted-clause-processor for documentation of an
analogous utility that does not require the clause-processor to be proved
correct. But please read the present documentation before reading about that
utility. Both utilities designate functions as ``clause-processors''. Such
functions must be executable — hence not constrained by virtue of being
introduced in the signature of an encapsulate — and must
respect stobj, df, and output arity restrictions. For example,
something like (car (mv ...)) is illegal; also see signature.
INTRODUCTION
A :clause-processor rule installs a simplifier at the level of goals,
where a goal is represented as a clause: a list of terms that is
implicitly viewed as a disjunction (the application of or). For
example, if ACL2 prints a goal in the form (implies (and p q) r), then
the clause might be the one-element list containing the internal
representation of this term — (implies (if p q 'nil) r) — but
more likely, the corresponding clause is ((not p) (not q) r). Note that
the members of a clause are translated terms; see term and
termp. For example, they do not contain calls of the macro AND,
and constants are quoted. The result of running a clause-processor must be a
list of legal clauses; see meta for a discussion of translated terms,
and for related discussion about ``forbidden'' function symbols, set-skip-meta-termp-checks.
The recognizer for a clause is the function term-listp and the
recognizer for a list of clauses is term-list-listp.
Note that clause-processor simplifiers are similar to metafunctions, and
similar efficiency considerations apply. See meta, in particular the
discussion on how to ``make a metafunction maximally efficient.''
Unlike rules of class :meta, rules of class
:clause-processor must be applied by explicit :clause-processor
hints; they are not applied automatically (unless by way of computed
hints; see computed-hints). But :clause-processor rules can be
useful in situations for which it is more convenient to code a simplifier that
manipulates the entire goal clause rather than individual subterms of terms in
the clause.
We begin with a simple illustrative example: a clause-processor that
assumes an alleged fact (named term in the example) and creates a
separate goal to prove that fact. We can extend the hypotheses of the current
goal (named cl in the example) with a term by adding the negation of that
term to the clause (disjunctive) representation of that goal. So the
following returns a list of two clauses: the result of adding term as a
hypothesis to the input clause, as just described, and a second clause
consisting only of that term. This list of two clauses can be viewed as the
conjunction of the first clause and the second clause (where again, each
clause is viewed as a disjunction).
(defun note-fact-clause-processor (cl term)
(declare (xargs :guard t)) ; optional, for better efficiency
(list (cons (list 'not term)
cl)
(list term)))
As with :meta rules, we need to introduce a suitable
evaluator; see defevaluator if you want details. Since we expect to
reason about the function not, because of its role in
note-fact-clause-processor as defined above, we include NOT in the
set of functions known to this evaluator. We also include IF, as is
often a good idea.
(defevaluator evl0 evl0-list
((not x) (if x y z)))
ACL2 can now prove the following theorem automatically. (This is the
example displayed at the outset of this documentation topic.) Of
course, :clause-processor rules about clause-processor functions less
trivial than note-fact-clause-processor may require lemmas to be proved
first! The function disjoin takes a clause and returns its disjunction
(the result of applying or to its members), and conjoin-clauses
applies disjoin to every element of a given list of clauses and then
conjoins (applies AND) to the corresponding list of resulting terms.
(defthm correctness-of-note-fact-clause-processor
(implies (and (pseudo-term-listp cl)
(alistp a)
(evl0 (conjoin-clauses
(note-fact-clause-processor cl term))
a))
(evl0 (disjoin cl) a))
:rule-classes :clause-processor)
Now let us submit a silly but illustrative example theorem to ACL2, to show
how a corresponding :clause-processor hint is applied. The hint says to
apply the clause-processor function, note-fact-clause-processor, to the
current goal clause and a ``user hint'' as the second argument of that
function, in this case (equal a a). Thus, a specific variable,
clause, is always bound to the current goal clause for the evaluation of
the :clause-processor hint, to produce a list of clauses. Since two
subgoals are created below, we know that this list contained two clauses.
Indeed, these are the clauses returned when note-fact-clause-processor is
applied to two arguments: the current clause, which is the one-element list
((equal (car (cons x y)) x)), and the user hint, (equal a a).
ACL2 !>(thm (equal (car (cons x y))
x)
:hints
(("Goal"
:clause-processor
(note-fact-clause-processor clause '(equal a a)))))
[Note: A hint was supplied for the goal above. Thanks!]
We now apply the verified :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE-
PROCESSOR to produce two new subgoals.
Subgoal 2
(IMPLIES (EQUAL A A)
(EQUAL (CAR (CONS X Y)) X)).
But we reduce the conjecture to T, by the :executable-counterpart of
IF and the simple :rewrite rule CAR-CONS.
Subgoal 1
(EQUAL A A).
But we reduce the conjecture to T, by primitive type reasoning.
Q.E.D.
Summary
Form: ( THM ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Proof succeeded.
ACL2 !>
That concludes our introduction to clause-processor rules and hints. We
turn now to detailed documentation.
DETAILED DOCUMENTATION
The signature of a clause-processor function, CL-PROC, must
have one of the following forms. Here, each st_i is a stobj
(possibly state) while the other parameters and results are not stobjs
(see stobj). Note that there need not be input stobjs in [3] —
i.e., k can be 0 — and even if there are, there need not be output
stobjs. In most ways [3] and [3+] are treated similarly; see make-summary-data for a discussion of the form of d in [3+] and, more
generally, for how [3+] differs from [3] by enhancing the summary.
[1] ((CL-PROC cl) => cl-list)
[2] ((CL-PROC cl hint) => cl-list)
[3] ((CL-PROC cl hint st_1 ... st_k) => (mv erp cl-list st_i1 ... st_in))
[3+] ((CL-PROC cl hint st_1 ... st_k) => (mv erp cl-list st_i1 ... st_in d))
We call cl-list the clauses-result. In [3] and [3+], we think
of the first component of the result as an error flag. Indeed, a proof will
instantly abort if that error flag is not nil.
We next discuss the legal forms of :clause-processor rules, followed
below by a discussion of :clause-processor hints. In the
discussion below, we use lower-case names to represent specific symbols, for
example implies, and also to represent stobj names; and we use
upper-case names to represent arbitrary pieces of syntax (which we will
describe), for example, CL.
If a :rule-classes specification includes
:clause-processor, then the corresponding term must have the following
form. (Additional ``meta-extract'' hypotheses, not shown or discussed below,
may be included as desired in order to use facts from the logical world to help prove the rule; see meta-extract for explanation of this
advanced feature.)
; General Form (omitting possible meta-extract hypotheses)
(implies (and (pseudo-term-listp CL)
(alistp A)
(EVL (conjoin-clauses <CL-LIST>)
B))
(EVL (disjoin CL) A))
Here EVL is a known evaluator; CL and A are distinct
non-stobj variables; and <CL-LIST> is an expression representing the
clauses returned by the clause-processor function CL-PROC, whose form
depends on the signature of that function, as follows. Typically
B is A, but it can be any term (useful when generalization is
occurring; see the example ``Test generalizing alist'' in community book
books/clause-processors/basic-examples.lisp). For cases [1] and [2]
above, <CL-LIST> is of the form (CL-PROC CL) or (CL-PROC CL
HINT), respectively, where in the latter case HINT is a non-stobj
variable distinct from the variables CL and A. For cases [3] and
[3+], <CL-LIST> is the result of wrapping the function
clauses-result around a call of CL-PROC:
(clauses-result (CL-PROC CL HINT ...))
Logically, clauses-result returns the cadr if the car
is NIL, and otherwise (for the error case) returns a list containing the
empty (false) clause. So in the non-error case, clauses-result picks out
the second result, denoted cl-list in [3] and [3+] above, and in the
error case the implication above trivially holds.
In the above theorem, we are asked to prove (EVL (disjoin CL) A)
assuming that the conjunction of all clauses produced by the clause processor
evaluates to a non-nil value under some alist B. In fact, we can
choose B so as to allow us to assume evaluations of the generated clauses
over many different alists. This technique is discussed in the community book
books/clause-processors/multi-env-trick.lisp, which introduces some
macros that may be helpful in accomplishing proofs of this type.
The clause-processor function, CL, must have a guard that ACL2 can
trivially prove from the hypotheses that the first argument of CL is
known to be a pseudo-term-listp and any stobj arguments are
assumed to satisfy their stobj predicates.
Next we specify the legal forms for :clause-processor hints.
The basic form is :clause-processor TERM, such that the translation of
TERM to a legal ACL2 term yields a call of a clause-processor function
(CL-PROC clause) or (CL-PROC clause HINT ...), where HINT is a
term whose only non-stobj free variable (if any) is the symbol, clause.
Note that the first argument of the call is literally the variable,
clause. Recall that at the time the :clause-processor hint is applied to
the clausal form CL of the current subgoal, clause is bound to
CL; moreover, any stobj names will be bound to the corresponding
stobjs.
But there are two additional general forms for :clause-processor
hints, which may viewed as abbreviations for the basic form discussed above.
The first additional general form, which we call the ``:function form'',
includes the following two classes of expressions.
:clause-processor (:function F)
:clause-processor (:function F :hint HINT)
The first of these :function forms abbreviates the following hint,
where either F is a macro-alias for the function symbol CL-PROC (see
add-macro-alias), and otherwise CL-PROC is just the function
symbol F.
:clause-processor (CL-PROC clause)
Similarly the second of the :function forms above abbreviates the
following, where CL-PROC is as above and the output signature of
CL-PROC is (nil nil st_1 ... st_k).
:clause-processor (CL-PROC clause HINT st_1 ... st_k)
Besides the ``:function form'', there is one more additional general
form for :clause-processor hint: a symbol, as follows.
:clause-processor F
This expands to a basic form as follows, depending on F.
- If F is a macro with one required argument or a function symbol with
one argument:
:clause-processor (F clause)
- If F is a macro with two required arguments or a function symbol with
two arguments:
:clause-processor (F clause nil)
- If F is a function symbol with inputs of the form [3] or [3+] above,
that is, with input signature (nil nil st_1 ... st_k):
:clause-processor (F clause nil st_1 ... st_k)
For examples of these syntactic forms, see community book
books/clause-processors/basic-examples.lisp). We turn now to discussion
of when a :clause-processor hint causes an abort.
A :clause-processor hint causes the proof to abort if the
clauses-result is not a list of clauses, i.e., a list of (translated) term lists in the current logical world. This test is done explicitly
every time a clause processor is run unless a :well-formedness-guarantee has been provided with the :clause-processor
rule or set-skip-meta-termp-checks has been used with an active trust
tag to skip the check at the user's risk.
The proof also aborts when the clause-processor function returns at least
two values and the first value returned — the ``erp'' value from
cases [3] and [3+] above — is not nil. In that case, erp is
used for printing an error message as follows: if it is a string, then that
string is printed; but if it is a non-empty true list whose first element is a
string, then it is printed as though by (fmt ~@0 (list (cons #\0 erp))
...) (see fmt). Otherwise, a non-nil erp value causes a
generic error message to be printed.
If there is no error as above, but the CL-PROC call returns a clause
list whose single element is equal to the input clause, then the hint is
ignored since we are left with the goal with which we started. In that case,
the other prover processes are then applied as usual (see hints-and-the-waterfall).
You can see all current :clause-processor rules by issuing the
following command: (print-clause-processor-rules).
The following paper discusses ACL2 clause-processors at a high level
suitable for a non-ACL2 audience:
M. Kaufmann, J S. Moore, S. Ray, and E. Reeber, ``Integrating External
Deduction Tools with ACL2.'' Journal of Applied Logic (Special Issue:
Empirically Successful Computerized Reasoning), Volume 7, Issue 1, March 2009,
pp. 3–25. Also published online (DOI 10.1016/j.jal.2007.07.002).
Preliminary version in: Proceedings of the 6th International Workshop on the
Implementation of Logics (IWIL 2006) (C. Benzmueller, B. Fischer, and
G. Sutcliffe, editors), CEUR Workshop
Proceedings Vol. 212, Phnom Penh, Cambodia, pp. 7–26, November
2006.
Subtopics
- Meta-extract
- Meta reasoning using valid terms extracted from context or world
- Set-skip-meta-termp-checks
- Skip output checks for meta functions and clause-processors
- Make-summary-data
- Return summary data from a clause-processor function
- Clause-processor-tools
- Noteworthy clause-processors
- Set-skip-meta-termp-checks!
- Skip output checks non-locally for meta functions and
clause-processors
