----------------------------------------------------------------------
ONCE_DEPTH_CONV                                                 (Conv)
----------------------------------------------------------------------
ONCE_DEPTH_CONV : (conv -> conv)

SYNOPSIS
Applies a conversion once to the first suitable sub-term(s) encountered in
top-down order.

KEYWORDS
conversional.

DESCRIBE
{ONCE_DEPTH_CONV c tm} applies the conversion {c} once to the first subterm or
subterms encountered in a top-down ‘parallel’ search of the term {tm} for which
{c} succeeds.  If the conversion {c} fails on all subterms of {tm}, the theorem
returned is {|- tm = tm}.

FAILURE
Never fails.

EXAMPLE
The following example shows how {ONCE_DEPTH_CONV} applies a conversion to only
the first suitable subterm(s) found in a top-down search:

   - ONCE_DEPTH_CONV BETA_CONV (Term `(\x. (\y. y + x) 1) 2`);
   > val it = |- (\x. (\y. y + x)1)2 = (\y. y + 2) 1 : thm

Here, there are two beta-redexes in the input term. One of these
occurs within the other, so {BETA_CONV} is applied only to the outermost one.

Note that the supplied conversion is applied by {ONCE_DEPTH_CONV} to all
independent subterms at which it succeeds.  That is, the conversion is applied
to every suitable subterm not contained in some other subterm for which the
conversions also succeeds, as illustrated by the following example:

   - ONCE_DEPTH_CONV numLib.num_CONV (Term `(\x. (\y. y + x) 1) 2`);
   > val it = |- (\x. (\y. y + x)1)2 = (\x. (\y. y + x)(SUC 0))(SUC 1) : thm

Here {num_CONV} is applied to both {1} and {2}, since neither term
occurs within a larger subterm for which the conversion {num_CONV} succeeds.

USES
{ONCE_DEPTH_CONV} is frequently used when there is only one subterm to which
the desired conversion applies. This can be much faster than using other
functions that attempt to apply a conversion to all subterms of a term (e.g.
{DEPTH_CONV}).  If, for example, the current goal in a goal-directed proof
contains only one beta-redex, and one wishes to apply {BETA_CONV} to it, then
the tactic

   CONV_TAC (ONCE_DEPTH_CONV BETA_CONV)

may, depending on where the beta-redex occurs, be much faster than

   CONV_TAC (TOP_DEPTH_CONV BETA_CONV)


{ONCE_DEPTH_CONV c} may also be used when the supplied conversion {c} never
fails, in which case using a conversion such as {DEPTH_CONV c}, which
applies {c} repeatedly would never terminate.

COMMENTS
The implementation of this function uses failure to avoid rebuilding
unchanged subterms. That is to say, during execution the exception
{QConv.UNCHANGED} may be generated and later trapped. The behaviour of
the function is dependent on this use of failure. So, if the
conversion given as an argument happens to generate the same
exception, the operation of {ONCE_DEPTH_CONV} will be unpredictable.

SEEALSO
Conv.DEPTH_CONV, Conv.REDEPTH_CONV, Conv.TOP_DEPTH_CONV.

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