The MetaPRL refiner uses the term rewriter to implement four kinds of formal objects:

- Computational rewrites,
- Conditional rewrites,
- Axioms: true statements in a logic,
- Inference rules: relations between the provable statements.

Computational rewrites represent equivalences between terms that hold in any context. For example, in our currently implemented logics, beta-equivalence holds in every context:

rewritebeta : apply{lambda{x. 'b['x]}; 'a} <--> 'b['a].

This rewrite may not hold in logics that formalize computational complexity, or in logics that allow effects or require an explicit evaluation order.

Conditional rewrites are defined specifically for sequent calculi. An example of a conditional rewrite is a rewrite for division:

rewriteone : ('x <> 0) --> ('x / 'x) --> 1

The application of this rewrite requires a proof that the term being divided is not zero.

Axioms are a degenerate form of inference rules that represent true statements of a logic. An axiom is usually just a term that represents a valid proposition. For instance:

ruletrue_ax : trueruleidentity_ax : int -> int

The second axiom states that the *proposition* `int
-> int` is true. This would be a valid axioms in the propositions-as-types
interpretation: it would be *proved* by any function over
the integers.

Inference rules are used to specify "conditional" axioms. Most logical statements have the form of a rule. An example in a sequent calculus is the rule for implication introduction:

ruleimp_intro 'H 'x : sequent { 'H; x: 'A >- 'B } --> sequent { 'H >- 'A => 'B }

This is the standard rule: the proposition `'A` implies
the proposition `'B` if `'B` can be proved by assuming
`'A`. The arguments `'H` and `'x` represent
*parameters* of the rewrite. Given a *goal* term matching
`sequent { 'H >- 'A => 'B }`, the application of
the `imp_intro` rule produces a *subgoal* of the form `sequent
{ 'H; x: 'A >- 'B }`. The parameters `'H` and `'x`
are necessary arguments to enable the application: `'H`
represents the list of hypotheses of the sequent, and the `'x`
parameter provides the new variable name used in the subgoal.

Refiners are constructed recursively as objects of type `refiner`.
The `null_refiner` value is the empty refiner containing
no rewrites, and no rules. The following types are related to
the refiner:

typerewritetypetactictypesentinaltypeextract

The `rewrite` type is used to represent both simple
and conditional rewrites. The `tactic` type is used to
represent axioms and inference rules. The `extract` type
is used to provide accounting information for applications of rules.
The `sentinal` type is a condensed representation of the
refiner that includes the collection of all valid rewrites and
rules in the refiner.

The objects in the refiner are constructed through four functions, one for each object type. These functions have the following types:

valcreate_rewrite : refiner ->rewrite args-> rewritevalcreate_cond_rewrite : refiner ->cond rewrite args-> rewritevalcreate_axiom : refiner ->axiom args-> tacticvalcreate_rule : refiner ->rule args-> tactic

Several operations are defined on rewrites:

valrwaddr : rewrite -> address -> rewritevalandthenrw : rewrite -> rewrite -> rewritevalorelserw : rewrite -> rewrite -> rewritevalrwhigher : rewrite -> rewritevalrwtactic : rewrite -> tactic

The `rwaddr` function applies the rewrite to a subterm
of the goal. The `andthenrw` provides sequencing: when
the rewrite `(andthenrw rw1 rw2)`is applied, the rewrite
`rw1` is first applied, and it is immediately followed
by applying the rewrite `rw2`. The `orelserw`
is similar for handling failures. When the rewrite `(orelserw
rw1 rw2)` is applied, the rewrite `rw1` is applied
to the goal. If `rw1` succeeds, the rewrite completes without
applying `rw2`. Otherwise, if `rw1` fails (by raising
a `RefineError` exception), the rewrite is restarted by applying `rw2`.
When the `(rwhigher rw)` rewrite is applied, the rewrite `rw` is
allied to all the outermost subterms of the goal where `rw` may be
applied successfully (without raising a `RefineError` exception).
Finally he `rwtactic` function converts a rewrite to a tactic, so that the
tactic mechanism can be used to apply the rewrite.

Tactics are applied with the `refine` function, with
this simplified type:

valrefine : sentinal -> tactic -> term -> term list * extract

The `refine` function takes a `sentinal` that
is used to check that the tactic performs a valid logical inference;
it takes a `tactic` that describes the logical operation
to be performed, and it produces a list of subgoals that results
from the application of the rewrites and inference rules defined
by the tactic. A successful refinement also returns an `extract`
that summarizes the logical operation. In constructive logics,
the `extract` may be used to compute the computational
content of a proof. The `extract` is also used to construct
proof trees with the function `compose`:

valcompose : extract -> extract list -> extract

If `extract1` is the extract of a refinement, and `extracts2`
is a list of extracts for refinements of each of the subgoals,
then `(compose extract1 extracts2)` is a valid extract
for the composed proof. As defined, extracts *always* represent
valid proofs. However, for untrusted distributed refinement, or
for proof-carrying code, a checker is implemented as the function:

valterm_of_extract : extract -> term

The `term_of_extract` function checks that the extract
is valid, and it also produces the computational contents for
constructive proofs.

The final important operation of the refiner is the sentinal
computation. A sentinal is essentially a summary of all the formal
objects in a refiner. The sentinal is used during refinement to
check for valid applications of rules and rewrites. The function
`sentinal_of_refiner` computes the summary for a refiner.

valsentinal_of_refiner : refiner -> sentinal