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

SYNOPSIS
Maps a partial function over sub-terms of a term.

KEYWORDS
sub-term, search

DESCRIBE
A call to {gen_find_terms f t} returns a list of values derived from
sub-terms of term {t}. The values are those generated by the function
{f} when it returns {SOME v}. The function {f} is successively passed
sub-terms of {t} starting with {t} itself and then proceeding in a
top-down, left-to-right traversal. The list of results returned in the
reverse of this order (but the fact that the traversal is done in the
described order is observable if {f} has side effects).

The additional list of terms passed to the function {f} is the list of bound variables “governing” the sub-term in question, with the innermost bound variable first in the list.

FAILURE
A call to {gen_find_terms f t} will fail if {f} fails when applied to any of the sub-terms of {t}.

EXAMPLE

> gen_find_terms (fn x => SOME x) ``SUC x``;
val it =
   [([], ``x``), ([], ``SUC``), ([], ``SUC x``)]:
   (term list * term) list

> gen_find_terms
    (fn (bvs,t) => if null bvs andalso
                      (is_var t orelse numSyntax.is_numeral t)
                   then
                     Lib.total (match_term ``x:num``) t
                   else NONE)
    ``SUC z + (\y. y) 5``;
val it =
   [([{redex = ``x``, residue = ``5``}], []),
    ([{redex = ``x``, residue = ``z``}], [])]:
   ((term, term) Term.subst * (hol_type, hol_type) Term.subst) list


SEEALSO
HolKernel.bvk_find_term, HolKernel.find_term, HolKernel.gen_find_term.

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