Reconstruction.bend
bend-edit-distance@0.2.0.0 · 252 lines · 0 definitions
1import Base
2import bend-edit-distance@0.2.0.0/EdlibTypes.bend as E
3import bend-edit-distance@0.2.0.0/DistanceDP.bend as DP
4
5# Global reconstruction of one already selected target interval. Small DP
6# stores a score and predecessor operation per cell, never path prefixes.
7# Equal scores prefer up (Insert), left (Delete), then diagonal, as upstream
8# traceback does. Hirschberg only promises an optimal path, not upstream ties.
9
10def diagonal_operation(matches: Bool) -> E.Operation:
11 Bool.pick(E.Operation, matches, E.Match{}, E.Mismatch{})
12
13type TraceCell is Data:
14 TraceCell{score: U32, operation: E.Operation}
15
16def cell_score(cell: TraceCell) -> U32:
17 match cell:
18 case TraceCell{score, _}:
19 score
20
21def choose_operation(matches: Bool, up_is_best: Bool, left_is_best: Bool) -> E.Operation:
22 match up_is_best left_is_best:
23 case True{} _:
24 E.Insert{}
25 case False{} True{}:
26 E.Delete{}
27 case False{} False{}:
28 diagonal_operation(matches)
29
30def dp_cell(above: U32, left: U32, diagonal: U32, +matches: Bool) -> TraceCell:
31 +up = U32.add(above, 1)
32 +across = U32.add(left, 1)
33 +diagonal_cost = U32.add(diagonal, Bool.to_u32(Bool.not(matches)))
34 TraceCell{U32.min(U32.min(up, across), diagonal_cost),
35 choose_operation(matches,
36 U32.is_le(up, U32.min(across, diagonal_cost)), U32.is_le(across, diagonal_cost))}
37
38def dp_row_cells(columns: String, previous: List<&2, TraceCell>, diagonal: U32,
39 left: U32, +symbol: Char, +pairs: List<&2, E.EqualityPair>) ->
40 List<&2, TraceCell>:
41 match columns previous:
42 case SNil{} _:
43 Nil{}
44 case SCon{_, _} Nil{}:
45 Nil{}
46 case SCon{h, t} TraceCell{+above, _} <> rest:
47 +next = dp_cell(above, left, diagonal, E.equal(pairs, symbol, h))
48 next <> dp_row_cells(t, rest, above, cell_score(next), symbol, pairs)
49
50def dp_row(previous: List<&2, TraceCell>, columns: String, symbol: Char,
51 +index: U32, pairs: List<&2, E.EqualityPair>) ->
52 List<&2, TraceCell>:
53 match previous:
54 case Nil{}:
55 [TraceCell{index, E.Insert{}}]
56 case TraceCell{diagonal, _} <> rest:
57 TraceCell{index, E.Insert{}} <>
58 dp_row_cells(columns, rest, diagonal, index, symbol, pairs)
59
60def dp_initial(target: String, +index: U32) -> List<&2, TraceCell>:
61 match target:
62 case SNil{}:
63 [TraceCell{index, E.Delete{}}]
64 case SCon{_, tail}:
65 TraceCell{index, E.Delete{}} <> dp_initial(tail, U32.add(index, 1))
66
67def dp_rows(query: String, +target: String, previous: List<&2, TraceCell>,
68 +index: U32, +pairs: List<&2, E.EqualityPair>,
69 directions: List<&2, List<&2, TraceCell>>) -> List<&2, List<&2, TraceCell>>:
70 match query:
71 case SNil{}:
72 directions
73 case SCon{h, t}:
74 +row = dp_row(previous, target, h, index, pairs)
75 dp_rows(t, target, row, U32.add(index, 1), pairs,
76 List.reverse(&2, TraceCell, row) <> directions)
77
78# Rows and their operations are reversed so left moves consume the current
79# row directly. Entering the row above skips only its unused right suffix.
80# Including boundary rows/columns handles all-insertion/deletion paths.
81def traceback(fuel: Nat, current: List<&2, TraceCell>,
82 previous: List<&2, List<&2, TraceCell>>, +width: Nat,
83 +column: Nat, operations: List<&2, E.Operation>) -> List<&2, E.Operation>:
84 match fuel current previous:
85 case 0n _ _:
86 operations
87 case 1n+p _ Nil{}:
88 List.append(&2, E.Operation, List.replicate(E.Operation, column, E.Delete{}), operations)
89 case 1n+p Nil{} _:
90 operations
91 case 1n+p TraceCell{_, E.Insert{}} <> _ row <> rest:
92 traceback(p, List.drop(&2, TraceCell, row, Nat.sub(width, column)),
93 rest, width, column, E.Insert{} <> operations)
94 case 1n+p TraceCell{_, E.Delete{}} <> tail +rows:
95 traceback(p, tail, rows, width, Nat.sub(column, 1n), E.Delete{} <> operations)
96 case 1n+p TraceCell{_, operation} <> _ row <> rest:
97 +next_column = Nat.sub(column, 1n)
98 traceback(p, List.drop(&2, TraceCell, row, Nat.sub(width, next_column)),
99 rest, width, next_column, operation <> operations)
100
101def dp_trace(matrix: List<&2, List<&2, TraceCell>>, query_length: Nat,
102 +target_length: Nat) -> List<&2, E.Operation>:
103 match matrix:
104 case Nil{}:
105 Nil{}
106 case row <> rest:
107 traceback(Nat.add(query_length, target_length), row, rest,
108 target_length, target_length, Nil{})
109
110def dp(+query: String, +target: String, pairs: List<&2, E.EqualityPair>) -> List<&2, E.Operation>:
111 qn +tn = String.length(query) String.length(target)
112 +boundary = dp_initial(target, 0)
113 dp_trace(dp_rows(query, target, boundary, 1, pairs,
114 [List.reverse(&2, TraceCell, boundary)]), qn, tn)
115
116# Bound the complete small matrix, including its boundary cells. A one-row
117# problem is also a base case, with linear storage in the column width.
118def small_matrix(query_length: Nat, +target_length: Nat) -> Bool:
119 Nat.is_le(1n+query_length, Nat.div(4096n, 1n+target_length))
120
121def score_row(query: String, +target: String, pairs: List<&2, E.EqualityPair>) -> List<U32>:
122 DP.final_row(query, target, DP.initial_row(String.length(target), 0), 1, pairs)
123
124type Split is Data:
125 Split{index: Nat, score: U32}
126
127def split_index(split: Split) -> Nat:
128 match split:
129 case Split{index, _}:
130 index
131
132def split_score(split: Split) -> U32:
133 match split:
134 case Split{_, score}:
135 score
136
137def split_update(index: Nat, score: U32, old_index: Nat, old_score: U32,
138 better: Bool) -> Split:
139 match better:
140 case True{}:
141 Split{index, score}
142 case False{}:
143 Split{old_index, old_score}
144
145# Forward[j] + reverse[n-j] is the cost through the midpoint at column j.
146# Strict comparison keeps the first minimum; this is our deterministic split
147# policy and is deliberately separate from upstream Hirschberg compatibility.
148def split_column(forward: List<U32>, backward: List<U32>, +index: Nat,
149 +best_index: Nat, +best_score: U32) -> Nat:
150 match forward backward:
151 case Nil{} _:
152 best_index
153 case _ Nil{}:
154 best_index
155 case a <> at b <> bt:
156 +score = U32.add(a, b)
157 +next = split_update(index, score, best_index, best_score,
158 U32.is_lt(score, best_score))
159 split_column(at, bt, 1n+index, split_index(next), split_score(next))
160
161def midpoint(left: String, right: String, +target: String,
162 +pairs: List<&2, E.EqualityPair>) -> Nat:
163 # Prepare recursive arguments before the fork. Passing String.reverse(...)
164 # inside its second call drains the frontier in the pinned native runtime.
165 reverse_query = String.reverse(right)
166 reverse_target = String.reverse(target)
167 forward backward =
168 score_row(left, target, pairs)
169 score_row(reverse_query, reverse_target, pairs)
170 split_column(forward, List.reverse(&1, U32, backward), 0n, 0n, 4294967295)
171
172# The fuel is the initial row length; every nonbase call halves that length.
173# Score passes run in balanced parallel calls and are consumed before recursion.
174# Subpaths are evaluated sequentially to bound live score storage even on many
175# threads; the result lists themselves necessarily use O(m+n) space.
176def divide(fuel: Nat, +query: String, +target: String, +query_length: Nat,
177 +target_length: Nat, +pairs: List<&2, E.EqualityPair>, small: Bool) ->
178 List<&2, E.Operation>:
179 match fuel query target small:
180 case _ SNil{} _ _:
181 List.replicate(E.Operation, target_length, E.Delete{})
182 case _ _ SNil{} _:
183 List.replicate(E.Operation, query_length, E.Insert{})
184 case 0n _ _ _:
185 dp(query, target, pairs)
186 case 1n+p SCon{_, SNil{}} _ _:
187 dp(query, target, pairs)
188 case 1n+p _ _ True{}:
189 dp(query, target, pairs)
190 case Succ{+p} _ _ False{}:
191 +half = Nat.div(query_length, 2n)
192 +left = String.take(query, half)
193 +right = String.drop(query, half)
194 +cut = midpoint(left, right, target, pairs)
195 left_path = divide(p, left, String.take(target, cut), half, cut, pairs,
196 small_matrix(half, cut))
197 +right_length = Nat.sub(query_length, half)
198 +right_width = Nat.sub(target_length, cut)
199 right_path = divide(p, right, String.drop(target, cut), right_length, right_width, pairs,
200 small_matrix(right_length, right_width))
201 List.append(&2, E.Operation, left_path, right_path)
202
203def transpose(operations: List<&2, E.Operation>) -> List<&2, E.Operation>:
204 match operations:
205 case Nil{}:
206 Nil{}
207 case E.Insert{} <> tail:
208 E.Delete{} <> transpose(tail)
209 case E.Delete{} <> tail:
210 E.Insert{} <> transpose(tail)
211 case operation <> tail:
212 operation <> transpose(tail)
213
214def reconstruct_order(query: String, target: String, +query_length: Nat,
215 +target_length: Nat, pairs: List<&2, E.EqualityPair>,
216 small: Bool, query_is_taller: Bool) -> List<&2, E.Operation>:
217 match small query_is_taller:
218 case True{} _:
219 dp(query, target, pairs)
220 case False{} True{}:
221 divide(query_length, query, target, query_length, target_length, pairs, False{})
222 case False{} False{}:
223 transpose(divide(target_length, target, query, target_length, query_length, pairs, False{}))
224
225def reconstruct(+query: String, +target: String, pairs: List<&2, E.EqualityPair>) ->
226 List<&2, E.Operation>:
227 +qn +tn = String.length(query) String.length(target)
228 reconstruct_order(query, target, qn, tn, pairs, small_matrix(qn, tn), Nat.is_ge(qn, tn))
229
230# Edlib codes: Match=0 consumes both, Insert=1 consumes query only,
231# Delete=2 consumes target only, Mismatch=3 consumes both. Validation requires
232# exact consumption, the configured (symmetric, nontransitive) predicate on
233# every diagonal operation, and an edit cost equal to the reported distance.
234def validate(operations: List<&2, E.Operation>, query: String, target: String,
235 +pairs: List<&2, E.EqualityPair>, +expected: Nat, cost: Nat) -> Bool:
236 match operations query target:
237 case Nil{} SNil{} SNil{}:
238 Nat.is_eq(cost, expected)
239 case E.Match{} <> tail SCon{q, qt} SCon{t, tt}:
240 Bool.and(E.equal(pairs, q, t), validate(tail, qt, tt, pairs, expected, cost))
241 case E.Mismatch{} <> tail SCon{q, qt} SCon{t, tt}:
242 Bool.and(Bool.not(E.equal(pairs, q, t)), validate(tail, qt, tt, pairs, expected, 1n+cost))
243 case E.Insert{} <> tail SCon{_, qt} _:
244 validate(tail, qt, target, pairs, expected, 1n+cost)
245 case E.Delete{} <> tail _ SCon{_, tt}:
246 validate(tail, query, tt, pairs, expected, 1n+cost)
247 case _ _ _:
248 False{}
249
250def valid_path(query: String, target: String, operations: List<&2, E.Operation>,
251 pairs: List<&2, E.EqualityPair>, distance: Nat) -> Bool:
252 validate(operations, query, target, pairs, distance, 0n)