mapFC -> pi

*

asp/adaptRules.lp

@@ -0,0 +1,19 @@
+%makeAdapt(smallerDot(CFC, DFC)) :- smallerDot(C, D), type(C, CN, CNP), type(D, DN, DNP), CNP != DNP
+	%, smaller(CFC, DFC), type(CFC, CN, CNP), type(DFC, DN, DNP), mapRootFC(smaller(CFC, DFC), _, _)
+	%.
+
+
+type(pointer(smallerDot(C,D)), DN, DNP)
+:- smallerDot(C, D), type(C, CN, CNP), type(D, DN, DNP), CNP != DNP
+	.
+smallerDot(pointer(smallerDot(C,D)), D)
+:- smallerDot(C, D), type(C, CN, CNP), type(D, DN, DNP), CNP != DNP
+	.
+
+param(pointer(smallerDot(C,D)), P, P2)
+:- smallerDot(C, D), type(C, CN, CNP), type(D, DN, DNP), CNP != DNP
+	, smaller(CFC, DFC), type(CFC, CN, CNP), type(DFC, DN, DNP)
+	, pi(CFC, DFC, P1, P2), param(C, P, P1)
+	.
+
+

asp/cartesian.lp

@@ -0,0 +1,22 @@
+
+%Mit Hilfe von Quelle: https://www.cs.uni-potsdam.de/~torsten/Papers/asp4ki.pdf
+
+%Dieser Code generiert das Karthesische Produkt der Constraints des Inputs.
+%und Constraints sind einfach weiterhin equals uns smallerDot
+%oder constraints:
+% oder(pointer, pointer)
+%constraints innerhalb des oders müssen eingepackt sein:
+% constraint(pointer, eigentlicher Constraint)
+% um mehrere constraints als Und-Constraint innerhalb eines Oders zu verbinden kann die list(..) verwendet werden
+
+%Die eigentliche Oder-Verknüpfung:
+cons(Cons1), cons(Cons2) :- oder(C1, C2), constraint(C1, Cons1), constraint(C2, Cons2).
+
+%Auspacken der constraints:
+equals(X,Y) :- cons(equals(X,Y)).
+smallerDot(X,Y) :- cons(smallerDot(X,Y)).
+oder(X,Y) :- cons(oder(X,Y)).
+list(X,Y) :- cons(list(X,Y)).
+equals(X,Y) :- list(equals(X,Y), _).
+smallerDot(X,Y) :- list(smallerDot(X,Y), _).
+list(A,B) :- list(_, list(A,B)).

asp/facultyTestInput.lp

@@ -0,0 +1,70 @@
+typeVar(cRO).
+smaller(cAVP,cAVQ).
+type(cAVY,cjava_DOT_lang_DOT_Integer,0).
+type(cAVI,cjava_DOT_lang_DOT_Integer,0).
+type(cAVD,cjava_DOT_lang_DOT_Comparable,1).
+type(cAVH,cjava_DOT_lang_DOT_Comparable,1).
+type(cAVJ,cjava_DOT_lang_DOT_Number,0).
+typeVar(cT).
+equals(cQ,cRO).
+smaller(cAVR,cAVS).
+param(cAVZ,cYO,1).
+param(cAVZ,cYP,2).
+type(cAWD,cjava_DOT_lang_DOT_Integer,0).
+typeVar(cO).
+smaller(cAVN,cAVO).
+type(cAWA,cjava_DOT_lang_DOT_Integer,0).
+type(cAVF,cjava_DOT_lang_DOT_Object,0).
+typeVar(cYA).
+type(cAVU,cjava_DOT_lang_DOT_Integer,0).
+equals(cN,cAVV).
+smaller(cAVB,cAVC).
+type(cAVO,cjava_DOT_lang_DOT_Object,0).
+type(cAVB,cjava_DOT_io_DOT_Serializable,0).
+smallerDot(cT,cM).
+typeVar(cL).
+smallerDot(cM,cL).
+typeVar(cP).
+type(cAVQ,cjava_DOT_lang_DOT_Number,0).
+type(cAVR,cFaculty,0).
+smallerDot(cAWD,cAWE).
+typeVar(cYB).
+type(cAVE,cjava_DOT_lang_DOT_Integer,0).
+type(cAVN,cjava_DOT_lang_DOT_Number,0).
+equals(cT,cAVT).
+type(cAVV,cFaculty,0).
+type(cAVC,cjava_DOT_lang_DOT_Object,0).
+type(cAVM,cjava_DOT_lang_DOT_Object,0).
+smaller(cAVG,cAVH).
+type(cAVL,cjava_DOT_lang_DOT_Object,0).
+type(cAWE,cjava_DOT_lang_DOT_Integer,0).
+type(cAVG,cjava_DOT_lang_DOT_Integer,0).
+param(cAVT,cAVU,2).
+typeVar(cYO).
+type(cAWB,cjava_DOT_lang_DOT_Integer,0).
+type(cAVW,cjava_DOT_lang_DOT_Integer,0).
+typeVar(cM).
+param(cAVH,cAVI,1).
+typeVar(cQ).
+type(cAVX,cjava_DOT_lang_DOT_Integer,0).
+equals(cYA,cO).
+equals(cAWA,cP).
+smallerDot(cM,cAVZ).
+type(cAVK,cjava_DOT_io_DOT_Serializable,0).
+smallerDot(cP,cQ).
+smallerDot(cO,cAWB).
+param(cAVD,cAVE,1).
+smallerDot(cAVY,cYB).
+smallerDot(cAVW,cAVX).
+smaller(cAVD,cAVF).
+smaller(cAVL,cAVM).
+type(cAVP,cjava_DOT_lang_DOT_Integer,0).
+typeVar(cYP).
+typeVar(cN).
+type(cAVT,cFun2,2).
+param(cAVT,cRO,1).
+type(cAVS,cjava_DOT_lang_DOT_Object,0).
+type(cAWC,cFaculty,0).
+smallerDot(cN,cAWC).
+type(cAVZ,cFun2,2).
+smaller(cAVJ,cAVK).

asp/fc.lp.backup

