How to efficiently process a batch of terms in one go for Tree Neural Networks about coqgym HOT 2 CLOSED

Batching trees is possible but needs extra effort compared to images.
Batching images is easy because all images have the same size (after preprocessing). You just have to stack them together to form a batch.
For trees, however, you cannot simply stack them since they have different shapes. In this case, the implementation of batching often depends on each specific use case. For example, in term_encoder.py, I put nodes of the same height into a batch, and process them bottom-up. In other words, I first process nodes with height 0, then height 1, then height 2, etc.

from coqgym.

discussion link: #48

from coqgym.