\newif\ifacmart
\acmarttrue

\ifacmart
  \documentclass[acmsmall, anonymous, review, natbib=false, pbalance]{acmart}
\else
  \documentclass[a4paper]{article}
\fi

%% Package Imports %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Provided by acmart
\ifacmart\else
  \usepackage{amsthm} %% proof environments
\fi

%% Incompatible with acmart
\ifacmart\else
  \usepackage[
    warnings-off={mathtools-colon,mathtools-overbracket}
  ]{unicode-math} %% math symbols
  \usepackage[subtle, margins=tight]{savetrees}
\fi

\usepackage[
  datamodel=acmdatamodel,
  style=acmnumeric
]{biblatex}   %% bibliography configuration
\usepackage{booktabs} %% table formatting
\usepackage{ebproof}  %% proof trees
\usepackage{expl3}  %% Latex 3
\usepackage{enumitem} %% format contributions list
\usepackage{float}  %% forcing figures
\usepackage{hyperref} %% hyperlinks within document
\usepackage{mathtools}  %% matrix alignment
\usepackage[verbatim]{minted}  %% code formatting
\usepackage{pifont} %% Check and cross marks
\usepackage{stackrel} %% Annotating judgements
\usepackage{subcaption} %% subfigures with captions
\usepackage{subfiles} %% splitting file into sections
\usepackage{thmtools} %% proof environments
\usepackage{tikz} %% diagram
\usepackage[dvipsnames]{xcolor} %% color TODO and FIXME
\usepackage{xr} %% cross reference between sections

%% After hyperref
\usepackage{cleveref} %% easier citations

%% Document Metadata %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\author{Greg Brown}
\ifacmart
  \orcid{0009-0000-3401-8637}
  \affiliation{%
    \institution{University of Edinburgh}
    \city{Edinburgh}
    \country{UK}
  }
  \email{greg.brown01@ed.ac.uk}{}
\fi