@@ -0,0 +1,125 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%Anzahl Wildcards in einem Typ feststellen:
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%Start, am Ende der Parameterliste:
+wildcard(A) :- extendsWildcard(A).
+wildcard(A) :- superWildcard(A).
+numWildcards(TP, Ende-1, Num) :- param(TP, Param, Ende),
+        numWildcards(Param, Num), type(TP,_,Ende)
+        , not wildcard(Param)
+        .
+numWildcards(TP, Ende-1, Num + 1) :- param(TP, Param, Ende),
+        numWildcards(Param, Num), type(TP,_,Ende)
+        , wildcard(Param)
+        .
+%Anschließend aufsummieren:
+numWildcards(TP, ParamNum-1, NumWC1 + NumWC2 + 1) :- param(TP, Param, ParamNum),
+        numWildcards(Param, NumWC1), numWildcards(TP,ParamNum, NumWC2)
+        , wildcard(Param)
+        .
+numWildcards(TP, ParamNum-1, NumWC1 + NumWC2) :- param(TP, Param, ParamNum),
+        numWildcards(Param, NumWC1), numWildcards(TP,ParamNum, NumWC2)
+        , not wildcard(Param)
+        .
+
+numWildcards(TP, Num) :- numWildcards(TP, 0, Num), param(TP, P, 1), wildcard(P).
+numWildcards(TP, Num) :- numWildcards(TP, 0, Num), param(TP, P, 1), not wildcard(P).
+numWildcards(TP, 0) :- type(TP, _, 0).
+numWildcards(TP, 0) :- typeVar(TP).
+
+%%%%%%%%%%%%%%%%
+% Greater
+%%%%%%%%%%%%%%%%
+{ greaterGen(P, A, AFC, BFC) : smaller(AFC, BFC), type(AFC, AN, ANum) } == 1 :- greaterGen(P, A), type(A, AN, ANum)
+%, greaterArgGenNum(P, N), N < 100000
+.
+%:- greaterGen(A, _, _ , _), numWildcards(A, NW), NW >= 1.
+type(P, BN, BNum) :- greaterGen(P, A, _, B), type(B, BN, BNum).
+%Bei den Parametern gibt es zwei Fälle:
+%% Die TPHs müssen gemapt werden, die anderen übernommen
+greaterArgGen(pointer(P, Param), Param) :- greaterGen(P, A, Afc, B), param(A, Param, PNum), mapFC(smaller(Afc, B), PNum, _).
+greaterArgGen(pointer(P, Param), Param) :- greaterGen(P, A, _, B), param(B, Param, PNum), type(B, _, _).
+param(P, pointer(P, Param), PNum) :- greaterGen(P, A, _, B), param(B, Param, PNum)
+	, type(Param, _, _)
+	.
+param(P, pointer(P, Param), PNum2) :- greaterGen(P, A, Afc, B), param(A, Param, PNum)
+	, mapFC(smaller(Afc,B), PNum, PNum2) 
+	.
+
+%TypeVars bleiben einfach TypeVars:
+typeVar(Pointer) :- greaterArgGen(Pointer, T), typeVar(T).
+
+makeGreaterGen(Pointer, T) :- greaterArgGen(Pointer, T), extendsWildcard(T).
+makeSmallerGen(Pointer, T) :- greaterArgGen(Pointer, T), superWildcard(T).
+makeSmallerGenG(Pointer, T),
+makeGreaterGenG(Pointer, T),
+makeSameGenG(Pointer, T)
+:- greaterArgGen(Pointer, T), not extendsWildcard(T), not superWildcard(T), type(T, N, Num).
+
+greaterGen(P, T) :- makeGreaterGenG(P, T).
+extendsWildcard(P) :- makeGreaterGenG(P, T).
+
+smallerGen(P, T) :- makeGreaterGenG(P, T).
+superWildcard(P) :- makeSmallerGenG(P, T).
+
+{ greaterGen(P, T, TFC, TFC) : smaller(TFC, _), type(TFC, TN, TNum) } == 1 :- makeSameGenG(P, T), type(T, TN, TNum).
+
+greaterArgGenNum(P, 0) :- greaterArgGen(P, _), type(P, _ ,_).
+greaterArgGenNum(pointer(P, P2), Num + 1) :- greaterArgGen(pointer(P, P2),_), greaterArgGenNum(P, Num).
+
+
+%%%%%%%%%%%%%%%%%
+% smaller
+%%%%%%%%%%%%%%%%
+{ smallerGen(P, A, AFC, BFC) : smaller(BFC, AFC), type(AFC, AN, ANum) } == 1 :- smallerGen(P, A), type(A, AN, ANum)
+.
+{ type(P, BN, BNum) : type(B,BN,BNum) } == 1 :- smallerGen(P, A, _, B).
+%Bei den Parametern gibt es drei Fälle:
+%% Die TPHs müssen gemapt werden, die anderen übernommen
+smallerArgGen(pointer(P, Param), Param) :- smallerGen(P, A, Afc, B), param(A, Param, PNum), mapFC(smaller(B, Afc), _, PNum).
+param(P, pointer(P, Param), PNum2) :- smallerGen(P, A, Afc, B), param(A, Param, PNum)
+	, mapFC(smaller(B,Afc), PNum2, PNum) 
+	.
+
+%Neue Parameter können hinzu kommen: TODO
+%smallerArgGen(pointer(P, Param), Param) :- smallerGen(P, A, _, B), param(B, Param, PNum).
+%param(P, pointer(P, Param), PNum) :- greaterGen(P, A, _, B), param(B, Param, PNum)
+%	%, type(Param, _, _) %Es ist egal ob es ein Typparameter oder eine TypeVar ist. smallerArgGen macht das richtige
+%	.
+
+%Es können voraussetzungen hinzukommen:
+equals(Param, PA) :- smallerGen(P, A, Afc, B), param(Afc, Param, PNum), type(Param, _, _), param(A, PA, PNum).
+
+%TypeVars bleiben einfach TypeVars:
+typeVar(Pointer) :- smallerArgGen(Pointer, T), typeVar(T).
+
+makeSmallerGenS(Pointer, T) :- smallerArgGen(Pointer, T), extendsWildcard(T).
+makeGreaterGenS(Pointer, T) :- smallerArgGen(Pointer, T), superWildcard(T).
+makeSmallerGenS(Pointer, T),
+makeGreaterGenS(Pointer, T),
+makeSameGenS(Pointer, T)
+:- smallerArgGen(Pointer, T), not extendsWildcard(T), not superWildcard(T), type(T, N, Num).
+
+greaterGen(P, T) :- makeGreaterGenS(P, T).
+extendsWildcard(P) :- makeGreaterGenS(P, T).
+
+smallerGen(P, T) :- makeSmallerGenS(P, T).
+superWildcard(P) :- makeSmallerGenS(P, T).
+
+{ smallerGen(P, T, TFC, TFC) : smaller(TFC, _), type(TFC, TN, TNum) } == 1 :- makeSameGenS(P, T), type(T, TN, TNum).
+
+
+%%%
+% Grundlegende Regeln
+%%%
+smaller(A, A) :- smaller(A, _).
+smaller(B, B) :- smaller(_, B).
+%smaller(A, A) :- type(A). %Alle Typen erben von sich selber. Hätte komische Nebeneffekte
+
+%Mapping:
+mapFC(smaller(A,B), Num, Num2) :- smaller(A,B), param(A, P, Num), typeVar(P), param(B, P, Num2).
+
+hasTypeInParameterList(A) :- type(A, _, _), param(A, P, _), type(P, _, _).
+mapRootFC(smaller(A,B), Num, Num2) :- smaller(A, B), not hasTypeInParameterList(A), param(A, P, Num), typeVar(P), param(B, P, Num2).
+

asp/fc.lp.old

