File: language.tex

package info (click to toggle)
hol88 2.02.19940316-8
links: PTS
area: main
in suites: lenny
size: 63,120 kB
ctags: 19,367
sloc: ml: 199,939; ansic: 9,300; sh: 7,118; makefile: 6,074; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (1433 lines) | stat: -rw-r--r-- 49,940 bytes
parent folder | download | duplicates (11)

\chapter{The pretty-printing language\label{language}}

A description of the syntax and informal semantics of the pretty-printing
language follows. The language is described top-down, and the description is
intended to provide detailed information about language constructs. The
information is intended for reference or for use when the examples do not
provide sufficient information.

A pretty-printer specification consists of the name of the pretty-printer
and a list of {\it rules}. The rules may optionally be preceded by
{\it declarations\/} and/or {\it abbreviations}.

\begin{small}\begin{verbatim}
<pp>                ::=  "prettyprinter" <identifier> "="
                            <body>
                         "end" "prettyprinter"
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<body>              ::=  <rules>
                      |  <declarations>  <rules>
                      |  <abbreviations> <rules>
                      |  <declarations>  <abbreviations> <rules>
\end{verbatim}\end{small}


\section{Naming a pretty-printer\label{naming}}

The name given to a pretty-printer is used to obtain the names of the \ML\
values generated by the compiler. In fact the compiler generates \ML\ code for
declarations of these values.

If the pretty-printer is called {\small\verb%xxxx%}, then the \ML\ file
generated by the compiler will declare \ml{xxxx\_rules} as a list of rules for
the pretty-printing program. The program normally uses a function derived from
the rules, and such a function is declared within the \ML\ file. Its name is
\ml{xxxx\_rules\_fun}.


\section{Declarations\label{declarations}}

The declarations are a list of bindings of an identifier (which is restricted
to the identifiers allowed in the pretty-printing language) to a piece of \ML\
code.

\begin{small}\begin{verbatim}
<declarations>      ::=  "declarations" <binding_list>
                            "end" "declarations"
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<binding_list>      ::=  <binding> ";"
                      |  <binding> ";" <binding_list>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<binding>           ::=  <identifier> "=" <ML_function>
\end{verbatim}\end{small}

\noindent
The \ML\ code must be function valued. The identifiers become \ML\ identifiers,
bound to the value of the \ML\ code. They become available for use within
blocks of \ML\ code later in the pretty-printer specification. They are also
available within the other declarations, that is the declarations are mutually
recursive.


\subsection{Blocks of ML code within the pretty-printer
            language\label{mlfunction}}

Text enclosed within braces in the pretty-printer language is interpreted as
a block of \ML\ code.

Absolutely no checks are performed on blocks of \ML\ code when the
pretty-printer code is compiled. The text between the braces is copied into
the generated \ML\ file. Only when the \ML\ file is loaded will any errors
within the code become apparent, and as one might expect, errors which
normally appear at run-time will not be spotted when the generated file is
loaded. \ML\ identifiers used within the code block need not be in scope when
the pretty-printer file is compiled, but they must be when the generated file
is loaded.

If braces are to appear in the block of \ML\ code they must be doubled-up,
i.e.~{\small\verb%{%} must be replaced by {\small\verb%{{%} and
{\small\verb%}%} must be replaced by {\small\verb%}}%}.

If the block of \ML\ code extends over more than one line, then the leading
brace must not be followed by anything other than white space on the same
line, for example,

\begin{small}\begin{verbatim}
   {\x. x}
\end{verbatim}\end{small}

\noindent
and

\begin{small}\begin{verbatim}
   {
    \x. x}
\end{verbatim}\end{small}

\noindent
are valid, but

\begin{small}\begin{verbatim}
   {\x.
     x}
\end{verbatim}\end{small}

\noindent
is not.

This restriction allows the \ML\ code to be inserted neatly into the \ML\ file
generated by the compiler.


\section{Abbreviations\label{abbreviations}}

Syntactically, abbreviations are identical to declarations (see
Section~\ref{declarations}). However, the \ML\ code block is not used to
determine the value of the identifier. Instead, the \ML\ code is textually
substituted for the identifier wherever the identifier is used in the
pretty-printing rules. So, the identifier is being used as an abbreviation for
the \ML\ code block.

\begin{small}\begin{verbatim}
<abbreviations>     ::=  "abbreviations" <binding_list>
                            "end" "abbreviations"
\end{verbatim}\end{small}


\section{Rules\label{rules}}

The pretty-printing rules are ordered. An earlier rule has priority over a
later rule. So, if rule $Y$ is a special case of rule $X$, $Y$ will only ever
be used if it appears before $X$ in the list of rules. This is because $X$
will match any tree that $Y$ would match. For every tree or sub-tree it has to
print, the pretty-printer begins searching from the beginning of the list for
a rule which matches.

\begin{small}\begin{verbatim}
<rules>             ::=  "rules" <rule_list> "end" "rules"
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<rule_list>         ::=  <rule> ";"  |  <rule> ";" <rule_list>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<rule>              ::=  <pattern> "->" <format>
                      |  <pattern> "->"
                            "<<" <p_special_list> ">>" <format>
\end{verbatim}\end{small}

\noindent
A rule normally consists of two parts. The {\it pattern\/} is used to match
the tree to be printed, and to bind sub-trees and node-names to variables. The
{\it format\/} specifies what to display. It can make use of the sub-trees and
node-names bound to the variables. There is an optional third part to a rule
which performs transformations on the variables between matching and passing
the variables to the format.


\subsection{Patterns\label{patterns}}

A pattern consists of a {\it context\/} in which the rule is supposed to apply
and a tree structure to be compared with the tree to be printed. There is also
an optional test which can be used to reject the rule under conditions which
cannot be expressed by the tree structure.

