4. On-Line Help

Most of the help and documentation facilities described in this chapter require that you have a workstation running Emacs under X windows. In particular, you need a TEX previewer and one of the Emacs X-menu facilities. On-line help falls into three categories:

• Retrieval of specific entries in the manual, such as documentation of an interactive proof command.
• Retrieval of def-forms. These are the forms which, when evaluated, define the various IMPS objects.
• Presentation and selection of options via pull-down or pop-up menus. This is especially important if you are new to IMPS, because most of your interaction with IMPS can be initiated using the menus.

4.1 The Manual

The manual can be viewed on a TEX preview window by selecting the Manual option in the Help menu or by entering the Emacs command M-x imps-manual-entry. You will be prompted for a specific entry in the manual. The entry can be in one the following categories:

• A command name.
• A def-form name.
• A glossary entry.

As usual, the Emacs input completion facility is available, so that you only need to type in the first few letters of the entry. When you complete your selection, the previewer window (which might be iconified) will display the IMPS manual on the page which contains the entry. However, other pages of the IMPS manual are accessible by using the previewer's page motion commands. This allows you to easily examine related entries in the manual.

4.2 Def-forms

All IMPS objects are built using a specification form called a def-form. The following are some examples of def-forms:

   (def-constant CONVERGENT%TO%INFINITY
     "lambda(s:[zz,rr],
        forall(m:rr,
          forsome(x:zz, 
            forall(j:zz, x<=j implies m<=s(j)))))"
     (theory h-o-real-arithmetic))

   (def-theory PARTIAL-ORDER
     (language language-for-partial-order)
     (component-theories h-o-real-arithmetic)
     (axioms
      (prec-transitivity
       "forall(a,b,c:uu, 
          a prec b and b prec c
           implies
          a prec c)")
      (prec-reflexivity
       "forall(a:uu, a prec a)")
      (prec-anti-symmetry
       "forall(a,b:uu, 
          a prec b and b prec a 
           implies
          a = b)")))

Def-forms have a tag which is the second s-expression of the form (that is, the name immediately following the string def-). Thus the tags of the two s-expressions above are convergent%to%infinity and partial-order. The tag of the def-form is usually the name of the object being defined or modified.

There are two good reasons you may want to locate def-forms:

• You may need to know how an object is defined. For example, in the case of a theory, you may want to know what the primitive constants of the theory are.
• You may want to define a new object modeled on an existing one.

Def-forms can be viewed in an Emacs buffer by selecting the Find def-form option in the Help menu or by typing C-c . in an IMPS buffer. IMPS will then request a name. As usual, the Emacs input completion facility is available, so that you only need to type in the first few letters of the entry. When you complete your selection, IMPS will then search in the theory library for those forms which define the selected entry. Note that there may be more than one entry. There are several reasons for this:

• There may be several theories which have an identically named object.
• An object may be defined in one def-form and modified in another def-form. The definition finder will attempt to locate all such occurrences.
• A name may refer to different kinds of objects. The name fuba might refer to a translation, a theorem, and a constant.

Note also that the located form may have a different tag than the name selected. For example, the definition of the theory partial-order contains the axiom prec-transitivity.

4.3 Using Menus

Almost all user interaction with IMPS can be initiated using menus. The method of menu invocation as well as the menu format depends on the version of Emacs you are using:

• Free Software Foundation version 19 and Lucid version 19menus are invoked by clicking on the menubar. The menus are of the more familiar pull-down variety available on most home computers. The resulting menu has a label plus a number of options. In the case of Lucid Emacs, some of the options open up to new submenus.
• Version 18 menus are invoked by clicking the right mouse button on the mode line. Moreover, the menu consists of one or more panes which are stacked like cards; each individual pane has a label plus a number of options.

The options available to the user are determined by the buffer of the selected window. The following is a partial list of the options associated to the two IMPS-related buffer modes:

• Scheme Mode. This is the mode used for files of def-forms. The following are some of the options that can be selected from the menus in this mode:
  • Start a deduction graph.
  • Set the current theory.
  • Insert a def-form template.
  • Insert a proof script.
  • Run a proof script (by line or by region).
• Sequent Mode. This is the mode used for examining sequent nodes in Emacs buffers. The following are some options that can be selected from the menus in this mode:
  • List applicable commands in a menu. Each entry in this menu can in turn be selected buy clicking right with the mouse. This will apply the corresponding command to the sequent node displayed in the buffer.
  • List applicable macetes in a menu. Each entry in this menu can in turn be selected with the mouse. This will apply the corresponding macete to the sequent node displayed in the buffer.
  • List applicable macetes with a brief description in an Emacs buffer. Each macete can be selected by moving the cursor to the corresponding menu entry and typing m.

Note that the applicable commands and macetes are determined dynamically based on the form of the current sequent.