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

Add Unify ASP prototype. Start implementing tests and Constraint -> ASP Input

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-05 20:03:18 +02:00
parent 7818722c96
commit e448d19616
4 changed files with 121 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
src/main/asp/unify.pl Normal file
View File

@ -0,0 +1,81 @@
% TEST INPUT
orCons(undCons(lessdot(type("ArrayList", params(tph(tphA))), type("List", params(type("Object", null)))), undCons(lessdot(type("List", params(tph(tphA))), tph(tphA)), null)),
undCons(lessdot(type("Object", null), type("List", null)), null)
).
lessdot(type("List", params(tph(tphA))), tph(tphA)).
%%%%%
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))).
% 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); undCons(C,D) :- orCons(undCons(A,B), undCons(C,D)).
lessdot(A,B); lessdot(C,D) :- orCons(lessdot(A,B), lessdot(C,D)).
lessdot(A,B) :- consList(lessdot(A,B), B).
consList(B,C) :- consList(A, consList(B, C)).
% undCons
lessdot(A,B) :- undCons(lessdot(A,B), _).
undCons(C,D) :- undCons(_, undCons(C,D)).
% 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)).
% 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)).
#show sigma/2.

33
src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java Normal file
View File

@ -0,0 +1,33 @@
package de.dhbwstuttgart.sat.asp;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.constraints.Pair;
import java.util.List;
import java.util.Set;
public class ASPGenerator {
public static String generateASP(List<Set<Set<Pair>>> orCons){
StringBuilder ret = new StringBuilder();
return ret.toString();
}
public static String generateOrCons(Set<Set<Pair>> undCons){
String ret = "orCons(";
for(Set<Pair> uCon : undCons){
String aspUndConstraint = generateUndCons(uCon);
ret += aspUndConstraint;
}
return ret + ").\n";
}
public static String generateUndCons(Set<Pair> undCon){
if(undCon.size() == 1){
}else {
// undCOns verschachteln
}
return "";
}
}

19
src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java
View File

@ -7,24 +7,7 @@ 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;

7
src/test/java/UnifyTest.java
View File

@ -1,3 +1,4 @@
import de.dhbwstuttgart.sat.asp.ASPGenerator;
import de.dhbwstuttgart.typeinference.constraints.Constraint;
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
import de.dhbwstuttgart.typeinference.constraints.Pair;
@ -35,6 +36,7 @@ public class UnifyTest {
return pair1;
}
/*
@Test
public void unifyTest(){
UnifyType type1;
@ -1237,7 +1239,7 @@ public class UnifyTest {
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
System.out.println(solution.size());
}
*/
@Test
public void matrixk2(){
UnifyType type1;
@ -2095,12 +2097,15 @@ public class UnifyTest {
fcConstraints.add(new UnifyPair(type1, type2, PairOperator.SMALLER));
FiniteClosure finiteClosure = new FiniteClosure(fcConstraints, new NullWriter());
/*
TypeUnify unifyAlgo = new TypeUnify();
ConstraintSet< Pair> cons = new ConstraintSet<>();
UnifyResultModelParallel urm = new UnifyResultModelParallel(cons, finiteClosure);
UnifyTaskModelParallel tasks = new UnifyTaskModelParallel();
Set<Set<UnifyPair>> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks);
System.out.println(solution.size());
*/
ASPGenerator.generateASP(undConstraints);
}
}