The refiner is the logic engine for MetaPRL. The logical objects are the following:
The refiner implementation has three main parts:
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 module TermHash : TermHashSig module TermNorm : TermNormSig module TermHeaderConstr (FromTerm : TermModuleSig) : TermHeaderContrSig 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 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.