From 8c5d117581230548fc23110d2d6095762306adf7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 18:06:58 +0100
Subject: Fix pseudocode.

- Make `arb` a keyword.
- Correct argument order to `map`.
---
 lexer.py         | 12 +++++++++++-
 sec/encoding.ltx |  4 ++--
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/lexer.py b/lexer.py
index 6963b77..cdce839 100644
--- a/lexer.py
+++ b/lexer.py
@@ -9,7 +9,17 @@ class SystemTLexer(OcamlLexer):
     aliases = ['syst']
     filenames = ['*.syst']
 
-    EXTRA_KEYWORDS = ['primrec', 'fold', 'foldmatch', 'roll', 'roll2']
+    EXTRA_KEYWORDS = [
+        'arb',
+        'arb)',
+        'fold',
+        'foldmatch',
+        'map',
+        'max',
+        'primrec',
+        'roll',
+        'roll2',
+    ]
 
     def get_tokens_unprocessed(self, text):
         for index, token, value in OcamlLexer.get_tokens_unprocessed(self, text):
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 8de40c4..dc3f8c8 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -158,7 +158,7 @@ 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}.
+\cref{fig:phase-2-encode}. 
 
 \TODO{
   \begin{itemize}
@@ -194,7 +194,7 @@ let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun index =>
-    let x = map (heap index) (fun x => ih (snoc xs x)) in
+    let x = map (fun x => ih (snoc xs x)) (heap index) in
     match x with
       Leaf f        => f
     | Branch (f, g) => fun x => f (g x)
-- 
cgit v1.2.3