Unification and Substitution

[tirix]

This introduces formula unification and substitution, which are straightforward once the formula syntax tree is known. This PR also comes along with a handful of simple tests cases for unification and substitution.

[tirix]

This is a naive implementation of formula unification and substitution, in the sense that it is not optimized.

Currently, the syntax tree nodes of a formula are stored in a Vec, which belongs to the formula. I plan to replace this by an Arc pointer to a slice, so that several formulas can use the same underlying node storage.

This would allow at least two optimizations:

• the extraction of a sub-formula would be in O(1), since a sub-formula could be built by pointing to the same node storage, and changing only the root. Building of sub-formulas is used a lot during the unification process. Right now it's O(n) since each node is copied.
• the equality test of two formulas, could also be O(1) in the case that they use the same underlying node storage, since if two formulas share the same underlying node storage and have the same root, they are equal. This could be done in a coming PR.

I included more ideas for improvements in the header of formula.rs.

[david-a-wheeler]

Looks okay, I appreciate the included test. That next stage ("Arc"ing) should produce a substantial performance boost.

[tirix]

Thanks for the review @david-a-wheeler ! I'll give Mario some more time if he wants to have a look.

I think next on the list would be a clippy pass, then this improvement (maybe some benchmarking to measure how much this improves would be nice?)