@@ -0,0 +1,110 @@
+
+wildcard(A) :- extendsWildcard(A).
+wildcard(A) :- superWildcard(A).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%Anzahl der Wildcards ist 1
+% Mehr benötigt man nicht verschachtelt
+% Dadurch ist numWildcards unnötig, man ändert einfach die grArg auf Wildcards
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+type(P, TN, TNum) :- makeSameGen(P, T), type(T, TN, TNum).
+param(P, TN, TNum) :- makeSameGen(P, T), param(T, TN, TNum).
+superWildcard(P) :- makeSameGen(P, T), superWildcard(T).
+extendsWildcard(P) :- makeSameGen(P, T), extendsWildcard(T).
+
+%%%%%%%%%%%%%%%%%
+% Greater
+%%%%%%%%%%%%%%%%
+{ greaterGen(P, A, AFC, BFC) : smaller(AFC, BFC), type(AFC, AN, ANum) } == 1 :- greaterGen(P, A), type(A, AN, ANum)
+.
+
+type(P, BN, BNum) :- greaterGen(P, A, _, B), type(B, BN, BNum).
+%Bei den Parametern gibt es zwei Fälle:
+%% Die TPHs müssen gemapt werden, die anderen übernommen
+greaterArgGen(pointer(P, Param), Param) :- greaterGen(P, A, Afc, B), param(A, Param, PNum), mapFC(smaller(Afc, B), PNum, _).
+greaterArgGen(pointer(P, Param), Param) :- greaterGen(P, A, _, B), param(B, Param, PNum), type(B, _, _).
+param(P, pointer(P, Param), PNum) :- greaterGen(P, A, _, B), param(B, Param, PNum)
+	, type(Param, _, _)
+	.
+param(P, pointer(P, Param), PNum2) :- greaterGen(P, A, Afc, B), param(A, Param, PNum)
+	, mapFC(smaller(Afc,B), PNum, PNum2)
+	.
+
+%TypeVars bleiben einfach TypeVars:
+typeVar(Pointer) :- greaterArgGen(Pointer, T), typeVar(T).
+
+%makeGreaterGen(Pointer, T) :- greaterArgGen(Pointer, T), extendsWildcard(T).
+%makeSmallerGen(Pointer, T) :- greaterArgGen(Pointer, T), superWildcard(T).
+makeSameGen(Pointer, T) :- greaterArgGen(Pointer, T), extendsWildcard(T).
+makeSameGen(Pointer, T) :- greaterArgGen(Pointer, T), superWildcard(T).
+makeSmallerGenG(Pointer, T),
+makeGreaterGenG(Pointer, T),
+makeSameGenG(Pointer, T)
+:- greaterArgGen(Pointer, T), not extendsWildcard(T), not superWildcard(T), type(T, N, Num).
+
+greaterGen(P, T) :- makeGreaterGenG(P, T).
+extendsWildcard(P) :- makeGreaterGenG(P, T).
+
+smallerGen(P, T) :- makeGreaterGenG(P, T).
+superWildcard(P) :- makeSmallerGenG(P, T).
+
+{ greaterGen(P, T, TFC, TFC) : smaller(TFC, _), type(TFC, TN, TNum) } == 1 :- makeSameGenG(P, T), type(T, TN, TNum).
+
+greaterArgGenNum(P, 0) :- greaterArgGen(P, _), type(P, _ ,_).
+greaterArgGenNum(pointer(P, P2), Num + 1) :- greaterArgGen(pointer(P, P2),_), greaterArgGenNum(P, Num).
+
+
+%%%%%%%%%%%%%%%%%
+% smaller
+%%%%%%%%%%%%%%%%
+{ smallerGen(P, A, AFC, BFC) : smaller(BFC, AFC), type(AFC, AN, ANum) } == 1 :- smallerGen(P, A), type(A, AN, ANum)
+.
+{ type(P, BN, BNum) : type(B,BN,BNum) } == 1 :- smallerGen(P, A, _, B).
+%Bei den Parametern gibt es drei Fälle:
+%% Die TPHs müssen gemapt werden, die anderen übernommen
+smallerArgGen(pointer(P, Param), Param) :- smallerGen(P, A, Afc, B), param(A, Param, PNum), mapFC(smaller(B, Afc), _, PNum).
+param(P, pointer(P, Param), PNum2) :- smallerGen(P, A, Afc, B), param(A, Param, PNum)
+	, mapFC(smaller(B,Afc), PNum2, PNum) 
+	.
+
+%Neue Parameter können hinzu kommen: TODO
+%smallerArgGen(pointer(P, Param), Param) :- smallerGen(P, A, _, B), param(B, Param, PNum).
+%param(P, pointer(P, Param), PNum) :- greaterGen(P, A, _, B), param(B, Param, PNum)
+%	%, type(Param, _, _) %Es ist egal ob es ein Typparameter oder eine TypeVar ist. smallerArgGen macht das richtige
+%	.
+
+%Es können voraussetzungen hinzukommen:
+equals(Param, PA) :- smallerGen(P, A, Afc, B), param(Afc, Param, PNum), type(Param, _, _), param(A, PA, PNum).
+
+%TypeVars bleiben einfach TypeVars:
+typeVar(Pointer) :- smallerArgGen(Pointer, T), typeVar(T).
+
+makeSameGen(Pointer, T) :- smallerArgGen(Pointer, T), extendsWildcard(T).
+makeSameGen(Pointer, T) :- smallerArgGen(Pointer, T), superWildcard(T).
+makeSmallerGenS(Pointer, T),
+makeGreaterGenS(Pointer, T),
+makeSameGenS(Pointer, T)
+:- smallerArgGen(Pointer, T), not extendsWildcard(T), not superWildcard(T), type(T, N, Num).
+
+greaterGen(P, T) :- makeGreaterGenS(P, T).
+extendsWildcard(P) :- makeGreaterGenS(P, T).
+
+smallerGen(P, T) :- makeSmallerGenS(P, T).
+superWildcard(P) :- makeSmallerGenS(P, T).
+
+{ smallerGen(P, T, TFC, TFC) : smaller(TFC, _), type(TFC, TN, TNum) } == 1 :- makeSameGenS(P, T), type(T, TN, TNum).
+
+
+%%%
+% Grundlegende Regeln
+%%%
+smaller(A, A) :- smaller(A, _).
+smaller(B, B) :- smaller(_, B).
+%smaller(A, A) :- type(A). %Alle Typen erben von sich selber. Hätte komische Nebeneffekte
+
+%Mapping:
+mapFC(smaller(A,B), Num, Num2) :- smaller(A,B), param(A, P, Num), typeVar(P), param(B, P, Num2).
+
+hasTypeInParameterList(A) :- type(A, _, _), param(A, P, _), type(P, _, _).
+mapRootFC(smaller(A,B), Num, Num2) :- smaller(A, B), not hasTypeInParameterList(A), param(A, P, Num), typeVar(P), param(B, P, Num2).
+

asp/greater.pl

