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