list.bend

bendlib-kernel-list@1.0.0.0 · 43 lines · 5 definitions

1# bendlib-kernel-list: frozen step-list permutations over List, generic over -A: Data.
2# Frozen set: swap_head, swap_at, apply, perm_steps, perm; the bytes are the type identity (F3).
3import Base
4
5# Swap the first two elements (no-op on lists shorter than two).
6def swap_head(-A: Data, xs: List<&2, A>) -> List<&2, A>:
7  match xs:
8    case Nil{}:
9      Nil{}
10    case +x <> t:
11      match t:
12        case Nil{}:
13          x <> Nil{}
14        case +y <> u:
15          y <> x <> u
16
17# Swap positions i and i+1.
18def swap_at(-A: Data, +i: Nat, xs: List<&2, A>) -> List<&2, A>:
19  match i:
20    case 0n:
21      swap_head(A, xs)
22    case 1n+p:
23      match xs:
24        case Nil{}:
25          Nil{}
26        case +x <> t:
27          x <> swap_at(A, p, t)
28
29# Apply a list of adjacent swaps, left to right.
30def apply(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>) -> List<&2, A>:
31  match steps:
32    case Nil{}:
33      xs
34    case +i <> rest:
35      apply(A, rest, swap_at(A, i, xs))
36
37# The derivation `perm_steps(A, steps, xs, ys)` holds when `apply(A, steps, xs)` is `ys`.
38def perm_steps(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>, ys: List<&2, A>) -> Data:
39  {apply(A, steps, xs) == ys : List<&2, A>}
40
41# Some swap derivation carries `xs` to `ys` (the existential `perm`).
42def perm(-A: Data, xs: List<&2, A>, ys: List<&2, A>) -> Data:
43  Sigma<&2, &2, List<&2, Nat>, s => perm_steps(A, s, xs, ys)>