def Entries.truncate

bend-trace-context@0.2.0.0 · trace_context.bend:2466

import Base

2466# Remove entries one step at a time while they take more than `budget`
2467# octets, and stop as soon as they fit. `fuel` bounds the steps. One per
2468# entry suffices: once every entry is removed, the empty list takes 0 octets,
2469# which fits any budget.
2470def Entries.truncate(fuel: Nat, +budget: Nat, +entries: List<&2, StateEntry>) -> List<&2, StateEntry>:
2471  match fuel:
2472    case 0n:
2473      entries
2474    case 1n+more:
2475      Bool.pick(List<&2, StateEntry>, Nat.is_le(Entries.size(entries), budget), entries,
2476        Entries.truncate(more, budget, Entries.shrink(entries)))