diff options
| -rw-r--r-- | sec/encoding.ltx | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index c5a311b..1078597 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -349,21 +349,20 @@ lists passed to \roll*{} have a static length making the \(\mathsf{max}\) operator easy to partially evaluate. After phase three, our example for \systemtinline{balanced} beta -reduces to the following: +reduces to the below. This example demonstrates both pattern matching +and indexing lists. In the \systemtinline{Suc} branch, the variable +\systemtinline{dh} stores the result of indexing the single list +\systemtinline{[(depth, heap)]}. \begin{listing}[H] \begin{systemt} let balanced n f = primrec n with - Zero => (1 , fun (length, idxs) => + Zero => (Suc Zero , fun (length, idxs) => if length == 0 then Leaf 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 Branch (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))) +| Suc (depth, heap) => (Suc depth, fun (length, idxs) => + if length == 0 then Branch (0, 0) else + let dh = if idxs 0 == 0 then (depth, heap) else arb in + snd dh (length - 1, fun i => idxs (Suc i))) \end{systemt} \vspace{-\baselineskip} \end{listing} |