thautwarm / rsolve.py Goto Github PK

This feature is natural in Python version but not for the Haskell's, which just shocked me because this is one of the cases that Python is more inspiring than Haskell.

HMUnify[NomTypeSystem] is a sort of atomic formulas, which represents the logic that two type are able to get unified with the other.
As the python version can use heterogeneous atomic formulas, this solver can be greatly enhanced: atomic formulas representing the equality of terms can be attached with an atomic formula of HM unification, like

eq = (TNom(int32) == tvar1).imply(Scope("a") == Term(Int(1))))
solver.check(eq)