forked from i21017/JavaTypeUnify
Compare commits
7 Commits
main
...
performanc
| Author | SHA1 | Date | |
|---|---|---|---|
|
3951b8451b | ||
|
|
a04be1336a | ||
|
|
dee55f0b0f | ||
|
|
c58897f5ba | ||
|
|
c938e69c76 | ||
|
|
1475661b84 | ||
|
|
e397375d2a |
1
pom.xml
1
pom.xml
@ -53,6 +53,7 @@ http://maven.apache.org/maven-v4_0_0.xsd">
|
||||
<artifactId>maven-compiler-plugin</artifactId>
|
||||
<version>3.8.0</version>
|
||||
<configuration>
|
||||
<compilerArgs>--enable-preview</compilerArgs>
|
||||
<source>21</source>
|
||||
<target>21</target>
|
||||
</configuration>
|
||||
|
||||
@ -1,23 +0,0 @@
|
||||
grammar ConstraintSet;
|
||||
|
||||
constraintSet : (constraints | orConstraint | extendsRelation | ',')+;
|
||||
|
||||
extendsRelation: IDENTIFIER typeParams? '<' type;
|
||||
typeParams : '<' IDENTIFIER (',' IDENTIFIER)* '>';
|
||||
|
||||
orConstraint : '{' constraints ('|' constraints)* '}';
|
||||
constraints : '{' constraint (','? constraint)* '}' | constraint (','? constraint)*;
|
||||
constraint: subtypeCons | equalsCons;
|
||||
|
||||
subtypeCons : type '<.' type;
|
||||
equalsCons : type '=.' type;
|
||||
|
||||
type : tph | namedType;
|
||||
tph : '_' IDENTIFIER;
|
||||
namedType : IDENTIFIER params?;
|
||||
params : '<' type (',' type)* '>';
|
||||
|
||||
IDENTIFIER: [0-9A-Za-z.]+;
|
||||
|
||||
NEWLINE : [\r\n]+ -> skip;
|
||||
WS: [ \t] -> skip ;
|
||||
@ -1,11 +0,0 @@
|
||||
grammar Solution;
|
||||
|
||||
solutionset : solution (solution)*;
|
||||
solution : 'sigma(' tph ',' type ')';
|
||||
tph : 'tph("_' IDENTIFIER '")';
|
||||
type : 'type("' IDENTIFIER '",' params ')';
|
||||
params : 'null' | 'params(' type (',' type)* ')';
|
||||
|
||||
IDENTIFIER: [0-9A-Za-z.]+;
|
||||
NEWLINE : [\r\n]+ -> skip;
|
||||
WS: [ \t] -> skip ;
|
||||
@ -1,127 +0,0 @@
|
||||
% TEST INPUT
|
||||
orCons(undCons(lessdot(tph("_BG"),type("java.lang.Number",null)),undCons(equalsdot(tph("_BE"),type("java.lang.Boolean",null)),undCons(equalsdot(type("java.lang.Boolean",null),tph("_AH")),undCons(lessdot(tph("_BC"),type("java.lang.Number",null)),undCons(lessdot(tph("_G"),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AS")),undCons(equalsdot(type("java.lang.Boolean",null),tph("_H")),undCons(lessdot(tph("_AP"),tph("_AM")),undCons(lessdot(tph("_AV"),tph("_AU")),undCons(equalsdot(tph("_AI"),type("Matrix",null)),undCons(lessdot(tph("_AD"),tph("_AB")),undCons(lessdot(type("Matrix",null),tph("_AD")),undCons(lessdot(tph("_AF"),type("java.lang.Number",null)),undCons(equalsdot(tph("_AU"),tph("_CD")),undCons(equalsdot(tph("_H"),type("java.lang.Boolean",null)),undCons(lessdot(tph("_BV"),tph("_BA")),undCons(lessdot(tph("_V"),type("java.lang.Integer",null)),undCons(lessdot(tph("_J"),type("java.lang.Number",null)),undCons(lessdot(tph("_AY"),type("java.lang.Number",null)),undCons(equalsdot(tph("_AH"),type("java.lang.Boolean",null)),undCons(equalsdot(type("java.lang.Boolean",null),tph("_BE")),undCons(equalsdot(tph("_AF"),tph("_CK")),undCons(equalsdot(type("java.lang.Boolean",null),tph("_AW")),undCons(lessdot(tph("_AU"),type("java.lang.Number",null)),undCons(lessdot(tph("_BD"),tph("_BC")),undCons(equalsdot(tph("_AW"),type("java.lang.Boolean",null)),undCons(lessdot(tph("_BB"),tph("_BA")),undCons(lessdot(tph("_AG"),tph("_AF")),undCons(equalsdot(tph("_S"),type("Matrix",null)),undCons(equalsdot(type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null))))),type("java.util.Vector",params(tph("_ANQ")))),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Number",null)),undCons(equalsdot(type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null))))),type("java.util.Vector",params(tph("_ANR")))),undCons(equalsdot(tph("_BC"),tph("_BW")),undCons(equalsdot(tph("_AQ"),type("Matrix",null)),undCons(lessdot(tph("_AK"),type("java.lang.Number",null)), null))))))))))))))))))))))))))))))))))), null).
|
||||
orCons(undCons(equalsdot(tph("_AE"),type("Matrix",null)),undCons(lessdot(type("Matrix",null),type("Matrix",null)), null)), null).
|
||||
orCons(undCons(equalsdot(tph("_AG"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(equalsdot(tph("_AI"),type("java.util.AbstractList",params(tph("_AMV")))),undCons(lessdot(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(equalsdot(tph("_AI"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AK")),undCons(equalsdot(tph("_AI"),type("java.util.List",params(tph("_AMU")))), null)),orCons(undCons(equalsdot(tph("_AI"),type("java.util.AbstractList",params(tph("_AMV")))),undCons(lessdot(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AK")),undCons(equalsdot(tph("_AI"),type("java.util.Vector",params(tph("_AMW")))), null)),orCons(undCons(equalsdot(tph("_AI"),type("java.util.List",params(tph("_AMU")))),undCons(lessdot(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AK")),undCons(equalsdot(tph("_AI"),type("java.util.Vector",params(tph("_AMW")))), null)),orCons(undCons(equalsdot(tph("_AI"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),tph("_AK")), null)), null)))))))).
|
||||
orCons(undCons(lessdot(tph("_AF"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AQ"),type("java.util.Vector",params(tph("_AMX")))),undCons(lessdot(tph("_AMX"),tph("_AP")), null))),orCons(undCons(lessdot(tph("_AF"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AQ"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AP")), null))),orCons(undCons(lessdot(tph("_AF"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AQ"),type("java.util.Vector",params(tph("_AMX")))),undCons(lessdot(tph("_AMX"),tph("_AP")), null))),orCons(undCons(lessdot(tph("_AF"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AQ"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AP")), null))), null)))).
|
||||
orCons(undCons(lessdot(type("java.util.Vector",params(tph("_AMY"))),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalsdot(tph("_AT"),type("java.util.Vector",params(type("GE",null)))), null)), null).
|
||||
orCons(undCons(equalsdot(tph("_AV"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_AMZ")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANB")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_AMZ")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_ANA")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_ANA")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_AY")),undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANB")))), null)), null)))))))).
|
||||
orCons(undCons(equalsdot(tph("_BB"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(equalsdot(tph("_BD"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANE")))),undCons(lessdot(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_BG")),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANE")))),undCons(lessdot(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_BG")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_AND")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_BG")),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_ANC")))),undCons(lessdot(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_ANC")))),undCons(lessdot(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_BG")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_AND")))), null)), null)))))))).
|
||||
orCons(undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BK")),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null))),orCons(undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BK")),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AM"),type("Matrix",null)), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANG"),tph("_BK")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_ANG")))), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANH")))),undCons(lessdot(tph("_ANH"),tph("_BK")), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANG"),tph("_BK")),undCons(equalsdot(tph("_AM"),type("java.util.AbstractList",params(tph("_ANG")))), null))),orCons(undCons(lessdot(tph("_ANF"),tph("_BK")),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_ANF")))), null))),orCons(undCons(lessdot(tph("_ANF"),tph("_BK")),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AM"),type("java.util.List",params(tph("_ANF")))), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANH"),tph("_BK")),undCons(equalsdot(tph("_AM"),type("java.util.Vector",params(tph("_ANH")))), null))), null)))))))).
|
||||
orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANI"),tph("_BR")),undCons(equalsdot(tph("_AC"),type("java.util.List",params(tph("_ANI")))), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AC"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BR")), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_AC"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BR")), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANJ"),tph("_BR")),undCons(equalsdot(tph("_AC"),type("java.util.AbstractList",params(tph("_ANJ")))), null))),orCons(undCons(equalsdot(tph("_AC"),type("java.util.Vector",params(tph("_ANK")))),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANK"),tph("_BR")), null))),orCons(undCons(equalsdot(tph("_AC"),type("java.util.Vector",params(tph("_ANK")))),undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANK"),tph("_BR")), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANI"),tph("_BR")),undCons(equalsdot(tph("_AC"),type("java.util.List",params(tph("_ANI")))), null))),orCons(undCons(lessdot(tph("_BC"),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANJ"),tph("_BR")),undCons(equalsdot(tph("_AC"),type("java.util.AbstractList",params(tph("_ANJ")))), null))), null)))))))).
|
||||
orCons(undCons(lessdot(tph("_ANM"),tph("_BO")),undCons(equalsdot(tph("_BR"),type("java.util.AbstractList",params(tph("_ANM")))),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_BR"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BO")), null))),orCons(undCons(equalsdot(tph("_BR"),type("java.util.List",params(tph("_ANL")))),undCons(lessdot(tph("_ANL"),tph("_BO")),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(equalsdot(tph("_BR"),type("java.util.List",params(tph("_ANL")))),undCons(lessdot(tph("_ANL"),tph("_BO")),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(lessdot(tph("_ANN"),tph("_BO")),undCons(equalsdot(tph("_BR"),type("java.util.Vector",params(tph("_ANN")))),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(lessdot(tph("_ANM"),tph("_BO")),undCons(equalsdot(tph("_BR"),type("java.util.AbstractList",params(tph("_ANM")))),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(lessdot(tph("_ANN"),tph("_BO")),undCons(equalsdot(tph("_BR"),type("java.util.Vector",params(tph("_ANN")))),undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(lessdot(tph("_AU"),type("java.lang.Integer",null)),undCons(equalsdot(tph("_BR"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BO")), null))), null)))))))).
|
||||
orCons(undCons(lessdot(tph("_BO"),type("java.lang.Integer",null)),undCons(equalsdot(type("java.lang.Integer",null),tph("_BU")),undCons(lessdot(tph("_BK"),type("java.lang.Integer",null)), null))), null).
|
||||
orCons(undCons(lessdot(tph("_BU"),type("java.lang.Integer",null)),undCons(lessdot(tph("_BA"),type("java.lang.Integer",null)),undCons(equalsdot(type("java.lang.Integer",null),tph("_BV")), null))), null).
|
||||
orCons(undCons(lessdot(tph("_BA"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalsdot(tph("_AS"),type("Matrix",null)), null)),orCons(undCons(lessdot(tph("_BA"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalsdot(tph("_AS"),type("Matrix",null)), null)),orCons(undCons(equalsdot(tph("_AS"),type("java.util.Vector",params(tph("_ANO")))),undCons(lessdot(tph("_BA"),tph("_ANO")), null)),orCons(undCons(equalsdot(tph("_AS"),type("java.util.Vector",params(tph("_ANO")))),undCons(lessdot(tph("_BA"),tph("_ANO")), null)), null)))).
|
||||
orCons(undCons(lessdot(tph("_AS"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalsdot(tph("_AD"),type("Matrix",null)), null)),orCons(undCons(equalsdot(tph("_AD"),type("java.util.Vector",params(tph("_ANP")))),undCons(lessdot(tph("_AS"),tph("_ANP")), null)),orCons(undCons(lessdot(tph("_AS"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalsdot(tph("_AD"),type("Matrix",null)), null)),orCons(undCons(equalsdot(tph("_AD"),type("java.util.Vector",params(tph("_ANP")))),undCons(lessdot(tph("_AS"),tph("_ANP")), null)), null)))).
|
||||
orCons(undCons(equalsdot(tph("_G"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_J")),undCons(equalsdot(tph("_F"),type("java.util.List",params(tph("_ANS")))), null)),orCons(undCons(equalsdot(tph("_F"),type("java.util.AbstractList",params(tph("_ANT")))),undCons(lessdot(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_J")),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANU")))), null)),orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_J")),undCons(equalsdot(tph("_F"),type("java.util.List",params(tph("_ANS")))), null)),orCons(undCons(lessdot(type("java.lang.Integer",null),tph("_J")),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANU")))), null)),orCons(undCons(equalsdot(tph("_F"),type("java.util.AbstractList",params(tph("_ANT")))),undCons(lessdot(type("java.lang.Integer",null),tph("_J")), null)), null)))))))).
|
||||
orCons(undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANV"),tph("_N")),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANV")))), null))),orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANV"),tph("_N")),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANV")))), null))),orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))).
|
||||
orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANX")))),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANX"),tph("_N")), null))),orCons(undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANX")))),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANX"),tph("_N")), null))),orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))).
|
||||
orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANZ")))),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANZ"),tph("_N")), null))),orCons(undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_ANZ")))),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_ANZ"),tph("_N")), null))), null)))).
|
||||
orCons(undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(lessdot(tph("_AOB"),tph("_N")),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_AOB")))), null))),orCons(undCons(lessdot(tph("_AOB"),tph("_N")),undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalsdot(tph("_F"),type("java.util.Vector",params(tph("_AOB")))), null))),orCons(undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalsdot(tph("_F"),type("Matrix",null)),undCons(lessdot(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))).
|
||||
orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(lessdot(tph("_N"),tph("_AOA")),undCons(equalsdot(tph("_S"),type("java.util.Vector",params(tph("_AOA")))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(lessdot(tph("_N"),tph("_ANW")),undCons(equalsdot(tph("_S"),type("java.util.List",params(tph("_ANW")))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(lessdot(tph("_N"),tph("_ANW")),undCons(equalsdot(tph("_S"),type("java.util.List",params(tph("_ANW")))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(lessdot(tph("_N"),tph("_AOA")),undCons(equalsdot(tph("_S"),type("java.util.Vector",params(tph("_AOA")))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(equalsdot(tph("_S"),type("Matrix",null)),undCons(lessdot(tph("_N"),type("java.util.Vector",params(type("java.lang.Integer",null)))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(equalsdot(tph("_S"),type("Matrix",null)),undCons(lessdot(tph("_N"),type("java.util.Vector",params(type("java.lang.Integer",null)))), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(equalsdot(tph("_S"),type("java.util.AbstractList",params(tph("_ANY")))),undCons(lessdot(tph("_N"),tph("_ANY")), null))),orCons(undCons(lessdot(type("java.lang.Boolean",null),tph("_R")),undCons(equalsdot(tph("_S"),type("java.util.AbstractList",params(tph("_ANY")))),undCons(lessdot(tph("_N"),tph("_ANY")), null))), null)))))))).
|
||||
orCons(undCons(equalsdot(tph("_U"),type("java.lang.Integer",null)), null), null).
|
||||
orCons(undCons(lessdot(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(lessdot(tph("_U"),type("java.lang.Integer",null)),undCons(equalsdot(type("java.lang.Integer",null),tph("_V")), null))), null).
|
||||
|
||||
super(type("java.lang.Boolean",null),type("Object",null)):-super(type("java.lang.Boolean",null)).super(type("java.lang.Integer",null),type("java.lang.Number",null)):-super(type("java.lang.Integer",null)).super(type("java.lang.Number",null),type("Object",null)):-super(type("java.lang.Number",null)).super(type("java.util.Vector",params(XX)),type("Object",null)):-super(type("java.util.Vector",params(XX))).super(type("Matrix",null),type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null)))))):-super(type("Matrix",null)).
|
||||
|
||||
|
||||
%%%%%
|
||||
|
||||
super(type("MyPair", params(X, Y)), type("Pair", params(Y, X))) :- super(type("MyPair", params(X, Y))).
|
||||
super(type("ArrayList", params(X)), type("List", params(X))) :- super(type("ArrayList", params(X))).
|
||||
super(type("List", params(X)), type("Object", null)) :- super(type("List", params(X))).
|
||||
super(type("Integer", null), type("Object", null)) :- super(type("Integer", null)).
|
||||
super(type("Matrix", null), type("Vector", params(type("Vector", params(type("Integer", null)))))) :- super(type("Matrix", null)).
|
||||
super(type("Vector", params(X)), type("Object", null)) :- super(type("Vector", params(X))).
|
||||
|
||||
% Subtyping
|
||||
super(A, A) :- super(A, B). % reflexive
|
||||
super(B) :- super(A, B). % transitive
|
||||
super(A, C) :- super(A, B), super(B, C). % transitive
|
||||
less(A,B) :- super(type(A, AP), type(B, BP)).
|
||||
|
||||
% Or-Constraints
|
||||
undCons(A,B) :- orCons(undCons(A,B), null).
|
||||
undCons(A,B); orCons(C,D) :- orCons(undCons(A,B), orCons(C,D)).
|
||||
lessdot(A,B) :- undCons(lessdot(A,B), _).
|
||||
undCons(B,C) :- undCons(A, undCons(B, C)).
|
||||
|
||||
% undCons
|
||||
lessdot(A,B) :- undCons(lessdot(A,B), _).
|
||||
undCons(C,D) :- undCons(_, undCons(C,D)).
|
||||
|
||||
% substitution
|
||||
subst(tph(A), type(C,P)) :- equalsdot(tph(A), type(C,P)).
|
||||
subst(A) :- equalsdot(A, B).
|
||||
subst(B) :- equalsdot(A, B).
|
||||
equalsdot(B, C) :- subst(A,B), equalsdot(A, C).
|
||||
equalsdot(C, B) :- subst(A,B), equalsdot(C, A).
|
||||
subst(A) :- lessdot(A, B).
|
||||
subst(B) :- lessdot(A, B).
|
||||
lessdot(B, C) :- subst(A,B), lessdot(A, C).
|
||||
lessdot(C, B) :- subst(A,B), lessdot(C, A).
|
||||
subst(type(N, params(P)), type(N, params(S))) :- subst(type(N, params(P))), subst(P, S).
|
||||
|
||||
% match
|
||||
super(C) :- lessdot(TPH, C).
|
||||
lessdot(C, D) :- lessdot(TPH, C), lessdot(TPH, D), super(C, D).
|
||||
|
||||
% reduce
|
||||
equalsdot(AP, BP) :- equalsdot(type(A, params(AP)), type(A, params(BP))).
|
||||
|
||||
equalsdot(AP, BP) :- equalsdot(type(A, params(AP, AP2)), type(A, params(BP, BP2))).
|
||||
equalsdot(AP2, BP2) :- equalsdot(type(A, params(AP, AP2)), type(A, params(BP, BP2))).
|
||||
|
||||
equalsdot(AP, BP) :- equalsdot(type(A, params(AP, AP2, AP3)), type(A, params(BP, BP2, BP3))).
|
||||
equalsdot(AP2, BP2) :- equalsdot(type(A, params(AP, AP2, AP3)), type(A, params(BP, BP2, BP3))).
|
||||
equalsdot(AP3, BP3) :- equalsdot(type(A, params(AP, AP2, AP3)), type(A, params(BP, BP2, BP3))).
|
||||
|
||||
% Swap
|
||||
equalsdot(tph(B),type(A, AP)) :- equalsdot(type(A, AP), tph(B)).
|
||||
|
||||
% adapt
|
||||
super(type(C,CP)) :- lessdot(type(C,CP),type(D, DP)). % generate
|
||||
equalsdot(type(D, N), type(D, DP)) :- lessdot(type(C,CP),type(D, DP)), super(type(C, CP), type(D, N)).
|
||||
|
||||
% adopt
|
||||
lessdot(tph(B), type(C, CP)) :- lessdot(tph(A), type(C, CP)), lessdot(tph(B), tph(A)).
|
||||
|
||||
% step 2
|
||||
super(type(C, CP)) :- lessdot(type(C, CP), tph(A)).
|
||||
equalsdot(tph(A), type(C, CP)); lessdot(type(D, DP), tph(A)) :- lessdot(type(C, CP), tph(A)), super(type(C, CP), type(D, DP)).
|
||||
equalsdot(tph(A), type(C, CP)) :- lessdot(type(C, CP), tph(A)), not super(type(C, CP),_).
|
||||
|
||||
% a <. C , a <. b constraints:
|
||||
lessdot(tph(B), type(C, CP)); lessdot(type(C, CP), tph(B)) :- lessdot(tph(A), type(C, CP)), lessdot(tph(A), tph(B)).
|
||||
|
||||
% errors
|
||||
tphs( P ) :- equalsdot(tph(A), type(C, P)).
|
||||
tphs(tph(P), params(tph(P))) :- tphs( params(tph(P))).
|
||||
tphs(P) :- tphs( params(type(C, P))).
|
||||
tphs(tph(A), params(type(C, P))) :- tphs( params(type(C, P))), tphs(tph(A), P).
|
||||
|
||||
tphs(tph(P), params(X, tph(P))) :- tphs( params(X, tph(P))).
|
||||
tphs(tph(P), params(tph(P), X)) :- tphs( params(tph(P), X)).
|
||||
tphs(P) :- tphs( params(X, type(C, P))).
|
||||
tphs(P) :- tphs( params(type(C, P), X)).
|
||||
tphs(tph(A), params(X, type(C, P))) :- tphs( params(X, type(C, P))), tphs(tph(A), P).
|
||||
tphs(tph(A), params(type(C, P), X)) :- tphs( params(type(C, P), X)), tphs(tph(A), P).
|
||||
|
||||
:- equalsdot(tph(A), type(C, P)), tphs(tph(A), P). % fail for subst
|
||||
|
||||
:- equalsdot(type(C, CP), type(D, DP)), C != D. % fail for reduce
|
||||
:- lessdot(type(C, CP), type(D, DP)), not less(C, D). % fail for adapt
|
||||
:- lessdot(tph(A), type(D, DP)), lessdot(tph(A), type(C, CP)), not less(C, D), not less(D, C). %Fail for match
|
||||
|
||||
% solve
|
||||
sigma(tph(A), type(C,P)) :- equalsdot(tph(A), type(C,P)).
|
||||
sigma2(tph(A), type(C,P)) :- lessdot(tph(A), type(C,P)), not sigma(tph(A), _).
|
||||
|
||||
#show sigma2/2.
|
||||
#show sigma/2.
|
||||
%#show subst/2.
|
||||
@ -1,155 +0,0 @@
|
||||
% TEST INPUT
|
||||
orCons(undCons(subcons(tph("_AG"),tph("_AD")),undCons(equalcons(tph("_O"),type("C1",null)),undCons(equalcons(type("java.lang.Object",null),type("java.lang.Object",null)),undCons(equalcons(tph("_W"),type("C2",null)),undCons(subcons(tph("_O"),tph("_N")),undCons(subcons(tph("_W"),tph("_V")), null)))))), null).
|
||||
orCons(undCons(subcons(tph("_N"),tph("_BC")),undCons(equalcons(tph("_AE"),type("C1",null)), null)),orCons(undCons(equalcons(tph("_AE"),type("C2",null)),undCons(subcons(tph("_V"),tph("_BC")), null)),orCons(undCons(equalcons(tph("_AE"),type("C2",null)),undCons(subcons(tph("_V"),tph("_BC")), null)),orCons(undCons(subcons(tph("_N"),tph("_BC")),undCons(equalcons(tph("_AE"),type("C1",null)), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_N"),tph("_BA")),undCons(equalcons(tph("_BC"),type("C1",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_BA")),undCons(equalcons(tph("_BC"),type("C2",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_BA")),undCons(equalcons(tph("_BC"),type("C2",null)), null)),null))).
|
||||
orCons(undCons(equalcons(tph("_BA"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AY")), null)),orCons(undCons(subcons(tph("_V"),tph("_AY")),undCons(equalcons(tph("_BA"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_BA"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AY")), null)),orCons(undCons(subcons(tph("_V"),tph("_AY")),undCons(equalcons(tph("_BA"),type("C2",null)), null)), null)))).
|
||||
orCons(undCons(equalcons(tph("_AY"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AW")), null)),orCons(undCons(equalcons(tph("_AY"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AW")), null)),orCons(undCons(equalcons(tph("_AY"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AW")), null)),orCons(undCons(equalcons(tph("_AY"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AW")), null)), null)))).
|
||||
orCons(undCons(equalcons(tph("_AW"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AU")), null)),orCons(undCons(equalcons(tph("_AW"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AU")), null)),orCons(undCons(equalcons(tph("_AW"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AU")), null)),orCons(undCons(equalcons(tph("_AW"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AU")), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_N"),tph("_AS")),undCons(equalcons(tph("_AU"),type("C1",null)), null)),orCons(undCons(equalcons(tph("_AU"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AS")), null)),orCons(undCons(subcons(tph("_N"),tph("_AS")),undCons(equalcons(tph("_AU"),type("C1",null)), null)),orCons(undCons(equalcons(tph("_AU"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AS")), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_N"),tph("_AQ")),undCons(equalcons(tph("_AS"),type("C1",null)), null)),orCons(undCons(subcons(tph("_N"),tph("_AQ")),undCons(equalcons(tph("_AS"),type("C1",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_AQ")),undCons(equalcons(tph("_AS"),type("C2",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_AQ")),undCons(equalcons(tph("_AS"),type("C2",null)), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_V"),tph("_AO")),undCons(equalcons(tph("_AQ"),type("C2",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_AO")),undCons(equalcons(tph("_AQ"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_AQ"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AO")), null)),orCons(undCons(equalcons(tph("_AQ"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AO")), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_V"),tph("_AM")),undCons(equalcons(tph("_AO"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_AO"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AM")), null)),orCons(undCons(subcons(tph("_V"),tph("_AM")),undCons(equalcons(tph("_AO"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_AO"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AM")), null)), null)))).
|
||||
orCons(undCons(equalcons(tph("_AM"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AK")), null)),orCons(undCons(equalcons(tph("_AM"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AK")), null)),orCons(undCons(subcons(tph("_V"),tph("_AK")),undCons(equalcons(tph("_AM"),type("C2",null)), null)),orCons(undCons(subcons(tph("_V"),tph("_AK")),undCons(equalcons(tph("_AM"),type("C2",null)), null)), null)))).
|
||||
orCons(undCons(subcons(tph("_V"),tph("_AI")),undCons(equalcons(tph("_AK"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_AK"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AI")), null)),orCons(undCons(subcons(tph("_V"),tph("_AI")),undCons(equalcons(tph("_AK"),type("C2",null)), null)),orCons(undCons(equalcons(tph("_AK"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AI")), null)), null)))).
|
||||
orCons(undCons(equalcons(tph("_AI"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AG")), null)),orCons(undCons(equalcons(tph("_AI"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AG")), null)),orCons(undCons(equalcons(tph("_AI"),type("C1",null)),undCons(subcons(tph("_N"),tph("_AG")), null)),orCons(undCons(equalcons(tph("_AI"),type("C2",null)),undCons(subcons(tph("_V"),tph("_AG")), null)), null)))).
|
||||
|
||||
subtype(type("java.lang.Boolean",null),type("java.lang.Object",null)):-subtype(type("java.lang.Boolean",null)).subtype(type("java.lang.String",null),type("java.lang.Object",null)):-subtype(type("java.lang.String",null)).subtype(type("java.lang.Integer",null),type("java.lang.Object",null)):-subtype(type("java.lang.Integer",null)).subtype(type("OrConsTest",null),type("java.lang.Object",null)):-subtype(type("OrConsTest",null)).subtype(type("MyPair",params(XX,XY)),type("Pair",params(XX,XX))):-subtype(type("MyPair",params(XX,XY))).subtype(type("Pair",params(XX,XY)),type("Object",null)):-subtype(type("Pair",params(XX,XY))).subtype(type("List",params(XX)),type("Object",null)):-subtype(type("List",params(XX))).subtype(type("Integer",null),type("Object",null)):-subtype(type("Integer",null)).subtype(type("String",null),type("Object",null)):-subtype(type("String",null)).
|
||||
|
||||
subtype(type("C1",null),type("java.lang.Object",null)):-subtype(type("C1",null)).
|
||||
subtype(type("C2",null),type("java.lang.Object",null)):-subtype(type("C2",null)).
|
||||
subtype(type("java.lang.Boolean",null),type("java.lang.Object",null)):-subtype(type("java.lang.Boolean",null)).subtype(type("java.lang.String",null),type("java.lang.Object",null)):-subtype(type("java.lang.String",null)).subtype(type("java.lang.Integer",null),type("java.lang.Object",null)):-subtype(type("java.lang.Integer",null)).subtype(type("OrConsTest",null),type("java.lang.Object",null)):-subtype(type("OrConsTest",null)).subtype(type("MyPair",params(XX,XY)),type("Pair",params(XX,XX))):-subtype(type("MyPair",params(XX,XY))).subtype(type("Pair",params(XX,XY)),type("Object",null)):-subtype(type("Pair",params(XX,XY))).subtype(type("List",params(XX)),type("Object",null)):-subtype(type("List",params(XX))).subtype(type("Integer",null),type("Object",null)):-subtype(type("Integer",null)).subtype(type("String",null),type("Object",null)):-subtype(type("String",null)).
|
||||
|
||||
%TODO: there is propably something wrong with the or-constraint generation
|
||||
|
||||
%%%%%
|
||||
|
||||
subtype(type("MyPair", params(X, Y)), type("Pair", params(Y, X))) :- subtype(type("MyPair", params(X, Y))).
|
||||
subtype(type("ArrayList", params(X)), type("List", params(X))) :- subtype(type("ArrayList", params(X))).
|
||||
subtype(type("List", params(X)), type("Object", null)) :- subtype(type("List", params(X))).
|
||||
subtype(type("Integer", null), type("Object", null)) :- subtype(type("Integer", null)).
|
||||
subtype(type("Matrix", null), type("Vector", params(type("Vector", params(type("Integer", null)))))) :- subtype(type("Matrix", null)).
|
||||
subtype(type("Vector", params(X)), type("Object", null)) :- subtype(type("Vector", params(X))).
|
||||
|
||||
|
||||
% Or-Constraints
|
||||
undCons(A,B) :- orCons(undCons(A,B), null).
|
||||
undCons(A,B); orCons(C,D) :- orCons(undCons(A,B), orCons(C,D)).
|
||||
|
||||
|
||||
% undCons
|
||||
subcons(A,B) :- undCons(subcons(A,B), _).
|
||||
undCons(C,D) :- undCons(_, undCons(C,D)).
|
||||
equalcons(A,B) :- undCons(equalcons(A,B), _).
|
||||
undCons(B,C) :- undCons(A, undCons(B, C)).
|
||||
|
||||
% Subtyping
|
||||
subtype(A, A) :- subtype(A). % reflexive
|
||||
subtype(A, A) :- subtype(A, B). % reflexive
|
||||
subtype(B) :- subtype(A, B). % transitive
|
||||
subtype(A, C) :- subtype(A, B), subtype(B, C). % transitive
|
||||
% named Subtyping
|
||||
namedSubtype(A,B) :- subtype(type(A, AP), type(B, BP)).
|
||||
% is reflexive and transitive because subtype it stems from subtype
|
||||
|
||||
% generate the subtype relations for every constraint where one is needed: (this could be optimized)
|
||||
subtype(type(A, P)) :- subcons(_, type(A, P)).
|
||||
subtype(type(A, P)) :- subcons(type(A, P), _).
|
||||
|
||||
% subst:
|
||||
subst(tph(A), type(N,P)) :- equalcons(tph(A), type(N, P)).
|
||||
|
||||
% subst-L:
|
||||
subcons(B,C) :- subst(A, B), subcons(A, C).
|
||||
%subst-R:
|
||||
subcons(C,B) :- subst(A, B), subcons(C, A).
|
||||
%subst-Equal:
|
||||
equalcons(B,C) :- subst(A, B), equalcons(A, C).
|
||||
|
||||
%swap:
|
||||
equalcons(A,B) :- equalcons(B,A).
|
||||
|
||||
%unfold:
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(T))).
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(T, _))).
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(_, T))).
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(T, _, _))).
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(_, T, _))).
|
||||
equalcons(T, T) :- equalcons(tph(_), type(_, params(_, _, T))).
|
||||
|
||||
% Subst-Param:
|
||||
subcons(A, type(C, params(T2))) :- subcons(A, type(C, params(T))), subst(T, T2).
|
||||
subcons(A, type(C, params(T2, P2))) :- subcons(A, type(C, params(T, P2))), subst(T, T2).
|
||||
subcons(A, type(C, params(P1, T2))) :- subcons(A, type(C, params(P1, T))), subst(T, T2).
|
||||
subcons(A, type(C, params(T2, P2, P3))) :- subcons(A, type(C, params(T, P2, P3))), subst(T, T2).
|
||||
subcons(A, type(C, params(P1, T2, P3))) :- subcons(A, type(C, params(P1, T, P3))), subst(T, T2).
|
||||
subcons(A, type(C, params( P1, P2, T2))) :- subcons(A, type(C, params(P1, P2, T))), subst(T, T2).
|
||||
|
||||
% match
|
||||
subcons(type(C, P1), type(D, P2)) :- subcons(tph(A), type(C, P1)), subcons(tph(A), type(D, P2)), namedSubtype(C, D).
|
||||
|
||||
% adopt
|
||||
subcons(tph(A), type(C,P)) :- subcons(tph(A), tph(B)), subcons(tph(B), type(C,P)).
|
||||
|
||||
% adapt
|
||||
equalcons(type(D,P3), type(D,P2)) :- subcons(type(C,P), type(D, P2)), subtype(type(C, P), type(D, P3)).
|
||||
|
||||
% reduce
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1)), type(C, params(PP1))).
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))).
|
||||
equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))).
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
equalcons(P3, PP3) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
|
||||
% super
|
||||
{ equalcons(tph(A), type(D, DP)): subtype(type(C, CP), type(D, DP)) } == 1 :- subcons(type(C, CP), tph(A)).
|
||||
%equalcons(tph(A), type(C, CP)) :- subcons(type(C, CP), tph(A)), not subtype(type(C, CP),_).
|
||||
|
||||
|
||||
%Solution-Gen
|
||||
%subst(tph(A), typeVar(tph(A))) :- subcons(tph(A), type(C,P)), not sigma(tph(A), _).
|
||||
%sigma2(tph(A), typeVar(tph(A))) :- subcons(tph(A), type(C,P)), not sigma(tph(A), _).
|
||||
|
||||
% here we check if there is a constraint a <. C, where there is no other Constraint. This is the solution-Gen rule
|
||||
%Solution-Subst:
|
||||
hasASubtype(tph(A), type(D,P2)) :- subcons(tph(A), type(C,P)), subcons(tph(A), type(D,P2)), namedSubtype(C, D), C != D.
|
||||
equalcons(tph(A), type(C,P)) :- subcons(tph(A), type(C,P)), not hasASubtype(tph(A), type(C,P)).
|
||||
|
||||
%Solution:
|
||||
tphs( P ) :- equalcons(tph(A), type(C, P)).
|
||||
sigma(tph(A), type(C,P)) :- equalcons(tph(A), type(C, P)), not tphs(_, P).
|
||||
|
||||
% Fail
|
||||
:- equalcons(tph(A), type(C, P)), tphs(tph(A), P). % fail for subst
|
||||
|
||||
:- equalcons(type(C, CP), type(D, DP)), C != D. % fail for reduce
|
||||
:- subcons(type(C, CP), type(D, DP)), not namedSubtype(C, D). % fail for adapt
|
||||
:- subcons(tph(A), type(D, DP)), subcons(tph(A), type(C, CP)), not namedSubtype(C, D), not namedSubtype(D, C). %Fail for match
|
||||
|
||||
%% Helpers
|
||||
%tphs:
|
||||
tphs(tph(P), params(tph(P))) :- tphs( params(tph(P))).
|
||||
tphs(P) :- tphs( params(type(C, P))).
|
||||
tphs(tph(A), params(type(C, P))) :- tphs( params(type(C, P))), tphs(tph(A), P).
|
||||
|
||||
tphs(tph(P), params(X, tph(P))) :- tphs( params(X, tph(P))).
|
||||
tphs(tph(P), params(tph(P), X)) :- tphs( params(tph(P), X)).
|
||||
tphs(P) :- tphs( params(X, type(C, P))).
|
||||
tphs(P) :- tphs( params(type(C, P), X)).
|
||||
tphs(tph(A), params(X, type(C, P))) :- tphs( params(X, type(C, P))), tphs(tph(A), P).
|
||||
tphs(tph(A), params(type(C, P), X)) :- tphs( params(type(C, P), X)), tphs(tph(A), P).
|
||||
|
||||
|
||||
tphs(tph(P), params(tph(P), X, Y)) :- tphs( params(tph(P), X, Y)).
|
||||
tphs(tph(P), params(X, tph(P), Y)) :- tphs( params(X, tph(P), Y)).
|
||||
tphs(tph(P), params(X,Y,tph(P))) :- tphs( params(X, Y, tph(P))).
|
||||
tphs(P) :- tphs( params(type(C, P), X, Y)).
|
||||
tphs(P) :- tphs( params(X, type(C, P),Y)).
|
||||
tphs(P) :- tphs( params(X,Y,type(C, P))).
|
||||
tphs(tph(A), params(type(C, P), X, Y)) :- tphs( params(type(C, P), X, Y)), tphs(tph(A), P).
|
||||
tphs(tph(A), params(X, type(C, P), Y)) :- tphs( params(X, type(C, P), Y)), tphs(tph(A), P).
|
||||
tphs(tph(A), params(X, Y, type(C, P))) :- tphs( params(X, Y, type(C, P))), tphs(tph(A), P).
|
||||
|
||||
|
||||
#show sigma/2.
|
||||
#show sigma2/2.
|
||||
@ -0,0 +1,7 @@
|
||||
package de.dhbwstuttgart.exceptions;
|
||||
|
||||
public class DebugException extends RuntimeException{
|
||||
public DebugException(String message){
|
||||
System.err.println(message);
|
||||
}
|
||||
}
|
||||
@ -1,87 +0,0 @@
|
||||
package de.dhbwstuttgart.input;
|
||||
|
||||
import de.dhbwstuttgart.input.parser.ConstraintSetLexer;
|
||||
import de.dhbwstuttgart.input.parser.ConstraintSetParser;
|
||||
import de.dhbwstuttgart.sat.asp.*;
|
||||
import org.antlr.v4.runtime.CharStream;
|
||||
import org.antlr.v4.runtime.CharStreams;
|
||||
import org.antlr.v4.runtime.CommonTokenStream;
|
||||
import org.antlr.v4.runtime.tree.ParseTree;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class ConstraintParser {
|
||||
|
||||
public static NamedType replaceGenerics(NamedType in, Set<String> genericNames){
|
||||
List<Type> superParams = in.params().stream().map(p -> {
|
||||
if(genericNames.contains(p.name())){
|
||||
return (Type) new TypeParameter(p.name());
|
||||
}else{
|
||||
return replaceGenerics((NamedType) p, genericNames);
|
||||
}
|
||||
}).toList();
|
||||
return new NamedType(in.name(), superParams);
|
||||
}
|
||||
public static List<ExtendsRelation> parseExtendsRelations(String cons){
|
||||
CharStream input = CharStreams.fromString(cons);
|
||||
de.dhbwstuttgart.input.parser.ConstraintSetLexer lexer = new ConstraintSetLexer(input);
|
||||
CommonTokenStream tokens = new CommonTokenStream(lexer);
|
||||
ConstraintSetParser parser = new ConstraintSetParser(tokens);
|
||||
ConstraintSetParser.ConstraintSetContext conSet = parser.constraintSet(); //Parsen
|
||||
List<ExtendsRelation> ret = new ArrayList<>();
|
||||
for(var ext : conSet.extendsRelation()){
|
||||
if(ext.typeParams()!=null){
|
||||
var typeParams = ext.typeParams().IDENTIFIER().stream().map(x -> new TypeParameter(x.getText())).toList();
|
||||
var typeParamNames = typeParams.stream().map(tp -> tp.name()).collect(Collectors.toSet());
|
||||
NamedType parsedSuperType = (NamedType) parseType(ext.type());
|
||||
parsedSuperType = replaceGenerics(parsedSuperType, typeParamNames);
|
||||
ret.add(new ExtendsRelation(ext.IDENTIFIER().getText(), typeParams, parsedSuperType));
|
||||
}else{
|
||||
ret.add(new ExtendsRelation(ext.IDENTIFIER().getText(), List.of(), (NamedType) parseType(ext.type())));
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
public static List<List<Set<Pair>>> parse(String cons){
|
||||
CharStream input = CharStreams.fromString(cons);
|
||||
de.dhbwstuttgart.input.parser.ConstraintSetLexer lexer = new ConstraintSetLexer(input);
|
||||
CommonTokenStream tokens = new CommonTokenStream(lexer);
|
||||
ConstraintSetParser parser = new ConstraintSetParser(tokens);
|
||||
ConstraintSetParser.ConstraintSetContext conSet = parser.constraintSet(); //Parsen
|
||||
Set<Pair> undCons = conSet.constraints().stream().flatMap(c -> parseUndConstraint(c).stream()).collect(Collectors.toSet());
|
||||
var ret = new ArrayList<List<Set<Pair>>>();
|
||||
var orCons = conSet.orConstraint().stream().map(ConstraintParser::parseOrConstraint).toList();
|
||||
if(undCons.size() > 0)ret.add(List.of(undCons));
|
||||
ret.addAll(orCons);
|
||||
return ret;
|
||||
}
|
||||
private static List<Set<Pair>> parseOrConstraint(ConstraintSetParser.OrConstraintContext ctx) {
|
||||
return ctx.constraints().stream().map(ConstraintParser::parseUndConstraint).toList();
|
||||
}
|
||||
private static Set<Pair> parseUndConstraint(ConstraintSetParser.ConstraintsContext ctx){
|
||||
return ctx.constraint().stream().map(ConstraintParser::parseConstraint).collect(Collectors.toSet());
|
||||
}
|
||||
private static Pair parseConstraint(ConstraintSetParser.ConstraintContext ctx){
|
||||
if(ctx.equalsCons() != null){
|
||||
return new EqualsDot(parseType(ctx.equalsCons().type().get(0)),
|
||||
parseType(ctx.equalsCons().type().get(1)));
|
||||
}else{
|
||||
return new LessDot(parseType(ctx.subtypeCons().type().get(0)),
|
||||
parseType(ctx.subtypeCons().type().get(1)));
|
||||
}
|
||||
}
|
||||
|
||||
private static Type parseType(ConstraintSetParser.TypeContext ctx) {
|
||||
if(ctx.tph()!=null){
|
||||
return new TypePlaceholder(ctx.tph().getText());
|
||||
}else{
|
||||
if(ctx.namedType().params() != null)
|
||||
return new NamedType(ctx.namedType().IDENTIFIER().getText(), ctx.namedType().params().type().stream().map(ConstraintParser::parseType).toList());
|
||||
else
|
||||
return new NamedType(ctx.namedType().IDENTIFIER().getText(), List.of());
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1,37 +0,0 @@
|
||||
package de.dhbwstuttgart.output;
|
||||
|
||||
import de.dhbwstuttgart.input.ConstraintParser;
|
||||
import de.dhbwstuttgart.sat.asp.Pair;
|
||||
import org.antlr.v4.runtime.CharStream;
|
||||
import org.antlr.v4.runtime.CharStreams;
|
||||
import org.antlr.v4.runtime.CommonTokenStream;
|
||||
|
||||
import java.util.*;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
record Sigma(String tphName, String typeReplacement){}
|
||||
public class SolutionParser {
|
||||
public static Map<String, String> parse(String cons){
|
||||
CharStream input = CharStreams.fromString(cons);
|
||||
de.dhbwstuttgart.input.parser.SolutionLexer lexer = new de.dhbwstuttgart.input.parser.SolutionLexer(input);
|
||||
CommonTokenStream tokens = new CommonTokenStream(lexer);
|
||||
de.dhbwstuttgart.input.parser.SolutionParser parser = new de.dhbwstuttgart.input.parser.SolutionParser(tokens);
|
||||
de.dhbwstuttgart.input.parser.SolutionParser.SolutionsetContext conSet = parser.solutionset(); //Parsen
|
||||
Set<Sigma> solutions = conSet.solution().stream().map(solutionContext -> new Sigma(solutionContext.tph().IDENTIFIER().getText(), parseType(solutionContext.type()))).collect(Collectors.toSet());
|
||||
Map<String, String> ret = new HashMap<>();
|
||||
for(Sigma solution : solutions){
|
||||
ret.put(solution.tphName(), solution.typeReplacement());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
private static String parseType(de.dhbwstuttgart.input.parser.SolutionParser.TypeContext type) {
|
||||
String params = "";
|
||||
if(type.params().type().size() > 0){
|
||||
params += "<";
|
||||
params += type.params().type().stream().map(t -> parseType(t)).collect(Collectors.joining(","));
|
||||
params += ">";
|
||||
}
|
||||
return type.IDENTIFIER().getText() + params;
|
||||
}
|
||||
}
|
||||
@ -1,53 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class ASPGenerator {
|
||||
public static String generateASP(List<List<Set<Pair>>> orCons){
|
||||
StringBuilder ret = new StringBuilder();
|
||||
for(List<Set<Pair>> orCon : orCons){
|
||||
ret.append(generateOrCons(orCon) + ".\n");
|
||||
}
|
||||
return ret.toString();
|
||||
}
|
||||
|
||||
public static String generateOrCons(List<Set<Pair>> undCon){
|
||||
if(undCon.size() < 2){
|
||||
return "orCons(" + generateUndCons(undCon.getFirst()) + ", null)";
|
||||
}else {
|
||||
Set<Pair> first = undCon.getFirst();
|
||||
undCon = undCon.subList(1, undCon.size());
|
||||
return "orCons(" + generateUndCons(first) + ","+ generateOrCons(undCon) + ")";
|
||||
}/*
|
||||
String ret = "orCons(";
|
||||
for(Set<Pair> uCon : undCons){
|
||||
String aspUndConstraint = generateUndCons(uCon);
|
||||
ret += aspUndConstraint + ",";
|
||||
}
|
||||
ret = ret.substring(0, ret.length()-1);
|
||||
return ret + ")";*/
|
||||
}
|
||||
|
||||
public static String generateUndCons(Set<Pair> undCon){
|
||||
if(undCon.size() == 1){
|
||||
return "undCons(" + undCon.iterator().next().toASP() + ", null)";
|
||||
}else {
|
||||
// undCOns verschachteln
|
||||
Pair first = undCon.iterator().next();
|
||||
undCon = undCon.stream().filter(x->!first.equals(x)).collect(Collectors.toSet());
|
||||
return "undCons(" + first.toASP() + ","+ generateUndCons(undCon) + ")";
|
||||
}
|
||||
}
|
||||
|
||||
public static String generateExtendsRelations(List<ExtendsRelation> extendsRelations) {
|
||||
String ret = "";
|
||||
for(var x : extendsRelations){
|
||||
NamedType subtype = new NamedType(x.subtypeName(), x.subtypeParams().stream().map(i -> (Type)i).toList());
|
||||
ret += "subtype("+subtype.toASP()+","+x.superType().toASP()+"):-subtype("+subtype.toASP()+").";
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record EqualsDot(Type left, Type right) implements Pair {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "equalcons("+ left().toASP() + "," + right().toASP() + ")";
|
||||
}
|
||||
}
|
||||
@ -1,6 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
import java.util.List;
|
||||
|
||||
public record ExtendsRelation(String subtypeName, List<TypeParameter> subtypeParams, NamedType superType) {
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record LessDot(Type left, Type right) implements Pair {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "subcons("+ left().toASP() + "," + right().toASP() + ")";
|
||||
}
|
||||
}
|
||||
@ -1,12 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public record NamedType(String name, List<Type> params) implements Type {
|
||||
@Override
|
||||
public String toASP() {
|
||||
if(params.size() > 0)return "type(\""+name+"\",params(" + params.stream().map(Type::toASP).collect(Collectors.joining(",")) + "))";
|
||||
return "type(\""+name+"\",null)";
|
||||
}
|
||||
}
|
||||
@ -1,5 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public interface Pair {
|
||||
String toASP();
|
||||
}
|
||||
@ -1,6 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public interface Type {
|
||||
String name();
|
||||
String toASP();
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record TypeParameter(String name) implements Type{
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "X"+name;
|
||||
}
|
||||
}
|
||||
@ -1,8 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record TypePlaceholder(String name) implements Type {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "tph(\""+name+"\")";
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,69 @@
|
||||
package de.dhbwstuttgart.typeinference.constraints;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.Collection;
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
public class Constraint<A> extends HashSet<A> {
|
||||
private static final long serialVersionUID = 1L;
|
||||
private Boolean isInherited = false;//wird nur für die Method-Constraints benoetigt
|
||||
|
||||
/*
|
||||
* wird verwendet um bei der Codegenerierung die richtige Methoden - Signatur
|
||||
* auszuwaehlen
|
||||
*/
|
||||
/*private*/ Set<A> methodSignatureConstraint = new HashSet<>();
|
||||
|
||||
private Constraint<A> extendConstraint = null;
|
||||
|
||||
public Constraint() {
|
||||
super();
|
||||
}
|
||||
|
||||
public Constraint(Boolean isInherited) {
|
||||
this.isInherited = isInherited;
|
||||
}
|
||||
|
||||
public Constraint(Boolean isInherited, Constraint<A> extendConstraint, Set<A> methodSignatureConstraint) {
|
||||
this.isInherited = isInherited;
|
||||
this.extendConstraint = extendConstraint;
|
||||
this.methodSignatureConstraint = methodSignatureConstraint;
|
||||
}
|
||||
|
||||
public void setIsInherited(Boolean isInherited) {
|
||||
this.isInherited = isInherited;
|
||||
}
|
||||
|
||||
public Boolean isInherited() {
|
||||
return isInherited;
|
||||
}
|
||||
|
||||
public Constraint<A> getExtendConstraint() {
|
||||
return extendConstraint;
|
||||
}
|
||||
|
||||
public void setExtendConstraint(Constraint<A> c) {
|
||||
extendConstraint = c;
|
||||
}
|
||||
|
||||
public Set<A> getmethodSignatureConstraint() {
|
||||
return methodSignatureConstraint;
|
||||
}
|
||||
|
||||
public void setmethodSignatureConstraint(Set<A> c) {
|
||||
methodSignatureConstraint = c;
|
||||
}
|
||||
|
||||
public String toString() {
|
||||
return super.toString() + "\nisInherited = " + isInherited
|
||||
//" + extendsContraint: " + (extendConstraint != null ? extendConstraint.toStringBase() : "null" )
|
||||
+ "\n" ;
|
||||
}
|
||||
|
||||
public String toStringBase() {
|
||||
return super.toString();
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,126 @@
|
||||
package de.dhbwstuttgart.typeinference.constraints;
|
||||
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.GuavaSetOperations;
|
||||
|
||||
import java.util.*;
|
||||
import java.util.function.BinaryOperator;
|
||||
import java.util.function.Consumer;
|
||||
import java.util.function.Function;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class ConstraintSet<A> {
|
||||
Constraint<A> undConstraints = new Constraint<>();
|
||||
List<Set<Constraint<A>>> oderConstraints = new ArrayList<>();
|
||||
|
||||
public void addUndConstraint(A p){
|
||||
undConstraints.add(p);
|
||||
}
|
||||
|
||||
public void addOderConstraint(Set<Constraint<A>> methodConstraints) {
|
||||
oderConstraints.add(methodConstraints);
|
||||
}
|
||||
|
||||
public void addAllUndConstraint(Constraint<A> allUndConstraints){
|
||||
undConstraints.addAll(allUndConstraints);
|
||||
}
|
||||
|
||||
public void addAllOderConstraint(List<Set<Constraint<A>>> allOderConstraints){
|
||||
this.oderConstraints.addAll(allOderConstraints);
|
||||
}
|
||||
|
||||
public void addAll(ConstraintSet constraints) {
|
||||
this.addAllUndConstraint(constraints.undConstraints);
|
||||
this.addAllOderConstraint(constraints.oderConstraints);
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString(){
|
||||
BinaryOperator<String> b = (x,y) -> x+y;
|
||||
return "\nUND:" + this.undConstraints.toString() + "\n" +
|
||||
"ODER:" + this.oderConstraints.stream().reduce("", (x,y) -> x.toString()+ "\n" +y, b);
|
||||
//cartesianProduct().toString();
|
||||
}
|
||||
|
||||
public Set<List<Constraint<A>>> cartesianProduct(){
|
||||
Set<Constraint<A>> toAdd = new HashSet<>();
|
||||
toAdd.add(undConstraints);
|
||||
List<Set<Constraint<A>>> allConstraints = new ArrayList<>();
|
||||
allConstraints.add(toAdd);
|
||||
allConstraints.addAll(oderConstraints);
|
||||
return new GuavaSetOperations().cartesianProduct(allConstraints);
|
||||
}
|
||||
|
||||
public <B> ConstraintSet<B> map(Function<? super A, ? extends B> o) {
|
||||
Hashtable<Constraint<A>,Constraint<B>> CSA2CSB = new Hashtable<>();
|
||||
ConstraintSet<B> ret = new ConstraintSet<>();
|
||||
ret.undConstraints = undConstraints.stream().map(o).collect(Collectors.toCollection(Constraint<B>::new));
|
||||
List<Set<Constraint<B>>> newOder = new ArrayList<>();
|
||||
/*
|
||||
for(Set<Constraint<A>> oderConstraint : oderConstraints){
|
||||
oderConstraint.forEach(as -> {
|
||||
Constraint<B> newConst = as.stream()
|
||||
.map(o)
|
||||
.collect(Collectors.toCollection(
|
||||
() -> new Constraint<B> (as.isInherited())));
|
||||
CSA2CSB.put(as, newConst);} );
|
||||
}
|
||||
*/
|
||||
|
||||
for(Set<Constraint<A>> oderConstraint : oderConstraints){
|
||||
newOder.add(
|
||||
oderConstraint.parallelStream().map((Constraint<A> as) -> {
|
||||
|
||||
Constraint<B> newConst = as.stream()
|
||||
.map(o)
|
||||
.collect(Collectors.toCollection((as.getExtendConstraint() != null)
|
||||
? () -> new Constraint<B> (as.isInherited(),
|
||||
as.getExtendConstraint().stream().map(o).collect(Collectors.toCollection(Constraint::new)),
|
||||
as.getmethodSignatureConstraint().stream().map(o).collect(Collectors.toCollection(HashSet::new)))
|
||||
: () -> new Constraint<B> (as.isInherited())
|
||||
));
|
||||
|
||||
//CSA2CSB.put(as, newConst);
|
||||
|
||||
return newConst;
|
||||
|
||||
/*
|
||||
Constraint<B> bs = CSA2CSB.get(as);
|
||||
if (as.getExtendConstraint() != null) {
|
||||
bs.setExtendConstraint(CSA2CSB.get(as.getExtendConstraint()));
|
||||
}
|
||||
return bs;
|
||||
*/
|
||||
}).collect(Collectors.toSet())
|
||||
);
|
||||
}
|
||||
|
||||
ret.oderConstraints = newOder;
|
||||
return ret;
|
||||
}
|
||||
|
||||
public void forEach (Consumer<? super A> c) {
|
||||
undConstraints.stream().forEach(c);
|
||||
for(Set<Constraint<A>> oderConstraint : oderConstraints){
|
||||
oderConstraint.parallelStream().forEach((Constraint<A> as) ->
|
||||
as.stream().forEach(c));
|
||||
}
|
||||
}
|
||||
|
||||
public Set<A> getAll () {
|
||||
Set<A> ret = new HashSet<>();
|
||||
ret.addAll(undConstraints);
|
||||
for(Set<Constraint<A>> oderConstraint : oderConstraints){
|
||||
oderConstraint.parallelStream().forEach((Constraint<A> as) -> ret.addAll(as));
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
public List<Set<Constraint<A>>> getOderConstraints() {
|
||||
return oderConstraints;
|
||||
}
|
||||
|
||||
public Set<A> getUndConstraints() {
|
||||
return undConstraints;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,13 @@
|
||||
package de.dhbwstuttgart.typeinference.constraints;
|
||||
import java.io.Serializable;
|
||||
import java.util.HashMap;
|
||||
import java.util.Map;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
|
||||
|
||||
public class Pair implements Serializable
|
||||
{
|
||||
|
||||
}
|
||||
// ino.end
|
||||
@ -0,0 +1,21 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
public class ConstraintSetRepository {
|
||||
private Set<Integer> sets = new HashSet<>();
|
||||
|
||||
public boolean containsSet(Set<Set<UnifyPair>> set){
|
||||
Integer hash = Integer.valueOf(set.hashCode());
|
||||
|
||||
if(sets.contains(hash)){
|
||||
return true;
|
||||
}else{
|
||||
sets.add(hash);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,23 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
import com.google.common.collect.Sets;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
|
||||
|
||||
/**
|
||||
* Implements set operations using google guava.
|
||||
* @author DH10STF
|
||||
*
|
||||
*/
|
||||
public class GuavaSetOperations implements ISetOperations {
|
||||
|
||||
@Override
|
||||
public <B> Set<List<B>> cartesianProduct(List<? extends Set<? extends B>> sets) {
|
||||
// Wraps the call to google guava
|
||||
return Sets.cartesianProduct(sets);
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,108 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
|
||||
/**
|
||||
* Implementation of the Martelli-Montanari unification algorithm.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public class MartelliMontanariUnify implements IUnify {
|
||||
|
||||
@Override
|
||||
public Optional<Unifier> unify(Set<UnifyType> terms) {
|
||||
// Sets with less than 2 terms are trivially unified
|
||||
if(terms.size() < 2)
|
||||
return Optional.of(Unifier.identity());
|
||||
|
||||
// For the the set of terms {t1,...,tn},
|
||||
// build a list of equations {(t1 = t2), (t2 = t3), (t3 = t4), ....}
|
||||
ArrayList<UnifyPair> termsList = new ArrayList<UnifyPair>();
|
||||
Iterator<UnifyType> iter = terms.iterator();
|
||||
UnifyType prev = iter.next();
|
||||
while(iter.hasNext()) {
|
||||
UnifyType next = iter.next();
|
||||
termsList.add(new UnifyPair(prev, next, PairOperator.EQUALSDOT));
|
||||
prev = next;
|
||||
}
|
||||
|
||||
// Start with the identity unifier. Substitutions will be added later.
|
||||
Unifier mgu = Unifier.identity();
|
||||
|
||||
// Apply rules while possible
|
||||
int idx = 0;
|
||||
while(idx < termsList.size()) {
|
||||
UnifyPair pair = termsList.get(idx);
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
TypeParams rhsTypeParams = rhsType.getTypeParams();
|
||||
TypeParams lhsTypeParams = lhsType.getTypeParams();
|
||||
|
||||
// REDUCE - Rule
|
||||
if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
// f<...> = g<...> with f != g are not unifiable
|
||||
if(!rhsType.getName().equals(lhsType.getName()))
|
||||
return Optional.empty(); // conflict
|
||||
// f<t1,...,tn> = f<s1,...,sm> are not unifiable
|
||||
if(rhsTypeParams.size() != lhsTypeParams.size())
|
||||
return Optional.empty(); // conflict
|
||||
// f = g is not unifiable (cannot be f = f because erase rule would have been applied)
|
||||
//if(rhsTypeParams.size() == 0)
|
||||
//return Optional.empty();
|
||||
|
||||
// Unpack the arguments
|
||||
for(int i = 0; i < rhsTypeParams.size(); i++)
|
||||
result.add(new UnifyPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
|
||||
|
||||
termsList.remove(idx);
|
||||
termsList.addAll(result);
|
||||
continue;
|
||||
}
|
||||
|
||||
// DELETE - Rule
|
||||
if(pair.getRhsType().equals(pair.getLhsType())) {
|
||||
termsList.remove(idx);
|
||||
continue;
|
||||
}
|
||||
|
||||
// SWAP - Rule
|
||||
if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
|
||||
termsList.remove(idx);
|
||||
termsList.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT));
|
||||
continue;
|
||||
}
|
||||
|
||||
// OCCURS-CHECK
|
||||
if(pair.getLhsType() instanceof PlaceholderType
|
||||
&& pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType()))
|
||||
return Optional.empty();
|
||||
|
||||
// SUBST - Rule
|
||||
if(lhsType instanceof PlaceholderType) {
|
||||
mgu.add((PlaceholderType) lhsType, rhsType);
|
||||
//PL 2018-04-01 nach checken, ob es richtig ist, dass keine Substitutionen uebergeben werden muessen.
|
||||
termsList = termsList.stream().map(x -> mgu.apply(x)).collect(Collectors.toCollection(ArrayList::new));
|
||||
idx = idx+1 == termsList.size() ? 0 : idx+1;
|
||||
continue;
|
||||
}
|
||||
|
||||
idx++;
|
||||
}
|
||||
|
||||
return Optional.of(mgu);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,92 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IMatch;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
|
||||
/**
|
||||
* Implementation of match derived from unification algorithm.
|
||||
* @author Martin Pluemicke
|
||||
*/
|
||||
public class Match implements IMatch {
|
||||
|
||||
@Override
|
||||
//vorne muss das Pattern stehen
|
||||
//A<X> =. A<Integer> ==> True
|
||||
//A<Integer> =. A<X> ==> False
|
||||
public Optional<Unifier> match(ArrayList<UnifyPair> termsList) {
|
||||
|
||||
// Start with the identity unifier. Substitutions will be added later.
|
||||
Unifier mgu = Unifier.identity();
|
||||
|
||||
// Apply rules while possible
|
||||
int idx = 0;
|
||||
while(idx < termsList.size()) {
|
||||
UnifyPair pair = termsList.get(idx);
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
TypeParams rhsTypeParams = rhsType.getTypeParams();
|
||||
TypeParams lhsTypeParams = lhsType.getTypeParams();
|
||||
|
||||
// REDUCE - Rule
|
||||
if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
// f<...> = g<...> with f != g are not unifiable
|
||||
if(!rhsType.getName().equals(lhsType.getName()))
|
||||
return Optional.empty(); // conflict
|
||||
// f<t1,...,tn> = f<s1,...,sm> are not unifiable
|
||||
if(rhsTypeParams.size() != lhsTypeParams.size())
|
||||
return Optional.empty(); // conflict
|
||||
// f = g is not unifiable (cannot be f = f because erase rule would have been applied)
|
||||
//if(rhsTypeParams.size() == 0)
|
||||
//return Optional.empty();
|
||||
|
||||
// Unpack the arguments
|
||||
for(int i = 0; i < rhsTypeParams.size(); i++)
|
||||
result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
|
||||
|
||||
termsList.remove(idx);
|
||||
termsList.addAll(result);
|
||||
continue;
|
||||
}
|
||||
|
||||
// DELETE - Rule
|
||||
if(pair.getRhsType().equals(pair.getLhsType())) {
|
||||
termsList.remove(idx);
|
||||
continue;
|
||||
}
|
||||
|
||||
// SWAP - Rule
|
||||
if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
|
||||
return Optional.empty(); // conflict
|
||||
}
|
||||
|
||||
// OCCURS-CHECK
|
||||
//deleted
|
||||
|
||||
// SUBST - Rule
|
||||
if(lhsType instanceof PlaceholderType) {
|
||||
mgu.add((PlaceholderType) lhsType, rhsType);
|
||||
termsList = termsList.stream().map(mgu::applyleft).collect(Collectors.toCollection(ArrayList::new));
|
||||
idx = idx+1 == termsList.size() ? 0 : idx+1;
|
||||
continue;
|
||||
}
|
||||
|
||||
idx++;
|
||||
}
|
||||
|
||||
return Optional.of(mgu);
|
||||
}
|
||||
}
|
||||
1050
src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java
Normal file
1050
src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java
Normal file
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,125 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.io.FileWriter;
|
||||
import java.io.IOException;
|
||||
import java.io.Writer;
|
||||
import java.util.ArrayList;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.concurrent.ForkJoinPool;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
public class TypeUnify {
|
||||
|
||||
public static Writer statistics;
|
||||
/**
|
||||
* unify parallel ohne result modell
|
||||
* @param undConstrains
|
||||
* @param oderConstraints
|
||||
* @param fc
|
||||
* @param logFile
|
||||
* @param log
|
||||
* @param cons
|
||||
* @return
|
||||
*/
|
||||
public Set<Set<UnifyPair>> unify(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) {
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks, new ConstraintSetRepository());
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
pool.invoke(unifyTask);
|
||||
Set<Set<UnifyPair>> res = unifyTask.join();
|
||||
try {
|
||||
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements + "\n");
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no log-File");
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
/**
|
||||
* unify asynchron mit Rückgabe UnifyResultModel ohne dass alle results gesammelt sind
|
||||
* @param undConstrains
|
||||
* @param oderConstraints
|
||||
* @param fc
|
||||
* @param logFile
|
||||
* @param log
|
||||
* @param cons
|
||||
* @param ret
|
||||
* @return
|
||||
*/
|
||||
public UnifyResultModel unifyAsync(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) {
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks, new ConstraintSetRepository());
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
pool.invoke(unifyTask);
|
||||
return ret;
|
||||
}
|
||||
|
||||
/**
|
||||
* unify parallel mit Rückgabe UnifyResultModel nachdem alle results gesammelt sind
|
||||
* @param undConstrains
|
||||
* @param oderConstraints
|
||||
* @param fc
|
||||
* @param logFile
|
||||
* @param log
|
||||
* @param cons
|
||||
* @param ret
|
||||
* @return
|
||||
*/
|
||||
public UnifyResultModel unifyParallel(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) {
|
||||
TypeUnifyTask unifyTask = //new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks);
|
||||
new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks, new ConstraintSetRepository(), statistics);
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
pool.invoke(unifyTask);
|
||||
Set<Set<UnifyPair>> res = unifyTask.join();
|
||||
try {
|
||||
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
|
||||
logFile.flush();
|
||||
unifyTask.statistics.write("Backtracking: " + unifyTask.noBacktracking);
|
||||
unifyTask.statistics.write("\nLoops: " + unifyTask.noLoop);
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no log-File");
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
/*
|
||||
public Set<Set<UnifyPair>> unifySequential(Set<UnifyPair> eq, IFiniteClosure fc, FileWriter logFile, Boolean log) {
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(eq, fc, false, logFile, log);
|
||||
Set<Set<UnifyPair>> res = unifyTask.compute();
|
||||
return res;
|
||||
}
|
||||
*/
|
||||
|
||||
/**
|
||||
* unify sequentiell mit oderconstraints
|
||||
* @param undConstrains
|
||||
* @param oderConstraints
|
||||
* @param fc
|
||||
* @param logFile
|
||||
* @param log
|
||||
* @param cons
|
||||
* @return
|
||||
*/
|
||||
public Set<Set<UnifyPair>> unifyOderConstraints(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) {
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, ret, usedTasks, new ConstraintSetRepository());
|
||||
unifyTask.statistics = statistics;
|
||||
Set<Set<UnifyPair>> res = unifyTask.compute();
|
||||
try {
|
||||
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no log-File");
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,80 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.io.FileWriter;
|
||||
import java.io.IOException;
|
||||
import java.io.Writer;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
public class TypeUnify2Task extends TypeUnifyTask {
|
||||
|
||||
Set<Set<UnifyPair>> setToFlatten;
|
||||
Set<UnifyPair> methodSignatureConstraintUebergabe;
|
||||
|
||||
//statistics
|
||||
TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq,
|
||||
List<Set<Constraint<UnifyPair>>> oderConstraints,
|
||||
Set<UnifyPair> nextSetElement,
|
||||
IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks,
|
||||
Set<UnifyPair> methodSignatureConstraintUebergabe, ConstraintSetRepository constraintSetRepository, Writer statistics) {
|
||||
this(setToFlatten, eq, oderConstraints, nextSetElement, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraintUebergabe, constraintSetRepository);
|
||||
|
||||
}
|
||||
|
||||
public TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, Set<UnifyPair> nextSetElement, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks, Set<UnifyPair> methodSignatureConstraintUebergabe, ConstraintSetRepository constraintSetRepository) {
|
||||
super(eq, oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, constraintSetRepository);
|
||||
this.setToFlatten = setToFlatten;
|
||||
this.nextSetElement = nextSetElement;
|
||||
this.methodSignatureConstraintUebergabe = methodSignatureConstraintUebergabe;
|
||||
}
|
||||
|
||||
Set<UnifyPair> getNextSetElement() {
|
||||
return nextSetElement;
|
||||
}
|
||||
|
||||
@Override
|
||||
protected Set<Set<UnifyPair>> compute() {
|
||||
if (one) {
|
||||
System.out.println("two");
|
||||
}
|
||||
one = true;
|
||||
Set<Set<UnifyPair>> res = new HashSet<>();
|
||||
|
||||
if(!constraintSetRepository.containsSet(setToFlatten)){
|
||||
res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField, methodSignatureConstraintUebergabe);
|
||||
}
|
||||
/*if (isUndefinedPairSetSet(res)) {
|
||||
return new HashSet<>(); }
|
||||
else
|
||||
*/
|
||||
//writeLog("xxx");
|
||||
//noOfThread--;
|
||||
synchronized (usedTasks) {
|
||||
if (this.myIsCancelled()) {
|
||||
return new HashSet<>();
|
||||
}
|
||||
else {
|
||||
return res;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public void closeLogFile() {
|
||||
|
||||
try {
|
||||
logFile.close();
|
||||
}
|
||||
catch (IOException ioE) {
|
||||
System.err.println("no log-File" + thNo);
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,11 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
public interface Unifikationsalgorithmus {
|
||||
|
||||
public Set<Set<UnifyPair>> apply (Set<UnifyPair> E);
|
||||
|
||||
}
|
||||
@ -0,0 +1,18 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.sql.ResultSet;
|
||||
import java.util.List;
|
||||
|
||||
|
||||
public class UnifyResultEvent {
|
||||
|
||||
private List<ResultSet> newTypeResult;
|
||||
|
||||
public UnifyResultEvent(List<ResultSet> newTypeResult) {
|
||||
this.newTypeResult = newTypeResult;
|
||||
}
|
||||
|
||||
public List<ResultSet> getNewTypeResult() {
|
||||
return newTypeResult;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,7 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
public interface UnifyResultListener {
|
||||
|
||||
void onNewTypeResultFound(UnifyResultEvent evt);
|
||||
|
||||
}
|
||||
@ -0,0 +1,21 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.sql.ResultSet;
|
||||
import java.util.ArrayList;
|
||||
import java.util.List;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
public class UnifyResultListenerImpl implements UnifyResultListener {
|
||||
|
||||
List<ResultSet> results = new ArrayList<>();
|
||||
|
||||
public synchronized void onNewTypeResultFound(UnifyResultEvent evt) {
|
||||
results.addAll(evt.getNewTypeResult());
|
||||
}
|
||||
|
||||
public List<ResultSet> getResults() {
|
||||
return results;
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,41 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.sql.ResultSet;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
public class UnifyResultModel {
|
||||
|
||||
ConstraintSet<de.dhbwstuttgart.typeinference.constraints.Pair> cons;
|
||||
|
||||
IFiniteClosure fc;
|
||||
|
||||
public UnifyResultModel(ConstraintSet<de.dhbwstuttgart.typeinference.constraints.Pair> cons,
|
||||
IFiniteClosure fc) {
|
||||
this.cons = cons;
|
||||
this.fc = fc;
|
||||
}
|
||||
|
||||
private List<UnifyResultListener> listeners = new ArrayList<>();
|
||||
|
||||
public void addUnifyResultListener(UnifyResultListener listenerToAdd) {
|
||||
listeners.add(listenerToAdd);
|
||||
}
|
||||
|
||||
public void removeUnifyResultListener(UnifyResultListener listenerToRemove) {
|
||||
listeners.remove(listenerToRemove);
|
||||
}
|
||||
|
||||
public void notify(Set<Set<UnifyPair>> eqPrimePrimeSet) {
|
||||
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,18 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
|
||||
public class UnifyTaskModel {
|
||||
|
||||
ArrayList<TypeUnifyTask> usedTasks = new ArrayList<>();
|
||||
|
||||
public synchronized void add(TypeUnifyTask t) {
|
||||
usedTasks.add(t);
|
||||
}
|
||||
|
||||
public synchronized void cancel() {
|
||||
for(TypeUnifyTask t : usedTasks) {
|
||||
t.myCancel(true);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,54 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.List;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
|
||||
public class distributeVariance extends visitUnifyTypeVisitor<Integer> {
|
||||
|
||||
public static int inverseVariance(int variance) {
|
||||
Integer ret = 0;
|
||||
if (variance == 1) {
|
||||
ret = -1;
|
||||
}
|
||||
if (variance == -1) {
|
||||
ret = 1;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public PlaceholderType visit(PlaceholderType phty, Integer ht) {
|
||||
if (ht != 0) {
|
||||
if (phty.getVariance() == 0) {
|
||||
phty.setVariance(ht);
|
||||
}
|
||||
//PL 2018-05-17 urspruengliche Variance nicht veraendern
|
||||
//else if (phty.getVariance() != ht) {
|
||||
// phty.setVariance(0);
|
||||
//}
|
||||
}
|
||||
return phty;
|
||||
}
|
||||
|
||||
public FunNType visit(FunNType funnty, Integer ht) {
|
||||
List<UnifyType> param = new ArrayList<>(funnty.getTypeParams().get().length);
|
||||
param.addAll(Arrays.asList(funnty.getTypeParams().get()));
|
||||
UnifyType resultType = param.remove(param.size()-1);
|
||||
Integer htInverse = inverseVariance(ht);
|
||||
param = param.stream()
|
||||
.map(x -> x.accept(this, htInverse))
|
||||
.collect(Collectors.toCollection(ArrayList::new));
|
||||
param.add(resultType.accept(this, ht));
|
||||
return FunNType.getFunNType(new TypeParams(param));
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
@ -0,0 +1,15 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
|
||||
import java.util.HashMap;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
|
||||
|
||||
public class freshPlaceholder extends visitUnifyTypeVisitor<HashMap<PlaceholderType,PlaceholderType>> {
|
||||
|
||||
@Override
|
||||
public PlaceholderType visit(PlaceholderType phty, HashMap<PlaceholderType,PlaceholderType> ht) {
|
||||
return ht.get(phty);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,68 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
|
||||
/**
|
||||
*
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public interface IFiniteClosure {
|
||||
|
||||
public void setLogTrue();
|
||||
/**
|
||||
* Returns all types of the finite closure that are subtypes of the argument.
|
||||
* @return The set of subtypes of the argument.
|
||||
*/
|
||||
public Set<UnifyType> smaller(UnifyType type, Set<UnifyType> fBounded);
|
||||
|
||||
/**
|
||||
* Returns all types of the finite closure that are supertypes of the argument.
|
||||
* @return The set of supertypes of the argument.
|
||||
*/
|
||||
public Set<UnifyType> greater(UnifyType type, Set<UnifyType> fBounded);
|
||||
|
||||
/**
|
||||
* Wo passt Type rein?
|
||||
* @param type
|
||||
* @return
|
||||
*/
|
||||
public Set<UnifyType> grArg(UnifyType type, Set<UnifyType> fBounded);
|
||||
|
||||
/**
|
||||
* Was passt in Type rein?
|
||||
* @param type
|
||||
* @return
|
||||
*/
|
||||
public Set<UnifyType> smArg(UnifyType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Set<UnifyType> grArg(ReferenceType type, Set<UnifyType> fBounded);
|
||||
public Set<UnifyType> smArg(ReferenceType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Set<UnifyType> grArg(ExtendsType type, Set<UnifyType> fBounded);
|
||||
public Set<UnifyType> smArg(ExtendsType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Set<UnifyType> grArg(SuperType type, Set<UnifyType> fBounded);
|
||||
public Set<UnifyType> smArg(SuperType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Set<UnifyType> grArg(PlaceholderType type, Set<UnifyType> fBounded);
|
||||
public Set<UnifyType> smArg(PlaceholderType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Set<UnifyType> grArg(FunNType type, Set<UnifyType> fBounded);
|
||||
public Set<UnifyType> smArg(FunNType type, Set<UnifyType> fBounded);
|
||||
|
||||
public Optional<UnifyType> getLeftHandedType(String typeName);
|
||||
public Set<UnifyType> getAncestors(UnifyType t);
|
||||
public Set<UnifyType> getChildren(UnifyType t);
|
||||
public Set<UnifyType> getAllTypesByName(String typeName);
|
||||
|
||||
public int compare(UnifyType rhsType, UnifyType rhsType2, PairOperator pairop);
|
||||
}
|
||||
@ -0,0 +1,29 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
/**
|
||||
* Match
|
||||
* @author Martin Pluemicke
|
||||
* abgeleitet aus IUnify.java
|
||||
*/
|
||||
public interface IMatch {
|
||||
|
||||
/**
|
||||
* Finds the most general matcher sigma of the set {t1 =. t1',...,tn =. tn'} so that
|
||||
* sigma(t1) = t1' , ... sigma(tn) = tn'.
|
||||
* @param terms The set of terms to be matched
|
||||
* @return An optional of the most general matcher if it exists or an empty optional if there is no matcher.
|
||||
*/
|
||||
public Optional<Unifier> match(ArrayList<UnifyPair> termsList);
|
||||
|
||||
|
||||
}
|
||||
@ -0,0 +1,103 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
/**
|
||||
* Contains the inference rules that are applied to the set Eq.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public interface IRuleSet {
|
||||
|
||||
public Optional<UnifyPair> reduceUp(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceLow(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceUpLow(UnifyPair pair);
|
||||
public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair, IFiniteClosure fc);
|
||||
public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair, IFiniteClosure fc);
|
||||
public Optional<Set<UnifyPair>> reduceEq(UnifyPair pair);
|
||||
public Optional<Set<UnifyPair>> reduce1(UnifyPair pair, IFiniteClosure fc);
|
||||
public Optional<Set<UnifyPair>> reduce2(UnifyPair pair);
|
||||
|
||||
/*
|
||||
* Missing Reduce-Rules for Wildcards
|
||||
*/
|
||||
public Optional<UnifyPair> reduceWildcardLow(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceWildcardLowRight(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceWildcardUp(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceWildcardUpRight(UnifyPair pair);
|
||||
|
||||
/*
|
||||
* vgl. JAVA_BSP/Wildcard6.java
|
||||
public Optional<UnifyPair> reduceWildcardLowUp(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceWildcardUpLow(UnifyPair pair);
|
||||
public Optional<UnifyPair> reduceWildcardLeft(UnifyPair pair);
|
||||
*/
|
||||
|
||||
/*
|
||||
* Additional Rules which replace cases of the cartesian product
|
||||
*/
|
||||
|
||||
/**
|
||||
* Rule that replaces the fourth case of the cartesian product where (a <.? Theta)
|
||||
*/
|
||||
public Optional<UnifyPair> reduceTph(UnifyPair pair);
|
||||
|
||||
/**
|
||||
* Rule that replaces the sixth case of the cartesian product where (? ext Theta <.? a)
|
||||
*/
|
||||
public Optional<Set<UnifyPair>> reduceTphExt(UnifyPair pair);
|
||||
|
||||
/**
|
||||
* Rule that replaces the fourth case of the cartesian product where (? sup Theta <.? a)
|
||||
*/
|
||||
public Optional<Set<UnifyPair>> reduceTphSup(UnifyPair pair);
|
||||
|
||||
/*
|
||||
* FunN Rules
|
||||
*/
|
||||
public Optional<Set<UnifyPair>> reduceFunN(UnifyPair pair);
|
||||
public Optional<Set<UnifyPair>> greaterFunN(UnifyPair pair);
|
||||
public Optional<Set<UnifyPair>> smallerFunN(UnifyPair pair);
|
||||
|
||||
/**
|
||||
* Checks whether the erase1-Rule applies to the pair.
|
||||
* @return True if the pair is erasable, false otherwise.
|
||||
*/
|
||||
public boolean erase1(UnifyPair pair, IFiniteClosure fc);
|
||||
|
||||
/**
|
||||
* Checks whether the erase2-Rule applies to the pair.
|
||||
* @return True if the pair is erasable, false otherwise.
|
||||
*/
|
||||
public boolean erase2(UnifyPair pair, IFiniteClosure fc);
|
||||
|
||||
/**
|
||||
* Checks whether the erase3-Rule applies to the pair.
|
||||
* @return True if the pair is erasable, false otherwise.
|
||||
*/
|
||||
public boolean erase3(UnifyPair pair);
|
||||
|
||||
public Optional<UnifyPair> swap(UnifyPair pair);
|
||||
|
||||
public Optional<UnifyPair> adapt(UnifyPair pair, IFiniteClosure fc);
|
||||
public Optional<UnifyPair> adaptExt(UnifyPair pair, IFiniteClosure fc);
|
||||
public Optional<UnifyPair> adaptSup(UnifyPair pair, IFiniteClosure fc);
|
||||
|
||||
/**
|
||||
* Applies the subst-Rule to a set of pairs (usually Eq').
|
||||
* @param pairs The set of pairs where the subst rule should apply.
|
||||
* @return An optional of the modified set, if there were any substitutions. An empty optional if there were no substitutions.
|
||||
*/
|
||||
public Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs, List<Set<Constraint<UnifyPair>>> oderConstraints);
|
||||
|
||||
/**
|
||||
* Applies the subst-Rule to a set of pairs (usually Eq').
|
||||
* @param pairs The set of pairs where the subst rule should apply.
|
||||
* @return An optional of the modified set, if there were any substitutions. An empty optional if there were no substitutions.
|
||||
*/
|
||||
public Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs);
|
||||
}
|
||||
@ -0,0 +1,16 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
/**
|
||||
* Contains operations on sets.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public interface ISetOperations {
|
||||
/**
|
||||
* Calculates the cartesian product of the sets.
|
||||
* @return The cartesian product
|
||||
*/
|
||||
<B> Set<List<B>> cartesianProduct(List<? extends Set<? extends B>> sets);
|
||||
}
|
||||
@ -0,0 +1,35 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.Arrays;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
|
||||
/**
|
||||
* Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari)
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public interface IUnify {
|
||||
|
||||
/**
|
||||
* Finds the most general unifier sigma of the set {t1 =. t1',...,tn =. tn'} so that
|
||||
* sigma(t1) = sigma(t1') , ... sigma(tn) = sigma(tn').
|
||||
* @param terms The set of terms to be unified
|
||||
* @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
|
||||
*/
|
||||
public Optional<Unifier> unify(Set<UnifyType> terms);
|
||||
|
||||
/**
|
||||
* Finds the most general unifier sigma of the set {t1 =. t1',...,tn =. tn'} so that
|
||||
* sigma(t1) = sigma(t1') , ... sigma(tn) = sigma(tn').
|
||||
* @param terms The set of terms to be unified
|
||||
* @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
|
||||
*/
|
||||
default public Optional<Unifier> unify(UnifyType... terms) {
|
||||
return unify(Arrays.stream(terms).collect(Collectors.toSet()));
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,23 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.HashMap;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
|
||||
public interface UnifyTypeVisitor<T> {
|
||||
|
||||
public ReferenceType visit(ReferenceType refty, T ht);
|
||||
|
||||
public PlaceholderType visit(PlaceholderType phty, T ht);
|
||||
|
||||
public FunNType visit(FunNType funnty, T ht);
|
||||
|
||||
public SuperType visit(SuperType suty, T ht);
|
||||
|
||||
public ExtendsType visit(ExtendsType extty, T ht);
|
||||
|
||||
}
|
||||
@ -0,0 +1,96 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.HashMap;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* An extends wildcard type "? extends T".
|
||||
*/
|
||||
public final class ExtendsType extends WildcardType {
|
||||
|
||||
public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht) {
|
||||
return visitor.visit(this, ht);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a new extends wildcard type.
|
||||
* @param extendedType The extended type e.g. Integer in "? extends Integer"
|
||||
*/
|
||||
public ExtendsType(UnifyType extendedType) {
|
||||
super("? extends " + extendedType.getName(), extendedType);
|
||||
if (extendedType instanceof ExtendsType) {
|
||||
System.out.print("");
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* The extended type e.g. Integer in "? extends Integer"
|
||||
*/
|
||||
public UnifyType getExtendedType() {
|
||||
return wildcardedType;
|
||||
}
|
||||
|
||||
/**
|
||||
* Sets the type parameters of the wildcarded type and returns a new extendstype that extends that type.
|
||||
*/
|
||||
@Override
|
||||
public UnifyType setTypeParams(TypeParams newTp) {
|
||||
UnifyType newType = wildcardedType.setTypeParams(newTp);
|
||||
if(newType == wildcardedType)
|
||||
return this; // Reduced the amount of objects created
|
||||
return new ExtendsType(wildcardedType.setTypeParams(newTp));
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
UnifyType apply(Unifier unif) {
|
||||
UnifyType newType = wildcardedType.apply(unif);
|
||||
if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType))
|
||||
return this; // Reduced the amount of objects created
|
||||
return new ExtendsType(newType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
/*
|
||||
* It is important that the prime that is added is different to the prime added in hashCode() of SuperType.
|
||||
* Otherwise ? extends T and ? super T have the same hashCode() for every Type T.
|
||||
*/
|
||||
return wildcardedType.hashCode() + 229;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof ExtendsType))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
ExtendsType other = (ExtendsType) obj;
|
||||
|
||||
|
||||
return other.getWildcardedType().equals(wildcardedType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "? extends " + wildcardedType;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
@ -0,0 +1,772 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.io.FileWriter;
|
||||
import java.io.IOException;
|
||||
import java.io.Writer;
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Hashtable;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.function.BiFunction;
|
||||
import java.util.function.BinaryOperator;
|
||||
import java.util.function.Predicate;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import com.google.common.collect.Ordering;
|
||||
|
||||
//PL 18-02-05/18-04-05 Unifier durch Matcher ersetzt
|
||||
//muss greater noch ersetzt werden ja erledigt 18--04-05
|
||||
import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.Match;
|
||||
import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
||||
import de.dhbwstuttgart.util.Pair;
|
||||
|
||||
/**
|
||||
* The finite closure for the type unification
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public class FiniteClosure //extends Ordering<UnifyType> //entfernt PL 2018-12-11
|
||||
implements IFiniteClosure {
|
||||
|
||||
Writer logFile;
|
||||
static Boolean log = false;
|
||||
public void setLogTrue() {
|
||||
log = true;
|
||||
}
|
||||
/**
|
||||
* A map that maps every type to the node in the inheritance graph that contains that type.
|
||||
*/
|
||||
private HashMap<UnifyType, Node<UnifyType>> inheritanceGraph;
|
||||
|
||||
/**
|
||||
* A map that maps every typename to the nodes of the inheritance graph that contain a type with that name.
|
||||
*/
|
||||
private HashMap<String, Set<Node<UnifyType>>> strInheritanceGraph;
|
||||
|
||||
|
||||
/**
|
||||
* The initial pairs of that define the inheritance tree
|
||||
*/
|
||||
private Set<UnifyPair> pairs;
|
||||
|
||||
/**
|
||||
* Hastable fuer die greater-Werte, damit sie nicht doppelt berechnet werden muessen
|
||||
*/
|
||||
Hashtable<hashKeyType, Set<UnifyType>> greaterHash = new Hashtable<>();
|
||||
|
||||
/**
|
||||
* Hastable fuer die smaller-Werte, damit sie nicht doppelt berechnet werden muessen
|
||||
*/
|
||||
Hashtable<hashKeyType, Set<UnifyType>> smallerHash = new Hashtable<>();
|
||||
|
||||
/**
|
||||
* Creates a new instance using the inheritance tree defined in the pairs.
|
||||
*/
|
||||
public FiniteClosure(Set<UnifyPair> pairs, Writer logFile) {
|
||||
this.logFile = logFile;
|
||||
this.pairs = new HashSet<>(pairs);
|
||||
inheritanceGraph = new HashMap<UnifyType, Node<UnifyType>>();
|
||||
|
||||
// Build the transitive closure of the inheritance tree
|
||||
for(UnifyPair pair : pairs) {
|
||||
|
||||
/*
|
||||
try {
|
||||
logFile.write("Pair: " + pair + "\n");
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");
|
||||
}
|
||||
*/
|
||||
|
||||
if(pair.getPairOp() != PairOperator.SMALLER)
|
||||
continue;
|
||||
|
||||
//VERSUCH PL 18-02-06
|
||||
//koennte ggf. die FC reduzieren
|
||||
//TO DO: Ueberpruefen, ob das sinnvll und korrekt ist
|
||||
//if (!pair.getLhsType().getTypeParams().arePlaceholders()
|
||||
// && !pair.getRhsType().getTypeParams().arePlaceholders())
|
||||
// continue;
|
||||
;
|
||||
// Add nodes if not already in the graph
|
||||
if(!inheritanceGraph.containsKey(pair.getLhsType()))
|
||||
inheritanceGraph.put(pair.getLhsType(), new Node<UnifyType>(pair.getLhsType()));
|
||||
if(!inheritanceGraph.containsKey(pair.getRhsType()))
|
||||
inheritanceGraph.put(pair.getRhsType(), new Node<UnifyType>(pair.getRhsType()));
|
||||
|
||||
Node<UnifyType> childNode = inheritanceGraph.get(pair.getLhsType());
|
||||
Node<UnifyType> parentNode = inheritanceGraph.get(pair.getRhsType());
|
||||
|
||||
// Add edge
|
||||
parentNode.addDescendant(childNode);
|
||||
|
||||
// Add edges to build the transitive closure
|
||||
parentNode.getPredecessors().stream().forEach(x -> x.addDescendant(childNode));
|
||||
childNode.getDescendants().stream().forEach(x -> x.addPredecessor(parentNode));
|
||||
|
||||
//PL eingefuegt 2020-05-07 File UnitTest InheritTest.java
|
||||
this.inheritanceGraph.forEach((x,y) -> { if (y.getDescendants().contains(parentNode)) { y.addDescendant(childNode); y.addAllDescendant(childNode.getDescendants());};
|
||||
if (y.getPredecessors().contains(childNode)) { y.addPredecessor(parentNode); y.addAllPredecessor(parentNode.getPredecessors());};} );
|
||||
}
|
||||
|
||||
// Build the alternative representation with strings as keys
|
||||
strInheritanceGraph = new HashMap<>();
|
||||
for(UnifyType key : inheritanceGraph.keySet()) {
|
||||
if(!strInheritanceGraph.containsKey(key.getName()))
|
||||
strInheritanceGraph.put(key.getName(), new HashSet<>());
|
||||
|
||||
strInheritanceGraph.get(key.getName()).add(inheritanceGraph.get(key));
|
||||
}
|
||||
}
|
||||
|
||||
void testSmaller() {
|
||||
UnifyType tq1, tq2, tq3;
|
||||
tq1 = new ExtendsType(PlaceholderType.freshPlaceholder());
|
||||
List<UnifyType> l1 = new ArrayList<>();
|
||||
List<UnifyType> l2 = new ArrayList<>();
|
||||
l1.add(tq1);
|
||||
tq2 = new ReferenceType("java.util.Vector", new TypeParams(l1));
|
||||
l2.add(tq2);
|
||||
tq3 = new ReferenceType("java.util.Vector", new TypeParams(l2));
|
||||
Set<UnifyType> smaller = smaller(tq3, new HashSet<>());
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns all types of the finite closure that are subtypes of the argument.
|
||||
* @return The set of subtypes of the argument.
|
||||
*/
|
||||
@Override
|
||||
public Set<UnifyType> smaller(UnifyType type, Set<UnifyType> fBounded) {
|
||||
|
||||
Set<UnifyType> ret;
|
||||
if ((ret = smallerHash.get(new hashKeyType(type))) != null) {
|
||||
//System.out.println(greaterHash);
|
||||
return new HashSet<>(ret);
|
||||
}
|
||||
|
||||
if(type instanceof FunNType)
|
||||
return computeSmallerFunN((FunNType) type, fBounded);
|
||||
|
||||
Set<Pair<UnifyType,Set<UnifyType>>> ts = new HashSet<>();
|
||||
ts.add(new Pair<>(type, fBounded));
|
||||
Set<UnifyType> result = computeSmaller(ts);
|
||||
smallerHash.put(new hashKeyType(type), result);
|
||||
/*
|
||||
try {
|
||||
logFile.write("\ntype: " + type + "\nret: " + ret + "\nresult: " + result);//"smallerHash: " + greaterHash.toString());
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");
|
||||
}*/
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* Computes the smaller functions for every type except FunNTypes.
|
||||
*/
|
||||
private Set<UnifyType> computeSmaller(Set<Pair<UnifyType,Set<UnifyType>>> types) {
|
||||
Set<Pair<UnifyType,Set<UnifyType>>> result = new HashSet<>();
|
||||
|
||||
//PL 18-02-05 Unifier durch Matcher ersetzt
|
||||
//IUnify unify = new MartelliMontanariUnify();
|
||||
Match match = new Match();
|
||||
|
||||
for(Pair<UnifyType,Set<UnifyType>> pt : types) {
|
||||
UnifyType t = pt.getKey();
|
||||
Set<UnifyType> fBounded = pt.getValue().get();
|
||||
|
||||
// if T = T' then T <* T'
|
||||
try {
|
||||
result.add(new Pair<>(t, fBounded));
|
||||
}
|
||||
catch (StackOverflowError e) {
|
||||
System.out.println("");
|
||||
}
|
||||
|
||||
// if C<...> <* C<...> then ... (third case in definition of <*)
|
||||
if(t.getTypeParams().size() > 0) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (int i = 0; i < t.getTypeParams().size(); i++)
|
||||
paramCandidates.add(smArg(t.getTypeParams().get(i), fBounded));
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(new Pair<>(t.setTypeParams(x), fBounded)));
|
||||
}
|
||||
|
||||
if(!strInheritanceGraph.containsKey(t.getName()))
|
||||
continue;
|
||||
|
||||
// if T <* T' then sigma(T) <* sigma(T')
|
||||
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName()); //cadidates= [???Node(java.util.Vector<java.util.Vector<java.lang.Integer>>)???
|
||||
// , Node(java.util.Vector<gen_hv>)
|
||||
//]
|
||||
for(Node<UnifyType> candidate : candidates) {
|
||||
UnifyType theta2 = candidate.getContent();
|
||||
//PL 18-02-05 Unifier durch Matcher ersetzt ANFANG
|
||||
ArrayList<UnifyPair> termList= new ArrayList<UnifyPair>();
|
||||
termList.add(new UnifyPair(theta2,t, PairOperator.EQUALSDOT));
|
||||
Optional<Unifier> optSigma = match.match(termList);
|
||||
//PL 18-02-05 Unifier durch Matcher ersetzt ENDE
|
||||
if(!optSigma.isPresent())
|
||||
continue;
|
||||
|
||||
Unifier sigma = optSigma.get();
|
||||
sigma.swapPlaceholderSubstitutions(t.getTypeParams());
|
||||
|
||||
Set<UnifyType> theta1Set = candidate.getContentOfDescendants();
|
||||
|
||||
for(UnifyType theta1 : theta1Set)
|
||||
result.add(new Pair<>(theta1.apply(sigma), fBounded));
|
||||
}
|
||||
}
|
||||
|
||||
HashSet<UnifyType> resut = result.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new));
|
||||
if(resut.equals(types.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new))))
|
||||
return resut;
|
||||
return computeSmaller(result);
|
||||
}
|
||||
|
||||
/**
|
||||
* Computes the smaller-Function for FunNTypes.
|
||||
*/
|
||||
private Set<UnifyType> computeSmallerFunN(FunNType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<>();
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result.add(type);
|
||||
|
||||
// Because real function types are implicitly variant
|
||||
// it is enough to permute the params with the values of greater / smaller.
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
paramCandidates.add(smaller(type.getTypeParams().get(0), fBounded));
|
||||
for (int i = 1; i < type.getTypeParams().size(); i++)
|
||||
paramCandidates.add(greater(type.getTypeParams().get(i), new HashSet<>()));
|
||||
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns all types of the finite closure that are supertypes of the argument.
|
||||
* @return The set of supertypes of the argument.
|
||||
*/
|
||||
@Override
|
||||
//Eingefuegt PL 2018-05-24 F-Bounded Problematik
|
||||
public Set<UnifyType> greater(UnifyType type, Set<UnifyType> fBounded) {
|
||||
|
||||
Set<UnifyType> ret;
|
||||
if ((ret = greaterHash.get(new hashKeyType(type))) != null) {
|
||||
//System.out.println(greaterHash);
|
||||
return new HashSet<>(ret);
|
||||
}
|
||||
|
||||
|
||||
if(type instanceof FunNType) {
|
||||
return computeGreaterFunN((FunNType) type, fBounded);
|
||||
}
|
||||
|
||||
Set<UnifyType> result = new HashSet<>();
|
||||
Set<Pair<UnifyType,Set<UnifyType>>> PairResultFBounded = new HashSet<>();
|
||||
|
||||
Match match = new Match();
|
||||
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result.add(type);
|
||||
if(!strInheritanceGraph.containsKey(type.getName()))
|
||||
return result;
|
||||
|
||||
// if T <* T' then sigma(T) <* sigma(T')
|
||||
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(type.getName());
|
||||
|
||||
/*
|
||||
try {
|
||||
if (log) logFile.write(candidates.toString());
|
||||
//log = false;
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");
|
||||
}
|
||||
*/
|
||||
|
||||
for(Node<UnifyType> candidate : candidates) {
|
||||
UnifyType theta1 = candidate.getContent();
|
||||
|
||||
//PL 18-04-05 Unifier durch Matcher ersetzt ANFANG
|
||||
ArrayList<UnifyPair> termList= new ArrayList<UnifyPair>();
|
||||
termList.add(new UnifyPair(theta1,type, PairOperator.EQUALSDOT));
|
||||
Optional<Unifier> optSigma = match.match(termList);
|
||||
//PL 18-04-05 Unifier durch Matcher ersetzt ENDE
|
||||
if(!optSigma.isPresent()) {
|
||||
continue;
|
||||
}
|
||||
Unifier sigma = optSigma.get();
|
||||
sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams());
|
||||
|
||||
Set<UnifyType> fBoundedNew = new HashSet<>(fBounded);
|
||||
fBoundedNew.add(theta1);
|
||||
Set<UnifyType> theta2Set = candidate.getContentOfPredecessors();
|
||||
//System.out.println("");
|
||||
for(UnifyType theta2 : theta2Set) {
|
||||
result.add(theta2.apply(sigma));
|
||||
PairResultFBounded.add(new Pair<>(theta2.apply(sigma), fBoundedNew));
|
||||
}
|
||||
}
|
||||
/*
|
||||
try {
|
||||
if (log) logFile.write(PairResultFBounded.toString());
|
||||
log = false;
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");
|
||||
}
|
||||
*/
|
||||
for(Pair<UnifyType,Set<UnifyType>> pt : PairResultFBounded) {
|
||||
UnifyType t = pt.getKey();
|
||||
Set<UnifyType> lfBounded = pt.getValue().get();
|
||||
|
||||
// if C<...> <* C<...> then ... (third case in definition of <*)
|
||||
//TypeParams typeparams = t.getTypeParams();
|
||||
if(t.getTypeParams().size() > 0) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
|
||||
for (int i = 0; i < t.getTypeParams().size(); i++) {
|
||||
//UnifyType parai = t.getTypeParams().get(i);
|
||||
int i_ef = i;
|
||||
BiFunction<Boolean,UnifyType,Boolean> f = (x,y) ->
|
||||
{
|
||||
ArrayList<UnifyPair> termList = new ArrayList<UnifyPair>();
|
||||
termList.add(new UnifyPair(y,t.getTypeParams().get(i_ef), PairOperator.EQUALSDOT));
|
||||
return ((match.match(termList).isPresent()) || x);
|
||||
};
|
||||
//if (parai.getName().equals("java.lang.Integer")) {
|
||||
// System.out.println("");
|
||||
//}
|
||||
BinaryOperator<Boolean> bo = (a,b) -> (a || b);
|
||||
if (lfBounded.stream().reduce(false,f,bo)) {
|
||||
//F-Bounded Endlosrekursion
|
||||
HashSet<UnifyType> res = new HashSet<UnifyType>();
|
||||
paramCandidates.add(res);
|
||||
}
|
||||
else {
|
||||
paramCandidates.add(grArg(t.getTypeParams().get(i), new HashSet<>(fBounded) ));
|
||||
}
|
||||
}
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x)));
|
||||
//System.out.println("");
|
||||
}
|
||||
}
|
||||
|
||||
greaterHash.put(new hashKeyType(type), result);
|
||||
/*
|
||||
try {
|
||||
logFile.write("\ntype: " + type + "\nret: " + ret + "\nresult: " + result);//"greaterHash: " + greaterHash.toString());
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");
|
||||
}*/
|
||||
return result;
|
||||
}
|
||||
|
||||
/* auskommentiert PL 2018-05-24
|
||||
/**
|
||||
* Returns all types of the finite closure that are supertypes of the argument.
|
||||
* @return The set of supertypes of the argument.
|
||||
*
|
||||
//@Override
|
||||
public Set<UnifyType> oldgreater(UnifyType type, Set<UnifyType> fBounded) {
|
||||
if(type instanceof FunNType)
|
||||
return computeGreaterFunN((FunNType) type, fBounded);
|
||||
|
||||
Set<Pair<UnifyType,Set<UnifyType>>> ts = new HashSet<>();
|
||||
ts.add(new Pair<>(type, fBounded));
|
||||
return computeGreater(ts);
|
||||
}
|
||||
|
||||
/**
|
||||
* Computes the greater function for all types except function types.
|
||||
*
|
||||
protected Set<UnifyType> computeGreater(Set<Pair<UnifyType,Set<UnifyType>>> types) {
|
||||
Set<Pair<UnifyType,Set<UnifyType>>> result = new HashSet<>();
|
||||
|
||||
//PL 18-04-05 Unifier durch Matcher ersetzt
|
||||
//IUnify unify = new MartelliMontanariUnify();
|
||||
Match match = new Match();
|
||||
|
||||
for(Pair<UnifyType,Set<UnifyType>> pt : types) {
|
||||
UnifyType t = pt.getKey();
|
||||
Set<UnifyType> fBounded = pt.getValue().get();
|
||||
// if T = T' then T <=* T'
|
||||
result.add(pt);
|
||||
|
||||
// if C<...> <* C<...> then ... (third case in definition of <*)
|
||||
if(t.getTypeParams().size() > 0) {
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
for (int i = 0; i < t.getTypeParams().size(); i++) {
|
||||
UnifyType parai = t.getTypeParams().get(i);
|
||||
int i_ef = i;
|
||||
BiFunction<Boolean,UnifyType,Boolean> f = (x,y) ->
|
||||
{
|
||||
ArrayList<UnifyPair> termList = new ArrayList<UnifyPair>();
|
||||
termList.add(new UnifyPair(y,t.getTypeParams().get(i_ef), PairOperator.EQUALSDOT));
|
||||
return ((match.match(termList).isPresent()) || x);
|
||||
};
|
||||
if (parai.getName().equals("java.lang.Integer")) {
|
||||
System.out.println("");
|
||||
}
|
||||
BinaryOperator<Boolean> bo = (a,b) -> (a || b);
|
||||
if (fBounded.stream().reduce(false,f,bo)) continue; //F-Bounded Endlosrekursion
|
||||
paramCandidates.add(grArg(t.getTypeParams().get(i), new HashSet<>(fBounded) ));
|
||||
}
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(new Pair<>(t.setTypeParams(x), new HashSet<>(fBounded))));
|
||||
}
|
||||
|
||||
if(!strInheritanceGraph.containsKey(t.getName()))
|
||||
continue;
|
||||
|
||||
// if T <* T' then sigma(T) <* sigma(T')
|
||||
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
|
||||
for(Node<UnifyType> candidate : candidates) {
|
||||
UnifyType theta1 = candidate.getContent();
|
||||
|
||||
//PL 18-04-05 Unifier durch Matcher ersetzt ANFANG
|
||||
ArrayList<UnifyPair> termList= new ArrayList<UnifyPair>();
|
||||
termList.add(new UnifyPair(theta1,t, PairOperator.EQUALSDOT));
|
||||
Optional<Unifier> optSigma = match.match(termList);
|
||||
//PL 18-04-05 Unifier durch Matcher ersetzt ENDE
|
||||
if(!optSigma.isPresent())
|
||||
continue;
|
||||
|
||||
Unifier sigma = optSigma.get();
|
||||
sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams());
|
||||
|
||||
Set<UnifyType> fBoundedNew = new HashSet<>(fBounded);
|
||||
fBoundedNew.add(theta1);
|
||||
Set<UnifyType> theta2Set = candidate.getContentOfPredecessors();
|
||||
|
||||
for(UnifyType theta2 : theta2Set)
|
||||
result.add(new Pair<>(theta2.apply(sigma), fBoundedNew));
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
HashSet<UnifyType> resut = result.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new));
|
||||
System.out.println(resut);
|
||||
if(resut.equals(types.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new))))
|
||||
return resut;
|
||||
return computeGreater(result);
|
||||
}
|
||||
*/
|
||||
|
||||
/**
|
||||
* Computes the greater function for FunN-Types
|
||||
*/
|
||||
protected Set<UnifyType> computeGreaterFunN(FunNType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<>();
|
||||
|
||||
// if T = T' then T <=* T'
|
||||
result.add(type);
|
||||
|
||||
// Because real function types are implicitly variant
|
||||
// it is enough to permute the params with the values of greater / smaller.
|
||||
ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
|
||||
paramCandidates.add(greater(type.getTypeParams().get(0), new HashSet<>()));
|
||||
for (int i = 1; i < type.getTypeParams().size(); i++)
|
||||
paramCandidates.add(smaller(type.getTypeParams().get(i), fBounded));
|
||||
permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(UnifyType type, Set<UnifyType> fBounded) {
|
||||
return type.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(ReferenceType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
smaller(type, fBounded).forEach(x -> result.add(new SuperType(x)));
|
||||
greater(type,fBounded).forEach(x -> result.add(new ExtendsType(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(FunNType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
smaller(type, fBounded).forEach(x -> result.add(new SuperType(x)));
|
||||
greater(type, fBounded).forEach(x -> result.add(new ExtendsType(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(ExtendsType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
UnifyType t = type.getExtendedType();
|
||||
greater(t, fBounded).forEach(x -> result.add(new ExtendsType(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(SuperType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
UnifyType t = type.getSuperedType();
|
||||
smaller(t, fBounded).forEach(x -> result.add(new SuperType(x)));
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> grArg(PlaceholderType type, Set<UnifyType> fBounded) {
|
||||
HashSet<UnifyType> result = new HashSet<>();
|
||||
result.add(type);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(UnifyType type, Set<UnifyType> fBounded) {
|
||||
return type.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(ReferenceType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(FunNType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(ExtendsType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
UnifyType t = type.getExtendedType();
|
||||
result.add(t);
|
||||
smaller(t, fBounded).forEach(x -> {
|
||||
result.add(new ExtendsType(x));
|
||||
result.add(x);
|
||||
});
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(SuperType type, Set<UnifyType> fBounded) {
|
||||
Set<UnifyType> result = new HashSet<UnifyType>();
|
||||
result.add(type);
|
||||
UnifyType t = type.getSuperedType();
|
||||
result.add(t);
|
||||
//*** ACHTUNG das koennte FALSCH sein PL 2018-05-23 evtl. HashSet durch smArg durchschleifen
|
||||
greater(t, fBounded).forEach(x -> {
|
||||
result.add(new SuperType(x));
|
||||
result.add(x);
|
||||
});
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> smArg(PlaceholderType type, Set<UnifyType> fBounded) {
|
||||
HashSet<UnifyType> result = new HashSet<>();
|
||||
result.add(type);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> getAllTypesByName(String typeName) {
|
||||
if(!strInheritanceGraph.containsKey(typeName))
|
||||
return new HashSet<>();
|
||||
return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new));
|
||||
}
|
||||
|
||||
@Override
|
||||
public Optional<UnifyType> getLeftHandedType(String typeName) {
|
||||
if(!strInheritanceGraph.containsKey(typeName))
|
||||
return Optional.empty();
|
||||
|
||||
for(UnifyPair pair : pairs)
|
||||
if(pair.getLhsType().getName().equals(typeName) && pair.getLhsType().typeParams.arePlaceholders())
|
||||
return Optional.of(pair.getLhsType());
|
||||
|
||||
return Optional.empty();
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> getAncestors(UnifyType t) {
|
||||
if(!inheritanceGraph.containsKey(t))
|
||||
return new HashSet<>();
|
||||
Set<UnifyType> result = inheritanceGraph.get(t).getContentOfPredecessors();
|
||||
result.add(t);
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<UnifyType> getChildren(UnifyType t) {
|
||||
if(!inheritanceGraph.containsKey(t))
|
||||
return new HashSet<>();
|
||||
Set<UnifyType> result = inheritanceGraph.get(t).getContentOfDescendants();
|
||||
result.add(t);
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* Takes a set of candidates for each position and computes all possible permutations.
|
||||
* @param candidates The length of the list determines the number of type params. Each set
|
||||
* contains the candidates for the corresponding position.
|
||||
*/
|
||||
protected Set<TypeParams> permuteParams(ArrayList<Set<UnifyType>> candidates) {
|
||||
Set<TypeParams> result = new HashSet<>();
|
||||
permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* Takes a set of candidates for each position and computes all possible permutations.
|
||||
* @param candidates The length of the list determines the number of type params. Each set
|
||||
* contains the candidates for the corresponding position.
|
||||
* @param idx Idx for the current permutatiton.
|
||||
* @param result Set of all permutations found so far
|
||||
* @param current The permutation of type params that is currently explored
|
||||
*/
|
||||
protected void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
|
||||
if(candidates.size() == idx) {
|
||||
result.add(new TypeParams(Arrays.copyOf(current, current.length)));
|
||||
return;
|
||||
}
|
||||
|
||||
Set<UnifyType> localCandidates = candidates.get(idx);
|
||||
|
||||
for(UnifyType t : localCandidates) {
|
||||
current[idx] = t;
|
||||
permuteParams(candidates, idx+1, result, current);
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString(){
|
||||
return this.inheritanceGraph.toString();
|
||||
}
|
||||
|
||||
/* entfernt PL 2018-12-11
|
||||
public int compare (UnifyType left, UnifyType right) {
|
||||
return compare(left, right, PairOperator.SMALLERDOT);
|
||||
}
|
||||
*/
|
||||
|
||||
public int compare (UnifyType left, UnifyType right, PairOperator pairop) {
|
||||
//try {logFile.write("left: "+ left + " right: " + right + " pairop: " + pairop);} catch (IOException ie) {}
|
||||
if (left.getName().equals("Matrix") || right.getName().equals("Matrix"))
|
||||
System.out.println("");
|
||||
/*
|
||||
pairop = PairOperator.SMALLERDOTWC;
|
||||
List<UnifyType> al = new ArrayList<>();
|
||||
PlaceholderType xx =new PlaceholderType("xx");
|
||||
al.add(xx);
|
||||
left = new ExtendsType(new ReferenceType("Vector", new TypeParams(al)));
|
||||
|
||||
List<UnifyType> alr = new ArrayList<>();
|
||||
UnifyType exx = new ExtendsType(xx);
|
||||
alr.add(exx);
|
||||
right = new ExtendsType(new ReferenceType("Vector", new TypeParams(alr)));
|
||||
*/
|
||||
/*
|
||||
List<UnifyType> al = new ArrayList<>();
|
||||
PlaceholderType xx =new PlaceholderType("xx");
|
||||
al.add(xx);
|
||||
left = new ExtendsType(xx);
|
||||
right = xx;
|
||||
*/
|
||||
/*
|
||||
List<UnifyType> al = new ArrayList<>();
|
||||
PlaceholderType xx =new PlaceholderType("xx");
|
||||
PlaceholderType yy =new PlaceholderType("yy");
|
||||
al.add(xx);
|
||||
left = yy;
|
||||
right = new ExtendsType(xx);
|
||||
*/
|
||||
//Die Faelle abfangen, bei den Variablen verglichen werden PL 2018-12-11
|
||||
UnifyType ex;
|
||||
if (left instanceof PlaceholderType) {
|
||||
if ((right instanceof WildcardType)
|
||||
&& ((ex = ((WildcardType)right).wildcardedType) instanceof PlaceholderType)
|
||||
&& ((PlaceholderType)left).getName().equals(((PlaceholderType)ex).getName())) {// a <.? ? extends a oder a <.? ? super a
|
||||
return -1;
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
if (right instanceof PlaceholderType) {//&& (left instanceof WildcardType)) {PL geloescht 2019-01-15 analog zu oben
|
||||
if ((left instanceof WildcardType) //PL eingefuegt 2019-01-15 analog zu oben
|
||||
&& ((ex = ((WildcardType)left).wildcardedType) instanceof PlaceholderType)
|
||||
&& ((PlaceholderType)right).getName().equals(((PlaceholderType)ex).getName())) {// ? extends a <. a oder ? super a <. a
|
||||
return 1;
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
UnifyPair up = new UnifyPair(left, right, pairop);
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask();
|
||||
HashSet<UnifyPair> hs = new HashSet<>();
|
||||
hs.add(up);
|
||||
Set<UnifyPair> smallerRes = unifyTask.applyTypeUnificationRules(hs, this);
|
||||
/*
|
||||
//if (left.getName().equals("Matrix") || right.getName().equals("Matrix"))
|
||||
{try {
|
||||
logFile.write("\nsmallerRes: " + smallerRes);//"smallerHash: " + greaterHash.toString());
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");}}
|
||||
*/
|
||||
//Gleichungen der Form a <./=. Theta oder Theta <./=. a oder a <./=. b sind ok.
|
||||
Predicate<UnifyPair> delFun = x -> !((x.getLhsType() instanceof PlaceholderType ||
|
||||
x.getRhsType() instanceof PlaceholderType)
|
||||
&& !((x.getLhsType() instanceof WildcardType) && //? extends/super a <.? a
|
||||
((WildcardType)x.getLhsType()).getWildcardedType().equals(x.getRhsType()))
|
||||
);
|
||||
long smallerLen = smallerRes.stream().filter(delFun).count();
|
||||
if (smallerLen == 0) return -1;
|
||||
else {
|
||||
up = new UnifyPair(right, left, pairop);
|
||||
//TypeUnifyTask unifyTask = new TypeUnifyTask();
|
||||
hs = new HashSet<>();
|
||||
hs.add(up);
|
||||
Set<UnifyPair> greaterRes = unifyTask.applyTypeUnificationRules(hs, this);
|
||||
/*
|
||||
//if (left.getName().equals("Matrix") || right.getName().equals("Matrix"))
|
||||
{try {
|
||||
logFile.write("\ngreaterRes: " + greaterRes);//"smallerHash: " + greaterHash.toString());
|
||||
logFile.flush();
|
||||
}
|
||||
catch (IOException e) {
|
||||
System.err.println("no LogFile");}}
|
||||
*/
|
||||
//Gleichungen der Form a <./=. Theta oder Theta <./=. a oder a <./=. b sind ok.
|
||||
long greaterLen = greaterRes.stream().filter(delFun).count();
|
||||
if (greaterLen == 0) return 1;
|
||||
else {
|
||||
//try {logFile.write("0 left: "+ left + " right: " + right + " pairop: " + pairop);} catch (IOException ie) {}
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,103 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.HashMap;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* A real function type in java.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public class FunNType extends UnifyType {
|
||||
|
||||
public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht) {
|
||||
return visitor.visit(this, ht);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a FunN-Type with the specified TypeParameters.
|
||||
*/
|
||||
protected FunNType(TypeParams p) {
|
||||
super("Fun"+(p.size()-1)+"$$", p);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a new FunNType.
|
||||
* @param tp The parameters of the type.
|
||||
* @return A FunNType.
|
||||
* @throws IllegalArgumentException is thrown when there are to few type parameters or there are wildcard-types.
|
||||
*/
|
||||
public static FunNType getFunNType(TypeParams tp) throws IllegalArgumentException {
|
||||
if(tp.size() == 0)
|
||||
throw new IllegalArgumentException("FunNTypes need at least one type parameter");
|
||||
for(UnifyType t : tp)
|
||||
if(t instanceof WildcardType)
|
||||
throw new IllegalArgumentException("Invalid TypeParams for a FunNType: " + tp);
|
||||
return new FunNType(tp);
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the degree of the function type, e.g. 2 for FunN<Integer, Integer, Integer>.
|
||||
*/
|
||||
public int getN() {
|
||||
return typeParams.size()-1;
|
||||
}
|
||||
|
||||
@Override
|
||||
public UnifyType setTypeParams(TypeParams newTp) {
|
||||
if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams))
|
||||
return this;
|
||||
return getFunNType(newTp);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
UnifyType apply(Unifier unif) {
|
||||
// TODO this bypasses the validation of the type parameters.
|
||||
// Wildcard types can be unified into FunNTypes.
|
||||
TypeParams newParams = typeParams.apply(unif);
|
||||
if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams))
|
||||
return this;
|
||||
|
||||
return new FunNType(newParams);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Boolean wrongWildcard() {
|
||||
return (new ArrayList<UnifyType>(Arrays.asList(getTypeParams()
|
||||
.get())).stream().filter(x -> (x instanceof WildcardType)).findFirst().isPresent());
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return 181 + typeParams.hashCode();
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof FunNType))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
FunNType other = (FunNType) obj;
|
||||
|
||||
return other.getTypeParams().equals(typeParams);
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,118 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
/**
|
||||
* A node of a directed graph.
|
||||
* @author Florian Steurer
|
||||
*
|
||||
* @param <T> The type of the content of the node.
|
||||
*/
|
||||
class Node<T> {
|
||||
|
||||
/**
|
||||
* The content of the node.
|
||||
*/
|
||||
private T content;
|
||||
|
||||
/**
|
||||
* The set of predecessors
|
||||
*/
|
||||
private HashSet<Node<T>> predecessors = new HashSet<>();
|
||||
|
||||
/**
|
||||
* The set of descendants
|
||||
*/
|
||||
private HashSet<Node<T>> descendants = new HashSet<>();
|
||||
|
||||
/**
|
||||
* Creates a node containing the specified content.
|
||||
*/
|
||||
public Node(T content) {
|
||||
this.content = content;
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a directed edge from this node to the descendant (this -> descendant)
|
||||
*/
|
||||
public void addDescendant(Node<T> descendant) {
|
||||
if(descendants.contains(descendant))
|
||||
return;
|
||||
|
||||
descendants.add(descendant);
|
||||
descendant.addPredecessor(this);
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds some directed edges from this node to the descendant (this -> descendant)
|
||||
*/
|
||||
public void addAllDescendant(Set<Node<T>> allDescendants) {
|
||||
for(Node<T> descendant: allDescendants) {
|
||||
addDescendant(descendant);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a directed edge from the predecessor to this node (predecessor -> this)
|
||||
*/
|
||||
public void addPredecessor(Node<T> predecessor) {
|
||||
if(predecessors.contains(predecessor))
|
||||
return;
|
||||
|
||||
predecessors.add(predecessor);
|
||||
predecessor.addDescendant(this);
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds some directed edges from the predecessor to this node (predecessor -> this)
|
||||
*/
|
||||
public void addAllPredecessor(Set<Node<T>> allPredecessors) {
|
||||
for(Node<T> predecessor: allPredecessors) {
|
||||
addPredecessor(predecessor);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* The content of this node.
|
||||
*/
|
||||
public T getContent() {
|
||||
return content;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns all predecessors (nodes that have a directed edge to this node)
|
||||
*/
|
||||
public Set<Node<T>> getPredecessors() {
|
||||
return predecessors;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns all descendants. All nodes M, where there is a edge from this node to the node M.
|
||||
* @return
|
||||
*/
|
||||
public Set<Node<T>> getDescendants() {
|
||||
return descendants;
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieves the content of all descendants.
|
||||
*/
|
||||
public Set<T> getContentOfDescendants() {
|
||||
return descendants.stream().map(x -> x.getContent()).collect(Collectors.toSet());
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieves the content of all predecessors.
|
||||
*/
|
||||
public Set<T> getContentOfPredecessors() {
|
||||
return predecessors.stream().map(x -> x.getContent()).collect(Collectors.toSet());
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "Elem: Node(" + content.toString() + ")\nPrec: " + getContentOfPredecessors().toString()
|
||||
+ "\nDesc: " + getContentOfDescendants().toString() + "\n\n";
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,89 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
public abstract class OrderingExtend<T> extends com.google.common.collect.Ordering<T> {
|
||||
|
||||
public List<T> maxElements(Iterable<T> iterable) {
|
||||
ArrayList<T> ret = new ArrayList<>();
|
||||
while (iterable.iterator().hasNext()) {
|
||||
Set<T> believe = new HashSet<>();
|
||||
|
||||
T max = max(iterable);
|
||||
ret.add(max);
|
||||
|
||||
Iterator<T> it = iterable.iterator();
|
||||
while (it.hasNext()) {
|
||||
T elem = it.next();
|
||||
if (!(compare(max, elem) == 1) && !max.equals(elem)) {
|
||||
believe.add(elem);
|
||||
}
|
||||
}
|
||||
iterable = believe;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
public List<T> minElements(Iterable<T> iterable) {
|
||||
ArrayList<T> ret = new ArrayList<>();
|
||||
while (iterable.iterator().hasNext()) {
|
||||
Set<T> believe = new HashSet<>();
|
||||
|
||||
T min = min(iterable);
|
||||
ret.add(min);
|
||||
|
||||
Iterator<T> it = iterable.iterator();
|
||||
while (it.hasNext()) {
|
||||
T elem = it.next();
|
||||
if (!(compare(min, elem) == -1) && !min.equals(elem)) {
|
||||
believe.add(elem);
|
||||
}
|
||||
}
|
||||
iterable = believe;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
public List<T> smallerEqThan(T elem, Iterable<T> iterable) {
|
||||
List<T> ret = smallerThan(elem, iterable);
|
||||
ret.add(elem);
|
||||
return ret;
|
||||
|
||||
}
|
||||
|
||||
public List<T> smallerThan(T elem, Iterable<T> iterable) {
|
||||
ArrayList<T> ret = new ArrayList<>();
|
||||
Iterator<T> it = iterable.iterator();
|
||||
while (it.hasNext()) {
|
||||
T itElem = it.next();
|
||||
if (!itElem.equals(elem) && compare(elem, itElem) == 1) {
|
||||
ret.add(itElem);
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
public List<T> greaterEqThan(T elem, Iterable<T> iterable) {
|
||||
List<T> ret = greaterThan(elem, iterable);
|
||||
ret.add(elem);
|
||||
return ret;
|
||||
|
||||
}
|
||||
|
||||
public List<T> greaterThan(T elem, Iterable<T> iterable) {
|
||||
ArrayList<T> ret = new ArrayList<>();
|
||||
Iterator<T> it = iterable.iterator();
|
||||
while (it.hasNext()) {
|
||||
T itElem = it.next();
|
||||
if (!itElem.equals(elem) && (compare(elem, itElem) == -1)) {
|
||||
ret.add(itElem);
|
||||
}
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,457 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.io.IOException;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.LinkedList;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.function.BinaryOperator;
|
||||
import java.util.function.Function;
|
||||
import java.util.stream.Collectors;
|
||||
import java.util.stream.Stream;
|
||||
|
||||
import com.google.common.collect.Ordering;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.Match;
|
||||
import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.util.Pair;
|
||||
|
||||
|
||||
|
||||
public class OrderingUnifyPair extends OrderingExtend<Set<UnifyPair>> {
|
||||
|
||||
protected IFiniteClosure fc;
|
||||
|
||||
public OrderingUnifyPair(IFiniteClosure fc) {
|
||||
this.fc = fc;
|
||||
}
|
||||
|
||||
/*
|
||||
* vergleicht Paare (a =. Theta) und (a =. Theta')
|
||||
* in dem compare(Theta, Theta') aufgerufen wird.
|
||||
*/
|
||||
public int compareEq (UnifyPair left, UnifyPair right) {
|
||||
try {
|
||||
//if (left.getRhsType() instanceof WildcardType || right.getRhsType() instanceof WildcardType) {//PL 2019-01-12 ausgetauscht
|
||||
if (((PlaceholderType)left.getLhsType()).isInnerType() && ((PlaceholderType)right.getLhsType()).isInnerType()) {
|
||||
return fc.compare(left.getRhsType(), right.getRhsType(), PairOperator.SMALLERDOTWC);
|
||||
}
|
||||
else {
|
||||
return fc.compare(left.getRhsType(), right.getRhsType(), PairOperator.SMALLERDOT);
|
||||
}}
|
||||
catch (ClassCastException e) {
|
||||
try {
|
||||
((FiniteClosure)fc).logFile.write("ClassCastException: " + left.toString() + " " + left.getGroundBasePair() + "\n\n");
|
||||
((FiniteClosure)fc).logFile.flush();
|
||||
}
|
||||
catch (IOException ie) {
|
||||
}
|
||||
return -99;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
public int compareEq (UnifyPair left, UnifyPair right) {
|
||||
if (left == null || right == null)
|
||||
System.out.println("Fehler");
|
||||
if (left.getLhsType() instanceof PlaceholderType) {
|
||||
return fc.compare(left.getRhsType(), right.getRhsType(), left.getPairOp());
|
||||
}
|
||||
else {
|
||||
return fc.compare(left.getLhsType(), right.getLhsType(), left.getPairOp());
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
public Pair<Integer,Set<UnifyPair>> compare (UnifyType left, UnifyType right) {
|
||||
UnifyPair up;
|
||||
if (left instanceof WildcardType || right instanceof WildcardType) {
|
||||
up = new UnifyPair(left, right, PairOperator.SMALLERDOTWC);
|
||||
if (((left instanceof ExtendsType)
|
||||
&& (((ExtendsType)left).getExtendedType().getName().equals("java.util.Vector"))
|
||||
&& (((ReferenceType)((ExtendsType)left).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)) ||
|
||||
((right instanceof ExtendsType)
|
||||
&& (((ExtendsType)right).getExtendedType().getName().equals("java.util.Vector"))
|
||||
&& (((ReferenceType)((ExtendsType)right).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)))
|
||||
{
|
||||
System.out.println("");
|
||||
}
|
||||
if (((right instanceof SuperType) && (((SuperType)right).getSuperedType().getName().equals("java.lang.Object")))
|
||||
||((left instanceof SuperType) && (((SuperType)left).getSuperedType().getName().equals("java.lang.Object"))))
|
||||
{
|
||||
System.out.println("");
|
||||
}
|
||||
}
|
||||
else {
|
||||
up = new UnifyPair(left, right, PairOperator.SMALLERDOT);
|
||||
}
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask();
|
||||
HashSet<UnifyPair> hs = new HashSet<>();
|
||||
hs.add(up);
|
||||
Set<UnifyPair> smallerRes = unifyTask.applyTypeUnificationRules(hs, fc);
|
||||
long smallerLen = smallerRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count();
|
||||
if (smallerLen == 0) return new Pair<>(-1, smallerRes);
|
||||
else {
|
||||
if (left instanceof WildcardType || right instanceof WildcardType) {
|
||||
up = new UnifyPair(right, left, PairOperator.SMALLERDOTWC);
|
||||
if (((left instanceof ExtendsType)
|
||||
&& (((ExtendsType)left).getExtendedType().getName().equals("java.util.Vector"))
|
||||
&& (((ReferenceType)((ExtendsType)left).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)) ||
|
||||
((right instanceof ExtendsType)
|
||||
&& (((ExtendsType)right).getExtendedType().getName().equals("java.util.Vector"))
|
||||
&& (((ReferenceType)((ExtendsType)right).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)))
|
||||
{
|
||||
System.out.println("");
|
||||
}
|
||||
if (right instanceof SuperType)
|
||||
{
|
||||
System.out.println("");
|
||||
}
|
||||
}
|
||||
else {
|
||||
up = new UnifyPair(right, left, PairOperator.SMALLERDOT);
|
||||
}
|
||||
//TypeUnifyTask unifyTask = new TypeUnifyTask();
|
||||
hs = new HashSet<>();
|
||||
hs.add(up);
|
||||
Set<UnifyPair> greaterRes = unifyTask.applyTypeUnificationRules(hs, fc);
|
||||
long greaterLen = greaterRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count();
|
||||
if (greaterLen == 0) return new Pair<>(1, greaterRes);
|
||||
else return new Pair<>(0, new HashSet<>());
|
||||
}
|
||||
}
|
||||
|
||||
/* TODO muss noch verifiziert werden PL 2018-03-21
|
||||
* (non-Javadoc)
|
||||
* fuehrt zu Fehlern bei Arrays.sort (contract nicht erfuellt)
|
||||
* @see com.google.common.collect.Ordering#compare(java.lang.Object, java.lang.Object)
|
||||
*/
|
||||
public int compare (Set<UnifyPair> leftpara, Set<UnifyPair> rightpara) {
|
||||
|
||||
Set<UnifyPair> left = new HashSet<>(leftpara);
|
||||
Set<UnifyPair> right = new HashSet<>(rightpara);
|
||||
|
||||
/*
|
||||
//pairop = PairOperator.SMALLERDOTWC;
|
||||
List<UnifyType> al = new ArrayList<>();
|
||||
PlaceholderType xx = PlaceholderType.freshPlaceholder();
|
||||
al.add(xx);
|
||||
UnifyType t1 = new ExtendsType(new ReferenceType("Vector", new TypeParams(al)));
|
||||
|
||||
//PlaceholderType yy =new PlaceholderType("yy");
|
||||
List<UnifyType> alr = new ArrayList<>();
|
||||
UnifyType exx = new ExtendsType(xx);
|
||||
alr.add(exx);
|
||||
UnifyType t2 = new ExtendsType(new ReferenceType("Vector", new TypeParams(alr)));
|
||||
|
||||
PlaceholderType a = PlaceholderType.freshPlaceholder();
|
||||
a.setInnerType(true);
|
||||
UnifyPair p1 = new UnifyPair(a, t1, PairOperator.SMALLERDOTWC);
|
||||
PlaceholderType b = PlaceholderType.freshPlaceholder();
|
||||
b.setInnerType(true);
|
||||
UnifyPair p2 = new UnifyPair(b, t2, PairOperator.SMALLERDOTWC);
|
||||
|
||||
List<UnifyType> al3 = new ArrayList<>();
|
||||
al3.add(a);
|
||||
|
||||
List<UnifyType> al4 = new ArrayList<>();
|
||||
al4.add(b);
|
||||
|
||||
UnifyPair p3 = new UnifyPair(new PlaceholderType("c"), new ReferenceType("Vector", new TypeParams(al3)), PairOperator.EQUALSDOT);
|
||||
UnifyPair p4 = new UnifyPair(new PlaceholderType("c"), new ReferenceType("Vector", new TypeParams(al4)), PairOperator.EQUALSDOT);
|
||||
|
||||
right = new HashSet<>();
|
||||
right.add(p1);
|
||||
right.add(p3);
|
||||
left = new HashSet<>();
|
||||
left.add(p2);
|
||||
left.add(p4);
|
||||
*/
|
||||
|
||||
|
||||
Set<UnifyPair> lefteq = left.stream()
|
||||
.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> righteq = right.stream()
|
||||
.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> leftle = left.stream()
|
||||
.filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType)
|
||||
&& x.getPairOp() == PairOperator.SMALLERDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> rightle = right.stream()
|
||||
.filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType)
|
||||
&& x.getPairOp() == PairOperator.SMALLERDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> leftlewc = left.stream()
|
||||
.filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType)
|
||||
&& x.getPairOp() == PairOperator.SMALLERDOTWC))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> rightlewc = right.stream()
|
||||
.filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType)
|
||||
&& x.getPairOp() == PairOperator.SMALLERDOTWC))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
//System.out.println(left.toString());
|
||||
//Fall 2
|
||||
//if (lefteq.iterator().next().getLhsType().getName().equals("AJO")) {
|
||||
// System.out.print("");
|
||||
//}
|
||||
|
||||
//ODER-CONSTRAINT
|
||||
Set<UnifyPair> leftBase = left.stream().map(x -> x.getGroundBasePair()).collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> rightBase = right.stream().map(x -> x.getGroundBasePair()).collect(Collectors.toCollection(HashSet::new));
|
||||
|
||||
Set<UnifyPair> lefteqOder = left.stream()
|
||||
.filter(x -> { UnifyPair y = x.getGroundBasePair();
|
||||
/*try {
|
||||
((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("y: " + y.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("y.getLhsType() : " + y.getLhsType() .toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("y.getRhsType(): " + y.getRhsType().toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("x.getPairOp(): " + x.getPairOp().toString() +"\n\n");
|
||||
}
|
||||
catch (IOException ie) {
|
||||
} */
|
||||
return (y.getLhsType() instanceof PlaceholderType &&
|
||||
!(y.getRhsType() instanceof PlaceholderType) &&
|
||||
x.getPairOp() == PairOperator.EQUALSDOT);})
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
left.removeAll(lefteqOder);
|
||||
Set<UnifyPair> righteqOder = right.stream()
|
||||
.filter(x -> { UnifyPair y = x.getGroundBasePair();
|
||||
return (y.getLhsType() instanceof PlaceholderType &&
|
||||
!(y.getRhsType() instanceof PlaceholderType) &&
|
||||
x.getPairOp() == PairOperator.EQUALSDOT);})
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
right.removeAll(righteqOder);
|
||||
Set<UnifyPair> lefteqRet = left.stream()
|
||||
.filter(x -> { UnifyPair y = x.getGroundBasePair();
|
||||
return (y.getRhsType() instanceof PlaceholderType &&
|
||||
((PlaceholderType)y.getRhsType()).getOrCons() == (byte)-1);})
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
left.removeAll(lefteqRet);
|
||||
Set<UnifyPair> righteqRet = right.stream()
|
||||
.filter(x -> { UnifyPair y = x.getGroundBasePair();
|
||||
return (y.getRhsType() instanceof PlaceholderType &&
|
||||
((PlaceholderType)y.getRhsType()).getOrCons() == (byte)-1);})
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
right.removeAll(righteqRet);
|
||||
Set<UnifyPair> leftleOder = left.stream()
|
||||
.filter(x -> (x.getPairOp() == PairOperator.SMALLERDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
Set<UnifyPair> rightleOder = right.stream()
|
||||
.filter(x -> (x.getPairOp() == PairOperator.SMALLERDOT))
|
||||
.collect(Collectors.toCollection(HashSet::new));
|
||||
|
||||
/*
|
||||
synchronized(this) {
|
||||
try {
|
||||
((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("lefteqOder: " + lefteqOder.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("righteqOder: " + righteqOder.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("lefteqRet: " + lefteqRet.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("righteqRet: " + righteqRet.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("leftleOder: " + leftleOder.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("rightleOder: " + rightleOder.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.flush();
|
||||
}
|
||||
catch (IOException ie) {
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
|
||||
Integer compareEq;
|
||||
if (lefteqOder.size() == 1 && righteqOder.size() == 1 && lefteqRet.size() == 1 && righteqRet.size() == 1) {
|
||||
Match m = new Match();
|
||||
if ((compareEq = compareEq(lefteqOder.iterator().next().getGroundBasePair(), righteqOder.iterator().next().getGroundBasePair())) == -1) {
|
||||
ArrayList<UnifyPair> matchList =
|
||||
rightleOder.stream().map(x -> {
|
||||
UnifyPair leftElem = leftleOder.stream()
|
||||
.filter(y -> y.getGroundBasePair().getLhsType().equals(x.getGroundBasePair().getLhsType()))
|
||||
.findAny().get();
|
||||
return new UnifyPair(x.getRhsType(), leftElem.getRhsType(), PairOperator.EQUALSDOT);})
|
||||
.collect(Collectors.toCollection(ArrayList::new));
|
||||
if (m.match(matchList).isPresent()) {
|
||||
//try { ((FiniteClosure)fc).logFile.write("result1: -1 \n\n"); } catch (IOException ie) {}
|
||||
return -1;
|
||||
}
|
||||
else {
|
||||
//try { ((FiniteClosure)fc).logFile.write("result1: 0 \n\n"); } catch (IOException ie) {}
|
||||
return 0;
|
||||
}
|
||||
} else if (compareEq == 1) {
|
||||
ArrayList<UnifyPair> matchList =
|
||||
leftleOder.stream().map(x -> {
|
||||
UnifyPair rightElem = rightleOder.stream()
|
||||
.filter(y ->
|
||||
y.getGroundBasePair().getLhsType().equals(x.getGroundBasePair().getLhsType()))
|
||||
.findAny().get();
|
||||
return new UnifyPair(x.getRhsType(), rightElem.getRhsType(), PairOperator.EQUALSDOT);})
|
||||
.collect(Collectors.toCollection(ArrayList::new));
|
||||
if (m.match(matchList).isPresent()) {
|
||||
//try { ((FiniteClosure)fc).logFile.write("result2: 1 \n\n"); } catch (IOException ie) {}
|
||||
return 1;
|
||||
}
|
||||
else {
|
||||
//try { ((FiniteClosure)fc).logFile.write("result2: 0 \n\n"); } catch (IOException ie) {}
|
||||
return 0;
|
||||
}
|
||||
} else {
|
||||
/*
|
||||
synchronized(this) {
|
||||
try {
|
||||
((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("lefteqOder: " + lefteqOder.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("righteqOder: " + righteqOder.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("lefteqRet: " + lefteqRet.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("righteqRet: " + righteqRet.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("leftleOder: " + leftleOder.toString() +"\n");
|
||||
((FiniteClosure)fc).logFile.write("rightleOder: " + rightleOder.toString() +"\n\n");
|
||||
((FiniteClosure)fc).logFile.write("result3: 0 \n\n");
|
||||
((FiniteClosure)fc).logFile.flush();
|
||||
}
|
||||
catch (IOException ie) {
|
||||
}
|
||||
}
|
||||
*/
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (lefteq.size() == 1 && lefteq.iterator().next().getRhsType() instanceof ExtendsType && leftle.size() == 1 && righteq.size() == 0 && rightle.size() == 1) {
|
||||
return 1;
|
||||
}
|
||||
//Fall 2
|
||||
if (lefteq.size() == 0 && leftle.size() == 1 && righteq.size() == 1 && righteq.iterator().next().getRhsType() instanceof ExtendsType && rightle.size() == 1) {
|
||||
return -1;
|
||||
}
|
||||
//Fall 3
|
||||
if (lefteq.size() == 1 && lefteq.iterator().next().getRhsType() instanceof SuperType && leftle.size() == 1 && righteq.size() == 0 && rightle.size() == 1) {
|
||||
return -1;
|
||||
}
|
||||
//Fall 3
|
||||
if (lefteq.size() == 0 && leftle.size() == 1 && righteq.size() == 1 && righteq.iterator().next().getRhsType() instanceof SuperType && rightle.size() == 1) {
|
||||
return 1;
|
||||
}
|
||||
//Fall 5
|
||||
if (lefteq.size() == 1 && leftle.size() == 0 && righteq.size() == 1 && rightle.size() == 1) {
|
||||
return -1;
|
||||
}
|
||||
//Fall 5
|
||||
if (lefteq.size() == 1 && leftle.size() == 1 && righteq.size() == 1 && rightle.size() == 0) {
|
||||
return 1;
|
||||
}
|
||||
//Fall 5
|
||||
if (lefteq.size() == 1 && leftle.size() == 1 && righteq.size() == 1 && rightle.size() == 1) {
|
||||
return 0;
|
||||
}
|
||||
// Nur Paare a =. Theta
|
||||
if (leftle.size() == 0 && rightle.size() == 0 && leftlewc.size() == 0 && rightlewc.size() ==0) {
|
||||
Stream<UnifyPair> lseq = lefteq.stream(); //left.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT));
|
||||
Stream<UnifyPair> rseq = righteq.stream(); //right.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT));
|
||||
BinaryOperator<HashMap<UnifyType,UnifyPair>> combiner = (x,y) -> { x.putAll(y); return x;};
|
||||
HashMap<UnifyType,UnifyPair> hm = rseq.reduce(new HashMap<UnifyType,UnifyPair>(), (x, y)-> { x.put(y.getLhsType(),y); return x; }, combiner);
|
||||
lseq = lseq.filter(x -> !(hm.get(x.getLhsType()) == null));//NOCHMALS UEBERPRUEFEN!!!!
|
||||
lseq = lseq.filter(x -> !x.equals(hm.get(x.getLhsType()))); //Elemente die gleich sind muessen nicht verglichen werden
|
||||
Optional<Integer> si = lseq.map(x -> compareEq(x, hm.get(x.getLhsType()))).reduce((x,y)-> { if (x == y) return x; else return 0; } );
|
||||
if (!si.isPresent()) return 0;
|
||||
else return si.get();
|
||||
}
|
||||
//Fall 1 und 4
|
||||
if (lefteq.size() >= 1 && righteq.size() >= 1 && (leftlewc.size() > 0 || rightlewc.size() > 0)) {
|
||||
if (lefteq.iterator().next().getLhsType().getName().equals("D"))
|
||||
System.out.print("");
|
||||
//Set<PlaceholderType> varsleft = lefteq.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new));
|
||||
//Set<PlaceholderType> varsright = righteq.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new));
|
||||
//filtern des Paares a = Theta, das durch a <. Thata' generiert wurde (nur im Fall 1 relevant) andere Substitutioen werden rausgefiltert
|
||||
lefteq.removeIf(x -> (x.getBasePair()!=null) && !(x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName())
|
||||
||x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())));//removeIf(x -> !varsright.contains(x.getLhsType()));
|
||||
righteq.removeIf(x -> (x.getBasePair()!=null) && !(x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName())
|
||||
||x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())));//.removeIf(x -> !varsleft.contains(x.getLhsType()));
|
||||
UnifyPair lseq = lefteq.iterator().next();
|
||||
UnifyPair rseq = righteq.iterator().next();
|
||||
if (lseq.getRhsType().getName().equals("Object")) {
|
||||
if (rseq.getRhsType().getName().equals("Object")) return 0;
|
||||
else return 1;
|
||||
}
|
||||
else {
|
||||
if (rseq.getRhsType().getName().equals("Object")) return -1;
|
||||
}
|
||||
if (leftlewc.size() == rightlewc.size()) {
|
||||
//TODO: Hier wird bei Wildcards nicht das richtige compare aufgerufen PL 18-04-20
|
||||
Pair<Integer, Set<UnifyPair>> int_Unifier = compare(lseq.getRhsType(), rseq.getRhsType());
|
||||
Unifier uni = new Unifier();
|
||||
int_Unifier.getValue().get().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType()));
|
||||
if (!lseq.getRhsType().getName().equals(rseq.getRhsType().getName())
|
||||
|| leftlewc.size() == 0 || rightlewc.size() == 0) return int_Unifier.getKey();
|
||||
else {
|
||||
Set <UnifyPair> lsleuni = leftlewc.stream().map(x -> uni.apply(x)).collect(Collectors.toCollection(HashSet::new));
|
||||
Set <UnifyPair> rsleuni = rightlewc.stream().map(x -> uni.apply(x)).collect(Collectors.toCollection(HashSet::new));
|
||||
BinaryOperator<HashMap<UnifyType,UnifyPair>> combiner = (x,y) -> { x.putAll(y); return x;};
|
||||
|
||||
HashMap<UnifyType,UnifyPair> hm;
|
||||
Optional<Integer> si;
|
||||
//1. Fall
|
||||
if (leftlewc.iterator().next().getLhsType() instanceof PlaceholderType) {
|
||||
hm = rsleuni.stream().reduce(new HashMap<UnifyType,UnifyPair>(), (x, y)-> { x.put(y.getLhsType(),y); return x; }, combiner);
|
||||
Stream<UnifyPair> lslewcstr = lsleuni.stream().filter(x -> !(hm.get(x.getLhsType()) == null));
|
||||
si = lslewcstr.map(x -> fc.compare(x.getRhsType(), hm.get(x.getLhsType()).getRhsType(), PairOperator.SMALLERDOTWC)).reduce((x,y)-> { if (x == y) return x; else return 0; } );
|
||||
}
|
||||
//4. Fall
|
||||
else {
|
||||
hm = rsleuni.stream().reduce(new HashMap<UnifyType,UnifyPair>(), (x, y)-> { x.put(y.getRhsType(),y); return x; }, combiner);
|
||||
Stream<UnifyPair> lslewcstr = lsleuni.stream().filter(x -> !(hm.get(x.getRhsType()) == null));
|
||||
si = lslewcstr.map(x -> fc.compare(x.getLhsType(), hm.get(x.getRhsType()).getLhsType(), PairOperator.SMALLERDOTWC)).reduce((x,y)-> { if (x == y) return x; else return 0; } );
|
||||
}
|
||||
if (!si.isPresent()) return 0;
|
||||
else return si.get();
|
||||
}
|
||||
} else {
|
||||
if (leftlewc.size() > 0) {
|
||||
Set<UnifyPair> subst;
|
||||
subst = leftlewc.stream().map(x -> {
|
||||
if (x.getLhsType() instanceof PlaceholderType) {
|
||||
return new UnifyPair(x.getLhsType(), x.getRhsType(), PairOperator.EQUALSDOT);
|
||||
}
|
||||
else {
|
||||
return new UnifyPair(x.getRhsType(), x.getLhsType(), PairOperator.EQUALSDOT);
|
||||
}}).collect(Collectors.toCollection(HashSet::new));
|
||||
Unifier uni = new Unifier();
|
||||
lseq = uni.apply(lseq);
|
||||
}
|
||||
else {
|
||||
Set<UnifyPair> subst;
|
||||
subst = rightlewc.stream().map(x -> {
|
||||
if (x.getLhsType() instanceof PlaceholderType) {
|
||||
return new UnifyPair(x.getLhsType(), x.getRhsType(), PairOperator.EQUALSDOT);
|
||||
}
|
||||
else {
|
||||
return new UnifyPair(x.getRhsType(), x.getLhsType(), PairOperator.EQUALSDOT);
|
||||
}}).collect(Collectors.toCollection(HashSet::new));
|
||||
Unifier uni = new Unifier();
|
||||
subst.stream().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType()));
|
||||
rseq = uni.apply(rseq);
|
||||
}
|
||||
return compareEq(lseq, rseq);
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
@ -0,0 +1,49 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
/**
|
||||
* Operators of pairs of the unification.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public enum PairOperator {
|
||||
/**
|
||||
* The smaller operator (T < P) is used to express a subtyping relation between
|
||||
* T and P for example in the finite closure. It is necessarily true.
|
||||
*/
|
||||
SMALLER,
|
||||
|
||||
/**
|
||||
* The smallerdot operator (T <. P) is used to express a subtyping relation between
|
||||
* of T and P in a CONSTRAINT during the unification. It is not necessarily true.
|
||||
*/
|
||||
SMALLERDOT,
|
||||
|
||||
/**
|
||||
* The smallernedot operator for arguments (T <!=. P) is the same as SMALLERDOT without
|
||||
* T == P. It is used for operations + / - / * / < / > / ... with the Supertype Number
|
||||
*/
|
||||
SMALLERNEQDOT,
|
||||
|
||||
/**
|
||||
* The smallerdot operator for arguments (T <.? P) is used to express that
|
||||
* T is an element of smArg(P) (or P is an element of grArg(T)) in a CONSTRAINT
|
||||
* during the unification. It is not necessarily true.
|
||||
*/
|
||||
SMALLERDOTWC,
|
||||
|
||||
/**
|
||||
* The equalsdot operator (T =. P) is used to express that two types during the unification
|
||||
* should be equal. It is not necessarily true.
|
||||
*/
|
||||
EQUALSDOT;
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
switch (this) {
|
||||
case SMALLER: return "<";
|
||||
case SMALLERDOT: return "<.";
|
||||
case SMALLERNEQDOT: return "<!=.";
|
||||
case SMALLERDOTWC: return "<.?";
|
||||
default: return "=."; // EQUALSDOT
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,208 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.Random;
|
||||
import java.util.Set;
|
||||
import java.util.concurrent.ConcurrentHashMap;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.distributeVariance;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* An unbounded placeholder type.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public final class PlaceholderType extends UnifyType{
|
||||
|
||||
/**
|
||||
* Static list containing the names of all existing placeholders.
|
||||
* Used for generating fresh placeholders.
|
||||
*/
|
||||
public static final Set<String> EXISTING_PLACEHOLDERS = ConcurrentHashMap.newKeySet();
|
||||
|
||||
/**
|
||||
* Prefix of auto-generated placeholder names.
|
||||
*/
|
||||
protected static String nextName = "gen_";
|
||||
|
||||
/**
|
||||
* Random number generator used to generate fresh placeholder name.
|
||||
*/
|
||||
protected static Random rnd = new Random(43558747548978L);
|
||||
|
||||
/**
|
||||
* True if this object was auto-generated, false if this object was user-generated.
|
||||
*/
|
||||
private final boolean IsGenerated;
|
||||
|
||||
|
||||
/**
|
||||
* isWildcardable gibt an, ob ein Wildcardtyp dem PlaceholderType zugeordnet werden darf
|
||||
*/
|
||||
private boolean wildcardable = true;
|
||||
|
||||
/**
|
||||
* is innerType gibt an, ob der Type des PlaceholderType innerhalb eines Typkonstruktorsverwendet wird
|
||||
*/
|
||||
private boolean innerType = false;
|
||||
|
||||
/**
|
||||
* variance shows the variance of the pair
|
||||
* -1: contravariant
|
||||
* 1 covariant
|
||||
* 0 invariant
|
||||
* PL 2018-03-21
|
||||
*/
|
||||
private int variance = 0;
|
||||
|
||||
/*
|
||||
* Fuer Oder-Constraints:
|
||||
* orCons = 1: Receiver
|
||||
* orCons = 0: Argument oder kein Oder-Constraint
|
||||
* orCons = -1: RetType
|
||||
*/
|
||||
private byte orCons = 0;
|
||||
|
||||
/**
|
||||
* Creates a new placeholder type with the specified name.
|
||||
*/
|
||||
public PlaceholderType(String name) {
|
||||
super(name, new TypeParams());
|
||||
EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names
|
||||
IsGenerated = false; // This type is user generated
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a new placeholdertype
|
||||
* @param isGenerated true if this placeholder is auto-generated, false if it is user-generated.
|
||||
*/
|
||||
protected PlaceholderType(String name, boolean isGenerated) {
|
||||
super(name, new TypeParams());
|
||||
EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names
|
||||
IsGenerated = isGenerated;
|
||||
}
|
||||
|
||||
public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht) {
|
||||
return visitor.visit(this, ht);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a fresh placeholder type with a name that does so far not exist.
|
||||
* A user could later instantiate a type using the same name that is equivalent to this type.
|
||||
* @return A fresh placeholder type.
|
||||
*/
|
||||
public static PlaceholderType freshPlaceholder() {
|
||||
String name = nextName + (char) (rnd.nextInt(22) + 97); // Returns random char between 'a' and 'z'
|
||||
// Add random chars while the name is in use.
|
||||
while(EXISTING_PLACEHOLDERS.contains(name)) {
|
||||
name += (char) (rnd.nextInt(22) + 97); // Returns random char between 'a' and 'z'
|
||||
}
|
||||
return new PlaceholderType(name, true);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* True if this placeholder is auto-generated, false if it is user-generated.
|
||||
*/
|
||||
public boolean isGenerated() {
|
||||
return IsGenerated;
|
||||
}
|
||||
|
||||
public void setVariance(int v) {
|
||||
variance = v;
|
||||
}
|
||||
|
||||
public int getVariance() {
|
||||
return variance;
|
||||
}
|
||||
|
||||
public void reversVariance() {
|
||||
if (variance == 1) {
|
||||
setVariance(-1);
|
||||
} else {
|
||||
if (variance == -1) {
|
||||
setVariance(1);
|
||||
}}
|
||||
}
|
||||
|
||||
public void setOrCons(byte i) {
|
||||
orCons = i;
|
||||
}
|
||||
|
||||
public byte getOrCons() {
|
||||
return orCons;
|
||||
}
|
||||
|
||||
public Boolean isWildcardable() {
|
||||
return wildcardable;
|
||||
}
|
||||
public void disableWildcardtable() {
|
||||
wildcardable = false;
|
||||
}
|
||||
|
||||
public void enableWildcardtable() {
|
||||
wildcardable = true;
|
||||
}
|
||||
|
||||
public void setWildcardtable(Boolean wildcardable) {
|
||||
this.wildcardable = wildcardable;
|
||||
}
|
||||
|
||||
public Boolean isInnerType() {
|
||||
return innerType;
|
||||
}
|
||||
|
||||
public void setInnerType(Boolean innerType) {
|
||||
this.innerType = innerType;
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
public UnifyType setTypeParams(TypeParams newTp) {
|
||||
return this; // Placeholders never have params.
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return typeName.hashCode();
|
||||
}
|
||||
|
||||
@Override
|
||||
UnifyType apply(Unifier unif) {
|
||||
if(unif.hasSubstitute(this)) {
|
||||
UnifyType ret = unif.getSubstitute(this);
|
||||
//PL 2018-05-17 Auskommentierung muesste korrekt sein,
|
||||
//bereits in JavaTXComplier Variancen gesetzt werden.
|
||||
//ret.accept(new distributeVariance(), this.getVariance());
|
||||
return ret;
|
||||
}
|
||||
return this;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof PlaceholderType))
|
||||
return false;
|
||||
|
||||
return ((PlaceholderType) obj).getName().equals(typeName);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public Collection<PlaceholderType> getInvolvedPlaceholderTypes() {
|
||||
ArrayList<PlaceholderType> ret = new ArrayList<>();
|
||||
ret.add(this);
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,100 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* A reference type e.q. Integer or List<T>.
|
||||
* @author Florian Steurer
|
||||
*
|
||||
*/
|
||||
public class ReferenceType extends UnifyType {
|
||||
|
||||
/**
|
||||
* The buffered hashCode
|
||||
*/
|
||||
private final int hashCode;
|
||||
|
||||
/**
|
||||
* gibt an, ob der ReferenceType eine generische Typvariable ist
|
||||
*/
|
||||
private final boolean genericTypeVar;
|
||||
|
||||
|
||||
public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht) {
|
||||
return visitor.visit(this, ht);
|
||||
}
|
||||
|
||||
public ReferenceType(String name, Boolean genericTypeVar) {
|
||||
super(name, new TypeParams());
|
||||
hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode();
|
||||
this.genericTypeVar = genericTypeVar;
|
||||
}
|
||||
|
||||
public ReferenceType(String name, UnifyType... params) {
|
||||
super(name, new TypeParams(params));
|
||||
hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode();
|
||||
genericTypeVar = false;
|
||||
}
|
||||
|
||||
public ReferenceType(String name, TypeParams params) {
|
||||
super(name, params);
|
||||
hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode();
|
||||
genericTypeVar = false;
|
||||
}
|
||||
|
||||
public boolean isGenTypeVar () {
|
||||
return genericTypeVar;
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
UnifyType apply(Unifier unif) {
|
||||
TypeParams newParams = typeParams.apply(unif);
|
||||
|
||||
if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams))
|
||||
return this;
|
||||
|
||||
return new ReferenceType(typeName, newParams);
|
||||
}
|
||||
|
||||
@Override
|
||||
public UnifyType setTypeParams(TypeParams newTp) {
|
||||
if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams))
|
||||
return this; // reduced the amount of objects created
|
||||
return new ReferenceType(typeName, newTp);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return hashCode;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof ReferenceType))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
ReferenceType other = (ReferenceType) obj;
|
||||
|
||||
if(!other.getName().equals(typeName))
|
||||
return false;
|
||||
|
||||
return other.getTypeParams().equals(typeParams);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,88 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* A super wildcard type e.g. ? super Integer.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public final class SuperType extends WildcardType {
|
||||
|
||||
public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht) {
|
||||
return visitor.visit(this, ht);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a new instance "? extends superedType"
|
||||
* @param superedType The type that is supered e.g. Integer in "? super Integer"
|
||||
*/
|
||||
public SuperType(UnifyType superedType) {
|
||||
super("? super " + superedType.getName(), superedType);
|
||||
}
|
||||
|
||||
/**
|
||||
* The type that is supered e.g. Integer in "? super Integer"
|
||||
*/
|
||||
public UnifyType getSuperedType() {
|
||||
return wildcardedType;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "? super " + wildcardedType;
|
||||
}
|
||||
|
||||
/**
|
||||
* Sets the type parameters of the wildcarded type and returns a new supertype that supers that type.
|
||||
*/
|
||||
@Override
|
||||
public UnifyType setTypeParams(TypeParams newTp) {
|
||||
UnifyType newType = wildcardedType.setTypeParams(newTp);
|
||||
if(newType == wildcardedType)
|
||||
return this; // Reduced the amount of objects created
|
||||
return new SuperType(wildcardedType.setTypeParams(newTp));
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.smArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded) {
|
||||
return fc.grArg(this, fBounded);
|
||||
}
|
||||
|
||||
@Override
|
||||
UnifyType apply(Unifier unif) {
|
||||
UnifyType newType = wildcardedType.apply(unif);
|
||||
if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType))
|
||||
return this; // Reduced the amount of objects created
|
||||
return new SuperType(newType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
/*
|
||||
* It is important that the prime that is added is different to the prime added in hashCode() of ExtendsType.
|
||||
* Otherwise ? extends T and ? super T have the same hashCode() for every Type T.
|
||||
*/
|
||||
return wildcardedType.hashCode() + 3917;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof SuperType))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
SuperType other = (SuperType) obj;
|
||||
return other.getSuperedType().equals(wildcardedType);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,191 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.*;
|
||||
|
||||
|
||||
/**
|
||||
* The generic or non-generic parameters of a type e.g. <T> for List<T>
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public final class TypeParams implements Iterable<UnifyType>{
|
||||
/**
|
||||
* The array which backs the type parameters.
|
||||
*/
|
||||
private final UnifyType[] typeParams;
|
||||
|
||||
/**
|
||||
* Hashcode calculation is expensive and must be cached.
|
||||
*/
|
||||
private final int hashCode;
|
||||
|
||||
/**
|
||||
* Creates a new set of type parameters.
|
||||
* @param types The type parameters.
|
||||
*/
|
||||
public TypeParams(List<UnifyType> types){
|
||||
typeParams = new UnifyType[types.size()];
|
||||
for(int i=0;i<types.size();i++){
|
||||
typeParams[i] = types.get(i);
|
||||
if(types.get(i)==null)throw new NullPointerException();
|
||||
}
|
||||
|
||||
// Hashcode calculation is expensive and must be cached.
|
||||
hashCode = Arrays.deepHashCode(typeParams);
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a new set of type parameters.
|
||||
* @param types The type parameters.
|
||||
*/
|
||||
public TypeParams(UnifyType... types) {
|
||||
typeParams = types;
|
||||
|
||||
// Hashcode calculation is expensive and must be cached.
|
||||
hashCode = Arrays.deepHashCode(typeParams);
|
||||
}
|
||||
|
||||
/**
|
||||
* True if every parameter in this object is a placeholder type, false otherwise.
|
||||
*/
|
||||
public boolean arePlaceholders() {
|
||||
return Arrays.stream(typeParams).allMatch(x -> x instanceof PlaceholderType);
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the number of the type parameters in this object.
|
||||
* @return number of type parameters, always positive (including 0).
|
||||
*/
|
||||
public int size() {
|
||||
return typeParams.length;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns true if this object has size() of zero, false otherwise.
|
||||
*/
|
||||
public boolean empty() {
|
||||
return typeParams.length == 0;
|
||||
}
|
||||
|
||||
/**
|
||||
* Applies a unifier to every parameter in this object.
|
||||
* @param unif The applied unifier.
|
||||
* @return A new type parameter object, where the unifier was applied to every parameter.
|
||||
*/
|
||||
public TypeParams apply(Unifier unif) {
|
||||
UnifyType[] newParams = new UnifyType[typeParams.length];
|
||||
|
||||
// If true, a type was modified and a new typeparams object has to be created.
|
||||
// Otherwise it is enough to return this object, since it is immutable
|
||||
// This reduced the needed TypeParams-Instances for the lambda14-Test from
|
||||
// 130.000 to 30.000 without a decrease in speed.
|
||||
boolean isNew = false;
|
||||
|
||||
for(int i = 0; i < typeParams.length; i++) {
|
||||
UnifyType newType = typeParams[i].apply(unif);
|
||||
newParams[i] = newType;
|
||||
if(!isNew && (newType.hashCode() != typeParams[i].hashCode() || !newType.equals(typeParams[i])))
|
||||
isNew = true;
|
||||
}
|
||||
|
||||
if(!isNew)
|
||||
return this;
|
||||
return new TypeParams(newParams);
|
||||
}
|
||||
|
||||
/**
|
||||
* True if the PlaceholderType t is a parameter of this object, or if any parameter
|
||||
* contains t (arbitrary depth of recursion), false otherwise.
|
||||
*/
|
||||
public boolean occurs(PlaceholderType t) {
|
||||
for(UnifyType p : typeParams)
|
||||
if(p instanceof PlaceholderType) {//PL 2018-01-31 dangeling else Problem { ... } eingefuegt.
|
||||
if(p.equals(t))
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
if(p.getTypeParams().occurs(t))
|
||||
return true; }
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the i-th parameter of this object.
|
||||
*/
|
||||
public UnifyType get(int i) {
|
||||
return typeParams[i];
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the parameters of this object.
|
||||
* PL 2018-03-17
|
||||
*/
|
||||
public UnifyType[] get() {
|
||||
return typeParams;
|
||||
}
|
||||
|
||||
/**
|
||||
* Sets the the type t as the i-th parameter and returns a new object
|
||||
* that equals this object, except for the i-th type.
|
||||
*/
|
||||
public TypeParams set(UnifyType t, int idx) {
|
||||
// Reduce the creation of new objects for less memory
|
||||
// Reduced the needed instances of TypeParams in the lambda14-Test from
|
||||
// 150.000 to 130.000
|
||||
if(t.hashCode() == typeParams[idx].hashCode() && t.equals(typeParams[idx]))
|
||||
return this;
|
||||
UnifyType[] newparams = Arrays.copyOf(typeParams, typeParams.length);
|
||||
newparams[idx] = t;
|
||||
return new TypeParams(newparams);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Iterator<UnifyType> iterator() {
|
||||
return Arrays.stream(typeParams).iterator();
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return hashCode;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof TypeParams))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
TypeParams other = (TypeParams) obj;
|
||||
|
||||
if(other.size() != this.size())
|
||||
return false;
|
||||
|
||||
for(int i = 0; i < this.size(); i++){
|
||||
//if(this.get(i) == null)
|
||||
//System.out.print("s");
|
||||
}
|
||||
for(int i = 0; i < this.size(); i++)
|
||||
if(!(this.get(i).equals(other.get(i))))
|
||||
return false;
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
String res = "";
|
||||
for(UnifyType t : typeParams)
|
||||
res += t + ",";
|
||||
return "<" + res.substring(0, res.length()-1) + ">";
|
||||
}
|
||||
|
||||
public Collection<? extends PlaceholderType> getInvolvedPlaceholderTypes() {
|
||||
ArrayList<PlaceholderType> ret = new ArrayList<>();
|
||||
for(UnifyType t : typeParams){
|
||||
ret.addAll(t.getInvolvedPlaceholderTypes());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
|
||||
@ -0,0 +1,189 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.Map.Entry;
|
||||
import java.util.Set;
|
||||
import java.util.function.Function;
|
||||
|
||||
/**
|
||||
* A set of substitutions (s -> t) that is an applicable function to types and pairs.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<PlaceholderType, UnifyType>> {
|
||||
|
||||
/**
|
||||
* The set of substitutions that unify a type-term
|
||||
*/
|
||||
private HashMap<PlaceholderType, UnifyType> substitutions = new HashMap<>();
|
||||
|
||||
/**
|
||||
* Creates a new instance with a single substitution (source -> target).
|
||||
* @param The type that is replaced
|
||||
* @param The type that replaces
|
||||
*/
|
||||
public Unifier(PlaceholderType source, UnifyType target) {
|
||||
substitutions.put(source, target);
|
||||
}
|
||||
|
||||
/**
|
||||
* Identity function as an "unifier".
|
||||
*/
|
||||
protected Unifier() {
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates an unifier that is the identity function (thus has no substitutions).
|
||||
*/
|
||||
public static Unifier identity() {
|
||||
return new Unifier();
|
||||
}
|
||||
|
||||
/**
|
||||
* Adds a substitution to the unifier from (source -> target)
|
||||
* @param The type that is replaced
|
||||
* @param The type that replaces
|
||||
*/
|
||||
public void add(PlaceholderType source, UnifyType target) {
|
||||
Unifier tempU = new Unifier(source, target);
|
||||
// Every new substitution must be applied to previously added substitutions
|
||||
// otherwise the unifier needs to be applied multiple times to unify two terms
|
||||
for(PlaceholderType pt : substitutions.keySet())
|
||||
substitutions.put(pt, substitutions.get(pt).apply(tempU));
|
||||
substitutions.put(source, target);
|
||||
}
|
||||
|
||||
@Override
|
||||
public UnifyType apply(UnifyType t) {
|
||||
return t.apply(this);
|
||||
}
|
||||
|
||||
/**
|
||||
* Applies the unifier to the two terms of the pair.
|
||||
* @return A new pair where the left and right-hand side are applied
|
||||
*/
|
||||
public UnifyPair apply(UnifyPair p) {
|
||||
UnifyType newLhs = this.apply(p.getLhsType());
|
||||
UnifyType newRhs = this.apply(p.getRhsType());
|
||||
return new UnifyPair(newLhs, newRhs, p.getPairOp());
|
||||
}
|
||||
|
||||
/**
|
||||
* Applies the unifier to the two terms of the pair.
|
||||
* works only for single subsitution
|
||||
* @return A new pair where the left and right-hand side are applied
|
||||
*/
|
||||
public UnifyPair apply(UnifyPair thisAsPair, UnifyPair p) {
|
||||
UnifyType newLhs = this.apply(p.getLhsType());
|
||||
UnifyType newRhs = this.apply(p.getRhsType());
|
||||
//Varianceweitergabe wird nicht benoetigt.
|
||||
//PlaceholderType lhsph = (PlaceholderType)thisAsPair.getLhsType();
|
||||
//if (lhsph.getVariance() != 0) {
|
||||
// if (p.getLhsType().equals(lhsph)) {
|
||||
// if (p.getRhsType() instanceof PlaceholderType) {
|
||||
// ((PlaceholderType)p.getRhsType()).setVariance(lhsph.getVariance());
|
||||
// }
|
||||
// }
|
||||
// if (p.getRhsType().equals(lhsph)) {
|
||||
// if (p.getLhsType() instanceof PlaceholderType) {
|
||||
// ((PlaceholderType)p.getLhsType()).setVariance(lhsph.getVariance());
|
||||
// }
|
||||
// }
|
||||
//}
|
||||
if (!(p.getLhsType().equals(newLhs)) || !(p.getRhsType().equals(newRhs))) {//Die Anwendung von this hat was veraendert PL 2018-04-01
|
||||
Set<UnifyPair> suniUnifyPair = new HashSet<>();
|
||||
suniUnifyPair.addAll(thisAsPair.getAllSubstitutions());
|
||||
suniUnifyPair.add(thisAsPair);
|
||||
if (p.getLhsType() instanceof PlaceholderType //&& newLhs instanceof PlaceholderType entfernt PL 2018-04-13
|
||||
&& p.getPairOp() == PairOperator.EQUALSDOT) {
|
||||
suniUnifyPair.add(p); //p koennte auch subsitution sein
|
||||
}
|
||||
return new UnifyPair(newLhs, newRhs, p.getPairOp(), suniUnifyPair, p);
|
||||
}
|
||||
return new UnifyPair(newLhs, newRhs, p.getPairOp(), p.getSubstitution(), p.getBasePair(), p.getfBounded());
|
||||
}
|
||||
|
||||
/**
|
||||
* Applies the unifier to the left terms of the pair.
|
||||
* @return A new pair where the left and right-hand side are applied
|
||||
*/
|
||||
public UnifyPair applyleft(UnifyPair p) {
|
||||
return new UnifyPair(this.apply(p.getLhsType()), p.getRhsType(), p.getPairOp());
|
||||
}
|
||||
|
||||
/**
|
||||
* True if the typevariable t will be substituted if the unifier is applied.
|
||||
* false otherwise.
|
||||
*/
|
||||
public boolean hasSubstitute(PlaceholderType t) {
|
||||
return substitutions.containsKey(t);
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the type that will replace the typevariable t if the unifier is applied.
|
||||
*/
|
||||
public UnifyType getSubstitute(PlaceholderType t) {
|
||||
return substitutions.get(t);
|
||||
}
|
||||
|
||||
/**
|
||||
* The number of substitutions in the unifier. If zero, this is the identity function.
|
||||
*/
|
||||
public int size() {
|
||||
return substitutions.size();
|
||||
}
|
||||
|
||||
/**
|
||||
* Garantuees that if there is a substitutions (a -> b) in this unifier,
|
||||
* a is not an element of the targetParams. Substitutions that do not
|
||||
* satisfy this condition, are swapped.
|
||||
*/
|
||||
public void swapPlaceholderSubstitutions(Iterable<UnifyType> targetParams) {
|
||||
for(UnifyType tph : targetParams) {
|
||||
if(!(tph instanceof PlaceholderType))
|
||||
continue;
|
||||
// Swap a substitutions (a -> b) if a is an element of the target params.
|
||||
if(substitutions.containsKey(tph)) {
|
||||
if((substitutions.get(tph) instanceof PlaceholderType)) {
|
||||
PlaceholderType newLhs = (PlaceholderType) substitutions.get(tph);
|
||||
substitutions.remove(tph);
|
||||
substitutions.put(newLhs, tph);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public void swapPlaceholderSubstitutionsReverse(Iterable<UnifyType> sourceParams) {
|
||||
for(UnifyType tph : sourceParams) {
|
||||
if(!(tph instanceof PlaceholderType))
|
||||
continue;
|
||||
if(substitutions.containsValue(tph)) {
|
||||
UnifyType key = substitutions.values().stream().filter(x -> x.equals(tph)).findAny().get();
|
||||
if(key instanceof PlaceholderType) {
|
||||
PlaceholderType newLhs = (PlaceholderType) tph;
|
||||
substitutions.remove(key);
|
||||
substitutions.put(newLhs, key);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
String result = "{ ";
|
||||
for(Entry<PlaceholderType, UnifyType> entry : substitutions.entrySet())
|
||||
result += "(" + entry.getKey() + " -> " + entry.getValue() + "), ";
|
||||
if(!substitutions.isEmpty())
|
||||
result = result.substring(0, result.length()-2);
|
||||
result += " }";
|
||||
return result;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Iterator<Entry<PlaceholderType, UnifyType>> iterator() {
|
||||
return substitutions.entrySet().iterator();
|
||||
}
|
||||
}
|
||||
|
||||
@ -0,0 +1,247 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.HashSet;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
|
||||
|
||||
/**
|
||||
* A pair which contains two types and an operator, e.q. (Integer <. a).
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public class UnifyPair {
|
||||
|
||||
/**
|
||||
* The type on the left hand side of the pair.
|
||||
*/
|
||||
private final UnifyType lhs;
|
||||
|
||||
/**
|
||||
* The type on the right hand side of the pair.
|
||||
*/
|
||||
private final UnifyType rhs;
|
||||
|
||||
/**
|
||||
* The operator that determines the relation between the left and right hand side type.
|
||||
*/
|
||||
private PairOperator pairOp;
|
||||
|
||||
private boolean undefinedPair = false;
|
||||
|
||||
/**
|
||||
* Unifier/substitute that generated this pair
|
||||
* PL 2018-03-15
|
||||
*/
|
||||
private Set<UnifyPair> substitution;
|
||||
|
||||
/**
|
||||
* Base on which the the unifier is applied
|
||||
* PL 2018-03-15
|
||||
*/
|
||||
private UnifyPair basePair;
|
||||
|
||||
/**
|
||||
* For pairs a <. Theta generated in the rule reduceTphSup
|
||||
* to store the f-Bouned Elements to avoid endless recursion
|
||||
* PL 2018-03-15
|
||||
*/
|
||||
private Set<UnifyType> fBounded = new HashSet<>();
|
||||
|
||||
private final int hashCode;
|
||||
|
||||
/**
|
||||
* Creates a new instance of the pair.
|
||||
* @param lhs The type on the left hand side of the pair.
|
||||
* @param rhs The type on the right hand side of the pair.
|
||||
* @param op The operator that determines the relation between the left and right hand side type.
|
||||
*/
|
||||
public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op) {
|
||||
this.lhs = lhs;
|
||||
this.rhs = rhs;
|
||||
pairOp = op;
|
||||
substitution = new HashSet<>();
|
||||
|
||||
// Caching hashcode
|
||||
hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode();
|
||||
}
|
||||
|
||||
public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Set<UnifyPair> uni, UnifyPair base) {
|
||||
this.lhs = lhs;
|
||||
this.rhs = rhs;
|
||||
pairOp = op;
|
||||
substitution = uni;
|
||||
basePair = base;
|
||||
|
||||
|
||||
// Caching hashcode
|
||||
hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode();
|
||||
}
|
||||
|
||||
public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Set<UnifyPair> uni, UnifyPair base, Set<UnifyType> fBounded) {
|
||||
this(lhs, rhs, op, uni, base);
|
||||
|
||||
this.fBounded = fBounded;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the type on the left hand side of the pair.
|
||||
*/
|
||||
public UnifyType getLhsType() {
|
||||
return lhs;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the type on the right hand side of the pair.
|
||||
*/
|
||||
public UnifyType getRhsType() {
|
||||
return rhs;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the operator that determines the relation between the left and right hand side type.
|
||||
*/
|
||||
public PairOperator getPairOp() {
|
||||
return pairOp;
|
||||
}
|
||||
|
||||
public void setPairOp(PairOperator po) {
|
||||
pairOp = po;
|
||||
}
|
||||
|
||||
public void addSubstitutions(Set<UnifyPair> sup) {
|
||||
substitution.addAll(sup);
|
||||
}
|
||||
|
||||
public void setUndefinedPair() {
|
||||
undefinedPair = true;
|
||||
}
|
||||
public Set<UnifyPair> getSubstitution() {
|
||||
return new HashSet<>(substitution);
|
||||
}
|
||||
|
||||
public UnifyPair getBasePair() {
|
||||
return basePair;
|
||||
}
|
||||
public boolean isUndefinedPair() {
|
||||
return undefinedPair;
|
||||
}
|
||||
|
||||
public Set<UnifyPair> getAllSubstitutions () {
|
||||
Set<UnifyPair> ret = new HashSet<>();
|
||||
ret.addAll(new ArrayList<>(getSubstitution()));
|
||||
if (basePair != null) {
|
||||
ret.addAll(new ArrayList<>(basePair.getAllSubstitutions()));
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
public Set<UnifyPair> getThisAndAllBases () {
|
||||
Set<UnifyPair> ret = getAllBases();
|
||||
ret.add(this);
|
||||
return ret;
|
||||
}
|
||||
public Set<UnifyPair> getAllBases () {
|
||||
Set<UnifyPair> ret = new HashSet<>();
|
||||
if (basePair != null) {
|
||||
ret.add(getBasePair());
|
||||
ret.addAll(basePair.getAllBases());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
public UnifyPair getGroundBasePair () {
|
||||
if (basePair == null) {
|
||||
return this;
|
||||
}
|
||||
if (basePair.getBasePair() == null) {
|
||||
return basePair;
|
||||
}
|
||||
else {
|
||||
return basePair.getGroundBasePair();
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* wenn in einem Paar bestehend aus 2 Typvariablen eine nicht wildcardtable ist,
|
||||
* so beide auf nicht wildcardtable setzen
|
||||
*/
|
||||
public void disableCondWildcards() {
|
||||
if (lhs instanceof PlaceholderType && rhs instanceof PlaceholderType
|
||||
&& (!((PlaceholderType)lhs).isWildcardable() || !((PlaceholderType)rhs).isWildcardable()))
|
||||
{
|
||||
((PlaceholderType)lhs).disableWildcardtable();
|
||||
((PlaceholderType)rhs).disableWildcardtable();
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
public Boolean wrongWildcard() {
|
||||
return lhs.wrongWildcard() || rhs.wrongWildcard();
|
||||
}
|
||||
|
||||
public Set<UnifyType> getfBounded() {
|
||||
return this.fBounded;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof UnifyPair))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
UnifyPair other = (UnifyPair) obj;
|
||||
|
||||
if (isUndefinedPair()) {
|
||||
if (other.getBasePair() != basePair || (other.getBasePair() == null && basePair == null)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if (!other.getBasePair().equals(basePair) ||
|
||||
!other.getAllSubstitutions().equals(getAllSubstitutions())) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
return other.getPairOp() == pairOp
|
||||
&& other.getLhsType().equals(lhs)
|
||||
&& other.getRhsType().equals(rhs);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return hashCode;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
String ret = "";
|
||||
if (lhs instanceof PlaceholderType) {
|
||||
ret = new Integer(((PlaceholderType)lhs).getVariance()).toString() + " "
|
||||
+ "WC: " + ((PlaceholderType)lhs).isWildcardable()
|
||||
+ ", IT: " + ((PlaceholderType)lhs).isInnerType();
|
||||
}
|
||||
if (rhs instanceof PlaceholderType) {
|
||||
ret = ret + ", " + new Integer(((PlaceholderType)rhs).getVariance()).toString() + " "
|
||||
+ "WC: " + ((PlaceholderType)rhs).isWildcardable()
|
||||
+ ", IT: " + ((PlaceholderType)rhs).isInnerType();
|
||||
}
|
||||
return "(" + lhs + " " + pairOp + " " + rhs + ", " + ret + ")"; //+ ", [" + getfBounded().toString()+ "])";
|
||||
}
|
||||
|
||||
/*
|
||||
public List<? extends PlaceholderType> getInvolvedPlaceholderTypes() {
|
||||
ArrayList<PlaceholderType> ret = new ArrayList<>();
|
||||
ret.addAll(lhs.getInvolvedPlaceholderTypes());
|
||||
ret.addAll(rhs.getInvolvedPlaceholderTypes());
|
||||
return ret;
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
@ -0,0 +1,119 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.HashMap;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
|
||||
/**
|
||||
* Represents a java type.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public abstract class UnifyType {
|
||||
|
||||
/**
|
||||
* The name of the type e.q. "Integer", "? extends Integer" or "List" for (List<T>)
|
||||
*/
|
||||
protected final String typeName;
|
||||
|
||||
/**
|
||||
* The type parameters of the type.
|
||||
*/
|
||||
protected final TypeParams typeParams;
|
||||
|
||||
/**
|
||||
* Creates a new instance
|
||||
* @param name Name of the type (e.q. List for List<T>, Integer or ? extends Integer)
|
||||
* @param typeParams Parameters of the type (e.q. <T> for List<T>)
|
||||
*/
|
||||
protected UnifyType(String name, TypeParams p) {
|
||||
typeName = name;
|
||||
typeParams = p;
|
||||
}
|
||||
|
||||
|
||||
abstract public <T> UnifyType accept(UnifyTypeVisitor<T> visitor, T ht);
|
||||
|
||||
/**
|
||||
* Returns the name of the type.
|
||||
* @return The name e.q. List for List<T>, Integer or ? extends Integer
|
||||
*/
|
||||
public String getName() {
|
||||
return typeName;
|
||||
}
|
||||
|
||||
/**
|
||||
* The parameters of the type.
|
||||
* @return Parameters of the type, e.q. <T> for List<T>.
|
||||
*/
|
||||
public TypeParams getTypeParams() {
|
||||
return typeParams;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns a new type that equals this type except for the type parameters.
|
||||
* @param newTp The type params of the new type.
|
||||
* @return A new type object.
|
||||
*/
|
||||
public abstract UnifyType setTypeParams(TypeParams newTp);
|
||||
|
||||
/**
|
||||
* Implementation of the visitor-pattern. Returns the set of smArg
|
||||
* by calling the most specific overload in the FC.
|
||||
* @param fc The FC that is called.
|
||||
* @return The set that is smArg(this)
|
||||
*/
|
||||
abstract Set<UnifyType> smArg(IFiniteClosure fc, Set<UnifyType> fBounded);
|
||||
|
||||
/**
|
||||
* Implementation of the visitor-pattern. Returns the set of grArg
|
||||
* by calling the most specific overload in the FC.
|
||||
* @param fc The FC that is called.
|
||||
* @return The set that is grArg(this)
|
||||
*/
|
||||
abstract Set<UnifyType> grArg(IFiniteClosure fc, Set<UnifyType> fBounded);
|
||||
|
||||
/**
|
||||
* Applies a unifier to this object.
|
||||
* @param unif The unifier
|
||||
* @return A UnifyType, that may or may not be a new object, that has its subtypes substituted.
|
||||
*/
|
||||
abstract UnifyType apply(Unifier unif);
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
String params = "";
|
||||
if(typeParams.size() != 0) {
|
||||
for(UnifyType param : typeParams)
|
||||
params += param.toString() + ",";
|
||||
params = "<" + params.substring(0, params.length()-1) + ">";
|
||||
}
|
||||
|
||||
return typeName + params;
|
||||
}
|
||||
|
||||
public Collection<PlaceholderType> getInvolvedPlaceholderTypes() {
|
||||
ArrayList<PlaceholderType> ret = new ArrayList<>();
|
||||
ret.addAll(typeParams.getInvolvedPlaceholderTypes());
|
||||
return ret;
|
||||
}
|
||||
|
||||
public Boolean wrongWildcard() {//default
|
||||
return false;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return this.toString().hashCode();
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(obj == null)return false;
|
||||
return this.toString().equals(obj.toString());
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,72 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
|
||||
/**
|
||||
* A wildcard type that is either a ExtendsType or a SuperType.
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public abstract class WildcardType extends UnifyType {
|
||||
|
||||
/**
|
||||
* The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself.
|
||||
*/
|
||||
protected UnifyType wildcardedType;
|
||||
|
||||
/**
|
||||
* Creates a new instance.
|
||||
* @param name The name of the type, e.q. ? extends Integer
|
||||
* @param wildcardedType The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself.
|
||||
*/
|
||||
protected WildcardType(String name, UnifyType wildcardedType) {
|
||||
super(name, wildcardedType.getTypeParams());
|
||||
this.wildcardedType = wildcardedType;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the wildcarded type, e.q. Integer for ? extends Integer.
|
||||
* @return The wildcarded type. Never a wildcard type itself.
|
||||
*/
|
||||
public UnifyType getWildcardedType() {
|
||||
return wildcardedType;
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the type parameters of the WILDCARDED TYPE.
|
||||
*/
|
||||
@Override
|
||||
public TypeParams getTypeParams() {
|
||||
return wildcardedType.getTypeParams();
|
||||
}
|
||||
|
||||
@Override
|
||||
public Boolean wrongWildcard () {//This is an error
|
||||
return (wildcardedType instanceof WildcardType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return wildcardedType.hashCode() + getName().hashCode() + 17;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof WildcardType))
|
||||
return false;
|
||||
|
||||
if(obj.hashCode() != this.hashCode())
|
||||
return false;
|
||||
|
||||
WildcardType other = (WildcardType) obj;
|
||||
return other.getWildcardedType().equals(wildcardedType);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public Collection<PlaceholderType> getInvolvedPlaceholderTypes() {
|
||||
ArrayList<PlaceholderType> ret = new ArrayList<>();
|
||||
ret.addAll(wildcardedType.getInvolvedPlaceholderTypes());
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,25 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
public class hashKeyType {
|
||||
UnifyType realType;
|
||||
|
||||
hashKeyType(UnifyType realType) {
|
||||
this.realType= realType;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if (obj instanceof hashKeyType) {
|
||||
return realType.equals(((hashKeyType)obj).realType);
|
||||
}
|
||||
else
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return realType.hashCode();
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,47 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.HashSet;
|
||||
import java.util.HashMap;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
|
||||
public class visitUnifyTypeVisitor<T> implements UnifyTypeVisitor<T> {
|
||||
|
||||
public ReferenceType visit(ReferenceType refty, T ht) {
|
||||
return new ReferenceType(refty.getName(),
|
||||
new TypeParams(
|
||||
Arrays.stream(refty.getTypeParams().get())
|
||||
.map(x -> x.accept(this, ht))
|
||||
.collect(Collectors.toCollection(ArrayList::new))));
|
||||
}
|
||||
|
||||
public PlaceholderType visit(PlaceholderType phty, T ht) {
|
||||
return phty;
|
||||
}
|
||||
|
||||
public FunNType visit(FunNType funnty, T ht) {
|
||||
return FunNType.getFunNType(
|
||||
new TypeParams(
|
||||
Arrays.stream(funnty.getTypeParams().get())
|
||||
.map(x -> x.accept(this, ht))
|
||||
.collect(Collectors.toCollection(ArrayList::new)))
|
||||
);
|
||||
}
|
||||
|
||||
public SuperType visit(SuperType suty, T ht) {
|
||||
return new SuperType(suty.getWildcardedType().accept(this, ht));
|
||||
}
|
||||
|
||||
public ExtendsType visit(ExtendsType extty, T ht) {
|
||||
return new ExtendsType(extty.getWildcardedType().accept(this, ht));
|
||||
}
|
||||
}
|
||||
19
src/main/java/de/dhbwstuttgart/util/BiRelation.java
Normal file
19
src/main/java/de/dhbwstuttgart/util/BiRelation.java
Normal file
@ -0,0 +1,19 @@
|
||||
package de.dhbwstuttgart.util;
|
||||
|
||||
import java.util.ArrayList;
|
||||
|
||||
public class BiRelation<X,Y> extends ArrayList<Pair<X,Y>>{
|
||||
|
||||
public void put(X x, Y y) {
|
||||
this.add(new Pair<>(x,y));
|
||||
}
|
||||
|
||||
public void put(Pair<X,Y> p) {
|
||||
this.add(p);
|
||||
}
|
||||
|
||||
|
||||
public void putAll(BiRelation<X,Y> br) {
|
||||
this.addAll(br);
|
||||
}
|
||||
}
|
||||
25
src/main/java/de/dhbwstuttgart/util/Pair.java
Normal file
25
src/main/java/de/dhbwstuttgart/util/Pair.java
Normal file
@ -0,0 +1,25 @@
|
||||
package de.dhbwstuttgart.util;
|
||||
|
||||
import java.util.Optional;
|
||||
|
||||
public class Pair<T, T1> {
|
||||
private final T key;
|
||||
private final T1 value;
|
||||
|
||||
public Pair(T a, T1 b) {
|
||||
this.value = b;
|
||||
this.key = a;
|
||||
}
|
||||
|
||||
public Optional<T1> getValue() {
|
||||
return Optional.of(value);
|
||||
}
|
||||
|
||||
public T getKey() {
|
||||
return key;
|
||||
}
|
||||
|
||||
public String toString() {
|
||||
return "(" + key.toString() + "," + value.toString() + ")\n";
|
||||
}
|
||||
}
|
||||
@ -1,33 +0,0 @@
|
||||
import de.dhbwstuttgart.output.SolutionParser;
|
||||
import org.junit.Test;
|
||||
|
||||
import java.util.Map;
|
||||
|
||||
public class SolutionParserTest {
|
||||
@Test
|
||||
public void parseMatrixSolution(){
|
||||
String solution = "sigma(tph(\"_AMY\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AK\"),type(\"java.lang.Number\",null)) sigma(tph(\"_AY\"),type(\"java.lang.Number\",null)) sigma(tph(\"_J\"),type(\"java.lang.Number\",null)) sigma(tph(\"_V\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_G\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BK\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BA\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_U\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BU\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BO\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BG\"),type(\"java.lang.Number\",null)) sigma(tph(\"_BB\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BV\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AU\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AF\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BC\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AS\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null)))) sigma(tph(\"_BD\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AG\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AV\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_ANN\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_ANH\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AD\"),type(\"Matrix\",null)) sigma(tph(\"_AP\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null)))) sigma(tph(\"_R\"),type(\"java.lang.Boolean\",null)) sigma(tph(\"_BR\"),type(\"Object\",null)) sigma(tph(\"_ANO\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AB\"),type(\"Matrix\",null)) sigma(tph(\"_AM\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null))))\n";
|
||||
Map<String,String> sigmas = SolutionParser.parse(solution);
|
||||
for(var key : sigmas.keySet()){
|
||||
System.out.println(key + " -> " + sigmas.get(key));
|
||||
}
|
||||
}
|
||||
@Test
|
||||
public void parseOneSigma(){
|
||||
String solution = "sigma(tph(\"_AMY\"),type(\"java.lang.Integer\",null))";
|
||||
System.out.println(solution);
|
||||
Map<String,String> sigmas = SolutionParser.parse(solution);
|
||||
for(var key : sigmas.keySet()){
|
||||
System.out.println(key + " -> " + sigmas.get(key));
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
public void parseSolution(){
|
||||
String solution ="sigma(tph(\"_O\"),type(\"C1\",null)) sigma(tph(\"_W\"),type(\"C2\",null)) sigma(tph(\"_AM\"),type(\"C1\",null)) sigma(tph(\"_BA\"),type(\"C1\",null)) sigma(tph(\"_AW\"),type(\"C1\",null)) sigma(tph(\"_AO\"),type(\"C1\",null)) sigma(tph(\"_AK\"),type(\"C1\",null)) sigma(tph(\"_AI\"),type(\"C1\",null)) sigma(tph(\"_AQ\"),type(\"C1\",null)) sigma(tph(\"_AY\"),type(\"C1\",null)) sigma(tph(\"_AE\"),type(\"C1\",null)) sigma(tph(\"_BC\"),type(\"C1\",null)) sigma(tph(\"_AU\"),type(\"C1\",null)) sigma(tph(\"_AS\"),type(\"C1\",null)) sigma(tph(\"_V\"),type(\"java.lang.Object\",null)) sigma(tph(\"_N\"),type(\"C1\",null)) sigma(tph(\"_AG\"),type(\"C1\",null)) sigma(tph(\"_AD\"),type(\"C1\",null))\n";
|
||||
Map<String,String> sigmas = SolutionParser.parse(solution);
|
||||
for(var key : sigmas.keySet()){
|
||||
System.out.println(key + " -> " + sigmas.get(key));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1,11 +1,14 @@
|
||||
import de.dhbwstuttgart.input.ConstraintParser;
|
||||
import de.dhbwstuttgart.sat.asp.*;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.TypeUnify;
|
||||
import de.dhbwstuttgart.typeinference.unify.UnifyResultModel;
|
||||
import de.dhbwstuttgart.typeinference.unify.UnifyTaskModel;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.*;
|
||||
import org.apache.commons.io.output.NullWriter;
|
||||
import org.junit.Test;
|
||||
|
||||
import java.io.IOException;
|
||||
import java.nio.file.Files;
|
||||
import java.nio.file.Paths;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
|
||||
@ -15,845 +18,7 @@ import java.util.Set;
|
||||
public class UnifyTest {
|
||||
|
||||
public static final String rootDirectory = System.getProperty("user.dir")+"/resources/javFiles/";
|
||||
@Test
|
||||
public void generateConstraintSet(){
|
||||
System.out.println(ASPGenerator.generateOrCons(generateOrConstraintTwoSolutions("test")));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void parserTest(){
|
||||
String input = "Boolean =. g," +
|
||||
"t =. bc," +
|
||||
"f <. e," +
|
||||
"e =. bj," +
|
||||
"Vector<Integer> <. r," +
|
||||
"p <. l," +
|
||||
"e <. Number,";
|
||||
System.out.println(ASPGenerator.generateASP(ConstraintParser.parse(input)));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void extendsRelationParserTest(){
|
||||
String input = "Matrix < Vector<Vector<Integer>>," +
|
||||
"Vector<X> < List<X>," +
|
||||
"MyPair<X,Y> < Pair<X,X>," +
|
||||
"Pair<X,Y> < Object," +
|
||||
"List<X> < Object";
|
||||
System.out.println(ASPGenerator.generateExtendsRelations(ConstraintParser.parseExtendsRelations(input)));
|
||||
//TODO: Finish Extends Relation parser
|
||||
}
|
||||
/*
|
||||
@Test
|
||||
public void orConsTest() throws IOException {
|
||||
String input =
|
||||
"java.lang.Boolean < java.lang.Object," +
|
||||
"java.lang.String < java.lang.Object," +
|
||||
"java.lang.Integer < java.lang.Object," +
|
||||
"OrConsTest < java.lang.Object," +
|
||||
"MyPair<X,Y> < Pair<X,X>," +
|
||||
"Pair<X,Y> < Object," +
|
||||
"List<X> < Object," +
|
||||
"Integer < Object, String < Object, " +
|
||||
Files.readString(Paths.get("/","tmp","output"));
|
||||
System.out.println(ASPGenerator.generateASP(ConstraintParser.parse(input)));
|
||||
System.out.println(ASPGenerator.generateExtendsRelations(ConstraintParser.parseExtendsRelations(input)));
|
||||
}
|
||||
*/
|
||||
@Test
|
||||
public void alotOfOrConstraintsTest(){
|
||||
String input =
|
||||
"Vector<X> < List<X>," +
|
||||
"MyPair<X,Y> < Pair<X,X>," +
|
||||
"Pair<X,Y> < Object," +
|
||||
"List<X> < Object," +
|
||||
"Integer < Object, String < Object, " +
|
||||
"{List<Integer> <. _a | List<String> <. _a}{List<_c> <. _b, String <. Object | List<_c> <. _b} {Vector<Integer> <. _b | Vector<String> <. _b}"+
|
||||
"{List<Integer> <. _aa | List<String> <. _aa}{List<_c> <. _ba | List<_c> <. _ba} {Vector<Integer> <. _ba | Vector<String> <. _ba}"+
|
||||
"{List<Integer> <. _aaa | List<String> <. _aaa}{List<_c> <. _baa | List<_c> <. _baa} {Vector<Integer> <. _baa | Vector<String> <. _baa}";
|
||||
|
||||
System.out.println(ASPGenerator.generateASP(ConstraintParser.parse(input)));
|
||||
System.out.println(ASPGenerator.generateExtendsRelations(ConstraintParser.parseExtendsRelations(input)));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void matrix(){
|
||||
String input = "java.lang.Boolean < Object," +
|
||||
"java.lang.Integer < java.lang.Number," +
|
||||
"java.lang.Number < Object," + //TODO: Implement smaller
|
||||
"java.util.Vector<X> < Object," +
|
||||
"Matrix < java.util.Vector<java.util.Vector<java.lang.Integer>>\n" +
|
||||
"_BE=.java.lang.Boolean\n" +
|
||||
"java.util.Vector<java.util.Vector<java.lang.Integer>>=.java.util.Vector<_ANR>\n" +
|
||||
"_AU<.java.lang.Number\n" +
|
||||
"java.util.Vector<java.lang.Integer><._AS\n" +
|
||||
"_AI=.Matrix\n" +
|
||||
"_AF=._CK\n" +
|
||||
"_AP<._AM\n" +
|
||||
"_BC<.java.lang.Number\n" +
|
||||
"java.util.Vector<java.util.Vector<java.lang.Integer>>=.java.util.Vector<_ANQ>\n" +
|
||||
"_S=.Matrix\n" +
|
||||
"_BD<._BC\n" +
|
||||
"_AV<._AU\n" +
|
||||
"_AU<.java.lang.Number\n" +
|
||||
"_BV<._BA\n" +
|
||||
"Matrix<._AD\n" +
|
||||
"_J<.java.lang.Number\n" +
|
||||
"java.lang.Boolean=._AH\n" +
|
||||
"_V<.java.lang.Integer\n" +
|
||||
"_AY<.java.lang.Number\n" +
|
||||
"_BC=._BW\n" +
|
||||
"_AK<.java.lang.Number\n" +
|
||||
"_AH=.java.lang.Boolean\n" +
|
||||
"_BC<.java.lang.Number\n" +
|
||||
"_AQ=.Matrix\n" +
|
||||
"_G<.java.lang.Integer\n" +
|
||||
"java.lang.Integer<.java.lang.Number\n" +
|
||||
"_AF<.java.lang.Number\n" +
|
||||
"_AW=.java.lang.Boolean\n" +
|
||||
"_BB<._BA\n" +
|
||||
"java.lang.Boolean=._AW\n" +
|
||||
"java.lang.Boolean=._H\n" +
|
||||
"_H=.java.lang.Boolean\n" +
|
||||
"_AD<._AB\n" +
|
||||
"_AF<.java.lang.Number\n" +
|
||||
"_BG<.java.lang.Number\n" +
|
||||
"java.lang.Boolean=._BE\n" +
|
||||
"_AU=._CD\n" +
|
||||
"_AG<._AF\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"Matrix<.Matrix\n" +
|
||||
"_AE=.Matrix\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AG=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AI=.java.util.AbstractList<_AMV>\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AI=.Matrix\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"_AI=.java.util.List<_AMU>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AI=.java.util.AbstractList<_AMV>\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AI=.java.util.Vector<_AMW>\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AI=.java.util.List<_AMU>\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"_AI=.java.util.Vector<_AMW>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AI=.Matrix\n" +
|
||||
"java.lang.Integer<._AK\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AF<.java.lang.Integer\n" +
|
||||
"_AQ=.java.util.Vector<_AMX>\n" +
|
||||
"_AMX<._AP\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AF<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._AP\n" +
|
||||
"_AQ=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AF<.java.lang.Integer\n" +
|
||||
"_AQ=.java.util.Vector<_AMX>\n" +
|
||||
"_AMX<._AP\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._AP\n" +
|
||||
"_AF<.java.lang.Integer\n" +
|
||||
"_AQ=.Matrix\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AT=.java.util.Vector<GE>\n" +
|
||||
"java.util.Vector<_AMY><.java.util.Vector<java.lang.Integer>\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AV=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"_AM=.java.util.List<_AMZ>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"_AM=.java.util.Vector<_ANB>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.List<_AMZ>\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"_AM=.java.util.AbstractList<_ANA>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.AbstractList<_ANA>\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.Vector<_ANB>\n" +
|
||||
"java.lang.Integer<._AY\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BB=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BD=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AM=.java.util.Vector<_ANE>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.Vector<_ANE>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.AbstractList<_AND>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.List<_ANC>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.List<_ANC>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.AbstractList<_AND>\n" +
|
||||
"java.lang.Integer<._BG\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.Matrix\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BK\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANG<._BK\n" +
|
||||
"_AM=.java.util.AbstractList<_ANG>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.Vector<_ANH>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_ANH<._BK\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.AbstractList<_ANG>\n" +
|
||||
"_ANG<._BK\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.List<_ANF>\n" +
|
||||
"_ANF<._BK\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AM=.java.util.List<_ANF>\n" +
|
||||
"_ANF<._BK\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANH<._BK\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_AM=.java.util.Vector<_ANH>\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_ANI<._BR\n" +
|
||||
"_AC=.java.util.List<_ANI>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AC=.Matrix\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BR\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AC=.Matrix\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BR\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANJ<._BR\n" +
|
||||
"_AC=.java.util.AbstractList<_ANJ>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_AC=.java.util.Vector<_ANK>\n" +
|
||||
"_ANK<._BR\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AC=.java.util.Vector<_ANK>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_ANK<._BR\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_AC=.java.util.List<_ANI>\n" +
|
||||
"_ANI<._BR\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AC=.java.util.AbstractList<_ANJ>\n" +
|
||||
"_BC<.java.lang.Integer\n" +
|
||||
"_ANJ<._BR\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BR=.java.util.AbstractList<_ANM>\n" +
|
||||
"_ANM<._BO\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BO\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"_BR=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"_ANL<._BO\n" +
|
||||
"_BR=.java.util.List<_ANL>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"_BR=.java.util.List<_ANL>\n" +
|
||||
"_ANL<._BO\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANN<._BO\n" +
|
||||
"_BR=.java.util.Vector<_ANN>\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANM<._BO\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"_BR=.java.util.AbstractList<_ANM>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANN<._BO\n" +
|
||||
"_BR=.java.util.Vector<_ANN>\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_BR=.Matrix\n" +
|
||||
"java.util.Vector<java.lang.Integer><._BO\n" +
|
||||
"_AU<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BK<.java.lang.Integer\n" +
|
||||
"java.lang.Integer=._BU\n" +
|
||||
"_BO<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BU<.java.lang.Integer\n" +
|
||||
"_BA<.java.lang.Integer\n" +
|
||||
"java.lang.Integer=._BV\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_BA<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"_AS=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AS=.Matrix\n" +
|
||||
"_BA<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_BA<._ANO\n" +
|
||||
"_AS=.java.util.Vector<_ANO>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_BA<._ANO\n" +
|
||||
"_AS=.java.util.Vector<_ANO>\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_AS<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"_AD=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AS<._ANP\n" +
|
||||
"_AD=.java.util.Vector<_ANP>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AS<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"_AD=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AS<._ANP\n" +
|
||||
"_AD=.java.util.Vector<_ANP>\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_G=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_F=.java.util.List<_ANS>\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.AbstractList<_ANT>\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_ANU>\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"_F=.java.util.List<_ANS>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"_F=.java.util.Vector<_ANU>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Integer<._J\n" +
|
||||
"_F=.java.util.AbstractList<_ANT>\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_F=.java.util.Vector<_ANV>\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_ANV<._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_ANV<._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_F=.java.util.Vector<_ANV>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_ANX>\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_ANX<._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_ANX>\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_ANX<._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_ANZ>\n" +
|
||||
"_ANZ<._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_ANZ>\n" +
|
||||
"_ANZ<._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_AOB<._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_F=.java.util.Vector<_AOB>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_F=.java.util.Vector<_AOB>\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_AOB<._N\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.util.Vector<java.lang.Integer><._N\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"_F=.Matrix\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_N<._AOA\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.java.util.Vector<_AOA>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_N<._ANW\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.java.util.List<_ANW>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_S=.java.util.List<_ANW>\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_N<._ANW\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_N<._AOA\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.java.util.Vector<_AOA>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"_N<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.Matrix\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.Matrix\n" +
|
||||
"_N<.java.util.Vector<java.lang.Integer>\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.java.util.AbstractList<_ANY>\n" +
|
||||
"_N<._ANY\n" +
|
||||
"}\n" +
|
||||
"|{\n" +
|
||||
"java.lang.Boolean<._R\n" +
|
||||
"_S=.java.util.AbstractList<_ANY>\n" +
|
||||
"_N<._ANY\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"_U=.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n" +
|
||||
"{\n" +
|
||||
"{\n" +
|
||||
"java.lang.Integer<.java.lang.Integer\n" +
|
||||
"java.lang.Integer=._V\n" +
|
||||
"_U<.java.lang.Integer\n" +
|
||||
"}\n" +
|
||||
"}\n";
|
||||
System.out.println(ASPGenerator.generateASP(ConstraintParser.parse(input)));
|
||||
System.out.println(ASPGenerator.generateExtendsRelations(ConstraintParser.parseExtendsRelations(input)));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void matrix2k(){
|
||||
//und-constraints
|
||||
//T =. BC
|
||||
//java.lang.Boolean =. G
|
||||
//G =. java.lang.Boolean
|
||||
//F <. E
|
||||
//E =. BJ
|
||||
//Vector<java.lang.Integer> <. R
|
||||
//P <. L
|
||||
//E <!=. java.lang.Number
|
||||
//C =. A
|
||||
//M =. Matrix
|
||||
//AC <. AB
|
||||
//Matrix <. C
|
||||
//AB =. AV
|
||||
//X <!=. java.lang.Number
|
||||
//java.lang.Boolean =. AD
|
||||
//AU <. Z
|
||||
//AD =. java.lang.Boolean
|
||||
//H =. Matrix
|
||||
//AA <. Z
|
||||
//AB <!=. java.lang.Number
|
||||
//V =. java.lang.Boolean
|
||||
//java.lang.Boolean =. V
|
||||
//J <!=. java.lang.Number
|
||||
//oder-constraints
|
||||
//set #1
|
||||
//Matrix <. Matrix
|
||||
//set #2
|
||||
//F =. java.lang.Float
|
||||
//F =. java.lang.Integer
|
||||
//set #3
|
||||
//H =. ? extends Matrix
|
||||
//java.lang.Integer =. J
|
||||
//H =. Vector<ALB>
|
||||
//java.lang.Integer =. J
|
||||
//H =. Matrix
|
||||
//java.lang.Integer =. J
|
||||
//H =. ? extends Vector<ALB>
|
||||
//java.lang.Integer =. J
|
||||
//set #4
|
||||
//ALC =. P
|
||||
//M =. Vector<ALC>
|
||||
//E <. java.lang.Integer
|
||||
//Vector<java.lang.Integer> =. P
|
||||
//M =. ? extends Matrix
|
||||
//E <. java.lang.Integer
|
||||
//Vector<java.lang.Integer> =. P
|
||||
//M =. Matrix
|
||||
//E <. java.lang.Integer
|
||||
//ALC =. P
|
||||
//M =. ? extends Vector<ALC>
|
||||
//E <. java.lang.Integer
|
||||
//set #5
|
||||
//Vector<ALD> <. Vector<java.lang.Integer>
|
||||
//set #6
|
||||
//U =. java.lang.Float
|
||||
//U =. java.lang.Integer
|
||||
//set #7
|
||||
//L =. ? extends Matrix
|
||||
//java.lang.Integer =. X
|
||||
//L =. ? extends Vector<AMH>
|
||||
//java.lang.Integer =. X
|
||||
//L =. Matrix
|
||||
//java.lang.Integer =. X
|
||||
//L =. Vector<AMH>
|
||||
//java.lang.Integer =. X
|
||||
//set #8
|
||||
//AA =. java.lang.Float
|
||||
//AA =. java.lang.Integer
|
||||
//set #9
|
||||
//AC =. java.lang.Integer
|
||||
//AC =. java.lang.Float
|
||||
//set #10
|
||||
//L =. ? extends Matrix
|
||||
//java.lang.Integer =. AF
|
||||
//L =. ? extends Vector<ANL>
|
||||
//java.lang.Integer =. AF
|
||||
//L =. Matrix
|
||||
//java.lang.Integer =. AF
|
||||
//L =. Vector<ANL>
|
||||
//java.lang.Integer =. AF
|
||||
//set #11
|
||||
//Vector<java.lang.Integer> =. AJ
|
||||
//L =. Matrix
|
||||
//AB <. java.lang.Integer
|
||||
//ANM =. AJ
|
||||
//L =. ? extends Vector<ANM>
|
||||
//AB <. java.lang.Integer
|
||||
//Vector<java.lang.Integer> =. AJ
|
||||
//L =. ? extends Matrix
|
||||
//AB <. java.lang.Integer
|
||||
//ANM =. AJ
|
||||
//L =. Vector<ANM>
|
||||
//AB <. java.lang.Integer
|
||||
//set #12
|
||||
//AB <. java.lang.Integer
|
||||
//Vector<java.lang.Integer> =. AN
|
||||
//B =. Matrix
|
||||
//ANN =. AN
|
||||
//AB <. java.lang.Integer
|
||||
//B =. ? extends Vector<ANN>
|
||||
//B =. Vector<ANN>
|
||||
//ANN =. AN
|
||||
//AB <. java.lang.Integer
|
||||
//B =. ? extends Matrix
|
||||
//AB <. java.lang.Integer
|
||||
//Vector<java.lang.Integer> =. AN
|
||||
//set #13
|
||||
//Vector<java.lang.Integer> =. AR
|
||||
//AN =. ? extends Matrix
|
||||
//T <. java.lang.Integer
|
||||
//AN =. ? extends Vector<ANO>
|
||||
//ANO =. AR
|
||||
//T <. java.lang.Integer
|
||||
//AN =. Vector<ANO>
|
||||
//ANO =. AR
|
||||
//T <. java.lang.Integer
|
||||
//AN =. Matrix
|
||||
//Vector<java.lang.Integer> =. AR
|
||||
//T <. java.lang.Integer
|
||||
//set #14
|
||||
//java.lang.Integer =. AT
|
||||
//AJ <. java.lang.Integer
|
||||
//AR <. java.lang.Integer
|
||||
|
||||
|
||||
}
|
||||
|
||||
@Test
|
||||
public void matrixTestBasic(){
|
||||
/*
|
||||
//und-constraints
|
||||
//Matrix <. ret
|
||||
//Integer <. i
|
||||
//Matrix <. Vector<x?>
|
||||
//x? <. v1
|
||||
//i <. Integer
|
||||
//Vector<Integer> <. v2
|
||||
//v1 <. Vector<y?>
|
||||
//m <. Vector<z?>
|
||||
//z? <. zr
|
||||
//zr <. Vector<z2?>
|
||||
//z2? <. z2r
|
||||
//z2r <. Integer
|
||||
//v1 <. Vector<y2?>
|
||||
//y2? <. y2r
|
||||
//y2r <. Integer
|
||||
*/
|
||||
HashSet<Pair> cons = new HashSet<>();
|
||||
//v2 <. x2r
|
||||
cons.add(new LessDot(new TypePlaceholder("v2"), new TypePlaceholder("x2r")));
|
||||
//x2? <. x2r
|
||||
cons.add(new LessDot(new TypePlaceholder("x2"), new TypePlaceholder("x2r")));
|
||||
//ret <. Vector<x2?>
|
||||
cons.add(new LessDot(new TypePlaceholder("ret"), new NamedType("Vector", List.of(new TypePlaceholder("x2")))));
|
||||
//v2 <. Vector<x3?>
|
||||
cons.add(new LessDot(new TypePlaceholder("v2"), new NamedType("Vector", List.of(new TypePlaceholder("x3")))));
|
||||
//x3? <. x3r
|
||||
cons.add(new LessDot(new TypePlaceholder("x3"), new TypePlaceholder("x3r")));
|
||||
//Integer <. x3r
|
||||
cons.add(new LessDot(new NamedType("Integer", List.of()), new TypePlaceholder("x3r")));
|
||||
|
||||
//Matrix <. ret
|
||||
cons.add(new LessDot(new NamedType("Matrix", List.of()), new TypePlaceholder("ret")));
|
||||
//Integer <. i
|
||||
cons.add(new LessDot(new NamedType("Integer", List.of()), new TypePlaceholder("i")));
|
||||
//Matrix <. Vector<x?>
|
||||
cons.add(new LessDot(new NamedType("Matrix", List.of()), new NamedType("Vector", List.of(new TypePlaceholder("x")))));
|
||||
//x? <. v1
|
||||
cons.add(new LessDot(new TypePlaceholder("x"), new TypePlaceholder("v1")));
|
||||
//i <. Integer
|
||||
cons.add(new LessDot(new TypePlaceholder("i"), new NamedType("Integer", List.of())));
|
||||
//Vector<Integer> <. v2
|
||||
cons.add(new LessDot(new NamedType("Vector", List.of(new NamedType("Integer", List.of()))), new TypePlaceholder("v2")));
|
||||
//v1 <. Vector<y?>
|
||||
cons.add(new LessDot(new TypePlaceholder("v1"), new NamedType("Vector", List.of(new TypePlaceholder("y")))));
|
||||
//m <. Vector<z?>
|
||||
cons.add(new LessDot(new TypePlaceholder("m"), new NamedType("Vector", List.of(new TypePlaceholder("z")))));
|
||||
//z? <. zr
|
||||
cons.add(new LessDot(new TypePlaceholder("z"), new TypePlaceholder("zr")));
|
||||
//zr <. Vector<z2?>
|
||||
cons.add(new LessDot(new TypePlaceholder("z"), new TypePlaceholder("zr")));
|
||||
//z2? <. z2r
|
||||
//z2r <. Integer
|
||||
//v1 <. Vector<y2?>
|
||||
//y2? <. y2r
|
||||
//y2r <. Integer
|
||||
cons.add(new LessDot(new TypePlaceholder("z2"), new TypePlaceholder("z2r"))); // z2? <. z2r
|
||||
cons.add(new LessDot(new TypePlaceholder("z2r"), new NamedType("Integer", List.of()))); // z2r <. Integer
|
||||
cons.add(new LessDot(new TypePlaceholder("v1"), new NamedType("Vector", List.of(new TypePlaceholder("y2"))))); // v1 <. Vector<y2?>
|
||||
cons.add(new LessDot(new TypePlaceholder("y2"), new TypePlaceholder("y2r"))); // y2? <. y2r
|
||||
cons.add(new LessDot(new TypePlaceholder("y2r"), new NamedType("Integer", List.of()))); // y2r <. Integer
|
||||
for(Pair p : cons){
|
||||
System.out.println(p.toASP() + ".");
|
||||
}
|
||||
System.out.println(ASPGenerator.generateUndCons(cons));
|
||||
}
|
||||
|
||||
private List<Set<Pair>> generateOrConstraintTwoSolutions(String name){
|
||||
return List.of(genOrConstraintWithOneSolution(name+"1"), genOrConstraintWithOneSolution(name+"2"));
|
||||
}
|
||||
private Set<Pair> genOrConstraintWithOneSolution(String name){
|
||||
Type type1 = new TypePlaceholder(name);
|
||||
Type type2 = new NamedType("List", List.of(new NamedType("Integer", List.of())));
|
||||
Pair pair1 = new LessDot(type2, type1);
|
||||
|
||||
type1 = new TypePlaceholder(name);
|
||||
type2 = new NamedType("List", List.of(new TypePlaceholder(name+"2")));
|
||||
Pair pair2 = new LessDot(type1, type2);
|
||||
Set<Pair> undCons2 = Set.of(pair1, pair2);
|
||||
|
||||
return undCons2;
|
||||
}
|
||||
|
||||
/*
|
||||
private UnifyPair genPairListOfInteger(String name){
|
||||
|
||||
UnifyType type1 = new PlaceholderType(name);
|
||||
@ -911,12 +76,13 @@ public class UnifyTest {
|
||||
|
||||
TypeUnify unifyAlgo = new TypeUnify();
|
||||
ConstraintSet<Pair> cons = new ConstraintSet<>();
|
||||
UnifyResultModelParallel urm = new UnifyResultModelParallel(cons, finiteClosure);
|
||||
UnifyTaskModelParallel tasks = new UnifyTaskModelParallel();
|
||||
UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
|
||||
UnifyTaskModel tasks = new UnifyTaskModel();
|
||||
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
|
||||
System.out.println(solution.size());
|
||||
//System.out.println(solution);
|
||||
}
|
||||
|
||||
@Test
|
||||
public void basicMatrixTest(){
|
||||
UnifyType type1;
|
||||
@ -1019,7 +185,7 @@ public class UnifyTest {
|
||||
type2 = new ReferenceType("Vector", new TypeParams(new ReferenceType("Vector", new TypeParams(new ReferenceType("Integer")))));
|
||||
constraints.add(new UnifyPair(type1, type2, PairOperator.SMALLER));
|
||||
//Vector<X> extends Object
|
||||
type1 = new ReferenceType("Vector", new TypeParams(new PlaceholderType("X")));
|
||||
type1 = new ReferenceType("Vector", new TypeParams(new ReferenceType("X")));
|
||||
type2 = new ReferenceType("Object");
|
||||
constraints.add(new UnifyPair(type1, type2, PairOperator.SMALLER));
|
||||
//Integer extends Object
|
||||
@ -1030,8 +196,8 @@ public class UnifyTest {
|
||||
|
||||
TypeUnify unifyAlgo = new TypeUnify();
|
||||
ConstraintSet< Pair> cons = new ConstraintSet<>();
|
||||
UnifyResultModelParallel urm = new UnifyResultModelParallel(cons, finiteClosure);
|
||||
UnifyTaskModelParallel tasks = new UnifyTaskModelParallel();
|
||||
UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
|
||||
UnifyTaskModel tasks = new UnifyTaskModel();
|
||||
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
|
||||
System.out.println(solution.size());
|
||||
}
|
||||
@ -1506,8 +672,8 @@ public class UnifyTest {
|
||||
FiniteClosure finiteClosure = new FiniteClosure(fcConstraints, new NullWriter());
|
||||
TypeUnify unifyAlgo = new TypeUnify();
|
||||
ConstraintSet< Pair> cons = new ConstraintSet<>();
|
||||
UnifyResultModelParallel urm = new UnifyResultModelParallel(cons, finiteClosure);
|
||||
UnifyTaskModelParallel tasks = new UnifyTaskModelParallel();
|
||||
UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
|
||||
UnifyTaskModel tasks = new UnifyTaskModel();
|
||||
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
|
||||
System.out.println(solution.size());
|
||||
}
|
||||
@ -2067,8 +1233,8 @@ public class UnifyTest {
|
||||
FiniteClosure finiteClosure = new FiniteClosure(fcConstraints, new NullWriter());
|
||||
TypeUnify unifyAlgo = new TypeUnify();
|
||||
ConstraintSet< Pair> cons = new ConstraintSet<>();
|
||||
UnifyResultModelParallel urm = new UnifyResultModelParallel(cons, finiteClosure);
|
||||
UnifyTaskModelParallel tasks = new UnifyTaskModelParallel();
|
||||
UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
|
||||
UnifyTaskModel tasks = new UnifyTaskModel();
|
||||
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
|
||||
System.out.println(solution.size());
|
||||
}
|
||||
@ -2176,7 +1342,7 @@ public class UnifyTest {
|
||||
//oder-constraints
|
||||
List<Set<Constraint<UnifyPair>>> oderConstraints = new ArrayList<>();
|
||||
Set<Constraint<UnifyPair>> constraints = new HashSet<>();
|
||||
HashSet<UnifyPair> constraint = new HashSet<>();
|
||||
Constraint<UnifyPair> constraint = new Constraint<>();
|
||||
|
||||
//set #1
|
||||
constraints = new HashSet<>();
|
||||
@ -2251,7 +1417,7 @@ public class UnifyTest {
|
||||
//set #4
|
||||
constraints = new HashSet<>();
|
||||
//ALC =. P
|
||||
constraint = new HashSet<UnifyPair>();
|
||||
constraint = new Constraint<>();
|
||||
type1 = new PlaceholderType("ALC");
|
||||
type2 = new PlaceholderType("P");
|
||||
constraint.add(new UnifyPair(type1, type2, PairOperator.EQUALSDOT));
|
||||
@ -2930,8 +2096,12 @@ public class UnifyTest {
|
||||
fcConstraints.add(new UnifyPair(type1, type2, PairOperator.SMALLER));
|
||||
|
||||
FiniteClosure finiteClosure = new FiniteClosure(fcConstraints, new NullWriter());
|
||||
ASPGenerator.generateASP(undConstraints);
|
||||
TypeUnify unifyAlgo = new TypeUnify();
|
||||
ConstraintSet< Pair> cons = new ConstraintSet<>();
|
||||
UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure);
|
||||
UnifyTaskModel tasks = new UnifyTaskModel();
|
||||
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
|
||||
System.out.println(solution.size());
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user