shared/lists.bend

bend-lint-api@0.2.0.0 · 129 lines · 16 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{}, [], [])