Documentation

A lazy stream of ExBudgets. Basically NonEmpty ExBudget, except the elements are stored strictly.

The semantics of a stream are those of the fold of its elements. I.e. a stream that is a reordered version of another stream is considered equal to that stream.

An ExBudgetStream is what one gets by zipping two CostStreams (one for CPU, one for memory), which is why the two data types are so similar. The only reason why we don't express both the concepts in terms of a single data type is efficiency, in particular unboxing is crucial for CostStream and we don't care about it in ExBudgetStream, because we can't get the spender in the CEK machine to get inlined and so unboxing ExBudget here would only result in boxing it back once it's about to be spent.

Add up all the budgets in a ExBudgetStream.

Zip two CostStream together (one with CPU costs and the other one with memory costs, respectively) to get an ExBudgetStream. If one is longer than the other, then it's assumed to contain the required amount of zeros for two streams to have the same length (all those zeros "appear" in the tail of the stream).