MetaPRL Display Forms

Introduction

MetaPRL provides built-in support for pretty-printing logical expressions, as well as ML programs. The display form mechanism provides automatic introduction of parentheses based on precedences of display forms, it provides control over indentation and line breaking, and it provides a special character set for display of logical operators.

A display form is defined with the dform directive. The syntax of a display form has the following form:

dform name : [options] term = definition

Display form precedences are declared with two additional forms:

prec name
prec name < name

The term part of a display form is a term expressed in the uniform syntax; the term must be defined with the declare directive. The definition is another term that is the display form expansion. Term display is a process of evaluation: a term is displayed by selecting the closest-matching display form, replacing it with its expansion, and recursively displaying the result. Naturally, there is a condition for termination, and the definition uses a syntax that includes terms representing strings, line breaking information, and other control terms, as well as recursive display. The options provide information about precedence, parenthesization and display modes.

Display is part of the logical context of a module, and different modules can define different display mechanisms. The following display forms illustrate some of the basic display form mechanism for terms in the Itt_logic module.

extends Nuprl_font
prec prec_and
prec prec_or
prec prec_or < prec_and

dform true_df : except_mode[src] :: true = `"True"
dform false_df : except_mode[src] :: false = `"False"
dform and_df : parens :: "prec"[prec_and] :: and{'t1; 't2} =
   slot{'t1} `" " wedge `" " slot{'t2}

dform or_df : parens :: "prec"[prec_or] :: or{'t1; 't2} =
   slot{'t1} `" " vee `" " slot{'t2}

These definitions produce (in the default "prl" mode) the following display for the term "and"{true; ."or"{false; true}}:


This module uses the display definitions in the Nuprl_font module (described in the "MetaPRL Font" section), used to define the display of wedge and vee. IT also establishes display precedences to control parenthesization, with the precedence of or being less than the precedence of and. The display form for and has two options: the parens option declares that parentheses should be used to enclose the display if the term context has a higher precedence, and the prec["prec_and"] specifies the precedence of the display form. The term and{'t1; 't2} gives the pattern for terms defined with this display.

The definition provides the expansion. Display is usually defined as a sequence of terms for each part of the display. The slot for is used to parenthesize recursive display, so that the slot{'t1} in the and_df display form places parentheses around the 't1 subterm if the precedence is less that prec_and. The string `" " is a literal string that is printed verbatim; in this case a space character.

The wedge term is another recursive display. The display form for wedge is defined in the Nuprl_font module; its definition is the literal string `"\203", which correspond to the "wedge" character in the Nuprl font.

dform wedge_df : mode[prl] :: wedge = `"\203"

Options

Display form options are used to provide precedence information. There are five options:

  1. parens
  2. prec[prec]
  3. inherit
  4. mode[mode]
  5. except_mode[mode]

The parens option specifies that the display may be parenthesized. No parentheses are ever added to the display form if this option is not included. The prec[prec] option specifies the precedence to be used in the precedence computation. The inherit option is an alternative to prec[prec]: it specifies that the precedence should be inherited from the context. The inheritoption is used for creating transparent display form, such as the slot term, which passes the precedence of its context to its subterm.

The mode and except_mode options describe the display modes that the display form would be added to. Currently the following four modes are used in the system, but users can specify other modes

  1. prl mode is used to display the term in a form sutable for presentation in a Unicode font.
  2. html mode is used to display the term in HTML format (you need special fonts to view the result).
  3. tex mode is used to display the term in LaTeX format
  4. src mode is used to produce the text that can be parsed back by the MetaPRL parser.

The mode option specifies that the display form should be added to a given mode. The except_option specifies that the display form should be added to all modes except for the given one. Both options may be repeated, but they can not be mixed. By default, the display form is added to all modes, but this is almost always undesirable since few display forms are intended for src mode.

When MetaPRL is started, the prl mode is active. set_dfmode command may be used to switch between modes. It affects the output of functions that return terms immediately. For theory/proof listing you have to cd to "/" in order this change to take effect.

The slot expression

The slot performs the precedence computation for parenthesizing subterms. The general slot syntax includes an optional parameter:

slot[option]{subterm}

The option is a string parameter, with two possible values: slot["le"]{t}, specifies that subterm t should be parenthesized if its precedence is less than or equal to the precedence of the enclosing term. The slot["lt"]{t} term specifies that the term t should be parenthesized only if its precedence is strictly less than the precedence of the current term. If the slot option is not given, the value defaults to "lt".

There is also a slot form for displaying parameters. If the slot body is empty, the parameter is displayed using a "standard" display:

Literals

The `"s" form displays the string s. It is equivalent to slot["s"].

Line breaking and zones

The display mechanism divides the output into zones that specify line breaking behavior. There are two types of line breaks:

There are three types of zones.

Zones are defined with the terms lzone, szone, hzone, and ezone. Zones can be nested; when a zone is terminated, the enclosing zone is resumed. The lzone term begins a linear zone, the szone a soft zone, the hzone are hard zone, and the ezone term terminates the most recently entered zone, and returns to the previous zone.

Line breaking is specified with the terms sbreak[take:s,inline:s] and hbreak[take:s,inline:s]. The inline string specifies a string to be displayed if the break is not taken, and the take string is printed before the end of the line if the line break is taken. The string arguments can be omitted; they default to the empty string "". For convenience, the space term is defined as sbreak["":s," ":s] and the hspace term is defined as hbreak["":s," ":s].

Indentation

Indentation is specified with the left-margin operators pushm[tab:n] and popm. These operations establish the location of the left margin. They can be nested; when the left margin is removed with the term popm, the left margin is replaced with its previous value. The pushm[tab:n] term pushes a new left margin at the current display position plus tab characters. The tab option can be omitted; it defaults to 0. The popm term removes the margin installed with the last pushm.

Example

As an example, we give the display form for the if-then-else term defined in the module Itt_bool.

dform ifthenelse_df : except_mode[src] :: parens :: "prec"[prec_or]
                   :: ifthenelse{'e1; 'e2; 'e3} =
   pushm[0] szone push_indent `"if" `" " slot{'e1} `" " `"then" hspace
   szone slot{'e2} ezone popm hspace
   push_indent `"else" hspace
   szone slot{'e3} ezone ezone popm popm

This is a fairly complicated display form. The options specify that the ifthenelse term may be parenthesized, and it has precedence prec_or. The display immediately pushes the current left margin, and enters a soft zone so that the ifthenelse is either displayed on a single line, or all display breaks are taken. The push_indent term pushes the left margin again to indent the body of the ifthenelse; it is defined in Ocaml_base_df module as the term pushm[3:n].

The condition is displayed on the first line, followed by a possible line break. The body of the conditional is displayed in an additional soft zone. After the body is displayed, the margin is popped so that a line break will return to the margin for the conditional. The else string is printed and the left margin is pushed again for the body of the else. Once the else-body is displayed, both soft zone are terminated, and both margins are popped, returning the display state to its original state.

The following two examples show how the conditional is displayed without line breaks, and with line breaks: