From 7e4d615e90e5d5287c1ddbc7a33232736a0d8b7f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 30 May 2025 14:32:05 +0100
Subject: Summarise the compiler passes.

---
 sec/compiler.ltx | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index fad68d4..b4fde16 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -4,9 +4,31 @@
 \section{Idris 2 Compiler for Artyst}%
 \label{sec:compiler}
 
+To aid the development of the System~T reducer and encoding
+algorithms, we have implemented a type checker and compiler for
+\lang{}. The compiler is written in Idris~2~\cite{idris}, a
+dependently typed programming language. The compiler is split into
+three main components:
+\begin{itemize}
+  \item First we have a parser based on \textcite{alg-parsing}. The
+    parser interface guarantees that we process the input without
+    backtracking. This produces an intrinsically-well-scoped abstract
+    syntax tree.
+
+  \item Second we perform type checking using a bidirectional
+    algorithm~\cite{bidir}. Along with the usual type checking result,
+    the algorithm produces a runtime-erased proof that the term is
+    well-typed.
+
+  \item Finally we compile the term to Guile~Scheme~\cite{guile}. By
+    requiring an erased well-typedness proof, the compiler can
+    statically guarantee it will only ever have to process well-typed
+    terms.
+\end{itemize}
+
+
 \TODO{
   \begin{itemize}
-    \item describe that I have a type checker and compiler implemented in Idris
     \item explain what intentionally well-scoped syntax is
     \item justify why I used intentionally well-scoped syntax
     \item describe how type checking produces a derivation
-- 
cgit v1.2.3