MetaPRL Compiler

MetaPRL is implemented as an extension of the OCaml compiler. The syntax of OCaml is extended by using CamlP4 to add a syntax for terms and a syntax for logical objects in modules. MetaPRL files have the same .ml and .mli suffixes as normal OCaml files. The MetaPRL compiler is called prlc. The usage is as follows:

% prlc [OCaml options] file.ml
% prlc [OCaml options] file.mli

The MetaPRL compiler produces additional files that summarize the logical content of the files that were compiled. For each interface file.mli, an file file.cmiz file is created that summarizes the logical content of the interface. The file.cmi file is still created, containing ML definitions used by the compiler for interface checking.

For each implementation file file.ml, a file file.cmoz is created that summarizes the logical content of the module (the file.cmo file is still created for the ML content). The logical files with the .cmiz and .cmoz suffixes are used during compilation for determining compile-time logical consistency. They are also used by the proof editor to navigate the logical theories. They represent a complete summary of the source: they can be compiled directly with the prlc compiler.

    % prlc [OCaml options] file.cmiz
    % prlc [OCaml options] file.cmoz

Implementation

The compiler is implemented in the filter directory. There are five main parts to the "filter."

1. The filter_parse module defines the extended logical syntax.
2. The filter_summary module defines the components of compiled files that are saved in the .cmiz and .cmoz files.
3. The filter_cache module defines the logical data structures used to maintain the logical consistency of compiled modules.
4. The filter_prog module defines the output routines that translate logical objects to their ML representations.
5. The filter_ocaml module defines the translation between ML programs and logical terms.