Give running examples for phase 4.

1 files changed, 40 insertions, 6 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 5c4fe4e..14d8c94 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -383,12 +383,46 @@ We encode the injection into a sum \(\tuple{i, t}\) by the pair
 to take. The pattern match on the right will be desugared into a
 sequence of equality tests in phase seven.
 
-\TODO{
-  \begin{itemize}
-    \item justify adding union types
-    \item justify the case operator on naturals
-  \end{itemize}
-}
+Our two examples reduce even further. We obtain the following for
+\systemtinline{balanced}:
+
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero => (1, fun (length, idxs) =>
+    if length == 0 then (0 , inj 0 f) else
+      snd arb (length - 1, fun i => idxs (Suc i)))
+| Suc (depth, heap) => (Suc ((depth - depth) + depth), fun (length, idxs) =>
+  if length == 0 then (1, inj 1 (0, 1)) else
+    let x = idxs 0 in
+    let dh =
+      if     x == 0 then (depth, heap) else
+      if x - 1 == 0 then (depth, heap) else
+        arb
+    in snd dh (length - 1, fun i => idxs (Suc i)))
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
+The \systemtinline{compose} example demonstrates how pattern matching
+is encoded:
+
+\begin{listing}[H]
+\begin{systemt}
+let compose (depth, heap) =
+  let go = primrec depth with
+    Zero   => arb
+  | Suc ih => fun (length, idxs) =>
+    let (tag, v) = map (fun x => ih (Suc length, fun i =>
+                         if i == length then x else idxs i))
+                       (heap (length, idxs))
+    in match tag with
+      0 => prj v 0
+    | 1 => let (f, g) = prj v 1 in fun x => f (g x)
+  in go
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
 
 \subsection{Phase 5: Encoding Products}%
 \label{subsec:products}