scan.bend
bend-parallel@0.1.0.0 · 234 lines · 25 definitions
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34import Base
35
36
37
38
39
40
41def sum.go(+n: Nat, +j: U32, +s: U32, r: Array<U32> & U32) -> Array<U32> & U32:
42 match n:
43 case 0n:
44 (a, +x) = r
45 (a, (s + x : U32))
46 case 1n+p:
47 (a, +x) = r
48 +q = (j + 1 : U32)
49 sum.go(p, q, (s + x : U32), a[q])
50
51
52
53
54def ex.go(+n: Nat, +j: U32, +s: U32, r: Array<U32> & U32) -> Array<U32> & U32:
55 match n:
56 case 0n:
57 (a, +x) = r
58 (a[j] <- s, (s + x : U32))
59 case 1n+p:
60 (a, +x) = r
61 +q = (j + 1 : U32)
62 ex.go(p, q, (s + x : U32), (a[j] <- s)[q])
63
64
65def in.go(+n: Nat, +j: U32, +s: U32, r: Array<U32> & U32) -> Array<U32> & U32:
66 match n:
67 case 0n:
68 (a, +x) = r
69 +t = (s + x : U32)
70 (a[j] <- t, t)
71 case 1n+p:
72 (a, +x) = r
73 +q = (j + 1 : U32)
74 +t = (s + x : U32)
75 in.go(p, q, t, (a[j] <- t)[q])
76
77
78def go(+inc: Bool, +n: Nat, +j: U32, +s: U32, r: Array<U32> & U32) -> Array<U32> & U32:
79 match inc:
80 case False{}:
81 ex.go(n, j, s, r)
82 case True{}:
83 in.go(n, j, s, r)
84
85
86
87
88type Two is Type:
89 Two{a: Array<U32>, s: Array<U32>}
90
91def two.join(l: Two, r: Two) -> Two:
92 Two{la, ls} = l
93 Two{ra, rs} = r
94 Two{Array.join(U32, la, ra), Array.join(U32, ls, rs)}
95
96
97def two.rejoin(a2: Array<U32>, s2: Array<U32>, r: Two) -> Two:
98 Two{a, s} = r
99 Two{Array.join(U32, a, a2), Array.join(U32, s, s2)}
100
101
102
103
104def sums.leaf.fin(+i: U32, s: Array<U32>, r: Array<U32> & U32) -> Two:
105 (a, +v) = r
106 Two{a, s[i] <- v}
107
108
109def sums.leaf(+i: U32, +e: Nat, a: Array<U32>, s: Array<U32>) -> Two:
110 +at = U32.shln(i, e)
111 sums.leaf.fin(i, s, sum.go(U32.to_nat((U32.shln(1, e) - 1 : U32)), at, 0, a[at]))
112
113
114
115
116def sums(+d: Nat, +i: U32, +e: Nat, fa: Array<U32> & Array<U32>, fs: Array<U32> & Array<U32>) -> Two:
117 match d:
118 case 0n:
119 (a, a2) = fa
120 (s, s2) = fs
121 two.rejoin(a2, s2, sums.leaf(i, e, a, s))
122 case 1n+p:
123 (a0, a1) = fa
124 (s0, s1) = fs
125 +j = (i * 2 : U32)
126 l r = sums(p, j, e, Array.fork(U32, a0), Array.fork(U32, s0))
127 sums(p, (j + 1 : U32), e, Array.fork(U32, a1), Array.fork(U32, s1))
128 two.join(l, r)
129
130
131
132
133def puts.leaf.fin(s: Array<U32>, r: Array<U32> & U32) -> Two:
134 (a, +t) = r
135 Two{a, s}
136
137def puts.leaf.at(+inc: Bool, +i: U32, +e: Nat, a: Array<U32>, r: Array<U32> & U32) -> Two:
138 (s, +base) = r
139 +at = U32.shln(i, e)
140 puts.leaf.fin(s, go(inc, U32.to_nat((U32.shln(1, e) - 1 : U32)), at, base, a[at]))
141
142
143def puts.leaf(+inc: Bool, +i: U32, +e: Nat, a: Array<U32>, s: Array<U32>) -> Two:
144 puts.leaf.at(inc, i, e, a, s[i])
145
146
147
148def puts(+inc: Bool, +d: Nat, +i: U32, +e: Nat, fa: Array<U32> & Array<U32>, fs: Array<U32> & Array<U32>) -> Two:
149 match d:
150 case 0n:
151 (a, a2) = fa
152 (s, s2) = fs
153 two.rejoin(a2, s2, puts.leaf(inc, i, e, a, s))
154 case 1n+p:
155 (a0, a1) = fa
156 (s0, s1) = fs
157 +j = (i * 2 : U32)
158 l r = puts(inc, p, j, e, Array.fork(U32, a0), Array.fork(U32, s0))
159 puts(inc, p, (j + 1 : U32), e, Array.fork(U32, a1), Array.fork(U32, s1))
160 two.join(l, r)
161
162
163
164
165
166def half(+d: Nat) -> Nat:
167 match d:
168 case 0n:
169 0n
170 case 1n+p:
171 match p:
172 case 0n:
173 0n
174 case 1n+q:
175 1n+half(q)
176
177def run.fin(r: Two, +total: U32) -> Array<U32> & U32:
178 Two{a, s} = r
179 (a, total)
180
181
182def run.mid(+inc: Bool, +d: Nat, +e: Nat, a: Array<U32>, r: Array<U32> & U32) -> Array<U32> & U32:
183 (s, +total) = r
184 run.fin(puts(inc, d, 0, e, Array.fork(U32, a), Array.fork(U32, s)), total)
185
186
187def run.pre(+d: Nat, +e: Nat, a: Array<U32>) -> Two:
188 sums(d, 0, e, Array.fork(U32, a), Array.fork(U32, Array.new(U32, d, 0)))
189
190
191def run0.sums(+inc: Bool, +d: Nat, +e: Nat, r: Two) -> Array<U32> & U32:
192 Two{a, s} = r
193 run.mid(inc, d, e, a, ex.go(U32.to_nat((U32.shln(1, d) - 1 : U32)), 0, 0, s[0]))
194
195def run0(+inc: Bool, +b: Nat, r: Array<U32> & U32) -> Array<U32> & U32:
196 (a, +n) = r
197 +lg = U32.log2(n)
198 +d = Nat.min(b, lg)
199 +e = Nat.sub(lg, d)
200 run0.sums(inc, d, e, run.pre(d, e, a))
201
202
203def run1.sums(+inc: Bool, +d: Nat, +e: Nat, r: Two) -> Array<U32> & U32:
204 Two{a, s} = r
205 run.mid(inc, d, e, a, run0(False{}, half(d), Array.size(U32, s)))
206
207
208
209
210def run.pick(lo: Bool, +inc: Bool, +d: Nat, +e: Nat, r: Two) -> Array<U32> & U32:
211 match lo:
212 case True{}:
213 run0.sums(inc, d, e, r)
214 case False{}:
215 run1.sums(inc, d, e, r)
216
217def run(+inc: Bool, +b: Nat, r: Array<U32> & U32) -> Array<U32> & U32:
218 (a, +n) = r
219 +lg = U32.log2(n)
220 +d = Nat.min(b, lg)
221 +e = Nat.sub(lg, d)
222 run.pick(U32.is_lt(U32.from_nat(d), 12), inc, d, e, run.pre(d, e, a))
223
224
225
226
227
228
229def exclusive(+b: Nat, a: Array<U32>) -> Array<U32> & U32:
230 run(False{}, b, Array.size(U32, a))
231
232
233def inclusive(+b: Nat, a: Array<U32>) -> Array<U32> & U32:
234 run(True{}, b, Array.size(U32, a))