%reduce:
unify(Pointer, Param1, Param2)
 :- unify(Pointer, T1, T2), type(T1, TName, Num), type(T2, TName, Num)
	, param(T1, Param1, PNum), param(T2, Param2, PNum)
	.

%swap:
unify(Pointer, B, A) :- unify(Pointer, A, B).

%subst:
%Neuen Typ erstellen, in diesem werden dann die TPHs ersetzt:
type(pointer(unify(Pointer, A, B, E)), Name, Num)
:- unify(Pointer, A, B), typeVar(A), not occurs(A, B), type(E, Name, Num)
	,param(E, Param, _), occurs(A, Param), Param != A.

param(pointer(unify(Pointer, A, B, E)), pointer(unify(Pointer, A, B, Param)), ParamNum)
:- unify(Pointer, A, B), typeVar(A), not occurs(A, B), type(E, Name, Num)
	,param(E, Param, ParamNum), occurs(A, Param), Param != A.

param(pointer(unify(Pointer, A, B, E)), B, ParamNum)
:- unify(Pointer, A, B), typeVar(A), not occurs(A, B), type(E, Name, Num)
	,param(E, A, ParamNum).

param(pointer(unify(Pointer, A, B, E)), Param, ParamNum)
:- unify(Pointer, A, B), typeVar(A), not occurs(A, B), type(E, Name, Num)
	,param(E, Param, ParamNum), not occurs(A, Param).


%Subst neu implementieren.
%Subst muss von hinten nach vorne durchgehen.
%Mit occurs kann man prüfen, welche unify(P, A, B) ausgetauscht werden müssen

%Diese Fälle dürfen nicht auftreten:
%TODO (möglicherweise braucht man sie nicht; Die Unifikation geht hier nie schief)

%Occurs Regeln:
occurs(A, A) :- typeVar(A).
occurs(A, T) :- type(T, _,_), param(T, B, _), occurs(A, B).