src/DistanceDP.bend

bend-edit-distance@0.2.2.0 · 175 lines · 19 definitions

1import Base
2import bend-edit-distance@0.2.2.0/EdlibTypes.bend as E
3
4# Independent Levenshtein distance with unit edit costs.
5# Keep only the previous and current rows. NW uses min(m,n)+1 cells;
6# directional modes retain target columns and use n+1 cells.
7# The CLI caps each input at 4096 characters before calling either algorithm.
8
9def initial_row(length: Nat, +column: U32) -> List<U32>:
10  match length:
11    case 0n:
12      [column]
13    case 1n+p:
14      column <> initial_row(p, U32.add(column, 1))
15
16# D[i,j] = min(D[i-1,j] + 1, D[i,j-1] + 1,
17#              D[i-1,j-1] + !equal(pairs, row_symbol, column_symbol)).
18def cell(above: U32, left: U32, diagonal: U32,
19         row_symbol: Char, column_symbol: Char,
20         pairs: List<&2, E.EqualityPair>) -> U32:
21  U32.min(U32.min(U32.add(above, 1), U32.add(left, 1)),
22    U32.add(diagonal, Bool.to_u32(Bool.not(E.equal(pairs, row_symbol, column_symbol)))))
23
24# Consume the old row as the new row is built. The left/diagonal dependency
25# makes adjacent cells sequential; copying a full matrix is unnecessary.
26def row_cells(columns: String, previous: List<U32>, diagonal: U32,
27              left: U32, +symbol: Char, +pairs: List<&2, E.EqualityPair>) -> List<U32>:
28  match columns previous:
29    case SNil{} _:
30      Nil{}
31    case SCon{h, t} Nil{}:
32      Nil{}
33    case SCon{h, t} +above <> rest:
34      +next = cell(above, left, diagonal, symbol, h, pairs)
35      next <> row_cells(t, rest, above, next, symbol, pairs)
36
37def next_row(previous: List<U32>, columns: String, symbol: Char,
38             +index: U32, pairs: List<&2, E.EqualityPair>) -> List<U32>:
39  match previous:
40    case Nil{}:
41      [index]
42    case diagonal <> rest:
43      index <> row_cells(columns, rest, diagonal, index, symbol, pairs)
44
45def last_cell(row: List<U32>) -> Nat:
46  match row:
47    case Nil{}:
48      0n
49    case value <> Nil{}:
50      U32.to_nat(value)
51    case _ <> rest:
52      last_cell(rest)
53
54def rows(sequence: String, +columns: String, previous: List<U32>,
55         +index: U32, +pairs: List<&2, E.EqualityPair>) -> Nat:
56  match sequence:
57    case SNil{}:
58      last_cell(previous)
59    case SCon{h, t}:
60      rows(t, columns, next_row(previous, columns, h, index, pairs), U32.add(index, 1), pairs)
61
62def distance_shorter(query: String, target: String, query_length: Nat,
63                     target_length: Nat, query_is_shorter: Bool,
64                     pairs: List<&2, E.EqualityPair>) -> Nat:
65  match query_is_shorter:
66    case True{}:
67      rows(target, query, initial_row(query_length, 0), 1, pairs)
68    case False{}:
69      rows(query, target, initial_row(target_length, 0), 1, pairs)
70
71# Public entry point: importing this module does not import or call Myers.
72def distance_with_equalities(query: String, target: String,
73                             pairs: List<&2, E.EqualityPair>) -> Nat:
74  match query target:
75    case SNil{} _:
76      String.length(target)
77    case SCon{h, t} SNil{}:
78      1n+String.length(t)
79    case SCon{qh, qt} SCon{th, tt}:
80      +q = {SCon{qh, qt} : String}
81      +t = {SCon{th, tt} : String}
82      +qn +tn = String.length(q) String.length(t)
83      distance_shorter(q, t, qn, tn, Nat.is_le(qn, tn), pairs)
84
85def distance(query: String, target: String) -> Nat:
86  distance_with_equalities(query, target, Nil{})
87
88# Directional DP keeps query rows and target columns in their original order.
89# D[i,0] = i in every mode. SHW has D[0,j] = j and a free target suffix;
90# HW has D[0,j] = 0 and both target ends free. Both minimize D[m,j].
91def initial_semiglobal_row(length: Nat, +column: U32, +mode: E.Mode) -> List<U32>:
92  match length mode:
93    case 0n E.HW{}:
94      [0]
95    case 0n _:
96      [column]
97    case 1n+p E.HW{}:
98      0 <> initial_semiglobal_row(p, U32.add(column, 1), mode)
99    case 1n+p _:
100      column <> initial_semiglobal_row(p, U32.add(column, 1), mode)
101
102def final_row(query: String, +target: String, previous: List<U32>,
103              +index: U32, +pairs: List<&2, E.EqualityPair>) -> List<U32>:
104  match query:
105    case SNil{}:
106      previous
107    case SCon{h, t}:
108      final_row(t, target, next_row(previous, target, h, index, pairs), U32.add(index, 1), pairs)
109
110type Best is Data:
111  Best{score: U32, ends: List<&2, E.Coordinate>}
112
113def collect_best(best: Best, score: U32, end: E.Coordinate, comparison: Cmp) -> Best:
114  match best comparison:
115    case _ LT{}:
116      Best{score, [end]}
117    case Best{old, ends} EQ{}:
118      Best{old, end <> ends}
119    case _ GT{}:
120      best
121
122def collect(cells: List<U32>, +index: Nat, +best: Best) -> Best:
123  match cells:
124    case Nil{}:
125      best
126    case +score <> tail:
127      Best{old, _} = best
128      collect(tail, 1n+index, collect_best(best, score, E.Position{index}, U32.cmp(score, old)))
129
130def semiglobal_endpoints(cells: List<U32>, include_before: Bool) -> Best:
131  match cells include_before:
132    case Nil{} _:
133      Best{0, Nil{}}
134    case score <> tail True{}:
135      collect(tail, 0n, Best{score, [E.BeforeStart{}]})
136    case _ <> tail False{}:
137      collect(tail, 0n, Best{4294967295, Nil{}})
138
139def semiglobal(+query: String, +target: String, mode: E.Mode,
140               pairs: List<&2, E.EqualityPair>) -> Best:
141  # Pinned Edlib omits column zero when its final 64-bit word has no padding.
142  qn tn = String.length(query) String.length(target)
143  semiglobal_endpoints(final_row(query, target,
144    initial_semiglobal_row(tn, 0, mode), 1, pairs), Nat.is_ne(Nat.mod(qn, 64n), 0n))
145
146def semiglobal_result.accept(score: U32, ends: List<&2, E.Coordinate>, accepted: Bool) -> E.AlignResult:
147  match accepted:
148    case True{}:
149      E.AlignResult{E.Ok{}, E.Found{U32.to_nat(score)}, List.reverse(&2, E.Coordinate, ends), None{}, None{}, None{}}
150    case False{}:
151      E.not_found()
152
153def semiglobal_result(best: Best, +threshold: E.Threshold) -> E.AlignResult:
154  match best:
155    case Best{+score, ends}:
156      semiglobal_result.accept(score, ends, E.within_threshold(threshold, U32.to_nat(score)))
157
158# The independent worker supports configured DISTANCE in every mode, including
159# Edlib's empty-input early return before threshold filtering.
160def align(query: String, target: String, config: E.AlignConfig) -> E.AlignResult:
161  match query target config:
162    case SNil{} +t E.AlignConfig{E.NW{}, E.Distance{}, _, _, _}:
163      +length = String.length(t)
164      E.distance_result(length, E.end_coordinate(length), True{})
165    case SNil{} _ E.AlignConfig{_, E.Distance{}, _, _, _}:
166      E.distance_result(0n, E.BeforeStart{}, True{})
167    case SCon{_, qt} SNil{} E.AlignConfig{_, E.Distance{}, _, _, _}:
168      E.distance_result(1n+String.length(qt), E.BeforeStart{}, True{})
169    case +q +t E.AlignConfig{E.NW{}, E.Distance{}, +threshold, pairs, _}:
170      +score = distance_with_equalities(q, t, pairs)
171      E.distance_result(score, E.end_coordinate(String.length(t)), E.within_threshold(threshold, score))
172    case +q +t E.AlignConfig{mode, E.Distance{}, threshold, pairs, _}:
173      semiglobal_result(semiglobal(q, t, mode, pairs), threshold)
174    case _ _ _:
175      E.AlignResult{E.Error{}, E.NotFound{}, Nil{}, None{}, None{}, None{}}