%
% Copyright 2016, NICTA
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(NICTA_GPL)
%

%\newlength{\tpheight}\setlength{\tpheight}{0.9\textheight}
%\newlength{\txtheight}\setlength{\txtheight}{0.9\tpheight}
%\newlength{\tpwidth}\setlength{\tpwidth}{0.9\textwidth}
%\newlength{\txtwidth}\setlength{\txtwidth}{0.9\tpwidth}
%\newlength{\drop}                     
%\setlength{\parindent}{0cm}
%\setlength{\parskip}{9pt plus 1pt minus 1pt}
\newcommand{\alt}{\;\mid\;}

\newcommand{\boxlabel}[1]{\begin{center}
\framebox{#1}
\end{center}}

\setlength{\fboxsep}{1pt}

\newsavebox{\@brx}
\newcommand{\llangle}[1][]{\savebox{\@brx}{\(\m@th{#1\langle}\)}%
    \mathopen{\copy\@brx\mkern2mu\kern-0.9\wd\@brx\usebox{\@brx}}}
\newcommand{\rrangle}[1][]{\savebox{\@brx}{\(\m@th{#1\rangle}\)}%
    \mathclose{\copy\@brx\mkern2mu\kern-0.9\wd\@brx\usebox{\@brx}}}

\newenvironment{inductive}[1]{\boxlabel{$#1$} \vspace{-0.8em} \start@gather\st@rredtrue}{\endgather}
\newenvironment{inductive0}{\vspace{-0.8em} \start@gather\st@rredtrue}{\endgather}
% Side by Side layout
\newenvironment{sidebyside}{
\begin{tabular}{p{0.48\textwidth}p{0.5\textwidth}}
  }{
\end{tabular}
}
\newenvironment{fundef}[2]{\begin{center}\boxlabel{$#1 : #2$} \begin{displaymath}\begin{array}{lclr}}{  \end{array}\end{displaymath}\end{center}}
\newcommand{\taken}[1]{\text{\sout{\ensuremath{#1}}}}
\newcommand{\PrimType}[1]{\texttt{#1}}
\newcommand{\Observed}[1]{#1!}
\newcommand{\Unit}{\texttt{()}}
\newcommand{\AbsN}[1]{\texttt{#1}}
\newcommand{\AbsTy}[3]{\AbsN{#1}\ #2\ #3}
\newcommand{\FunTy}[2]{#1 \rightarrow #2}
\newcommand{\PrdTy}[2]{#1 \times #2}
\newcommand{\PolyTy}[2]{\forall (#1).\ #2}
\newcommand{\VariantTy}[1]{\langle #1 \rangle}
\newcommand{\RecordTy}[2]{\{ #1 \}\ #2}
\newcommand{\ConsN}[1]{\mathsf{#1}}
\newcommand{\FunN}[1]{#1}
\newcommand{\VarN}[1]{#1}
\newcommand{\Cons}[2]{\ConsN{#1}\ #2}
\newcommand{\FieldN}[1]{\text{#1}}
\newcommand{\FieldTy}[2]{\FieldN{#1}\ :: #2}
\newcommand{\FieldEq}[2]{\FieldN{#1}\ = #2}
\newcommand{\Discardable}{\mathsf{D}}
\newcommand{\Shareable}{\mathsf{S}}
\newcommand{\Escapable}{\mathsf{E}}
\newcommand{\Linear}{\mathsf{DS}}
\newcommand{\TyApp}[2]{\FunN{#1}[#2]}
\newcommand{\GenPrimOp}[2]{#1(#2)}
\newcommand{\LET}{\mathbf{let}}
\newcommand{\IN}{\mathbf{in}}
\newcommand{\CAST}{\mathbf{cast}}
\newcommand{\SPLIT}{\mathbf{split}}
\newcommand{\IF}{\mathbf{if}}
\newcommand{\PROMOTE}{\mathbf{promote}}
\newcommand{\THEN}{\mathbf{then}}
\newcommand{\ELSE}{\mathbf{else}}
\newcommand{\OF}{\mathbf{of}}
\newcommand{\CASE}{\mathbf{case}}
\newcommand{\ESAC}{\mathbf{esac}}
\newcommand{\TAKE}{\mathbf{take}}
\newcommand{\PUT}{\mathbf{put}}
\newcommand{\VAR}{\mathbf{var}}
\newcommand{\Let}[3]{\LET\ \VarN{#1} = #2\ \IN\ #3}
\newcommand{\LetBang}[4]{\LET!(\VarN{#1})\ \VarN{#2} = #3\ \IN\ #4}
\newcommand{\Cast}[2]{\CAST\ #1\ #2}
\newcommand{\Split}[3]{\SPLIT\ #1\ \IN\ \VarN{#2}.\ #3}
%\newcommand{\Split}[3]{\FIXME{Split now absent.}}
\newcommand{\Promote}[2]{\PROMOTE\ \VariantTy{#1}\ #2}
\newcommand{\If}[3]{\IF\ #1\ \THEN\ #2\ \ELSE\ #3}
\newcommand{\Esac}[1]{\ESAC\ #1}
\newcommand{\Case}[5]{\CASE\ #1\ \OF\ #2 \rightarrow #3\ \ELSE\ #4 \rightarrow #5}
\newcommand{\Take}[5]{\TAKE\ \VarN{#1}\ \{ \FieldEq{#2}{#3} \} = #4\ \IN\ #5}
\newcommand{\Put}[3]{\PUT\ #1.\FieldN{#2} \coloneqq #3}
\newcommand{\FunDef}[4]{\langle #1 :: #2, #1\ \VarN{#3} = #4\rangle}
\newcommand{\AbsFunDef}[2]{\langle #1 :: #2, \blacksquare\rangle}
\newcommand{\StructInit}[1]{\{ #1 \}}
\newcommand{\Tup}[2]{(#1,#2)}
%\newcommand{\Tup}[2]{\FIXME{Tuples now absent.}}
\newcommand{\App}[2]{#1\ #2}
\newcommand{\Member}[2]{#1.\FieldN{#2}}
\newcommand{\ModeN}[1]{\texttt{#1}}
\newcommand{\ReadOnly}{\ModeN{r}}
\newcommand{\Writable}{\ModeN{w}}
\newcommand{\Unboxed}{\ModeN{u}}
\newcommand{\perhaps}[1]{#1^?}
\newcommand{\many}[1]{\overline{#1}}
\newcommand{\OfKind}[2]{#1 ::_{\mathrm{K}} #2}
\newcommand{\ofKind}[2]{#1 :_{\mathrm{K}} #2}
\newcommand{\ofType}[2]{#1 : #2}
\newcommand{\ofTypeS}[2]{#1 :\!*\ #2}
\newcommand{\Kinding}[3]{#1 \vdash \ofKind{#2}{#3} }
\newcommand{\BangF}[1]{\textbf{bang}(#1)}
\newcommand{\LitType}[1]{\textbf{litType}(#1)}
%\newcommand{\FunType}[1]{\textbf{funType}(#1)}
\newcommand{\FunType}[1]{\FIXME{funType now absent}}
%\newcommand{\FunTypes}{\textbf{funType}}
\newcommand{\FunTypes}[1]{\FIXME{funType now absent}}
%\newcommand{\FunTyEnv}[2]{\textbf{funType}(#1) = #2}
\newcommand{\FunTyEnv}[2]{\textbf{funDef}(#1) = \langle#2,\_\rangle}
\newcommand{\AbsFunTyEnv}[2]{\textbf{funDef}(#1) = \langle#2,\blacksquare\rangle}
%\newcommand{\FunTyEnv}[1]{\FIXME{funType now absent}}
\newcommand{\Typing}[4]{#1; #2 \vdash \ofType{#3}{#4}}
\newcommand{\TypingS}[4]{#1; #2 \vdash \ofTypeS{#3}{#4}}
\newcommand{\Subst}[3]{#1[#3 / #2]}
\newcommand{\Weakening}[3]{#1 \vdash #2 \stackrel{\text{weak}}{\leadsto} #3}
\newcommand{\Contraction}[4]{#1 \vdash #2 \leadsto #3 \boxplus #4}
\newcommand{\PrimOpType}[1]{\textbf{primopType}(#1)}
\newcommand{\ValSem}[3]{#1 \vdash #2 \Downarrow_v #3}
\newcommand{\FunVal}[2]{ \llangle \lambda #1.\ #2 \rrangle }
\newcommand{\AbsFunVal}[2]{ \llangle \textbf{abs.} #1\ |\ #2 \rrangle }
\newcommand{\FunDefn}[1]{\textbf{funDef}(#1)}
\newcommand{\FunDefns}{\textbf{funDef}}
\newcommand{\EnvBind}[2]{#1 \mapsto #2}
\newcommand{\rulename}[1]{\textsc{\small#1}}
\newcommand{\semantics}[1]{\llbracket #1 \rrbracket}
\newcommand{\AValSem}[2]{\semantics{#1}_v\ #2}
\newcommand{\AUpdSem}[1]{\semantics{#1}_u}
\newcommand{\AbsValSem}[3]{\AValSem{#1}{#2} = #3}
\newcommand{\AbsUpdSem}[5]{\AUpdSem{#1}\ (#2,#3) = (#4,#5)}
\newcommand{\RecordVal}[1]{\StructInit{#1}}
\newcommand{\UpdSem}[5]{#1 \vdash #2\ |\ #3 \Downarrow_u #4\ |\ #5}
\newcommand{\UpdSemA}[5]{#1 \vdash #2\ |\ #3 \Downarrow_u\!\!*\ #4\ |\ #5}
\newcommand{\HiBlue}[1]{\text{\colorbox{light-gray}{$\textcolor{blue}{#1}$}}}
\newcommand{\HiPurple}[1]{\textcolor{purple}{#1}}
\newcommand{\VTRN}[6]{#1\ |\ #2 : #3 :\ #4\ [#5 \ast #6]}
\newcommand{\VTR}[6]{\HiBlue{#1\ |\ #2 :}\ \HiPurple{#3 :}\ #4\ \HiBlue{[#5 \ast #6]}}
\newcommand{\VTRA}[6]{\HiBlue{#1\ |\ #2 :\!\!*}\ \HiPurple{#3 :\!\!*}\ #4\ \HiBlue{[#5 \ast  #6]}}
\newcommand{\VTRAbs}[6]{\HiBlue{#1\ |\ #2 :_A}\ \HiPurple{#3 :_A}\ #4\ \HiBlue{[#5 \ast #6]}}
\newcommand{\dash}{\mbox{-}}
\newcommand{\set}{\ensuremath{\mathit{set}}\xspace}
\newcommand{\bool}{\ensuremath{\mathit{bool}}\xspace}
\newcommand{\monad}{\ensuremath{\mathit{monad}}\xspace}

\newcommand{\srel}{\ensuremath{\mathit{\mathcal{R}}}\xspace}
\newcommand{\valrel}{\ensuremath{\mathit{val\dash{}rel}}\xspace}
\newcommand{\typerel}{\ensuremath{\mathit{type\dash{}rel}}\xspace}
\newcommand{\heaprelptr}{\ensuremath{\mathit{heap\dash{}rel\dash{}ptr}}\xspace}
\newcommand{\heaprel}{\ensuremath{\mathit{heap\dash{}rel}}\xspace}
\newcommand{\heap}{\ensuremath{\mathit{heap}}\xspace}
\newcommand{\isvalid}{\ensuremath{\mathit{is\dash{}valid}}\xspace}

\newcommand{\TYPE}{\ensuremath{\mathit{TYPE}}\xspace}

\newcommand{\corres}{\ensuremath{\mathbf{corres}}\xspace}
\newcommand{\correspond}{\ensuremath{\mathbf{correspondence}}\xspace}
\newcommand{\corresargs}[2]{\ensuremath{\corres \ R\ #1 \ #2 \ U \ \Gamma \ \mu \ \sigma}\xspace}
\newcommand{\corresargsE}[4]{\ensuremath{\corres \ R\ #1 \ #2 \ #3 \ #4 \ \mu \ \sigma}\xspace}

\newcommand{\scorres}{\ensuremath{\mathbf{scorres}}\xspace}
\newcommand{\monoexpr}{\ensuremath{\mathcal{M}_e}\xspace}
\newcommand{\monoval}{\ensuremath{\mathcal{M}_v}\xspace}
\newcommand{\rename}{\ensuremath{r}\xspace}

\newcommand{\some}{\ensuremath{\mathit{Some}}\xspace}
\newcommand{\none}{\ensuremath{\mathit{None}}\xspace}
\newcommand{\failed}{\ensuremath{\mathit{failed}}\xspace}
\newcommand{\results}{\ensuremath{\mathit{results}}\xspace}

\newcommand{\mreturn}{\ensuremath{\mathbf{return}}\xspace}
\newcommand{\mgets}{\ensuremath{\mathbf{gets}}\xspace}
