manual.tex

\documentclass{article}

\title{The Ott \LaTeX{} Layout Package \texttt{ottlayout.sty}}

\author{Rok Strni\v sa \and Matthew Parkinson}

% the un-wrapped (-tex_wrap false) generated LaTeX file for LJ
\include{lj_included}

% currently required by Ott-generated, un-wrapped LaTeX
\usepackage{amsmath}

% required by LJ's LaTeX
\usepackage{amssymb}

% the package that allows customized layout described in this document
\usepackage{ottlayout}

% the automatically generated file (with our Makefile) to link the generated
% LaTeX with the ottlayout package
\include{lj_override}

% supertabular package required if using the default grammar tabular
\usepackage{supertabular}

% only used in bibliography to link to LJ's webpage
\usepackage{url}

\begin{document}

\maketitle

\section{Introduction}
%

The Ott \LaTeX{} Layout Package, \texttt{ottlayout.sty}, provides a
range of options to tune the typesetting of 
Ott-generated inductive definition rules and grammars, overriding the
default typesetting of the Ott-generated \LaTeX{} code.

This document illustrates the common-case usage of the package, using
Lightweight Java (LJ)~\cite{lj} as an example Ott project.
It should be read in conjunction with the source for this document (\verb+manual.tex+) and the \verb+Makefile+.

\section{Usage}
To use the package, one first uses Ott to generate \LaTeX{} code with
a chosen \verb+-tex_name_prefix+, by default \verb+ott+, but here
\verb+lj+, as in the example \verb+Makefile+:
\begin{verbatim}
lj_included.tex : $(lj)
         ott $(INC_ARGS) -tex_name_prefix lj -tex $@ \
             -merge true $(lj)
\end{verbatim}
Then one builds a file such as \verb+lj_override.tex+, e.g.~as below.
\begin{verbatim}
%_override.tex: override.tex empty.ott
         ott $(INC_ARGS) -tex_name_prefix lj \
           -tex_filter override.tex $@ empty.ott
