1	import Base
2	import ../EdlibTypes.bend as E
3	import ./Alignment.bend as A
4	
5	# The distance paths from vendor/edlib/edlib/src/edlib.cpp. Bend's native
6	# integer is U32, so a Myers word covers 32 query characters instead of 64.
7	# The scalar helper is NW, unit costs, unlimited distance (k = -1). The
8	# configured API extends it with the typed modes/tasks in EdlibTypes.bend.
9	
10	type Peq is Data:
11	  Mask{bits: U32}
12	  Branch{low: Peq, high: Peq}
13	
14	type Block is Data:
15	  Block{positive: U32, negative: U32, score: U32}
16	
17	# Horizontal differences are -1, 0, or +1. Keep both signs explicit rather
18	# than relying on signed shifts or two's-complement arithmetic.
19	type Carry is Data:
20	  Carry{positive: U32, negative: U32}
21	
22	def split_query.prepend(h: Char, parts: String & String) -> String & String:
23	  match parts:
24	    case (prefix, suffix):
25	      (SCon{h, prefix}, suffix)
26	
27	def split_query(n: Nat, query: String) -> String & String:
28	  match n query:
29	    case 0n _:
30	      ("", query)
31	    case 1n+p SNil{}:
32	      ("", "")
33	    case 1n+p SCon{h, t}:
34	      split_query.prepend(h, split_query(p, t))
35	
36	# Bit i matches query[i] literally or through an explicit symmetric pair.
37	# Unused high bits are wildcards regardless of the pairs, as in buildPeq.
38	def build_peq_word(query: String, +symbol: Char, +bit: U32,
39	                   +pairs: List<&2, E.EqualityPair>) -> U32:
40	  match query:
41	    case SNil{}:
42	      U32.not(U32.sub(bit, 1))
43	    case SCon{h, t}:
44	      (U32.mul(Bool.to_u32(E.equal(pairs, h, symbol)), bit) .|.
45	        build_peq_word(t, symbol, U32.shl(bit), pairs) : U32)
46	
47	# A byte-indexed immutable table replaces the C++ transformed alphabet.
48	# Low bits select branches, so lookup takes eight steps for every byte.
49	# Both halves of the table have equal, independent work and run in parallel.
50	def build_peq_table(+depth: Nat, +query: String, +symbol: U32, +step: U32,
51	                    +pairs: List<&2, E.EqualityPair>) -> Peq:
52	  match depth:
53	    case 0n:
54	      Mask{build_peq_word(query, Chr{symbol}, 1, pairs)}
55	    case 1n+p:
56	      low high = build_peq_table(p, query, symbol, U32.shl(step), pairs) build_peq_table(p, query, U32.add(symbol, step), U32.shl(step), pairs)
57	      Branch{low, high}
58	
59	def peq_get(table: Peq, +code: U32, bit: Bool) -> U32:
60	  match table bit:
61	    case Mask{bits} _:
62	      bits
63	    case Branch{low, high} True{}:
64	      +next = U32.shr(code)
65	      peq_get(high, next, U32.is_ne(U32.and(next, 1), 0))
66	    case Branch{low, high} False{}:
67	      +next = U32.shr(code)
68	      peq_get(low, next, U32.is_ne(U32.and(next, 1), 0))
69	
70	def build_peq.step(parts: String & String, pairs: List<&2, E.EqualityPair>,
71	                   tail: String -> List<&2, Peq>) -> List<&2, Peq>:
72	  match parts:
73	    case (word, rest):
74	      build_peq_table(8n, word, 0, 1, pairs) <> tail(rest)
75	
76	def build_peq(fuel: Nat, query: String, +pairs: List<&2, E.EqualityPair>) -> List<&2, Peq>:
77	  match fuel:
78	    case 0n:
79	      Nil{}
80	    case 1n+p:
81	      build_peq.step(split_query(32n, query), pairs, rest => build_peq(p, rest, pairs))
82	
83	def ceil_div(+x: Nat, +y: Nat) -> Nat:
84	  Nat.div(Nat.add(x, Nat.sub(y, 1n)), y)
85	
86	def init_blocks(n: Nat, +bottom: U32) -> List<Block>:
87	  match n:
88	    case 0n:
89	      Nil{}
90	    case 1n+p:
91	      Block{4294967295, 0, bottom} <> init_blocks(p, U32.add(bottom, 32))
92	
93	# calculateBlock / Advance_Block from Myers. Addition intentionally wraps
94	# at 32 bits. Xv uses the original Eq, before the negative carry is added.
95	def calculate_block(block: Block, +eq: U32, hin: Carry) -> Block & Carry:
96	  Block{+pv, +mv, score} = block
97	  Carry{hin_positive, +hin_negative} = hin
98	  +xv = U32.or(eq, mv)
99	  +eq_in = U32.or(eq, hin_negative)
100	  +xh = (U32.xor(U32.add(U32.and(eq_in, pv), pv), pv) .|. eq_in : U32)
101	  +ph = U32.or(mv, U32.not(U32.or(xh, pv)))
102	  +mh = U32.and(pv, xh)
103	  +hout_positive = U32.shrn(ph, 31n)
104	  +hout_negative = U32.shrn(mh, 31n)
105	  +ph_shifted = U32.or(U32.shl(ph), hin_positive)
106	  mh_shifted = U32.or(U32.shl(mh), hin_negative)
107	  next_pv = U32.or(mh_shifted, U32.not(U32.or(xv, ph_shifted)))
108	  next_mv = U32.and(ph_shifted, xv)
109	  (Block{next_pv, next_mv, U32.sub(U32.add(score, hout_positive), hout_negative)},
110	    Carry{hout_positive, hout_negative})
111	
112	# A column and consecutive target columns depend on their predecessor;
113	# parallelizing those calls would violate the Myers carry dependency.
114	def advance_column.step(result: Block & Carry,
115	                        tail: Carry -> List<Block>) -> List<Block>:
116	  match result:
117	    case (next, hout):
118	      next <> tail(hout)
119	
120	def advance_column(blocks: List<Block>, profiles: List<&2, Peq>, +symbol: U32,
121	                   hin: Carry) -> List<Block>:
122	  match blocks profiles:
123	    case Nil{} _:
124	      Nil{}
125	    case _ Nil{}:
126	      Nil{}
127	    case block <> rest profile <> tail:
128	      advance_column.step(
129	        calculate_block(block, peq_get(profile, symbol, U32.is_ne(U32.and(symbol, 1), 0)), hin),
130	        hout => advance_column(rest, tail, symbol, hout))
131	
132	# getBlockCellValues(block)[W], without constructing the other 31 cells.
133	# Walking up a row subtracts its positive vertical difference and adds its
134	# negative difference. W is always in 0..31, never a whole extra block.
135	def get_block_cell_value(padding: Nat, +pv: U32, +mv: U32, score: U32) -> U32:
136	  match padding:
137	    case 0n:
138	      score
139	    case 1n+p:
140	      get_block_cell_value(p, U32.shl(pv), U32.shl(mv),
141	        U32.add(U32.sub(score, U32.shrn(pv, 31n)), U32.shrn(mv, 31n)))
142	
143	def last_block_score(blocks: List<Block>, +padding: Nat) -> Nat:
144	  match blocks:
145	    case Nil{}:
146	      0n
147	    case Block{pv, mv, score} <> Nil{}:
148	      U32.to_nat(get_block_cell_value(padding, pv, mv, score))
149	    case _ <> rest:
150	      last_block_score(rest, padding)
151	
152	# An active entry owns its current block and shares its immutable profile.
153	# Dropped leading entries are never visited again. Trailing profiles remain
154	# available for expansion; retries share the full profile but reset all blocks.
155	type BandEntry is Data:
156	  BandEntry{profile: Peq, block: Block}
157	
158	type Band is Type:
159	  Band{first: Nat, entries: List<&2, BandEntry>, rest: List<&2, Peq>}
160	
161	type UpdatedBand is Type:
162	  UpdatedBand{entries: List<&2, BandEntry>, score: U32, carry: Carry, bottom: Nat}
163	
164	type BandStep is Type:
165	  BandStep{band: Band, maximum: Nat, work: Nat}
166	
167	# Work counts actual calculate_block calls, consumed columns and fresh attempts.
168	# The probe uses these production counters to verify pruning and retry behavior.
169	type Search is Data:
170	  Search{distance: E.EditDistance, blocks: Nat, columns: Nat, attempts: Nat}
171	
172	def init_band_entries.step(parts: List<&2, BandEntry> & List<&2, Peq>,
173	                           profile: Peq, bottom: U32) -> List<&2, BandEntry> & List<&2, Peq>:
174	  match parts:
175	    case (entries, rest):
176	      (BandEntry{profile, Block{4294967295, 0, bottom}} <> entries, rest)
177	
178	def init_band_entries(fuel: Nat, profiles: List<&2, Peq>,
179	                      +bottom: U32) -> List<&2, BandEntry> & List<&2, Peq>:
180	  match fuel profiles:
181	    case 0n _:
182	      (Nil{}, profiles)
183	    case _ Nil{}:
184	      (Nil{}, Nil{})
185	    case 1n+p profile <> tail:
186	      init_band_entries.step(init_band_entries(p, tail, U32.add(bottom, 32)), profile, bottom)
187	
188	def init_band.step(parts: List<&2, BandEntry> & List<&2, Peq>) -> Band:
189	  match parts:
190	    case (entries, rest):
191	      Band{0n, entries, rest}
192	
193	def init_band(profiles: List<&2, Peq>, +length: Nat, +target_length: Nat,
194	              maximum: Nat) -> Band:
195	  # Called only after k >= target_length - length, with length <= target_length.
196	  count = Nat.min(ceil_div(length, 32n),
197	    ceil_div(1n+Nat.div(Nat.sub(maximum, Nat.sub(target_length, length)), 2n), 32n))
198	  init_band.step(init_band_entries(count, profiles, 32))
199	
200	def advance_band.join(entry: BandEntry, updated: UpdatedBand) -> UpdatedBand:
201	  match updated:
202	    case UpdatedBand{entries, score, carry, bottom}:
203	      UpdatedBand{entry <> entries, score, carry, bottom}
204	
205	def advance_band.last(result: Block & Carry, profile: Peq, bottom: Nat) -> UpdatedBand:
206	  match result:
207	    case (Block{+pv, +mv, +score}, carry):
208	      UpdatedBand{[BandEntry{profile, Block{pv, mv, score}}], score, carry, bottom}
209	
210	def advance_band.next(result: Block & Carry, profile: Peq,
211	                      tail: Carry -> UpdatedBand) -> UpdatedBand:
212	  match result:
213	    case (next, carry):
214	      advance_band.join(BandEntry{profile, next}, tail(carry))
215	
216	def advance_band(entries: List<&2, BandEntry>, +symbol: U32,
217	                 hin: Carry, +bottom: Nat) -> UpdatedBand:
218	  match entries:
219	    case Nil{}:
220	      UpdatedBand{Nil{}, 0, Carry{1, 0}, bottom}
221	    case BandEntry{+profile, block} <> Nil{}:
222	      advance_band.last(calculate_block(block,
223	        peq_get(profile, symbol, U32.is_ne(U32.and(symbol, 1), 0)), hin), profile, bottom)
224	    case BandEntry{+profile, block} <> tail:
225	      advance_band.next(calculate_block(block,
226	        peq_get(profile, symbol, U32.is_ne(U32.and(symbol, 1), 0)), hin), profile,
227	        carry => advance_band(tail, symbol, carry, Nat.add(bottom, 32n)))
228	
229	# Edlib's conservative Ukkonen block bounds, rearranged so every term is
230	# nonnegative Nat arithmetic. Rows/columns here count consumed characters.
231	# The 62/63 constants adapt 2*WORD_SIZE-2/-1 from the pinned 64-bit code.
232	def band_keep_last(+score: Nat, bottom: Nat, +maximum: Nat,
233	                   length: Nat, target_length: Nat, column: Nat) -> Bool:
234	  Bool.and(Nat.is_lt(score, Nat.add(maximum, 32n)),
235	    Nat.is_le(Nat.add(Nat.add(bottom, score), target_length),
236	      Nat.add(Nat.add(Nat.add(maximum, length), column), 63n)))
237	
238	def band_keep_first(+score: Nat, bottom: Nat, +maximum: Nat,
239	                    length: Nat, target_length: Nat, column: Nat) -> Bool:
240	  Bool.and(Nat.is_lt(score, Nat.add(maximum, 32n)),
241	    Nat.is_ge(Nat.add(Nat.add(bottom, maximum), target_length),
242	      Nat.add(Nat.add(score, length), column)))
243	
244	def trim_last.choose(entry: BandEntry, entries: List<&2, BandEntry>, rest: List<&2, Peq>,
245	                     keep: Bool) -> List<&2, BandEntry> & List<&2, Peq>:
246	  match entry entries keep:
247	    case BandEntry{profile, _} Nil{} False{}:
248	      (Nil{}, profile <> rest)
249	    case _ _ _:
250	      (entry <> entries, rest)
251	
252	def trim_last.join(entry: BandEntry, tail: List<&2, BandEntry> & List<&2, Peq>,
253	                   keep: Bool) -> List<&2, BandEntry> & List<&2, Peq>:
254	  match tail:
255	    case (entries, rest):
256	      trim_last.choose(entry, entries, rest, keep)
257	
258	def trim_last(entries: List<&2, BandEntry>, rest: List<&2, Peq>, +bottom: Nat,
259	              +maximum: Nat, +length: Nat, +target_length: Nat,
260	              +column: Nat) -> List<&2, BandEntry> & List<&2, Peq>:
261	  match entries:
262	    case Nil{}:
263	      (Nil{}, rest)
264	    case BandEntry{profile, Block{pv, mv, +score}} <> tail:
265	      trim_last.join(BandEntry{profile, Block{pv, mv, score}},
266	        trim_last(tail, rest, Nat.add(bottom, 32n), maximum, length, target_length, column),
267	        band_keep_last(U32.to_nat(score), bottom, maximum, length, target_length, column))
268	
269	def trim_first.step(entry: BandEntry, tail: List<&2, BandEntry>, rest: List<&2, Peq>,
270	                    first: Nat, keep: Bool, next: Unit -> Band) -> Band:
271	  match keep:
272	    case True{}:
273	      Band{first, entry <> tail, rest}
274	    case False{}:
275	      next(Unit{})
276	
277	def trim_first(entries: List<&2, BandEntry>, +rest: List<&2, Peq>, +first: Nat,
278	               +maximum: Nat, +length: Nat, +target_length: Nat,
279	               +column: Nat) -> Band:
280	  match entries:
281	    case Nil{}:
282	      Band{first, Nil{}, rest}
283	    case BandEntry{profile, Block{pv, mv, +score}} <> +tail:
284	      trim_first.step(BandEntry{profile, Block{pv, mv, score}}, tail, rest,
285	        first,
286	        band_keep_first(U32.to_nat(score), Nat.mul(1n+first, 32n),
287	          maximum, length, target_length, column),
288	        _ => trim_first(tail, rest, 1n+first, maximum, length, target_length, column))
289	
290	def reduce_band.step(parts: List<&2, BandEntry> & List<&2, Peq>, first: Nat,
291	                     +maximum: Nat, length: Nat, target_length: Nat,
292	                     column: Nat, work: Nat) -> BandStep:
293	  match parts:
294	    case (entries, rest):
295	      BandStep{trim_first(entries, rest, first, maximum, length, target_length, column), maximum, work}
296	
297	def reduce_band(entries: List<&2, BandEntry>, rest: List<&2, Peq>, +first: Nat,
298	                +maximum: Nat, +length: Nat, +target_length: Nat,
299	                +column: Nat, work: Nat) -> BandStep:
300	  reduce_band.step(trim_last(entries, rest, Nat.mul(1n+first, 32n),
301	    maximum, length, target_length, column), first, maximum, length, target_length, column, work)
302	
303	def expand_band.step(result: Block & Carry, entries: List<&2, BandEntry>, profile: Peq,
304	                     rest: List<&2, Peq>, first: Nat, maximum: Nat, length: Nat,
305	                     target_length: Nat, column: Nat, work: Nat) -> BandStep:
306	  match result:
307	    case (block, _):
308	      reduce_band(List.append(&2, BandEntry, entries, [BandEntry{profile, block}]),
309	        rest, first, maximum, length, target_length, column, 1n+work)
310	
311	def expand_band(entries: List<&2, BandEntry>, rest: List<&2, Peq>, +score: U32,
312	                carry: Carry, +symbol: U32, first: Nat, +maximum: Nat,
313	                length: Nat, target_length: Nat, column: Nat,
314	                work: Nat, expand: Bool) -> BandStep:
315	  match rest carry expand:
316	    case +profile <> tail Carry{+positive, +negative} True{}:
317	      previous = U32.add(U32.sub(U32.add(score, negative), positive), 32)
318	      expand_band.step(calculate_block(Block{4294967295, 0, previous},
319	        peq_get(profile, symbol, U32.is_ne(U32.and(symbol, 1), 0)), Carry{positive, negative}),
320	        entries, profile, tail, first, maximum, length, target_length, column, work)
321	    case _ _ _:
322	      reduce_band(entries, rest, first, maximum, length, target_length, column, work)
323	
324	def band_step.updated(updated: UpdatedBand, rest: List<&2, Peq>, +first: Nat,
325	                      symbol: U32, +length: Nat, +target_length: Nat,
326	                      +column: Nat, maximum: Nat, padding: Nat) -> BandStep:
327	  match updated:
328	    case UpdatedBand{entries, +score, carry, +bottom}:
329	      # Completing the suffix by edits bounds the optimum. Padding can lower
330	      # the stored bottom score, so add it back before tightening k.
331	      +k = Nat.min(maximum, Nat.add(U32.to_nat(score),
332	        Nat.add(Nat.max(Nat.sub(target_length, column), Nat.sub(length, bottom)),
333	          Bool.pick(Nat, Nat.is_ge(bottom, length), padding, 0n))))
334	      work = Nat.sub(Nat.div(bottom, 32n), first)
335	      expand_band(entries, rest, score, carry, symbol, first, k, length, target_length,
336	        column, work, Nat.is_le(Nat.add(Nat.add(bottom, U32.to_nat(score)), target_length),
337	          Nat.add(Nat.add(Nat.add(k, length), column), 62n)))
338	
339	def band_step(band: Band, +symbol: U32, length: Nat, target_length: Nat,
340	              column: Nat, maximum: Nat, padding: Nat) -> BandStep:
341	  match band:
342	    case Band{+first, entries, rest}:
343	      band_step.updated(advance_band(entries, symbol, Carry{1, 0}, Nat.mul(1n+first, 32n)),
344	        rest, first, symbol, length, target_length, column, maximum, padding)
345	
346	def band_last_score(entries: List<&2, BandEntry>, +padding: Nat) -> Nat:
347	  match entries:
348	    case Nil{}:
349	      0n
350	    case BandEntry{_, Block{pv, mv, score}} <> Nil{}:
351	      U32.to_nat(get_block_cell_value(padding, pv, mv, score))
352	    case _ <> tail:
353	      band_last_score(tail, padding)
354	
355	def band_finish(band: Band, maximum: Nat, padding: Nat,
356	                blocks: Nat, columns: Nat) -> Search:
357	  match band:
358	    case Band{_, Nil{}, _}:
359	      Search{E.NotFound{}, blocks, columns, 1n}
360	    case Band{_, entries, Nil{}}:
361	      +score = band_last_score(entries, padding)
362	      Search{Bool.pick(E.EditDistance, Nat.is_le(score, maximum), E.Found{score}, E.NotFound{}),
363	        blocks, columns, 1n}
364	    case _:
365	      Search{E.NotFound{}, blocks, columns, 1n}
366	
367	def myers_calc_edit_distance_nw.step(step: BandStep, next: Band -> Nat -> Nat -> Search) -> Search:
368	  match step:
369	    case BandStep{band, maximum, work}:
370	      next(band, maximum, work)
371	
372	def myers_calc_edit_distance_nw(target: String, band: Band, +length: Nat, +target_length: Nat,
373	                                maximum: Nat, +padding: Nat, +column: Nat, blocks: Nat) -> Search:
374	  match target band:
375	    case _ Band{_, Nil{}, _}:
376	      Search{E.NotFound{}, blocks, column, 1n}
377	    case SNil{} _:
378	      band_finish(band, maximum, padding, blocks, column)
379	    case SCon{h, t} _:
380	      myers_calc_edit_distance_nw.step(band_step(band, Char.to_u32(h), length, target_length,
381	        1n+column, maximum, padding), next => k => work =>
382	          myers_calc_edit_distance_nw(t, next, length, target_length, k, padding, 1n+column, Nat.add(blocks, work)))
383	
384	def band_attempt(target: String, profiles: List<&2, Peq>, +length: Nat,
385	                 +target_length: Nat, +maximum: Nat, padding: Nat) -> Search:
386	  myers_calc_edit_distance_nw(target, init_band(profiles, length, target_length, maximum),
387	    length, target_length, maximum, padding, 0n, 0n)
388	
389	def adaptive_search.step(distance: E.EditDistance, blocks: Nat, columns: Nat,
390	                         attempts: Nat, retry: Unit -> Search) -> Search:
391	  match distance:
392	    case E.Found{value}:
393	      Search{E.Found{value}, blocks, columns, attempts}
394	    case E.NotFound{}:
395	      retry(Unit{})
396	
397	def adaptive_search.result(search: Search, blocks: Nat, columns: Nat, +attempts: Nat,
398	                           retry: Nat -> Nat -> Search) -> Search:
399	  match search:
400	    case Search{distance, work, consumed, _}:
401	      +next_blocks = Nat.add(blocks, work)
402	      +next_columns = Nat.add(columns, consumed)
403	      adaptive_search.step(distance, next_blocks, next_columns, 1n+attempts,
404	        _ => retry(next_blocks, next_columns))
405	
406	def adaptive_search(fuel: Nat, +target: String, +profiles: List<&2, Peq>,
407	                    +length: Nat, +target_length: Nat, +maximum: Nat,
408	                    +padding: Nat, +blocks: Nat, +columns: Nat,
409	                    +attempts: Nat) -> Search:
410	  match fuel:
411	    case 0n:
412	      Search{E.NotFound{}, blocks, columns, attempts}
413	    case 1n+p:
414	      adaptive_search.result(band_attempt(target, profiles, length, target_length, maximum, padding),
415	        blocks, columns, attempts, bs => cs =>
416	          adaptive_search(p, target, profiles, length, target_length,
417	            Nat.min(target_length, Nat.mul(maximum, 2n)), padding, bs, cs, 1n+attempts))
418	
419	def search_profiles(target: String, profiles: List<&2, Peq>, +length: Nat,
420	                    +target_length: Nat, threshold: E.Threshold) -> Search:
421	  match threshold:
422	    case E.MaxDistance{maximum}:
423	      band_attempt(target, profiles, length, target_length, Nat.min(maximum, target_length),
424	        Nat.sub(Nat.mul(ceil_div(length, 32n), 32n), length))
425	    case E.Unlimited{}:
426	      adaptive_search(1n+target_length, target, profiles, length, target_length,
427	        Nat.min(target_length, Nat.max(32n, Nat.sub(target_length, length))),
428	        Nat.sub(Nat.mul(ceil_div(length, 32n), 32n), length), 0n, 0n, 0n)
429	
430	def search_query(+query: String, target: String, +length: Nat, target_length: Nat,
431	                 threshold: E.Threshold, pairs: List<&2, E.EqualityPair>,
432	                 rejected: Bool) -> Search:
433	  match rejected:
434	    case True{}:
435	      Search{E.NotFound{}, 0n, 0n, 0n}
436	    case False{}:
437	      search_profiles(target, build_peq(ceil_div(length, 32n), query, pairs), length, target_length, threshold)
438	
439	def search_shorter(query: String, target: String, +query_length: Nat,
440	                   +target_length: Nat, +threshold: E.Threshold,
441	                   query_is_shorter: Bool, pairs: List<&2, E.EqualityPair>) -> Search:
442	  match query_is_shorter:
443	    case True{}:
444	      search_query(query, target, query_length, target_length, threshold, pairs,
445	        Bool.not(E.within_threshold(threshold, Nat.sub(target_length, query_length))))
446	    case False{}:
447	      search_query(target, query, target_length, query_length, threshold, pairs,
448	        Bool.not(E.within_threshold(threshold, Nat.sub(query_length, target_length))))
449	
450	# Directional modes never swap query and target. The initial vertical scores
451	# are i in both modes, while the top horizontal difference is +1 for SHW and
452	# 0 for HW. NW's length/remaining-target band bounds do not apply here.
453	def semiglobal_carry(mode: E.Mode) -> Carry:
454	  match mode:
455	    case E.HW{}:
456	      Carry{0, 0}
457	    case _:
458	      Carry{1, 0}
459	
460	def init_semiglobal_band(profiles: List<&2, Peq>, length: Nat, +maximum: Nat) -> Band:
461	  init_band.step(init_band_entries(
462	    Nat.min(ceil_div(length, 32n), ceil_div(1n+maximum, 32n)), profiles, 32))
463	
464	# If the bottom score is >= k+32 every cell in that block is > k. Only
465	# trailing blocks are removed. HW always retains block zero: its free top
466	# boundary can seed a new alignment after an arbitrarily long target prefix.
467	def trim_semiglobal(entries: List<&2, BandEntry>, rest: List<&2, Peq>,
468	                    +mode: E.Mode, +index: Nat, +maximum: Nat) -> List<&2, BandEntry> & List<&2, Peq>:
469	  match entries mode:
470	    case Nil{} _:
471	      (Nil{}, rest)
472	    case BandEntry{profile, Block{pv, mv, +score}} <> tail E.HW{}:
473	      trim_last.join(BandEntry{profile, Block{pv, mv, score}},
474	        trim_semiglobal(tail, rest, mode, 1n+index, maximum),
475	        Bool.or(Nat.is_eq(index, 0n), Nat.is_lt(U32.to_nat(score), Nat.add(maximum, 32n))))
476	    case BandEntry{profile, Block{pv, mv, +score}} <> tail _:
477	      trim_last.join(BandEntry{profile, Block{pv, mv, score}},
478	        trim_semiglobal(tail, rest, mode, 1n+index, maximum),
479	        Nat.is_lt(U32.to_nat(score), Nat.add(maximum, 32n)))
480	
481	def reduce_semiglobal(parts: List<&2, BandEntry> & List<&2, Peq>) -> Band:
482	  match parts:
483	    case (entries, rest):
484	      Band{0n, entries, rest}
485	
486	def expand_semiglobal.result(result: Block & Carry, entries: List<&2, BandEntry>,
487	                              profile: Peq, rest: List<&2, Peq>, mode: E.Mode,
488	                              maximum: Nat) -> Band:
489	  match result:
490	    case (block, _):
491	      reduce_semiglobal(trim_semiglobal(
492	        List.append(&2, BandEntry, entries, [BandEntry{profile, block}]), rest, mode, 0n, maximum))
493	
494	def expand_semiglobal.choose(entries: List<&2, BandEntry>, profile: Peq,
495	                             rest: List<&2, Peq>, previous: U32, eq: U32,
496	                             carry: Carry, mode: E.Mode, maximum: Nat, expand: Bool) -> Band:
497	  match expand:
498	    case True{}:
499	      expand_semiglobal.result(calculate_block(Block{4294967295, 0, U32.add(previous, 32)}, eq, carry),
500	        entries, profile, rest, mode, maximum)
501	    case False{}:
502	      reduce_semiglobal(trim_semiglobal(entries, profile <> rest, mode, 0n, maximum))
503	
504	def expand_semiglobal(updated: UpdatedBand, rest: List<&2, Peq>, +symbol: U32,
505	                       mode: E.Mode, +maximum: Nat) -> Band:
506	  match updated rest:
507	    case UpdatedBand{entries, +score, Carry{+positive, +negative}, _} +profile <> tail:
508	      +previous = U32.sub(U32.add(score, negative), positive)
509	      +eq = peq_get(profile, symbol, U32.is_ne(U32.and(symbol, 1), 0))
510	      expand_semiglobal.choose(entries, profile, tail, previous, eq, Carry{positive, negative}, mode, maximum,
511	        Bool.and(Nat.is_le(U32.to_nat(previous), maximum),
512	          Bool.or(U32.is_ne(U32.and(eq, 1), 0), U32.is_ne(negative, 0))))
513	    case UpdatedBand{entries, _, _, _} Nil{}:
514	      reduce_semiglobal(trim_semiglobal(entries, Nil{}, mode, 0n, maximum))
515	
516	def semiglobal_step(band: Band, +symbol: U32, +mode: E.Mode, maximum: Nat) -> Band:
517	  match band:
518	    case Band{_, entries, rest}:
519	      expand_semiglobal(advance_band(entries, symbol, semiglobal_carry(mode), 32n),
520	        rest, symbol, mode, maximum)
521	
522	def semiglobal_endpoint(entries: List<&2, BandEntry>, rest: List<&2, Peq>, padding: Nat,
523	                         column: Nat, +best: A.Best) -> A.Best:
524	  match entries rest:
525	    case Nil{} _:
526	      best
527	    case _ Nil{}:
528	      A.Best{old, _} = best
529	      +score = U32.from_nat(band_last_score(entries, padding))
530	      A.update_best(best, score, A.Location{E.Position{column}, 0n}, U32.cmp(score, old))
531	    case _ _:
532	      best
533	
534	def myers_calc_edit_distance_semiglobal.step(band: Band, padding: Nat, column: Nat,
535	                                             best: A.Best, next: Band -> A.Best -> A.Best) -> A.Best:
536	  match band:
537	    case Band{first, +entries, +rest}:
538	      next(Band{first, entries, rest}, semiglobal_endpoint(entries, rest, padding, column, best))
539	
540	# Decode the real last query cell at every column, without Edlib's delayed
541	# padded endpoints. Tighten k after a better score, but continue for every tie.
542	def myers_calc_edit_distance_semiglobal(target: String, band: Band, +mode: E.Mode,
543	                                         +padding: Nat, +column: Nat, +maximum: Nat,
544	                                         +best: A.Best) -> A.Best:
545	  match target band:
546	    case _ Band{_, Nil{}, _}:
547	      A.ordered(best)
548	    case SNil{} _:
549	      A.ordered(best)
550	    case SCon{h, t} _:
551	      A.Best{score, _} = best
552	      +k = Nat.min(maximum, U32.to_nat(score))
553	      myers_calc_edit_distance_semiglobal.step(semiglobal_step(band, Char.to_u32(h), mode, k),
554	        padding, column, best, next => found =>
555	          myers_calc_edit_distance_semiglobal(t, next, mode, padding, 1n+column, k, found))
556	
557	def semiglobal_initial_best(+length: Nat, include_before: Bool) -> A.Best:
558	  match include_before:
559	    case True{}:
560	      A.Best{U32.from_nat(length), [A.Location{E.BeforeStart{}, 0n}]}
561	    case False{}:
562	      A.Best{4294967295, Nil{}}
563	
564	def semiglobal_maximum(threshold: E.Threshold, +length: Nat) -> Nat:
565	  match threshold:
566	    case E.Unlimited{}:
567	      length
568	    case E.MaxDistance{maximum}:
569	      Nat.min(maximum, length)
570	
571	def semiglobal_best(target: String, profiles: List<&2, Peq>, +length: Nat,
572	                      +maximum: Nat, +mode: E.Mode) -> A.Best:
573	  +count = ceil_div(length, 32n)
574	  # Preserve pinned Edlib's 64-bit column-zero convention independently of
575	  # this implementation's 32-bit padding (especially lengths 32 and 96).
576	  best = semiglobal_initial_best(length, Nat.is_ne(Nat.mod(length, 64n), 0n))
577	  myers_calc_edit_distance_semiglobal(target,
578	    init_semiglobal_band(profiles, length, maximum), mode,
579	    Nat.sub(Nat.mul(count, 32n), length), 0n, maximum, best)
580	
581	# Edlib selects the LAST optimal reverse-SHW end, hence the earliest start
582	# for each forward end. Preserve the special forward end -1 with start 0.
583	def hw_start(+end: Nat, reverse_location: A.Location) -> A.Location:
584	  match reverse_location:
585	    case A.Location{E.BeforeStart{}, _}:
586	      A.Location{E.Position{end}, 1n+end}
587	    case A.Location{E.Position{reverse_end}, _}:
588	      A.Location{E.Position{end}, Nat.sub(end, reverse_end)}
589	
590	def hw_start_best(+end: Nat, best: A.Best) -> A.Location:
591	  match best:
592	    case A.Best{_, locations}:
593	      hw_start(end, Maybe.default(&2, A.Location,
594	        List.last(&2, A.Location, locations), A.Location{E.BeforeStart{}, 0n}))
595	
596	def hw_location(location: A.Location, reverse_target: String, target_length: Nat,
597	                  profiles: List<&2, Peq>, query_length: Nat, maximum: Nat) -> A.Location:
598	  match location:
599	    case A.Location{E.BeforeStart{}, _}:
600	      A.Location{E.BeforeStart{}, 0n}
601	    case A.Location{E.Position{+end}, _}:
602	      hw_start_best(end, semiglobal_best(
603	        String.drop(reverse_target, Nat.sub(target_length, 1n+end)),
604	        profiles, query_length, maximum, E.SHW{}))
605	
606	# Independent starts share one reversed query profile. Split their searches
607	# into balanced parallel branches, then concatenate in the original end order.
608	def hw_locations(fuel: Nat, locations: List<&2, A.Location>,
609	                   +reverse_target: String, +target_length: Nat,
610	                   +profiles: List<&2, Peq>, +query_length: Nat,
611	                   +maximum: Nat) -> List<&2, A.Location>:
612	  match fuel locations:
613	    case 0n _:
614	      locations
615	    case 1n+p Nil{}:
616	      Nil{}
617	    case 1n+p location <> Nil{}:
618	      [hw_location(location, reverse_target, target_length, profiles, query_length, maximum)]
619	    case Succ{+p} +values:
620	      +half = Nat.div(List.length(&2, A.Location, values), 2n)
621	      left right =
622	        hw_locations(p, List.take(&2, A.Location, values, half),
623	          reverse_target, target_length, profiles, query_length, maximum)
624	        hw_locations(p, List.drop(&2, A.Location, values, half),
625	          reverse_target, target_length, profiles, query_length, maximum)
626	      List.append(&2, A.Location, left, right)
627	
628	def configured_found(task: E.Task, mode: E.Mode, +query: String, +target: String,
629	                        +pairs: List<&2, E.EqualityPair>, format: E.CigarFormat,
630	                        best: A.Best) -> E.AlignResult:
631	  match task mode best:
632	    case E.Distance{} _ _:
633	      A.result(query, target, task, pairs, format, best, True{})
634	    case _ E.HW{} A.Best{+score, +locations}:
635	      +qn +tn = String.length(query) String.length(target)
636	      rq rt = String.reverse(query) String.reverse(target)
637	      resolved = hw_locations(List.length(&2, A.Location, locations), locations,
638	        rt, tn, build_peq(ceil_div(qn, 32n), rq, pairs), qn, U32.to_nat(score))
639	      A.result(query, target, task, pairs, format, A.Best{score, resolved}, True{})
640	    case _ _ _:
641	      # NW/SHW always start at zero; only PATH needs reconstruction.
642	      A.result(query, target, task, pairs, format, best, True{})
643	
644	def configured_result(query: String, target: String, mode: E.Mode, task: E.Task,
645	                         pairs: List<&2, E.EqualityPair>, format: E.CigarFormat,
646	                         best: A.Best, accepted: Bool) -> E.AlignResult:
647	  match accepted:
648	    case False{}:
649	      E.not_found()
650	    case True{}:
651	      configured_found(task, mode, query, target, pairs, format, best)
652	
653	def configured_finish(query: String, target: String, mode: E.Mode, task: E.Task,
654	                         threshold: E.Threshold, pairs: List<&2, E.EqualityPair>,
655	                         format: E.CigarFormat, +best: A.Best) -> E.AlignResult:
656	  A.Best{score, _} = best
657	  configured_result(query, target, mode, task, pairs, format, best,
658	    E.within_threshold(threshold, U32.to_nat(score)))
659	
660	def semiglobal_align(+query: String, +target: String, +mode: E.Mode, task: E.Task,
661	                       +threshold: E.Threshold, +pairs: List<&2, E.EqualityPair>,
662	                       format: E.CigarFormat) -> E.AlignResult:
663	  +length = String.length(query)
664	  configured_finish(query, target, mode, task, threshold, pairs, format,
665	    semiglobal_best(target, build_peq(ceil_div(length, 32n), query, pairs),
666	      length, semiglobal_maximum(threshold, length), mode))
667	
668	def search_distance(search: Search) -> E.EditDistance:
669	  match search:
670	    case Search{distance, _, _, _}:
671	      distance
672	
673	def found_value(distance: E.EditDistance) -> Nat:
674	  match distance:
675	    case E.Found{value}:
676	      value
677	    case E.NotFound{}:
678	      0n
679	
680	def align_shorter(query: String, target: String, query_length: Nat,
681	                  target_length: Nat, query_is_shorter: Bool) -> Nat:
682	  found_value(search_distance(search_shorter(query, target, query_length,
683	    target_length, E.Unlimited{}, query_is_shorter, Nil{})))
684	
685	def distance(query: String, target: String) -> Nat:
686	  match query target:
687	    case SNil{} _:
688	      String.length(target)
689	    case SCon{h, t} SNil{}:
690	      1n+String.length(t)
691	    case SCon{qh, qt} SCon{th, tt}:
692	      +q = {SCon{qh, qt} : String}
693	      +t = {SCon{th, tt} : String}
694	      +qn +tn = String.length(q) String.length(t)
695	      align_shorter(q, t, qn, tn, Nat.is_le(qn, tn))
696	
697	def nw_result(query: String, target: String, task: E.Task,
698	                 pairs: List<&2, E.EqualityPair>, format: E.CigarFormat,
699	                 end: E.Coordinate, distance: E.EditDistance) -> E.AlignResult:
700	  match distance:
701	    case E.NotFound{}:
702	      E.not_found()
703	    case E.Found{score}:
704	      configured_result(query, target, E.NW{}, task, pairs, format,
705	        A.Best{U32.from_nat(score), [A.Location{end, 0n}]}, True{})
706	
707	def edlib_align(query: String, target: String, config: E.AlignConfig) -> E.AlignResult:
708	  match query target config:
709	    case SNil{} _ _:
710	      A.empty_result("", target, config)
711	    case SCon{h, t} SNil{} _:
712	      A.empty_result(SCon{h, t}, "", config)
713	    case +q +t E.AlignConfig{E.NW{}, task, threshold, +pairs, format}:
714	      +qn +tn = String.length(q) String.length(t)
715	      nw_result(q, t, task, pairs, format, E.end_coordinate(tn),
716	        search_distance(search_shorter(q, t, qn, tn, threshold, Nat.is_le(qn, tn), pairs)))
717	    case +q +t E.AlignConfig{mode, task, threshold, pairs, format}:
718	      semiglobal_align(q, t, mode, task, threshold, pairs, format)
719	
720	def response(query: String, target: String) -> String:
721	  Nat.show(distance(query, target))