In many parts of this library, we take callbacks as input, mainly as a way of avoiding intermediate allocations and to allow equality saturation to be an "anytime" algorithm. We should replace these with a stream processing library like pipes or streaming. Since this library is meant to be performant, we will probably want to go with streaming.
This could also make it possible to do even more optimizations; for example, it might make sense to have equality saturation emit a stream of differences to the equality proof tree, rather than re-emitting the proof tree every time. It also naturally supports incrementalization: it could accept a Producer for diffs to the original Term.
This idea is courtesy of @mckeankylej
In many parts of this library, we take callbacks as input, mainly as a way of avoiding intermediate allocations and to allow equality saturation to be an "anytime" algorithm. We should replace these with a stream processing library like
pipesorstreaming. Since this library is meant to be performant, we will probably want to go withstreaming.This could also make it possible to do even more optimizations; for example, it might make sense to have equality saturation emit a stream of differences to the equality proof tree, rather than re-emitting the proof tree every time. It also naturally supports incrementalization: it could accept a
Producerfor diffs to the originalTerm.This idea is courtesy of @mckeankylej