Give termhints according to the structure of a function with hintcontext annotations.

Usage (as a computed hint):

(function-termhint function-name case1 case2 ...)

where each case is of one of the following two forms, and each ctxname is the name given by some hintcontext annotation in the named function:

;; provides termhint at the ctxname hintcontext (ctxname termhint) ;; provides termhint at the ctxname1 and ctxname2 hintcontexts ((ctxname1 ctxname2 ...) termhint)

Sometimes when using use-termhint an otherwise sensible hint might
require replicating much of the body of a function. This utility offers an
alternative. First, place hintcontext annotations in the body of the
function in contexts where it makes sense to give a hint. Then use function-termhint, which transforms the body of the function to place
user-provided termhint fragments in those contexts. For example, if

(defun foo (x) (if (test1 x) (let ((y (foo-y x))) (if (test2 y) (hintcontext :test2-true (foo-ans1 y x)) (hintcontext :test2-false (foo-ans2 y x)))) (hintcontext :test1-false (foo-ans3 x))))

then

(defthm foo-prop (prop (foo x)) :hints ((function-termhint foo (:test2-true `(:expand ((foo-ans ,(hq y) ,(hq x))))) ((:test1-false :test2-false) '(:use ((:instance my-lemma (z x))))))))

This is equivalent to:

(defthm foo-prop (prop (foo x)) :hints ((use-termhint (if (test1 x) (let ((y (foo-y x))) (if (test2 y) `(:expand ((foo-ans ,(hq y) ,(hq x)))) ;; :test2-true '(:use ((:instance my-lemma (z x)))))) ;; :test2-false '(:use ((:instance my-lemma (z x)))))))) ;; :test1-false

But note that in the latter form, we replicate the IF and LET structure of the original function, whereas in the former, we only make reference to the hintcontext labels and bound variables of that function.

An additional utility, hintcontext-bind, can be used to add variable
bindings that don't actually exist in the function but may be used by the
hints. This is convenient for reasoning about stobjs: each binding of a stobj
in an executable function must shadow all of its previous bindings, but

Function-termhint analyzes the (unnormalized) body of the given function and
transforms it into a termhint term by replacing each

- If term is a variable or quote, return NIL.
- If term is a hintcontext annotation, find the corresponding hint from the case list and join this with the result of recurring on the body (third argument).
- If term is a hintcontext-bind annotation, create a b* term whose bindings are the (unquoted) second argument and whose body is the result of recurring on the third argument.
- If term is any other kind of RETURN-LAST call, return the result of
recurring on the last argument. (Note: this means we only process the
:logic part of MBE forms.) - If term is an IF, recur on the then and else branches; if either returns a
non-nil result, return
(if original-test then-result else-result , otherwise NIL. - If term is a function call, join the results of recurring on all the function arguments.
- If term is a lambda call, join the results of recurring on all the
arguments as well as, if the recursive call on the lambda body returns a
non-NIL result, the term
((lambda formals body-result) . original-args) .

- Hintcontext-bind
- Bind variables for use in function-termhint.
- Hintcontext
- Name a context within a function definition for later use in function-termhint.