Give phase 3 examples.

1 files changed, 39 insertions, 0 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 525568d..482c7b0 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -255,6 +255,45 @@ eliminators.
   \end{itemize}
 }
 
+After phase three, our example for \systemtinline{balanced} beta
+reduces to the following:
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero              => (1 , fun (length, idxs) =>
+    match length with
+      Zero  => Leaf f
+    | Suc l => snd arb (l, fun i => idxs (1 + i)))
+| Suc (depth, heap) => (1 + max depth depth, fun (length, idxs) =>
+    match length with
+      Zero  => Branch (0, 1)
+    | Suc l =>
+        let dh = match idxs 0 with
+          Zero  => (depth, heap)
+        | Suc x => match x with
+            Zero  => (depth, heap)
+          | Suc x => arb
+        in snd (dh (l, fun i => idxs (1 + i))))
+\end{systemt}
+\end{listing}
+
+And \systemtinline{compose} reduces to:
+\begin{listing}[H]
+\begin{systemt}
+let compose (depth, heap) =
+  let go = primrec depth with
+    Zero   => arb
+  | Suc ih => fun (length, idxs) =>
+    let x = map (fun x => ih (1 + length, fun i =>
+                  if i == length then x else idxs i))
+                (heap (length, idxs))
+    in match x with
+      Leaf f        => f
+    | Branch (f, g) => fun x => f (g x)
+  in go
+\end{systemt}
+\end{listing}
+
 \subsection{Phase 4: Encoding Sums}%
 \label{subsec:sums}