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
The compiler is implemented in the filter directory. There are five main parts to the "filter."