writing-instructions.tex

\documentclass[12pt,draft]{article}

% LaTeX magic
\newcounter{chapter}
\input{prelude}
\renewcommand{\theExercise}{\if@ExeStared\else{\thesection.\arabic{\@ExerciseCounter}}\fi}

\begin{document}
\listoftodos

This document describes how to use macros defined in \verb#prelude.tex# and how to define new ones. It also mentions conventions used in the tutorial, to keep it consistent. And, you know, other stuff.

\section{General}
\begin{itemize}
\item Follow the ``Notational Conventions'' from Appendix B of TAPL; use the same nomenclature as in the book.
\item Use \verb#\beluga# to get \beluga, same with other names defined in ``Names of languages'' section of the prelude; \emph{FIXME} what's the status of that? Do we want other languages emphasized like that?
\item All macros, packages used etc should be in \verb#prelude.tex#, don't add that stuff to your chapter file.
\item When creating new macros, stick to the naming conventions and style that we have; put them in the correct place in \verb#prelude.tex# file.
\item It probably makes sense to browse through the \verb#prelude.tex#, there are some useful shortcuts there, not all of them described here.
\end{itemize}

\section{Syntax, inference rules, proofs}
\begin{itemize}
\item Macros for inference rules' names are created using \verb#\ruleName{rule-name}#, e.g. \ruleName{rule-name}; technically you can use that directly but creating macros for the new ones will make the code cleaner.
\item Do not use \verb#\textsf, \mathsf# etc directly in the text, add macros.
\item Avoid \verb#\;# in the text -- what you probably want is to define a command that takes some arguments instead. For instance $\tmhastype {(\tmlam x {T_1} M)} (\tmarr {T_1} T_2)$ is generated by \verb#$\tmhastype {(\tmlam x {T_1} M)} (\tmarr T_1 T_2)$#, if the macros don't take arguments the code is\\
\verb#$\tmhastype\;(\tmlam\;x{:}T_1.M)\;(\tmarr\;T_1\;T_2)$#.
\item To define a BNF grammar for syntax:
\[
\begin{array}{ll@{\bnfas}l}
\mbox{Terms} & M, N & x \bnfalt \lam x{:}T.M \bnfalt M \app N
\end{array}
\]
\begin{verbatim}
\[
\begin{array}{ll@{\bnfas}l}
\mbox{Terms} & M, N & x \bnfalt \lam x{:}T.M \bnfalt M \app N
\end{array}
\]
\end{verbatim}
In particular, use \verb#\bnfas# and \verb#\bnfalt# rather than \verb#::=# \verb#\mid# directly.
\item When defining inference rules, the following should be a good starting point:
\begin{verbatim}
\[
\begin{array}{l@{\quad}l}
\multicolumn{2}{l}
  {\fbox{$e \Value$}: \mbox{Expression $e$ is a value}}\\[1em]
\infer[\VZero]{\tmzero \Value}{} &
\infer[\VSucc]{(\tmsucc t) \Value}{t \Value} \\[1em]
\infer[\VTrue]{\tmtrue \Value}{} &
\infer[\VFalse]{\tmfalse \Value}{}
\end{array}
\]
\end{verbatim}
The resulting array is:
\[
\begin{array}{l@{\quad}l}
\multicolumn{2}{l}{\fbox{$e \Value$}: \mbox{Expression $e$ is a value}}\\[1em]
\infer[\VZero]{\tmzero \Value}{} &
\infer[\VSucc]{(\tmsucc t) \Value}{t \Value} \\[1em]
\infer[\VTrue]{\tmtrue \Value}{} &
\infer[\VFalse]{\tmfalse \Value}{}
\end{array}
\]
\item We use \verb#\infer# (also \verb#\infer*# and \verb#\deduce#) from proof package for inference rules \url{http://www.logicmatters.net/resources/ndexamples/proofsty.html}. However, because we want to sometimes have nicer alignment, the commands \verb#\infera \inferaa \inferaaa# exist (for 1, 2 and 3 premise-rules). It seems to be enough to use them as the outermost commands. Compare
\[
\D = \inferaa
            {\TApp}
            { \Gamma \vdash \tmhastype {(\tmapp M N)} S}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype M {(\tmarr T S)}}{\D_1}}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype N T}{\D_2}}\]
with
\[\D = \infer
            [\TApp]
            { \Gamma \vdash \tmhastype {(\tmapp M N)} S}
            { \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype M {(\tmarr T S)}}{\D_1} &
              \deduce[\vspace{2pt}]{\Gamma \vdash \tmhastype N T}{\D_2}}\]
