ref.py

from dataclasses import dataclass

@dataclass
class Ref:
    """Representação de uma variável.
    
    Se ela não possuir um valor ainda, é dita livre; se não, ela está ligada."""
    name: str
    value: any = None

    def __repr__(self):
        if self.value is None:
            return self.name
        return f"{self.name}={self.value!r}"

def deref(t):
    """Caminha pela cadeia de refs até encontrar um valor concreto, ou uma variável livre."""
    while isinstance(t, Ref) and t.value is not None:
        t = t.value
    return t

saida.txt

(1, 2, 3) = (1, 2, 3)
[]

(1, 2, 3) = (1, 2, 4)
(1, 2, 3) != (1, 2, 4) at #3: 3 != 4

(1, 2, 3) = (1, 2, 3, 4)
(1, 2, 3) != (1, 2, 3, 4): len 3 != len 4

(1, 2, 3) = (1, 3, 2)
(1, 2, 3) != (1, 3, 2) at #2: 2 != 3

(1, x, 3) = (1, 2, 3)
[x=2]

(1, 2, (3, y)) = (1, 2, (3, 4))
[y=4]

(1, x, (3, 5)) = (1, (3, y), x)
[x=(3, y=5), y=5]

(x, y) = ((2, y), (2, x))
[x=(2, y=(2, x=(...))), y=(2, x=(2, y=(...)))]

(1, 2, x) = (x, y, y)
(1, 2, x=1) != (x=1, y=2, y=2) at #3: 1 != 2

test.py

def test(xs, t1, t2):
    print(f"{t1} = {t2}")
    try:
        unify(t1, t2)
        print(xs)
    except UnifyError as e:
        print(e)
    print()

if __name__ == '__main__':
    test([], (1, 2, 3), (1, 2, 3))
    test([], (1, 2, 3), (1, 2, 4))
    test([], (1, 2, 3), (1, 2, 3, 4))
    test([], (1, 2, 3), (1, 3, 2))

    x = Ref("x")
    test([x], (1, x, 3), (1, 2, 3))

    y = Ref("y")
    test([y], (1, 2, (3, y)), (1, 2, (3, 4)))

    x, y = Ref("x"), Ref("y")
    test([x, y], (1, x, (3, 5)), (1, (3, y), x))

    x, y = Ref("x"), Ref("y")
    test([x, y], (x, y), ((2, y), (2, x)))

    x, y = Ref("x"), Ref("y")
    test([x, y], (1, 2, x), (x, y, y))

unify.py

def unify(t1, t2):
    """Unifica os termos, modificando as refs para apontar para seus valores ligados."""
    # Desreferencia ambos t1 e t2, de modo que nenhum é uma variável ligada.
    t1, t2 = deref(t1), deref(t2)

    # Caso #1: um dos dois termos é uma variável livre.
    if isinstance(t1, Ref) or isinstance(t2, Ref):
        if not isinstance(t2, Ref):
            t1.value = t2
        elif not isinstance(t1, Ref):
            t2.value = t1
        elif t1.name != t2.name:
            # Caso limite: duas variáveis livres são ligadas na ordem
            # dos seus nomes para garantir determinismo.
            #
            # Isto é, tanto X = Y quanto Y = X resultam em Y apontando para X.
            if t1.name > t2.name:
                t1, t2 = t2, t1
            t2.value = t1
        return

    # Caso #2: ambos são listas.
    if isinstance(t1, tuple) and isinstance(t2, tuple):
        # Inicialmente verifica os comprimentos.
        l1, l2 = len(t1), len(t2)
        if l1 != l2:
            cause = UnifyError(f"len {l1}", f"len {l2}")
            raise UnifyError(t1, t2, cause=cause)

        # Unifica seus elementos um a um.
        for i, (a, b) in enumerate(zip(t1, t2)):
            try:
                unify(a, b)
            except UnifyError as e:
                raise UnifyError(t1, t2, index=i, cause=e)
        return

    # Caso #3: lance um erro se os termos são diferentes (segundo o Python)
    if t1 != t2:
        raise UnifyError(t1, t2)

unify_error.py

class UnifyError(Exception):
    def __init__(self, t1, t2, index=None, cause=None):
        self.t1 = t1
        self.t2 = t2
        self.index = index
        self.cause = cause
        super().__init__(str(self))

    def __str__(self):
        msg = f"{self.t1} != {self.t2}"
        if self.index is not None:
            msg += f" at #{self.index+1}"
        if self.cause:
            msg += f": {self.cause}"
        return msg