MetaPRL Term Modules and Types

MetaPRL terms have an interface (type term') and an abstract (type term) representations. The term' type is defined in refiner/refsig/term_simple_sig.mlz and is fixed while the term type may be different in different modules.

The Term_std module (actually, it is not a single module, but a collection of several modules, files in refiner/term_std/) can be considered a reference implementation. In Term_std, term is just equal to term'.

In the Term_ds module ("ds" stands for delayed substitutions", files in refiner/term_ds/) term type is different from term' - term has a field for set of free variables (which is computed lazily) and a field core that carries either term' or a delayed substitution or a sequent or a variable (in Term_std variables and sequents are encoded with term's, but it turned out to be more efficient to handle them specially).

There are also some parts of the term module that do not have to know what the term is as they work through the term' interface type - these files are located in refiner/term_gen. For most (if not all) of these files it was possible to write a more efficient implementation for Term_ds, so Term_ds may have its own version of these files.

The parts of the term module are collected together and packed with refiner and rewriter in refiner/refiner/refiner_*.ml files. Few parts of the system specify which of the term modules they want. The REFINER variable in the mk/config file decides which term module would be used in the rest of the system.

For more information see: