COMPUTED-HINTS

Major Section:  MISCELLANEOUS

General Form of :hints:
(hint1 hint2 ... hintk)

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.

A computed hint is either a function symbol, fn, of three, four or seven arguments or is any term whose only free variables are among ID, CLAUSE, WORLD, STABLE-UNDER-SIMPLIFICATIONP, HIST, PSPV, and CTX. The function symbol case is treated as an abbreviation 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.) In the discussion below we assume all computed hints are of the term form.

The evaluation of the term (in a context in which its variables are bound as described below) should be either nil, indicating that the hint is not applicable to the clause in question, or else the value is an alternating list of :keyi vali ``pairs.'' Except possibly for the first keyword, the :keyi vali pairs should be as specified in hints. That is, those elements of the result should be hint settings as you might have typed in a common hint. The first keyword 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.

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 to generate 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 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 hint is left in 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 chr are 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 behavior.

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.

After a computed hint is applied to a goal and before the goal is processed, the remaining applicable computed hints are applied. For hint settings, such as :USE, that modify the goal, the effect of multiple applicable hints just compounds. But for hint settings, such as :IN-THEORY that determine the context of the subsequent goal processing, only the last applicable hint is effective.

It remains only to describe the bindings of the four 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 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.

For some instruction about how to use computed hints, see using-computed-hints.