From 415ab5c2062d534e23fbe6182f29db65f0b0be82 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 30 Apr 2025 13:57:08 +0100
Subject: Make phase 2 `balanced` use `index`.

---
 sec/encoding.ltx | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index bf2c96e..b00213a 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -158,13 +158,14 @@ index of the given child.
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
 We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}. We add three new operators for working with
+\cref{fig:phase-2-encode}. We add four new operators for working with
 lists:
 \begin{description}
   \item[\(\mathsf{max}\)] for calculating the maximum from a list of
     naturals;
   \item[\(\mathsf{snoc}\)] for appending a single item to the end of a
     list;
+  \item[\(\mathsf{index}\)] for retrieving an item from a list;
   \item[\(\mathsf{match}\)] for pattern matching on a list.
 \end{description}
 Computing the maximum value from a list is necessary to correctly
@@ -197,15 +198,11 @@ let balanced n f = primrec n with
   Zero              => (1, fun xs =>
     match xs with
       []      => Leaf f
-    | x :: xs => match x with
-      _ => arb)
+    | x :: xs => snd (index [] x) xs)
 | Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
     match xs with
       []      => Branch (0, 1)
-    | x :: xs => match x with
-        0 => heap xs
-      | 1 => heap xs
-      | _ => arb)
+    | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
-- 
cgit v1.2.3