\end{verbatim}
This file simply contains redefinitions of some default \LaTeX{}
commands generated by Ott (with the \verb+lj+ prefix) to use the
\texttt{ottlayout.sty} commands, e.g.
\begin{verbatim}
  \renewcommand{\ljpremise}[1]{\premiseSTY{#1}}
  \renewcommand{\ljusedrule}[1]{\usedruleSTY{#1}}
  \renewcommand{\ljdrule}[4][]{\druleSTY[#1]{#2}{#3}{#4}}
  \renewenvironment{ljdefnblock}[3][]{%
    \defnblockSTY[#1]{#2}{#3}}{\enddefnblockSTY}
\end{verbatim}
Finally, in the user \LaTeX{} document (for example this
\texttt{manual.tex}), one:
(a) includes the generated \LaTeX{} for the user language, e.g.~with
\verb+\include{lj_included}+;
(b) uses the \texttt{ottlayout.sty} package, e.g.~with
\verb+\usepackage{ottlayout}+; and
(c) uses the generated override file to link the generated \LaTeX{}
with \verb+ottlayout.sty+, e.g.~with
\verb+\include{lj_override}+.




\section{Displaying grammar}
%
To display all Ott-generated \LaTeX{} for LJ, we would normally write the command
\verb+\ljall{}+. To output all the LJ's grammar, we would use the \LaTeX{}
command: \verb+\ljgrammar{}+. To show only selected parts of the grammar, we
would normally use the command \verb+\ljgrammartabular{}+. For example, to
display the grammar of LJ's statement ({\tt s}) and class definition ({\tt
  cld}), we would write
\footnote{The automatically generated grammar tabular command, here \texttt{$\backslash{}$ljgrammartabular\{\}}, uses the {\tt supertabular} package. Therefore, if we use the
default grammar tabular, we have to explicitly import this package by writing
\texttt{$\backslash{}$usepackage\{supertabular\}} in our \LaTeX{} document's prelude.}
%
\begin{verbatim}
  \ljgrammartabular{\ljs\ljinterrule\ljcld\ljafterlastrule}
\end{verbatim}
%
to produce:\\[2ex]
\ljgrammartabular{\ljs\ljinterrule\ljcld\ljafterlastrule}\\[2ex]


Alternatively, we can use the \texttt{ottlayout} package's
\verb+\grammartabularSTY{}+ to produce a slightly more compact output, usually
more suitable for publications. To display the same grammars, we would write
%
\begin{verbatim}
  \grammartabularSTY{\ljs\\\ljcld}
\end{verbatim}
%
to produce:\\[2ex]
\grammartabularSTY{\ljs\\\ljcld}\\[2ex]

Note that in both cases the comments on the right are aligned according to the
longest production in the block. Therefore, if the length of productions varies
a lot, it is sometimes suitable to split them up into separate grammar
tabulars. We could split the above example by writing
%
\begin{verbatim}
  \grammartabularSTY{\ljs}\\
  \grammartabularSTY{\ljcld}
\end{verbatim}
%
to produce:\\[2ex]
\grammartabularSTY{\ljs}\\
\grammartabularSTY{\ljcld}\\[2ex]

\section{Displaying rules}
%
To display all the rules of LJ, we would normally use the Ott-generated \LaTeX{} command
\verb+\ljdefnss{}+. To show all the rules of the LJ's reduction relation, we
would use the command \verb+\ljdefnrXXstmt{}+ --- if you are not sure what the
name of the command you are looking for is, the easiest way to find out is to
check the Ott-generated \LaTeX{} file, which is in our case {\tt
  lj\_included.tex}.

The \texttt{ottlayout} package gives many different options for displaying a
particular rule and groups of rules. The currently available display options
are:
%
\begin{center}
\begin{tabular}{|l|l|c|}
\hline
{\bf Setting name} & {\bf Possible values} & {\bf Default value}\\\hline
\hline
showruleschema & yes $|$ no & yes\\\hline
showcomment & yes $|$ no & yes\\\hline
rulelayout & oneperline $|$ nobreaks & oneperline\\\hline
premiselayout & oneperline $|$ oneline $|$ justify & justify\\\hline
premisenamelayout & right $|$ left $|$ topright $|$ none & right\\\hline
numberpremises & yes $|$ no & no\\\hline
numbercolour & {\it any dvips colour name} & \color{Gray}{Gray}\\\hline
\end{tabular}
\end{center}
%
The default settings result in the same output as if the \texttt{ottlayout}
package was not used.

We use  LJ's (fairly complicated) reduction rule for methods to
demonstrate a few of the available display settings for an example. To
display the LJ rule {\tt r\_mcall} with default settings we write
%
\begin{verbatim}
  \ljdrulerXXmcall{}
\end{verbatim}
%
which produces:\\[2ex]
\ljdrulerXXmcall{}\\[2ex]
%
Note that math mode is entered automatically, which means that we can use any
\LaTeX{} text layout utilities to layout our rules as we wish.

We can change the default setting with command \verb+\ottstyledefaults{}+ by
passing keys and values in the KeyVal style. For example, to make the premises
display more compactly in all rules from now on, we write
%
\begin{verbatim}
  \ottstyledefaults{premiselayout=justify}
\end{verbatim}
\ottstyledefaults{premiselayout=justify}
%
Now the the command \verb+\ljdruleXXmcall{}+ produces the following instead:\\[2ex]
\ljdrulerXXmcall{}\\[2ex]

To use the non-default settings for a particular rule, we can write the same
KeyVal pairs inside as the parameter to the rule command. For example, to number
the premises in the rule, to make the numbers yellow-orange, and to place the
rule's name in top-right corner, we write
%
\begin{verbatim}
  \ljdrulerXXmcall{numberpremises=yes,
                   numbercolour=YellowOrange,
                   premisenamelayout=topright}
\end{verbatim}
%
which produces:\\[2ex]
\ljdrulerXXmcall{numberpremises=yes,
                 numbercolour=YellowOrange,
                 premisenamelayout=topright}\\[2ex]
%
As you can see, the setting for compacting the premises was kept, because it was
set globally for all rules following the \verb+\ottstyledefaults{}+ command.

As with commands for individual rules, we can pass in KeyVal pairs to the
commands that display groups of rules, which will affect how the rules of that
particular group of rules is displayed. If we wanted to display LJ's
reduction rules for statements with current default display settings, we would
write \verb+\ljdefnrXXstmt{}+. To display the reduction rules with rule names on
the left side, and their premises numbered, we write
%
\begin{verbatim}
  \ljdefnrXXstmt{numberpremises=yes, premisenamelayout=left}
\end{verbatim}
%
This produces\footnote{We set the font size to {\tt small} so that the rules
  are not too wide.}:\\[2ex]
{\small\ljdefnrXXstmt{numberpremises=yes, premisenamelayout=left}}\\[2ex]
%
Therefore, Ott-generated \LaTeX{} commands for rules of a specific {\bf defn} in
the Ott source file can take KeyVal arguments. However, note that currently the
Ott-generated \LaTeX{} output does not allow for this package to allow the same
arguments being passed to commands for a group of {\bf defn}s, i.e.~{\bf defns}.

\bibliographystyle{acm}
\bibliography{manual}

\end{document}