@@ -0,0 +1,17 @@
+{ fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)) : type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8) } == 1 :- greaterGen(V1,V2).
+{ fun19(typeVar(V15),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : typeVar(V15) ; fun20(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : notSuper(V15), notExtends(V15), type(V15,V16,V17) ; fun21(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : notSuper(V15), notExtends(V15), type(V15,V16,V17) ; fun22(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : notSuper(V15), extendsWildcard(V15), type(V15,V16,V17) ; fun23(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : notSuper(V15), notExtends(V15), type(V15,V16,V17) ; fun24(superWildcard(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)) : superWildcard(V15), notExtends(V15), type(V15,V16,V17) } == 1 :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14).
+param(V2,V15,V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), typeVar(V15), fun19(typeVar(V15),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+param(V2,V15,V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun20(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+superWildcard(pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun21(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+param(V2,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun21(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+smallerGen(V15,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun21(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+superWildcard(pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun22(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+param(V2,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun22(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+smallerGen(V15,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun22(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+extendsWildcard(pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun23(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+param(V2,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun23(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+greaterGen(V15,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun23(notSuper(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+extendsWildcard(pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun24(superWildcard(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+param(V2,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun24(superWildcard(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+greaterGen(V15,pointer(greaterGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)), param(V1,V15,V13), pi(V7,V8,V13,V14), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun24(superWildcard(V15),notExtends(V15),type(V15,V16,V17),greaterGen(V1,V2),greaterGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)),param(V1,V15,V13),pi(V7,V8,V13,V14)).
+type(V2,V9,V12) :- greaterGen(V1,V2), greaterGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V7,V8), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V7,V8),greaterGen(V1,V2)).

asp/pi.pl

@@ -0,0 +1,4 @@
+pi(V1,V2,V4,V5) :- typeVar(V3), param(V1,V3,V4), param(V2,V3,V5), type(V1,V10,V8), param(V1,V9,V7), typeVar(V9), V7 = 1 .. V8, type(V2,V14,V12), param(V2,V13,V11), typeVar(V13), V11 = 1 .. V12.
+
+notSuper(V1) :- type(V1,_,_), not superWildcard(V1).
+notExtends(V1) :- type(V1,_,_), not extendsWildcard(V1).

asp/reduceRules.lp

@@ -0,0 +1,44 @@
+
+%%%%%%%%%%%%%%%%%%%%
+% reduce1
+%%%%%%%%%%%%%%%%%%%%
+smallerDotWC(CP, DP)
+:- smallerDot(C, D), type(C, CN, NP), type(D, DN, NP)
+	, type(CFC, CN, NP), type(DFC, DN, NP), smaller(CFC, DFC)
+	, pi(CFC, DFC, N, N2)
+	, param(C, CP, N), param(D, DP, N2), N = 1 .. NP
+	.
+
+
+%%%%%%%%%%%%%%%%%%%%
+% reduceExt
+%%%%%%%%%%%%%%%%%%%%
+%TODO
+%smallerDotWC(CP, DP)
+%:- smallerDotWC(C, D), type(C, CN, NP), type(D, DN, NP)
+	%, type(CFC, CN, NP), type(DFC, DN, NP), smaller(CFC, DFC)
+	%, pi(CFC, DFC, N, N2)
+	%, param(C, CP, N), param(D, DP, N2), N = 1 .. NP
+	%.
+
+
+%%%%%%%%%%%%%%%%%%%%
+% reduceEq
+%%%%%%%%%%%%%%%%%%%%
+equals(CP, DP)
+:- smallerDot(C, D), type(C, CN, NP), type(D, CN, NP)
+	, param(C, CP, N), param(D, DP, N), N = 1 .. NP
+	.
+
+
+%%%%%%%%%%%%%%%%%%%%
+% reduce2
+%%%%%%%%%%%%%%%%%%%%
+equals(P1, P2) :- equals(C, D), type(C, CN, NP), type(D, CN, NP)
+	, param(C, P1, N), param(D, P2, N)
+	.
+
+%%%%%%%%%%%%%%%%%%%%
+% swap
+%%%%%%%%%%%%%%%%%%%%
+equals(A, B) :- equals(B, A), typeVar(A), not typeVar(B).

asp/result.lp

@@ -0,0 +1 @@
+:- equals(A, B), equals(A, C), type(B,BN,_), type(C,CN,_), CN != BN.

asp/rule5.test

@@ -0,0 +1,291 @@
+param(cEPQ,cAEG,1).
+param(cEQX,cAEG,1).
+param(cEQE,cAEG,1).
+typeVar(cBFS).
+type(cEON,cjava_DOT_io_DOT_Serializable,0).
+constraint(cESK,list(equals(cESN,cM),list(smallerDot(cL,cESM),list(smallerDot(cESL,cQC),null)))).
+type(cESM,cjava_DOT_util_DOT_ArrayList,1).
+param(cERA,cDKY,1).
+param(cEQM,cDKY,1).
+type(cEQE,cjava_DOT_util_DOT_List,1).
+type(cEQI,cjava_DOT_util_DOT_Collection,1).
+type(cEPS,cjava_DOT_util_DOT_AbstractList,1).
+param(cEQD,cBFS,1).
+type(cEPQ,cjava_DOT_lang_DOT_Iterable,1).
+type(cEOM,cjava_DOT_util_DOT_ArrayList,1).
+smaller(cEOW,cEOX).
+type(cEPV,cjava_DOT_lang_DOT_Object,0).
+param(cERQ,cCII,1).
+param(cEPY,cDKY,1).
+smaller(cEPM,cEPN).
+param(cEOQ,cBFS,1).
+smaller(cEQC,cEQD).
+type(cERM,cjava_DOT_util_DOT_Vector,1).
+param(cESJ,cQF,1).
+type(cESN,cjava_DOT_lang_DOT_Boolean,0).
+smaller(cEPI,cEPJ).
+type(cERJ,cjava_DOT_util_DOT_Collection,1).
+type(cEQA,cjava_DOT_util_DOT_ArrayList,1).
+type(cEOA,cjava_DOT_util_DOT_ArrayList,1).
+param(cEOT,cBFS,1).
+type(cEOW,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cEPC,cCII,1).
+type(cEQB,cjava_DOT_util_DOT_AbstractList,1).
+param(cENS,cCII,1).
+type(cEQS,cjava_DOT_util_DOT_Collection,1).
+typeVar(cDKY).
+type(cEPU,cjava_DOT_util_DOT_AbstractCollection,1).
+smaller(cEQG,cEQH).
+type(cEQJ,cjava_DOT_lang_DOT_Object,0).
+param(cEQG,cCII,1).
+param(cEPN,cCII,1).
+param(cESE,cDKY,1).
+param(cEQZ,cBFS,1).
+type(cERK,cjava_DOT_util_DOT_Vector,1).
+smaller(cEPE,cEPF).
+type(cEOK,cjava_DOT_util_DOT_ArrayList,1).
+typeVar(cQC).
+smaller(cERE,cERF).
+param(cEOA,cCII,1).
+type(cEQQ,cjava_DOT_lang_DOT_Iterable,1).
+smaller(cEPA,cEPB).
+typeVar(cM).
+smaller(cERA,cERB).
+type(cEPP,cjava_DOT_lang_DOT_Object,0).
+param(cEPS,cCII,1).
+param(cENQ,cAEG,1).
+param(cEPH,cCII,1).
+smaller(cERW,cERX).
+type(cEOG,cjava_DOT_util_DOT_Collection,1).
+type(cERE,cjava_DOT_io_DOT_Serializable,0).
+param(cERG,cDKY,1).
+smaller(cERS,cERT).
+param(cEOF,cBFS,1).
+type(cESA,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cERY,cDKY,1).
+typeVar(cCII).
+type(cEOO,cjava_DOT_util_DOT_Collection,1).
+type(cERN,cjava_DOT_lang_DOT_Cloneable,0).
+param(cENO,cBFS,1).
+typeVar(cAEG).
+type(cERB,cjava_DOT_lang_DOT_Object,0).
+typeVar(cQD).
+param(cEQP,cAEG,1).
+param(cEOO,cAEG,1).
+type(cESF,cjava_DOT_io_DOT_Serializable,0).
+param(cEPE,cBFS,1).
+type(cEPG,cjava_DOT_util_DOT_ArrayList,1).
+type(cEPD,cjava_DOT_util_DOT_Collection,1).
+type(cERC,cjava_DOT_util_DOT_AbstractCollection,1).
+type(cERQ,cjava_DOT_util_DOT_ArrayList,1).
+type(cENW,cjava_DOT_lang_DOT_Iterable,1).
+type(cENQ,cjava_DOT_util_DOT_ArrayList,1).
+smaller(cESC,cESD).
+type(cEOU,cjava_DOT_util_DOT_List,1).
+smaller(cENO,cENP).
+smaller(cEOE,cEOF).
+smaller(cERO,cERP).
+type(cEPH,cjava_DOT_util_DOT_List,1).
+smaller(cESE,cESF).
+param(cERO,cCII,1).
+param(cEOS,cBFS,1).
+type(cEQX,cjava_DOT_util_DOT_List,1).
+type(cEQR,cjava_DOT_lang_DOT_Object,0).
+param(cEQY,cBFS,1).
+smaller(cEQW,cEQX).
+smaller(cEOC,cEOD).
+smaller(cERM,cERN).
+param(cEPT,cCII,1).
+param(cEQQ,cBFS,1).
+param(cERZ,cDKY,1).
+type(cENV,cjava_DOT_util_DOT_AbstractCollection,1).
+type(cEOZ,cjava_DOT_lang_DOT_Object,0).
+param(cEQK,cAEG,1).
+type(cEQO,cjava_DOT_util_DOT_AbstractList,1).
+type(cEQU,cjava_DOT_util_DOT_Vector,1).
+smaller(cEOK,cEOL).
+type(cEQW,cjava_DOT_util_DOT_ArrayList,1).
+type(cENO,cjava_DOT_util_DOT_ArrayList,1).
+type(cERF,cjava_DOT_lang_DOT_Object,0).
+param(cEPA,cCII,1).
+type(cERV,cjava_DOT_io_DOT_Serializable,0).
+smaller(cERG,cERH).
+param(cEOU,cCII,1).
+param(cENU,cDKY,1).
+param(cESM,cQE,1).
+param(cEOP,cAEG,1).
+param(cEPO,cBFS,1).
+param(cEOK,cBFS,1).
+constraint(cESG,list(smallerDot(cL,cESJ),list(equals(cESI,cM),list(smallerDot(cESH,cQD),null)))).
+type(cEPE,cjava_DOT_util_DOT_ArrayList,1).
+param(cEQF,cAEG,1).
+smaller(cEPY,cEPZ).
+param(cESC,cDKY,1).
+param(cENY,cAEG,1).
+param(cEOM,cAEG,1).
+smaller(cEQO,cEQP).
+type(cEOR,cjava_DOT_lang_DOT_Object,0).
+type(cESC,cjava_DOT_util_DOT_List,1).
+type(cEOP,cjava_DOT_lang_DOT_Iterable,1).
+type(cERU,cjava_DOT_util_DOT_ArrayList,1).
+type(cERY,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cEPL,cAEG,1).
+param(cEOX,cAEG,1).
+type(cEQK,cjava_DOT_util_DOT_ArrayList,1).
+type(cERZ,cjava_DOT_util_DOT_Collection,1).
+param(cEQA,cBFS,1).
+param(cERI,cDKY,1).
+smaller(cEPC,cEPD).
+type(cEQT,cjava_DOT_lang_DOT_Iterable,1).
+type(cERT,cjava_DOT_lang_DOT_Object,0).
+type(cEOY,cjava_DOT_lang_DOT_Cloneable,0).
+param(cEQU,cDKY,1).
+type(cEPB,cjava_DOT_util_DOT_AbstractCollection,1).
+type(cESI,cjava_DOT_lang_DOT_Boolean,0).
+smaller(cENU,cENV).
+type(cESE,cjava_DOT_util_DOT_Vector,1).
+param(cEOG,cCII,1).
+type(cEOI,cjava_DOT_util_DOT_List,1).
+type(cENU,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cERU,cERV).
+type(cEPN,cjava_DOT_util_DOT_AbstractList,1).
+type(cEQV,cjava_DOT_util_DOT_List,1).
+type(cEPA,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cEPQ,cEPR).
+type(cEQL,cjava_DOT_util_DOT_AbstractList,1).
+param(cEQH,cCII,1).
+type(cEOL,cjava_DOT_lang_DOT_Cloneable,0).
+type(cEQY,cjava_DOT_util_DOT_AbstractList,1).
+type(cEOF,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cEQT,cBFS,1).
+smaller(cEOS,cEOT).
+type(cENR,cjava_DOT_lang_DOT_Cloneable,0).
+type(cEQD,cjava_DOT_util_DOT_Collection,1).
+type(cENZ,cjava_DOT_lang_DOT_Object,0).
+param(cEPG,cCII,1).
+type(cEQF,cjava_DOT_util_DOT_Collection,1).
+type(cEQN,cjava_DOT_util_DOT_List,1).
+type(cEQH,cjava_DOT_util_DOT_Collection,1).
+smaller(cEOY,cEOZ).
+type(cERR,cjava_DOT_lang_DOT_Cloneable,0).
+param(cERU,cCII,1).
+type(cESB,cjava_DOT_lang_DOT_Object,0).
+smaller(cEPO,cEPP).
+param(cEPU,cDKY,1).
+param(cEQI,cDKY,1).
+smaller(cEQE,cEQF).
+smaller(cEQA,cEQB).
+type(cEPM,cjava_DOT_util_DOT_ArrayList,1).
+param(cENW,cCII,1).
+param(cEOE,cBFS,1).
+type(cEOX,cjava_DOT_util_DOT_Collection,1).
+type(cEQG,cjava_DOT_util_DOT_List,1).
+param(cERH,cDKY,1).
+smaller(cEQI,cEQJ).
+param(cEOC,cAEG,1).
+type(cEPT,cjava_DOT_util_DOT_List,1).
+type(cEOT,cjava_DOT_util_DOT_Collection,1).
+type(cERP,cjava_DOT_lang_DOT_Object,0).
+type(cERS,cMyVector,0).
+type(cESD,cjava_DOT_lang_DOT_Object,0).
+type(cEOD,cjava_DOT_util_DOT_RandomAccess,0).
+smaller(cEPK,cEPL).
+type(cEPK,cjava_DOT_util_DOT_AbstractList,1).
+param(cERM,cDKY,1).
+smaller(cEPG,cEPH).
+type(cEOS,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cEQS,cBFS,1).
+param(cEQW,cAEG,1).
+type(cENY,cjava_DOT_util_DOT_Collection,1).
+param(cEPW,cBFS,1).
+type(cEOJ,cjava_DOT_lang_DOT_Object,0).
+param(cEQC,cBFS,1).
+type(cENT,cjava_DOT_lang_DOT_Iterable,1).
+param(cERK,cDKY,1).
+type(cEPY,cjava_DOT_util_DOT_Vector,1).
+type(cEQM,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cENW,cENX).
+smaller(cEPW,cEPX).
+smaller(cEOM,cEON).
+smaller(cEQM,cEQN).
+smaller(cEPS,cEPT).
+type(cENX,cjava_DOT_lang_DOT_Object,0).
+smallerDot(cL,cK).
+type(cESJ,cjava_DOT_util_DOT_Vector,1).
+type(cEQC,cjava_DOT_util_DOT_List,1).
+type(cEOB,cjava_DOT_util_DOT_RandomAccess,0).
+smaller(cEOU,cEOV).
+param(cERC,cAEG,1).
+smaller(cEQU,cEQV).
+type(cERG,cjava_DOT_util_DOT_Collection,1).
+type(cESH,cjava_DOT_lang_DOT_Object,0).
+smaller(cEOQ,cEOR).
+oder(cESG,cESK).
+smaller(cEQQ,cEQR).
+param(cEPD,cCII,1).
+type(cEPZ,cjava_DOT_util_DOT_AbstractList,1).
+param(cEQL,cAEG,1).
+type(cEPC,cjava_DOT_util_DOT_AbstractCollection,1).
+smaller(cENS,cENT).
+param(cESA,cBFS,1).
+type(cERA,cjava_DOT_lang_DOT_Iterable,1).
+smaller(cEQY,cEQZ).
+typeVar(cQE).
+type(cEOE,cjava_DOT_util_DOT_AbstractList,1).
+type(cESL,cjava_DOT_lang_DOT_Object,0).
+type(cERX,cjava_DOT_lang_DOT_Object,0).
+type(cENP,cjava_DOT_util_DOT_List,1).
+type(cEPI,cjava_DOT_util_DOT_RandomAccess,0).
+typeVar(cK).
+smaller(cERK,cERL).
+type(cERD,cjava_DOT_lang_DOT_Object,0).
+type(cERI,cjava_DOT_util_DOT_List,1).
+type(cEPJ,cjava_DOT_lang_DOT_Object,0).
+smaller(cESA,cESB).
+type(cEOC,cjava_DOT_util_DOT_ArrayList,1).
+param(cEOW,cAEG,1).
+param(cERJ,cDKY,1).
+param(cEQB,cBFS,1).
+smaller(cEOI,cEOJ).
+type(cEPL,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cEQO,cAEG,1).
+smaller(cERI,cERJ).
+typeVar(cQF).
+param(cEPK,cAEG,1).
+param(cENP,cBFS,1).
+type(cERO,cjava_DOT_util_DOT_AbstractCollection,1).
+typeVar(cL).
+smaller(cEOG,cEOH).
+param(cEQV,cDKY,1).
+type(cERW,cjava_DOT_lang_DOT_Object,0).
+type(cEQZ,cjava_DOT_util_DOT_List,1).
+type(cENS,cjava_DOT_util_DOT_Collection,1).
+smaller(cENY,cENZ).
+param(cEOI,cAEG,1).
+smaller(cEOO,cEOP).
+smaller(cERY,cERZ).
+param(cEPZ,cDKY,1).
+param(cEQN,cDKY,1).
+smaller(cEQK,cEQL).
+type(cEOH,cjava_DOT_lang_DOT_Object,0).
+type(cEPF,cjava_DOT_util_DOT_RandomAccess,0).
+smaller(cERC,cERD).
+type(cEPO,cjava_DOT_util_DOT_List,1).
+type(cEPR,cjava_DOT_lang_DOT_Object,0).
+type(cEQP,cjava_DOT_util_DOT_List,1).
+smaller(cEQS,cEQT).
+type(cERL,cjava_DOT_util_DOT_RandomAccess,0).
+param(cENT,cCII,1).
+type(cEOQ,cjava_DOT_util_DOT_Collection,1).
+type(cEPW,cjava_DOT_util_DOT_ArrayList,1).
+type(cEPX,cjava_DOT_io_DOT_Serializable,0).
+smaller(cEPU,cEPV).
+smaller(cEOA,cEOB).
+type(cEOV,cjava_DOT_lang_DOT_Object,0).
+param(cEPB,cCII,1).
+smaller(cENQ,cENR).
+param(cEPM,cCII,1).
+smaller(cERQ,cERR).
+param(cENV,cDKY,1).
+type(cERH,cjava_DOT_lang_DOT_Iterable,1).
+

asp/smaller.pl

@@ -0,0 +1,15 @@
+{ fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)) : type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7) } == 1 :- smallerGen(V1,V2).
+{ fun19(typeVar(V15),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : typeVar(V15) ; fun20(notSuper(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : notSuper(V15), notExtends(V15), type(V15,V16,V17) ; fun21(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : superWildcard(V15), notExtends(V15), type(V15,V16,V17) ; fun22(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : superWildcard(V15), notExtends(V15), type(V15,V16,V17) ; fun23(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : notSuper(V15), extendsWildcard(V15), type(V15,V16,V17) ; fun24(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)) : notSuper(V15), extendsWildcard(V15), type(V15,V16,V17) } == 1 :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13).
+param(V2,V15,V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), typeVar(V15), fun19(typeVar(V15),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+param(V2,V15,V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), notExtends(V15), type(V15,V16,V17), fun20(notSuper(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+param(V2,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun21(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+greaterGen(V15,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun21(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+superWildcard(pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun22(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+param(V2,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun22(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+greaterGen(V15,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), superWildcard(V15), notExtends(V15), type(V15,V16,V17), fun22(superWildcard(V15),notExtends(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+extendsWildcard(pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun23(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+param(V2,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun23(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+smallerGen(V15,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun23(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+param(V2,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17)),V14) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun24(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+smallerGen(V15,pointer(smallerGen(V1,V2), notSuper(V15), notExtends(V15), type(V15,V16,V17))) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)), param(V1,V15,V13), pi(V8,V7,V14,V13), notSuper(V15), extendsWildcard(V15), type(V15,V16,V17), fun24(notSuper(V15),extendsWildcard(V15),type(V15,V16,V17),smallerGen(V1,V2),smallerGen(V1,V2),type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)),param(V1,V15,V13),pi(V8,V7,V14,V13)).
+type(V2,V9,V12) :- smallerGen(V1,V2), smallerGen(V1,V2), type(V1,V10,V11), type(V7,V10,V11), type(V8,V9,V12), smaller(V8,V7), fun18(type(V1,V10,V11),type(V7,V10,V11),type(V8,V9,V12),smaller(V8,V7),smallerGen(V1,V2)).

asp/step4.lp

@@ -0,0 +1,116 @@
+wildcard(A) :- superWildcard(A).
+wildcard(A) :- extendsWildcard(A).
+
+%Problem hier: Es gibt in der FiniteClosure nun smaller Beziehungen der Art:
+%%(Matrix<A> <) Vector<Vector<A>> < List<Vector<A>>
+%Mit diesen funktioniert die Unifikation in Schritt 4 des Algorithmus nicht korrekt.
+%Lösung: Man könnte es lösen mit:
+%typeVarOnly(TP) :- type(TP, _, PN), {notTypeVarOnly(TP, A) : param(TP, A, _), type(A, _, _)} == 0.
+
+% Die Karthesischen Produkte von Schritt 4 des Unifikationsalgorithmus
+
+{ makeRule1(A,TP,TPFC, SmallerType) : smaller(SmallerType, TPFC), type(TPFC, TypeName, NumParams) } = 1
+:- smallerDot(A, TP), type(TP, TypeName, NumParams), typeVar(A).%, smaller(_, TPFC), type(TPFC, TypeName, NumParams).
+
+%:- makeRule1(A, B, C,_), makeRule1(A,B,D,_), D != C.
+
+%Alle Greater Arg Paralisten des Typen C generieren
+greaterArgParaList(pointer(rule1(A, TP)), TPFC) :- makeRule1(A,TP,TPFC,_).
+
+%Es braucht greaterArg Parameter von allen Parametern des Typs:
+greaterArg(pointer(P, Param), Param)  :- greaterArgParaList(P, FCType), type(FCType, FCTName, FCTPN), param(FCType, Param, Num), not typeVar(Param).
+
+%Ein neuer Typ muss angelegt werden:
+type(P, FCTName, FCTPN) 
+:- greaterArgParaList(P, FCType), type(FCType, FCTName, FCTPN).
+
+param(P, pointer(P, Param), N)
+:- greaterArgParaList(P, FCType), type(FCType, FCTName, FCTPN)
+	, param(FCType, Param, N), not typeVar(Param)
+	.
+%Typvariablen bleiben bestehen. Sie werden durch das unify ausgetauscht
+param(P, Param, N)
+:- greaterArgParaList(P, FCType), type(FCType, FCTName, FCTPN)
+	, param(FCType, Param, N), typeVar(Param)
+	.
+
+
+%Die Unifikation vom AusgangsTyp im Constraint und dem greaterArgList gebildeten Typen
+unify(pointer(rule1unify(A,TP)), pointer(rule1(A,TP)), TP) 
+:- makeRule1(A,TP,TPFC, _).
+
+%Unify auf den SmallerType anwenden:
+type(pointer(rule1unify(A,TP,TPFC,SmallerType)), TN, TNum)
+:- makeRule1(A, TP, TPFC, SmallerType), type(SmallerType, TN, TNum).
+
+{ param(pointer(rule1unify(A,TP,TPFC,SmallerType)), PNew, PN) : unify(pointer(rule1unify(A,TP)), P, PNew)} == 1
+:- makeRule1(A, TP, TPFC, SmallerType), param(SmallerType, P, PN).
+
+%Am Schluss davon noch das smaller bilden:
+smallerGen(pointer(smallerDot(A,TP), SmallerType), pointer(rule1unify(A,TP,TPFC,SmallerType)))
+:- makeRule1(A, TP, TPFC, SmallerType), type(TP, TypeName, NumParams) %Die Bedingung für Regel 1
+	.
+
+smallerGen(A) :- list(smallerGen(A),_).
+type(A,B,C) :- list(type(A,B,C),_).
+list(A,B) :- list(_, list(A,B)).
+
+smallerGen(A,A) :- smallerGen(A).
+
+{ equals(A, NewType) : smallerGen(pointer(smallerDot(A,TP), SmallerType), NewType) } == 1
+:- smallerDot(A, TP), type(TP, TypeName, NumParams), typeVar(A) %Das karthesische Produkt
+	, smaller(SmallerType, TPFC), type(pointer(smallerDot(A,TP), SmallerType), _, _)
+ 	.
+
+%TODO: Typen welche durch Unifikation ersetzt werden auch zu Constraints machen
+%%%%%%%%%%%%%%%%%%
+% Regel 2
+%%%%%%%%%%%%%%%%%
+
+%{ makeRule2(A, Theta', TPFC) : smaller(SmallerType, TPFC), type(TPFC, TypeName, NumParams) } == 1
+%:- smallerDotWC(A, Theta'), extendsWildcard(Theta'), typeVar(A).
+%
+%%Alle Greater Arg Paralisten des Typen C generieren
+%greaterArgParaList(pointer(rule2(A, TP)), TPFC) :- makeRule2(A,TP,TPFC,_).
+%
+%unify(pointer(rule2(A,TP)), TP) 
+%:- makeRule2(A,TP,TPFC)
+%%	, type(TP, TypeName, NumParams), typeVar(A), type(TPFC, TypeName, NumParams)
+	%.
+%
+%{ list(smallerArgGen(pointer(smallerDot(A,TP), SmallerType), SmallerType),
+%list(extendsWildcard(pointer(smallerDot(A,TP), SmallerType)), null))
+%: smaller(SmallerType, TPFC), type(SmallerType, SmallerName, SmallerPNum) } == 1
+%:- makeRule2(A, TP, TPFC) %Die Bedingung für Regel 2
+	%.
+%
+%smallerArgGen(A, B) :- list(smallerArgGen(A, B), _).
+%extendsWildcard(A) :- list(extendsWildcard(A), _).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Regel 3
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+smallerArgGen(pointer(smallerDotWC(A, Theta')), Theta') :- smallerDotWC(A, Theta'), superWildcard(Theta').
+equals(A, pointer(smallerDotWC(A, Theta'))) :- smallerDotWC(A, Theta'), superWildcard(Theta').
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Regel 4
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+equals(A, Theta') :- smallerDotWC(A, Theta'), not wildcard(Theta').
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Regel 5
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+greaterGen(pointer(smallerDot(Theta,A)), Theta) :- smallerDot(Theta, A), not wildcard(Theta), not typeVar(Theta), typeVar(A) .
+equals(A, pointer(smallerDot(Theta,A))) :- smallerDot(Theta, A), not wildcard(Theta) , not typeVar(Theta), typeVar(A) .
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Regel 6
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+greaterArgGen(pointer(smallerDotWC(Theta,A)), Theta) :- smallerDotWC(Theta, A), extendsWildcard(Theta) .
+equals(A, pointer(smallerDot(Theta,A))) :- smallerDotWC(Theta, A), extendsWildcard(Theta) .
+
+%TODO: Regel 7

asp/step4.test

@@ -0,0 +1,8 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Regel 5
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+greaterGen(pointer(smallerDot(Theta,A)), Theta) :- smallerDot(Theta, A), not wildcard(Theta), not typeVar(Theta), typeVar(A) .
+equals(A, pointer(smallerDot(Theta,A))) :- smallerDot(Theta, A), not wildcard(Theta) , not typeVar(Theta), typeVar(A) .
+
+

asp/subst.lp

@@ -0,0 +1,14 @@
+subst(TV,T) :- equals(TV, T), not occurs(TV, T), not typeVar(T), typeVar(TV).
+
+equals(A, pointer(TP, subst(TV, T)))
+:- equals(A, TP), subst(TV, T), not typeVar(TP), occurs(TV, TP).
+
+type(pointer(TP, subst(TV, T)), Name, Num)
+:- type(TP, Name, Num), subst(TV, T), occurs(TV, TP).
+
+param(pointer(TP, subst(TV, T)), Param, PNum)
+:- type(pointer(TP, subst(TV, T)), Name, Num), subst(TV, T), param(TP, Param, PNum), not occurs(TV, Param).
+
+param(pointer(TP, subst(TV, T)), pointer(Param, subst(TV, T)), PNum)
+:- type(pointer(TP, subst(TV, T)), Name, Num), subst(TV, T), param(TP, Param, PNum), occurs(TV, Param).
+

asp/testInput.lp

@@ -0,0 +1,219 @@
+typeVar(a).
+type(t1, cjava_DOT_util_DOT_Vector, 1).
+param(t1, t2, 1).
+type(t2, cjava_DOT_util_DOT_Vector, 1).
+param(t2, b, 1).
+typeVar(b).
+
+smallerDot(a, t1).
+
+
+typeFC(cBUF,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBQX,cAKH,1).
+typeFC(cBRW,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBRF,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBTR,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBTZ,cAKH,1).
+paramFC(cBUN,cAKH,1).
+typeFC(cBRY,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBUE,cBUF,1).
+paramFC(cBRL,cAKH,1).
+smaller(cBSB,cBSE).
+paramFC(cBTR,cBTS,1).
+smaller(cBQJ,cBQK).
+typeFC(cBQP,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBUA,cjava_DOT_util_DOT_Collection,1).
+typeFC(cBSD,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBUE,cjava_DOT_util_DOT_Collection,1).
+typeFC(cBUK,cjava_DOT_util_DOT_Collection,1).
+paramFC(cBTJ,cAKH,1).
+typeFC(cBRZ,cjava_DOT_lang_DOT_Integer,0).
+smaller(cBSF,cBSI).
+typeFC(cBRT,cjava_DOT_lang_DOT_Integer,0).
+paramFC(cBRX,cBRY,1).
+typeFC(cBRJ,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBRF,cBRG,1).
+typeFC(cBQN,cjava_DOT_lang_DOT_Integer,0).
+smaller(cBRL,cBRM).
+smaller(cBUH,cBUK).
+smaller(cBTR,cBTU).
+paramFC(cBUL,cBUM,1).
+smaller(cBRH,cBRI).
+typeFC(cBTV,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBSQ,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBUL,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBTX,cjava_DOT_lang_DOT_Object,0).
+paramFC(cBSN,cAKH,1).
+typeFC(cBTE,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBUC,cBUD,1).
+smaller(cBST,cBSU).
+paramFC(cBRI,cAKH,1).
+typeFC(cBSR,cjava_DOT_lang_DOT_Iterable,1).
+typeFC(cBRC,cjava_DOT_util_DOT_RandomAccess,0).
+typeFC(cBTL,cjava_DOT_util_DOT_Collection,1).
+typeFC(cBSF,cjava_DOT_util_DOT_AbstractList,1).
+typeFC(cBSX,cjava_DOT_util_DOT_AbstractList,1).
+paramFC(cBSI,cBSJ,1).
+typeFC(cBTH,cjava_DOT_util_DOT_Collection,1).
+paramFC(cBSV,cAKH,1).
+paramFC(cBQZ,cBRA,1).
+paramFC(cBQJ,cAKH,1).
+smaller(cBRD,cBRE).
+paramFC(cBRO,cBRP,1).
+typeFC(cBSI,cjava_DOT_util_DOT_List,1).
+typeFC(cBQX,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBUI,cBUJ,1).
+paramFC(cBQO,cBQP,1).
+typeFC(cBTA,cjava_DOT_util_DOT_AbstractCollection,1).
+paramFC(cBRJ,cAKH,1).
+paramFC(cBTV,cBTW,1).
+typeFC(cBUO,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBSA,cjava_DOT_lang_DOT_Object,0).
+smaller(cBUB,cBUE).
+typeFC(cBUD,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBQZ,cjava_DOT_util_DOT_Vector,1).
+smaller(cBTL,cBTO).
+typeFC(cBTU,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cBTZ,cBUA).
+typeFC(cBRG,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBSC,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBSK,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBST,cjava_DOT_util_DOT_AbstractList,1).
+paramFC(cBSY,cBSZ,1).
+typeFC(cBTW,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBQW,cjava_DOT_lang_DOT_Integer,0).
+smaller(cBSP,cBSQ).
+paramFC(cBSG,cBSH,1).
+smaller(cBTD,cBTG).
+typeFC(cBUG,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBSW,cjava_DOT_lang_DOT_Object,0).
+paramFC(cBTD,cBTE,1).
+paramFC(cBSX,cBSY,1).
+paramFC(cBQM,cBQN,1).
+typeFC(cBRH,cjava_DOT_util_DOT_AbstractCollection,1).
+smaller(cBSN,cBSO).
+paramFC(cBQK,cAKH,1).
+typeFC(cBTM,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBTU,cBTV,1).
+typeFC(cBQM,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBRA,cjava_DOT_util_DOT_Vector,1).
+smaller(cBSV,cBSW).
+typeFC(cBSO,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBSZ,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBQL,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBSL,cAKH,1).
+typeFC(cBRB,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBSY,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBUH,cBUI,1).
+paramFC(cBTH,cAKH,1).
+typeFC(cBTN,cjava_DOT_lang_DOT_Integer,0).
+smaller(cBRJ,cBRK).
+typeFC(cBRP,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBUH,cjava_DOT_util_DOT_List,1).
+paramFC(cBRE,cBRF,1).
+typeFC(cBQR,cjava_DOT_util_DOT_Collection,1).
+typeFC(cBTY,cjava_DOT_lang_DOT_Object,0).
+paramFC(cBQS,cBQT,1).
+typeFC(cBTI,cjava_DOT_lang_DOT_Iterable,1).
+typeFC(cBUC,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBSB,cBSC,1).
+typeFC(cBQS,cjava_DOT_util_DOT_Vector,1).
+smaller(cBQR,cBQU).
+paramFC(cBTE,cBTF,1).
+paramFC(cBUB,cBUC,1).
+typeFC(cBRO,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBST,cAKH,1).
+typeFC(cBQO,cjava_DOT_util_DOT_List,1).
+typeFC(cBRE,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBQY,cjava_DOT_io_DOT_Serializable,0).
+typeFC(cBTQ,cjava_DOT_lang_DOT_Object,0).
+smaller(cBSX,cBTA).
+typeFC(cBRN,cjava_DOT_util_DOT_AbstractCollection,1).
+typeVar(cAKH).
+paramFC(cBRH,cAKH,1).
+paramFC(cBQP,cBQQ,1).
+typeFC(cBSE,cjava_DOT_io_DOT_Serializable,0).
+smaller(cBTP,cBTQ).
+paramFC(cBRN,cBRO,1).
+typeFC(cBUI,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBRV,cjava_DOT_io_DOT_Serializable,0).
+typeFC(cBSJ,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBTK,cjava_DOT_util_DOT_RandomAccess,0).
+paramFC(cBSJ,cBSK,1).
+typeFC(cBQK,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cBUN,cBUO).
+typeFC(cBUB,cjava_DOT_util_DOT_AbstractCollection,1).
+paramFC(cBSR,cAKH,1).
+paramFC(cBSC,cBSD,1).
+paramFC(cBRA,cBRB,1).
+paramFC(cBRM,cAKH,1).
+paramFC(cBQR,cBQS,1).
+typeFC(cBSM,cjava_DOT_util_DOT_AbstractCollection,1).
+smaller(cBTH,cBTI).
+paramFC(cBTA,cBTB,1).
+smaller(cBQL,cBQO).
+typeFC(cBTB,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBUF,cBUG,1).
+paramFC(cBQL,cBQM,1).
+smaller(cBRN,cBRQ).
+smaller(cBRR,cBRU).
+smaller(cBQX,cBQY).
+typeFC(cBRM,cjava_DOT_util_DOT_List,1).
+typeFC(cBTZ,cjava_DOT_util_DOT_List,1).
+paramFC(cBTL,cBTM,1).
+typeFC(cBRI,cjava_DOT_util_DOT_Collection,1).
+typeFC(cBRK,cjava_DOT_lang_DOT_Cloneable,0).
+typeFC(cBTS,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBUN,cjava_DOT_util_DOT_Collection,1).
+paramFC(cBRR,cBRS,1).
+smaller(cBQZ,cBRC).
+smaller(cBRV,cBRW).
+smaller(cBSL,cBSM).
+typeFC(cBSB,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBSN,cjava_DOT_util_DOT_AbstractCollection,1).
+typeFC(cBTF,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBTG,cjava_DOT_lang_DOT_Object,0).
+paramFC(cBTI,cAKH,1).
+typeFC(cBSH,cjava_DOT_lang_DOT_Integer,0).
+paramFC(cBTM,cBTN,1).
+paramFC(cBSM,cAKH,1).
+typeFC(cBTD,cjava_DOT_util_DOT_List,1).
+typeFC(cBTJ,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBQJ,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBQU,cjava_DOT_lang_DOT_Iterable,1).
+paramFC(cBSF,cBSG,1).
+typeFC(cBTC,cjava_DOT_lang_DOT_Integer,0).
+paramFC(cBQU,cBQV,1).
+typeFC(cBTT,cjava_DOT_lang_DOT_Integer,0).
+paramFC(cBUK,cBUL,1).
+paramFC(cBUA,cAKH,1).
+typeFC(cBUM,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBQT,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBSL,cjava_DOT_util_DOT_AbstractList,1).
+smaller(cBSR,cBSS).
+typeFC(cBUJ,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBQQ,cjava_DOT_lang_DOT_Integer,0).
+typeFC(cBRD,casp_DOT_UnifyWithoutWildcards_DOLLAR_MatrixTest,0).
+paramFC(cBSU,cAKH,1).
+typeFC(cBSU,cjava_DOT_util_DOT_List,1).
+typeFC(cBTP,cjava_DOT_util_DOT_RandomAccess,0).
+typeFC(cBRQ,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBRX,cjava_DOT_lang_DOT_Iterable,1).
+typeFC(cBQV,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBSG,cjava_DOT_util_DOT_Vector,1).
+paramFC(cBRY,cBRZ,1).
+typeFC(cBSV,cjava_DOT_util_DOT_List,1).
+smaller(cBRX,cBSA).
+typeFC(cBRS,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBRL,cjava_DOT_util_DOT_Vector,1).
+typeFC(cBRR,cjava_DOT_util_DOT_Vector,1).
+smaller(cBTJ,cBTK).
+typeFC(cBRU,cjava_DOT_lang_DOT_Cloneable,0).
+paramFC(cBRS,cBRT,1).
+paramFC(cBTB,cBTC,1).
+paramFC(cBTS,cBTT,1).
+typeFC(cBSP,cjava_DOT_lang_DOT_Cloneable,0).
+smaller(cBTX,cBTY).
+paramFC(cBQV,cBQW,1).
+typeFC(cBSS,cjava_DOT_lang_DOT_Object,0).
+typeFC(cBTO,cjava_DOT_lang_DOT_Object,0).

asp/testReduce.lp

@@ -0,0 +1,28 @@
+equals(t1, t2). % Map<Object, Integer> =. Map<Integer, Object>
+%smallerDot(t2, t1).
+
+type(t1, cMap, 2).
+type(t2, cMap, 2).
+%type(t2, cHashMap, 2).
+param(t1, t3, 1).
+param(t1, t4, 2).
+param(t2, t6, 1).
+param(t2, t5, 2).
+
+type(t3, cObject, 0).
+type(t5, cInteger, 0).
+typeVar(t4).
+typeVar(t6).
+
+type(tfc1, cMap, 2).
+type(tfc2, cHashMap, 2).
+param(tfc1, gA, 1).
+param(tfc1, gB, 2).
+param(tfc2, gB, 1).
+param(tfc2, gA, 2).
+typeVar(gA).
+typeVar(gB).
+smaller(tfc2, tfc1).
+smaller(tfc1, tfc1).
+
+#show equals/2.

asp/testUnifikation.lp

@@ -0,0 +1,12 @@
+type(t1, cjava_DOT_util_DOT_Vector, 1).
+param(t1, t2, 1).
+type(t2, cjava_DOT_util_DOT_Vector, 1).
+param(t2, b, 1).
+typeVar(b).
+type(t3, cjava_DOT_util_DOT_Vector, 1).
+param(t3, a, 1).
+typeVar(a).
+
+unify(p, t1, t3).
+
+#show unify/3.

asp/unifikation.lp

@@ -0,0 +1,23 @@
+
+%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)
+	.
+
+%Ich lasse das Subst hier aus. Vector Beispiel funktioniert womöglich auch ohne
+
+%swap:
+unify(Pointer, B, A) :- unify(Pointer, A, B).
+
+%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).
+

asp/unifikation.lp.backup

@@ -0,0 +1,40 @@
+
+%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).
+

asp/vectorTestInput.lp

@@ -0,0 +1,95 @@
+
+%#show smallerGen/2.
+%#show smallerGen/4.
+
+typeVar(cZW).
+smallerDot(cN,cK).
+smaller(cBHW,cBHX).
+param(cBHW,cZW,1).
+type(cBHO,cjava_DOT_util_DOT_Vector,1).
+smaller(cBIM,cBIN).
+type(cBIQ,cjava_DOT_util_DOT_AbstractList,1).
+type(cBIB,cjava_DOT_lang_DOT_Object,0).
+type(cBIC,cjava_DOT_util_DOT_List,1).
+type(cBHN,cjava_DOT_lang_DOT_Object,0).
+param(cBHS,cZW,1).
+param(cBHT,cZW,1).
+param(cBHU,cZW,1).
+param(cBHV,cZW,1).
+smaller(cBHY,cBHZ).
+type(cBIA,cjava_DOT_lang_DOT_Cloneable,0).
+type(cBIV,cjava_DOT_lang_DOT_Object,0).
+typeVar(cK).
+smaller(cBHU,cBHV).
+smallerDot(cL,cBIY).
+type(cBIM,cjava_DOT_lang_DOT_Object,0).
+smaller(cBIK,cBIL).
+type(cBIL,cjava_DOT_lang_DOT_Object,0).
+type(cBIE,cjava_DOT_util_DOT_Vector,1).
+type(cBII,cjava_DOT_util_DOT_AbstractCollection,1).
+param(cBIY,cLL,1).
+type(cBHZ,cjava_DOT_lang_DOT_Object,0).
+typeVar(cLL).
+type(cBIR,cjava_DOT_util_DOT_List,1).
+param(cBID,cZW,1).
+type(cBHY,cMyVector,0).
+smaller(cBII,cBIJ).
+param(cBIF,cZW,1).
+type(cBIG,cjava_DOT_util_DOT_Collection,1).
+type(cBHT,cjava_DOT_util_DOT_AbstractCollection,1).
+type(cBIT,cjava_DOT_util_DOT_AbstractList,1).
+param(cBHQ,cZW,1).
+smaller(cBIE,cBIF).
+typeVar(cL).
+param(cBHO,cZW,1).
+type(cBHM,cjava_DOT_io_DOT_Serializable,0).
+type(cBIK,cjava_DOT_util_DOT_RandomAccess,0).
+type(cBIJ,cjava_DOT_lang_DOT_Object,0).
+type(cBIO,cjava_DOT_util_DOT_AbstractCollection,1).
+type(cBIZ,cjava_DOT_lang_DOT_Integer,0).
+type(cBHX,cjava_DOT_lang_DOT_Object,0).
+type(cBIS,cjava_DOT_util_DOT_Vector,1).
+smaller(cBIG,cBIH).
+param(cBIW,cZW,1).
+smaller(cBIW,cBIX).
+smaller(cBHM,cBHN).
+smaller(cBIC,cBID).
+type(cBHP,cjava_DOT_util_DOT_RandomAccess,0).
+param(cBIS,cZW,1).
+param(cBIQ,cZW,1).
+param(cBIU,cZW,1).
+param(cBIR,cZW,1).
+param(cBIT,cZW,1).
+smaller(cBHO,cBHP).
+param(cBIP,cZW,1).
+type(cBIH,cjava_DOT_lang_DOT_Object,0).
+typeVar(cM).
+type(cBIU,cjava_DOT_lang_DOT_Iterable,1).
+type(cBHR,cjava_DOT_lang_DOT_Cloneable,0).
+type(cBIF,cjava_DOT_util_DOT_List,1).
+smaller(cBIU,cBIV).
+type(cBHV,cjava_DOT_lang_DOT_Iterable,1).
+smaller(cBIA,cBIB).
+equals(cLL,cN).
+type(cBIP,cjava_DOT_util_DOT_Collection,1).
+type(cBHS,cjava_DOT_util_DOT_AbstractList,1).
+type(cBIN,cjava_DOT_lang_DOT_Object,0).
+smaller(cBHS,cBHT).
+param(cBIE,cZW,1).
+smaller(cBIS,cBIT).
+param(cBIC,cZW,1).
+param(cBIG,cZW,1).
+param(cBII,cZW,1).
+type(cBID,cjava_DOT_util_DOT_Collection,1).
+param(cBIO,cZW,1).
+type(cBIW,cjava_DOT_util_DOT_Vector,1).
+smallerDot(cM,cBIZ).
+smaller(cBIO,cBIP).
+type(cBIY,cjava_DOT_util_DOT_Vector,1).
+typeVar(cN).
+type(cBHW,cjava_DOT_util_DOT_List,1).
+type(cBHU,cjava_DOT_util_DOT_Collection,1).
+type(cBIX,cjava_DOT_io_DOT_Serializable,0).
+smaller(cBHQ,cBHR).
+smaller(cBIQ,cBIR).
+type(cBHQ,cjava_DOT_util_DOT_Vector,1).

doc/Generics/generics.tex

@@ -1,25 +0,0 @@
-\documentclass{article}
-
-\begin{document}
-
-\section{Generics sind notwendig}
-Generics können nicht ignoriert werden.
-Folgender Fall ist Typisierbar:
-
-\begin{program}
-<T> T m1(T x){
-	return m2(x);
-}
-
-m2(x){
-	m1(1);
-	m2("Test");
-	return m1(x);
-}
-\end{program}
-
-Beim weglassen des Generics T wäre es aber nicht mehr möglich.
-Dann erhält jeder Constraint, welcher in Verbindung mit der Methode m1 steht
-den selben TPH.
-
-\end{document}