computing advice to the theorem proving process

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

A common hint is of the form

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 function symbol, fn, 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-triples. 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.


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.



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.




As for CTX and STATE, they are provided so that you can pass them to the er macro to print error messages. We recommend not writing computed hints that otherwise change STATE!

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.
