diff options
| -rw-r--r-- | sec/encoding.ltx | 11 |
1 files changed, 4 insertions, 7 deletions
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} |