Current state of affairs.

1 files changed, 107 insertions, 29 deletions

diff --git a/main.tex b/main.tex
index e96270e..c2eaafe 100644
--- a/main.tex
+++ b/main.tex
@@ -37,6 +37,7 @@
 \usepackage{hyperref} %% hyperlinks within document
 \usepackage{mathtools}  %% matrix alignment
 \usepackage[outputdir=build]{minted}  %% code formatting
+\usepackage{pifont} %% Check and cross marks
 \usepackage{stackrel} %% Annotating judgements
 \usepackage{subcaption} %% subfigures with captions
 \usepackage{subfiles} %% splitting file into sections
@@ -166,40 +167,127 @@
 
 %%% Term syntax
 
-%% Godel encoding
+%% Let
+\newcommand\letkw{\ensuremath{\mathsf{let}}}
+\newcommand\lettm[3]{\letkw~{#2} \coloneq {#1}~\mathsf{in}~{#3}}
+\ExplSyntaxOn
+\NewDocumentCommand \squid_letpart {m m}
+  { \letkw & {#1} = \cr
+    & {#2} \cr
+    \mathsf{in} &
+  }
+\NewDocumentCommand \squid_contlet {> {\SplitArgument{1}{=}} m}
+  { \squid_letpart #1 \squid_checklet [\cr]
+  }
+\NewDocumentCommand \squid_checklet {o s m}
+  { \IfBooleanTF{#2}
+      { \IfNoValueF{#1}{#1} & {#3}
+        \end{array}
+        \wlog{End~let}
+      }
+      { \IfNoValueF{#1}{#1} \squid_contlet {#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\tuple{\langle}{\rangle}
-\newcommand\lettm[3]{\mathsf{let}~{#1} \coloneq {#2}~\mathsf{in}~{#3}}
 
 %% Naturals
-\newcommand\nat{\mathsf{N}}
+\newcommand\nat{\ensuremath{\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}%
-  }
+\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
+\newcommand\roll{\ensuremath{\mathsf{roll}}}
+\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[5]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{{#4}<{#5}}}}
+\newcommand\casetm[4]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{#4}}}
+
+\ExplSyntaxOn
+\NewDocumentCommand \squid_matchpart:nn {m m m}
+  { \IfBooleanT{#1}{\quad} \tuple{#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
@@ -207,17 +295,14 @@
 \NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m}
   { \squid_subpart:nn #1 \squid_checksub
   }
-\NewDocumentCommand \squid_checksub {O{\parallel}}
+\NewDocumentCommand \squid_checksub {O{\parallel} g}
   {
-   \peek_meaning_ignore_spaces:NTF \bgroup
-      {#1 \squid_contsub:n}
+    \IfValueTF{#2}
+      {#1 \squid_contsub:n {#2}}
       {]}
   }
-\NewDocumentCommand \squid_startsub:n {m}
-  { {#1} [ \squid_checksub []
-  }
 \NewDocumentCommand \sub {m > {\SplitList{,}} m}
-  { \squid_startsub:n {#1} #2
+  { {#1} [ \squid_checksub [] #2
   }
 \ExplSyntaxOff
 
@@ -230,14 +315,7 @@
 \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.
+\TODO{}
 \end{abstract}
 
 \ifacmart
@@ -249,9 +327,9 @@ proofs.
 \subfile{sec/intro.ltx}
 \subfile{sec/systemt.ltx}
 \subfile{sec/lang.ltx}
-\subfile{sec/embedding.ltx}
-\subfile{sec/reducer.ltx}
+\subfile{sec/encoding.ltx}
 \subfile{sec/compiler.ltx}
+\subfile{sec/reducer.ltx}
 \subfile{sec/related.ltx}
 
 \printbibliography{}