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).
3	import Base
4	
5	# Swap the first two elements (no-op on lists shorter than two).
6	def 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.
18	def 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.
30	def 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`.
38	def 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`).
42	def 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)>