1\DOC DEPTH_CONV 2 3\TYPE {DEPTH_CONV : conv -> conv} 4 5\SYNOPSIS 6Applies a conversion repeatedly to all the sub-terms of a term, in bottom-up 7order. 8 9\KEYWORDS 10conversional. 11 12\DESCRIBE 13{DEPTH_CONV c tm} repeatedly applies the conversion {c} to all the subterms of 14the term {tm}, including the term {tm} itself. The supplied conversion is 15applied repeatedly (zero or more times, as is done by {REPEATC}) to each 16subterm until it fails. The conversion is applied to subterms in bottom-up 17order. 18 19\FAILURE 20{DEPTH_CONV c tm} never fails but can diverge if the conversion {c} can be 21applied repeatedly to some subterm of {tm} without failing. 22 23\EXAMPLE 24The following example shows how {DEPTH_CONV} applies a conversion to all 25subterms to which it applies: 26{ 27 - DEPTH_CONV BETA_CONV (Term `(\x. (\y. y + x) 1) 2`); 28 > val it = |- (\x. (\y. y + x)1)2 = 1 + 2 : thm 29} 30Here, there are two beta-redexes in the input term, one of which 31occurs within the other. {DEPTH_CONV BETA_CONV} applies beta-conversion to 32innermost beta-redex {(\y. y + x) 1} first. The outermost beta-redex is then 33{(\x. 1 + x) 2}, and beta-conversion of this redex gives {1 + 2}. 34 35Because {DEPTH_CONV} applies a conversion bottom-up, the final result may still 36contain subterms to which the supplied conversion applies. For example, in: 37{ 38 - DEPTH_CONV BETA_CONV (Term `(\f x. (f x) + 1) (\y.y) 2`); 39 > val it = |- (\f x. (f x) + 1)(\y. y)2 = ((\y. y)2) + 1 : thm 40} 41the right-hand side of the result still contains a beta-redex, 42because the redex {(\y.y)2} is introduced by virtue of an application of 43{BETA_CONV} higher-up in the structure of the input term. By contrast, 44in the example: 45{ 46 - DEPTH_CONV BETA_CONV (Term `(\f x. (f x)) (\y.y) 2`); 47 > val it = |- (\f x. f x)(\y. y)2 = 2 : thm 48} 49all beta-redexes are eliminated, because {DEPTH_CONV} repeats the 50supplied conversion (in this case, {BETA_CONV}) at each subterm (in this case, 51at the top-level term). 52 53\USES 54If the conversion {c} implements the evaluation of a function in logic, then 55{DEPTH_CONV c} will do bottom-up evaluation of nested applications of it. 56For example, the conversion {ADD_CONV} implements addition of natural number 57constants within the logic. Thus, the effect of: 58{ 59 - DEPTH_CONV reduceLib.ADD_CONV (Term `(1 + 2) + (3 + 4 + 5)`); 60 > val it = |- (1 + 2) + (3 + (4 + 5)) = 15 : thm 61} 62is to compute the sum represented by the input term. 63 64\COMMENTS 65The implementation of this function uses failure to avoid rebuilding 66unchanged subterms. That is to say, during execution the exception 67{QConv.UNCHANGED} may be generated and later trapped. The behaviour of 68the function is dependent on this use of failure. So, if the 69conversion given as an argument happens to generate the same 70exception, the operation of {DEPTH_CONV} will be unpredictable. 71 72\SEEALSO 73Conv.ONCE_DEPTH_CONV, Conv.REDEPTH_CONV, Conv.TOP_DEPTH_CONV. 74\ENDDOC 75