HolKernel.gen_find

STRUCTURE

SYNOPSIS

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

DESCRIPTION

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

bvk_find_term, find_term, gen_find_term