diff options
| -rw-r--r-- | sec/encoding.ltx | 32 |
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} |