From e448d196168ac3c0acacffa822384f9729ea8c30 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 5 Jun 2024 20:03:18 +0200 Subject: [PATCH] Add Unify ASP prototype. Start implementing tests and Constraint -> ASP Input --- src/main/asp/unify.pl | 81 +++++++++++++++++++ .../dhbwstuttgart/sat/asp/ASPGenerator.java | 33 ++++++++ .../typeinference/constraints/Constraint.java | 19 +---- src/test/java/UnifyTest.java | 7 +- 4 files changed, 121 insertions(+), 19 deletions(-) create mode 100644 src/main/asp/unify.pl create mode 100644 src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java diff --git a/src/main/asp/unify.pl b/src/main/asp/unify.pl new file mode 100644 index 0000000..9888349 --- /dev/null +++ b/src/main/asp/unify.pl @@ -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. \ No newline at end of file diff --git a/src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java b/src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java new file mode 100644 index 0000000..8de3fcc --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java @@ -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>> orCons){ + StringBuilder ret = new StringBuilder(); + + return ret.toString(); + } + + public static String generateOrCons(Set> undCons){ + String ret = "orCons("; + for(Set uCon : undCons){ + String aspUndConstraint = generateUndCons(uCon); + ret += aspUndConstraint; + } + return ret + ").\n"; + } + + public static String generateUndCons(Set undCon){ + if(undCon.size() == 1){ + + }else { + // undCOns verschachteln + } + return ""; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java index ffac994..9e2c02c 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java @@ -7,24 +7,7 @@ import java.util.HashSet; import java.util.Set; public class Constraint extends HashSet { - 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 methodSignatureConstraint = new HashSet<>(); - - private Constraint extendConstraint = null; - - public Constraint() { - super(); - } - - public Constraint(Boolean isInherited) { - this.isInherited = isInherited; - } + public Constraint(Boolean isInherited, Constraint extendConstraint, Set methodSignatureConstraint) { this.isInherited = isInherited; diff --git a/src/test/java/UnifyTest.java b/src/test/java/UnifyTest.java index bcbd890..c5d77c3 100644 --- a/src/test/java/UnifyTest.java +++ b/src/test/java/UnifyTest.java @@ -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> 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> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks); System.out.println(solution.size()); + */ + ASPGenerator.generateASP(undConstraints); } }