[FEATURE] Use disjoint sets for equivalence classes in the type checker

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

439 stars 40 forks source link

[FEATURE] Use disjoint sets for equivalence classes in the type checker #973

Open konnov opened 3 years ago

konnov commented 3 years ago

Following the discussion in #952

konnov commented 3 years ago

Somehow, I messed up the title several times. @Kukovec would you like to implement that in October?

konnov commented 2 years ago

The chapter 10 of Advanced Topics... by Pottier and Remy contains the unification algorithm that uses union-find. Shall we check that one before re-inventing anything?