Before the big rewrite

1 files changed, 261 insertions, 0 deletions

diff --git a/main.tex b/main.tex
new file mode 100644
index 0000000..e96270e
--- /dev/null
+++ b/main.tex
@@ -0,0 +1,261 @@
+\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,
+  giveninits,
+  doi,
+  eprint = false
+]{biblatex}   %% bibliography configuration
+\usepackage{booktabs} %% table formatting
+\usepackage{ebproof}  %% proof trees
+\usepackage{expl3}  %% Latex 3
+\usepackage{enumitem} %% format contributions list
+\usepackage{float}  %% forcing appendix figures
+\usepackage{hyperref} %% hyperlinks within document
+\usepackage{mathtools}  %% matrix alignment
+\usepackage[outputdir=build]{minted}  %% code formatting
+\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{ARTiST:\ Adding Regular Types in 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 -x'}{}
+\newmintinline[systemtinline]{'lexer.py:SystemTLexer -x'}{}
+
+% TODOS and such
+\newcommand\lang{{\color{Green} ARTiST}}
+\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
+\newcommand\judgement[4][]{{#2} \vdash^{#1} {#3} : {#4}}
+\newcommand\jdgmnt[3]{{#2} \vdash {#3}~\mathrm{#1}}
+
+%%% Term syntax
+
+%% Godel encoding
+\newcommand\encode[1]{\llcorner {#1} \lrcorner}
+
+%% Tuples
+\DeclarePairedDelimiter\tuple{\langle}{\rangle}
+\newcommand\lettm[3]{\mathsf{let}~{#1} \coloneq {#2}~\mathsf{in}~{#3}}
+
+%% Naturals
+\newcommand\nat{\mathsf{N}}
+\newcommand\zero{\ensuremath{\mathsf{zero}}}
+\newcommand\suc{\ensuremath{\mathsf{suc}}}
+
+\newcommand\primreckw{\ensuremath{\mathsf{primrec}}}
+\NewDocumentCommand\primrec{m m g}{%
+    \primreckw~{#1}~{#2}\IfValueT{#3}{~{#3}}%
+  }
+
+\newcommand\pairingkw{\ensuremath{\mathsf{pair}}}
+\NewDocumentCommand\pairing{m m}{%
+    \pairingkw~{#1}~{#2}%
+  }
+
+%% Functors
+\newcommand\mapkw{\ensuremath{\mathsf{map}}}
+% e.g. \maptm{X}{1 + X}
+\newcommand\maptm[2]{\mapkw_{\Lambda {#1}.{#2}}}
+
+%% Recursive types
+\newcommand\foldkw{\ensuremath{\mathsf{fold}}}
+\newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}}
+
+%% Sums
+\newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}}
+\newcommand\casetm[5]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{{#4}<{#5}}}}
+
+%%% 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}}
+  {
+   \peek_meaning_ignore_spaces:NTF \bgroup
+      {#1 \squid_contsub:n}
+      {]}
+  }
+\NewDocumentCommand \squid_startsub:n {m}
+  { {#1} [ \squid_checksub []
+  }
+\NewDocumentCommand \sub {m > {\SplitList{,}} m}
+  { \squid_startsub:n {#1} #2
+  }
+\ExplSyntaxOff
+
+%% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{document}
+
+\ifacmart\else
+  \maketitle{}
+\fi
+
+\begin{abstract}
+G\"odel's System T is a simple calculus that performs computation. The absence
+of any type abstractions, such as products or sums, along with the limited form
+of recursion makes using System T as a target language difficult. In this paper
+we introduce \lang{}, a new intermediate language. One can compile \lang{} into
+System~T using well-known type encodings, and we have written this algorithm
+within \lang{} itself. We also describe a compiler for \lang{} written in Idris
+2, featuring an intrinsically well-scoped AST and runtime-erased type-checking
+proofs.
+\end{abstract}
+
+\ifacmart
+  \maketitle{}
+\fi
+
+%% Body
+
+\subfile{sec/intro.ltx}
+\subfile{sec/systemt.ltx}
+\subfile{sec/lang.ltx}
+\subfile{sec/embedding.ltx}
+\subfile{sec/reducer.ltx}
+\subfile{sec/compiler.ltx}
+\subfile{sec/related.ltx}
+
+\printbibliography{}
+
+\appendix
+
+\end{document}