The word "conversion" is used to describe rewriting
rules. Like a "tactical," a "conversional"
is an operation on conversions. A conversion is created in a module
whenever a rewrite rule is defined. For example, the following
definition of *beta* reduction defines a conversion called
`beta`:

rewritebeta : (lambda{x. 'b['x]} 'a) <--> 'b['a].

The ML conversion has the following type:

valbeta : conv

A conversion is applied to the current goal by using the rw function:

topvalrw : conv -> int -> tactic

The `rw` function assumes the conversion is being applied
in a sequent calculus, and the number passed to the rw function
is the number of the sequent clause to be rewritten. There is
an additional function `rwh` to perform rewriting on the
"higher" occurrences of subterms.

topvalrwh : conv -> int -> tactic

For example, beta conversion is performed in the following proof fragment:

Goal: sequent { 'H; x: (lambda{x. 'x} 1) < 0) >- false }BYrwh beta 2 Subgoal 1: sequent { 'H; x: 1 < 0 >- false }

There are several simple conversions:

topvalidC : convtopvalfailC : conv

The `idC` conversion is the identity: when `idC`
is applied to a term, the result of the rewriting is the argument,
unchanged. The `failC` conversion always fails.

There are several standard conversionals:

topvalprefix_thenC : conv -> conv -> convtopvalprefix_orelseC : conv -> conv -> convtopvaladdrC : int list -> conv -> convtopvalfoldC : term -> conv -> convtopvalmakeFoldC : term -> conv -> convtopvalcutC : term -> convvalfunC : (env -> conv) -> conv

The `thenC` conversional is for sequencing: the conversion
`(rw1 thenC rw2)` applies rewrite `rw1` and follows
it by applying `rw2` to the resulting term. The `orelseC`
is for conditional application: the conversion `(rw1 orelseC
rw2)` first tries applying the conversion `rw1`. If
the rewrite succeeds, `rw2` is not applied. Otherwise,
rw2 is applied to the initial argument.

The conversion `addrC` applies a rewrite to a subterm
of the goal. The `foldC` conversion is for reversing a
rewrite. For example, the following proof fragment reverses a
beta reduction:

Goal: sequent { 'H; x: 1 < 0 >- false }BYrwh (foldC << lambda{x. 'x} 1 >> beta) 2Subgoal: sequent { 'H; x: (lambda{x. 'x} 1) < 0 >- false }

The `makeFoldC` conversional performs the same operation
as `foldC`, but it performs a (relatively expensive) preprocessing
step. The `makeFoldC` conversional is typically used at
the top level of a module to define standard reversed rewriting.

The `cutC` conversion replaces the current goal with
a new goal, producing a rewriting subgoal. The following proof
fragment illustrates its use:

Goal: sequent { 'H >- ('x + 1) - 1 }BYrw (cutC << 'x >>) 0 Subgoal 1: sequent { 'H >- 'x } Subgoal 2: sequent { 'H >- 'x <--> ('x + 1) - 1 }

The `funC` conversional produces an *environment*
for a conversion. The current goal can be accessed with the following
functions:

valenv_term : env -> termvalenv_goal : env -> term

The `env_term` function returns the term that the rewriting
is to be performed on, and the `env_goal` returns the entire
goal (so, for instance, the results will be different if rewriting
is being performed on a subterm of the goal with `addrC`).

Typically, rewriting is performed by search. For example, it
is often useful to reduce *all* beta redices in the goal.
The following conversionals provide search strategies.

topvalsomeSubC : conv -> convtopvalallSubC : conv -> conv

These two conversions apply their arguments to the immediate *subterms*
of the current goal. The `(someSubC conv)` conversion applies
`conv` to subterms from left-to-right, succeeding when
the first rewrite succeeds. The `(allSubC conv)` applies
`conv` to all subgoals; all rewrites must succeed.

topvalhigherC : conv -> convtopvallowerC : conv -> conv

The `higherC` conversion searches for the *outermost*
terms where a rewrite is successful. It may defined by recursion:

lethigherC conv = conv orelseC (allSubC (higherC conv))

Since higherC conversional is used very often, MetaPRL provides a highly tuned efficient implementation of rewriting using higherC conversionals

The `lowerC` conversion searches for the *innermost*
terms:

letlowerC conv = (allSubC (lowerC conv)) orelseC conv

The `repeatC` conversion applies a conversion until
a fixpoint is reached:

topvalrepeatC : conv -> conv