\ifacmart
  \acmJournal{PACMPL}
  %% \acmConference[ICFP '25]{}{January 21, 2025}{Denver, CO, USA}
\fi

\ifacmart
  \setcopyright{none}
\fi

\title{ARTyST:\ Adding Regular Types to System~T}

\ifacmart
  \keywords{}
\fi

%% Package Configuration %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% biblatex
\addbibresource{\subfix{main.bib}}

%% hyperref
\ifacmart\else
  \makeatletter
  \hypersetup{
    pdftitle={\@title},
    pdfauthor={\@author},
  }
  \makeatother
\fi

%% Minted centered
\RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{}

%% xr
\externaldocument[M-]{\subfix{main}}

%% Possessive textcite
\DeclareNameWrapperFormat{labelname:poss}{#1's}
\DeclareFieldFormat{shorthand:poss}{%
  \ifnameundef{labelname}{#1's}{#1}}
\DeclareFieldFormat{citetitle:poss}{\mkbibemph{#1}'s}
\DeclareFieldFormat{label:poss}{#1's}

\newrobustcmd*{\posscitealias}{%
  \AtNextCite{%
    \DeclareNameWrapperAlias{labelname}{labelname:poss}%
    \DeclareFieldAlias{shorthand}{shorthand:poss}%
    \DeclareFieldAlias{citetitle}{citetitle:poss}%
    \DeclareFieldAlias{label}{label:poss}}}

\newrobustcmd*{\posscite}{%
  \posscitealias%
  \textcite}

\newrobustcmd*{\Posscite}{\bibsentence\posscite}

\newrobustcmd*{\posscites}{%
  \posscitealias%
  \textcites}

%% Theorem Environments %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ifacmart\else
  \declaretheorem[
    style=plain,
    numberwithin=section
  ]{definition}
  \declaretheorem[
    numberwithin=section,
    sibling=definition
  ]{lemma,corollary,proposition,theorem, conjecture}
  \declaretheorem[
    style=remark,
    numberwithin=section,
    sibling=definition
  ]{remark,example}
\fi

\renewcommand*{\textcitedelim}{\addcomma\addspace\iflastcitekey{\bibstring{and}\addspace}{}}

%% Custom Macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Needed for compatibility
\ifacmart\else
  \newcommand{\bibliofont}{\footnotesize}
\fi

% Psuedocode
\newminted[systemt]{lexer.py:SystemTLexer}{}
\newmintinline[systemtinline]{lexer.py:SystemTLexer}{}

% TODOS and such
\newcommand\lang{{\color{Green} ARTyST}}
\newcommand\TODO[1]{{\color{Blue}TODO:\ {#1}}}
\newcommand\FIXME[1]{{\color{Red}FIXME:\ {#1}}}

% Quantification: e.g. \rangeover{x_i}{i < n}
\newcommand\rangeover[2]{\overrightarrow{#1}}

% Judgements for typing and such
\NewDocumentCommand\judgement{momO{:}m}{%
  {#1} \vdash^{\IfNoValueF{#2}{#2}} {#3} \mathrel{#4} {#5}
}
\newcommand\jdgmnt[3]{{#2} \vdash {#3}~\mathrm{#1}}

% List operators
\newcommand\append{\mathbin{@}}

%%% Term syntax

%% Let
\newcommand\letkw{\ensuremath{\mathsf{let}}}
\newcommand\lettm[3]{\letkw~{#2} \coloneq {#1}~\mathsf{in}~{#3}}
\ExplSyntaxOn
%% args:
%%   1. Do I need a & on the first line?
%%   2. Binder name
%%   3. Is value multiline?
%%   4. Value
\NewDocumentCommand \squid_letpart {m m m m}
  { \IfBooleanTF{#3}
      { \letkw \IfBooleanTF{#1}{&}{\nobreakspace} {#2} = \cr
        & {#4} \cr
        \mathsf{in}
      }
      { \letkw \IfBooleanTF{#1}{&}{\nobreakspace} {#2} = {#4} \nobreakspace \mathsf{in}
      }
  }
%% args:
%%   1. Do I need a & on the first line?
%%   2. Binder name
%%   3. Is value multiline?
%%   4. Value
%%   ... further processing
\NewDocumentCommand \squid_contlet {m m s m}
  { \squid_letpart {#1} {#2} {#3} {#4}
    \IfBooleanTF{#3}
      { \squid_checklet [\BooleanFalse] }
      { \squid_checklet [\BooleanTrue] }
  }
%% args:
%%   1. If something, do I need a new line?
%%   2. Is the next arg not a binder?
%%   ... further processing
\NewDocumentCommand \squid_checklet {o s m}
  { \IfBooleanTF{#2}
      { \IfNoValueF{#1}{\IfBooleanT{#1}{\cr}} & {#3}
        \end{array}
        \wlog{End~let}
      }
      { \IfNoValueTF{#1}
          { \squid_contlet \BooleanTrue {#3} }
          { \IfBooleanTF{#1}{\cr}{&}
            \squid_contlet {#1} {#3}
          }
      }
  }
\NewDocumentCommand \dolet {O{t}}
  { \arraycolsep=0.2em
    \wlog{Begin~let}
    \begin{array}[#1]{ll}
      \squid_checklet
  }
\ExplSyntaxOff

%% Encoding
\newcommand\encode[1]{\llcorner {#1} \lrcorner}

%% Tuples
\DeclarePairedDelimiter\rawtuple{\langle}{\rangle}
\NewDocumentCommand\domultituple{mm}{%
  \langle & {#1} \cr
  , & {#2} \cr
  \rangle &
}
\NewDocumentCommand\multituple{>{\SplitArgument{1}{,}}m}{{%
  \arraycolsep=0.2em
  \begin{array}[t]{rl}
  \domultituple#1
  \end{array}%
}}
\NewDocumentCommand\tuple{s}{\IfBooleanTF{#1}{\multituple}{\rawtuple}}

%% Naturals
\newcommand\nat{\ensuremath{\mathsf{N}}}
\newcommand\zero{\ensuremath{\mathsf{zero}}}
\newcommand\suc{\ensuremath{\mathsf{suc}}}

\newcommand\primreckw{\ensuremath{\mathsf{primrec}}}
\newcommand\primrec[3]{\primreckw~{#1}~{#2}~{#3}}

%% Functors
\newcommand\mapkw{\ensuremath{\mathsf{map}}}
% e.g. \maptm{X}{1 + X}
\newcommand\maptm[2]{\mapkw_{\Lambda {#1}.{#2}}}

%% Arbitrary values
\newcommand\arb{\ensuremath{\mathsf{arb}}}

%% Recursive types
\ExplSyntaxOn
\NewDocumentCommand \roll {s}
  { \ensuremath{\mathsf{roll \IfBooleanT{#1}{2}}} }
\ExplSyntaxOff
\newcommand\unroll{\ensuremath{\mathsf{unroll}}}
\newcommand\foldkw{\ensuremath{\mathsf{fold}}}
\newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}}

\ExplSyntaxOn
\NewDocumentCommand \squid_foldpart:nn {m m m}
  { {#2}. \IfBooleanT{#1}{\\ &} {# 3}
  }
\NewDocumentCommand \dofold {s m m m}
  { \IfBooleanTF{#1}
      { \begin{aligned}
          \MoveEqLeft
            { \foldkw \nobreakspace
              {#2} \nobreakspace
              \mathsf{with} \nobreakspace
              {#3} .
            } \\
          & {#4}
        \end{aligned}
      }
      { \foldtm{#2}{#3}{#4} }
  }
\ExplSyntaxOff

%% Sums
\newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}}
\newcommand\casetm[4]{\matchtm{#1}{\rangeover{{#2}.~{#3}}{#4}}}

\ExplSyntaxOn
\NewDocumentCommand \squid_matchpart:nn {m m m}
  { \IfBooleanT{#1}{\quad} {#2}. \IfBooleanTF{#1}{&}{\nobreakspace} {#3}
  }
\NewDocumentCommand \squid_contmatch:n {m m > {\SplitArgument{1}{.}} m}
  { \squid_matchpart:nn {#1} #3 \squid_checkmatch {#1} {#2} {#2}
  }
\NewDocumentCommand \squid_checkmatch {m m m g}
  { \IfValueTF{#4}
      {#2 \squid_contmatch:n {#1} {#3} {#4}}
      {\IfBooleanT{#1}{\end{array}}}
  }
%% Arguments are kw; multiline; alignment; target
\NewDocumentCommand \squid_startmatch {m m m m}
  { \IfBooleanTF{#2}
      {\arraycolsep=0.2em
       \begin{array}[#3]{ll}
         \multicolumn{2}{l}{
           {#1} \nobreakspace
           {#4} \nobreakspace
           \mathsf{with}
         }
         \squid_checkmatch {#2} {\\} {\\}
      }
      { {#1} \nobreakspace
        {#4} \nobreakspace
        \mathsf{with} \nobreakspace
        \squid_checkmatch {#2} {} {;}
      }
  }
\NewDocumentCommand \domatch {s O{t} m > {\SplitList{;}} m}
  { \squid_startmatch {\mathsf{match}} {#1} {#2} {#3} #4 }
\NewDocumentCommand \dofoldmatch {s O{t} m > {\SplitList{;}} m}
  { \squid_startmatch {\mathsf{fold}} {#1} {#2} {#3} #4 }
\NewDocumentCommand \doprimrec {s O{t} m m m m}
  { \squid_startmatch {\mathsf{primrec}} {#1} {#2} {#3}
      {\zero. {#4}}
      {\suc \nobreakspace {#5}. {#6}}
  }
\ExplSyntaxOff

%%% Substitution

\ExplSyntaxOn
\NewDocumentCommand \squid_subpart:nn {m m} {{#1} \mapsto {#2}}
\NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m}
  { \squid_subpart:nn #1 \squid_checksub
  }
\NewDocumentCommand \squid_checksub {O{\parallel} g}
  {
    \IfValueTF{#2}
      {#1 \squid_contsub:n {#2}}
      {]}
  }
\NewDocumentCommand \sub {m > {\SplitList{,}} m}
  { {#1} [ \squid_checksub [] #2
  }
\ExplSyntaxOff

\NewDocumentCommand\suball{mm}{{#1} [#2]}

%% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\ifacmart\else
  \maketitle{}
\fi

\begin{abstract}
\TODO{}
\end{abstract}

\ifacmart
  \maketitle{}
\fi

%% Body

\subfile{sec/intro.ltx}
\subfile{sec/systemt.ltx}
\subfile{sec/lang.ltx}
\subfile{sec/encoding.ltx}
\subfile{sec/reducer.ltx}
\subfile{sec/compiler.ltx}
\subfile{sec/related.ltx}

\printbibliography{}

\appendix

\end{document}