The *refiner* is the logic engine for MetaPRL. The
logical objects are the following:

*Syntax definitions*extend the logical term language,*Rewrite rules*define computational equivalences,*Inference rules*define logical axioms and derived rules,*Programs*define computation, including arbitrary programs, tactic definitions, search algorithms, and the MetaPRL implementation itself.

The refiner implementation has three main parts:

- The definition of the
*term*language, used to express all logical statements. - The
*rewriter*defines rewriting operations on terms, used both for computation and rule application. - The
*refiner*implements accounting, rule application, and proof checking.

The refiner implementation is in the `refiner` directory.
The structure of the refiner implementation is given by the signature
for the refiner module, containing the following modules:

module typeRefinerSig =sigmoduleTermType : TermSigmoduleTerm : TermBaseSigmoduleTermOp : TermOpSigmoduleTermAddr : TermAddrSigmoduleTermMan : TermManSigmoduleTermSubst : TermSubstSigmoduleTermShape : TermShapeSigmoduleTermMeta : TermMetaSigmoduleTermEval : TermEvalSigmoduleRefineError : RefineErrorSigmoduleRewrite : RewriteSigmoduleRefine : RefineSigmoduleTermHash : TermHashSigmoduleTermNorm : TermNormSigmoduleTermHeaderConstr (FromTerm : TermModuleSig) : TermHeaderContrSigend

The refiner implementation is contained in the `refiner`
directory, with the following tree structure.

refiner ----> refbase |--------> refsig |--------> term_std |--------> term_ds |--------> term_gen |--------> rewrite |--------> refine \--------> reflib

The `refbase` directory contains basic refiner types,
including the definition of the `Opname` module. The `refsig`
directory contains the signatures for each of the modules in the
refiner. No code is implemented here--the signatures contain just
type definitions.

There are two implementations of terms. The `term_std`
directory contains the naive implementation of terms, where the
abstract implementation `term` is the same as the visible
definition `term'`. The `term_std` implementation
is being phased out in favor of the `term_ds` module ("ds"
for "delayed substitution"). The `term_ds` module
is much more efficient for performing refinement operations because
the lazy computation of substitutions has nearly linear complexity
for large refinements, while the `term_std` module performs
a complete term copy on every substitution. Both term modules
have identical signatures, and they can be interchanged without
affecting the refinement functionality. The `term_gen`
directory contains term operations that treat the `term` type
abstractly and, as a result, may be shared between different
implementations of terms.

The `rewrite` directory contains the implementation
of the rewriter. The `refine` directory implements the
refiner. Two separate refiner modules are composed in the `refiner_std`
and `refiner_ds` modules.

The final directory contains general term operations for arbitrary
implementations of the refiner. Some modules include `term_table`:
a hash table with term keys, `dform`: the display mechanism
for pretty-printing terms; `resource`: the basic definitions
for defining inheritable module resources.