Fix 540--568.

1 files changed, 12 insertions, 9 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index f2ace28..9ffe418 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -229,8 +229,11 @@ let balanced n f = primrec n with
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
-
-And here is the updated value of \systemtinline{compose}:
+And below is the updated value of \systemtinline{compose}. In the
+\systemtinline{Suc} branch, the \systemtinline{update} function
+recursively looks up a pointer in the result map. The value
+\systemtinline{x} is the result of mapping \systemtinline{update}
+through the payload at \systemtinline{index}.
 \begin{listing}[H]
 \begin{systemt}
 let compose (depth, heap) =
@@ -238,7 +241,7 @@ let compose (depth, heap) =
     Zero   => arb
   | Suc ih => fun index =>
     let update = fun i => ih (snoc index i) in
-    let x = match heap (length, idxs) with
+    let x = match heap index with
       Leaf i        => Leaf (update i)
     | Branch (i, j) => Branch (update i, update j)
     in match x with
@@ -249,19 +252,19 @@ let compose (depth, heap) =
 \vspace{-\baselineskip}
 \end{listing}
 
-To keep our example small, we will perform a commuting conversion
-within \systemtinline{compose} to reduce the two match statements into
-one. After some further beta reductions, we obtain the simplified
-defintion
+Again to keep our example small, we will perform a commuting
+conversion within the \systemtinline{Suc} branch to combine the two
+match statements into one. After some further beta reductions, we
+obtain the simplified definition
 
 \begin{listing}[H]
 \begin{systemt}
-let compose' (depth, heap) =
+let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun index =>
     let update = fun i => ih (snoc index i) in
-    match heap (length, idxs) with
+    match heap index with
       Leaf i        => update i
     | Branch (i, j) => fun x => update i (update j x)
   in go []