1	# List helpers. They recurse only in tail position, so a long list is fine on the JS lane, whose stack is small;
2	# Base's append, concat, length, any and sort recurse on the stack.
3	import Base
4	
5	def when(-A: Data, hit: Bool, v: A) -> Maybe<&2, A>:
6	  match hit:
7	    case True{}:
8	      Some{v}
9	    case False{}:
10	      None{}
11	
12	# `xs`, last first, onto `out`.
13	def onto(a, -A: Kind(a), xs: List<a, A>, out: List<a, A>) -> List<a, A>:
14	  match xs:
15	    case Nil{}:
16	      out
17	    case Con{h, t}:
18	      onto(a, A, t, h <> out)
19	
20	def append(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>:
21	  onto(a, A, List.reverse(a, A, xs), ys)
22	
23	def concat.go(a, -A: Kind(a), xss: List<a, List<a, A>>, out: List<a, A>) -> List<a, A>:
24	  match xss:
25	    case Nil{}:
26	      List.reverse(a, A, out)
27	    case Con{xs, rest}:
28	      concat.go(a, A, rest, onto(a, A, xs, out))
29	
30	def concat(a, -A: Kind(a), xss: List<a, List<a, A>>) -> List<a, A>:
31	  concat.go(a, A, xss, [])
32	
33	def length.go(a, -A: Kind(a), xs: List<a, A>, n: Nat) -> Nat:
34	  match xs:
35	    case Nil{}:
36	      n
37	    case Con{h, t}:
38	      length.go(a, A, t, 1n+n)
39	
40	def length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
41	  length.go(a, A, xs, 0n)
42	
43	def any.go(~A: Data, ~f: A -> Bool, xs: List<&2, A>, found: Bool) -> Bool:
44	  match xs found:
45	    case _ True{}:
46	      True{}
47	    case Nil{} False{}:
48	      False{}
49	    case Con{h, t} False{}:
50	      any.go(~A, ~f, t, f(h))
51	
52	# Whether `f` holds for some `x` of `xs`; it stops at the first.
53	def any(~A: Data, ~f: A -> Bool, xs: List<&2, A>) -> Bool:
54	  any.go(~A, ~f, xs, False{})
55	
56	def push(-A: Data, x: Maybe<&2, A>, out: List<&2, A>) -> List<&2, A>:
57	  match x:
58	    case Some{v}:
59	      v <> out
60	    case None{}:
61	      out
62	
63	def sort.runs(-A: Data, xs: List<&2, A>, out: List<&2, List<&2, A>>) -> List<&2, List<&2, A>>:
64	  match xs:
65	    case Nil{}:
66	      List.reverse(&2, List<&2, A>, out)
67	    case Con{h, t}:
68	      sort.runs(A, t, [h] <> out)
69	
70	# One pass: each two runs merged, in order.
71	def sort.pass(
72	  ~A: Data,
73	  ~le: A -> A -> Bool,
74	  +n: Nat,
75	  runs: List<&2, List<&2, A>>,
76	  out: List<&2, List<&2, A>>
77	) -> List<&2, List<&2, A>>:
78	  match runs:
79	    case Nil{}:
80	      List.reverse(&2, List<&2, A>, out)
81	    case Con{r, Nil{}}:
82	      List.reverse(&2, List<&2, A>, r <> out)
83	    case Con{r1, Con{r2, rest}}:
84	      sort.pass(~A, ~le, n, rest, List.merge.go(~A, ~le, n, (Nil{}, r1, r2)) <> out)
85	
86	# Passes until one run is left; each pass halves the runs, so `fuel` (the length) is more than enough.
87	def sort.go(
88	  ~A: Data,
89	  ~le: A -> A -> Bool,
90	  fuel: Nat,
91	  +n: Nat,
92	  runs: List<&2, List<&2, A>>
93	) -> List<&2, A>:
94	  match fuel runs:
95	    case _ Nil{}:
96	      []
97	    case _ Con{r, Nil{}}:
98	      r
99	    case 0n _:
100	      concat(&2, A, runs)
101	    case 1n+f _:
102	      sort.go(~A, ~le, f, n, sort.pass(~A, ~le, n, runs, []))
103	
104	# `xs` in `le` order, stable: a bottom-up merge sort.
105	def sort(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>) -> List<&2, A>:
106	  +ys = {xs: List<&2, A>}
107	  +n = length(&2, A, ys)
108	  sort.go(~A, ~le, n, n, sort.runs(A, ys, []))
109	
110	def deal.go(
111	  a,
112	  -A: Kind(a),
113	  xs: List<a, A>,
114	  even: Bool,
115	  l: List<a, A>,
116	  r: List<a, A>
117	) -> List<a, A>
118	  & List<a, A>:
119	  match xs even:
120	    case Nil{} _:
121	      (List.reverse(a, A, l), List.reverse(a, A, r))
122	    case Con{h, t} True{}:
123	      deal.go(a, A, t, False{}, h <> l, r)
124	    case Con{h, t} False{}:
125	      deal.go(a, A, t, True{}, l, h <> r)
126	
127	# `xs` dealt into two halves, each in order: those at even positions, and those at odd ones.
128	def deal(a, -A: Kind(a), xs: List<a, A>) -> List<a, A> & List<a, A>:
129	  deal.go(a, A, xs, True{}, [], [])