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
35
36
37
38
39
|
\DOC TOP_SWEEP_CONV
\TYPE {TOP_SWEEP_CONV : conv -> conv}
\SYNOPSIS
Repeatedly applies a conversion top-down at all levels, but after descending to
subterms, does not return to higher ones.
\DESCRIBE
The call {TOP_SWEEP_CONV conv} applies {conv} repeatedly at the top level of a
term, and then descends into subterms of the result, recursively doing the same
thing. However, once the subterms are dealt with, it does not, unlike
{TOP_DEPTH_CONV conv}, return to re-examine them.
\FAILURE
Never fails.
\EXAMPLE
If we create an equation between large tuples:
{
# let tm =
let pairup x i t = mk_pair(mk_var(x^string_of_int i,aty),t) in
let mkpairs x = itlist (pairup x) (1--200) (mk_var(x,aty)) in
mk_eq(mkpairs "x",mkpairs "y");;
...
}
\noindent we can observe that
{
# time (TOP_DEPTH_CONV(REWR_CONV PAIR_EQ)); ();;
}
\noindent is a little bit slower than
{
# time (TOP_SWEEP_CONV(REWR_CONV PAIR_EQ)); ();;
}
\SEEALSO
DEPTH_CONV, ONCE_DEPTH_CONV, REDEPTH_CONV, TOP_DEPTH_CONV.
\ENDDOC
|
