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. Nuturally, 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 predecedence and parenthesization.
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.
include Nuprl_font
prec prec_and
prec prec_or
prec prec_or < prec_and
dform true_df : true = `"True"
dform false_df : 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 the following display for the term "and"{true; ."or"{false; true}}:
This module uses the display definitions in the Nuprl_font module, 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 parenteses 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 : wedge = `"\203"
Display form options are used to provide precedence information. There are three options:
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 ot its context to its subterm.
The slot performs the precedence computation for parenthesizing subterms. The general slot stntax includes an optional parameter:
slot[option]{subterm}
The option is a string parameter, with two possible values: slot["le":s]{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":s]{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:
The `"s" form displays the string s. It is equivalent to slot[s:s].
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[inline:s,take:s] and hbreak[inline:s,take: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 ommitted; they default to the empty string "". For convenience, the hspace term is defined in the Nuprl_font module as hbreak[" ":s,"":s].
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.
As an example, we give the display form for the if-then-else term defined in the module Itt_bool.
dform ifthenelse_df : 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 magin, 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 Nuprl_font 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 ispushed again for the body of the else. Once the else-body is displayed, both soft zone are timinated, 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:
