Compare commits
18 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
db3f3bcbac | ||
|
|
163e130b13 | ||
|
|
cddf3ccece | ||
|
8b55d8f159 | ||
|
|
02275e0b41 | ||
|
3c0f0dcf55 | ||
|
|
af0dad2b09 | ||
|
|
2887b8936d | ||
|
2827098a27 | ||
|
|
cd017ba665 | ||
|
|
2cf39b3b8c | ||
|
|
33b4710dac | ||
|
|
cb99c79213 | ||
|
|
d82c4d3ebf | ||
|
|
536fe9239e | ||
|
|
2b7b17060a | ||
|
|
313b021fdc | ||
|
|
e448d19616 |
1
pom.xml
1
pom.xml
@ -53,7 +53,6 @@ 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>
|
||||
|
||||
@ -0,0 +1,23 @@
|
||||
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.$[;][0-9A-Za-z.$[;_]*;
|
||||
|
||||
NEWLINE : [\r\n]+ -> skip;
|
||||
WS: [ \t] -> skip ;
|
||||
11
src/main/antlr4/de/dhbwstuttgart/input/parser/Solution.g4
Normal file
11
src/main/antlr4/de/dhbwstuttgart/input/parser/Solution.g4
Normal file
@ -0,0 +1,11 @@
|
||||
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 ;
|
||||
127
src/main/asp/unify.lp
Normal file
127
src/main/asp/unify.lp
Normal file
@ -0,0 +1,127 @@
|
||||
% 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.
|
||||
153
src/main/asp/unifyOrCons.lp
Normal file
153
src/main/asp/unifyOrCons.lp
Normal file
File diff suppressed because one or more lines are too long
155
src/main/asp/unifyPaper.lp
Normal file
155
src/main/asp/unifyPaper.lp
Normal file
@ -0,0 +1,155 @@
|
||||
% 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.
|
||||
@ -1,7 +0,0 @@
|
||||
package de.dhbwstuttgart.exceptions;
|
||||
|
||||
public class DebugException extends RuntimeException{
|
||||
public DebugException(String message){
|
||||
System.err.println(message);
|
||||
}
|
||||
}
|
||||
87
src/main/java/de/dhbwstuttgart/input/ConstraintParser.java
Normal file
87
src/main/java/de/dhbwstuttgart/input/ConstraintParser.java
Normal file
@ -0,0 +1,87 @@
|
||||
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());
|
||||
}
|
||||
}
|
||||
}
|
||||
37
src/main/java/de/dhbwstuttgart/output/SolutionParser.java
Normal file
37
src/main/java/de/dhbwstuttgart/output/SolutionParser.java
Normal file
@ -0,0 +1,37 @@
|
||||
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;
|
||||
}
|
||||
}
|
||||
53
src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java
Normal file
53
src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java
Normal file
@ -0,0 +1,53 @@
|
||||
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;
|
||||
}
|
||||
}
|
||||
8
src/main/java/de/dhbwstuttgart/sat/asp/EqualsDot.java
Normal file
8
src/main/java/de/dhbwstuttgart/sat/asp/EqualsDot.java
Normal file
@ -0,0 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record EqualsDot(Type left, Type right) implements Pair {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "equalcons("+ left().toASP() + "," + right().toASP() + ")";
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,6 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
import java.util.List;
|
||||
|
||||
public record ExtendsRelation(String subtypeName, List<TypeParameter> subtypeParams, NamedType superType) {
|
||||
}
|
||||
8
src/main/java/de/dhbwstuttgart/sat/asp/LessDot.java
Normal file
8
src/main/java/de/dhbwstuttgart/sat/asp/LessDot.java
Normal file
@ -0,0 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record LessDot(Type left, Type right) implements Pair {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "subcons("+ left().toASP() + "," + right().toASP() + ")";
|
||||
}
|
||||
}
|
||||
12
src/main/java/de/dhbwstuttgart/sat/asp/NamedType.java
Normal file
12
src/main/java/de/dhbwstuttgart/sat/asp/NamedType.java
Normal file
@ -0,0 +1,12 @@
|
||||
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)";
|
||||
}
|
||||
}
|
||||
5
src/main/java/de/dhbwstuttgart/sat/asp/Pair.java
Normal file
5
src/main/java/de/dhbwstuttgart/sat/asp/Pair.java
Normal file
@ -0,0 +1,5 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public interface Pair {
|
||||
String toASP();
|
||||
}
|
||||
6
src/main/java/de/dhbwstuttgart/sat/asp/Type.java
Normal file
6
src/main/java/de/dhbwstuttgart/sat/asp/Type.java
Normal file
@ -0,0 +1,6 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public interface Type {
|
||||
String name();
|
||||
String toASP();
|
||||
}
|
||||
@ -0,0 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record TypeParameter(String name) implements Type{
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "X"+name;
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
public record TypePlaceholder(String name) implements Type {
|
||||
@Override
|
||||
public String toASP() {
|
||||
return "tph(\""+name+"\")";
|
||||
}
|
||||
}
|
||||
@ -1,69 +0,0 @@
|
||||
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();
|
||||
}
|
||||
|
||||
}
|
||||
@ -1,126 +0,0 @@
|
||||
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;
|
||||
}
|
||||
}
|
||||
@ -1,13 +0,0 @@
|
||||
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
|
||||
@ -1,21 +0,0 @@
|
||||
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;
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -1,23 +0,0 @@
|
||||
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);
|
||||
}
|
||||
|
||||
}
|
||||
@ -1,11 +0,0 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
public interface IUnifyResultListener {
|
||||
|
||||
void onNewTypeResultFound(Set<Set<UnifyPair>> evt);
|
||||
|
||||
}
|
||||
@ -1,108 +0,0 @@
|
||||
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);
|
||||
}
|
||||
}
|
||||
@ -1,92 +0,0 @@
|
||||
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);
|
||||
}
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,130 +0,0 @@
|
||||
package de.dhbwstuttgart.typeinference.unify;
|
||||
|
||||
import java.io.FileWriter;
|
||||
import java.io.IOException;
|
||||
import java.io.Writer;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.concurrent.ForkJoinPool;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
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, UnifyResultModelParallel ret, UnifyTaskModelParallel usedTasks) {
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
ConstraintSetRepository constraintSetRepository = new ConstraintSetRepository();
|
||||
usedTasks.setPool(pool);
|
||||
ret.setPool(pool);
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, constraintSetRepository);
|
||||
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 UnifyResultModelParallel unifyAsync(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModelParallel ret, UnifyTaskModelParallel usedTasks) {
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
ConstraintSetRepository constraintSetRepository = new ConstraintSetRepository();
|
||||
usedTasks.setPool(pool);
|
||||
ret.setPool(pool);
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, constraintSetRepository);
|
||||
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 UnifyResultModelParallel unifyParallel(Set<UnifyPair> undConstrains, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModelParallel ret, UnifyTaskModelParallel usedTasks) {
|
||||
ForkJoinPool pool = new ForkJoinPool(Runtime.getRuntime().availableProcessors(), ForkJoinPool.defaultForkJoinWorkerThreadFactory, null, true);
|
||||
ConstraintSetRepository constraintSetRepository = new ConstraintSetRepository();
|
||||
usedTasks.setPool(pool);
|
||||
ret.setPool(pool);
|
||||
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, constraintSetRepository, statistics);
|
||||
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;
|
||||
| ||||