gen_find_term

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

Finds first value in range of partial function mapped over sub-terms of a term.

If a call to gen_find_term f t returns SOME v, then that result is the first value returned by a call of function f to one of the sub-terms of term t. 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 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_term f t will fail if f fails when applied to any of the sub-terms of t.

Example

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

> gen_find_term
    (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 =
  SOME ([{redex = ``x``, residue = ``z``}], [])] :
   ((term, term) Term.subst * (hol_type, hol_type) Term.subst) option

Comments

This function is used to implement bvk_find_term. This function could itself be approximated by returning the last value in the list returned by gen_find_terms. Such an implementation would be less efficient because it would unnecessarily construct a list of all possible results. It would also be semantically different if f had side effects.

See also

HolKernel.bvk_find_term, HolKernel.find_term, HolKernel.gen_find_terms