1	import Base
2	import ./EdlibTypes.bend as E
3	import ./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	
10	def diagonal_operation(matches: Bool) -> E.Operation:
11	  Bool.pick(E.Operation, matches, E.Match{}, E.Mismatch{})
12	
13	type TraceCell is Data:
14	  TraceCell{score: U32, operation: E.Operation}
15	
16	def cell_score(cell: TraceCell) -> U32:
17	  match cell:
18	    case TraceCell{score, _}:
19	      score
20	
21	def 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	
30	def 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	
38	def 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	
50	def 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	
60	def 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	
67	def 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.
81	def 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	
101	def 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	
110	def 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.
118	def small_matrix(query_length: Nat, +target_length: Nat) -> Bool:
119	  Nat.is_le(1n+query_length, Nat.div(4096n, 1n+target_length))
120	
121	def 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	
124	type Split is Data:
125	  Split{index: Nat, score: U32}
126	
127	def split_index(split: Split) -> Nat:
128	  match split:
129	    case Split{index, _}:
130	      index
131	
132	def split_score(split: Split) -> U32:
133	  match split:
134	    case Split{_, score}:
135	      score
136	
137	def 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.
148	def 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	
161	def 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.
176	def 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	
203	def 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	
214	def 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	
225	def 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.
234	def 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	
250	def 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)