TOP_DEPTH_CONV : (conv -> conv)
STRUCTURE
SYNOPSIS
Applies a conversion top-down to all subterms, retraversing changed ones.
DESCRIPTION
TOP_DEPTH_CONV c tm repeatedly applies the conversion c to all the subterms of the term tm, including the term tm itself. The supplied conversion c is applied to the subterms of tm in top-down order and is applied repeatedly (zero or more times, as is done by REPEATC) at each subterm until it fails. If a subterm t is changed (up to alpha-equivalence) by virtue of the application of c to its own subterms, then the term into which t is transformed is retraversed by applying TOP_DEPTH_CONV c to it.
FAILURE
TOP_DEPTH_CONV c tm never fails but can diverge.
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 TOP_DEPTH_CONV will be unpredictable.
SEEALSO
HOL  Trindemossen-1