## 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:

- a representation of
*proofs*,
- a representation of
*modules*,
- a
*toploop.*

### 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`.