stan/JavaTypeUnifyASP
1
0
Fork 0
forked from i21017/JavaTypeUnify
Code Pull Requests Activity

OL example and fix orCOnstraints

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-01 12:37:00 +02:00
parent 2887b8936d
commit af0dad2b09
1 changed files with 29 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/main/asp/unifyPaper.pl
View File

@ -1,7 +1,26 @@
% TEST INPUT
subcons(tph("_O"),type("java.lang.Object",null)).
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))).
@ -15,14 +34,16 @@ subtype(type("Vector", params(X)), type("Object", null)) :- subtype(type("Vector
% Or-Constraints
undCons(A,B) :- orCons(undCons(A,B), null).
undCons(A,B); orCons(C,D) :- orCons(undCons(A,B), orCons(C,D)).
subcons(A,B) :- undCons(subcons(A,B), _).
undCons(B,C) :- undCons(A, undCons(B, C)).
% 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
@ -85,6 +106,9 @@ equalcons(P3, PP3) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1,
%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:
@ -127,4 +151,5 @@ tphs(tph(A), params(X, type(C, P), Y)) :- tphs( params(X, type(C, P), Y)), tphs(
tphs(tph(A), params(X, Y, type(C, P))) :- tphs( params(X, Y, type(C, P))), tphs(tph(A), P).
#show sigma/2.
#show sigma/2.
#show sigma2/2.