\begin{small}\begin{verbatim}
<pattern>           ::=  <string> "::" <pattern_tree>
                      |  <string> "::" <pattern_tree> "where" <test>
\end{verbatim}\end{small}


\subsubsection{Context\label{context}}

A context is represented by a string {\small\verb%'...'%}. If the string is
empty, i.e.~{\small\verb%''%}, the rule can apply in any context. If the
string has any other form, the rule can only apply in a context corresponding
to that string. The initial context is set when the pretty-printing function
is called.


\subsubsection{Tests in patterns\label{tests}}

A test can be used to reject a rule even when the context matches and the tree
matches.

\begin{small}\begin{verbatim}
<test>              ::=  <ML_function>  |  <identifier>
\end{verbatim}\end{small}

\noindent
A test is either a block of \ML\ code (see Section~\ref{mlfunction}) or
an identifier which must have been defined as an abbreviation for a block of
\ML\ code (see Section~\ref{abbreviations}). In either case the block of \ML\
code must evaluate to a function of type:

\begin{small}\begin{verbatim}
   (string # int) list -> print_binding -> bool
\end{verbatim}\end{small}

\noindent
The first argument to such a function is a list of parameters, represented by
pairs. The first element of a pair is the name of the parameter. The second
element is the parameter value. The second argument is the binding of
metavariables to sub-trees and node-names resulting from matching the tree.
The result is a Boolean value indicating whether the test is successful or
whether it fails.

So, the test is an \ML\ function which can examine the values of the
pretty-printing parameters (e.g.~precedence) and the bindings of metavariables.
The context is also available for testing. It appears in the parameter list as
a pair of the form:

\begin{small}\begin{verbatim}
   (`CONTEXT_xxxx`,n)
\end{verbatim}\end{small}

\noindent
where {\small\verb%xxxx%} is the current context, and {\small\verb%n%} is any
number (it does not matter which).


\subsubsection{Metavariables\label{metavars}}

Before considering patterns for tree structures, it is worth considering
metavariables.

\begin{small}\begin{verbatim}
<name_metavar>      ::=  "***"  |  "***" <identifier>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<child_metavar>     ::=  "*"    |  "*"   <identifier>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<children_metavar>  ::=  "**"   |  "**"  <identifier>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<metavar_list>      ::=  <name_metavar>
                      |  <child_metavar>
                      |  <children_metavar>
                      |  <name_metavar>     ";" <metavar_list>
                      |  <child_metavar>    ";" <metavar_list>
                      |  <children_metavar> ";" <metavar_list>
\end{verbatim}\end{small}

\noindent
There are three kinds of metavariable. Metavariables of the form
{\small\verb%***...%} match any node-name and if the {\small\verb%***%} is
followed by an identifier, the node-name is bound to a metavariable named as
the identifier. Metavariables of the form {\small\verb%*...%} match any
sub-tree. {\small\verb%**...%} matches a list of sub-trees. The list can be
empty.

Consider the following tree:

\begin{small}\begin{verbatim}
                                     cond
                                     / | \
                                 true one zero
\end{verbatim}\end{small}

\noindent
The pattern {\small\verb%*x%} will match this tree and bind the whole tree to
the metavariable {\small\verb%*x%}. The pattern {\small\verb%***x(*,*,*)%}
also matches the tree and binds {\small\verb%***x%} to the name
{\small\verb%cond%}. The same is true for {\small\verb%***x(**)%},
{\small\verb%***x(*,**)%}, {\small\verb%***x(*,**,*)%}, because
{\small\verb%**%} matches zero or more sub-trees ({\it children}). The pattern
{\small\verb%cond(**)%} also matches, but no binding occurs.

{\small\verb%cond(*x,*y,*z)%} matches the tree and binds {\small\verb%*x%},
{\small\verb%*y%}, {\small\verb%*z%} to {\small\verb%true()%},
{\small\verb%one()%}, {\small\verb%zero()%} respectively.
{\small\verb%true()%} means a tree with root node labelled with
{\small\verb%true%} and no children. {\small\verb%cond(*x,*y)%} does not match
as this pattern is for a node with precisely two children.

The pattern {\small\verb%cond(true(),**x)%} matches the tree and binds the
metavariable {\small\verb%**x%} to a list of two elements. The first element
is the tree {\small\verb%one()%}. The second element is the tree
{\small\verb%zero()%}.

If more than one {\small\verb%**...%} metavariable is used for matching the
children (for example {\small\verb%cond(**x,**y)%}), all but the first have to
match precisely one child.

The name of a metavariable (if present) should be thought of as separate from
the {\small\verb%***%}, {\small\verb%*%}, or {\small\verb%**%}. The latter
specify what kind of object is to be matched. The name binds the matched
object. The upshot of this is that {\small\verb%***x%} and {\small\verb%*x%}
(for example) are not distinct.


\subsubsection{Patterns for trees\label{patterntrees}}

In describing metavariables (see Section~\ref{metavars}) it was necessary to
describe simple patterns. The full syntax of patterns for trees is:

\begin{small}\begin{verbatim}
<pattern_tree>      ::=  <node_name> "(" ")"
                      |  <node_name> "(" <child_list> ")"
                      |  <child_metavar>
                      |  <label> <pattern_tree>
                      |  <loop_link>
                      |  <loop_link> <pattern_tree>
                      |  <loop>
                      |  <loop> <pattern_tree>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<loop>              ::=  "[" <pattern_tree> "]"
\end{verbatim}\end{small}

\noindent
Consider the tree:

\begin{small}\begin{verbatim}
                                     comb
                                     /  \
                                   comb  c
                                   /  \
                                comb  b
                                /  \
                               f    a
\end{verbatim}\end{small}

\noindent
This can be written as:

\begin{small}\begin{verbatim}
   comb(comb(comb(f(),a()),b()),c())
\end{verbatim}\end{small}

\noindent
The simplest pattern is something of the form {\small\verb%*x%}. This pattern
matches any tree. The pattern {\small\verb%comb(*,*)%} consists of a node-name
which is fixed and two sub-trees (children) which are variable. This pattern
matches the tree in the example.

The pattern {\small\verb%comb(***x(*,*y),*z)%} matches the tree and binds
{\small\verb%***x%} to the name {\small\verb%comb%}, {\small\verb%*y%} to the
sub-tree {\small\verb%b()%}, and {\small\verb%*z%} to the sub-tree
{\small\verb%c()%}.

The syntax of these forms of pattern is given by the following (together with
syntax already given):

\begin{small}\begin{verbatim}
<node_name>         ::=  <identifier>  |  <name_metavar>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<child>             ::=  <children_metavar>
                      |  <pattern_tree>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<child_list>        ::=  <child>
                      |  <child> "," <child_list>
\end{verbatim}\end{small}

\noindent
The patterns given so far only allow a sub-tree to be bound to a metavariable
if the sub-tree has not been investigated by the pattern. To put it another
way, metavariables which match trees can only occur at the leaves of the
pattern tree. Binding a sub-tree to a metavariable and testing it with a
pattern can be achieved by labelling the node which will match the root node
of the sub-tree concerned.

\begin{small}\begin{verbatim}
<label>             ::=  "|" <child_metavar> "|"
\end{verbatim}\end{small}

\noindent
So, the pattern \verb!comb(comb(|*x|comb(*y,*),*),*)! matches the example and
binds {\small\verb%*y%} to the tree {\small\verb%f()%}. In addition,
{\small\verb%*x%} is bound to the tree {\small\verb%comb(f(),a())%}.

If a metavariable occurs more than once in a pattern, it must match to the
same object at every place it appears. If it does not, the pattern does not
match.


\subsubsection{Looping patterns}

The remainder of the syntax for patterns is concerned with {\it looping
patterns}. A simple looping pattern is {\small\verb%[comb(<>,*x)]*y%}. This
pattern matches the tree in the example. {\small\verb%*x%} becomes bound to a
list of sub-trees, namely {\small\verb%c()%}, {\small\verb%b()%},
{\small\verb%a()%}. {\small\verb%*y%} becomes bound to the sub-tree
{\small\verb%f()%}.

The part of the pattern in the square brackets is repeatedly used in matching
attempts, first on the original tree, then on the sub-tree that was bound to
the {\small\verb%<>%} on the previous match. When the part of the pattern in
the square brackets will no longer match, an attempt is made to match the
remaining part of the pattern to the remaining sub-tree. The {\small\verb%<>%}
in the pattern is referred to as the {\it loop-link}.

The second part of the pattern (i.e.~that outside the brackets) can be omitted.
The pattern {\small\verb%*%} is taken as the default.

The loop-link may be used as for labelling of nodes, that is it may be
followed by a pattern. For example, the pattern
{\small\verb%[comb(<>comb(*,*),*x)]*y%} matches the example and binds
{\small\verb%*x%} to the list {\small\verb%c()%}, {\small\verb%b()%}.
{\small\verb%*y%} is bound to {\small\verb%comb(f(),a())%}. On each match
attempt in the loop, the pattern used is {\small\verb%comb(comb(*,*),*x)%}. If
the match succeeds, the new sub-tree to be matched is that matched by the
second {\small\verb%comb%} of this pattern. The result is that the looping
stops before the last {\small\verb%comb%} node.

The looping part of a pattern need not match at all for the whole pattern to
match. Put another way, the pattern in square brackets matches zero or more
times. So, the pattern {\small\verb%[abs(<>,*x)]*y%} matches the example tree
binding {\small\verb%*x%} to an empty list, and {\small\verb%*y%} to the whole
tree. This illustrates a danger of looping patterns. If {\small\verb%*y%} is
used in the format, the recursive call to the printer will be identical to the
previous call. This results in the printer looping indefinitely with the tree
to be printed getting no smaller.

The loop can be forced to match at least once by writing the loop-link as
{\small\verb%<1..>%}. So, {\small\verb%[abs(<1..>,*x)]*y%} does not match the
example. Any positive integer can be specified, for example
{\small\verb%<3..>%} means match at least three times. In addition, an upper
limit can be specified. {\small\verb%<..4>%} means match 0,1,2,3 or 4 times.
{\small\verb%<3..4>%} means match either 3 or 4 times. When the number of
matches has reached the upper limit, an attempt is made to match the remaining
part of the pattern to the remaining sub-tree.

\begin{small}\begin{verbatim}
<min>               ::=  <number>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<max>               ::=  <number>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<loop_range>        ::=  <min> ".."
                      |  ".." <max>
                      |  <min> ".." <max>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<loop_link>         ::=  "<" ">"
                      |  "<" <metavar_list> ">"
                      |  "<" <loop_range> ">"
                      |  "<" <loop_range> ":" <metavar_list> ">"
\end{verbatim}\end{small}

\noindent
Metavariables within a looping pattern normally become bound to a list with one
element for each successful match. It is possible to override this behaviour
so that a metavariable has to match the same object on each loop. Instead of
being bound to a list, the metavariable becomes bound to the repeated object.
So, the pattern {\small\verb%[***name(<***name>,*x)]*y%} matches the example.
{\small\verb%*x%} is bound to a list as before, and {\small\verb%*y%} is bound
to {\small\verb%f()%}. {\small\verb%***name%} is bound to the node-name
{\small\verb%comb%} (note {\em not\/} a list of these\footnote{If a looping
pattern loops zero times, any fixed metavariable is bound to an empty list and
ceases to be treated as fixed.}). Observe that a metavariable is {\it fixed\/}
by naming it in the loop-link.

The control of the number of loops and the fixing can be used together in a
loop-link, e.g.~{\small\verb%<3..4: ***name; *x>%}.

A looping pattern must contain precisely one loop-link, and loop-links should
not appear outside of a looping pattern. These restrictions are not enforced
by the syntax of the language. Violations are dealt with at a later stage of
compilation.


\subsubsection{Sequences of looping patterns}

A loop can be followed by another loop. For example, the pattern:

\begin{small}\begin{verbatim}
   [comb(<..2>,*x)][comb(<>,*y)]*z
\end{verbatim}\end{small}

\noindent
matches the example. {\small\verb%*x%} is bound to the list {\small\verb%c()%},
{\small\verb%b()%}. {\small\verb%*y%} is bound to the list (of one element)
{\small\verb%a()%}, and {\small\verb%*z%} is bound to {\small\verb%f()%}.

The pattern:

\begin{small}\begin{verbatim}
   [comb(<..2>,*x)][comb(<>,*x)]*z
\end{verbatim}\end{small}

\noindent
also matches. {\small\verb%*x%} becomes bound to the list {\small\verb%c()%},
{\small\verb%b()%}, {\small\verb%a()%}, and {\small\verb%*z%} is bound to
{\small\verb%f()%}. This is a useful property of metavariable binding across
loops, although it is not really required for the example. As another example,
the pattern:

\begin{small}\begin{verbatim}
   [comb(<..2>,*x)][comb(<>,*y)]*x
\end{verbatim}\end{small}

\noindent
matches with {\small\verb%*x%} binding to the list {\small\verb%c()%},
{\small\verb%b()%}, {\small\verb%f()%}. {\small\verb%*y%} is bound to
{\small\verb%a()%}. The pattern:

\begin{small}\begin{verbatim}
   [comb(<..2>,*x)][comb(<>,*x)]*x
\end{verbatim}\end{small}

\noindent
matches with {\small\verb%*x%} binding to the list {\small\verb%c()%},
{\small\verb%b()%}, {\small\verb%a()%}, {\small\verb%f()%}.

This property does not apply to metavariables which have been fixed. If such
a metavariable appears in two or more loops, or in a loop and after a loop, it
binds to a single object. So, the metavariable must match to the same object
everywhere it appears in the pattern.


\subsubsection{Nested looping patterns}

Loops can be nested. The scope of a loop-link extends only to the first set of
enclosing square brackets. So, the loop-link for a loop must always come from
the non-looping part of the pattern within the loop. For example, the pattern:

\begin{small}\begin{verbatim}
   [[comb(<1..>,*x)][abs(<1..>,*y)]]
\end{verbatim}\end{small}

\noindent
is invalid because the outermost loop has no link. The links within the two
nested loops are not visible to the outer loop. A valid version is:

\begin{small}\begin{verbatim}
   [[comb(<1..>,*x)][abs(<1..>,*y)]<>]
\end{verbatim}\end{small}

\noindent
This pattern matches one or more {\small\verb%comb%} nodes, followed by one or
more {\small\verb%abs%} nodes, followed by one or more {\small\verb%comb%}
nodes, and so on. {\small\verb%*x%} becomes bound to a list of sub-trees for
the {\small\verb%comb%} nodes and {\small\verb%*y%} becomes bound to a list of
sub-trees for the {\small\verb%abs%} nodes. If the same metavariable were used
in both nested loops, it would become bound to a list of all the sub-trees.

Note that the use of {\small\verb%abs%} here would not be very useful for the
abstractions of \HOL\ terms. This is because the loop-link appears in the
bound-variable position, not in the body position. A more useful pattern might
be:

\begin{small}\begin{verbatim}
   [comb(<1..>,[abs(*bvars,<>)]*body)]*f
\end{verbatim}\end{small}

\noindent
This pattern matches one or more {\small\verb%comb%} nodes, where the
sub-trees can be abstractions. The pattern is of limited use because the
metavariable {\small\verb%*bvars%} becomes bound to a list containing all the
bound variables of the first abstraction, followed by all the bound variables
of the second abstraction and so on. For example matching the pattern against
the tree:

\begin{small}\begin{verbatim}
                                   comb
                                   /  \
                                 comb  abs
                                 /  \   | \
                               comb  b c1  abs
                               /  \         | \
                              f    abs     c2  c
                                    | \
                                   a1  a
\end{verbatim}\end{small}

\noindent
would result in {\small\verb%*bvars%} being bound to the list
{\small\verb%c1()%}, {\small\verb%c2()%}, {\small\verb%a1()%}.


\subsection{Metavariable transformations\label{pspecials}}

Section~\ref{patterns} describes how a pattern can be matched against a
parse-tree to produce a binding of metavariables to node-names and sub-trees.
This binding can be used in the format (see Section~\ref{formats}).
However, the form of the binding is not always suitable for performing the
operations required within the format. This section describes the facilities
available to manipulate the binding into a suitable form. This is achieved by
the use of \ML\ functions.

The transformations are expressed as a list of declarations. Each declaration
binds a metavariable to the result of evaluating an \ML\ function of a
specific type. The \ML\ function either appears directly as a block of \ML\
code enclosed within braces, or it can be an identifier. The identifier should
be the name of an abbreviation for a block of \ML\ code (see
Section~\ref{abbreviations}).

\begin{small}\begin{verbatim}
<transformation>    ::=  <ML_function>  |  <identifier>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<p_special>         ::=  <name_metavar>     "=" <transformation>
                      |  <child_metavar>    "=" <transformation>
                      |  <children_metavar> "=" <transformation>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<p_special_list>    ::=  <p_special>
                      |  <p_special> ";" <p_special_list>
\end{verbatim}\end{small}

\noindent
The block of \ML\ code (see Section~\ref{mlfunction}) must evaluate to a
function of type:

\begin{small}\begin{verbatim}
   (string # int) list -> print_binding -> metavar_binding
\end{verbatim}\end{small}

\noindent
The first argument to such a function is a list of parameters, represented by
pairs. The first element of a pair is the name of the parameter. The second
element is the parameter value. The second argument is the binding of
metavariables to sub-trees and node-names resulting from matching the tree.
The result is a value suitable for binding to a metavariable.

Chapter~\ref{functions} discusses how these \ML\ functions may be constructed.
A typical use might be to append two lists bound to different metavariables
into one list, and to bind it to a new metavariable. Another use might be to
reverse a list bound to a metavariable.

If a metavariable declared in the transformations has the same name as a
metavariable obtained from the pattern, the metavariable from the pattern is
discarded before passing the binding to the format. The original binding of
the metavariable is however available within the transformation functions.


\subsection{Formats\label{formats}}

A format specifies the form of the output from the printer. The layout of the
text can be specified and text from nodes of the parse-tree can be displayed
along with other text specified as constants within the format.

A format is either an empty {\it box}, which produces no output, or it can be
a box with layout information. A format can also be a conditional box which
consists of two formats, one of which is used depending on the result of
performing a test. The tests used are of the same form as those used in
patterns (see Section~\ref{tests}).

\begin{small}\begin{verbatim}
<format>            ::=  "[" "]"
                      |  "[" <box_spec> "]"
                      |  "if" <test> "then" <format> "else" <format>
\end{verbatim}\end{small}


\subsubsection{Boxes}

A box consists of a list of {\it objects\/} together with a specification of
how the objects should be composed, that is where they appear relative to each
other in the displayed text.

\begin{small}\begin{verbatim}
<box_spec>          ::=  "<" <h_box>   ">" <h_object_list>
                      |  "<" <v_box>   ">" <v_object_list>
                      |  "<" <hv_box>  ">" <hv_object_list>
                      |  "<" <hov_box> ">" <hov_object_list>
\end{verbatim}\end{small}

\noindent
There are four kinds of box: horizontal ({\small\verb%h%}), vertical
({\small\verb%v%}), horizontal/vertical ({\small\verb%hv%}) and
horizontal-or-vertical ({\small\verb%hov%}).

\begin{small}\begin{verbatim}
<h_box>             ::=  "h"   <h_params>
<v_box>             ::=  "v"   <v_params>
<hv_box>            ::=  "hv"  <hv_params>
<hov_box>           ::=  "hov" <hov_params>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<h_params>          ::=  <number>
<v_params>          ::=  <indent> "," <number>
<hv_params>         ::=  <number> "," <indent> "," <number>
<hov_params>        ::=  <number> "," <indent> "," <number>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<indent>            ::=  <integer>  |  "+" <integer>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<integer>           ::=  <number>  |  "-" <number>
\end{verbatim}\end{small}

\noindent
The objects of a horizontal box appear continuously in the output, that is,
no line breaks are inserted between the objects. If each object extends over
only one line, then the entire box will appear on one line, though it may
overflow the right margin. The printer cannot avoid this overflow, since it
has not been instructed how to break the text. For this reason horizontal
boxes should only be used where really necessary.

The objects in a vertical box each appear on a separate line of the output.

In a horizontal/vertical box the objects will appear continously unless there
is an overflow over the right margin. If this occurs, the overflowing objects
will be placed continously on the next line. If there is overflow again, a
third line is begun, and so on.

A horizontal-or-vertical box behaves like a horizontal box provided there is
no overflow over the right margin. If there is, it behaves like a vertical box.

Some examples: the format:

\begin{small}\begin{verbatim}
   [<h 1> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
is a horizontal box containing four objects, each of which is a constant
string. The {\small\verb%1%} in {\small\verb%<h 1>%} instructs the printer to
insert one blank space between each object. The output would appear as:

\begin{small}\begin{verbatim}
   This is a test
\end{verbatim}\end{small}

\noindent
The format:

\begin{small}\begin{verbatim}
   [<v 1,0> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This
    is
    a
    test
\end{verbatim}\end{small}

\noindent
Here the specification is of the form
{\small\verb%<v%}~{\it di,dh\/}{\small\verb%>%} where {\it di\/} is the
indentation of all later objects relative to the first, and {\it dh\/} is the
number of blank lines between objects. The indentation can be made relative to
the previous object by preceding the value with a {\small\verb%+%}.

\begin{small}\begin{verbatim}
   [<v +1,0> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This
    is
     a
      test
\end{verbatim}\end{small}

\noindent
As another example, the format:

\begin{small}\begin{verbatim}
   [<v +3,1> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This

      is

         a

            test
\end{verbatim}\end{small}

\noindent
The indentation value can be negative, but this may cause a printing error due
to an attempt to begin a piece of text to the left of the left margin.

The format:

\begin{small}\begin{verbatim}
   [<hv 2,+1,0> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This  is  a  test
\end{verbatim}\end{small}

\noindent
provided this fits on one line. If not, the following may be produced:

\begin{small}\begin{verbatim}
   This  is  a
    test
\end{verbatim}\end{small}

\noindent
or perhaps:

\begin{small}\begin{verbatim}
   This  is
    a  test
\end{verbatim}\end{small}

\noindent
or perhaps:

\begin{small}\begin{verbatim}
   This  is
    a
     test
\end{verbatim}\end{small}

\noindent
The format:

\begin{small}\begin{verbatim}
   [<hov 2,+1,0> "This" "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This  is  a  test
\end{verbatim}\end{small}

\noindent
provided this fits on one line. If not, the following will be produced:

\begin{small}\begin{verbatim}
   This
    is
     a
      test
\end{verbatim}\end{small}

\noindent
A {\small\verb%hv%} box corresponds to the
inconsistent\index{line breaks!inconsistent} breaking of the standard \HOL\
pretty-printer, whereas a {\small\verb%hov%} box corresponds to
consistent\index{line breaks!consistent} breaking.

Boxes may contain formats as objects. The next example illustrates this and
also demonstrates that the contents of a horizontal box may not all appear on
the same line of output, though no line breaks are inserted between the output
for each object.

\begin{small}\begin{verbatim}
   [<h 0> "(" [<hov 2,+1,0> "This" "is" "a" "test"] ")"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (This  is  a  test)
\end{verbatim}\end{small}

\noindent
provided this fits on one line. If not, the following will be produced:

\begin{small}\begin{verbatim}
   (This
     is
      a
       test)
\end{verbatim}\end{small}

Note that there is no line break between the left parenthesis and
{`}{\small\verb%This%}{'}, and there is no line break between
{`}{\small\verb%test%}{'} and the right parenthesis.


\subsubsection{Box parameters}

The examples given so far have not made use of the facility to override the
layout parameters. Each object can be preceded by a set of parameters which
determine its behaviour.

\begin{small}\begin{verbatim}
<h_object_list>     ::=  <h_object>    |  <h_object>   <h_object_list>
<v_object_list>     ::=  <v_object>    |  <v_object>   <v_object_list>
<hv_object_list>    ::=  <hv_object>   |  <hv_object>  <hv_object_list>
<hov_object_list>   ::=  <hov_object>  |  <hov_object> <hov_object_list>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<h_object>          ::=  <object>  |  "<" <h_params>   ">" <object>
<v_object>          ::=  <object>  |  "<" <v_params>   ">" <object>
<hv_object>         ::=  <object>  |  "<" <hv_params>  ">" <object>
<hov_object>        ::=  <object>  |  "<" <hov_params> ">" <object>
\end{verbatim}\end{small}

\noindent
The format:

\begin{small}\begin{verbatim}
   [<h 1> "This" <2> "is" "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This  is a test
\end{verbatim}\end{small}

\noindent
The format:

\begin{small}\begin{verbatim}
   [<v 0,0> "This" <3,0> "is" <3,0> "a" "test"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   This
      is
      a
   test
\end{verbatim}\end{small}

\noindent
A set of parameters can be placed before the first object, but this will not
normally have any effect. However, there are cases when the object appearing
in the format expands into more than one object in the output. In such a case
the first of these expanded objects is considered to be the first object in
the box, and the set of parameters applies to all the other expanded objects.


\subsubsection{Objects}

The examples have illustrated two kinds of object: constant strings and
formats. There are also {\it expansion boxes\/} which are similar to formats,
{\it leaves}, which are items of text obtained from metavariables bound to
node-names, and {\it subcalls}, which are recursive calls of the printer to
print sub-trees bound to metavariables. Leaves and subcalls have a similar
syntax.

\begin{small}\begin{verbatim}
<object>            ::=  <terminal>
                      |  <leaf_or_subcall>
                      |  <format>
                      |  <expand>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<leaf_or_subcall>   ::=  <context_subcall>
                      |  <context_subcall>
                            "with" <assignments> "end" "with"
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<assignments>       ::=  <assignment>
                      |  <assignment> ";" <assignments>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<assignment>        ::=  <identifier> ":=" <int_expression>
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<int_expression>    ::=  <integer>  |  <ML_function>  |  <identifier>
\end{verbatim}\end{small}


\subsubsection{Assignments}

Subcalls can contain {\it assignments\/} to parameters. The parameters can be
used to pass information (such as precedence of operators) between recursive
calls to the printer. Since a leaf is not a recursive call, assignments are of
no use. The syntax allows assignments in leaves, but an error occurs at a later
stage of the compilation.

The assignments change the values of the parameters which are passed to the
recursive call. Any parameter not included in the assignments retains its
previous value. An assignment consists of an identifier which is the name of
the parameter, and an integer value. The integer value can either be given as
a constant or it can be derived from an \ML\ function. The \ML\ function can
either be an explicit block of \ML\ code (see Section~\ref{mlfunction}) or an
identifier which is an abbreviation for a block of \ML\ code (see
Section~\ref{abbreviations}).

The block of \ML\ code must evaluate to a function of type:

\begin{small}\begin{verbatim}
   (string # int) list -> print_binding -> int
\end{verbatim}\end{small}

\noindent
The first argument to such a function is a list of parameters, represented by
pairs. The first element of a pair is the name of the parameter. The second
element is the parameter value. These parameters are the parameters the
assignments can be used to change, so the new value of a parameter can depend
on its old value.

The second argument to the function is the binding of metavariables to
sub-trees and node-names resulting from matching a tree. This information
allows parameters such as precedence to be modified appropriately.

The result of the function is the required integer value.
Section~\ref{functions} discusses how these \ML\ functions may be constructed.

The current context is also available for testing. It appears in the parameter
list as a pair of the form:

\begin{small}\begin{verbatim}
   (`CONTEXT_xxxx`,n)
\end{verbatim}\end{small}

\noindent
where {\small\verb%xxxx%} is the current context, and {\small\verb%n%} is any
number (it does not matter which). The context cannot be updated using an
assignment. Any assignment to a parameter of the form shown above will have no
effect.


\subsubsection{Changing context}

In addition to having assignments, subcalls (but not leaves) can be made in a
new context.

\begin{small}\begin{verbatim}
<context_subcall>   ::=  <fun_subcall>
                      |  <string> "::" <fun_subcall>
\end{verbatim}\end{small}

\noindent
The context is represented by a string of characters in single quotation-marks.
If no context is given, the new call is made in the same context as the current
call.


\subsubsection{Leaves and subcalls}

Leaves in formats are represented by a metavariable of the form
{\small\verb%***...%}, that is a metavariable which has been bound to a
node-name. The corresponding output is that node-name. Subcalls are
represented by metavariables of the form {\small\verb%*...%} and
{\small\verb%**...%}. The corresponding output is that obtained by calling the
printer recursively on the sub-tree or sub-trees bound to the metavariable. An
error occurs if any metavariable used as a leaf or subcall does not have a
name, or does not appear in the binding.

\begin{small}\begin{verbatim}
<fun_subcall>       ::=  <name_metavar>
                      |  <child_metavar>
                      |  <children_metavar>
                      |  <transformation> "(" <name_metavar> ")"
                      |  <transformation> "(" <child_metavar> ")"
                      |  <transformation> "(" <children_metavar> ")"
\end{verbatim}\end{small}

\begin{small}\begin{verbatim}
<transformation>    ::=  <ML_function>  |  <identifier>
\end{verbatim}\end{small}

\noindent
If {\small\verb%***name%} is bound to the string {\small\verb%test%}, then the
format:

\begin{small}\begin{verbatim}
   [<h 0> "(" ***name ")"]
\end{verbatim}\end{small}

\noindent
produces the following output:

\begin{small}\begin{verbatim}
   (test)
\end{verbatim}\end{small}

\noindent
If {\small\verb%*x%} is bound to a tree which when printed produces the text:

\begin{small}\begin{verbatim}
   This is
     a test
\end{verbatim}\end{small}

\noindent
then the format:

\begin{small}\begin{verbatim}
   [<h 0> "(" *x ")"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (This is
      a test)
\end{verbatim}\end{small}

\noindent
If {\small\verb%**x%} is bound to a list of four trees which when printed
produce the output {\small\verb%This%} (from first tree), {\small\verb%is%}
(from second tree), {\small\verb%a%}, {\small\verb%test%}, then the format:

\begin{small}\begin{verbatim}
   [<h 0> "(" **x ")"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (Thisisatest)
\end{verbatim}\end{small}

\noindent
The {\small\verb%**x%} behaves not as one object, but as four. The format:

\begin{small}\begin{verbatim}
   [<h 1> "(" **x ")"]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   ( This is a test )
\end{verbatim}\end{small}

\noindent
Note that a metavariable of the form {\small\verb%*...%} may also be bound to
a list due to it occurring within a loop in the pattern (see
Section~\ref{patterns}), and so may behave as more than one object. To put
this another way, the behaviour of a subcall depends on what the metavariable
is bound to, not on whether it begins with {\small\verb%*%} or
{\small\verb%**%}.


\subsubsection{Transformations}

A leaf or subcall can be more than just the metavariable. The binding of the
metavariable may undergo a transformation. A transformation is a block of \ML\
code either given explicitly or by an abbreviation (see
Sections~\ref{mlfunction} and \ref{abbreviations}).

In the case of leaves, the block of \ML\ code must evaluate to a function of
type:

\begin{small}\begin{verbatim}
   string -> string
\end{verbatim}\end{small}

\noindent
The function is given the node-name bound to the metavariable as argument, and
can return any string.

For subcalls, the \ML\ code must be of type:

\begin{small}\begin{verbatim}
   (print_tree # address) list -> (print_tree # address) list
\end{verbatim}\end{small}

\noindent
or have a type which can be instantiated to this type. \ml{print\_tree} is an
\ML\ datatype for the parse-trees which are to be pretty-printed.
\ml{address} is an \ML\ datatype for addresses of sub-trees within these
parse-trees. (See Section~\ref{leafandsubtrans} for a detailed explanation).
If the metavariable of the subcall is bound to a list of trees, it is this
list which is given to the function as argument. If the metavariable is bound
to a single tree, the tree is made into a one element list and this list is
given as argument. The transformation is intended to allow re-ordering of the
list, taking the tail of the list, or other similar operations, though it
would be possible to use it to change the trees themselves.

So, a complicated subcall might appear in a format as:

\begin{small}\begin{verbatim}
   [<h 0> "(" 'test'::rev(**x) with prec := 4 end with ")"]
\end{verbatim}\end{small}

\noindent
where {\small\verb%rev%} is defined as an abbreviation for a list reversing
function.


\subsubsection{Expansion-boxes}

The only feature of formats left to describe is expansion boxes.

\begin{small}\begin{verbatim}
<expand>            ::=  "**[" <box_spec> "]"
\end{verbatim}\end{small}

\noindent
When a metavariable which is bound to a list of trees appears in a format,
it behaves like {\it n\/} objects where {\it n\/} is the length of the list.

Suppose the metavariable {\small\verb%**x%} is bound to a list of four trees
which print as the numbers {\small\verb%1%}, {\small\verb%2%},
{\small\verb%3%}, {\small\verb%4%}. The format:

\begin{small}\begin{verbatim}
   [<h 1> **x ","]
\end{verbatim}\end{small}

\noindent
produces the output:

\begin{small}\begin{verbatim}
   1 2 3 4 ,
\end{verbatim}\end{small}

\noindent
A more likely requirement is the output:

\begin{small}\begin{verbatim}
   1, 2, 3, 4,
\end{verbatim}\end{small}

\noindent
and this can be achieved using a format containing an expansion box:

\begin{small}\begin{verbatim}
   [<h 1> **[<h 0> **x ","]]
\end{verbatim}\end{small}

\noindent
Here it is the expansion box ({\small\verb%**[...]%}), not the metavariable
which behaves as four objects. Within the expansion box, the metavariable
behaves as a single object. The format above can be thought of as expanding to:

\begin{small}\begin{verbatim}
   [<h 1> [<h 0> *x1 ","] [<h 0> *x2 ","]
             [<h 0> *x3 ","] [<h 0> *x4 ","]]
\end{verbatim}\end{small}

\noindent
where {\small\verb%*x1%} is bound to the first tree in the list to which
{\small\verb%**x%} is bound, and so on. For this reason, an expansion box
cannot be used at top-level, that is as the whole format, since it would have
no box in which to expand into.

The printer determines how many times the box should be expanded by
investigating the bindings of the metavariables used within it. The length of
the longest bound list is the value used. So, if {\small\verb%***y%} is bound
to the list {\small\verb%a%}, {\small\verb%b%}, {\small\verb%c%} of
node-names, then the format:

\begin{small}\begin{verbatim}
   [<h 1> **[<h 0> "(" **x "," ***y ")"]]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (1,a) (2,b) (3,c) (4,)
\end{verbatim}\end{small}

\noindent
So, when a list is too short, the difference is made up by empty boxes which
produce no output.

Some care is required when applying a list transformation function to a
metavariable within an expansion box. When determining how many times to
expand, the printer looks at the list bound to the metavariable, not the list
which is the result of applying the transformation. Furthermore, the
transformation is applied to the single element of the list obtained for
the specific instance of the expansion. So, the results may not be as expected.
This problem can be avoided by making the transformation between the pattern
and the format rather than within the format (see Section~\ref{pspecials}).


\subsubsection{Nested expansion-boxes}

Expansion boxes can be nested. Continuing the example, the format:

\begin{small}\begin{verbatim}
   [<v 0,0> **[<v 1,0> **[<h 0> "(" **x ","] **[<h 0> ***y ")"]]]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (1,
    a)
   (2,
    b)
   (3,
    c)
   (4,
    )
\end{verbatim}\end{small}

\noindent
The nested expansion boxes can be thought of as a format in which no expansion
takes place, but where the whole of that format is duplicated {\it n\/} times,
{\it n\/} being the length of the longest list bound to a metavariable
occurring withing the expansion boxes. So, the expansion takes place at the
least deeply nested level of expansion box.

Ordinary boxes nested within expansion boxes are treated for expansion purposes
just like a string constant. The contents of such a box are processed as if
it was an entire format, to produce a fixed piece of text. This text may then
be duplicated within each expanded box, but it is the same text which appears
in each expanded box. When determining how many expansions to make, the
printer does not `look inside' nested boxes which are not expansion boxes. So,
the metavariables used within such a nested box are not considered unless they
are `visible' in some other way. To see this consider the following two
examples.

The format:

\begin{small}\begin{verbatim}
   [<v 0,0> **[<v 1,0> **[<h 0> "(" **x ","] [<h 0> ***y ")"]]]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (1,
    abc)
   (2,
    abc)
   (3,
    abc)
   (4,
    abc)
\end{verbatim}\end{small}

\noindent
The format:

\begin{small}\begin{verbatim}
   [<v 0,0> **[<v 1,0> [<h 0> "(" **x ","] **[<h 0> ***y ")"]]]
\end{verbatim}\end{small}

\noindent
produces:

\begin{small}\begin{verbatim}
   (1234,
    a)
   (1234,
    b)
   (1234,
    c)
\end{verbatim}\end{small}


\subsubsection{Conditionals and expansion-boxes}

Conditionals cannot be expanded. They can be duplicated, but only as the same
object for each copy. This shortcoming can be circumvented by having the
entire expansion appear twice in the code, once for the {\small\verb%then%}
clause of the conditional, and once for the {\small\verb%else%}.


\section{Additional language features\label{addfeatures}}


\subsection{Identifiers\label{identifiers}}

Identifiers in the pretty-printing language must begin with a letter. They can
be of any length. The remaining characters can be letters, decimal digits, or
underscores. Any underscore must be followed by either a letter or a digit.

\index{node-names!non-alphanumeric}
\index{node-names!clashing with reserved words}
Any string of characters (including space, but not line-feed, form-feed or
carriage-return) can be used as an identifier by enclosing it within sharp
signs ({\small\verb%#%}), e.g.~{\small\verb%#/\#%}. This mechanism also allows
the use of identifiers which are reserved words of the language. To include a
sharp sign in the identifier it should be doubled-up,
e.g.~{\small\verb%#test##test#%} denotes the identifier
{\small\verb%test#test%}.

The identifiers used in declarations, abbreviations, and as the name of the
pretty-printer should be legal \ML\ identifiers. This is necessary because the
compiler uses them as identifiers within the \ML\ code it generates.


\subsection{Strings\label{strings}}

A string is any sequence of characters other than line-feed, form-feed, and
carriage-return, enclosed within single quotation marks. A single quote can be
included in the string by doubling it, i.e.~use {\small\verb%''%} for
{\small\verb%'%}. Note that forward-quote is used as the string delimiter, not
back-quote as in \ML.


\subsection{Terminals\label{terminals}}

A {\it terminal\/} is a string constant used in formats to denote a piece of
text which is to appear in the output from the printer. Terminals are like
strings, only using double quotation-marks in place of single quotes.


\subsection{Comments\label{comments}}

A comment is any sequence of characters including line-feed, form-feed and
carriage-return enclosed within percent signs ({\small\verb|%|}). Percent
signs can be included within the comment by doubling them up. Comments are
ignored by the language parser.