def encode.go

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

import Base

69# applies the rules from the oldest to the newest; `done` keeps the ones already applied
70# (newest first), which is exactly the table that decode needs. Only the proofs read it, so it
71# is erased (`-done`): the checker keeps it and the compiled program never builds it. Building
72# it cost half of the time to encode (found by Mathews Fernando's bend-lint, dead_accumulator).
73def encode.go(todo: List<&2, Rule>, -done: List<&2, Rule>, xs: List<&2, Tk>) -> List<&2, Tk>:
74  match todo:
75    case Nil{}:
76      xs
77    case Con{+r, rest}:
78      match r:
79        case Rule{+i, +a, +b}:
80          encode.go(rest, Rule{i, a, b} <> done, merge(a, b, M{i}, xs))