Termhint-seq
Sequence hints within a use-termhint term.
Termhint-seq is both a standalone macro and a B* binder that allows
hints to be sequenced within a use-termhint term. For example:
(defun my-sequenced-hints (x)
(declare (xargs :normalize nil))
(termhint-seq
`'(:use ((:instance foo (a ,(hq x)))))
(if (bar x)
`'(:use ((:instance foo-when-bar (q ,(hq x)))))
`'(:expand ((bar ,(hq x)))))))
Here, the hint form (use-termhint (my-sequenced-hints x)) will (when
stable under simplification) first issue a hint using an instance of foo,
then cause a case split on (bar x) and when stable under simplification
again, use an instance of foo-when-bar in the case where (bar x) is
assumed true and expand (bar x) in the other case.
Note the :normalize nil declaration: this is useful for functions that
use termhint-seq, because it makes use of hide to keep the second set
of hints from causing case splits before the first set of hints is in play;
normalization tends to disrupt this.
A b* binder form of termhint-seq also exists; the following function is
equivalent to the one above:
(defun my-sequenced-hints (x)
(declare (xargs :normalize nil))
(b* (((termhint-seq `'(:use ((:instance foo (a ,(hq x)))))))
((when (bar x))
`'(:use ((:instance foo-when-bar (q ,(hq x)))))))
`'(:expand ((bar ,(hq x))))))
The argument to the termhint-seq binder is the first hint and the rest
of the b* form after that binder is the second hint.
