\documentclass{article}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{semantic}
\usepackage{listings}

\newenvironment{Table}
  {\begin{center}\begin{tabular}{l l l l @{\quad}l}}
  {\end{tabular}\end{center}}

\begin{document}

% General utility
\newcommand{\seq}[1]{\overline{#1}}
\newcommand{\spaced}{\quad\quad}
\newcommand{\twolines}[2]{\begin{array}{l}#1 \\ #2\end{array}}
\newcommand{\threelines}[3]{\begin{array}{l}#1 \\ #2 \\ #3\end{array}}
\newcommand{\fourlines}[4]{\begin{array}{l}#1 \\ #2 \\ #3 \\ #4\end{array}}
\newcommand{\ifempty}[3]{\ifx\foobaz#1\foobaz #2 \else #3 \fi}
\newcommand{\inabox}[1]{\vspace{0.5em}\boxed{#1}\vspace{0.5em}}

% Operators
\newcommand{\ld}{\lessdot}
\newcommand{\gd}{\gtrdot}
\newcommand{\head}[1]{\textit{head}(#1)}

% Fixity
\newcommand{\atom}{\text{atom}}
\newcommand{\prefix}[2]{\ifempty{#1}{\text{prefix}}{\text{prefix}_{#1}(#2)}}
\newcommand{\suffix}[2]{\ifempty{#1}{\text{suffix}}{\text{suffix}_{#1}(#2)}}
\newcommand{\infix}[2]{\ifempty{#1}{\text{infix}}{\text{infix}_{#1}(#2)}}

% Judgements
\newcommand{\hasfix}[3]{#1\ #2 \in #3}
\newcommand{\sld}[3]{#1 \vdash #2 \ld #3}
\newcommand{\sgd}[3]{#1 \vdash #2 \gd #3}
\newcommand{\stree}[2]{#1 \vdash #2}

% States
\newcommand{\state}[3]{#1\, \big\langle \,#2\, \big\rangle \,#3}
\newcommand{\qstate}[3]{#1\,?\, \big\langle \,#2\, \big\rangle \,#3}
\newcommand{\sstate}[4]{#1 \vdash #2\, \big\langle \,#3\, \big\rangle \,#4}
\newcommand{\sqstate}[5]{#1 \vdash #2\,#3\, \big\langle \,#4\, \big\rangle \,#5}
\newcommand{\sstep}[3]{#1 \vdash #2 \rightarrow #3}

\begin{Table}
token &$t,u,v,w$ &$::=$& $\textit{string}$ \\
associativity &$a$ &$::=$& $L$ & (left assoc) \\
&&$|$& $R$ & (right assoc) \\
precedence &$n,m$ &$::=$& $\mathbb{N}$ \\
fixity &\textit{fix} &$::=$& $\atom$ & (has no children) \\
&&$|$& $\prefix{a}{n}$ \\
&&$|$& $\suffix{a}{n}$ \\
&&$|$& $\infix{a}{n}$ \\
rule &$r$ &$::=$& $t\;\textit{fix}$ \\
grammar &$G$ &$::=$& $\seq{r}$ \\
\\
tree & $x,y,z$ &$::=$& $(\seq{x} t)$ & (tree in RPN) \\
state & $s$ &$::=$& $\state{\seq{x}}{\seq{t}}{\seq{t}}$ & (parsing state) \\
&&$|$& $\qstate{\seq{x}}{\seq{t}}{\seq{t}}$ & (parsing state w/ hole) \\
\end{Table}

Precedence rules:

\begin{figure}
  \inabox{
    \sld{G}{n}{t}\spaced\sgd{G}{t}{n}\spaced
    \sld{G}{t}{n}\spaced\sgd{G}{n}{t}\spaced
    \sld{G}{\emptyset}{t}\spaced\sgd{G}{t}{\emptyset}}
  \[
  \inference{\hasfix{t}{\atom}{G}}{\twolines{\sld{G}{t}{0}}{\sgd{G}{0}{t}}}
  \quad
  \inference{\hasfix{t}{\infix{L}{n}}{G}}{\fourlines
    {\sld{G}{n}{t}}
    {\sgd{G}{t}{n-1}}
    {\sld{G}{t}{n}}
    {\sgd{G}{n}{t}}}
  \quad
  \inference{\hasfix{t}{\infix{L}{n}}{G}}{\fourlines
    {\sld{G}{n-1}{t}}
    {\sgd{G}{t}{n}}
    {\sld{G}{t}{n}}
    {\sgd{G}{n}{t}}}
  \]
  
  \[
  \inference{\hasfix{t}{\prefix{L}{n}}{G}}{\fourlines
    {\sld{G}{\emptyset}{t}}
    {\sgd{G}{t}{n-1}}
    {\sld{G}{t}{n}}
    {\sgd{G}{0}{t}}}
  \quad
  \inference{\hasfix{t}{\prefix{R}{n}}{G}}{\fourlines
    {\sld{G}{\emptyset}{t}}
    {\sgd{G}{t}{n}}
    {\sld{G}{t}{n}}
    {\sgd{G}{0}{t}}}
  \quad
  \inference{\hasfix{t}{\suffix{L}{n}}{G}}{\fourlines
    {\sld{G}{n}{t}}
    {\sgd{G}{t}{\emptyset}}
    {\sld{G}{t}{0}}
    {\sgd{G}{n}{t}}}
  \quad
  \inference{\hasfix{t}{\suffix{R}{n}}{G}}{\fourlines
    {\sld{G}{n-1}{t}}
    {\sgd{G}{t}{\emptyset}}
    {\sld{G}{t}{0}}
    {\sgd{G}{n}{t}}}
  \]

  \[
    \inference
      {\sld{G}{t}{n} & n \leq m}
      {\sld{G}{t}{m}}
    \quad
    \inference
      {\sgd{G}{t}{n} & n \geq m}
      {\sgd{G}{t}{m}}
  \]
  
  \inabox{\sld{G}{t}{t}}
  \[
  \inference{\sld{G}{t}{n} & \sld{G}{n}{u}}{\sld{G}{t}{u}}
  \quad
  \inference{\sgd{G}{t}{n} & \sgd{G}{n}{u}}{\sgd{G}{t}{u}}
  \]
  
  \inabox{\stree{G}{x}}
  \[
  \inference[T-Atom]{\hasfix{t}{\atom}{G}}{\stree{G}{(t)}}
  \quad
  \inference[T-Infix]
    {\hasfix{t}{\infix{}{}}{G} \\ \stree{G}{x} & \sld{G}{\head{x}}{t}
     \\ \stree{G}{y} & \sgd{G}{t}{\head{y}}}
    {\stree{G}{(x\,t)}}
  \]
  
  \[
  \inference[T-Prefix]
    {\hasfix{t}{\prefix{}{}}{G} \\ \stree{G}{x} & \sgd{G}{t}{\head{x}}}
    {\stree{G}{(x\,t)}}
  \quad
  \inference[T-Suffix]
    {\hasfix{t}{\suffix{}{}}{G} \\ \stree{G}{x} & \sld{G}{\head{x}}{t}}
    {\stree{G}{(x\,t)}}
  \]

\caption{Precedence Rules and validity of parse trees}
\end{figure}

\begin{figure}
  \inabox{\sstate{G}{\seq{x}}{\seq{t}}{\seq{t}}}
  \[
  \inference{\stree{G}{x}}{\sstate{G}{x}{}{\seq{w}}}
  \quad
  \inference{
    \hasfix{u}{\prefix{}{}}{G} \\
    \stree{G}{y} & \sgd{G}{u}{\head{y}} \\
    \sqstate{G}{\seq{x}}{0}{\seq{t}}{\seq{w}} \\
  \sld{G}{y}{\textit{first}(\seq{w})} \textit{ or } \seq{w}=\epsilon}
    {\sstate{G}{\seq{x}\,y}{\seq{t}\,u}{\seq{w}}}
  \quad
  \inference{
    \hasfix{u}{\infix{}{}}{G} \\
    \stree{G}{y} & \sld{G}{\head{y}}{u} \\
    \stree{G}{z} & \sgd{G}{u}{\head{z}} \\
    \sgd{G}{n}{u} & \sqstate{G}{\seq{x}}{n}{\seq{t}}{\seq{w}} \\
    \sld{G}{z}{\textit{first}(\seq{w})} \textit{ or } \seq{w}=\epsilon}
    {\sstate{G}{\seq{x}\,y\,z}{\seq{t}\,u}{\seq{w}}}
  \]
  
  \inabox{\sqstate{G}{\seq{x}}{n}{\seq{t}}{\seq{t}}}
  \[
  \inference{}{\sqstate{G}{}{n}{}{}}
  \quad
  \inference{
    \hasfix{u}{\prefix{}{}}{G} & \sgd{G}{u}{m} \\
    \sqstate{G}{\seq{x}}{0}{\seq{t}}{\seq{w}}}
    {\sqstate{G}{\seq{x}}{m}{\seq{t}\,u}{\seq{w}}}
  \quad
  \inference{
    \hasfix{u}{\infix{}{}}{G} & \sgd{G}{u}{m} \\
    \stree{G}{y} & \sld{G}{\head{y}}{u} \\
    \sgd{G}{n}{u} & \sqstate{G}{\seq{x}}{n}{\seq{t}}{\seq{w}}}
    {\sqstate{G}{\seq{x}\,y}{m}{\seq{t}\,u}{\seq{w}}}
  \]

\caption{Validity of parsing states}
\end{figure}

\begin{figure}
  \inabox{\sstep{G}{s}{s}}
  \[
  \inference[P-Atom]
    {\hasfix{v}{\atom}{G}}
    {\sstep{G}
      {\qstate{\seq{x}}{\seq{t}}{v\,\seq{w}}}
      {\state{\seq{x}\,v}{\seq{t}}{\seq{w}}}}
  \quad
  \inference[P-Suffix]
    {\hasfix{v}{\suffix{}{}}{G} \\
     \sgd{G}{\textit{last}(\seq{t})}{v} \textit{ or } \seq{t}=\epsilon}
    {\sstep{G}
      {\state{\seq{x}\,y}{\seq{t}}{v\,\seq{w}}}
      {\state{\seq{x}\,(y\,v)}{\seq{t}}{\seq{w}}}}
  \]

  \[
  \inference[P-PushPrefix]
    {\hasfix{v}{\prefix{}{}}{G}}
    {\sstep{G}
      {\qstate{\seq{x}}{\seq{t}}{v\,\seq{w}}}
      {\qstate{\seq{x}}{\seq{t}\,v}{\seq{w}}}}
  \quad
  \inference[P-PushInfix]
    {\hasfix{v}{\infix{}{}}{G} \\
     \sgd{G}{\textit{last}(\seq{t})}{v} \textit{ or } \seq{t}=\epsilon}
    {\sstep{G}
      {\state{\seq{x}}{\seq{t}}{v\,\seq{w}}}
      {\qstate{\seq{x}}{\seq{t}\,v}{\seq{w}}}}
  \]

  \[
  \inference[P-PopPrefix]
    {\hasfix{u}{\prefix{}{}}{G} \\
     \sld{G}{u}{\textit{first}(\seq{w})} \textit{ or } \seq{w}=\epsilon}
    {\sstep{G}
      {\state{\seq{x}\,y}{\seq{t}\,u}{\seq{w}}}
      {\state{\seq{x}\,(y\,u)}{\seq{t}}{\seq{w}}}}
  \quad
  \inference[P-PopInfix]
    {\hasfix{u}{\infix{}{}}{G} \\
     \sld{G}{u}{\textit{first}(\seq{w})} \textit{ or } \seq{w}=\epsilon}
    {\sstep{G}
      {\state{\seq{x}\,y\,z}{\seq{t}\,u}{\seq{w}}}
      {\state{\seq{x}\,(y\,z\,u)}{\seq{t}}{\seq{w}}}}
  \]

  \caption{Parsing algorithm}
\end{figure}

\begin{figure}
  \begin{lstlisting}
  function parse(ts):
    let (x, vs) = parseRightArg(top, ts) in
    assert vs is empty
    return (x, vs)

  function parseRightArg(u, v ts):
    case v of
      atom => parseSuffix(u, (v), ts)
      prefix => let (x, ts') = parseRightArg(v, ts)
                parseSuffix(u, (x v), ts')

  function parseSuffix(u, x, ts):
    case ts of
      empty => (x, empty)
      v ts =>
        if u *> v and x <* v
        then case v of
          suffix => parseSuffix(u, (x v), ts)
          infix => let (y, ts') = parseRightArg(v, ts)
                   parseSuffix(u, (x y v), ts')
        else (x, v ts)
  \end{lstlisting}

  \caption{Parsing algorithm (code)}
\end{figure}

\end{document}