def unify(x,y,v={}):
    """
    Find one valuation extending v and unifying x with y
    """
    
    def extend(v, x, t):
        """
        Extend valuation v with v[x] = t
        """
        v1 = copy.copy(v)
        v1[x] = t
        return v1

    def occur_check(x, t):
        """
        Test if the variable x occurr in structure t
        """
        if x == t:
            return True
        elif isinstance(t, Struct):
            return t.head == x.head or occur_check(x, t.subs)
        return False

    def unify_var(x, t, v):
        """
        Test if v can be extended with v[x] = t;
        In that case return the extention
        Else return None
        """
        if x in v:
            return unify( v[ x ], t, v)
        elif occur_check(x, t):
            return None
        else:
            return extend(v, x, t)

    if v == None:
        return None
    elif x == y:
        return v
    elif isinstance(x, Variable):
        return unify_var(x, y, v)
    elif isinstance(y, Variable):
        return unify_var(y, x, v)
    elif isinstance(x, Struct) and isinstance(y, Struct) and (x.head == y.head):
        z = v
        n = len(x.subs)
        m = len(y.subs)
        if n == m:
            for i in range( n ):
                z = unify( x.subs[i], y.subs[i], z)
            return z
        else:
            return None
    else:
        return None

    Find one valuation extending v and unifying x with y
    
recipes/Python/360698_Extending_pythprolog_syntax/recipe-360698.py