diff options
| -rw-r--r-- | sec/encoding.ltx | 21 |
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 [] |