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