The former is generated using
\begin{verbatim}
$\D =
\inferaa{\TApp}
  {\Gamma \vdash \tmhastype {(\tmapp M N)} S}
  {\deduce[\vspace{2pt}]
     {\Gamma \vdash \tmhastype M {(\tmarr T S)}}{\D_1}}
  {\deduce[\vspace{2pt}]
     {\Gamma \vdash \tmhastype N T}{\D_2}}$
\end{verbatim}

\item When formulating a theorem, it's good to name the derivations. I use \\
\verb#$\proofderiv{name-in-mathcal}{judgment}$#, e.g. $\proofderiv{\D}{M \Steps M'}$. There's also a variant with built-in $\vdash$:\\
\verb#$\proofderivc{\D}{\Gamma}{M : T}$# $\proofderivc{\D}{\Gamma}{M : T}$\\
I'd suggest using the same when describing proofs.
\item There's an environment for writing cases in proofs (actually, there's more than one). It's not fully satisfactory, but at least it a way of keeping things looking consistent.\\
\verb#\begin{case}{you can put the case here}actual proof\end{case}#
\begin{case}{$\D = \infera{u} {\Gamma \vdash \tmhastype x T}
    {x, u : \tmhastype x T \in \Gamma}$}
Here goes the actual proof
\end{case}
There are examples of this environment in use in chapters 2 and 3.
\end{itemize}

\section{Beluga code}
\begin{itemize}
\item When you mention Beluga code in a paragraph use:

  \verb#\lstinline![ |- t_lam \x . x]!# to get \lstinline![ |- t_lam \x . x]!
\item For longer code, and code examples use literate programming. You have three options for your code:
  \begin{enumerate}
  \item The code you write is part of the main example for this
    chapter and you want to extract it: use

    \verb#\begin{extract}[file1.bel, file2.bel] .. \end{extract}# to

    append this program to file1.bel and file2.bel. In the pdf the
    code will be formatted using the current settings of lstlisting.
  \item The code you write should not be extracted (perhaps is a code
    snippet showing something that does not work). Then you use:

    \verb#\begin{lstlisting} .. \end{lstlisting}#.
  \item Finally, you have some code that is needs to be extracted but
    you do not want it in the document. In this case you use:

    \verb#\begin{extract*}[file1.bel, file2.bel] .. \end{extract*}#
  \end{enumerate}
% \item Use \verb#\begin{lslisting} .. \end{lslisting}# to show bigger fragments of \beluga code
\item The code formatting commands above are like verbatim mode, so whitespace is (..should be, anyway) preserved.
\item If you feel lazy, \verb#\bel{beluga code}# can be used instead of \\
  \verb#\lstinline!beluga code!#.
\item Some keywords in \beluga code are automatically highlighted/coloured etc -- if you feel there's something missing, ``Contextual ML'' section of \verb#prelude.tex# contains all the settings. It will get a proper cleanup at some point, right now some more advanced settings are voodoo (to me anyway).
\end{itemize}



\section{Exercises}
The following code is a way to add exercises and their solutions.\todo{How to extract beluga sourcecode to a separate directory? Does it just work as-is?}
\begin{verbatim}
\begin{Exercise}[title=Some named exercise,label=exerc1]
Extend the language with a let-value-construct
\end{Exercise}

\begin{Exercise}
Write the \bel!step! data-type
\end{Exercise}
\begin{Answer}
\begin{lstlisting}
datatype step: term -> term -> type =
| e_app_1    : step M M'
             -> step (app M N) (app M' N)
| e_app_2    : step N N' -> value V
              -> step (app V N) (app V N')
| e_app_abs : value V
              -> step (app (lam M) V) (M V)
;
\end{lstlisting}
\end{Answer}
\begin{Answer}[ref=exerc1]
Presumably some beluga code with highlighted changes
\end{Answer}
\end{verbatim}
Produces the following exercises.\todo{How does highlighting interact with extraction} By default, the answer is to the latest exercise defined. In order to mix the order, you need to use \verb!label! and a matchin \verb!ref!. However, note that the answers will be printed in the order they were given, not in the order the exercises were defined.\todo{Is there a way to sort them?}.
\begin{Exercise}[title=Some named exercise,label=exerc1]
Extend the language with a let-value-construct
\end{Exercise}
\begin{Exercise}
Write the \bel!step! data-type
\end{Exercise}
\begin{Answer}
\begin{lstlisting}
datatype step: term -> term -> type =
| e_app_1    : step M M'
             -> step (app M N) (app M' N)
| e_app_2    : step N N' -> value V
              -> step (app V N) (app V N')
| e_app_abs : value V
              -> step (app (lam M) V) (M V)
;
\end{lstlisting}
\end{Answer}
\begin{Answer}[ref=exerc1]
Presumably some beluga code with highlighted changes
\end{Answer}

To show the solutions we use \verb|\shipoutAnswer|, this is now done in the appendix.

\shipoutAnswer
\end{document}