Define the final desugaring

1 files changed, 23 insertions, 9 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index b93ca8f..7bfa1cf 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -518,14 +518,28 @@ let dupfirst t = fun x => match x with
 \subsection{Phase 7: Desugaring}%
 \label{subsec:desugar}
 
-\TODO{
-  \begin{itemize}
-    \item state that we desugar other operators last
-    \item define desugaring of arb
-    \item define desugaring of case
-    \item define desugaring of map
-    \item define desugaring of let
-  \end{itemize}
-}
+This final phase of encoding performs desugaring; there are only a
+couple of remaining operations to encode. These include case splitting
+on a natural number; constructing an arbitrary value of a type; and
+\letkw{} expressions.
+
+We encode case splitting on a number by a chain of equality tests. If
+all the tests fail, we will return an arbitrary value. We can
+construct an arbitrary value at any type by using the function that
+constantly returns zero. Let expressions are given their usual
+functional decoding.
+
+The \systemtinline{dupfirst} example desugars into the following
+expression:
+\begin{listing}[H]
+\begin{systemt}
+let dupfirst t = fun x =>
+  if x == 0 then fun x y => t 0 x else
+  if x == 1 then fun x y => t 0 y else
+  if x == 2 then fun x y => t 1 0 else
+    fun x y => 0
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
 
 \end{document}