shared/lists.bend
bend-lint-api@0.1.1.0 · 129 lines · 0 definitions
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.
3import Base
4
5def 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`.
13def 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
20def 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
23def 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
30def concat(a, -A: Kind(a), xss: List<a, List<a, A>>) -> List<a, A>:
31 concat.go(a, A, xss, [])
32
33def 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
40def length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
41 length.go(a, A, xs, 0n)
42
43def 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.
53def any(~A: Data, ~f: A -> Bool, xs: List<&2, A>) -> Bool:
54 any.go(~A, ~f, xs, False{})
55
56def 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
63def 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.
71def 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.
87def 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.
105def 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
110def 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.
128def deal(a, -A: Kind(a), xs: List<a, A>) -> List<a, A> & List<a, A>:
129 deal.go(a, A, xs, True{}, [], [])