Module ena::unify

Union-find implementation. The main type is UnificationTable.

You can define your own type for the keys in the table, but you must implement UnifyKey for that type. The assumption is that keys will be newtyped integers, hence we require that they implement Copy.

Keys can have values associated with them. The assumption is that these values are cheaply cloneable (ideally, Copy), and some of the interfaces are oriented around that assumption. If you just want the classical "union-find" algorithm where you group things into sets, use the Value type of ().

When you have keys with non-trivial values, you must also define how those values can be merged. As part of doing this, you can define the "error" type to return on error; if errors are not possible, use NoError (an uninstantiable struct). Using this type also unlocks various more ergonomic methods (e.g., union() in place of unify_var_var()).

Structs

NoError	A struct which can never be instantiated. Used for the error type for infallible cases.
Snapshot	At any time, users may snapshot a unification table. The changes made during the snapshot may either be committed or rolled back.
UnificationTable	Table of unification keys and their values.
UnionedKeys	Iterator over keys that have been unioned together.

Traits

EqUnifyValue	A convenient helper for unification values which must be equal or else an error occurs. For example, if you are unifying types in a simple functional language, this may be appropriate, since (e.g.) you can't unify a type variable bound to int with one bound to float (but you can unify two type variables both bound to int).
UnifyKey	This trait is implemented by any type that can serve as a type variable. We call such variables unification keys. For example, this trait is implemented by IntVid, which represents integral variables.
UnifyValue	Trait implemented for values associated with a unification key. This trait defines how to merge the values from two keys that are unioned together. This merging can be fallible. If you attempt to union two keys whose values cannot be merged, then the error is propagated up and the two keys are not unioned.