This section presents a simplified implementation of conversions and conversionals to convey the general ideas. Later sections describe the actual conversions that are implemented. Note however that the conversionals introduced here have the same names and same behaviours as those in the actual system.
Let
convn be an ML
concrete type alias for the type of
conversions.
In this section, assume that
convn is an
alias for the type
term -> term, where
term is a type of
terms that we want to rewrite.
Later on, I describe the type that
convn is
actually an alias for.
If c is of type
convn, then we
can use c to rewrite t of type
term by simply running the
ML
evaluator on the application 
.
For the purposes of the section only, let me introduce a basic conversion
called
RuleC : term -> convn. The conversion
RuleC
expects its term argument to be of form a = b where the free
variables of b are a subset of those in a.
If the conversion
RuleC 'a = b'
is applied to a term t,
RuleC tries to find a
substitution 
such
that 
. If it succeeds, it returns the term 
.
If a substitution cannot be found,
RuleC raises an exception
.
The conversion
RuleC 'a = b' therefore rewrites instances of a to
corresponding instances of b. For example:
RuleC 'x + 0 = x'
when applied to the term 
yields the term 
.
RuleC cannot by itself rewrite subterms of a term; if
RuleC 'x + 0 = x'
is applied to the term 
, it fails. There
are a variety of higher-order conversions that map a conversion such
as
RuleC over all subterms of a term. An example of a
conversional is
SweepUpC : convn -> convn . If c is a
conversion, then
SweepUpC c is also a conversion. if
SweepUpC c is applied to some term t, an attempt is made to apply c once to each subterm of t working from the leaves of term t up to its root. SweepUpC c only fails every every application of c fails. So if
is applied to term 
, it succeeds and returns the term
.
The basic conversion for sequencing conversions is
ANDTHENC : convn -> convn
-> convn. In , we reserve all-capital names for infix
functions so a normal application of
ANDTHENC to conversions
and 
has form
ANDTHENC 
. When applied to a
term t,
ANDTHENC 
first applies 
to t. If
succeeds, returning a term 
, then 
is applied to 
and the result is returned. If either 
or 
fails, then
ANDTHENC 
also fails. By analogy with tacticals being
higher-order tactics,
ANDTHENC is called a conversional.
The
ORELSEC : convn -> convn -> convn conversional is
for combining alternative conversions. When
ORELSEC 
is
applied to a term t, it first tries applying 
to t, and
if this succeeds returns the result. If the application of 
fails,
then it tries applying 
to t, failing if 
fails.
The definition for SweepUpC is:
SubC : convn -> convn when applied to a conversion c
and a term t, applies c to each of the immediate subterms of t.
It fails only when c fails on every immediate subterm
. Hence, it
always fails when t is a leaf node and has no immediate subterms.
ORTHENC 
is similar to
ANDTHENC 
in
that it first tries 
and then 
. However
ORTHENC only
fails if both 
and 
fail. So, a call of
SweepUpC c on
argument t first tries to apply
SweepUpC c to the immediate
subterms of t and then then tries to apply c to t itself.
Note that without the
t argument on the left and right sides
of the definition,
SweepUpC in ML's call-by-value evaluation scheme
would recurse indefinitely.
The definition for ORTHENC is:
let c1 ORTHENC c2 = (c1 ANDTHENC TryC c2) ORELSEC c2 where TryC c is defined as c ORELSE IdC and IdC: convn, when applied to any t, always returns t.
Other conversionals that are commonly used in the work described in this thesis are:
tries c on
each node in t in pre-order order, but only on the ith success
of c does it go through with the rewrite that c suggests. This is very
useful during interactive proof when for example you want to unfold one
instance of a definition but not any others.