def ext_dec

bend-ml-bpe-tokenizer@0.1.3.0 · main.bend:390

import Base

390# decoding a list of known tokens does not change when the new rule is added
391def ext_dec(+D: List<&2, Rule>, +i: Nat, +a: Tk, +b: Tk, xs: List<&2, Tk>, +kx: {True{} == knl(D, xs) : Bool}, +nf: {True{} == Bool.not(has(D, i)) : Bool}) -> {dec(Rule{i, a, b} <> D, xs) == dec(D, xs) : List<&2, Nat>}:
392  match xs:
393    case Nil{}:
394      {==}
395    case Con{+x, +t}:
396      ext_dec.step(D, i, a, b, x, t, and_true_l(kn(D, x), knl(D, t), kx), nf, ext_dec(D, i, a, b, t, and_true_r(kn(D, x), knl(D, t), kx), nf))