diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/compiler.ltx | 24 |
1 files changed, 23 insertions, 1 deletions
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 |