Compare commits

...

18 Commits
main ... main

Author SHA1 Message Date
Andreas Stadelmeier
db3f3bcbac Many Or Constraint test used for benchmark for KRRUP Seminar presentation 2024-11-28 13:12:30 +01:00
Andreas Stadelmeier
163e130b13 Fix Identifier in Grammar 2024-11-28 13:09:25 +01:00
Andreas Stadelmeier
cddf3ccece Add Or Cons Test 2024-11-26 13:51:45 +01:00
Andreas Stadelmeier
8b55d8f159 rename pl -> lp 2024-09-11 09:46:54 +02:00
Andreas Stadelmeier
02275e0b41 Comment out coConsTest 2024-07-16 15:39:21 +02:00
Andreas Stadelmeier
3c0f0dcf55 Fix Parser. Add Numbers for Identifiers 2024-07-01 12:37:27 +02:00
Andreas Stadelmeier
af0dad2b09 OL example and fix orCOnstraints 2024-07-01 12:37:00 +02:00
Andreas Stadelmeier
2887b8936d o <. Object does not work 2024-06-28 11:58:01 +02:00
JanUlrich
2827098a27 Change super to subtype in ASP generation 2024-06-27 21:52:36 +02:00
JanUlrich
cd017ba665 Fix Constraint Set Grammar. Add Or Constraint Test 2024-06-23 00:45:49 +02:00
Andreas Stadelmeier
2cf39b3b8c Change ASP Generator and add Solution Parser 2024-06-21 02:33:15 +02:00
JanUlrich
33b4710dac New Algorithm with Matrix input 2024-06-19 23:15:52 +02:00
Andreas Stadelmeier
cb99c79213 Start Implementation of the Algorithm described in the paper 2024-06-18 18:44:11 +02:00
Andreas Stadelmeier
d82c4d3ebf First Workin Matrix Test 2024-06-10 08:57:04 +02:00
Andreas Stadelmeier
536fe9239e Fix 2024-06-07 11:16:41 +02:00
Andreas Stadelmeier
2b7b17060a Implement Parser 2024-06-07 10:51:42 +02:00
JanUlrich
313b021fdc Implement First Test 2024-06-06 20:38:03 +02:00
Andreas Stadelmeier
e448d19616 Add Unify ASP prototype. Start implementing tests and Constraint -> ASP Input 2024-06-05 20:03:18 +02:00
65 changed files with 2926 additions and 7451 deletions

View File

@ -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>

View File

@ -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 ;

View 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
View 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

File diff suppressed because one or more lines are too long

155
src/main/asp/unifyPaper.lp Normal file
View 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.

View File

@ -1,7 +0,0 @@
package de.dhbwstuttgart.exceptions;
public class DebugException extends RuntimeException{
public DebugException(String message){
System.err.println(message);
}
}

View 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());
}
}
}

View 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;
}
}

View 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;
}
}

View 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() + ")";
}
}

View File

@ -0,0 +1,6 @@
package de.dhbwstuttgart.sat.asp;
import java.util.List;
public record ExtendsRelation(String subtypeName, List<TypeParameter> subtypeParams, NamedType superType) {
}

View 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() + ")";
}
}

View 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)";
}
}

View File

@ -0,0 +1,5 @@
package de.dhbwstuttgart.sat.asp;
public interface Pair {
String toASP();
}

View File

@ -0,0 +1,6 @@
package de.dhbwstuttgart.sat.asp;
public interface Type {
String name();
String toASP();
}

View File

@ -0,0 +1,8 @@
package de.dhbwstuttgart.sat.asp;
public record TypeParameter(String name) implements Type{
@Override
public String toASP() {
return "X"+name;
}
}

View File

@ -0,0 +1,8 @@
package de.dhbwstuttgart.sat.asp;
public record TypePlaceholder(String name) implements Type {
@Override
public String toASP() {
return "tph(\""+name+"\")";
}
}

View File

@ -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();
}
}

View File

@ -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;
}
}

View File

@ -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

View File

@ -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;
}
}
}

View File

@ -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);
}
}

View File

@ -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);
}

View File

@ -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);
}
}

View File

@ -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

View File

@ -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;