summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-04-29 18:06:58 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-04-29 18:06:58 +0100
commit8c5d117581230548fc23110d2d6095762306adf7 (patch)
tree161efd1f8eae74a13bc17ec2d3dfafd89069ca2d
parent2d033819b2666f92e90a91d8284768097fa0ee79 (diff)
Fix pseudocode.
- Make `arb` a keyword. - Correct argument order to `map`.
-rw-r--r--lexer.py12
-rw-r--r--sec/encoding.ltx4
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)