def validate

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

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

231# Edlib codes: Match=0 consumes both, Insert=1 consumes query only,
232# Delete=2 consumes target only, Mismatch=3 consumes both. Validation requires
233# exact consumption, the configured (symmetric, nontransitive) predicate on
234# every diagonal operation, and an edit cost equal to the reported distance.
235def validate(operations: List<&2, E.Operation>, query: String, target: String,
236               +pairs: List<&2, E.EqualityPair>, +expected: Nat, cost: Nat) -> Bool:
237  match operations query target:
238    case Nil{} SNil{} SNil{}:
239      Nat.is_eq(cost, expected)
240    case E.Match{} <> tail SCon{q, qt} SCon{t, tt}:
241      Bool.and(E.equal(pairs, q, t), validate(tail, qt, tt, pairs, expected, cost))
242    case E.Mismatch{} <> tail SCon{q, qt} SCon{t, tt}:
243      Bool.and(Bool.not(E.equal(pairs, q, t)), validate(tail, qt, tt, pairs, expected, 1n+cost))
244    case E.Insert{} <> tail SCon{_, qt} _:
245      validate(tail, qt, target, pairs, expected, 1n+cost)
246    case E.Delete{} <> tail _ SCon{_, tt}:
247      validate(tail, query, tt, pairs, expected, 1n+cost)
248    case _ _ _:
249      False{}