diff options
author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-05-06 16:20:17 +0100 |
---|---|---|
committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-05-06 16:20:17 +0100 |
commit | 66037ec63a8f44250054d6b251323c35f21d5c39 (patch) | |
tree | 1ef3efa5e0317630cb9a1bf40ae1884809312c56 /sec/encoding.ltx | |
parent | 8c23267879b41a113f50b31678d1302ccbf90393 (diff) |
Give running examples for phase 4.
Diffstat (limited to 'sec/encoding.ltx')
-rw-r--r-- | sec/encoding.ltx | 46 |
1 files changed, 40 insertions, 6 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 5c4fe4e..14d8c94 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -383,12 +383,46 @@ We encode the injection into a sum \(\tuple{i, t}\) by the pair to take. The pattern match on the right will be desugared into a sequence of equality tests in phase seven. -\TODO{ - \begin{itemize} - \item justify adding union types - \item justify the case operator on naturals - \end{itemize} -} +Our two examples reduce even further. We obtain the following for +\systemtinline{balanced}: + +\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 + 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))) +\end{systemt} +\vspace{-\baselineskip} +\end{listing} + +The \systemtinline{compose} example demonstrates how pattern matching +is encoded: + +\begin{listing}[H] +\begin{systemt} +let compose (depth, heap) = + let go = primrec depth with + Zero => arb + | Suc ih => fun (length, idxs) => + let (tag, v) = map (fun x => ih (Suc length, fun i => + if i == length then x else idxs i)) + (heap (length, idxs)) + in match tag with + 0 => prj v 0 + | 1 => let (f, g) = prj v 1 in fun x => f (g x) + in go +\end{systemt} +\vspace{-\baselineskip} +\end{listing} \subsection{Phase 5: Encoding Products}% \label{subsec:products} |