1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC TOP_DEPTH_CONV
\TYPE {TOP_DEPTH_CONV : (conv -> conv)}
\SYNOPSIS
Applies a conversion top-down to all subterms, retraversing changed ones.
\KEYWORDS
conversional.
\DESCRIBE
{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 failure string
{`QCONV`} may be generated and later trapped. The behaviour of the function
is dependent on this use of failure. So, if the conversion given as argument
happens to generate a failure with string {`QCONV`}, the operation of
{TOP_DEPTH_CONV} will be unpredictable.
\SEEALSO
DEPTH_CONV, ONCE_DEPTH_CONV, REDEPTH_CONV, REW_DEPTH_CONV.
\ENDDOC
|
