TOP_SWEEP_CONV : conv -> conv
Repeatedly applies a conversion top-down at all levels, but after descending to
subterms, does not return to higher ones.
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 CONDITIONS
If we create an equation between large tuples:
we can observe that
# 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");;
is a little bit slower than
# time (TOP_DEPTH_CONV(REWR_CONV PAIR_EQ)); ();;
# time (TOP_SWEEP_CONV(REWR_CONV PAIR_EQ)); ();;
- SEE ALSO
DEPTH_CONV, ONCE_DEPTH_CONV, REDEPTH_CONV, TOP_DEPTH_CONV.