		Search-engine friendly clone of the ACL2 documentation.

Use-termhint

Function-termhint

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)

Rationale

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 foo is defined as follows:

(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 function-termhint can be invoked as follows:

(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 hintcontext-bind can make previous bindings also available to termhints.

Operation

Function-termhint analyzes the (unnormalized) body of the given function and transforms it into a termhint term by replacing each hintcontext annotation with the corresponding hint from the user-provided case list. This transformation is done by the function term-replace-hintcontexts, which we describe below. It uses an operator hintcontext-join which produces the first non-NIL hint out of its arguments. In the following description, we call this joining two potential hints. The function term-replace-hintcontexts behaves as follows:

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).

Subtopics

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