Major Section: MISCELLANEOUS
General Form of :hints: (hint1 hint2 ... hintk)Each element, hinti, must be either a common hint or a computed hint.
A common hint is of the form
(goal-spec :key1 val1 ... :keyn valn)where
goal-specis as specified in goal-spec and each
valiis as specified in hints. Among the ``common hints'' we include both the primitive hints and user-defined custom keyword hints (see custom-keyword-hints).
A computed hint may be a function symbol,
fn, of three, four or seven
arguments. Otherwise, a computed hint is a term with the following
(a) the only free variables allowed in the term are
(b) the output signature of the term is either
(MV * * STATE), which is
to be treated as an error triple (see below), or is
*, denoting a single
non-stobj value; and
(c) in the former case of (b) above, the term is single-threaded in
If a computed hint is a function symbol
fn, whose arity n is therefore
three, four, or seven, then it is treated as the term resulting from applying
fn to the first n variables shown in (a) above. Notice that it must
then return a single non-stobj value, not an error triple, since
state is not one of the first seven variables shown in (a).
Note: Error triples are an ACL2 idiom for implementing ``errors.'' If a
(mv erp val state) in a context in which ACL2 is
respecting the error triple convention (see ld-error-triples and
see ld-error-action), then an error is deemed to have occurred if
nil. The computation is expected to have printed an appropriate
error message to
state and further computation is aborted. On the
other hand, if a computation returns an error triple in which
erp is nil,
then ``value'' of the computation is taken to be the second component,
val, of the triple (along with the possibly modified
The function symbol cases are treated as abbreviations of the term
(fn ID CLAUSE WORLD),
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP), or
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX)
as appropriate for the arity of
fn. (Note that this tells you which
fn is which.) Moreover, in these cases the value returned
must be a single ordinary (non-stobj) value, not an error triple. In
the discussion below we assume all computed hints are of the term form.
Indeed, we almost assume all computed hints are of the 3 and 4 argument
forms. We only comment briefly on the 7 argument form in
The semantics of a computed hint term is as follows. On every subgoal, the
term is evaluated in an environment in which the variables mentioned in (a)
above are bound to context-sensitive values explained below. Either the
computed hint signals an error, in which the proof attempt aborts, or else it
returns a value,
val and a new state,
state. Any changes to those
state that affect logical soundness are undone; more
specifically, the values of symbols (sometimes called ``state global
variables'') in the list
*protected-system-state-globals* in the global
table of the state (see state) are restored when changed during evaluation.
val, of a non-erroneous computed hint calculation is either
nil, which means the computed hint did not apply to the subgoal in
question, or it is an alternating list of
:keyi vali pairs as specified
in hints. With one exception, those new hints are applied to the given
subgoal as though the user had typed them explicitly.
The exception is that the first keyword in the returned
val is allowed to
:COMPUTED-HINT-REPLACEMENT. Its value should be
t, or a
list of terms. If this keyword is not present, the default value of
is provided. We explain
The evaluation of a hint term is done with guard checking turned off
(see set-guard-checking); e.g., the form
(car 23) in a
computed hint returns
nil as per the axioms.
When a non-
nil value is returned, the keyword/value pairs (other than the
:COMPUTED-HINT-REPLACEMENT) are used as the hint for the subgoal
in question. Thus, your job as the programmer of computed hints is either to
cause an error, typically by invoking
er, or to return a non-erroneous
value triple whose value is the list of keys and values you would have typed
had you supplied a common hint for the subgoal. (In particular, any theory
expressions in it are evaluated with respect to the global current-theory,
not whatever theory is active at the subgoal in question.) If the generated
list of keywords and values is illegal, an error will be signaled and the
proof attempt will be aborted.
The purpose of the
:COMPUTED-HINT-REPLACEMENT keyword and its value,
chr, is to change the list of hints. If
nil, then the
hint which was applied is removed from the list of hints that is passed down
to the children of the subgoal in question. This is the default. If
t, then the hint is left in the list of hints. This means that the
same hint may act on the children of the subgoal. Otherwise,
chr must be
a list of terms, each of which is treated as a computed hint. The hint which
was applied is deleted from the list of hints and the hints in
added to the list of hints passed to the children of the subgoal. The
ability to compute new hints and pass them down allows strange and wonderful
For these purposes, the goals produced by induction and the top-level goals of forcing rounds are not considered children; all original hints are available to them.
Only the first hint applicable to a goal, as specified in the user-supplied
:hints followed by the
default-hints-table, will be applied
to that goal. (For an advanced exception, see override-hints.)
It remains only to describe the bindings of the free variables.
Suppose the theorem prover is working on some clause, clause, named by some
goal-spec, e.g., "Subgoal *1/2'''" in some logical world, world.
Corresponding to the printed
goal-spec is an internal data structure
called a ``clause identifier'' id. See clause-identifier.
In the case of a common hint, the hint applies if the goal-spec of the hint is the same as the goal-spec of the clause in question.
In the case of a computed hint, the variable
ID is bound to the clause
id, the variable
CLAUSE is bound to the (translated form of the) clause,
and the variable
WORLD is bound to the current ACL2 world. The variable
STABLE-UNDER-SIMPLIFICATIONP is bound to
nil. It is bound
t only if the clause is known to be stable under simplification. That
is, the simplifier has been applied to the clause and did not change it.
Such a clause is sometimes known as a ``simplification checkpoint.'' It is
frequently useful to inject hints (e.g., to enable a rule or provide a
:use hint) only when the goal in question has stabilized. If a hint is
provided, the processing of the clause starts over with simplification.
STATE, they are provided so that you can pass them
er macro to print error messages. We recommend not writing
computed hints that otherwise change
The remaining variables,
PSPV are not documented yet. Only
users familiar with the internals of ACL2 are likely to need them or
understand their values.
For some instruction about how to use computed hints,