From 5c92cbf4246650a072bb3e5018e1607623abe2ef Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 15:02:34 +0100
Subject: Fix 663--666.

---
 sec/encoding.ltx | 65 ++++++++++++++++++++++++++++----------------------------
 1 file changed, 32 insertions(+), 33 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 2d32f30..45eb639 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -372,7 +372,7 @@ changes happened to the \systemtinline{update} function as it computes
 the \(\mathsf{snoc}\) on a given index.
 \begin{listing}[H]
 \begin{systemt}
-let compose' (depth, heap) =
+let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
@@ -396,60 +396,59 @@ encode the type \(\sum_{\ell \in I} A_\ell\) by the pair \(\nat \times \bigsqcup
 of a tag indicating the variant, and a union which can contain a value
 from any variant.
 
-Unions have two operators: \(\mathsf{inj}~i~t\) and
-\(\mathsf{prj}~t~i\) for injecting and projecting values at type
-\(A_i\) respectively. When the two operators have the same index,
+Unions have two operators: \(\mathsf{inj}~\ell~t\) and
+\(\mathsf{prj}~t~\ell\) for injecting and projecting values at type
+\(A_\ell\) respectively. When the two operators have the same label,
 unions have the beta reduction rule
-\(\mathsf{prj}~(\mathsf{inj}~i~t)~i = t\). If the two indices are
+\(\mathsf{prj}~(\mathsf{inj}~\ell~t)~\ell = t\). If the two labels are
 different then projection is stuck.
 
-We encode the injection into a sum \(\tuple{i, t}\) by the pair
-\(\tuple{i, \mathsf{inj}~i~t}\). We encode pattern matching
-\((\casetm{t}{\tuple{i,x_i}}{t_i}{i})\) by the term \(
-(\casetm{t.0}{i}{\sub{t_i}{x_i/\mathsf{prj}~t.1~i}}{i})
-\) performing a pattern match over the tag to find the correct branch
-to take. The pattern match on the right will be desugared into a
-sequence of equality tests in phase seven.
-
-\FIXME{these examples are hard to read}
+We encode the injection into a sum \(\ell~t\) by the pair \(\tuple{\ell,
+  \mathsf{inj}~\ell~t}\). We encode pattern matching
+\((\casetm{t}{\ell~x_\ell}{t_\ell}{\ell})\) by the term \(
+(\casetm{t.0}{\ell}{\sub{t_\ell}{x_\ell/\mathsf{prj}~t.1~\ell}}{\ell}) \) performing
+a pattern match over the tag to find the correct branch to take. The
+pattern match on the right will be desugared into a sequence of
+equality tests in phase seven.
 
 Our two examples reduce even further. We obtain the following for
-\systemtinline{balanced}:
+\systemtinline{balanced} after encoding \systemtinline{Leaf} and
+\systemtinline{Branch} as tagged unions.
 
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
-  Zero => (1, fun (length, idxs) =>
-    if length == 0 then (0 , inj 0 f) else
+  Zero => (Suc Zero, fun (length, idxs) =>
+    if length == 0 then (Leaf , inj 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 (1, inj 1 (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, inj 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}
 
-The \systemtinline{compose'} example demonstrates how pattern matching
-is encoded:
+The \systemtinline{compose} example demonstrates how pattern matching
+is encoded. We first pattern match on the tag and then project the
+payload into the corresponding type.
 
 \begin{listing}[H]
 \begin{systemt}
-let compose' (depth, heap) =
+let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun (length, idxs) =>
-    let update = fun i => ih (Suc length, fun j =>
-                   if j == length then i else idxs j)
+    let update =
+      fun i => ih (Suc length, fun j =>
+        if j == length then i else idxs j)
     let (tag, v) = heap (length, idxs) in
     match tag with
-      0 => update (prj v 0)
-    | 1 => let (i, j) = prj v 1 in fun x => update i (update j x)
-  in go
+      Leaf   => update (prj v Leaf)
+    | Branch =>
+        let (i, j) = prj v Branch in
+        fun x => update i (update j x)
+  in go (Zero, arb)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}
-- 
cgit v1.2.3

