MetaPRL Editor Module

The editor is for navigation and proof editing. The "MetaPRL Editor" section of the MetaPRL User Guide explains how to use the editor. The editor include three parts:

Proofs

Proofs have two representations in the editor. The Io_proof_type, and Io_proof modules define the proof structure that is saved in files. The Proof_step, Proof, and Proof_edit modules define the interactive proofs. Proofs are a recursive structure. A proof step is a single refinement step. It either primitive: containing a goal, a tactic, and a list of subgoals, or it is another proof. A proof is a tree of proof steps.

One objective of the proof structure is that work should never be discarded. When a proof is replayed, and a tactic is re-applied to the goal of a proof step, the subgoals may change because the tactic library changed as part of an upgrade. When subgoals change, the proof structure attempts to rebuild the proof tree by reordering subgoals. Goals that cannot be matched are saved as extras in a proof step. These extras can be navigated and, if necessary, modified to reconstruct the proof tree.

Modules

The module operations are defined in the Package_info module. This module contains operations to find and load a theory module, and save a module when it is modified. The Package_df module defines the display code for printing a module.

Toploop

The toploop is defined in several modules. The Shell module defines the commands that are available from the toploop, and the Shell_p4 and Shell_nl modules add the term syntax to the toploop. Each object in a module, including rewrites, inference rules, and display forms, has a module the defines the toploop operations on the object. The operations are defined in the signature Shell_type, and implementations are contains in Shell_rewrite and Shell_rule.