----------------------------------------------------------------------
bvk_find_term                                              (HolKernel)
----------------------------------------------------------------------
bvk_find_term : (term list * term -> bool) -> (term -> 'a) -> term -> 'a option

SYNOPSIS
Finds a sub-term satisfying predicate argument; applies a continuation.

KEYWORDS
Term.

DESCRIBE
A call to {bvk_find_term P k tm} searches {tm} for a sub-term
satisfying {P} and calls the continuation {k} on the first that it
finds.  If {k} succeeds on this sub-term, the result is wrapped in
{SOME} and returned to the caller.  If {k} raises a {HOL_ERR}
exception on the sub-term, control returns to {bvk_find_term}, which
continues to look for a sub-term satisfying {P}.  Other exceptions are
returned to the caller. If there is no sub-term that both satisfies
{P} and on which {k} operates successfully, the result is {NONE}.

The search order is top-down, left-to-right (i.e., rators of combs are
examined before rands).

As with {find_term}, {P} should be total.  In addition, {P} is given
not just the sub-term of interest, but also the stack of bound
variables that have scope over the sub-term, with the innermost bound
variables appearing earlier in the list.

FAILURE
Fails if the predicate argument fails (i.e., raises an exception;
returning false is acceptable) on a sub-term, or if the contination
argument raises a non-{HOL_ERR} exception on a sub-term on which the
predicate has returned true.

EXAMPLE
The {RED_CONV} function from {reduceLib} reduces a ground arithmetic
term over the natural numbers, failing if the term is not of the right
shape.

   - val find = bvk_find_term (equal ``:num`` o type_of o #2)
                              reduceLib.RED_CONV;
   > val find = fn : term -> thm option

   - find ``SUC n``;
   > val it = NONE : thm option

   - find ``2 * 3 + SUC n``;
   > val it = SOME |- 2 * 3 = 6 : thm option

   - find ``SUC n + 2 * 3``;
   > val it = SOME |- 2 * 3 = 6 : thm option

   - find ``2 + 1 + SUC n + 2 * 3``;
   > val it = SOME |- 2 + 1 = 3 : thm option


SEEALSO
HolKernel.find_term, HolKernel.find_terms.

----------------------------------------------------------------------