src/Myers.bend
bend-edit-distance@0.2.1.0 · 721 lines · 0 definitions
1import Base
2import bend-edit-distance@0.2.1.0/EdlibTypes.bend as E
3import bend-edit-distance@0.2.1.0/src/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
10type Peq is Data:
11 Mask{bits: U32}
12 Branch{low: Peq, high: Peq}
13
14type 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.
19type Carry is Data:
20 Carry{positive: U32, negative: U32}
21
22def split_query.prepend(h: Char, parts: String & String) -> String & String:
23 match parts:
24 case (prefix, suffix):
25 (SCon{h, prefix}, suffix)
26
27def 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.
38def 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.
50def 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
59def 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
70def 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
76def 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
83def ceil_div(+x: Nat, +y: Nat) -> Nat:
84 Nat.div(Nat.add(x, Nat.sub(y, 1n)), y)
85
86def 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.
95def 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.
114def 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
120def 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.
135def 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
143def 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.
155type BandEntry is Data:
156 BandEntry{profile: Peq, block: Block}
157
158type Band is Type:
159 Band{first: Nat, entries: List<&2, BandEntry>, rest: List<&2, Peq>}
160
161type UpdatedBand is Type:
162 UpdatedBand{entries: List<&2, BandEntry>, score: U32, carry: Carry, bottom: Nat}
163
164type 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.
169type Search is Data:
170 Search{distance: E.EditDistance, blocks: Nat, columns: Nat, attempts: Nat}
171
172def 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
178def 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
188def init_band.step(parts: List<&2, BandEntry> & List<&2, Peq>) -> Band:
189 match parts:
190 case (entries, rest):
191 Band{0n, entries, rest}
192
193def 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
200def 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
205def 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
210def 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
216def 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.
232def 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
238def 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
244def 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
252def 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
258def 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
269def 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
277def 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
290def 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
297def 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
303def 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
311def 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
324def 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
339def 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
346def 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
355def 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
367def 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
372def 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
384def 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
389def 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
397def 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
406def 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
419def 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
430def 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
439def 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.
453def semiglobal_carry(mode: E.Mode) -> Carry:
454 match mode:
455 case E.HW{}:
456 Carry{0, 0}
457 case _:
458 Carry{1, 0}
459
460def 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.
467def 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
481def reduce_semiglobal(parts: List<&2, BandEntry> & List<&2, Peq>) -> Band:
482 match parts:
483 case (entries, rest):
484 Band{0n, entries, rest}
485
486def 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
494def 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
504def 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
516def 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
522def 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
534def 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.
542def 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
557def 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
564def 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
571def 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.
583def 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
590def 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
596def 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.
608def 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
628def 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
644def 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
653def 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
660def 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
668def search_distance(search: Search) -> E.EditDistance:
669 match search:
670 case Search{distance, _, _, _}:
671 distance
672
673def found_value(distance: E.EditDistance) -> Nat:
674 match distance:
675 case E.Found{value}:
676 value
677 case E.NotFound{}:
678 0n
679
680def 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
685def 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
697def 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
707def 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
720def response(query: String, target: String) -> String:
721 Nat.show(distance(query, target))