Computed-hints
Computing advice to the theorem proving process
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-spec is as specified in goal-spec and each
:keyi and vali is 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 symbol, in which case it must be a function symbol
of three, four or seven arguments. Otherwise, a computed hint is a term with
the following properties:
(a) the only free variables allowed in the term are ID, CLAUSE,
WORLD, STABLE-UNDER-SIMPLIFICATIONP, HIST, PSPV, CTX,
and state;
(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 state.
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
that 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''; see
error-triple. If a computation returns (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 erp is non-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 state), and computation continues. For more information
about programming with error triples, see programming-with-state.
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
argument of 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 using-computed-hints-8.
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 parts of 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. The value, 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 be :COMPUTED-HINT-REPLACEMENT. Its value should be nil, t,
or a list of terms. If this keyword is not present, the default value of
nil is provided. We explain :COMPUTED-HINT-REPLACEMENT below.
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 optional :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 chr is nil, then the
computed 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 chr is t, then the computed hint is left in the list of hints.
This means that the same computed 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 computed hint which was applied is deleted from the list
of hints and the computed hints in chr are added to the list of hints
passed to the children of the subgoal. The ability to generate new computed
hints and pass them down allows strange and wonderful behavior. Notice that
certain hints, for example :in-theory and :expand hints, which
appear in the computed hint will continue to take effect even when chr is
nil. This might give one the false impression that a removed computed
hint still hangs around. See hints-and-the-waterfall for a more
detailed discussion about how :in-theory and other hints are handled in
the waterfall.
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
list of :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 a clause named by some
goal-spec, e.g., "Subgoal *1/2'''". 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 t or nil. It is bound
to 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.
As for CTX and state, they are provided so that you can pass
them to the er macro to print error messages.
The remaining variables, HIST and 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, see using-computed-hints.
Subtopics
- Autohide
- Tell ACL2 to automatically hide some terms.
- Instantiate-thm-for-matching-terms
- A computed hint which produces :use hints of the given theorem, based
on occurences of a pattern in the current goal clause.
- Using-computed-hints
- How to use computed hints