def dashspan

mylsm-lsm-store@0.3.2.0 · src/Wal.bend:295

import Base

295# RLen dash-run skip (unified len phase; next stored, never matched here).
296# Fuel is len(span++tail): deconstructs with the Nat induction, tail opaque.
297def dashspan(
298  num: Nat,
299  tail: String,
300  muts0: List<&2, Mut>,
301  tag: Char,
302  next: Phase,
303  +num0: Nat,
304  kacc0: String,
305) -> {dec_run(String.length(dashes(num) ++ tail), dashes(num) ++ tail, DS{RLen{next}, muts0, tag, num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, jump(num, num0), kacc0, "", "", True{}}) : DecState}:
306  match num:
307    case 0n:
308      {==}
309    case 1n++m:
310      %jump_succ(m, num0) : {dec_run(String.length(dashes(m) ++ tail), dashes(m) ++ tail, DS{RLen{next}, muts0, tag, 1n+num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, _, kacc0, "", "", True{}}) : DecState}
311      %dashspan(m, tail, muts0, tag, next, 1n+num0, kacc0) : {dec_run(String.length(dashes(m) ++ tail), dashes(m) ++ tail, DS{RLen{next}, muts0, tag, 1n+num0, kacc0, "", "", True{}}) == _ : DecState}
312      {==}