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.

DESCRIPTION

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

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");;
  ...

we can observe that

  # time (TOP_DEPTH_CONV(REWR_CONV PAIR_EQ)); ();;

is a little bit slower than

  # time (TOP_SWEEP_CONV(REWR_CONV PAIR_EQ)); ();;