def divide

bend-edit-distance@0.2.2.0 · src/Reconstruction.bend:173

import Base
import bend-edit-distance@0.2.2.0/EdlibTypes.bend as E

173# The fuel is the initial row length; every nonbase call halves that length.
174# Score passes run in balanced parallel calls and are consumed before recursion.
175# Subpaths are evaluated sequentially to bound live score storage even on many
176# threads; the result lists themselves necessarily use O(m+n) space.
177def divide(fuel: Nat, +query: String, +target: String, +query_length: Nat,
178             +target_length: Nat, +pairs: List<&2, E.EqualityPair>, small: Bool) ->
179             List<&2, E.Operation>:
180  match fuel query target small:
181    case _ SNil{} _ _:
182      List.replicate(E.Operation, target_length, E.Delete{})
183    case _ _ SNil{} _:
184      List.replicate(E.Operation, query_length, E.Insert{})
185    case 0n _ _ _:
186      dp(query, target, pairs)
187    case 1n+p SCon{_, SNil{}} _ _:
188      dp(query, target, pairs)
189    case 1n+p _ _ True{}:
190      dp(query, target, pairs)
191    case Succ{+p} _ _ False{}:
192      +half = Nat.div(query_length, 2n)
193      +left = String.take(query, half)
194      +right = String.drop(query, half)
195      +cut = midpoint(left, right, target, pairs)
196      left_path = divide(p, left, String.take(target, cut), half, cut, pairs,
197        small_matrix(half, cut))
198      +right_length = Nat.sub(query_length, half)
199      +right_width = Nat.sub(target_length, cut)
200      right_path = divide(p, right, String.drop(target, cut), right_length, right_width, pairs,
201        small_matrix(right_length, right_width))
202      List.append(&2, E.Operation, left_path, right_path)