MetaPRL Refiner

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:

1. The definition of the term language, used to express all logical statements.
2. The rewriter defines rewriting operations on terms, used both for computation and rule application.
3. 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 type RefinerSig =
sig
   module TermType : TermSig
   module Term : TermBaseSig
   module TermOp : TermOpSig
   module TermAddr : TermAddrSig
   module TermMan : TermManSig
   module TermSubst : TermSubstSig
   module TermShape : TermShapeSig
   module TermMeta : TermMetaSig
   module TermEval : TermEvalSig
   module RefineError : RefineErrorSig
   module Rewrite : RewriteSig
   module Refine : RefineSig
end

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 are shared between the two implementations of terms.

The rewrite directory contains the implementation of the rewriter. The refine directory implements the refiner. The 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.