MetaPRL Module Editor

Introduction

The module editor is used to navigate the module hierarchy, and to fulfill interactive proof obligations. The modules are presented as a module hierarchy, and the editor includes commands to change the "current" module, and to switch between multiple proofs that are being edited. Proofs are saved as complete tactic-trees, allowing proofs to be later navigated and modified if necessary.

Getting started

The editor provides a top-loop that is compiled with the modules to the edited. The standard editor, in the directory editor/ml is compiled by default with the theories in theories/base and theories/itt. Additional theories can be included by adding them to the THEORIES variable in the mk/config. There are three standard editors:

The MetaPRL toploop is a simplified version of the OCaml toploop. It supports an interactive subset of ML programs intended specifically for editing and proof refinement. The MetaPRL toploop is integrated with the editor, so that module changes automatically open the ML namespace. However, general ML programming is not possible in the MetaPRL toploop. In contrast, the OCaml toploop used by mp.run contains an interpretor for the full OCaml language, but it is not connected with the editor, and explicit open directives must be used to access tactics and conversions. In addition, the OCaml toploop runs only in bytecode mode; for native-code, the MetaPRL toploop must be used.

The editor requires the installation of the Nuprl font. This character set includes symbols for the common logical operators, defined in the Nuprl_font module. The editor/fonts directory contains fonts for X11 and Windows, as well as an Emacs program to use all 256 characters in the set. It is recommended that you run the editor in an Emacs shell window, using the Nuprl font.

The editor directory includes shell scripts to invoke the editor. The mp script invokes the mp.run editor, the mptop and mpopt scripts invoke the corresponding editor. These scripts establish some common environment settings for the MetaPRL search path and Ensemble settings if Ensemble is being used.

For the OCaml toploop, you will need to open several modules before you can get started. The common modules are defined in the file x.ml, your first action would be to evaluate this file:

% editor/ml/mp
MetaPRL version 0.1
# #use "x.ml"

Module navigation

All editor commands are declared in the interface editor/ml/mp.mli. The editor maintains a state value representing the "current module." There are several commands to navigate the module hierarchy:

val pwd : unit -> string
val save : unit -> unit
val cd : string -> unit
val ls : string -> unit

The pwd command prints the current module. The cd command changes the current module loading the module if necessary. Module names are separated by the '/' character as in the Unix filesystem. Modified modules are saved with the save. The ls "flags" command prints the contents of the current module or proof. When flags string is empty, ls lists everything; when flags string contains r, then only rewrites would be listed; when flags string contains R, then only rules would be listed; and when flags string contains u, then only unproven objects would be listed.

The root of the hierarchy "/" is the module containing all loaded modules. Here is a script fragment showing the initial state of MetaPRL:

% ./mpopt

MetaPRL 0.6.0:
                build [Mon Oct 11 16:19:29 EDT 1999]
                on tulare.cs.cornell.edu
                Uses SIMPLE Refiner_ds
# pwd ();;
- : string = "/"
# ls "";;
--+--modules--+--
Module listing dir: modules; path: /
--
base_cache
base_dform
...
#

Each of the lines after the -- line is the name of a currently loaded module. We can navigate into a sub-module by changing the current directory.
































The module listing contains an entry for each of the items in the module, including the extends directives, open directives, ML values, and logical constructs for the axiom and rewrite directives. Each logical item is listed with its status:

Proof editing

Proof editing is performed by changing the current directory to be the proof to be edited. The ls command then produces a listing of the logical object.













The proof window contains the name of the proof, its assumptions (which are just the type definitions in this case), and the goal of the proof. The functions to navigate and modify the proof are the following:

val up : unit -> unit
val down : int -> unit
val root : unit -> unit

The up command moves up the proof tree, the down command navigates to a subgoal, and the root command returns to the root of the proof tree. The keyword refine is used to modify the proof. The following example show the first step of the proof:


























Creating new objects

New objects are created in a module with the following create_ commands (note that these functions are mostly disabled in the current distribution - you have to edit .ml files instead).

(*
 * All functions for creating objects in a package.
 *)
val create_rw : string -> unit
val create_axiom : string -> unit
val create_thm : string -> unit
val create_tptp : string -> unit
val create_opname : string -> unit
val create_condition : string -> unit
val create_parent : string -> unit
val create_dform : string -> unit
val create_prec : string -> unit
val create_prec_rel : string -> string -> string -> unit
val create_resource : string -> unit
val create_infix : string -> unit
val create_ml : string -> unit

Created objects are empty. They have no useful logical content. The logic definition is changed with the following functions:

val set_goal : term -> unit
val set_redex : term -> unit
val set_contractum : term -> unit
val set_assumptions : term list -> unit
val set_params : term Filter_summary.param list -> unit

The set_goal function set the goal for an axiom or inference rule. The set_assumptions function sets the assumptions for the rule. The set_redex and set_contractum functions are used just for rewrite rules.

Proof checking

There are two functions for checking proofs. A proof checks only if all the logical rules it uses are valid rules of its logic, and if all proof obligations for interactive proofs have been met. The valid logical rules include rules defined previously in the same module as the checked rule, and all the rules in extends'd modules.

val check : unit -> unit
val expand : unit -> unit

The check function checks a module object for validity; it does not modify the object. The expand function reapplies the existing proof to the object. This may cause the proof object to change if the tactic library has changed since the time the proof was constructed.