list.bend source

list.bend on the hub · documented module

# bendlib-kernel-list: frozen step-list permutations over List, generic over -A: Data.# Frozen set: swap_head, swap_at, apply, perm_steps, perm; the bytes are the type identity (F3).import Base# Swap the first two elements (no-op on lists shorter than two).def swap_head(-A: Data, xs: List<&2, A>) -> List<&2, A>:  match xs:    case Nil{}:      Nil{}    case +x <> t:      match t:        case Nil{}:          x <> Nil{}        case +y <> u:          y <> x <> u# Swap positions i and i+1.def swap_at(-A: Data, +i: Nat, xs: List<&2, A>) -> List<&2, A>:  match i:    case 0n:      swap_head(A, xs)    case 1n+p:      match xs:        case Nil{}:          Nil{}        case +x <> t:          x <> swap_at(A, p, t)# Apply a list of adjacent swaps, left to right.def apply(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>) -> List<&2, A>:  match steps:    case Nil{}:      xs    case +i <> rest:      apply(A, rest, swap_at(A, i, xs))# The derivation `perm_steps(A, steps, xs, ys)` holds when `apply(A, steps, xs)` is `ys`.def perm_steps(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>, ys: List<&2, A>) -> Data:  {apply(A, steps, xs) == ys : List<&2, A>}# Some swap derivation carries `xs` to `ys` (the existential `perm`).def perm(-A: Data, xs: List<&2, A>, ys: List<&2, A>) -> Data:  Sigma<&2, &2, List<&2, Nat>, s => perm_steps(A, s, xs, ys)>