Module 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()).

The best way to see how it is used is to read the tests.rs file; search for e.g. UnitKey.

Structs

• InPlace
  Backing store for an in-place unification table. Not typically used directly.
• 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. You must define a key type K that implements the UnifyKey trait. Unification tables can be used in two-modes:
• VarValue
  Value of a unification key. We implement Tarjan’s union-find algorithm: when two keys are unified, one of them is converted into a “redirect” pointing at the other. These redirects form a DAG: the roots of the DAG (nodes that are not redirected) are each associated with a value of type V and a rank. The rank is used to keep the DAG relatively balanced, which helps keep the running time of the algorithm under control. For more information, see http://en.wikipedia.org/wiki/Disjoint-set_data_structure.

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).
• UnificationStore
• UnificationStoreBase
  Largely internal trait implemented by the unification table backing store types. The most common such type is InPlace, which indicates a standard, mutable unification table.
• UnificationStoreMut
• 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.

Type Aliases

• InPlaceUnificationTable
  A unification table that uses an “in-place” vector.
• UnificationStorage
• UnificationTableStorage