% note 'oneside' here prevents blank pages
% by default book tries to make every chapter start on odd (left side)
% so it works better for double-sided books
% see http://stackoverflow.com/a/8371473/337237
\documentclass[11pt,oneside]{book}

\usepackage[margin=1in]{geometry}
\usepackage{amssymb}
\def\emptyset{$\varnothing$}
\def\natnumbers{$\mathbb{N}$}
\usepackage{bussproofs}
\usepackage{listings}

% had to add nounderscore when I moved files out into inputs
% see https://tex.stackexchange.com/a/166630
\usepackage[nounderscore]{syntax}

% custom macro to insert labels into grammar
\newcommand{\synlabel}[1]{\hfill \textit{#1}}

\begin{document}

\frontmatter

\mainmatter

\pagebreak

\begin{center}
    {
        \bf
        \huge
        Lambda Untyped
    }
\end{center}

\begin{center}
{
    \bf
    \huge
    Grammar
}
\end{center}


% taken from https://tex.stackexchange.com/a/24934
\setlength{\grammarindent}{10em} % increase separation between LHS/RHS

% found in http://texdoc.net/texmf-dist/doc/latex/mdwtools/syntax.pdf
\setlength{\grammarparsep}{5pt} % default is 8pt, decrease sep, between rules

\textbf{Expressions}

\begin{grammar}

    <e> ::=  x                           \synlabel{variable}
        \alt $\lambda$ x.<e>             \synlabel{abstraction}
        \alt $<e>_1$ $<e>_2$             \synlabel{application}
        \alt unit                        \synlabel{unit literal}
        \alt true                        \synlabel{true literal}
        \alt false                       \synlabel{false literal}
        \alt if $<e>_1$ $<e>_2$ $<e>_3$  \synlabel{if-else}

\end{grammar}

\textbf{Values}

\begin{grammar}

    <v> ::=  $\lambda$ x.<e>            \synlabel{abstraction}
        \alt unit                       \synlabel{unit literal}
        \alt true                       \synlabel{true literal}
        \alt false                      \synlabel{false literal}

\end{grammar}

\textbf{Evaluation Contexts}

\begin{grammar}

    <C[\textbullet]> ::=  \textbullet                          \synlabel{default}
                     \alt <C[\textbullet]> $<e>_2$             \synlabel{application left}
                     \alt $<v>_1$ <C[\textbullet]>             \synlabel{application right}
                     \alt if <C[\textbullet]> $<e>_2$ $<e>_3$  \synlabel{if-else condition}
\end{grammar}

\hfill
\begin{center}
{
    \bf
    \huge
    Operational semantics
}
\end{center}

\textbf{Syntactic domains}

\begin{tabular}{ l l }
    \textit{e} & Expression \\
    \textit{v} & Values \\
\end{tabular}

\hfill\break

\textbf{Operational semantics}

\begin{center}
\framebox{
                $
                e
                \quad
                \rightarrow
                \quad
                e'
                $
}
\end{center}

\begin{prooftree}
    \AxiomC{ $
                e
                \quad
                \rightarrow
                \quad
                e'
             $ }
    \RightLabel{\it context}
    \UnaryInfC{ $
                C[e]
                \quad
                \rightarrow
                \quad
                C[e']
                $ }
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $
             $ }
    \RightLabel{\it application}
    \UnaryInfC{ $
                (\lambda x . e_1) v_2
                \quad
                \rightarrow
                \quad
                e_1 [v_2 / x]
                $ }
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $
                e_1
                \quad
                \rightarrow
                \quad
                true
             $ }
    \RightLabel{\it if-true}
    \UnaryInfC{ $
                if \ e_1 \ e_2 \ e_3
                \quad
                \rightarrow
                \quad
                e_2
                $ }
\end{prooftree}

\begin{prooftree}
    \AxiomC{ $
                e_1
                \quad
                \rightarrow
                \quad
                false
             $ }
    \RightLabel{\it if-false}
    \UnaryInfC{ $
                if \ e_1 \ e_2 \ e_3
                \quad
                \rightarrow
                \quad
                e_3
                $ }
\end{prooftree}

\end{document}

