From 10096cbaebc15e34f432069d788abb69a31b4a20 Mon Sep 17 00:00:00 2001 From: NoName11234 <47484268+NoName11234@users.noreply.github.com> Date: Thu, 25 Apr 2024 16:03:18 +0200 Subject: [PATCH] initial commit --- .gitignore | 31 + Makefile | 3 + README_aktuelle_Branches | 11 + pom.xml | 126 + .../exceptions/DebugException.java | 7 + .../typeinference/constraints/Constraint.java | 69 + .../constraints/ConstraintSet.java | 126 + .../typeinference/constraints/Pair.java | 13 + .../unify/GuavaSetOperations.java | 23 + .../unify/MartelliMontanariUnify.java | 108 + .../typeinference/unify/Match.java | 92 + .../typeinference/unify/RuleSet.java | 1050 +++++++ .../typeinference/unify/TypeUnify.java | 125 + .../typeinference/unify/TypeUnify2Task.java | 76 + .../typeinference/unify/TypeUnifyTask.java | 2641 +++++++++++++++++ .../unify/Unifikationsalgorithmus.java | 11 + .../typeinference/unify/UnifyResultEvent.java | 18 + .../unify/UnifyResultListener.java | 7 + .../unify/UnifyResultListenerImpl.java | 21 + .../typeinference/unify/UnifyResultModel.java | 41 + .../typeinference/unify/UnifyTaskModel.java | 18 + .../unify/distributeVariance.java | 54 + .../typeinference/unify/freshPlaceholder.java | 15 + .../unify/interfaces/IFiniteClosure.java | 68 + .../unify/interfaces/IMatch.java | 29 + .../unify/interfaces/IRuleSet.java | 103 + .../unify/interfaces/ISetOperations.java | 16 + .../unify/interfaces/IUnify.java | 35 + .../unify/interfaces/UnifyTypeVisitor.java | 23 + .../unify/model/ExtendsType.java | 96 + .../unify/model/FiniteClosure.java | 772 +++++ .../typeinference/unify/model/FunNType.java | 103 + .../typeinference/unify/model/Node.java | 118 + .../unify/model/OrderingExtend.java | 89 + .../unify/model/OrderingUnifyPair.java | 457 +++ .../unify/model/PairOperator.java | 49 + .../unify/model/PlaceholderType.java | 211 ++ .../unify/model/ReferenceType.java | 100 + .../typeinference/unify/model/SuperType.java | 88 + .../typeinference/unify/model/TypeParams.java | 191 ++ .../typeinference/unify/model/Unifier.java | 189 ++ .../typeinference/unify/model/UnifyPair.java | 247 ++ .../typeinference/unify/model/UnifyType.java | 119 + .../unify/model/WildcardType.java | 72 + .../unify/model/hashKeyType.java | 25 + .../unify/visitUnifyTypeVisitor.java | 47 + .../de/dhbwstuttgart/util/BiRelation.java | 19 + src/main/java/de/dhbwstuttgart/util/Pair.java | 25 + src/test/java/UnifyTest.java | 85 + 49 files changed, 8062 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 README_aktuelle_Branches create mode 100644 pom.xml create mode 100644 src/main/java/de/dhbwstuttgart/exceptions/DebugException.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/constraints/ConstraintSet.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/constraints/Pair.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/Match.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/Unifikationsalgorithmus.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultEvent.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListener.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListenerImpl.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultModel.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyTaskModel.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/distributeVariance.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/freshPlaceholder.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/UnifyTypeVisitor.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/FunNType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/Node.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingExtend.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/PairOperator.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/SuperType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/Unifier.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/model/hashKeyType.java create mode 100644 src/main/java/de/dhbwstuttgart/typeinference/unify/visitUnifyTypeVisitor.java create mode 100644 src/main/java/de/dhbwstuttgart/util/BiRelation.java create mode 100644 src/main/java/de/dhbwstuttgart/util/Pair.java create mode 100644 src/test/java/UnifyTest.java diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2d0d611 --- /dev/null +++ b/.gitignore @@ -0,0 +1,31 @@ +CVS +bin +*.class +*.log + +# Mobile Tools for Java (J2ME) +.mtj.tmp/ + +# Package Files # +*.jar +*.war +*.ear + +# IDEs +.classpath +*.iml +.idea/ +/target/ +.DS_Store +.project +.settings/ +/target/ + +# +manually/ + +logFiles/** +!logFiles/.gitkeep + +src/main/java/de/dhbwstuttgart/parser/antlr/ +src/main/java/de/dhbwstuttgart/sat/asp/parser/antlr/ diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..e73556a --- /dev/null +++ b/Makefile @@ -0,0 +1,3 @@ +NoOptParallel: + mvn -DskipTests package + cp target/JavaTXcompiler-0.1-jar-with-dependencies.jar target/JavaTXcompiler-0.1-jar-with-dependencies_NoOptParallel.jar diff --git a/README_aktuelle_Branches b/README_aktuelle_Branches new file mode 100644 index 0000000..5e9fc63 --- /dev/null +++ b/README_aktuelle_Branches @@ -0,0 +1,11 @@ +Stand: 24.5.21 + bigRefactoring: Master-Brach + targetBytecode: Neuer Codegenerator mit generated generics Daniel + bigRefactoringUnifyComment: Dokumentation Unify, Martin + bytecodeGenericsSecond: Generated Generics, Ali, Martin + inferWildcards, Wildcards, Till + master, derzeit nicht genutzt + plugin, eigemntlicher Branch fuer Plugin-Basis, derzeit nicht aktuelle (aktuelle Version in simplifyRes + simplifyRes, Basis fuer Plugin, sollte auf Plugin gemerged werden, noch keine Packages, Michael + strucTypesNew, Struturelle Typen, alte Basis, arbeite derzeit niemand + diff --git a/pom.xml b/pom.xml new file mode 100644 index 0000000..1470115 --- /dev/null +++ b/pom.xml @@ -0,0 +1,126 @@ + + 4.0.0 + de.dhbwstuttgart + JavaTXcompiler + jar + + 0.1 + JavaTXcompiler + http://maven.apache.org + + + junit + junit + 4.11 + test + + + + org.antlr + antlr4 + 4.11.1 + + + commons-io + commons-io + 2.6 + + + com.google.guava + guava + 22.0 + + + org.reflections + reflections + 0.9.11 + + + + org.ow2.asm + asm + 7.0 + + + + + + + org.apache.maven.plugins + maven-compiler-plugin + 3.8.0 + + --enable-preview + 21 + 21 + + + + org.antlr + antlr4-maven-plugin + 4.11.1 + + + antlr + + antlr4 + + + + + + org.apache.maven.plugins + maven-jar-plugin + + + + de.dhbwstuttgart.core.ConsoleInterface + + + + + + maven-assembly-plugin + + + package + + single + + + + + + + de.dhbwstuttgart.core.ConsoleInterface + + + + jar-with-dependencies + + + + + + + + maven-repository + file:///${project.basedir}/target + + + + 19 + 19 + de.dhbwstuttgart.core.ConsoleInterface + + + + maven-repository + MyCo Internal Repository + file:///${project.basedir}/maven-repository/ + + + diff --git a/src/main/java/de/dhbwstuttgart/exceptions/DebugException.java b/src/main/java/de/dhbwstuttgart/exceptions/DebugException.java new file mode 100644 index 0000000..559b7f1 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/exceptions/DebugException.java @@ -0,0 +1,7 @@ +package de.dhbwstuttgart.exceptions; + +public class DebugException extends RuntimeException{ + public DebugException(String message){ + System.err.println(message); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java new file mode 100644 index 0000000..ffac994 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Constraint.java @@ -0,0 +1,69 @@ +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 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; + this.extendConstraint = extendConstraint; + this.methodSignatureConstraint = methodSignatureConstraint; + } + + public void setIsInherited(Boolean isInherited) { + this.isInherited = isInherited; + } + + public Boolean isInherited() { + return isInherited; + } + + public Constraint getExtendConstraint() { + return extendConstraint; + } + + public void setExtendConstraint(Constraint c) { + extendConstraint = c; + } + + public Set getmethodSignatureConstraint() { + return methodSignatureConstraint; + } + + public void setmethodSignatureConstraint(Set c) { + methodSignatureConstraint = c; + } + + public String toString() { + return super.toString() + "\nisInherited = " + isInherited + //" + extendsContraint: " + (extendConstraint != null ? extendConstraint.toStringBase() : "null" ) + + "\n" ; + } + + public String toStringBase() { + return super.toString(); + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/constraints/ConstraintSet.java b/src/main/java/de/dhbwstuttgart/typeinference/constraints/ConstraintSet.java new file mode 100644 index 0000000..c88c12a --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/constraints/ConstraintSet.java @@ -0,0 +1,126 @@ +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 { + Constraint undConstraints = new Constraint<>(); + List>> oderConstraints = new ArrayList<>(); + + public void addUndConstraint(A p){ + undConstraints.add(p); + } + + public void addOderConstraint(Set> methodConstraints) { + oderConstraints.add(methodConstraints); + } + + public void addAllUndConstraint(Constraint allUndConstraints){ + undConstraints.addAll(allUndConstraints); + } + + public void addAllOderConstraint(List>> allOderConstraints){ + this.oderConstraints.addAll(allOderConstraints); + } + + public void addAll(ConstraintSet constraints) { + this.addAllUndConstraint(constraints.undConstraints); + this.addAllOderConstraint(constraints.oderConstraints); + } + + @Override + public String toString(){ + BinaryOperator 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>> cartesianProduct(){ + Set> toAdd = new HashSet<>(); + toAdd.add(undConstraints); + List>> allConstraints = new ArrayList<>(); + allConstraints.add(toAdd); + allConstraints.addAll(oderConstraints); + return new GuavaSetOperations().cartesianProduct(allConstraints); + } + + public ConstraintSet map(Function o) { + Hashtable,Constraint> CSA2CSB = new Hashtable<>(); + ConstraintSet ret = new ConstraintSet<>(); + ret.undConstraints = undConstraints.stream().map(o).collect(Collectors.toCollection(Constraint::new)); + List>> newOder = new ArrayList<>(); + /* + for(Set> oderConstraint : oderConstraints){ + oderConstraint.forEach(as -> { + Constraint newConst = as.stream() + .map(o) + .collect(Collectors.toCollection( + () -> new Constraint (as.isInherited()))); + CSA2CSB.put(as, newConst);} ); + } + */ + + for(Set> oderConstraint : oderConstraints){ + newOder.add( + oderConstraint.parallelStream().map((Constraint as) -> { + + Constraint newConst = as.stream() + .map(o) + .collect(Collectors.toCollection((as.getExtendConstraint() != null) + ? () -> new Constraint (as.isInherited(), + as.getExtendConstraint().stream().map(o).collect(Collectors.toCollection(Constraint::new)), + as.getmethodSignatureConstraint().stream().map(o).collect(Collectors.toCollection(HashSet::new))) + : () -> new Constraint (as.isInherited()) + )); + + //CSA2CSB.put(as, newConst); + + return newConst; + + /* + Constraint 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 c) { + undConstraints.stream().forEach(c); + for(Set> oderConstraint : oderConstraints){ + oderConstraint.parallelStream().forEach((Constraint as) -> + as.stream().forEach(c)); + } + } + + public Set getAll () { + Set ret = new HashSet<>(); + ret.addAll(undConstraints); + for(Set> oderConstraint : oderConstraints){ + oderConstraint.parallelStream().forEach((Constraint as) -> ret.addAll(as)); + } + return ret; + } + + public List>> getOderConstraints() { + return oderConstraints; + } + + public Set getUndConstraints() { + return undConstraints; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/constraints/Pair.java b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Pair.java new file mode 100644 index 0000000..cbb9899 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/constraints/Pair.java @@ -0,0 +1,13 @@ +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 diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java new file mode 100644 index 0000000..19e7c48 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java @@ -0,0 +1,23 @@ +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 Set> cartesianProduct(List> sets) { + // Wraps the call to google guava + return Sets.cartesianProduct(sets); + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java new file mode 100644 index 0000000..2fceb24 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java @@ -0,0 +1,108 @@ +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 unify(Set 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 termsList = new ArrayList(); + Iterator 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 result = new HashSet<>(); + + // f<...> = g<...> with f != g are not unifiable + if(!rhsType.getName().equals(lhsType.getName())) + return Optional.empty(); // conflict + // f = f 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); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/Match.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/Match.java new file mode 100644 index 0000000..9140661 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/Match.java @@ -0,0 +1,92 @@ +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 =. A ==> True + //A =. A ==> False + public Optional match(ArrayList 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 result = new HashSet<>(); + + // f<...> = g<...> with f != g are not unifiable + if(!rhsType.getName().equals(lhsType.getName())) + return Optional.empty(); // conflict + // f = f 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); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java new file mode 100644 index 0000000..3355975 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java @@ -0,0 +1,1050 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Optional; +import java.util.Queue; +import java.util.Set; +import java.util.Stack; +import java.util.function.Function; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.exceptions.DebugException; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +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; +import de.dhbwstuttgart.typeinference.unify.model.WildcardType; +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.unify.distributeVariance; + +import java.io.FileWriter; +import java.io.IOException; +import java.io.Writer; +import java.io.OutputStreamWriter; + +import org.apache.commons.io.output.NullOutputStream; + +/** + * Implementation of the type inference rules. + * @author Florian Steurer + * + */ +public class RuleSet implements IRuleSet{ + + Writer logFile; + + public RuleSet() { + super(); + logFile = new OutputStreamWriter(new NullOutputStream()); + } + + RuleSet(Writer logFile) { + this.logFile = logFile; + } + + @Override + public Optional reduceUp(UnifyPair pair) { + // Check if reduce up is applicable + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType rhsType = pair.getRhsType(); + if(!(rhsType instanceof SuperType)) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType)) + return Optional.empty(); + + // Rule is applicable, unpack the SuperType + return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional reduceLow(UnifyPair pair) { + // Check if rule is applicable + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + if(!(lhsType instanceof ExtendsType)) + return Optional.empty(); + + UnifyType rhsType = pair.getRhsType(); + if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType)) + return Optional.empty(); + + // Rule is applicable, unpack the ExtendsType + return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional reduceUpLow(UnifyPair pair) { + // Check if rule is applicable + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + if(!(lhsType instanceof ExtendsType)) + return Optional.empty(); + + UnifyType rhsType = pair.getRhsType(); + if(!(rhsType instanceof SuperType)) + return Optional.empty(); + + // Rule is applicable, unpack both sides + return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional> reduceExt(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType x = pair.getLhsType(); + UnifyType sTypeX; + + if(x instanceof ReferenceType) + sTypeX = x; + else if(x instanceof ExtendsType) + sTypeX = ((ExtendsType) x).getExtendedType(); + else + return Optional.empty(); + + UnifyType extY = pair.getRhsType(); + + if(!(extY instanceof ExtendsType)) + return Optional.empty(); + + if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size()) + return Optional.empty(); + + UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null); + + if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) + return Optional.empty(); + + if(x instanceof ExtendsType) + xFromFc = new ExtendsType(xFromFc); + + UnifyType extYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); + + if(extYFromFc == null || extYFromFc.getTypeParams() != xFromFc.getTypeParams()) + return Optional.empty(); + + TypeParams extYParams = extY.getTypeParams(); + TypeParams xParams = x.getTypeParams(); + + int[] pi = pi(xParams, extYParams); + + if(pi.length == 0) + return Optional.empty(); + + Set result = new HashSet<>(); + + for(int rhsIdx = 0; rhsIdx < extYParams.size(); rhsIdx++) + result.add(new UnifyPair(xParams.get(pi[rhsIdx]), extYParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + + @Override + public Optional> reduceSup(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType x = pair.getLhsType(); + UnifyType sTypeX; + + if(x instanceof ReferenceType) + sTypeX = x; + else if(x instanceof SuperType) + sTypeX = ((SuperType) x).getSuperedType(); + else + return Optional.empty(); + + UnifyType supY = pair.getRhsType(); + + if(!(supY instanceof SuperType)) + return Optional.empty(); + + if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size()) + return Optional.empty(); + + UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null); + + if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) + return Optional.empty(); + + if(x instanceof SuperType) + xFromFc = new SuperType(xFromFc); + + UnifyType supYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); + + if(supYFromFc == null || supYFromFc.getTypeParams() != xFromFc.getTypeParams()) + return Optional.empty(); + + TypeParams supYParams = supY.getTypeParams(); + TypeParams xParams = x.getTypeParams(); + Set result = new HashSet<>(); + + int[] pi = pi(xParams, supYParams); + + if(pi.length == 0) + return Optional.empty(); + + for(int rhsIdx = 0; rhsIdx < supYParams.size(); rhsIdx++) + result.add(new UnifyPair(supYParams.get(rhsIdx), xParams.get(pi[rhsIdx]), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + + @Override + public Optional> reduceEq(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + if(lhsType instanceof PlaceholderType || lhsType.getTypeParams().empty()) + return Optional.empty(); + + UnifyType rhsType = pair.getRhsType(); + + if(!rhsType.getName().equals(lhsType.getName())) + return Optional.empty(); + + if(rhsType instanceof PlaceholderType || lhsType instanceof PlaceholderType || rhsType.getTypeParams().empty()) + return Optional.empty(); + + if(rhsType.getTypeParams().size() != lhsType.getTypeParams().size()) + return Optional.empty(); + + // Keine Permutation wie im Paper nötig + Set result = new HashSet<>(); + TypeParams lhsTypeParams = lhsType.getTypeParams(); + TypeParams rhsTypeParams = rhsType.getTypeParams(); + + for(int i = 0; i < lhsTypeParams.size(); i++) + result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + + @Override + public Optional> reduce1(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType c = pair.getLhsType(); + if(!(c instanceof ReferenceType)) + return Optional.empty(); + + UnifyType d = pair.getRhsType(); + if(!(d instanceof ReferenceType)) + return Optional.empty(); + + ReferenceType lhsSType = (ReferenceType) c; + ReferenceType rhsSType = (ReferenceType) d; + + //try { + // logFile.write("PAIR Rules: " + pair + "\n"); + // logFile.flush(); + //} + //catch (IOException e) { } + + if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size()) + return Optional.empty(); + + UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null); + //2018-02-23: liefert Vector>: Das kann nicht sein. + + //NOCHMAL UEBERPRUEFEN + //PL 18-02-09 Eingfuegt Anfang + //C und D koennen auch gleich sein. + if (c.getName().equals(d.getName())) { + Set result = new HashSet<>(); + TypeParams rhsTypeParams = d.getTypeParams(); + TypeParams lhsTypeParams = c.getTypeParams(); + for(int rhsIdx = 0; rhsIdx < c.getTypeParams().size(); rhsIdx++) + result.add(new UnifyPair(lhsTypeParams.get(rhsIdx), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + //PL 18-02-09 Eingfuegt ENDE + + //try { + // logFile.write("cFromFc: " + cFromFc); + // logFile.flush(); + //} + //catch (IOException e) { } + + if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders()) + return Optional.empty(); + + UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null); + + //try { + // logFile.write("cFromFc: " + cFromFc); + // logFile.flush(); + //} + //catch (IOException e) { } + + if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size()) + return Optional.empty(); + //System.out.println("cFromFc: " + cFromFc); + //System.out.println("dFromFc: " + dFromFc); + int[] pi = pi(cFromFc.getTypeParams(), dFromFc.getTypeParams()); + + if(pi.length == 0) + return Optional.empty(); + + TypeParams rhsTypeParams = d.getTypeParams(); + TypeParams lhsTypeParams = c.getTypeParams(); + Set result = new HashSet<>(); + + for(int rhsIdx = 0; rhsIdx < rhsTypeParams.size(); rhsIdx++) + result.add(new UnifyPair(lhsTypeParams.get(pi[rhsIdx]), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + + @Override + public Optional> reduce2(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.EQUALSDOT) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + ReferenceType lhsSType; + UnifyType rhsType = pair.getRhsType(); + ReferenceType rhsSType; + + if ((lhsType instanceof ReferenceType) && (rhsType instanceof ReferenceType)) { + lhsSType = (ReferenceType) lhsType; + rhsSType = (ReferenceType) rhsType; + } + else if (((lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType)) + || ((lhsType instanceof SuperType) && (rhsType instanceof SuperType))) { + UnifyType lhsSTypeRaw = ((WildcardType) lhsType).getWildcardedType(); + UnifyType rhsSTypeRaw = ((WildcardType) rhsType).getWildcardedType(); + if ((lhsSTypeRaw instanceof ReferenceType) && (rhsSTypeRaw instanceof ReferenceType)) { + lhsSType = (ReferenceType) lhsSTypeRaw; + rhsSType = (ReferenceType) rhsSTypeRaw; + } + else + return Optional.empty(); + } + else + return Optional.empty(); + + if(lhsSType.getTypeParams().empty()) + return Optional.empty(); + + /* PL 2018-01-22 in obere Teil integriert + UnifyType rhsType = pair.getRhsType(); + ReferenceType rhsSType; + + if(rhsType instanceof ReferenceType) + rhsSType = (ReferenceType) rhsType; + else if(rhsType instanceof WildcardType) { + UnifyType rhsSTypeRaw = ((WildcardType) rhsType).getWildcardedType(); + if(rhsSTypeRaw instanceof ReferenceType) + rhsSType = (ReferenceType) rhsSTypeRaw; + else + return Optional.empty(); + } + else + return Optional.empty(); + */ + + if(!rhsSType.getName().equals(lhsSType.getName())) + return Optional.empty(); + + if(!(lhsSType.getTypeParams().size()==rhsSType.getTypeParams().size()))throw new DebugException("Fehler in Unifizierung"+ " " + lhsSType.toString() + " " + rhsSType.toString()); + //if(rhsSType.getTypeParams().size() != lhsSType.getTypeParams().size()) + // return Optional.empty(); + + Set result = new HashSet<>(); + + TypeParams rhsTypeParams = rhsSType.getTypeParams(); + TypeParams lhsTypeParams = lhsSType.getTypeParams(); + for(int i = 0; i < rhsTypeParams.size(); i++) + result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + + return Optional.of(result); + } + + @Override + public boolean erase1(UnifyPair pair, IFiniteClosure fc) { + if((pair.getPairOp() != PairOperator.SMALLERDOT) && (pair.getPairOp() != PairOperator.SMALLERNEQDOT)) + return false; + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + /* + * ty <. ? extends ty' is wrong + */ + if (rhsType instanceof ExtendsType) { + return false; + } + + /* + * ? super ty <. ty' is wrong + * except Ty' = Object or ty' = ? super Object + */ + if ((lhsType instanceof SuperType) && + (!(rhsType.equals(new ReferenceType("java.lang.Object", false)))) && + !(rhsType.equals(new SuperType (new ReferenceType("java.lang.Object", false))))) { + return false; + } + + /* + * ? extends ty <. ty' is equivalent to ty < ty' + */ + if (lhsType instanceof ExtendsType) { + lhsType = ((WildcardType)lhsType).getWildcardedType(); + } + + /* + * ty <. ? super ty' ist equivalent to ty <. ty' + */ + if (rhsType instanceof SuperType) { + rhsType = ((WildcardType)rhsType).getWildcardedType(); + } + + /* + * SMALLERNEQDOT => type must not be equal + */ + if (pair.getPairOp() == PairOperator.SMALLERNEQDOT && lhsType.equals(rhsType)){ + return false; + } + + if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType)) + return false; + + + if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType)) + return false; + + return fc.greater(lhsType, new HashSet<>()).contains(rhsType); + } + + @Override + public boolean erase2(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return false; + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + return fc.grArg(lhsType, new HashSet<>()).contains(rhsType); + } + + @Override + public boolean erase3(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.EQUALSDOT) + return false; + + return pair.getLhsType().equals(pair.getRhsType()); + } + + @Override + public Optional swap(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.EQUALSDOT) + return Optional.empty(); + + if(pair.getLhsType() instanceof PlaceholderType) + return Optional.empty(); + + if(!(pair.getRhsType() instanceof PlaceholderType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(pair.getRhsType(), pair.getLhsType(), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional adapt(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType typeD = pair.getLhsType(); + if(!(typeD instanceof ReferenceType)) + return Optional.empty(); + + UnifyType typeDs = pair.getRhsType(); + if(!(typeDs instanceof ReferenceType)) + return Optional.empty(); + + /*if(typeD.getTypeParams().size() == 0 || typeDs.getTypeParams().size() == 0) + return Optional.empty();*/ + + if(typeD.getName().equals(typeDs.getName())) + return Optional.empty(); + + + Optional opt = fc.getLeftHandedType(typeD.getName()); + if(!opt.isPresent()) + return Optional.empty(); + + // The generic Version of Type D (D) + UnifyType typeDgen = opt.get(); + + // Actually greater+ because the types are ensured to have different names + Set greater = fc.getAncestors(typeDgen); + opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); + + if(!opt.isPresent()) + return Optional.empty(); + + UnifyType newLhs = opt.get(); + + TypeParams typeDParams = typeD.getTypeParams(); + TypeParams typeDgenParams = typeDgen.getTypeParams(); + + //System.out.println("Pair: " +pair); + //System.out.println("typeD: " +typeD); + //System.out.println("typeDParams: " +typeDParams); + //System.out.println("typeDgen: " +typeD); + //System.out.println("typeDgenParams: " +typeDgenParams); + Unifier unif = Unifier.identity(); + for(int i = 0; i < typeDParams.size(); i++) { + //System.out.println("ADAPT" +typeDgenParams); + if (typeDgenParams.get(i) instanceof PlaceholderType) + unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)); + else System.out.println("ERROR"); + } + return Optional.of(new UnifyPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional adaptExt(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType typeD = pair.getLhsType(); + if(!(typeD instanceof ReferenceType) && !(typeD instanceof ExtendsType)) + return Optional.empty(); + + UnifyType typeExtDs = pair.getRhsType(); + if(!(typeExtDs instanceof ExtendsType)) + return Optional.empty(); + + if(typeD.getTypeParams().size() == 0 || typeExtDs.getTypeParams().size() == 0) + return Optional.empty(); + + UnifyType typeDgen; + if(typeD instanceof ReferenceType) + typeDgen = fc.getLeftHandedType(typeD.getName()).orElse(null); + else { + Optional opt = fc.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName()); + typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null; + } + + if(typeDgen == null) + return Optional.empty(); + + Set grArg = fc.grArg(typeDgen, new HashSet<>()); + + Optional opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny(); + + if(!opt.isPresent()) + return Optional.empty(); + + UnifyType newLhs = ((ExtendsType) opt.get()).getExtendedType(); + + TypeParams typeDParams = typeD.getTypeParams(); + TypeParams typeDgenParams = typeDgen.getTypeParams(); + + Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0)); + for(int i = 1; i < typeDParams.size(); i++) + unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)); + + return Optional.of(new UnifyPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional adaptSup(UnifyPair pair, IFiniteClosure fc) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType typeDs = pair.getLhsType(); + if(!(typeDs instanceof ReferenceType) && !(typeDs instanceof SuperType)) + return Optional.empty(); + + UnifyType typeSupD = pair.getRhsType(); + if(!(typeSupD instanceof SuperType)) + return Optional.empty(); + + if(typeDs.getTypeParams().size() == 0 || typeSupD.getTypeParams().size() == 0) + return Optional.empty(); + + + Optional opt = fc.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName()); + + if(!opt.isPresent()) + return Optional.empty(); + + UnifyType typeDgen = opt.get(); + UnifyType typeSupDgen = new SuperType(typeDgen); + + // Use of smArg instead of grArg because + // a in grArg(b) => b in smArg(a) + Set smArg = fc.smArg(typeSupDgen, new HashSet<>()); + opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); + + if(!opt.isPresent()) + return Optional.empty(); + + // New RHS + UnifyType newRhs = null; + if(typeDs instanceof ReferenceType) + newRhs = new ExtendsType(typeDs); + else + newRhs = new ExtendsType(((SuperType) typeDs).getSuperedType()); + + // New LHS + UnifyType newLhs = opt.get(); + TypeParams typeDParams = typeSupD.getTypeParams(); + TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams(); + + Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0)); + for(int i = 1; i < typeDParams.size(); i++) + unif.add((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i)); + + return Optional.of(new UnifyPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + } + + /** + * Finds the permutation pi of the type arguments of two types based on the finite closure + * @param cArgs The type which arguments are permuted + * @param dArgs The other type + * @return An array containing the values of pi for every type argument of C or an empty array if the search failed. + */ + private int[] pi(TypeParams cArgs, TypeParams dArgs) { + if(!(cArgs.size()==dArgs.size()))throw new DebugException("Fehler in Unifizierung"); + + int[] permutation = new int[dArgs.size()]; + + boolean succ = true; + for (int dArgIdx = 0; dArgIdx < dArgs.size() && succ; dArgIdx++) { + UnifyType dArg = dArgs.get(dArgIdx); + succ = false; + for (int pi = 0; pi < cArgs.size(); pi++) + if (cArgs.get(pi).getName().equals(dArg.getName())) { + permutation[dArgIdx] = pi; + succ = true; + break; + } + } + + return succ ? permutation : new int[0]; + } + + public Optional> subst(Set pairs) { + return subst(pairs, new ArrayList<>()); + } + + @Override + public Optional> subst(Set pairs, List>> oderConstraints) { + HashMap typeMap = new HashMap<>(); + + Stack occuringTypes = new Stack<>(); + + for(UnifyPair pair : pairs) { + occuringTypes.push(pair.getLhsType()); + occuringTypes.push(pair.getRhsType()); + } + + while(!occuringTypes.isEmpty()) { + UnifyType t1 = occuringTypes.pop(); + if(!typeMap.containsKey(t1)) + typeMap.put(t1, 0); + typeMap.put(t1, typeMap.get(t1)+1); + + if(t1 instanceof ExtendsType) + occuringTypes.push(((ExtendsType) t1).getExtendedType()); + if(t1 instanceof SuperType) + occuringTypes.push(((SuperType) t1).getSuperedType()); + else + t1.getTypeParams().forEach(x -> occuringTypes.push(x)); + } + Queue result1 = new LinkedList(pairs); + ArrayList result = new ArrayList(); + boolean applied = false; + + while(!result1.isEmpty()) { + UnifyPair pair = result1.poll(); + PlaceholderType lhsType = null; + UnifyType rhsType; + + if(pair.getPairOp() == PairOperator.EQUALSDOT + && pair.getLhsType() instanceof PlaceholderType) + lhsType = (PlaceholderType) pair.getLhsType(); + rhsType = pair.getRhsType(); //PL eingefuegt 2017-09-29 statt !((rhsType = pair.getRhsType()) instanceof PlaceholderType) + + if(lhsType != null + //&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType) //PL geloescht am 2017-09-29 Begründung: auch Typvariablen muessen ersetzt werden. + && typeMap.get(lhsType) > 1 // The type occurs in more pairs in the set than just the recent pair. + && !rhsType.getTypeParams().occurs(lhsType) + && !((rhsType instanceof WildcardType) && ((WildcardType)rhsType).getWildcardedType().equals(lhsType))) //PL eigefuegt 2018-02-18 + { + Unifier uni = new Unifier(lhsType, rhsType); + result = result.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(ArrayList::new)); + result1 = result1.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(LinkedList::new)); + + Function,? extends Constraint> applyUni = b -> b.stream().map( + x -> uni.apply(pair,x)).collect(Collectors.toCollection((b.getExtendConstraint() != null) + ? () -> new Constraint( + b.isInherited(), + b.getExtendConstraint().stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(Constraint::new)), + b.getmethodSignatureConstraint().stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(HashSet::new))) + : () -> new Constraint(b.isInherited()) + )); + oderConstraints.replaceAll(oc -> oc.stream().map(applyUni).collect(Collectors.toCollection(HashSet::new))); + /* + oderConstraints = oderConstraints.stream().map( + a -> a.stream().map(applyUni + //b -> b.stream().map( + // x -> uni.apply(pair,x)).collect(Collectors.toCollection(HashSet::new) ) + ).collect(Collectors.toCollection(HashSet::new)) + ).collect(Collectors.toList(ArrayList::new)); + } + */ + applied = true; + } + result.add(pair); + } + + return applied ? Optional.of(new HashSet<>(result)) : Optional.empty(); + } + + @Override + public Optional reduceWildcardLow(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof ExtendsType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional reduceWildcardLowRight(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof ExtendsType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional reduceWildcardUp(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof SuperType) || !(rhsType instanceof SuperType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), ((SuperType) lhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional reduceWildcardUpRight(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof SuperType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), lhsType, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair())); + } + + /* PL 2018-03-06 auskommentiert sind mutmaßlich falsch + * vgl. JAVA_BSP/Wildcard6.java + @Override + public Optional reduceWildcardLowUp(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof SuperType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((SuperType) rhsType).getSuperedType(), PairOperator.EQUALSDOT)); + } + + @Override + public Optional reduceWildcardUpLow(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof SuperType) || !(rhsType instanceof ExtendsType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(((SuperType) lhsType).getSuperedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT)); + } + + + @Override + public Optional reduceWildcardLeft(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType rhsType = pair.getRhsType(); + if(!(rhsType instanceof ReferenceType)) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + + if(lhsType instanceof WildcardType) + return Optional.of(new UnifyPair(((WildcardType) lhsType).getWildcardedType(), rhsType, PairOperator.EQUALSDOT)); + + return Optional.empty(); + } + */ + @Override + public Optional> reduceFunN(UnifyPair pair) { + if((pair.getPairOp() != PairOperator.SMALLERDOT) + && (pair.getPairOp() != PairOperator.EQUALSDOT)) //PL 2017-10-03 hinzugefuegt + //da Regel auch fuer EQUALSDOT anwendbar + //TODO: fuer allen anderen Relationen noch pruefen + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + if(!(lhsType instanceof FunNType) || !(rhsType instanceof FunNType)) + return Optional.empty(); + + FunNType funNLhsType = (FunNType) lhsType; + FunNType funNRhsType = (FunNType) rhsType; + + if(funNLhsType.getN() != funNRhsType.getN()) + return Optional.empty(); + + Set result = new HashSet(); + if (pair.getPairOp() == PairOperator.SMALLERDOT) { + result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) { + result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + } + else {// pair.getPairOp() == PairOperator.EQUALDOT + result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) { + result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + } + } + result.stream().forEach(x -> { UnifyType l = x.getLhsType(); + if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } + UnifyType r = x.getRhsType(); + if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); } + } ); + try { + logFile.write("FUNgreater: " + pair + "\n"); + logFile.write("FUNred: " + result + "\n"); + logFile.flush(); + } + catch (IOException e) { + System.out.println("logFile-Error"); + } + return Optional.of(result); + } + + + @Override + public Optional> greaterFunN(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + if(!(lhsType instanceof FunNType) || !(rhsType instanceof PlaceholderType)) + return Optional.empty(); + + FunNType funNLhsType = (FunNType) lhsType; + + Set result = new HashSet(); + + Integer variance = ((PlaceholderType)rhsType).getVariance(); + Integer inversVariance = distributeVariance.inverseVariance(variance); + + UnifyType[] freshPlaceholders = new UnifyType[funNLhsType.getTypeParams().size()]; + for(int i = 0; i < freshPlaceholders.length-1; i++) { + freshPlaceholders[i] = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance); + } + freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance); + result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), freshPlaceholders[funNLhsType.getTypeParams().size()-1], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + + for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) { + result.add(new UnifyPair(freshPlaceholders[i], funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + result.add(new UnifyPair(rhsType, funNLhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + + result.stream().forEach(x -> { UnifyType l = x.getLhsType(); + if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } + UnifyType r = x.getRhsType(); + if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); } + } ); + try { + logFile.write("FUNgreater: " + pair + "\n"); + logFile.write("FUNgreater: " + result + "\n"); + logFile.flush(); + } + catch (IOException e) { + System.out.println("lofFile-Error"); + } + return Optional.of(result); + } + + @Override + public Optional> smallerFunN(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOT) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof FunNType)) + return Optional.empty(); + + FunNType funNRhsType = (FunNType) rhsType; + + Set result = new HashSet(); + + Integer variance = ((PlaceholderType)lhsType).getVariance(); + Integer inversVariance = distributeVariance.inverseVariance(variance); + + UnifyType[] freshPlaceholders = new UnifyType[funNRhsType.getTypeParams().size()]; + for(int i = 0; i < freshPlaceholders.length-1; i++) { + freshPlaceholders[i] = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance); + } + freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance); + + result.add(new UnifyPair(freshPlaceholders[funNRhsType.getTypeParams().size()-1], funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + + for(int i = 0; i < funNRhsType.getTypeParams().size()-1; i++) { + result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), freshPlaceholders[i], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + result.add(new UnifyPair(lhsType, funNRhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + + result.stream().forEach(x -> { UnifyType l = x.getLhsType(); + if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); } + UnifyType r = x.getRhsType(); + if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); } + } ); + try { + logFile.write("FUNgreater: " + pair + "\n"); + logFile.write("FUNsmaller: " + result + "\n"); + logFile.flush(); + } + catch (IOException e) { + System.out.println("lofFile-Error"); + } + return Optional.of(result); + } + + @Override + public Optional reduceTph(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof ReferenceType)) + return Optional.empty(); + + return Optional.of(new UnifyPair(lhsType, rhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + } + + @Override + public Optional> reduceTphExt(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof PlaceholderType)) + return Optional.empty(); + + UnifyType extendedType = ((ExtendsType)lhsType).getExtendedType(); + + if (extendedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? extends a <.? a + + boolean isGen = extendedType instanceof PlaceholderType && !((PlaceholderType) extendedType).isGenerated(); + + Set result = new HashSet<>(); + if(isGen) + result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + else { + UnifyType freshTph = PlaceholderType.freshPlaceholder(); + result.add(new UnifyPair(rhsType, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + result.add(new UnifyPair(extendedType, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); + } + + return Optional.of(result); + } + + @Override + public Optional> reduceTphSup(UnifyPair pair) { + if(pair.getPairOp() != PairOperator.SMALLERDOTWC) + return Optional.empty(); + + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + if(!(lhsType instanceof SuperType) || !(rhsType instanceof PlaceholderType)) + return Optional.empty(); + + UnifyType superedType = ((SuperType)lhsType).getSuperedType(); + + if (superedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? super a <.? a + + boolean isGen = superedType instanceof PlaceholderType && !((PlaceholderType) superedType).isGenerated(); + + Set result = new HashSet<>(); + if(isGen) + result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + else { + UnifyType freshTph = PlaceholderType.freshPlaceholder(); + result.add(new UnifyPair(rhsType, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair())); + Set fBounded = pair.getfBounded(); + fBounded.add(lhsType); + result.add(new UnifyPair(freshTph, superedType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair(), fBounded)); + } + + return Optional.of(result); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java new file mode 100644 index 0000000..a011aa9 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -0,0 +1,125 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.io.FileWriter; +import java.io.IOException; +import java.io.Writer; +import java.util.ArrayList; +import java.util.List; +import java.util.Set; +import java.util.concurrent.ForkJoinPool; + +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; +import de.dhbwstuttgart.typeinference.constraints.Pair; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure; +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> unify(Set undConstrains, List>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) { + TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks); + ForkJoinPool pool = new ForkJoinPool(); + pool.invoke(unifyTask); + Set> 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 UnifyResultModel unifyAsync(Set undConstrains, List>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) { + TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks); + ForkJoinPool pool = new ForkJoinPool(); + 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 UnifyResultModel unifyParallel(Set undConstrains, List>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) { + TypeUnifyTask unifyTask = //new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks); + new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, usedTasks, statistics); + ForkJoinPool pool = new ForkJoinPool(); + pool.invoke(unifyTask); + Set> 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; + } + + /* + public Set> unifySequential(Set eq, IFiniteClosure fc, FileWriter logFile, Boolean log) { + TypeUnifyTask unifyTask = new TypeUnifyTask(eq, fc, false, logFile, log); + Set> res = unifyTask.compute(); + return res; + } + */ + + /** + * unify sequentiell mit oderconstraints + * @param undConstrains + * @param oderConstraints + * @param fc + * @param logFile + * @param log + * @param cons + * @return + */ + public Set> unifyOderConstraints(Set undConstrains, List>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret, UnifyTaskModel usedTasks) { + TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, ret, usedTasks); + unifyTask.statistics = statistics; + Set> res = unifyTask.compute(); + try { + logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n"); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no log-File"); + } + return res; + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java new file mode 100644 index 0000000..61d6ce8 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java @@ -0,0 +1,76 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.io.FileWriter; +import java.io.IOException; +import java.io.Writer; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; +import de.dhbwstuttgart.typeinference.constraints.Pair; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +public class TypeUnify2Task extends TypeUnifyTask { + + Set> setToFlatten; + Set methodSignatureConstraintUebergabe; + + //statistics + TypeUnify2Task(Set> setToFlatten, Set eq, + List>> oderConstraints, + Set nextSetElement, + IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks, + Set methodSignatureConstraintUebergabe, Writer statistics) { + this(setToFlatten, eq, oderConstraints, nextSetElement, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraintUebergabe ); + + } + + public TypeUnify2Task(Set> setToFlatten, Set eq, List>> oderConstraints, Set nextSetElement, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks, Set methodSignatureConstraintUebergabe) { + super(eq, oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); + this.setToFlatten = setToFlatten; + this.nextSetElement = nextSetElement; + this.methodSignatureConstraintUebergabe = methodSignatureConstraintUebergabe; + } + + Set getNextSetElement() { + return nextSetElement; + } + + @Override + protected Set> compute() { + if (one) { + System.out.println("two"); + } + one = true; + Set> res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField, methodSignatureConstraintUebergabe); + /*if (isUndefinedPairSetSet(res)) { + return new HashSet<>(); } + else + */ + //writeLog("xxx"); + //noOfThread--; + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + else { + return res; + } + } + } + + public void closeLogFile() { + + try { + logFile.close(); + } + catch (IOException ioE) { + System.err.println("no log-File" + thNo); + } + + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java new file mode 100644 index 0000000..ff9e6cd --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -0,0 +1,2641 @@ +//PL 2018-12-19: Merge checken +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedHashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Map.Entry; +import java.util.Optional; +import java.util.Set; +import java.util.concurrent.RecursiveTask; +import java.util.function.BiFunction; +import java.util.function.BinaryOperator; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import de.dhbwstuttgart.exceptions.DebugException; +import org.apache.commons.io.output.NullOutputStream; + +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IMatch; +import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; +import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.OrderingExtend; +import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +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; +import de.dhbwstuttgart.typeinference.unify.model.WildcardType; +import de.dhbwstuttgart.util.Pair; +import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair; + +import java.io.File; +import java.io.FileWriter; +import java.io.IOException; +import java.io.OutputStreamWriter; +import java.io.Writer; + +import com.google.common.collect.Ordering; +import org.apache.commons.io.output.NullWriter; + + +/** + * Implementation of the type unification algorithm + * @author Florian Steurer + */ +public class TypeUnifyTask extends RecursiveTask>> { + + private static final long serialVersionUID = 1L; + private static int i = 0; + private boolean printtag = false; + Boolean log = true; //gibt an ob ein Log-File nach System.getProperty("user.dir")+"/test/logFiles/log" geschrieben werden soll? + + /** + * Element, das aus dem nextSet den Gleichunen dieses Threads hinzugefuegt wurde + */ + Set nextSetElement; + + /** + * Fuer die Threads + */ + UnifyResultModel urm; + protected static int noOfThread = 0; + private static int totalnoOfThread = 0; + int thNo; + protected boolean one = false; + Integer MaxNoOfThreads = 128; + + public static final String rootDirectory = System.getProperty("user.dir")+"/test/logFiles/"; + Writer logFile; + + /** + * The implementation of setOps that will be used during the unification + */ + protected ISetOperations setOps = new GuavaSetOperations(); + + /** + * The implementation of the standard unify that will be used during the unification + */ + protected IUnify stdUnify = new MartelliMontanariUnify(); + + /** + * The implementation of the rules that will be used during the unification. + */ + protected IRuleSet rules; + + protected Set eq; //und-constraints + + protected List>> oderConstraintsField; + + protected IFiniteClosure fc; + + protected OrderingExtend> oup; + + protected boolean parallel; + + //Gives if unify is not called from checkA + private boolean finalresult = true; + + int rekTiefeField; + + Integer nOfUnify = 0; + + Integer noUndefPair = 0; + + Integer noAllErasedElements = 0; + + static Integer noou = 0; + + static int noBacktracking; + + static int noLoop; + + static Integer noShortendElements = 0; + + Boolean myIsCanceled = false; + + volatile UnifyTaskModel usedTasks; + + static Writer statistics; + + public TypeUnifyTask() { + rules = new RuleSet(); + } + + /* + public TypeUnifyTask(Set eq, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log) { + this.eq = eq; + this.fc = fc; + this.oup = new OrderingUnifyPair(fc); + this.parallel = parallel; + this.logFile = logFile; + this.log = log; + rules = new RuleSet(logFile); + noOfThread++; + thNo = noOfThread; + } + */ + + //statistics + public TypeUnifyTask(Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks, Writer statistics) { + this(eq,oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); + this.statistics = statistics; + } + public TypeUnifyTask(Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks) { + synchronized (this) { + if(statistics==null){ + statistics = new NullWriter(); + } + this.eq = eq; + //this.oderConstraints = oderConstraints.stream().map(x -> x.stream().map(y -> new HashSet<>(y)).collect(Collectors.toSet(HashSet::new))).collect(Collectors.toList(ArrayList::new)); + this.oderConstraintsField = oderConstraints; /*.stream().map(x -> { + Set> ret = new HashSet<>(); + for (Constraint y : x) { + ret.add(new HashSet<>(y)); + } + return ret; + }).collect(Collectors.toCollection(ArrayList::new)); + */ + + //x.stream().map(y -> new HashSet<>(y)).collect(Collectors.toSet(HashSet::new))).collect(Collectors.toList(ArrayList::new)); + this.nextSetElement = nextSetElement; + this.fc = fc; + this.oup = new OrderingUnifyPair(fc); + this.parallel = parallel; + this.logFile = logFile; + this.log = log; + + noOfThread++; + totalnoOfThread++; + //writeLog("thNo1 " + thNo); + thNo = totalnoOfThread; + writeLog("thNo2 " + thNo); + try { + this.logFile = log ? new FileWriter(new File(System.getProperty("user.dir") + "/logFiles/" + "Thread_"+thNo)) + : new OutputStreamWriter(new NullOutputStream()); + logFile.write(""); + } + catch (IOException e) { + System.err.println("log-File nicht vorhanden"); + } + /*Abbruchtest + if (thNo > 10) { + System.out.println("cancel"); + usedTasks.cancel(); + writeLog(nOfUnify.toString() + "cancel"); + System.out.println("cancel"); + try { + logFile.write("Abbruch"); + } + catch (IOException e) { + System.err.println("log-File nicht vorhanden"); + } + } + */ + rules = new RuleSet(logFile); + this.rekTiefeField = rekTiefe; + this.urm = urm; + this.usedTasks = usedTasks; + this.usedTasks.add(this); + } + } + + /** + * Vererbt alle Variancen + * @param eq The set of constraints + */ + /* PL 2018-05- 17 verschoben nach JavaTXCompiler + private void varianceInheritance(Set eq) { + Set usedTPH = new HashSet<>(); + Set phSet = eq.stream().map(x -> { + Set pair = new HashSet<>(); + if (x.getLhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getLhsType()); + if (x.getRhsType() instanceof PlaceholderType) pair.add((PlaceholderType)x.getRhsType()); + return pair; + }).reduce(new HashSet<>(), (a,b) -> { a.addAll(b); return a;} , (c,d) -> { c.addAll(d); return c;}); + + ArrayList phSetVariance = new ArrayList<>(phSet); + phSetVariance.removeIf(x -> (x.getVariance() == 0)); + while(!phSetVariance.isEmpty()) { + PlaceholderType a = phSetVariance.remove(0); + usedTPH.add(a); + //HashMap ht = new HashMap<>(); + //ht.put(a, a.getVariance()); + Set eq1 = new HashSet<>(eq); + eq1.removeIf(x -> !(x.getLhsType() instanceof PlaceholderType && ((PlaceholderType)x.getLhsType()).equals(a))); + eq1.stream().forEach(x -> { x.getRhsType().accept(new distributeVariance(), a.getVariance());}); + eq1 = new HashSet<>(eq); + eq1.removeIf(x -> !(x.getRhsType() instanceof PlaceholderType && ((PlaceholderType)x.getRhsType()).equals(a))); + eq1.stream().forEach(x -> { x.getLhsType().accept(new distributeVariance(), a.getVariance());}); + phSetVariance = new ArrayList<>(phSet); + phSetVariance.removeIf(x -> (x.getVariance() == 0 || usedTPH.contains(x))); + } +} +*/ + void myCancel(Boolean b) { + myIsCanceled = true; + } + + public boolean myIsCancelled() { + return myIsCanceled; + } + + protected Set> compute() { + if (one) { + //System.out.println("two"); + } + one = true; + Set neweq = new HashSet<>(eq); + /* 1-elementige Oder-Constraints werden in und-Constraints umgewandelt */ + oderConstraintsField.stream() + .filter(x -> x.size()==1) + .map(y -> y.stream().findFirst().get()).forEach(x -> neweq.addAll(x)); + ArrayList>> remainingOderconstraints = oderConstraintsField.stream() + .filter(x -> x.size()>1) + .collect(Collectors.toCollection(ArrayList::new)); + Set> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField, new HashSet<>()); + noOfThread--; + try { + logFile.close(); + } + catch (IOException ioE) { + System.err.println("no log-File"); + } + if (isUndefinedPairSetSet(res)) { + //fuer debug-Zwecke + ArrayList al = res.stream().map(x -> x.stream().collect(Collectors.toCollection(ArrayList::new))) + .collect(Collectors.toCollection(ArrayList::new)); + throw new DebugException("Unresolved constraints: " + res.toString()); //return new HashSet<>(); + } + else { + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + else { + return res; + } + } + } + } +/* + @Override + protected Set> compute() { + Set> fstElems = new HashSet<>(); + fstElems.add(eq); + Set> res = computeCartesianRecursiveOderConstraints(fstElems, oderConstraints, fc, parallel); + if (isUndefinedPairSetSet(res)) { return new HashSet<>(); } + else return res; + } +*/ + + + + + /** + * Computes all principal type unifiers for a set of constraints. + * @param eq The set of constraints + * @param fc The finite closure + * @return The set of all principal type unifiers + */ + protected Set> unify(final Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set methodSignatureConstraint) { + //Set aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT) + // ).collect(Collectors.toCollection(HashSet::new)); + //writeLog(nOfUnify.toString() + " AA: " + aas.toString()); + //if (aas.isEmpty()) { + // System.out.println(""); + //} + + //.collect(Collectors.toCollection(HashSet::new))); + + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + + rekTiefe++; + nOfUnify++; + writeLog(nOfUnify.toString() + " Unifikation: " + eq.toString()); + writeLog(nOfUnify.toString() + " Oderconstraints: " + oderConstraints.toString()); + + /* + * Variancen auf alle Gleichungen vererben + */ + //PL 2018-05-17 nach JavaTXCompiler verschoben + //varianceInheritance(eq); + + /* + * ? extends ? extends Theta rausfiltern + */ + Set doubleExt = eq.stream().filter(x -> (x.wrongWildcard())).map(x -> { x.setUndefinedPair(); return x;}) + .collect(Collectors.toCollection(HashSet::new)); + if (doubleExt.size() > 0) { + Set> ret = new HashSet<>(); + ret.add(doubleExt); + return ret; + } + + /* + * Occurs-Check durchfuehren + */ + + Set ocurrPairs = eq.stream().filter(x -> { + UnifyType lhs, rhs; + return (lhs = x.getLhsType()) instanceof PlaceholderType + && !((rhs = x.getRhsType()) instanceof PlaceholderType) + && rhs.getTypeParams().occurs((PlaceholderType)lhs);}) + .map(x -> { x.setUndefinedPair(); return x;}) + .collect(Collectors.toCollection(HashSet::new)); + writeLog("ocurrPairs: " + ocurrPairs); + if (ocurrPairs.size() > 0) { + Set> ret = new HashSet<>(); + ret.add(ocurrPairs); + return ret; + } + + + + /* + * Step 1: Repeated application of reduce, adapt, erase, swap + */ + Set eq0; + Set eq0Prime; + Optional> eqSubst = Optional.of(eq); + do { + eq0Prime = eqSubst.get(); + eq0 = applyTypeUnificationRules(eq0Prime, fc); + eqSubst = rules.subst(eq0, oderConstraints); + } while (eqSubst.isPresent()); + + eq0.forEach(x -> x.disableCondWildcards()); + + writeLog(nOfUnify.toString() + " Unifikation nach applyTypeUnificationRules: " + eq.toString()); + writeLog(nOfUnify.toString() + " Oderconstraints nach applyTypeUnificationRules: " + oderConstraints.toString()); + + /* + * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs + */ + Set eq1s = new HashSet<>(); + Set eq2s = new HashSet<>(); + splitEq(eq0, eq1s, eq2s); + + /* + * Step 4: Create possible typings + * + * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) + * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia + */ + + // There are up to 10 toplevel set. 8 of 10 are the result of the + // cartesian product of the sets created by pattern matching. + List>> topLevelSets = new ArrayList<>(); + + //System.out.println(eq2s); + + if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. + Set> wrap = new HashSet<>(); + wrap.add(eq1s); + topLevelSets.add(wrap); // Add Eq1' + } + + // Add the set of [a =. Theta | (a=. Theta) in Eq2'] + //TODO: Occurscheck anwenden als Fehler identifizieren + Set bufferSet = eq2s.stream() + .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) + .collect(Collectors.toSet()); + + if(bufferSet.size() != 0) { // Do not add empty sets or the cartesian product will always be empty. + Set> wrap = new HashSet<>(); + wrap.add(bufferSet); + topLevelSets.add(wrap); + eq2s.removeAll(bufferSet); + } + + // Sets that originate from pair pattern matching + // Sets of the "second level" + Set undefinedPairs = new HashSet<>(); + if (printtag) System.out.println("eq2s " + eq2s); + //writeLog("BufferSet: " + bufferSet.toString()+"\n"); + List>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints); + Set>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput); + //PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer + //nicht ausgewertet Faculty Beispiel im 1. Schritt + //PL 2017-10-03 geloest, muesste noch mit FCs mit kleineren + //Typen getestet werden. + writeLog(nOfUnify.toString() + " Oderconstraints2: " + oderConstraintsOutput.toString()); + if (printtag) System.out.println("secondLevelSets:" +secondLevelSets); + // If pairs occured that did not match one of the cartesian product cases, + // those pairs are contradictory and the unification is impossible. + if(!undefinedPairs.isEmpty()) { + noUndefPair++; + for (UnifyPair up : undefinedPairs) { + writeLog(noUndefPair.toString() + " UndefinedPairs; " + up); + writeLog("BasePair; " + up.getBasePair()); + } + Set> error = new HashSet<>(); + undefinedPairs = undefinedPairs.stream().map(x -> { x.setUndefinedPair(); return x;}).collect(Collectors.toCollection(HashSet::new)); + error.add(undefinedPairs); + undefinedPairs.forEach(x -> writeLog("AllSubst: " +x.getAllSubstitutions().toString())); + return error; + } + + /* Up to here, no cartesian products are calculated. + * filters for pairs and sets can be applied here */ + + // Alternative: Sub cartesian products of the second level (pattern matched) sets + // "the big (x)" + /* for(Set>> secondLevelSet : secondLevelSets) { + //System.out.println("secondLevelSet "+secondLevelSet.size()); + List>> secondLevelSetList = new ArrayList<>(secondLevelSet); + Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); + //System.out.println("CardResult: "+cartResult.size()); + // Flatten and add to top level sets + Set> flat = new HashSet<>(); + int j = 0; + for(List> s : cartResult) { + j++; + //System.out.println("s from CardResult: "+cartResult.size() + " " + j); + Set flat1 = new HashSet<>(); + for(Set s1 : s) + flat1.addAll(s1); + flat.add(flat1); + } + //topLevelSets.add(flat); + } + */ + + //Alternative KEIN KARTESISCHES PRODUKT der secondlevel Ebene bilden + for(Set>> secondLevelSet : secondLevelSets) { + for (Set> secondlevelelem : secondLevelSet) { + topLevelSets.add(secondlevelelem); + } + } + //System.out.println(topLevelSets); + //System.out.println(); + + + //Aufruf von computeCartesianRecursive ANFANG + //writeLog("topLevelSets: " + topLevelSets.toString()); + return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, methodSignatureConstraint); + + } + + + Set> unify2(Set> setToFlatten, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set methodSignatureConstraint) { + //Aufruf von computeCartesianRecursive ENDE + + //keine Ahnung woher das kommt + //Set> setToFlatten = topLevelSets.stream().map(x -> x.iterator().next()).collect(Collectors.toCollection(HashSet::new)); + + //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG + // Cartesian product over all (up to 10) top level sets + //Set>> eqPrimeSet = setOps.cartesianProduct(topLevelSets) + // .stream().map(x -> new HashSet<>(x)) + // .collect(Collectors.toCollection(HashSet::new)); + //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE + + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + + Set> eqPrimePrimeSet = new HashSet<>(); + + Set forks = new HashSet<>(); + + //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG + //for(Set> setToFlatten : eqPrimeSet) { + // Flatten the cartesian product + //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE + Set eqPrime = new HashSet<>(); + setToFlatten.stream().forEach(x -> eqPrime.addAll(x)); + + /* + * Step 5: Substitution + */ + //writeLog("vor Subst: " + eqPrime); + writeLog("vor Subst: " + oderConstraints); + String ocString = oderConstraints.toString(); + List>> newOderConstraints = new ArrayList<>(oderConstraints); + Optional> eqPrimePrime = rules.subst(eqPrime, newOderConstraints); + Set> unifyres1 = null; + Set> unifyres2 = null; + if (!ocString.equals(newOderConstraints.toString())) writeLog("nach Subst: " + newOderConstraints); + //writeLog("nach Subst: " + eqPrimePrime); + /* + * Step 6 a) Restart (fork) for pairs where subst was applied + */ + /* + if(parallel) { + if (eqPrime.equals(eq) && !eqPrimePrime.isPresent() + && oderConstraints.isEmpty()) //PL 2017-09-29 //(!eqPrimePrime.isPresent()) auskommentiert und durch + //PL 2017-09-29 dies ersetzt //(!eqPrimePrime.isPresent()) + //PL 2018-05-18 beide Bedingungen muessen gelten, da eqPrime Veränderungen in allem ausser subst + //eqPrimePrime Veraenderungen in subst repraesentieren. + eqPrimePrimeSet.add(eqPrime); + else if(eqPrimePrime.isPresent()) { + //System.out.println("nextStep: " + eqPrimePrime.get()); + TypeUnifyTask fork = new TypeUnifyTask(eqPrimePrime.get(), fc, true, logFile, log); + forks.add(fork); + fork.fork(); + } + else { + //System.out.println("nextStep: " + eqPrime); + TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc, true, logFile, log); + forks.add(fork); + fork.fork(); + } + } + else */ + {// sequentiell (Step 6b is included) + if (printtag) System.out.println("nextStep: " + eqPrimePrime); + if (eqPrime.equals(eq) && !eqPrimePrime.isPresent() + && oderConstraints.isEmpty()) { //PL 2017-09-29 //(!eqPrimePrime.isPresent()) auskommentiert und durch + //PL 2017-09-29 dies ersetzt //(!eqPrimePrime.isPresent()) + //PL 2018-05-18 beide Bedingungen muessen gelten, da eqPrime Veränderungen in allem ausser subst + //eqPrimePrime Veraenderungen in subst repraesentieren. + //try { + //if (isSolvedForm(eqPrime)) { + // writeLog("eqPrime:" + eqPrime.toString()+"\n"); + //} + //} + //catch (IOException e) { + // System.err.println("log-File nicht vorhanden"); + //} + eqPrimePrimeSet.add(eqPrime); + if (finalresult && isSolvedForm(eqPrime)) { + writeLog("eqPrime:" + eqPrime.toString()+"\n"); + + /* methodconstraintsets werden zum Ergebnis hinzugefuegt + * Anfang + */ + //System.out.println("methodSignatureConstraint Return: " + methodSignatureConstraint); + eqPrimePrimeSet.forEach(x -> x.addAll(methodSignatureConstraint)); + + //Substitutionen in methodcontraintsets werdne ausgeführt + eqPrimePrimeSet = eqPrimePrimeSet.stream().map( + x -> { Optional> help = rules.subst(x); + return help.isPresent() ? + help.get(): + x; }).collect(Collectors.toSet()); + /* + * Ende + */ + + + urm.notify(eqPrimePrimeSet); + writeStatistics("Result: " + eqPrimePrimeSet.toString()); + } + } + else if(eqPrimePrime.isPresent()) { + Set> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint); + + eqPrimePrimeSet.addAll(unifyres); + } + else { + Set> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint); + + + eqPrimePrimeSet.addAll(unifyres); + } + } + //Muss auskommentiert werden, wenn computeCartesianRecursive ANFANG + //} + //Muss auskommentiert werden, wenn computeCartesianRecursive ENDE + + /* + * Step 6 b) Build the union over everything. + */ + /* + * PL 2019-01-22: geloescht + + if(parallel) + for(TypeUnifyTask fork : forks) + eqPrimePrimeSet.addAll(fork.join()); + */ + /* + * Step 7: Filter empty sets; + */ + eqPrimePrimeSet = eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x) || this.isUndefinedPairSet(x)).collect(Collectors.toCollection(HashSet::new)); + if (!eqPrimePrimeSet.isEmpty() && !isUndefinedPairSetSet(eqPrimePrimeSet)) { + writeLog("Result1 " + eqPrimePrimeSet.toString()); + } + return eqPrimePrimeSet; + } + + + /** + * Computes the cartesian product of topLevelSets step by step. + * @param topLevelSets List of Sets of Sets, where a cartesian product have to be built + * Ex.: [{{a =. Integer}, {a = Object}}, {{a = Vector, b =. Integer}, {a = Vector, b =. Object}}] + * @param eq Original set of equations which should be unified + * @param oderConstraints Remaining or-constraints + * @param fc The finite closure + * @param parallel If the algorithm should be parallelized run + * @param rekTiefe Deep of recursive calls + * @return The set of all principal type unifiers + */ + Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set methodSignatureConstraint) { + + //oneElems: Alle 1-elementigen Mengen, die nur ein Paar + //a <. theta, theta <. a oder a =. theta enthalten + + //statistics + //writeStatistics("\nNumber of Constraints (" + rekTiefe + "): " + topLevelSets.size()); + + Set> oneElems = new HashSet<>(); + oneElems.addAll(topLevelSets.stream() + .filter(x -> x.size()==1) + .map(y -> y.stream().findFirst().get()) + .collect(Collectors.toCollection(HashSet::new))); + + //optNextSet: Eine mehrelementige Menge, wenn vorhanden + Optional>> optNextSet = topLevelSets.stream().filter(x -> x.size()>1).findAny(); + + if (!optNextSet.isPresent()) {//Alle Elemente sind 1-elementig + Set> result = unify2(oneElems, eq, oderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint); + return result; + } + + Set> nextSet = optNextSet.get(); + //writeLog("nextSet: " + nextSet.toString()); + List> nextSetasList =new ArrayList<>(nextSet); + + //writeStatistics(" Start Number of elements ( " /* + nextSetasList.get(0).stream().findFirst().get().getBasePair()*/ +"): (" + rekTiefe + "): " + nextSetasList.size()); + + /* + try { + //List> + //nextSetasList = oup.sortedCopy(nextSet);//new ArrayList<>(nextSet); + } + catch (java.lang.IllegalArgumentException e) { + System.out.print(""); + } + */ + Set> result = new HashSet<>(); + int variance = 0; + + /* Varianzbestimmung Anfang + * Oderconstraint, wenn entweder kein Basepair oder unterschiedliche Basepairs => oderConstraint = true; + * Varianz = 1 => Argumentvariable + * Varianz = -1 => Rückgabevariable + * Varianz = 0 => unklar + * Varianz = 2 => Operatoren oderConstraints */ + ArrayList zeroNextElem = new ArrayList<>(nextSetasList.get(0)); + UnifyPair fstBasePair = zeroNextElem.remove(0).getBasePair(); + Boolean oderConstraint = false; + + if (fstBasePair != null) { + Boolean sameBase = true; + for (UnifyPair ele : nextSetasList.get(0)) {//check ob a <. ty base oder ob Ueberladung + sameBase = sameBase && ele.getBasePair() != null && ele.getBasePair().equals(fstBasePair); + } + if (sameBase) { //angefuegt PL 2020-02-30 + Optional xi = nextSetasList.stream().map(x -> x.stream().filter(y -> (y.getLhsType() instanceof PlaceholderType && !(y.getRhsType() instanceof PlaceholderType))) + .filter(z -> ((PlaceholderType)z.getLhsType()).getVariance() != 0) + .map(c -> ((PlaceholderType)c.getLhsType()).getVariance()) + .reduce((a,b)-> {if (a==b) return a; else return 0; })) //2 kommt insbesondere bei Oder-Constraints vor + .filter(d -> d.isPresent()) + .map(e -> e.get()) + .findAny(); + if (xi.isPresent()) { + variance = xi.get(); + } + } + else { + oderConstraint = true; + } + } + else { + oderConstraint = true; + } + + //Varianz-Bestimmung Oder-Constraints + if (oderConstraint) { + if (printtag) System.out.println("nextSetasList " + nextSetasList); + Optional optVariance = + nextSetasList.iterator() + .next() + .stream() + .filter(x -> x.getGroundBasePair().getLhsType() instanceof PlaceholderType && + ! (x.getRhsType() instanceof PlaceholderType) && + x.getPairOp() == PairOperator.EQUALSDOT) + .map(x -> + ((PlaceholderType)x.getGroundBasePair().getLhsType()).getVariance()) + .reduce((n,m) -> { if ((n == 0) && (m==0)) return 0; + else if (n !=0) return n; //es muss mindestens eine Variance != 0 sein + else return m; + }); + //Fuer Operatorenaufrufe wird variance auf 2 gesetzt. + //da kein Receiver existiert also kein x.getGroundBasePair().getLhsType() instanceof PlaceholderType + //Bei Varianz = 2 werden alle Elemente des Kartesischen Produkts abgearbeitet + variance = optVariance.isPresent() ? optVariance.get() : 2; + } + /* Varianzbestimmung Ende */ + + //writeLog("nextSetasList: " + nextSetasList.toString()); + Set nextSetElem = nextSetasList.get(0); + //writeLog("BasePair1: " + nextSetElem + " " + nextSetElem.iterator().next().getBasePair()); + + /* sameEqSet-Bestimmung: Wenn a = ty \in nextSet dann enthaelt sameEqSet + * alle Paare a < ty1 oder ty2 < a aus oneElems */ + Set sameEqSet = new HashSet<>(); + + //optOrigPair enthaelt ggf. das Paar a = ty \in nextSet + Optional optOrigPair = null; + if (!oderConstraint) { + optOrigPair = nextSetElem.stream().filter(x -> ( + //x.getBasePair() != null && ist gegeben wenn variance != 2 + //x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT) && + (x.getPairOp().equals(PairOperator.EQUALSDOT) + /* + (x.getBasePair().getLhsType() instanceof PlaceholderType + && x.getLhsType().equals(x.getBasePair().getLhsType())) + || (x.getBasePair().getRhsType() instanceof PlaceholderType + && x.getLhsType().equals(x.getBasePair().getRhsType()) + */ + ))).filter(x -> //Sicherstellen, dass bei a = ty a auch wirklich die gesuchte Typvariable ist + x.getLhsType().equals(x.getBasePair().getLhsType()) || + x.getLhsType().equals(x.getBasePair().getRhsType()) + ).findFirst(); + writeLog("optOrigPair: " + optOrigPair); + if (optOrigPair.isPresent()) { + UnifyPair origPair = optOrigPair.get(); + UnifyType tyVar; + if (!((tyVar = origPair.getLhsType()) instanceof PlaceholderType)) { + tyVar = origPair.getRhsType(); + } + UnifyType tyVarEF = tyVar; + sameEqSet = oneElems.stream().map(xx -> xx.iterator().next()) + .filter(x -> (((x.getLhsType().equals(tyVarEF) && !(x.getRhsType() instanceof PlaceholderType)) + || (x.getRhsType().equals(tyVarEF) && !(x.getLhsType() instanceof PlaceholderType))))) + .collect(Collectors.toCollection(HashSet::new)); + } + } + /* sameEqSet-Bestimmung Ende */ + + int hilf = 0; + Set a = null; + while (nextSetasList.size() > 0) { + + //statistics + //writeStatistics(" Actual Number of elements( " + nextSetasList.get(0).stream().findFirst().get().getBasePair() +"): (" + rekTiefe + "): " + nextSetasList.size()); + Set a_last = a; + + /* Liste der Faelle für die parallele Verarbeitung + * Enthaelt Elemente, die nicht in Relation zu aktuellem Fall in der + * Variablen a stehen. Diese muesse auf alle Faelle bearbeitet werden, + * Deshalb wird ihre Berechnung parallel angestossen. + */ + List> nextSetasListRest = new ArrayList<>(); + + /* Liste der Faelle, bei dem Receiver jeweils "? extends" enthaelt bzw. nicht enthaelt + * In der Regel ist dies genau ein Element + * Dieses Element wird später aus nextSetasList geloescht, wenn das jeweils andere Element zum Erfolg + * gefuehrt hat. + */ + List> nextSetasListOderConstraints = new ArrayList<>(); + + writeLog("nextSet: " + nextSet.toString()); + writeLog("nextSetasList: " + nextSetasList.toString()); + + /* staistics Nextvar an Hand Varianzbestimmung auskommentieren Anfang + if (variance == 1) { + a = oup.max(nextSetasList.iterator()); + nextSetasList.remove(a); + if (oderConstraint) { + nextSetasListOderConstraints.add(((Constraint)a).getExtendConstraint()); + } + writeLog("nextSetasListOderConstraints 1: " + nextSetasListOderConstraints); + nextSetasListRest = new ArrayList<>(nextSetasList); + Iterator> nextSetasListItRest = new ArrayList>(nextSetasListRest).iterator(); + while (nextSetasListItRest.hasNext()) { + Set a_next = nextSetasListItRest.next(); + if (//a.equals(a_next) || + (oup.compare(a, a_next) == 1)) { + nextSetasListRest.remove(a_next); + } + } + + //Alle maximale Elemente in nextSetasListRest bestimmen + //nur für diese wird parallele Berechnung angestossen. + nextSetasListRest = oup.maxElements(nextSetasListRest); + } + else if (variance == -1) { + a = oup.min(nextSetasList.iterator()); + writeLog("Min: a in " + variance + " "+ a); + if (oderConstraint) { + nextSetasListOderConstraints.add(((Constraint)a).getExtendConstraint()); + } + writeLog("nextSetasListOderConstraints -1: " + nextSetasListOderConstraints); + nextSetasList.remove(a); + nextSetasListRest = new ArrayList<>(nextSetasList); + Iterator> nextSetasListItRest = new ArrayList>(nextSetasListRest).iterator(); + while (nextSetasListItRest.hasNext()) { + Set a_next = nextSetasListItRest.next(); + if (//a.equals(a_next) || + (oup.compare(a, a_next) == -1)) { + nextSetasListRest.remove(a_next); + } + } + //Alle minimalen Elemente in nextSetasListRest bestimmen + //nur für diese wird parallele Berechnung angestossen. + nextSetasListRest = oup.minElements(nextSetasListRest); + } + else if (variance == 2) { + a = nextSetasList.remove(0); + + //Fuer alle Elemente wird parallele Berechnung angestossen. + nextSetasListRest = new ArrayList<>(nextSetasList); + } + else if (variance == 0) { + //wenn a <. theta dann ist ein maximales Element sehr wahrscheinlich + //wenn theta <. a dann ist ein minimales Element sehr wahrscheinlich + if (!oderConstraint && optOrigPair != null && optOrigPair.isPresent()) { + if (optOrigPair.get().getBasePair().getLhsType() instanceof PlaceholderType) { + a = oup.max(nextSetasList.iterator()); + } + else { + a = oup.min(nextSetasList.iterator()); + } + nextSetasList.remove(a); + } + else { + if (oderConstraint) { + a = oup.max(nextSetasList.iterator()); + nextSetasList.remove(a); + nextSetasListOderConstraints.add(((Constraint)a).getExtendConstraint()); + } + else { + a = nextSetasList.remove(0); + } + } + } + Nextvar an Hand Varianzbestimmung auskommentieren Ende */ + a = nextSetasList.remove(0); //statisticsList + + //writeStatistics(a.toString()); + if (oderConstraint) {//Methodconstraints werden abgespeichert für die Bytecodegenerierung von Methodenaufrufen + methodSignatureConstraint.addAll(((Constraint)a).getmethodSignatureConstraint()); + //System.out.println("ERSTELLUNG: " +methodSignatureConstraint); + } + + i++; + Set> elems = new HashSet>(oneElems); + writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n"); + + //Ergebnisvariable für den aktuelle Thread + Set> res = new HashSet<>(); + + //Menge der Ergebnisse der geforkten Threads + Set>> add_res = new HashSet<>(); + + + Set> aParDef = new HashSet<>(); + + /* Wenn bei (a \in theta) \in a zu Widerspruch in oneElems wird + * a verworfen und zu nächstem Element von nextSetasList gegangen + */ + /* statistics sameEq wird nicht betrachtet ANGFANG + if (!oderConstraint && !sameEqSet.isEmpty() && !checkNoContradiction(a, sameEqSet, result)) { + a = null; + noShortendElements++; + continue; + } + statistics sameEq wird nicht betrachtet ENDE */ + + /* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread + * gestartet, der parallel weiterarbeitet. + */ + if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) { + Set forks = new HashSet<>(); + Set newEqOrig = new HashSet<>(eq); + Set> newElemsOrig = new HashSet<>(elems); + List>> newOderConstraintsOrig = new ArrayList<>(oderConstraints); + newElemsOrig.add(a); + + /* FORK ANFANG */ + TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraint); + //forks.add(forkOrig); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + forkOrig.fork(); + } + /* FORK ENDE */ + + synchronized (this) { + writeLog("a in " + variance + " "+ a); + writeLog("nextSetasListRest: " + nextSetasListRest.toString()); + } + while (!nextSetasList.isEmpty()) { + Set nSaL = nextSetasList.remove(0); + synchronized (this) { //nextSetasList.remove(nSaL); + writeLog("1 RM" + nSaL.toString()); + } + + if (!oderConstraint) { + + /* statistics sameEq wird nicht betrachtet ANGFANG + //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht + if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) { + nSaL = null; + noShortendElements++; + continue; + } + statistics sameEq wird nicht betrachtet ENDE */ + } + else { + nextSetasListOderConstraints.add(((Constraint)nSaL).getExtendConstraint()); + } + Set newEq = new HashSet<>(eq); + Set> newElems = new HashSet<>(elems); + List>> newOderConstraints = new ArrayList<>(oderConstraints); + newElems.add(nSaL); + TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint)); + forks.add(fork); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + fork.fork(); + } + } + //res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe); + + /* FORK ANFANG */ + synchronized (this) { + writeLog("wait "+ forkOrig.thNo); + noOfThread--; + res = forkOrig.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + forkOrig.writeLog("final Orig 1"); + forkOrig.closeLogFile(); + //Set> fork_res = forkOrig.join(); + writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + //add_res.add(fork_res); + }; + /* FORK ENDE */ + + forks.forEach(x -> writeLog("wait: " + x.thNo)); + for(TypeUnify2Task fork : forks) { + synchronized (this) { + noOfThread--; + Set> fork_res = fork.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + writeLog("Join " + new Integer(fork.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + writeLog("fork_res: " + fork_res.toString()); + writeLog(new Boolean((isUndefinedPairSetSet(fork_res))).toString()); + add_res.add(fork_res); + if (!isUndefinedPairSetSet(fork_res)) { + aParDef.add(fork.getNextSetElement()); + } + fork.writeLog("final 1"); + fork.closeLogFile(); + }; + } + //noOfThread++; + } else { + if(parallel && (variance == -1) && noOfThread <= MaxNoOfThreads) { + Set forks = new HashSet<>(); + Set newEqOrig = new HashSet<>(eq); + Set> newElemsOrig = new HashSet<>(elems); + List>> newOderConstraintsOrig = new ArrayList<>(oderConstraints); + newElemsOrig.add(a); + + /* FORK ANFANG */ + TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint)); + //forks.add(forkOrig); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + forkOrig.fork(); + } + /* FORK ENDE */ + + synchronized (this) { + writeLog("a in " + variance + " "+ a); + writeLog("nextSetasListRest: " + nextSetasListRest.toString()); + } + while (!nextSetasList.isEmpty()) { + Set nSaL = nextSetasList.remove(0); + synchronized (this) { //nextSetasList.remove(nSaL); + writeLog("-1 RM" + nSaL.toString()); + } + + if (!oderConstraint) { + /* statistics sameEq wird nicht betrachtet ANGFANG + //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht + if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) { + nSaL = null; + noShortendElements++; + continue; + } + statistics sameEq wird nicht betrachtet ENDE */ + } + else { + nextSetasListOderConstraints.add(((Constraint)nSaL).getExtendConstraint()); + } + Set newEq = new HashSet<>(eq); + Set> newElems = new HashSet<>(elems); + List>> newOderConstraints = new ArrayList<>(oderConstraints); + newElems.add(nSaL); + TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint)); + forks.add(fork); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + fork.fork(); + } + } + //res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe); + + /* FORK ANFANG */ + synchronized (this) { + writeLog("wait "+ forkOrig.thNo); + noOfThread--; + res = forkOrig.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + forkOrig.writeLog("final Orig -1"); + forkOrig.closeLogFile(); + //Set> fork_res = forkOrig.join(); + writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + //add_res.add(fork_res); + }; + /* FORK ENDE */ + + forks.forEach(x -> writeLog("wait: " + x.thNo)); + for(TypeUnify2Task fork : forks) { + synchronized (this) { + noOfThread--; + Set> fork_res = fork.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + writeLog("Join " + new Integer(fork.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + writeLog("fork_res: " + fork_res.toString()); + writeLog(new Boolean((isUndefinedPairSetSet(fork_res))).toString()); + add_res.add(fork_res); + if (!isUndefinedPairSetSet(fork_res)) { + aParDef.add(fork.getNextSetElement()); + } + fork.writeLog("final -1"); + fork.closeLogFile(); + }; + } + //noOfThread++; + } else { + if(parallel && (variance == 2) && noOfThread <= MaxNoOfThreads) { + writeLog("var2einstieg"); + Set forks = new HashSet<>(); + Set newEqOrig = new HashSet<>(eq); + Set> newElemsOrig = new HashSet<>(elems); + List>> newOderConstraintsOrig = new ArrayList<>(oderConstraints); + newElemsOrig.add(a); + + /* FORK ANFANG */ + TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint)); + //forks.add(forkOrig); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + forkOrig.fork(); + } + /* FORK ENDE */ + + synchronized (this) { + writeLog("a in " + variance + " "+ a); + writeLog("nextSetasListRest: " + nextSetasListRest.toString()); + } + while (!nextSetasList.isEmpty()) { + Set nSaL = nextSetasList.remove(0); + //nextSetasList.remove(nSaL); //PL einkommentiert 20-02-03 + Set newEq = new HashSet<>(eq); + Set> newElems = new HashSet<>(elems); + List>> newOderConstraints = new ArrayList<>(oderConstraints); + newElems.add(nSaL); + TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraint); + forks.add(fork); + synchronized(usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + fork.fork(); + } + } + //res = unify2(newElemsOrig, newEqOrig, newOderConstraintsOrig, fc, parallel, rekTiefe); + + /* FORK ANFANG */ + synchronized (this) { + writeLog("wait "+ forkOrig.thNo); + noOfThread--; + res = forkOrig.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + forkOrig.writeLog("final Orig 2"); + forkOrig.closeLogFile(); + //Set> fork_res = forkOrig.join(); + writeLog("JoinOrig " + new Integer(forkOrig.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + //add_res.add(fork_res); //vermutlich falsch + }; + /* FORK ENDE */ + forks.forEach(x -> writeLog("wait: " + x.thNo)); + for(TypeUnify2Task fork : forks) { + synchronized (this) { + noOfThread--; + Set> fork_res = fork.join(); + synchronized (usedTasks) { + if (this.myIsCancelled()) { + return new HashSet<>(); + } + } + //noOfThread++; + writeLog("Join " + new Integer(fork.thNo).toString()); + //noOfThread--; an das Ende von compute verschoben + add_res.add(fork_res); + fork.writeLog("final 2"); + fork.closeLogFile(); + }; + } + //noOfThread++; + } else {//parallel = false oder MaxNoOfThreads ist erreicht, sequentiell weiterarbeiten + elems.add(a); //PL 2019-01-16 muss das wirklich hin steht schon in Zeile 859 ja braucht man siehe Zeile 859 + res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe, new HashSet<>(methodSignatureConstraint)); + }}} + + //Ab hier alle parallele Berechnungen wieder zusammengeführt. + //if (hilf == 1) + //System.out.println(); + //writeStatistics("Zusammengeführt(" + rekTiefe + "): " + nextSetasList.size()); + if (oderConstraint) {//Wenn weiteres Element nextSetasList genommen wird, muss die vorherige methodsignatur geloescht werden + methodSignatureConstraint.removeAll(((Constraint)a).getmethodSignatureConstraint()); + //System.out.println("REMOVE: " +methodSignatureConstraint); + } + if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) { + //wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen + result = res; + } + else { + if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) + || (!isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result)) + || result.isEmpty()) { + + /* auskommentiert damit alle Lösungen reinkommen ANFANG + if ((!result.isEmpty() && !res.isEmpty() && !isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result)) //korrekte Loesungen aus und-constraints + && (a.stream().map(x-> (x.getBasePair() != null)).reduce(true, (x, y) -> (x && y)))) //bei oder-Constraints nicht ausfuehren + { + //TODO: PL 2019-01-15: Bug 129: Im Moment wird nur das Maximum und das Minimum des aktuellen Elements betrachtet. + //Die zu vereinigenden Mengen können mehrere Elemente enthalten. Das ist bisher nicht berücksichtigt + + //Alle Variablen bestimmen die nicht hinzugefügt wurden in a + //PL 2018-12-28: Hier gab es eine ClassCastException, war nicht reproduzierbar + System.out.println(""); + List vars_a = + a.stream().filter(x -> ((x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName()) + && (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getLhsType() instanceof PlaceholderType)) + || ((x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())) + && (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getRhsType() instanceof PlaceholderType))) + ) + .map(y -> (PlaceholderType)y.getLhsType()).collect(Collectors.toCollection(ArrayList::new)); + Set fstElemRes = res.iterator().next(); + Set compRes = fstElemRes.stream().filter(x -> vars_a.contains(((PlaceholderType)x.getLhsType()))).collect(Collectors.toCollection(HashSet::new)); + + //Alle Variablen bestimmen die nicht hinzugefügt wurden in a_last + //System.out.println(a_last); + if (a_last != null) { + try {//PL eingefuegt 2019-03-06 da bei map mmer wieder Nullpointer kamen + a_last.forEach(x -> {writeLog("a_last_elem:" + x + " basepair: " + x.getBasePair());});//PL 2019-05-13 ins try hinzugefuegt Nullpointer-Exception ist in der Zeile aufgetaucht. + List varsLast_a = + a_last.stream().filter(x -> ((x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName()) + && (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getLhsType() instanceof PlaceholderType)) + || ((x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName()))) + && (x.getLhsType() instanceof PlaceholderType) && (x.getBasePair().getRhsType() instanceof PlaceholderType))) + .map(y -> (PlaceholderType)y.getLhsType()).collect(Collectors.toCollection(ArrayList::new)); + //[(java.util.Vector <. gen_aq, , 1), (CEK =. ? extends gen_aq, 1)] KANN VORKOMMEN + //erstes Element genügt, da vars immer auf die gleichen Elemente zugeordnet werden muessen + Set fstElemResult = result.iterator().next(); + Set compResult = fstElemResult.stream().filter(x -> varsLast_a.contains(((PlaceholderType)x.getLhsType()))).collect(Collectors.toCollection(HashSet::new));; + if (variance == 1) { + writeLog("a_last:" + a_last + " a: " + a); + writeLog("varsLast_a:" + varsLast_a + " vars_a: " + vars_a); + writeLog("compResult:" + compResult + " compRes: " + compRes); + int resOfCompare = oup.compare(compResult, compRes); + if (resOfCompare == -1) { + writeLog("Geloescht result: " + result); + result = res; + } else { + if (resOfCompare == 0) { + result.addAll(res); + } //else { + if (resOfCompare == 1) { + writeLog("Geloescht res: " + res); + //result = result; + }}} + else { if (variance == -1) { + writeLog("a_last:" + a_last + " a: " + a); + writeLog("varsLast_a:" + varsLast_a + " vars_a: " + vars_a); + writeLog("compResult:" + compResult + " compRes: " + compRes); + int resOfCompare = oup.compare(compResult, compRes); + if (resOfCompare == 1) { + writeLog("Geloescht result: " + result); + result = res; + } else { + if (resOfCompare == 0) { + result.addAll(res); + } else { + if (resOfCompare == -1) { + writeLog("Geloescht res: " + res); + //result = result; + }}}} + else { if (variance == 0) { + writeLog("RES var=1 ADD:" + result.toString() + " " + res.toString()); + result.addAll(res); + }}} + } + catch (NullPointerException e) { + writeLog("NullPointerException: " + a_last.toString()); + }} + } + else + auskommentiert damit alle Lösungen reinkommen ANFANG */ + { + //alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden + writeLog("RES Fst: result: " + result.toString() + " res: " + res.toString()); + result.addAll(res); + } + } + //else { + //wenn Korrekte Ergebnisse da und Feherfälle dazukommen Fehlerfälle ignorieren + // if (isUndefinedPairSetSet(res) && !isUndefinedPairSetSet(result)) { + // result = result; + // } + //} + } + + if (parallel) { + for (Set> par_res : add_res) { + if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) { + //wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen + result = par_res; + if (!par_res.isEmpty() && par_res.iterator().next() instanceof WildcardType) { + //System.out.println(""); + } + } + else { + if ((isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) + || (!isUndefinedPairSetSet(par_res) && !isUndefinedPairSetSet(result)) + || result.isEmpty()) { + //alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden + writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString()); + result.addAll(par_res); + } + } + } + //break; + } + + /* auskommentiert um alle Max und min Betrachtung auszuschalten ANFANG + if (!result.isEmpty() && (!isUndefinedPairSetSet(res) || !aParDef.isEmpty())) { + if (nextSetasList.iterator().hasNext() && nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("B")).findFirst().isPresent() && nextSetasList.size()>1) + System.out.print(""); + Iterator> nextSetasListIt = new ArrayList>(nextSetasList).iterator(); + if (variance == 1) { + System.out.println(""); + writeLog("a: " + rekTiefe + " variance: " + variance + a.toString()); + writeLog("aParDef: " + aParDef.toString()); + aParDef.add(a); + Iterator> aParDefIt = aParDef.iterator(); + if (oderConstraint) { + nextSetasList.removeAll(nextSetasListOderConstraints); + nextSetasListOderConstraints = new ArrayList<>(); + writeLog("Removed: " + nextSetasListOderConstraints); + while(aParDefIt.hasNext()) { + Set a_new = aParDefIt.next(); + List> smallerSetasList = oup.smallerThan(a_new, nextSetasList); + List> notInherited = smallerSetasList.stream() + .filter(x -> !((Constraint)x).isInherited()) + .collect(Collectors.toCollection(ArrayList::new)); + List> notErased = new ArrayList<>(); + notInherited.stream().forEach(x -> { notErased.addAll(oup.smallerEqThan(x, smallerSetasList)); }); + List> erased = new ArrayList<>(smallerSetasList); + erased.removeAll(notErased); + nextSetasList.removeAll(erased); + + writeLog("Removed: " + erased); + + writeLog("Not Removed: " + nextSetasList); + + } + } + else { + while(aParDefIt.hasNext()) { + //nextSetasListIt = nextSetasList.iterator(); Sollte eingefuegt werden PL 2020-04-28 + Set a_new = aParDefIt.next(); + List> erased = oup.smallerEqThan(a_new, nextSetasList); + nextSetasList.removeAll(erased); + + writeLog("Removed: " + erased); + + writeLog("Not Removed: " + nextSetasList); + } + } + } + else { if (variance == -1) { + System.out.println(""); + writeLog("a: " + rekTiefe + " variance: " + variance + a.toString()); + writeLog("aParDef: " + aParDef.toString()); + aParDef.add(a); + Iterator> aParDefIt = aParDef.iterator(); + if (oderConstraint) { + nextSetasList.removeAll(nextSetasListOderConstraints); + writeLog("Removed: " + nextSetasListOderConstraints); + nextSetasListOderConstraints = new ArrayList<>(); + while(aParDefIt.hasNext()) { + Set a_new = aParDefIt.next(); + List> greaterSetasList = oup.greaterThan(a_new, nextSetasList); + + //a_new muss hingefuegt werden, wenn es nicht vererbt ist, dann wird es spaeter wieder geloescht + if (!((Constraint)a_new).isInherited()) { + greaterSetasList.add(a_new); + } + List> notInherited = greaterSetasList.stream() + .filter(x -> !((Constraint)x).isInherited()) + .collect(Collectors.toCollection(ArrayList::new)); + List> notErased = new ArrayList<>(); + + //Wenn x nicht vererbt ist, beginnt beim naechstgroesseren Element die naechste Ueberladung + notInherited.stream().forEach(x -> { notErased.addAll(oup.greaterEqThan(x, greaterSetasList)); }); + + //das kleineste Element ist das Element von dem a_new geerbt hat + //muss deshalb geloescht werden + Iterator> notErasedIt = notErased.iterator(); + if (notErasedIt.hasNext()) { + Set min = oup.min(notErasedIt); + notErased.remove(min); + notErased.remove(((Constraint)min).getExtendConstraint()); + } + + List> erased = new ArrayList<>(greaterSetasList); + erased.removeAll(notErased); + nextSetasList.removeAll(erased); + + writeLog("Removed: " + erased); + + writeLog("Not Removed: " + nextSetasList); + + } + } + else { + while(aParDefIt.hasNext()) { + //nextSetasListIt = nextSetasList.iterator(); Sollte eingefuegt werden PL 2020-04-28 + Set a_new = aParDefIt.next(); + List> erased = oup.greaterEqThan(a_new, nextSetasList); + + nextSetasList.removeAll(erased); + + writeLog("Removed: " + erased); + + writeLog("Not Removed: " + nextSetasList); + } + } + } + else { if (variance == 0) { + writeLog("a: " + rekTiefe + " variance: " + variance + a.toString()); + if (!oderConstraint) { + writeStatistics("break"); + break; + } + else { + nextSetasList.removeAll(nextSetasListOderConstraints); + nextSetasListOderConstraints = new ArrayList<>(); + writeLog("Removed: " + nextSetasListOderConstraints); + List> smallerSetasList = oup.smallerThan(a, nextSetasList); + List> notInherited = smallerSetasList.stream() + .filter(x -> !((Constraint)x).isInherited()) + .collect(Collectors.toCollection(ArrayList::new)); + List> notErased = new ArrayList<>(); + notInherited.stream().forEach(x -> { notErased.addAll(oup.smallerEqThan(x, smallerSetasList)); }); + List> erased = new ArrayList<>(smallerSetasList); + erased.removeAll(notErased); + nextSetasList.removeAll(erased); + + writeLog("Removed: " + erased); + + writeLog("Not Removed: " + nextSetasList); + + } + + } + else { if (variance == 2) { + }}} + writeLog("a: " + rekTiefe + " variance: " + variance + a.toString()); + } + } + auskommentiert um alle Max und min Betrachtung auszuschalten ENDE */ + + if (isUndefinedPairSetSet(res) && aParDef.isEmpty()) { + int nofstred= 0; + Set abhSubst = res.stream() + .map(b -> + b.stream() + .map(x -> x.getAllSubstitutions()) + .reduce((y,z) -> { y.addAll(z); return y;}).get()) + .reduce((y,z) -> { y.addAll(z); return y;}).get(); + abhSubst.addAll( + res.stream() + .map(b -> + b.stream() + .map(x -> x.getThisAndAllBases()) //getAllBases durch getThisAndAllBases ersetzt, weil auch im UnifyPair selbst schon ein Fehler liegen kann. + .reduce((y,z) -> { y.addAll(z); return y;}).get()) + .reduce((y,z) -> { y.addAll(z); return y;}).get() + ); + Set b = a;//effective final a + Set durchschnitt = abhSubst.stream() + .filter(x -> b.contains(x)) + //.filter(y -> abhSubst.contains(y)) + .collect(Collectors.toCollection(HashSet::new)); + //Set vars = durchschnitt.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new)); + int len = nextSetasList.size(); + Set undefRes = res.stream().reduce((y,z) -> { y.addAll(z); return y;}).get(); //flatten aller undef results + Set, UnifyPair>> reducedUndefResSubstGroundedBasePair = undefRes.stream() + .map(x -> { Set su = x.getAllSubstitutions(); //alle benutzten Substitutionen + su.add(x.getGroundBasePair()); // urspruengliches Paar + su.removeAll(durchschnitt); //alle aktuell genänderten Paare entfernen + return new Pair<>(su, x.getGroundBasePair());}) + .collect(Collectors.toCollection(HashSet::new)); + if (res.size() > 1) { + //System.out.println(); + } + /* statistics no erase + writeLog("nextSetasList vor filter-Aufruf: " + nextSetasList); + if (!oderConstraint) {//PL 2023-02-08 eingefuegt: Bei oderconstraints sind Subststitutionen nicht als Substitutionen in idesem Sinne zu sehen + nextSetasList = nextSetasList.stream().filter(x -> { + //Boolean ret = false; + //for (PlaceholderType var : vars) { + // ret = ret || x.stream().map(b -> b.getLhsType().equals(var)).reduce((c,d) -> c || d).get(); + //} + return (!x.containsAll(durchschnitt)); + })//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) //fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10 + .collect(Collectors.toCollection(ArrayList::new)); + } + writeLog("nextSetasList nach filter-Aufruf: " + nextSetasList); + */ + nofstred = nextSetasList.size(); + //NOCH NICHT korrekt PL 2018-10-12 + //nextSetasList = nextSetasList.stream().filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) + // .collect(Collectors.toCollection(ArrayList::new)); + writeLog("res (undef): " + res.toString()); + writeLog("abhSubst: " + abhSubst.toString()); + writeLog("a2: " + rekTiefe + " " + a.toString()); + writeLog("Durchschnitt: " + durchschnitt.toString()); + writeLog("nextSet: " + nextSet.toString()); + writeLog("nextSetasList: " + nextSetasList.toString()); + writeLog("Number first erased Elements (undef): " + (len - nofstred)); + writeLog("Number second erased Elements (undef): " + (nofstred- nextSetasList.size())); + writeLog("Number erased Elements (undef): " + (len - nextSetasList.size())); + noAllErasedElements = noAllErasedElements + (len - nextSetasList.size()); + writeLog("Number of all erased Elements (undef): " + noAllErasedElements.toString()); + noBacktracking++; + writeLog("Number of Backtracking: " + noBacktracking); + //writeStatistics("Number of erased elements: " + (len - nextSetasList.size())); + //writeStatistics("Number of Backtracking: " + noBacktracking); + //System.out.println(""); + } + else //writeStatistics("res: " + res.toString()); + //if (nextSetasList.size() == 0 && isUndefinedPairSetSet(result) && nextSet.size() > 1) { + // return result; + //} + //else { + // result.removeIf(y -> isUndefinedPairSet(y)); + //} + //else result.stream().filter(y -> !isUndefinedPairSet(y)); + writeLog("res: " + res.toString()); + //writeStatistics(" End Number of Elements (" + rekTiefe + "): " + nextSetasList.size()); + noLoop++; + //writeStatistics("Number of Loops: " + noLoop); + } + //2020-02-02: if (variance ==2) Hier Aufruf von filterOverriding einfuegen + writeLog("Return computeCR: " + result.toString()); + return result; + } + + /** + * checks if there is for (a = ty) \in a in sameEqSet a constradiction + * @param a Set of actual element of constraints with a =. ty \in a + * @param sameEqSet Set of constraints where a <. ty' and ty' <. a + * @param result set of results which contains correct solution s and the + * the error constraints. Error constraints are added + * @result contradiction of (a = ty) in sameEqSet + */ + protected Boolean checkNoContradiction(Set a, Set sameEqSet, Set> result) { + + //optAPair enthaelt ggf. das Paar a = ty' \in a + //unterscheidet sich von optOrigPair, da dort a = ty + Optional optAPair = + a.stream().filter(x -> (x.getPairOp().equals(PairOperator.EQUALSDOT))) + .filter(x -> //Sicherstellen, dass bei a = ty a auch wirklich die gesuchte Typvariable ist + x.getLhsType().equals(x.getBasePair().getLhsType()) || + x.getLhsType().equals(x.getBasePair().getRhsType())) + .findFirst(); + + if (optAPair.isPresent()) {//basepair ist entweder a <. Ty oder ty <. a + UnifyPair aPair = optAPair.get(); + //writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair()); + + writeLog("checkA: " + aPair + "sameEqSet: " + sameEqSet); + for (UnifyPair sameEq : sameEqSet) { + if (sameEq.getLhsType() instanceof PlaceholderType) { + Set localEq = new HashSet<>(); + Set unitedSubst = new HashSet<>(aPair.getAllSubstitutions()); + unitedSubst.addAll(aPair.getAllBases()); + unitedSubst.addAll(sameEq.getAllSubstitutions()); + unitedSubst.addAll(sameEq.getAllBases()); + localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); + finalresult = false; + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, new HashSet<>()); + finalresult = true; + if (isUndefinedPairSetSet(localRes)) { + if (result.isEmpty() || isUndefinedPairSetSet(result)) { + result.addAll(localRes); + } + writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); + return false; + } + } + else { + Set localEq = new HashSet<>(); + Set unitedSubst = new HashSet<>(aPair.getAllSubstitutions()); + unitedSubst.addAll(aPair.getAllBases()); + unitedSubst.addAll(sameEq.getAllSubstitutions()); + unitedSubst.addAll(sameEq.getAllBases()); + localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); + finalresult = false; + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, new HashSet<>()); + finalresult = true; + if (isUndefinedPairSetSet(localRes)) { + if (result.isEmpty() || isUndefinedPairSetSet(result)) { + result.addAll(localRes); + } + writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); + return false; + } + } + } + writeLog("TRUE: " + aPair + "sameEqSet: " + sameEqSet); + return true; + } + return true; + } + + + protected boolean couldBecorrect(Set, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set nextElem) { + return reducedUndefResSubstGroundedBasePair.stream() + .map(pair -> { + Set reducedAbhSubst = pair.getKey(); + reducedAbhSubst.addAll(nextElem); + Optional> substRes = rules.subst(reducedAbhSubst); + if (!substRes.isPresent()) { + return true; + } + //PL 2018-10-12 + //Evtl. zurest applyTypeUnification aufrufen + //evtl auch unify aufrufen + else { + UnifyPair checkPair = substRes.get().stream() + .filter(x -> x.getGroundBasePair().equals(pair.getValue().get())).findFirst().get(); + if (((checkPair.getLhsType() instanceof PlaceholderType) || (checkPair.getRhsType() instanceof PlaceholderType)) + && (checkPair.getPairOp() == PairOperator.SMALLERDOT || checkPair.getPairOp() == PairOperator.SMALLERDOTWC)) + { + /* + Set setCheckPair = new HashSet<>(); + setCheckPair.add(checkPair); + Set setReturnCheckPair = applyTypeUnificationRules(setCheckPair, fc); + UnifyPair checkPair1 = setReturnCheckPair.iterator().next(); + Set up = new HashSet<>(); + up.add(checkPair1); + Set undef = new HashSet<>(); + */ + PairOperator pairOp = checkPair.getPairOp(); + UnifyType lhsType = checkPair.getLhsType(); + UnifyType rhsType = checkPair.getRhsType(); + ///* Case 1: (a <. Theta') + if ((((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.SMALLERNEQDOT)) && lhsType instanceof PlaceholderType) + // Case 2: (a <.? ? ext Theta') + || (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) + // Case 3: (a <.? ? sup Theta') + || (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) + + // Case 4 was replaced by an inference rule + // Case 4: (a <.? Theta') + || (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) + // Case 5: (Theta <. a) + || ((pairOp == PairOperator.SMALLERDOT) && rhsType instanceof PlaceholderType) + // Case 6 was replaced by an inference rule. + // Case 6: (? ext Theta <.? a) + || (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) + // Case 7 was replaced by an inference rule + // Case 7: (? sup Theta <.? a) + || (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) + // Case 8: (Theta <.? a) + || (pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) + //reduceWildcardLow + || (pairOp == PairOperator.SMALLERDOTWC && (lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType)) + //reduceWildcardLowRight + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof ExtendsType)) + //reduceWildcardUp + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && (rhsType instanceof SuperType)) + //reduceWildcardUpRight + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof SuperType)) + //reduceFunN + || (((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.EQUALSDOT)) + //PL 2017-10-03 hinzugefuegt + //da Regel auch fuer EQUALSDOT anwendbar + && (lhsType instanceof FunNType) && (rhsType instanceof FunNType)) + //greaterFunN + || ((pairOp== PairOperator.SMALLERDOT) && (lhsType instanceof FunNType) && (rhsType instanceof PlaceholderType)) + //smallerFunN + || ((pairOp == PairOperator.SMALLERDOT) && (lhsType instanceof PlaceholderType && rhsType instanceof FunNType)) + //reduceTph + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof PlaceholderType && rhsType instanceof ReferenceType)) + //reduceTphExt + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ExtendsType) && rhsType instanceof PlaceholderType) + //reduceTphSup + || ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && rhsType instanceof PlaceholderType)) { + return true; + } + // Case unknown: If a pair fits no other case, then the type unification has failed. + // Through application of the rules, every pair should have one of the above forms. + // Pairs that do not have one of the aboves form are contradictory. + else { + writeLog("Second erase:" +checkPair.toString()); + return false; + } + //*/ + } else { + //Pair type <. ? extends ? extends type betrachten TODO PL 2018-10-09 + }} + return true;}).reduce((xx, yy) -> xx || yy).get(); + } + + protected boolean isUndefinedPairSet(Set s) { + if (s.size() >= 1 ) { + Boolean ret = s.stream().map(x -> x.isUndefinedPair()).reduce(true, (x,y)-> (x && y)); + return ret; + } + else { + return false; + } + } + + protected boolean isUndefinedPairSetSet(Set> s) { + if (s.size() >= 1) { + Boolean ret = s.stream(). map(x -> isUndefinedPairSet(x)).reduce(true, (x,y)-> (x && y)); + return ret; + } + return false; + + } + /** + * Checks whether a set of pairs is in solved form. + * @param eqPrimePrime The set of pair + * @return True if in solved form, false otherwise. + */ + protected boolean isSolvedForm(Set eqPrimePrime) { + for(UnifyPair pair : eqPrimePrime) { + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + if(!(lhsType instanceof PlaceholderType)) + return false; + + // If operator is not equals, both sides must be placeholders + if(pair.getPairOp() != PairOperator.EQUALSDOT && !(rhsType instanceof PlaceholderType)) + return false; + } + return true; + } + + /** + * Repeatedly applies type unification rules to a set of equations. + * This is step one of the unification algorithm. + * @return The set of pairs that results from repeated application of the inference rules. + */ + public Set applyTypeUnificationRules(Set eq, IFiniteClosure fc) { + + /* + * Rule Application Strategy: + * + * 1. Swap all pairs and erase all erasable pairs + * 2. Apply all possible rules to a single pair, then move it to the result set. + * Iterating over pairs first, then iterating over rules prevents the application + * of rules to a "finished" pair over and over. + * 2.1 Apply all rules repeatedly except for erase rules. If + * the application of a rule creates new pairs, check immediately + * against the erase rules. + */ + + + LinkedHashSet targetSet = new LinkedHashSet(); + LinkedList eqQueue = new LinkedList<>(); + + /* + * Swap all pairs and erase all erasable pairs + */ + eq.forEach(x -> swapAddOrErase(x, fc, eqQueue)); + + /* + * Apply rules until the queue is empty + */ + while(!eqQueue.isEmpty()) { + UnifyPair pair = eqQueue.pollFirst(); + + // ReduceUp, ReduceLow, ReduceUpLow + Optional opt = rules.reduceUpLow(pair); + opt = opt.isPresent() ? opt : rules.reduceLow(pair); + opt = opt.isPresent() ? opt : rules.reduceUp(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLow(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardLowRight(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardUp(pair); + opt = opt.isPresent() ? opt : rules.reduceWildcardUpRight(pair); + //PL 2018-03-06 auskommentiert muesste falsch sein vgl. JAVA_BSP/Wildcard6.java + //opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair); + //opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair); + //opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair); + + // Reduce TPH + opt = opt.isPresent() ? opt : rules.reduceTph(pair); + + // One of the rules has been applied + if(opt.isPresent()) { + swapAddOrErase(opt.get(), fc, eqQueue); + continue; + } + + // Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq + //try { + // logFile.write("PAIR1 " + pair + "\n"); + // logFile.flush(); + //} + //catch (IOException e) { } + + Optional> optSet = rules.reduce1(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduce2(pair); + optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair); + + // ReduceTphExt, ReduceTphSup + optSet = optSet.isPresent() ? optSet : rules.reduceTphExt(pair); + optSet = optSet.isPresent() ? optSet : rules.reduceTphSup(pair); + + + // FunN Rules + optSet = optSet.isPresent() ? optSet : rules.reduceFunN(pair); + optSet = optSet.isPresent() ? optSet : rules.greaterFunN(pair); + optSet = optSet.isPresent() ? optSet : rules.smallerFunN(pair); + + // One of the rules has been applied + if(optSet.isPresent()) { + optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue)); + continue; + } + + // Adapt, AdaptExt, AdaptSup + //try { + // logFile.write("PAIR2 " + pair + "\n"); + // logFile.flush(); + //} + //catch (IOException e) { } + opt = rules.adapt(pair, fc); + opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc); + opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc); + + // One of the rules has been applied + if(opt.isPresent()) { + swapAddOrErase(opt.get(), fc, eqQueue); + continue; + } + + // None of the rules has been applied + targetSet.add(pair); + } + + return targetSet; + } + + /** + * Applies the rule swap to a pair if possible. Then adds the pair to the set if no erase rule applies. + * If an erase rule applies, the pair is not added (erased). + * @param pair The pair to swap and add or erase. + * @param collection The collection to which the pairs are added. + */ + protected void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection collection) { + Optional opt = rules.swap(pair); + UnifyPair pair2 = opt.isPresent() ? opt.get() : pair; + + if(rules.erase1(pair2, fc) || rules.erase3(pair2) || rules.erase2(pair2, fc)) + return; + + collection.add(pair2); + } + + /** + * Splits the equation eq into a set eq1s where both terms are type variables, + * and a set eq2s where one of both terms is not a type variable. + * @param eq Set of pairs to be splitted. + * @param eq1s Subset of eq where both terms are type variables. + * @param eq2s eq/eq1s. + */ + protected void splitEq(Set eq, Set eq1s, Set eq2s) { + for(UnifyPair pair : eq) + if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType) + eq1s.add(pair); + else + eq2s.add(pair); + } + + /** + * Creates sets of pairs specified in the fourth step. Does not calculate cartesian products. + * @param undefined All pairs that did not match one of the 8 cases are added to this set. + * @return The set of the eight cases (without empty sets). Each case is a set, containing sets generated + * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements + * (as in case 1 where sigma is added to the innermost set). + */ + protected Set>>> calculatePairSets(Set eq2s, List>> oderConstraintsInput, IFiniteClosure fc, Set undefined, List>> oderConstraintsOutput) { + writeLog("eq2s: " + eq2s.toString()); + oderConstraintsOutput.addAll(oderConstraintsInput); + List>>> result = new ArrayList<>(9); + + // Init all 8 cases + 9. Case: oderConstraints + for(int i = 0; i < 9; i++) + result.add(new HashSet<>()); + + ArrayList eq2sprime = new ArrayList<>(eq2s); + Iterator eq2sprimeit = eq2sprime.iterator(); + ArrayList eq2sAsListFst = new ArrayList<>(); + ArrayList eq2sAsListSnd = new ArrayList<>(); + ArrayList eq2sAsListThird = new ArrayList<>(); + ArrayList eq2sAsListFourth = new ArrayList<>(); + ArrayList eq2sAsListBack = new ArrayList<>(); + ArrayList eq2sAsList = new ArrayList<>(); + Boolean first = true; + while(eq2sprimeit.hasNext()) {// alle mit Variance != 0 nach vorne schieben + UnifyPair up = eq2sprimeit.next(); + if ((up.getLhsType() instanceof PlaceholderType && + ((PlaceholderType)up.getLhsType()).getVariance() == 1 && + !((PlaceholderType)up.getLhsType()).isInnerType()) || + (up.getRhsType() instanceof PlaceholderType && + ((PlaceholderType)up.getRhsType()).getVariance() == -1) && + !((PlaceholderType)up.getRhsType()).isInnerType()) + { + eq2sAsListFst.add(up); + eq2s.remove(up); + } + else if ((up.getLhsType() instanceof PlaceholderType && ((PlaceholderType)up.getLhsType()).getVariance() == 1 && ((PlaceholderType)up.getLhsType()).isInnerType()) + || (up.getRhsType() instanceof PlaceholderType && ((PlaceholderType)up.getRhsType()).getVariance() == -1) && ((PlaceholderType)up.getRhsType()).isInnerType()) { + eq2sAsListSnd.add(up); + eq2s.remove(up); + } + else if ((up.getLhsType() instanceof PlaceholderType && + ((PlaceholderType)up.getLhsType()).getVariance() == -1 && + !((PlaceholderType)up.getLhsType()).isInnerType()) || + (up.getRhsType() instanceof PlaceholderType && + ((PlaceholderType)up.getRhsType()).getVariance() == -1) && + !((PlaceholderType)up.getRhsType()).isInnerType()) + { + eq2sAsListThird.add(up); + eq2s.remove(up); + } + else if ((up.getLhsType() instanceof PlaceholderType && ((PlaceholderType)up.getLhsType()).getVariance() == -1 && ((PlaceholderType)up.getLhsType()).isInnerType()) + || (up.getRhsType() instanceof PlaceholderType && ((PlaceholderType)up.getRhsType()).getVariance() == 1) && ((PlaceholderType)up.getRhsType()).isInnerType()) { + eq2sAsListFourth.add(up); + eq2s.remove(up); + } + else if ((up.getLhsType() instanceof PlaceholderType && ((PlaceholderType)up.getLhsType()).isInnerType()) + || (up.getRhsType() instanceof PlaceholderType && ((PlaceholderType)up.getRhsType()).isInnerType())) { + eq2sAsListBack.add(up); + eq2s.remove(up); + } + } + //if (eq2sAsListFst.isEmpty()) + { + List>> oderConstraintsVariance = oderConstraintsOutput.stream() //Alle Elemente rauswerfen, die Variance 0 haben oder keine TPH in LHS oder RHS sind + .filter(x -> x.stream() + .filter(y -> + y.stream().filter(z -> ((z.getLhsType() instanceof PlaceholderType) + && (((PlaceholderType)(z.getLhsType())).getVariance() != 0)) + || ((z.getRhsType() instanceof PlaceholderType) + && (((PlaceholderType)(z.getRhsType())).getVariance() != 0)) + ).findFirst().isPresent() + ).findFirst().isPresent()).collect(Collectors.toList()); + if (!oderConstraintsVariance.isEmpty()) { + Set> ret = oderConstraintsVariance.get(0); + oderConstraintsOutput.remove(ret); + //Set retFlat = new HashSet<>(); + //ret.stream().forEach(x -> retFlat.addAll(x)); + + //Alle wildcard Faelle rausfiltern bei not wildcardable + ret = ret.stream().filter(x -> { Optional optElem; + return !((optElem=x.stream().filter(y -> (y.getLhsType()) instanceof PlaceholderType + && !((PlaceholderType)y.getLhsType()).isWildcardable() + && y.getPairOp() == PairOperator.EQUALSDOT + && !(y.getRhsType() instanceof PlaceholderType)) + .findAny()).isPresent() + && optElem.get().getRhsType() instanceof ExtendsType);}) + .collect(Collectors.toSet()); + ret.stream().forEach(x -> x.stream().forEach(y -> { Set x_new = new HashSet<>(x); //PL 2020-03-18: y selbst darf nicht in die Substitutionen + x_new.remove(y); + y.addSubstitutions(x_new); + })); + result.get(8).add(ret); + first = false; + } + } + + writeLog("eq2s: " + eq2s.toString()); + writeLog("eq2sAsListFst: " + eq2sAsListFst.toString()); + writeLog("eq2sAsListSnd: " + eq2sAsListSnd.toString()); + writeLog("eq2sAsListBack: " + eq2sAsListBack.toString()); + + eq2sAsList.addAll(eq2sAsListFst); + eq2sAsList.addAll(eq2sAsListSnd); + eq2sAsList.addAll(eq2sAsListThird); + eq2sAsList.addAll(eq2sAsListFourth); + eq2sAsList.addAll(eq2s); + eq2sAsList.addAll(eq2sAsListBack); + + if (eq2sAsList.isEmpty() && first) {//Alle eq2s sind empty und alle oderConstraints mit Variance != 0 sind bearbeitet + if (!oderConstraintsOutput.isEmpty()) { + Set> ret = oderConstraintsOutput.remove(0); + //if (ret.iterator().next().iterator().next().getLhsType().getName().equals("M")) + // System.out.println("M"); + //Set retFlat = new HashSet<>(); + //ret.stream().forEach(x -> retFlat.addAll(x)); + + //Alle wildcard Faelle rausfiltern bei not wildcardable + ret = ret.stream().filter(x -> { Optional optElem; + return !((optElem=x.stream().filter(y -> (y.getLhsType()) instanceof PlaceholderType + && !((PlaceholderType)y.getLhsType()).isWildcardable() + && y.getPairOp() == PairOperator.EQUALSDOT + && !(y.getRhsType() instanceof PlaceholderType)) + .findAny()).isPresent() + && optElem.get().getRhsType() instanceof ExtendsType);}) + .collect(Collectors.toSet()); + + ret.stream().forEach(x -> x.stream().forEach(y -> { Set x_new = new HashSet<>(x); //PL 2020-03-18: y selbst darf nicht in die Substitutionen + x_new.remove(y); + y.addSubstitutions(x_new); + })); + result.get(8).add(ret); + first = false; + } + } + /* + Bei allen die Abhaengigkeit der Elemente aus eq2sAsList als evtl. als Substitution + hinzufuegen + */ + Set consideredElements = new HashSet<>(); + for(UnifyPair pair : eq2sAsList) { + if (consideredElements.contains(pair)) { + continue; + } + PairOperator pairOp = pair.getPairOp(); + UnifyType lhsType = pair.getLhsType(); + UnifyType rhsType = pair.getRhsType(); + + // Case 1: (a <. Theta') + if (((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.SMALLERNEQDOT)) && lhsType instanceof PlaceholderType) { + //System.out.println(pair); + if (first) { //writeLog(pair.toString()+"\n"); + if (((PlaceholderType)(pair.getLhsType())).getName().equals("AR")) { + //System.out.println("AR"); + } + Set> x1 = unifyCase1(pair, fc); + if (pairOp == PairOperator.SMALLERNEQDOT) { + Set remElem = new HashSet<>(); + remElem.add(new UnifyPair(pair.getLhsType(), pair.getRhsType(), PairOperator.EQUALSDOT)); + x1.remove(remElem); + remElem = new HashSet<>(); + remElem.add(new UnifyPair(pair.getLhsType(), new ExtendsType(pair.getRhsType()), PairOperator.EQUALSDOT)); + x1.remove(remElem); + remElem = new HashSet<>(); + remElem.add(new UnifyPair(pair.getLhsType(), new SuperType(pair.getRhsType()), PairOperator.EQUALSDOT)); + x1.remove(remElem); + } + /* ZU LOESCHEN ANFANG + //System.out.println(x1); + Set sameEqSet = eq2sAsList.stream() + .filter(x -> ((x.getLhsType().equals(lhsType) || x.getRhsType().equals(lhsType)) && !x.equals(pair))) + .collect(Collectors.toCollection(HashSet::new)); + consideredElements.addAll(sameEqSet); + Set> x2 = x1; + Set> x1Res = new HashSet<>(); + writeLog("pair:\n" + pair.toString()); + writeLog("x1 Start:\n" + x1.toString()); + writeLog("sameEqSet:\n" + sameEqSet.toString()); + for (UnifyPair sameEq : sameEqSet) { + writeLog("x1 Original:\n" + x1.toString()); + if (sameEq.getLhsType() instanceof PlaceholderType) { + x1 = x1.stream().filter(y -> { + UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get(); + Set localEq = new HashSet<>(); + Set unitedSubst = new HashSet<>(type.getSubstitution()); + unitedSubst.addAll(sameEq.getSubstitution()); + localEq.add(new UnifyPair(type.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false); + Boolean localCorr = !isUndefinedPairSetSet(localRes); + if (!localCorr) { + collectErr.addAll(localRes); + } + else { + localRes.forEach(z -> z.addAll(y)); + x1Res.addAll(localRes); + } + return localCorr; + } + ).collect(Collectors.toCollection(HashSet::new)); + } + else { + x1 = x1.stream().filter(y -> { + UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get(); + Set localEq = new HashSet<>(); + Set unitedSubst = new HashSet<>(type.getSubstitution()); + unitedSubst.addAll(sameEq.getSubstitution()); + localEq.add(new UnifyPair(sameEq.getLhsType(), type.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false); + Boolean localCorr = !isUndefinedPairSetSet(localRes); + if (!localCorr) { + collectErr.addAll(localRes); + } + else { + localRes.forEach(z -> z.addAll(y)); + x1Res.addAll(localRes); + } + return localCorr; + } + ).collect(Collectors.toCollection(HashSet::new)); + } + writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString()); + } + Set> x1ResPrime; + if (sameEqSet.isEmpty()) { + x1ResPrime = x1; + } + else { + x1ResPrime = x1Res; + } + result.get(0).add(x1ResPrime); + ZU LOESCHEN ENDE */ + result.get(0).add(x1); + if (x1.isEmpty()) { + undefined.add(pair); //Theta ist nicht im FC => Abbruch + } + } + else { + Set s1 = new HashSet<>(); + s1.add(pair); + Set> s2 = new HashSet<>(); + s2.add(s1); + result.get(0).add(s2); + } + + } + // Case 2: (a <.? ? ext Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) + if (first) { //writeLog(pair.toString()+"\n"); + Set> x1 = unifyCase2(pair, fc); + result.get(1).add(x1); + if (x1.isEmpty()) { + undefined.add(pair); //Theta ist nicht im FC + } + } + else { + Set s1 = new HashSet<>(); + s1.add(pair); + Set> s2 = new HashSet<>(); + s2.add(s1); + result.get(1).add(s2); + } + + // Case 3: (a <.? ? sup Theta') + else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) + if (first) { //writeLog(pair.toString()+"\n"); + Set> x1 = unifyCase3(pair, fc); + result.get(2).add(x1); + if (x1.isEmpty()) { + undefined.add(pair); //Theta ist nicht im FC + } + } + else { + Set s1 = new HashSet<>(); + s1.add(pair); + Set> s2 = new HashSet<>(); + s2.add(s1); + result.get(2).add(s2); + } + + // Case 4 was replaced by an inference rule + // Case 4: (a <.? Theta') + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) + // result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); + + // Case 5: (Theta <. a) + else if ((pairOp == PairOperator.SMALLERDOT) && rhsType instanceof PlaceholderType) + if (first) { //writeLog(pair.toString()+"\n"); + Set> x1 = unifyCase5(pair, fc); + result.get(4).add(x1); + if (x1.isEmpty()) { + undefined.add(pair); //Theta ist nicht im FC + } + } + else { + Set s1 = new HashSet<>(); + s1.add(pair); + Set> s2 = new HashSet<>(); + s2.add(s1); + result.get(4).add(s2); + } + + // Case 6 was replaced by an inference rule. + // Case 6: (? ext Theta <.? a) + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) + // result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); + + // Case 7 was replaced by an inference rule + // Case 7: (? sup Theta <.? a) + //else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) + // result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); + + // Case 8: (Theta <.? a) + else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) + if (first) { //writeLog(pair.toString()+"\n"); + Set> x1 = unifyCase8(pair, fc); + result.get(7).add(x1); + if (x1.isEmpty()) { + undefined.add(pair); //Theta ist nicht im FC + } + } + else { + Set s1 = new HashSet<>(); + s1.add(pair); + Set> s2 = new HashSet<>(); + s2.add(s1); + result.get(7).add(s2); + } + // Case unknown: If a pair fits no other case, then the type unification has failed. + // Through application of the rules, every pair should have one of the above forms. + // Pairs that do not have one of the aboves form are contradictory. + else { + // If a pair is not defined, the unificiation will fail, so the loop can be stopped here. + undefined.add(pair); + break; + } + first = false; + } + + // Filter empty sets or sets that only contain an empty set. + return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new))) + .filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); + } + + //TODO: Wenn Theta' nicht im FC muss ein Fehler produziert werden PL 18-04-20 + /** + * Cartesian product Case 1: (a <. Theta') + */ + protected Set> unifyCase1(UnifyPair pair, IFiniteClosure fc) { + PlaceholderType a = (PlaceholderType)pair.getLhsType(); + UnifyType thetaPrime = pair.getRhsType(); + + if (thetaPrime instanceof ExtendsType) { + thetaPrime = ((ExtendsType)thetaPrime).getExtendedType(); + } + + if (thetaPrime instanceof SuperType) { + //HIER MUSS NOCH WAS UEBERLEGT WERDEN + } + + Set> result = new HashSet<>(); + + if (thetaPrime instanceof ReferenceType && ((ReferenceType)thetaPrime).isGenTypeVar()) { + Set resultOne = new HashSet<>(); + resultOne.add(new UnifyPair (a, thetaPrime, PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + result.add(resultOne); + } + + boolean allGen = thetaPrime.getTypeParams().size() > 0; + for(UnifyType t : thetaPrime.getTypeParams()) + if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) { + allGen = false; + break; + } + //if (thetaPrime.getName().equals("java.util.Vector") //Fuer Bug 127 + // && thetaPrime instanceof ReferenceType + // && ((ReferenceType)thetaPrime).getTypeParams().iterator().next() instanceof PlaceholderType) //.getName().equals("java.util.Vector")) + // && ((ReferenceType)((ReferenceType)thetaPrime).getTypeParams().iterator().next()).getTypeParams().iterator().next().getName().equals("java.lang.Integer")) { + // { + // System.out.println(""); + //} + Set cs = fc.getAllTypesByName(thetaPrime.getName());//cs= [java.util.Vector, java.util.Vector>, ????java.util.Vector???] + + writeLog("cs: " + cs.toString()); + //PL 18-02-06 entfernt, kommt durch unify wieder rein + //cs.add(thetaPrime); + //PL 18-02-06 entfernt + + //cs muessen fresh Typvars gesetzt werden PL 2018-03-18 + Set csPHRenamed = cs.stream().map(x -> { + BinaryOperator> combiner = (aa,b) -> { aa.putAll(b); return aa;}; + HashMap hm = x.getInvolvedPlaceholderTypes().stream() + .reduce(new HashMap(), + (aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner); + return x.accept(new freshPlaceholder(), hm); + }).collect(Collectors.toCollection(HashSet::new)); + + IMatch match = new Match(); + for(UnifyType c : csPHRenamed) { + //PL 18-02-05 getChildren durch smaller ersetzt in getChildren werden die Varianlen nicht ersetzt. + Set thetaQs = new HashSet<>(); + //TODO smaller wieder reinnehmen? + //thetaQs.add(c);// + thetaQs = fc.smaller(c, new HashSet<>()).stream().collect(Collectors.toCollection(HashSet::new)); + ArrayList ml = new ArrayList<>(); + ml.add(new UnifyPair(c, thetaPrime, PairOperator.EQUALSDOT)); + if (!(match.match(ml)).isPresent()) { + thetaQs.remove(c); + } + writeLog("thetaQs von " + c + ": " + thetaQs.toString()); + //Set thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new)); + //thetaQs.add(thetaPrime); //PL 18-02-05 wieder geloescht + //PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert, + //da children offensichtlich ein echtes kleiner und kein kleinergleich ist + + //PL 18-02-06: eingefuegt, thetaQs der Form V> <. V'> werden entfernt + //TODO PL 19-01-14 wieder reinnehmen kurzfristig auskommentiert + //thetaQs = thetaQs.stream().filter(ut -> ut.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); + //PL 18-02-06: eingefuegt + + Set thetaQPrimes = new HashSet<>(); + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + + for(UnifyType param : cParams) + candidateParams.add(fc.grArg(param, new HashSet<>())); + + for(TypeParams tp : permuteParams(candidateParams)) + thetaQPrimes.add(c.setTypeParams(tp)); + } + writeLog("thetaQPrimes von " + c + ": " + thetaQPrimes.toString()); + for(UnifyType tqp : thetaQPrimes) {//PL 2020-03-08 umbauen in der Schleife wird nur unifizierbarer Typ gesucht break am Ende + Collection tphs = tqp.getInvolvedPlaceholderTypes(); + Optional opt = stdUnify.unify(tqp, thetaPrime); + if (!opt.isPresent()) { + continue; + } + Unifier unifier = opt.get(); + unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams()); + Set substitutionSet = new HashSet<>(); + for (Entry sigma : unifier) { + if (!tphs.contains(sigma.getKey())) {//eingefuegt PL 2019-02-02 Bug 127 + substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT, + //TODO: nochmals ueberlegen ob hier pair.getSubstitution() korrekt ist, oder ob leere Menge hin müsste + //alle folgenden New UnifyPair ebenfalls ueberpruefen PL 2018-04-19 + pair.getSubstitution(), pair)); + } + } + //List freshTphs = new ArrayList<>(); PL 18-02-06 in die For-Schleife verschoben + for (UnifyType tq : thetaQs) { + //geaendert PL 20-03-07 + Set smaller = new HashSet<>(); + smaller.add(unifier.apply(tq)); + //Set smaller = fc.smaller(unifier.apply(tq), new HashSet<>()); + //eingefuegt PL 2018-03-29 Anfang ? ext. theta hinzufuegen + if (a.isWildcardable()) { + Set smaller_ext = smaller.stream().filter(x -> !(x instanceof ExtendsType) && !(x instanceof SuperType)) + .map(x -> { + //BinaryOperator> combiner = (aa,b) -> { aa.putAll(b); return aa;}; //Variablenumbenennung rausgenommen + //HashMap hm = x.getInvolvedPlaceholderTypes().stream() //Variablen muessen wahrscheinlich erhalten bleiben + // .reduce(new HashMap(), + // (aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner); + return new ExtendsType (x);})//.accept(new freshPlaceholder(), hm));} + .collect(Collectors.toCollection(HashSet::new)); + smaller.addAll(smaller_ext); + } + //eingefuegt PL 2018-03-29 Ende ? ext. theta hinzufuegen + for(UnifyType theta : smaller) { + List freshTphs = new ArrayList<>(); + Set resultPrime = new HashSet<>(); + + for(int i = 0; !allGen && i < theta.getTypeParams().size(); i++) { + if(freshTphs.size()-1 < i)//IST DAS RICHTIG??? PL 2018-12-12 + freshTphs.add(PlaceholderType.freshPlaceholder()); + freshTphs.forEach(x -> ((PlaceholderType)x).setInnerType(true)); + resultPrime.add(new UnifyPair(freshTphs.get(i), theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair)); + } + + if(allGen) { + UnifyPair up = new UnifyPair(a, theta, PairOperator.EQUALSDOT, pair.getSubstitution(), pair); + Iterator upit = up.getRhsType().getTypeParams().iterator(); + //TODO PL 2019-01-24: upit.next() ist nicht unbedingt ein PlaceholderType -> Visitor erledigt + while (upit.hasNext()) upit.next().accept(new distributeVariance(), a.getVariance());//((PlaceholderType)upit.next()).setVariance(a.getVariance()); + resultPrime.add(up); + } + else { + UnifyPair up = new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT, pair.getSubstitution(), pair); + Iterator upit = up.getRhsType().getTypeParams().iterator(); + distributeVariance dv = new distributeVariance(); + //TODO PL 2019-01-24: upit.next() ist nicht unbedingt ein PlaceholderType -> Visitor erledigt + while (upit.hasNext()) upit.next().accept(new distributeVariance(), a.getVariance()); //((PlaceholderType)upit.next()).setVariance(a.getVariance()); + resultPrime.add(up); + } + resultPrime.addAll(substitutionSet); + //writeLog("Substitution: " + substitutionSet.toString()); + result.add(resultPrime); + //writeLog("Result: " + resultPrime.toString()); + //writeLog("MAX: " + oup.max(resultPrime.iterator()).toString()); + } + } + } + } + writeLog("result von " + pair + ": " + result.toString()); + return result; + } + + /** + * Cartesian Product Case 2: (a <.? ? ext Theta') + */ + private Set> unifyCase2(UnifyPair pair, IFiniteClosure fc) { + PlaceholderType a = (PlaceholderType) pair.getLhsType(); + ExtendsType extThetaPrime = (ExtendsType) pair.getRhsType(); + Set> result = new HashSet<>(); + + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance()); + ((PlaceholderType)aPrime).disableWildcardtable(); + UnifyType extAPrime = new ExtendsType(aPrime); + UnifyType thetaPrime = extThetaPrime.getExtendedType(); + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + //writeLog("Result: " + resultPrime.toString()); + return result; + } + + /** + * Cartesian Product Case 3: (a <.? ? sup Theta') + */ + private Set> unifyCase3(UnifyPair pair, IFiniteClosure fc) { + PlaceholderType a = (PlaceholderType) pair.getLhsType(); + a.reversVariance(); + SuperType subThetaPrime = (SuperType) pair.getRhsType(); + Set> result = new HashSet<>(); + + UnifyType aPrime = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance()); + ((PlaceholderType)aPrime).disableWildcardtable(); + UnifyType supAPrime = new SuperType(aPrime); + UnifyType thetaPrime = subThetaPrime.getSuperedType(); + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT, pair.getSubstitution(), pair, pair.getfBounded())); + result.add(resultPrime); + //writeLog(resultPrime.toString()); + + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + //writeLog(resultPrime.toString()); + + return result; + } + + /** + * Cartesian Product Case 5: (Theta <. a) + */ + private Set> unifyCase5(UnifyPair pair, IFiniteClosure fc) { + UnifyType theta = pair.getLhsType(); + PlaceholderType a = (PlaceholderType) pair.getRhsType(); + Set> result = new HashSet<>(); + + boolean allGen = theta.getTypeParams().size() > 0; + for(UnifyType t : theta.getTypeParams()) + if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) { + allGen = false; + break; + } + + //eingefuegt PL 2019-01-03 ANFANG + //fc.setLogTrue(); + //writeLog("FBOUNDED: " + pair.getfBounded()); + //writeLog("Pair: " + pair); + Set greater = fc.greater(theta, pair.getfBounded()); + //writeLog("GREATER: " + greater + pair + "THETA: " + theta + "FBOUNDED: " + pair.getfBounded() + " "); + if (a.isWildcardable()) { + Set greater_ext = greater.stream().filter(x -> !(x instanceof ExtendsType) && !(x instanceof SuperType)) + .map(x -> { + //BinaryOperator> combiner = (aa,b) -> { aa.putAll(b); return aa;}; //Variablenumbenennung rausgenommen + //HashMap hm = x.getInvolvedPlaceholderTypes().stream() //Variablen muessen wahrscheinlich erhalten bleiben + // .reduce(new HashMap(), + // (aa, b)-> { aa.put(b,PlaceholderType.freshPlaceholder()); return aa; }, combiner); + return new SuperType (x);})//.accept(new freshPlaceholder(), hm));} + .collect(Collectors.toCollection(HashSet::new)); + greater.addAll(greater_ext); + } + //eingefuegt PL 2019-01-03 ENDE + + //for(UnifyType thetaS : fc.greater(theta, pair.getfBounded())) { + for(UnifyType thetaS : greater) { + Set resultPrime = new HashSet<>(); + Match match = new Match(); + + UnifyType[] freshTphs = new UnifyType[thetaS.getTypeParams().size()]; + for(int i = 0; !allGen && i < freshTphs.length; i++) { + freshTphs[i] = PlaceholderType.freshPlaceholder(); + ((PlaceholderType)freshTphs[i]).setVariance(((PlaceholderType)a).getVariance()); + Set fBounded = new HashSet<>(pair.getfBounded()); //PL 2019-01-09 new HashSet eingefuegt + + int i_ef = i; + BiFunction f = (x,y) -> + { + ArrayList termList = new ArrayList(); + termList.add(new UnifyPair(y,thetaS.getTypeParams().get(i_ef), PairOperator.EQUALSDOT)); + return ((match.match(termList).isPresent()) || x); + }; + //if (parai.getName().equals("java.lang.Integer")) { + // System.out.println(""); + //} + BinaryOperator bo = (x,y) -> (x || y); + if (fBounded.stream().reduce(false,f,bo)) { + resultPrime.add(new UnifyPair(freshTphs[i], thetaS.getTypeParams().get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + } + else { + fBounded.add(thetaS.getTypeParams().get(i)); + resultPrime.add(new UnifyPair(thetaS.getTypeParams().get(i), freshTphs[i], PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair, fBounded)); + } + } + + if(allGen) + resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + else + resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + //writeLog("FBOUNDED2: " + pair.getfBounded()); + //writeLog("resultPrime Theta < a: " + greater + pair + "THETA: " + theta + "FBOUNDED: " + pair.getfBounded() + " " + resultPrime.toString()); + } + + return result; + } + + /** + * Cartesian Product Case 8: (Theta <.? a) + */ + private Set> unifyCase8(UnifyPair pair, IFiniteClosure fc) { + UnifyType theta = pair.getLhsType(); + PlaceholderType a = (PlaceholderType) pair.getRhsType(); + Set> result = new HashSet<>(); + //for(UnifyType thetaS : fc.grArg(theta)) { + Set resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + //writeLog(resultPrime.toString()); + + UnifyType freshTph = PlaceholderType.freshPlaceholder(); + + ((PlaceholderType)freshTph).setVariance(a.getVariance()); + ((PlaceholderType)freshTph).disableWildcardtable(); + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair, pair.getfBounded())); + result.add(resultPrime); + //writeLog("resultPrime: " + resultPrime.toString()); + + resultPrime = new HashSet<>(); + resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair)); + resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT, pair.getSubstitution(), pair)); + result.add(resultPrime); + //writeLog(resultPrime.toString()); + //} + + return result; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + */ + protected Set permuteParams(ArrayList> candidates) { + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new UnifyType[candidates.size()]); + return result; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + * @param idx Idx for the current permutatiton. + * @param result Set of all permutations found so far + * @param current The permutation of type params that is currently explored + */ + private void permuteParams(ArrayList> candidates, int idx, Set result, UnifyType[] current) { + if(candidates.size() == idx) { + result.add(new TypeParams(Arrays.copyOf(current, current.length))); + return; + } + + Set localCandidates = candidates.get(idx); + + for(UnifyType t : localCandidates) { + current[idx] = t; + permuteParams(candidates, idx+1, result, current); + } + } + + void writeLog(String str) { + synchronized ( this ) { + if (log && finalresult) { + try { + logFile.write("Thread no.:" + thNo + "\n"); + logFile.write("noOfThread:" + noOfThread + "\n"); + logFile.write("parallel:" + parallel + "\n"); + logFile.write(str+"\n\n"); + logFile.flush(); + + } + catch (IOException e) { + System.err.println("kein LogFile"); + } + } + } + } + + void writeStatistics(String str) { + if (finalresult) { + synchronized ( this ) { + try { + statistics.write("Thread No. " + thNo + ": " + str + "\n"); + statistics.flush(); + + } + catch (IOException e) { + System.err.println("kein StatisticsFile"); + } + }} + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/Unifikationsalgorithmus.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/Unifikationsalgorithmus.java new file mode 100644 index 0000000..39c25e5 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/Unifikationsalgorithmus.java @@ -0,0 +1,11 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +public interface Unifikationsalgorithmus { + + public Set> apply (Set E); + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultEvent.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultEvent.java new file mode 100644 index 0000000..0d420e4 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultEvent.java @@ -0,0 +1,18 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.sql.ResultSet; +import java.util.List; + + +public class UnifyResultEvent { + + private List newTypeResult; + + public UnifyResultEvent(List newTypeResult) { + this.newTypeResult = newTypeResult; + } + + public List getNewTypeResult() { + return newTypeResult; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListener.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListener.java new file mode 100644 index 0000000..f490ccd --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListener.java @@ -0,0 +1,7 @@ +package de.dhbwstuttgart.typeinference.unify; + +public interface UnifyResultListener { + + void onNewTypeResultFound(UnifyResultEvent evt); + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListenerImpl.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListenerImpl.java new file mode 100644 index 0000000..f66400b --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultListenerImpl.java @@ -0,0 +1,21 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.sql.ResultSet; +import java.util.ArrayList; +import java.util.List; + +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +public class UnifyResultListenerImpl implements UnifyResultListener { + + List results = new ArrayList<>(); + + public synchronized void onNewTypeResultFound(UnifyResultEvent evt) { + results.addAll(evt.getNewTypeResult()); + } + + public List getResults() { + return results; + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultModel.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultModel.java new file mode 100644 index 0000000..2168a65 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyResultModel.java @@ -0,0 +1,41 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.sql.ResultSet; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +public class UnifyResultModel { + + ConstraintSet cons; + + IFiniteClosure fc; + + public UnifyResultModel(ConstraintSet cons, + IFiniteClosure fc) { + this.cons = cons; + this.fc = fc; + } + + private List listeners = new ArrayList<>(); + + public void addUnifyResultListener(UnifyResultListener listenerToAdd) { + listeners.add(listenerToAdd); + } + + public void removeUnifyResultListener(UnifyResultListener listenerToRemove) { + listeners.remove(listenerToRemove); + } + + public void notify(Set> eqPrimePrimeSet) { + + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyTaskModel.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyTaskModel.java new file mode 100644 index 0000000..e60054f --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/UnifyTaskModel.java @@ -0,0 +1,18 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; + +public class UnifyTaskModel { + + ArrayList usedTasks = new ArrayList<>(); + + public synchronized void add(TypeUnifyTask t) { + usedTasks.add(t); + } + + public synchronized void cancel() { + for(TypeUnifyTask t : usedTasks) { + t.myCancel(true); + } + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/distributeVariance.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/distributeVariance.java new file mode 100644 index 0000000..1779c94 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/distributeVariance.java @@ -0,0 +1,54 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.UnifyType; + +public class distributeVariance extends visitUnifyTypeVisitor { + + public static int inverseVariance(int variance) { + Integer ret = 0; + if (variance == 1) { + ret = -1; + } + if (variance == -1) { + ret = 1; + } + return ret; + } + + + @Override + public PlaceholderType visit(PlaceholderType phty, Integer ht) { + if (ht != 0) { + if (phty.getVariance() == 0) { + phty.setVariance(ht); + } + //PL 2018-05-17 urspruengliche Variance nicht veraendern + //else if (phty.getVariance() != ht) { + // phty.setVariance(0); + //} + } + return phty; + } + + public FunNType visit(FunNType funnty, Integer ht) { + List param = new ArrayList<>(funnty.getTypeParams().get().length); + param.addAll(Arrays.asList(funnty.getTypeParams().get())); + UnifyType resultType = param.remove(param.size()-1); + Integer htInverse = inverseVariance(ht); + param = param.stream() + .map(x -> x.accept(this, htInverse)) + .collect(Collectors.toCollection(ArrayList::new)); + param.add(resultType.accept(this, ht)); + return FunNType.getFunNType(new TypeParams(param)); + } + + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/freshPlaceholder.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/freshPlaceholder.java new file mode 100644 index 0000000..69870bd --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/freshPlaceholder.java @@ -0,0 +1,15 @@ +package de.dhbwstuttgart.typeinference.unify; + + +import java.util.HashMap; + +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; + + +public class freshPlaceholder extends visitUnifyTypeVisitor> { + + @Override + public PlaceholderType visit(PlaceholderType phty, HashMap ht) { + return ht.get(phty); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java new file mode 100644 index 0000000..50371d3 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -0,0 +1,68 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.Optional; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.UnifyType; + +/** + * + * @author Florian Steurer + */ +public interface IFiniteClosure { + + public void setLogTrue(); + /** + * Returns all types of the finite closure that are subtypes of the argument. + * @return The set of subtypes of the argument. + */ + public Set smaller(UnifyType type, Set fBounded); + + /** + * Returns all types of the finite closure that are supertypes of the argument. + * @return The set of supertypes of the argument. + */ + public Set greater(UnifyType type, Set fBounded); + + /** + * Wo passt Type rein? + * @param type + * @return + */ + public Set grArg(UnifyType type, Set fBounded); + + /** + * Was passt in Type rein? + * @param type + * @return + */ + public Set smArg(UnifyType type, Set fBounded); + + public Set grArg(ReferenceType type, Set fBounded); + public Set smArg(ReferenceType type, Set fBounded); + + public Set grArg(ExtendsType type, Set fBounded); + public Set smArg(ExtendsType type, Set fBounded); + + public Set grArg(SuperType type, Set fBounded); + public Set smArg(SuperType type, Set fBounded); + + public Set grArg(PlaceholderType type, Set fBounded); + public Set smArg(PlaceholderType type, Set fBounded); + + public Set grArg(FunNType type, Set fBounded); + public Set smArg(FunNType type, Set fBounded); + + public Optional getLeftHandedType(String typeName); + public Set getAncestors(UnifyType t); + public Set getChildren(UnifyType t); + public Set getAllTypesByName(String typeName); + + public int compare(UnifyType rhsType, UnifyType rhsType2, PairOperator pairop); +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java new file mode 100644 index 0000000..a60de87 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java @@ -0,0 +1,29 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.unify.model.UnifyType; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +/** + * Match + * @author Martin Pluemicke + * abgeleitet aus IUnify.java + */ +public interface IMatch { + + /** + * Finds the most general matcher sigma of the set {t1 =. t1',...,tn =. tn'} so that + * sigma(t1) = t1' , ... sigma(tn) = tn'. + * @param terms The set of terms to be matched + * @return An optional of the most general matcher if it exists or an empty optional if there is no matcher. + */ + public Optional match(ArrayList termsList); + + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java new file mode 100644 index 0000000..bac6bcb --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java @@ -0,0 +1,103 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.List; +import java.util.Optional; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; + +/** + * Contains the inference rules that are applied to the set Eq. + * @author Florian Steurer + */ +public interface IRuleSet { + + public Optional reduceUp(UnifyPair pair); + public Optional reduceLow(UnifyPair pair); + public Optional reduceUpLow(UnifyPair pair); + public Optional> reduceExt(UnifyPair pair, IFiniteClosure fc); + public Optional> reduceSup(UnifyPair pair, IFiniteClosure fc); + public Optional> reduceEq(UnifyPair pair); + public Optional> reduce1(UnifyPair pair, IFiniteClosure fc); + public Optional> reduce2(UnifyPair pair); + + /* + * Missing Reduce-Rules for Wildcards + */ + public Optional reduceWildcardLow(UnifyPair pair); + public Optional reduceWildcardLowRight(UnifyPair pair); + public Optional reduceWildcardUp(UnifyPair pair); + public Optional reduceWildcardUpRight(UnifyPair pair); + + /* + * vgl. JAVA_BSP/Wildcard6.java + public Optional reduceWildcardLowUp(UnifyPair pair); + public Optional reduceWildcardUpLow(UnifyPair pair); + public Optional reduceWildcardLeft(UnifyPair pair); + */ + + /* + * Additional Rules which replace cases of the cartesian product + */ + + /** + * Rule that replaces the fourth case of the cartesian product where (a <.? Theta) + */ + public Optional reduceTph(UnifyPair pair); + + /** + * Rule that replaces the sixth case of the cartesian product where (? ext Theta <.? a) + */ + public Optional> reduceTphExt(UnifyPair pair); + + /** + * Rule that replaces the fourth case of the cartesian product where (? sup Theta <.? a) + */ + public Optional> reduceTphSup(UnifyPair pair); + + /* + * FunN Rules + */ + public Optional> reduceFunN(UnifyPair pair); + public Optional> greaterFunN(UnifyPair pair); + public Optional> smallerFunN(UnifyPair pair); + + /** + * Checks whether the erase1-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ + public boolean erase1(UnifyPair pair, IFiniteClosure fc); + + /** + * Checks whether the erase2-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ + public boolean erase2(UnifyPair pair, IFiniteClosure fc); + + /** + * Checks whether the erase3-Rule applies to the pair. + * @return True if the pair is erasable, false otherwise. + */ + public boolean erase3(UnifyPair pair); + + public Optional swap(UnifyPair pair); + + public Optional adapt(UnifyPair pair, IFiniteClosure fc); + public Optional adaptExt(UnifyPair pair, IFiniteClosure fc); + public Optional adaptSup(UnifyPair pair, IFiniteClosure fc); + + /** + * Applies the subst-Rule to a set of pairs (usually Eq'). + * @param pairs The set of pairs where the subst rule should apply. + * @return An optional of the modified set, if there were any substitutions. An empty optional if there were no substitutions. + */ + public Optional> subst(Set pairs, List>> oderConstraints); + + /** + * Applies the subst-Rule to a set of pairs (usually Eq'). + * @param pairs The set of pairs where the subst rule should apply. + * @return An optional of the modified set, if there were any substitutions. An empty optional if there were no substitutions. + */ + public Optional> subst(Set pairs); +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java new file mode 100644 index 0000000..cf0def3 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/ISetOperations.java @@ -0,0 +1,16 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.List; +import java.util.Set; + +/** + * Contains operations on sets. + * @author Florian Steurer + */ +public interface ISetOperations { + /** + * Calculates the cartesian product of the sets. + * @return The cartesian product + */ + Set> cartesianProduct(List> sets); +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java new file mode 100644 index 0000000..5647e18 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -0,0 +1,35 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.Arrays; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.unify.model.UnifyType; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; + +/** + * Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari) + * @author Florian Steurer + */ +public interface IUnify { + + /** + * Finds the most general unifier sigma of the set {t1 =. t1',...,tn =. tn'} so that + * sigma(t1) = sigma(t1') , ... sigma(tn) = sigma(tn'). + * @param terms The set of terms to be unified + * @return An optional of the most general unifier if it exists or an empty optional if there is no unifier. + */ + public Optional unify(Set terms); + + /** + * Finds the most general unifier sigma of the set {t1 =. t1',...,tn =. tn'} so that + * sigma(t1) = sigma(t1') , ... sigma(tn) = sigma(tn'). + * @param terms The set of terms to be unified + * @return An optional of the most general unifier if it exists or an empty optional if there is no unifier. + */ + default public Optional unify(UnifyType... terms) { + return unify(Arrays.stream(terms).collect(Collectors.toSet())); + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/UnifyTypeVisitor.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/UnifyTypeVisitor.java new file mode 100644 index 0000000..8d06b3e --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/interfaces/UnifyTypeVisitor.java @@ -0,0 +1,23 @@ +package de.dhbwstuttgart.typeinference.unify.interfaces; + +import java.util.HashMap; + +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; + +public interface UnifyTypeVisitor { + + public ReferenceType visit(ReferenceType refty, T ht); + + public PlaceholderType visit(PlaceholderType phty, T ht); + + public FunNType visit(FunNType funnty, T ht); + + public SuperType visit(SuperType suty, T ht); + + public ExtendsType visit(ExtendsType extty, T ht); + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java new file mode 100644 index 0000000..ef7e950 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java @@ -0,0 +1,96 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; + +/** + * An extends wildcard type "? extends T". + */ +public final class ExtendsType extends WildcardType { + + public UnifyType accept(UnifyTypeVisitor visitor, T ht) { + return visitor.visit(this, ht); + } + + /** + * Creates a new extends wildcard type. + * @param extendedType The extended type e.g. Integer in "? extends Integer" + */ + public ExtendsType(UnifyType extendedType) { + super("? extends " + extendedType.getName(), extendedType); + if (extendedType instanceof ExtendsType) { + System.out.print(""); + } + } + + /** + * The extended type e.g. Integer in "? extends Integer" + */ + public UnifyType getExtendedType() { + return wildcardedType; + } + + /** + * Sets the type parameters of the wildcarded type and returns a new extendstype that extends that type. + */ + @Override + public UnifyType setTypeParams(TypeParams newTp) { + UnifyType newType = wildcardedType.setTypeParams(newTp); + if(newType == wildcardedType) + return this; // Reduced the amount of objects created + return new ExtendsType(wildcardedType.setTypeParams(newTp)); + } + + @Override + Set smArg(IFiniteClosure fc, Set fBounded) { + return fc.smArg(this, fBounded); + } + + @Override + Set grArg(IFiniteClosure fc, Set fBounded) { + return fc.grArg(this, fBounded); + } + + @Override + UnifyType apply(Unifier unif) { + UnifyType newType = wildcardedType.apply(unif); + if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created + return new ExtendsType(newType); + } + + @Override + public int hashCode() { + /* + * It is important that the prime that is added is different to the prime added in hashCode() of SuperType. + * Otherwise ? extends T and ? super T have the same hashCode() for every Type T. + */ + return wildcardedType.hashCode() + 229; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof ExtendsType)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + ExtendsType other = (ExtendsType) obj; + + + return other.getWildcardedType().equals(wildcardedType); + } + + @Override + public String toString() { + return "? extends " + wildcardedType; + } + + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java new file mode 100644 index 0000000..5f047d0 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -0,0 +1,772 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.io.FileWriter; +import java.io.IOException; +import java.io.Writer; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Hashtable; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.function.BiFunction; +import java.util.function.BinaryOperator; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import com.google.common.collect.Ordering; + +//PL 18-02-05/18-04-05 Unifier durch Matcher ersetzt +//muss greater noch ersetzt werden ja erledigt 18--04-05 +import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify; + +import de.dhbwstuttgart.typeinference.unify.Match; +import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +import de.dhbwstuttgart.util.Pair; + +/** + * The finite closure for the type unification + * @author Florian Steurer + */ +public class FiniteClosure //extends Ordering //entfernt PL 2018-12-11 +implements IFiniteClosure { + + Writer logFile; + static Boolean log = false; + public void setLogTrue() { + log = true; + } + /** + * A map that maps every type to the node in the inheritance graph that contains that type. + */ + private HashMap> inheritanceGraph; + + /** + * A map that maps every typename to the nodes of the inheritance graph that contain a type with that name. + */ + private HashMap>> strInheritanceGraph; + + + /** + * The initial pairs of that define the inheritance tree + */ + private Set pairs; + + /** + * Hastable fuer die greater-Werte, damit sie nicht doppelt berechnet werden muessen + */ + Hashtable> greaterHash = new Hashtable<>(); + + /** + * Hastable fuer die smaller-Werte, damit sie nicht doppelt berechnet werden muessen + */ + Hashtable> smallerHash = new Hashtable<>(); + + /** + * Creates a new instance using the inheritance tree defined in the pairs. + */ + public FiniteClosure(Set pairs, Writer logFile) { + this.logFile = logFile; + this.pairs = new HashSet<>(pairs); + inheritanceGraph = new HashMap>(); + + // Build the transitive closure of the inheritance tree + for(UnifyPair pair : pairs) { + + /* + try { + logFile.write("Pair: " + pair + "\n"); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no LogFile"); + } + */ + + if(pair.getPairOp() != PairOperator.SMALLER) + continue; + + //VERSUCH PL 18-02-06 + //koennte ggf. die FC reduzieren + //TO DO: Ueberpruefen, ob das sinnvll und korrekt ist + //if (!pair.getLhsType().getTypeParams().arePlaceholders() + // && !pair.getRhsType().getTypeParams().arePlaceholders()) + // continue; +; + // Add nodes if not already in the graph + if(!inheritanceGraph.containsKey(pair.getLhsType())) + inheritanceGraph.put(pair.getLhsType(), new Node(pair.getLhsType())); + if(!inheritanceGraph.containsKey(pair.getRhsType())) + inheritanceGraph.put(pair.getRhsType(), new Node(pair.getRhsType())); + + Node childNode = inheritanceGraph.get(pair.getLhsType()); + Node parentNode = inheritanceGraph.get(pair.getRhsType()); + + // Add edge + parentNode.addDescendant(childNode); + + // Add edges to build the transitive closure + parentNode.getPredecessors().stream().forEach(x -> x.addDescendant(childNode)); + childNode.getDescendants().stream().forEach(x -> x.addPredecessor(parentNode)); + + //PL eingefuegt 2020-05-07 File UnitTest InheritTest.java + this.inheritanceGraph.forEach((x,y) -> { if (y.getDescendants().contains(parentNode)) { y.addDescendant(childNode); y.addAllDescendant(childNode.getDescendants());}; + if (y.getPredecessors().contains(childNode)) { y.addPredecessor(parentNode); y.addAllPredecessor(parentNode.getPredecessors());};} ); + } + + // Build the alternative representation with strings as keys + strInheritanceGraph = new HashMap<>(); + for(UnifyType key : inheritanceGraph.keySet()) { + if(!strInheritanceGraph.containsKey(key.getName())) + strInheritanceGraph.put(key.getName(), new HashSet<>()); + + strInheritanceGraph.get(key.getName()).add(inheritanceGraph.get(key)); + } + } + + void testSmaller() { + UnifyType tq1, tq2, tq3; + tq1 = new ExtendsType(PlaceholderType.freshPlaceholder()); + List l1 = new ArrayList<>(); + List l2 = new ArrayList<>(); + l1.add(tq1); + tq2 = new ReferenceType("java.util.Vector", new TypeParams(l1)); + l2.add(tq2); + tq3 = new ReferenceType("java.util.Vector", new TypeParams(l2)); + Set smaller = smaller(tq3, new HashSet<>()); + } + + /** + * Returns all types of the finite closure that are subtypes of the argument. + * @return The set of subtypes of the argument. + */ + @Override + public Set smaller(UnifyType type, Set fBounded) { + + Set ret; + if ((ret = smallerHash.get(new hashKeyType(type))) != null) { + //System.out.println(greaterHash); + return new HashSet<>(ret); + } + + if(type instanceof FunNType) + return computeSmallerFunN((FunNType) type, fBounded); + + Set>> ts = new HashSet<>(); + ts.add(new Pair<>(type, fBounded)); + Set result = computeSmaller(ts); + smallerHash.put(new hashKeyType(type), result); + /* + try { + logFile.write("\ntype: " + type + "\nret: " + ret + "\nresult: " + result);//"smallerHash: " + greaterHash.toString()); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no LogFile"); + }*/ + return result; + } + + /** + * Computes the smaller functions for every type except FunNTypes. + */ + private Set computeSmaller(Set>> types) { + Set>> result = new HashSet<>(); + + //PL 18-02-05 Unifier durch Matcher ersetzt + //IUnify unify = new MartelliMontanariUnify(); + Match match = new Match(); + + for(Pair> pt : types) { + UnifyType t = pt.getKey(); + Set fBounded = pt.getValue().get(); + + // if T = T' then T <* T' + try { + result.add(new Pair<>(t, fBounded)); + } + catch (StackOverflowError e) { + System.out.println(""); + } + + // if C<...> <* C<...> then ... (third case in definition of <*) + if(t.getTypeParams().size() > 0) { + ArrayList> paramCandidates = new ArrayList<>(); + for (int i = 0; i < t.getTypeParams().size(); i++) + paramCandidates.add(smArg(t.getTypeParams().get(i), fBounded)); + permuteParams(paramCandidates).forEach(x -> result.add(new Pair<>(t.setTypeParams(x), fBounded))); + } + + if(!strInheritanceGraph.containsKey(t.getName())) + continue; + + // if T <* T' then sigma(T) <* sigma(T') + Set> candidates = strInheritanceGraph.get(t.getName()); //cadidates= [???Node(java.util.Vector>)??? + // , Node(java.util.Vector) + //] + for(Node candidate : candidates) { + UnifyType theta2 = candidate.getContent(); + //PL 18-02-05 Unifier durch Matcher ersetzt ANFANG + ArrayList termList= new ArrayList(); + termList.add(new UnifyPair(theta2,t, PairOperator.EQUALSDOT)); + Optional optSigma = match.match(termList); + //PL 18-02-05 Unifier durch Matcher ersetzt ENDE + if(!optSigma.isPresent()) + continue; + + Unifier sigma = optSigma.get(); + sigma.swapPlaceholderSubstitutions(t.getTypeParams()); + + Set theta1Set = candidate.getContentOfDescendants(); + + for(UnifyType theta1 : theta1Set) + result.add(new Pair<>(theta1.apply(sigma), fBounded)); + } + } + + HashSet resut = result.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new)); + if(resut.equals(types.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new)))) + return resut; + return computeSmaller(result); + } + + /** + * Computes the smaller-Function for FunNTypes. + */ + private Set computeSmallerFunN(FunNType type, Set fBounded) { + Set result = new HashSet<>(); + + // if T = T' then T <=* T' + result.add(type); + + // Because real function types are implicitly variant + // it is enough to permute the params with the values of greater / smaller. + ArrayList> paramCandidates = new ArrayList<>(); + paramCandidates.add(smaller(type.getTypeParams().get(0), fBounded)); + for (int i = 1; i < type.getTypeParams().size(); i++) + paramCandidates.add(greater(type.getTypeParams().get(i), new HashSet<>())); + + permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x))); + return result; + } + + /** + * Returns all types of the finite closure that are supertypes of the argument. + * @return The set of supertypes of the argument. + */ + @Override + //Eingefuegt PL 2018-05-24 F-Bounded Problematik + public Set greater(UnifyType type, Set fBounded) { + + Set ret; + if ((ret = greaterHash.get(new hashKeyType(type))) != null) { + //System.out.println(greaterHash); + return new HashSet<>(ret); + } + + + if(type instanceof FunNType) { + return computeGreaterFunN((FunNType) type, fBounded); + } + + Set result = new HashSet<>(); + Set>> PairResultFBounded = new HashSet<>(); + + Match match = new Match(); + + + // if T = T' then T <=* T' + result.add(type); + if(!strInheritanceGraph.containsKey(type.getName())) + return result; + + // if T <* T' then sigma(T) <* sigma(T') + Set> candidates = strInheritanceGraph.get(type.getName()); + + /* + try { + if (log) logFile.write(candidates.toString()); + //log = false; + } + catch (IOException e) { + System.err.println("no LogFile"); + } + */ + + for(Node candidate : candidates) { + UnifyType theta1 = candidate.getContent(); + + //PL 18-04-05 Unifier durch Matcher ersetzt ANFANG + ArrayList termList= new ArrayList(); + termList.add(new UnifyPair(theta1,type, PairOperator.EQUALSDOT)); + Optional optSigma = match.match(termList); + //PL 18-04-05 Unifier durch Matcher ersetzt ENDE + if(!optSigma.isPresent()) { + continue; + } + Unifier sigma = optSigma.get(); + sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams()); + + Set fBoundedNew = new HashSet<>(fBounded); + fBoundedNew.add(theta1); + Set theta2Set = candidate.getContentOfPredecessors(); + //System.out.println(""); + for(UnifyType theta2 : theta2Set) { + result.add(theta2.apply(sigma)); + PairResultFBounded.add(new Pair<>(theta2.apply(sigma), fBoundedNew)); + } + } + /* + try { + if (log) logFile.write(PairResultFBounded.toString()); + log = false; + } + catch (IOException e) { + System.err.println("no LogFile"); + } + */ + for(Pair> pt : PairResultFBounded) { + UnifyType t = pt.getKey(); + Set lfBounded = pt.getValue().get(); + + // if C<...> <* C<...> then ... (third case in definition of <*) + //TypeParams typeparams = t.getTypeParams(); + if(t.getTypeParams().size() > 0) { + ArrayList> paramCandidates = new ArrayList<>(); + + for (int i = 0; i < t.getTypeParams().size(); i++) { + //UnifyType parai = t.getTypeParams().get(i); + int i_ef = i; + BiFunction f = (x,y) -> + { + ArrayList termList = new ArrayList(); + termList.add(new UnifyPair(y,t.getTypeParams().get(i_ef), PairOperator.EQUALSDOT)); + return ((match.match(termList).isPresent()) || x); + }; + //if (parai.getName().equals("java.lang.Integer")) { + // System.out.println(""); + //} + BinaryOperator bo = (a,b) -> (a || b); + if (lfBounded.stream().reduce(false,f,bo)) { + //F-Bounded Endlosrekursion + HashSet res = new HashSet(); + paramCandidates.add(res); + } + else { + paramCandidates.add(grArg(t.getTypeParams().get(i), new HashSet<>(fBounded) )); + } + } + permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x))); + //System.out.println(""); + } + } + + greaterHash.put(new hashKeyType(type), result); + /* + try { + logFile.write("\ntype: " + type + "\nret: " + ret + "\nresult: " + result);//"greaterHash: " + greaterHash.toString()); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no LogFile"); + }*/ + return result; + } + + /* auskommentiert PL 2018-05-24 + /** + * Returns all types of the finite closure that are supertypes of the argument. + * @return The set of supertypes of the argument. + * + //@Override + public Set oldgreater(UnifyType type, Set fBounded) { + if(type instanceof FunNType) + return computeGreaterFunN((FunNType) type, fBounded); + + Set>> ts = new HashSet<>(); + ts.add(new Pair<>(type, fBounded)); + return computeGreater(ts); + } + + /** + * Computes the greater function for all types except function types. + * + protected Set computeGreater(Set>> types) { + Set>> result = new HashSet<>(); + + //PL 18-04-05 Unifier durch Matcher ersetzt + //IUnify unify = new MartelliMontanariUnify(); + Match match = new Match(); + + for(Pair> pt : types) { + UnifyType t = pt.getKey(); + Set fBounded = pt.getValue().get(); + // if T = T' then T <=* T' + result.add(pt); + + // if C<...> <* C<...> then ... (third case in definition of <*) + if(t.getTypeParams().size() > 0) { + ArrayList> paramCandidates = new ArrayList<>(); + for (int i = 0; i < t.getTypeParams().size(); i++) { + UnifyType parai = t.getTypeParams().get(i); + int i_ef = i; + BiFunction f = (x,y) -> + { + ArrayList termList = new ArrayList(); + termList.add(new UnifyPair(y,t.getTypeParams().get(i_ef), PairOperator.EQUALSDOT)); + return ((match.match(termList).isPresent()) || x); + }; + if (parai.getName().equals("java.lang.Integer")) { + System.out.println(""); + } + BinaryOperator bo = (a,b) -> (a || b); + if (fBounded.stream().reduce(false,f,bo)) continue; //F-Bounded Endlosrekursion + paramCandidates.add(grArg(t.getTypeParams().get(i), new HashSet<>(fBounded) )); + } + permuteParams(paramCandidates).forEach(x -> result.add(new Pair<>(t.setTypeParams(x), new HashSet<>(fBounded)))); + } + + if(!strInheritanceGraph.containsKey(t.getName())) + continue; + + // if T <* T' then sigma(T) <* sigma(T') + Set> candidates = strInheritanceGraph.get(t.getName()); + for(Node candidate : candidates) { + UnifyType theta1 = candidate.getContent(); + + //PL 18-04-05 Unifier durch Matcher ersetzt ANFANG + ArrayList termList= new ArrayList(); + termList.add(new UnifyPair(theta1,t, PairOperator.EQUALSDOT)); + Optional optSigma = match.match(termList); + //PL 18-04-05 Unifier durch Matcher ersetzt ENDE + if(!optSigma.isPresent()) + continue; + + Unifier sigma = optSigma.get(); + sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams()); + + Set fBoundedNew = new HashSet<>(fBounded); + fBoundedNew.add(theta1); + Set theta2Set = candidate.getContentOfPredecessors(); + + for(UnifyType theta2 : theta2Set) + result.add(new Pair<>(theta2.apply(sigma), fBoundedNew)); + } + + } + + HashSet resut = result.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new)); + System.out.println(resut); + if(resut.equals(types.stream().map(x -> x.getKey()).collect(Collectors.toCollection(HashSet::new)))) + return resut; + return computeGreater(result); + } + */ + + /** + * Computes the greater function for FunN-Types + */ + protected Set computeGreaterFunN(FunNType type, Set fBounded) { + Set result = new HashSet<>(); + + // if T = T' then T <=* T' + result.add(type); + + // Because real function types are implicitly variant + // it is enough to permute the params with the values of greater / smaller. + ArrayList> paramCandidates = new ArrayList<>(); + paramCandidates.add(greater(type.getTypeParams().get(0), new HashSet<>())); + for (int i = 1; i < type.getTypeParams().size(); i++) + paramCandidates.add(smaller(type.getTypeParams().get(i), fBounded)); + permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x))); + return result; + } + + + @Override + public Set grArg(UnifyType type, Set fBounded) { + return type.grArg(this, fBounded); + } + + @Override + public Set grArg(ReferenceType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + smaller(type, fBounded).forEach(x -> result.add(new SuperType(x))); + greater(type,fBounded).forEach(x -> result.add(new ExtendsType(x))); + return result; + } + + @Override + public Set grArg(FunNType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + smaller(type, fBounded).forEach(x -> result.add(new SuperType(x))); + greater(type, fBounded).forEach(x -> result.add(new ExtendsType(x))); + return result; + } + + @Override + public Set grArg(ExtendsType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + UnifyType t = type.getExtendedType(); + greater(t, fBounded).forEach(x -> result.add(new ExtendsType(x))); + return result; + } + + @Override + public Set grArg(SuperType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + UnifyType t = type.getSuperedType(); + smaller(t, fBounded).forEach(x -> result.add(new SuperType(x))); + return result; + } + + @Override + public Set grArg(PlaceholderType type, Set fBounded) { + HashSet result = new HashSet<>(); + result.add(type); + return result; + } + + @Override + public Set smArg(UnifyType type, Set fBounded) { + return type.smArg(this, fBounded); + } + + @Override + public Set smArg(ReferenceType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + return result; + } + + @Override + public Set smArg(FunNType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + return result; + } + + @Override + public Set smArg(ExtendsType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + UnifyType t = type.getExtendedType(); + result.add(t); + smaller(t, fBounded).forEach(x -> { + result.add(new ExtendsType(x)); + result.add(x); + }); + return result; + } + + + @Override + public Set smArg(SuperType type, Set fBounded) { + Set result = new HashSet(); + result.add(type); + UnifyType t = type.getSuperedType(); + result.add(t); +//*** ACHTUNG das koennte FALSCH sein PL 2018-05-23 evtl. HashSet durch smArg durchschleifen + greater(t, fBounded).forEach(x -> { + result.add(new SuperType(x)); + result.add(x); + }); + return result; + } + + @Override + public Set smArg(PlaceholderType type, Set fBounded) { + HashSet result = new HashSet<>(); + result.add(type); + return result; + } + + @Override + public Set getAllTypesByName(String typeName) { + if(!strInheritanceGraph.containsKey(typeName)) + return new HashSet<>(); + return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new)); + } + + @Override + public Optional getLeftHandedType(String typeName) { + if(!strInheritanceGraph.containsKey(typeName)) + return Optional.empty(); + + for(UnifyPair pair : pairs) + if(pair.getLhsType().getName().equals(typeName) && pair.getLhsType().typeParams.arePlaceholders()) + return Optional.of(pair.getLhsType()); + + return Optional.empty(); + } + + @Override + public Set getAncestors(UnifyType t) { + if(!inheritanceGraph.containsKey(t)) + return new HashSet<>(); + Set result = inheritanceGraph.get(t).getContentOfPredecessors(); + result.add(t); + return result; + } + + @Override + public Set getChildren(UnifyType t) { + if(!inheritanceGraph.containsKey(t)) + return new HashSet<>(); + Set result = inheritanceGraph.get(t).getContentOfDescendants(); + result.add(t); + return result; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + */ + protected Set permuteParams(ArrayList> candidates) { + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new UnifyType[candidates.size()]); + return result; + } + + /** + * Takes a set of candidates for each position and computes all possible permutations. + * @param candidates The length of the list determines the number of type params. Each set + * contains the candidates for the corresponding position. + * @param idx Idx for the current permutatiton. + * @param result Set of all permutations found so far + * @param current The permutation of type params that is currently explored + */ + protected void permuteParams(ArrayList> candidates, int idx, Set result, UnifyType[] current) { + if(candidates.size() == idx) { + result.add(new TypeParams(Arrays.copyOf(current, current.length))); + return; + } + + Set localCandidates = candidates.get(idx); + + for(UnifyType t : localCandidates) { + current[idx] = t; + permuteParams(candidates, idx+1, result, current); + } + } + + @Override + public String toString(){ + return this.inheritanceGraph.toString(); + } + + /* entfernt PL 2018-12-11 + public int compare (UnifyType left, UnifyType right) { + return compare(left, right, PairOperator.SMALLERDOT); + } + */ + + public int compare (UnifyType left, UnifyType right, PairOperator pairop) { + //try {logFile.write("left: "+ left + " right: " + right + " pairop: " + pairop);} catch (IOException ie) {} + if (left.getName().equals("Matrix") || right.getName().equals("Matrix")) + System.out.println(""); + /* + pairop = PairOperator.SMALLERDOTWC; + List al = new ArrayList<>(); + PlaceholderType xx =new PlaceholderType("xx"); + al.add(xx); + left = new ExtendsType(new ReferenceType("Vector", new TypeParams(al))); + + List alr = new ArrayList<>(); + UnifyType exx = new ExtendsType(xx); + alr.add(exx); + right = new ExtendsType(new ReferenceType("Vector", new TypeParams(alr))); + */ + /* + List al = new ArrayList<>(); + PlaceholderType xx =new PlaceholderType("xx"); + al.add(xx); + left = new ExtendsType(xx); + right = xx; + */ + /* + List al = new ArrayList<>(); + PlaceholderType xx =new PlaceholderType("xx"); + PlaceholderType yy =new PlaceholderType("yy"); + al.add(xx); + left = yy; + right = new ExtendsType(xx); + */ + //Die Faelle abfangen, bei den Variablen verglichen werden PL 2018-12-11 + UnifyType ex; + if (left instanceof PlaceholderType) { + if ((right instanceof WildcardType) + && ((ex = ((WildcardType)right).wildcardedType) instanceof PlaceholderType) + && ((PlaceholderType)left).getName().equals(((PlaceholderType)ex).getName())) {// a <.? ? extends a oder a <.? ? super a + return -1; + } + else { + return 0; + } + } + if (right instanceof PlaceholderType) {//&& (left instanceof WildcardType)) {PL geloescht 2019-01-15 analog zu oben + if ((left instanceof WildcardType) //PL eingefuegt 2019-01-15 analog zu oben + && ((ex = ((WildcardType)left).wildcardedType) instanceof PlaceholderType) + && ((PlaceholderType)right).getName().equals(((PlaceholderType)ex).getName())) {// ? extends a <. a oder ? super a <. a + return 1; + } + else { + return 0; + } + } + UnifyPair up = new UnifyPair(left, right, pairop); + TypeUnifyTask unifyTask = new TypeUnifyTask(); + HashSet hs = new HashSet<>(); + hs.add(up); + Set smallerRes = unifyTask.applyTypeUnificationRules(hs, this); + /* + //if (left.getName().equals("Matrix") || right.getName().equals("Matrix")) + {try { + logFile.write("\nsmallerRes: " + smallerRes);//"smallerHash: " + greaterHash.toString()); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no LogFile");}} + */ + //Gleichungen der Form a <./=. Theta oder Theta <./=. a oder a <./=. b sind ok. + Predicate delFun = x -> !((x.getLhsType() instanceof PlaceholderType || + x.getRhsType() instanceof PlaceholderType) + && !((x.getLhsType() instanceof WildcardType) && //? extends/super a <.? a + ((WildcardType)x.getLhsType()).getWildcardedType().equals(x.getRhsType())) + ); + long smallerLen = smallerRes.stream().filter(delFun).count(); + if (smallerLen == 0) return -1; + else { + up = new UnifyPair(right, left, pairop); + //TypeUnifyTask unifyTask = new TypeUnifyTask(); + hs = new HashSet<>(); + hs.add(up); + Set greaterRes = unifyTask.applyTypeUnificationRules(hs, this); + /* + //if (left.getName().equals("Matrix") || right.getName().equals("Matrix")) + {try { + logFile.write("\ngreaterRes: " + greaterRes);//"smallerHash: " + greaterHash.toString()); + logFile.flush(); + } + catch (IOException e) { + System.err.println("no LogFile");}} + */ + //Gleichungen der Form a <./=. Theta oder Theta <./=. a oder a <./=. b sind ok. + long greaterLen = greaterRes.stream().filter(delFun).count(); + if (greaterLen == 0) return 1; + else { + //try {logFile.write("0 left: "+ left + " right: " + right + " pairop: " + pairop);} catch (IOException ie) {} + return 0; + } + } + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FunNType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FunNType.java new file mode 100644 index 0000000..f46ac91 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/FunNType.java @@ -0,0 +1,103 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; + +/** + * A real function type in java. + * @author Florian Steurer + */ +public class FunNType extends UnifyType { + + public UnifyType accept(UnifyTypeVisitor visitor, T ht) { + return visitor.visit(this, ht); + } + + /** + * Creates a FunN-Type with the specified TypeParameters. + */ + protected FunNType(TypeParams p) { + super("Fun"+(p.size()-1)+"$$", p); + } + + /** + * Creates a new FunNType. + * @param tp The parameters of the type. + * @return A FunNType. + * @throws IllegalArgumentException is thrown when there are to few type parameters or there are wildcard-types. + */ + public static FunNType getFunNType(TypeParams tp) throws IllegalArgumentException { + if(tp.size() == 0) + throw new IllegalArgumentException("FunNTypes need at least one type parameter"); + for(UnifyType t : tp) + if(t instanceof WildcardType) + throw new IllegalArgumentException("Invalid TypeParams for a FunNType: " + tp); + return new FunNType(tp); + } + + /** + * Returns the degree of the function type, e.g. 2 for FunN. + */ + public int getN() { + return typeParams.size()-1; + } + + @Override + public UnifyType setTypeParams(TypeParams newTp) { + if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) + return this; + return getFunNType(newTp); + } + + @Override + Set smArg(IFiniteClosure fc, Set fBounded) { + return fc.smArg(this, fBounded); + } + + @Override + Set grArg(IFiniteClosure fc, Set fBounded) { + return fc.grArg(this, fBounded); + } + + @Override + UnifyType apply(Unifier unif) { + // TODO this bypasses the validation of the type parameters. + // Wildcard types can be unified into FunNTypes. + TypeParams newParams = typeParams.apply(unif); + if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this; + + return new FunNType(newParams); + } + + @Override + public Boolean wrongWildcard() { + return (new ArrayList(Arrays.asList(getTypeParams() + .get())).stream().filter(x -> (x instanceof WildcardType)).findFirst().isPresent()); + } + + @Override + public int hashCode() { + return 181 + typeParams.hashCode(); + } + + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof FunNType)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + FunNType other = (FunNType) obj; + + return other.getTypeParams().equals(typeParams); + } + +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Node.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Node.java new file mode 100644 index 0000000..031130c --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Node.java @@ -0,0 +1,118 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashSet; +import java.util.Set; +import java.util.stream.Collectors; + +/** + * A node of a directed graph. + * @author Florian Steurer + * + * @param The type of the content of the node. + */ +class Node { + + /** + * The content of the node. + */ + private T content; + + /** + * The set of predecessors + */ + private HashSet> predecessors = new HashSet<>(); + + /** + * The set of descendants + */ + private HashSet> descendants = new HashSet<>(); + + /** + * Creates a node containing the specified content. + */ + public Node(T content) { + this.content = content; + } + + /** + * Adds a directed edge from this node to the descendant (this -> descendant) + */ + public void addDescendant(Node descendant) { + if(descendants.contains(descendant)) + return; + + descendants.add(descendant); + descendant.addPredecessor(this); + } + + /** + * Adds some directed edges from this node to the descendant (this -> descendant) + */ + public void addAllDescendant(Set> allDescendants) { + for(Node descendant: allDescendants) { + addDescendant(descendant); + } + } + + /** + * Adds a directed edge from the predecessor to this node (predecessor -> this) + */ + public void addPredecessor(Node predecessor) { + if(predecessors.contains(predecessor)) + return; + + predecessors.add(predecessor); + predecessor.addDescendant(this); + } + + /** + * Adds some directed edges from the predecessor to this node (predecessor -> this) + */ + public void addAllPredecessor(Set> allPredecessors) { + for(Node predecessor: allPredecessors) { + addPredecessor(predecessor); + } + } + + /** + * The content of this node. + */ + public T getContent() { + return content; + } + + /** + * Returns all predecessors (nodes that have a directed edge to this node) + */ + public Set> getPredecessors() { + return predecessors; + } + + /** + * Returns all descendants. All nodes M, where there is a edge from this node to the node M. + * @return + */ + public Set> getDescendants() { + return descendants; + } + + /** + * Retrieves the content of all descendants. + */ + public Set getContentOfDescendants() { + return descendants.stream().map(x -> x.getContent()).collect(Collectors.toSet()); + } + + /** + * Retrieves the content of all predecessors. + */ + public Set getContentOfPredecessors() { + return predecessors.stream().map(x -> x.getContent()).collect(Collectors.toSet()); + } + + @Override + public String toString() { + return "Elem: Node(" + content.toString() + ")\nPrec: " + getContentOfPredecessors().toString() + + "\nDesc: " + getContentOfDescendants().toString() + "\n\n"; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingExtend.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingExtend.java new file mode 100644 index 0000000..8fa3234 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingExtend.java @@ -0,0 +1,89 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Set; + +public abstract class OrderingExtend extends com.google.common.collect.Ordering { + + public List maxElements(Iterable iterable) { + ArrayList ret = new ArrayList<>(); + while (iterable.iterator().hasNext()) { + Set believe = new HashSet<>(); + + T max = max(iterable); + ret.add(max); + + Iterator it = iterable.iterator(); + while (it.hasNext()) { + T elem = it.next(); + if (!(compare(max, elem) == 1) && !max.equals(elem)) { + believe.add(elem); + } + } + iterable = believe; + } + return ret; + } + + public List minElements(Iterable iterable) { + ArrayList ret = new ArrayList<>(); + while (iterable.iterator().hasNext()) { + Set believe = new HashSet<>(); + + T min = min(iterable); + ret.add(min); + + Iterator it = iterable.iterator(); + while (it.hasNext()) { + T elem = it.next(); + if (!(compare(min, elem) == -1) && !min.equals(elem)) { + believe.add(elem); + } + } + iterable = believe; + } + return ret; + } + + + public List smallerEqThan(T elem, Iterable iterable) { + List ret = smallerThan(elem, iterable); + ret.add(elem); + return ret; + + } + + public List smallerThan(T elem, Iterable iterable) { + ArrayList ret = new ArrayList<>(); + Iterator it = iterable.iterator(); + while (it.hasNext()) { + T itElem = it.next(); + if (!itElem.equals(elem) && compare(elem, itElem) == 1) { + ret.add(itElem); + } + } + return ret; + } + + public List greaterEqThan(T elem, Iterable iterable) { + List ret = greaterThan(elem, iterable); + ret.add(elem); + return ret; + + } + + public List greaterThan(T elem, Iterable iterable) { + ArrayList ret = new ArrayList<>(); + Iterator it = iterable.iterator(); + while (it.hasNext()) { + T itElem = it.next(); + if (!itElem.equals(elem) && (compare(elem, itElem) == -1)) { + ret.add(itElem); + } + } + return ret; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java new file mode 100644 index 0000000..7e319a4 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java @@ -0,0 +1,457 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedList; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.function.BinaryOperator; +import java.util.function.Function; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import com.google.common.collect.Ordering; + +import de.dhbwstuttgart.typeinference.unify.Match; +import de.dhbwstuttgart.typeinference.unify.TypeUnifyTask; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.util.Pair; + + + +public class OrderingUnifyPair extends OrderingExtend> { + + protected IFiniteClosure fc; + + public OrderingUnifyPair(IFiniteClosure fc) { + this.fc = fc; + } + + /* + * vergleicht Paare (a =. Theta) und (a =. Theta') + * in dem compare(Theta, Theta') aufgerufen wird. + */ + public int compareEq (UnifyPair left, UnifyPair right) { + try { + //if (left.getRhsType() instanceof WildcardType || right.getRhsType() instanceof WildcardType) {//PL 2019-01-12 ausgetauscht + if (((PlaceholderType)left.getLhsType()).isInnerType() && ((PlaceholderType)right.getLhsType()).isInnerType()) { + return fc.compare(left.getRhsType(), right.getRhsType(), PairOperator.SMALLERDOTWC); + } + else { + return fc.compare(left.getRhsType(), right.getRhsType(), PairOperator.SMALLERDOT); + }} + catch (ClassCastException e) { + try { + ((FiniteClosure)fc).logFile.write("ClassCastException: " + left.toString() + " " + left.getGroundBasePair() + "\n\n"); + ((FiniteClosure)fc).logFile.flush(); + } + catch (IOException ie) { + } + return -99; + } + } + + /* + public int compareEq (UnifyPair left, UnifyPair right) { + if (left == null || right == null) + System.out.println("Fehler"); + if (left.getLhsType() instanceof PlaceholderType) { + return fc.compare(left.getRhsType(), right.getRhsType(), left.getPairOp()); + } + else { + return fc.compare(left.getLhsType(), right.getLhsType(), left.getPairOp()); + } + } + */ + + public Pair> compare (UnifyType left, UnifyType right) { + UnifyPair up; + if (left instanceof WildcardType || right instanceof WildcardType) { + up = new UnifyPair(left, right, PairOperator.SMALLERDOTWC); + if (((left instanceof ExtendsType) + && (((ExtendsType)left).getExtendedType().getName().equals("java.util.Vector")) + && (((ReferenceType)((ExtendsType)left).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)) || + ((right instanceof ExtendsType) + && (((ExtendsType)right).getExtendedType().getName().equals("java.util.Vector")) + && (((ReferenceType)((ExtendsType)right).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType))) + { + System.out.println(""); + } + if (((right instanceof SuperType) && (((SuperType)right).getSuperedType().getName().equals("java.lang.Object"))) + ||((left instanceof SuperType) && (((SuperType)left).getSuperedType().getName().equals("java.lang.Object")))) +{ + System.out.println(""); + } + } + else { + up = new UnifyPair(left, right, PairOperator.SMALLERDOT); + } + TypeUnifyTask unifyTask = new TypeUnifyTask(); + HashSet hs = new HashSet<>(); + hs.add(up); + Set smallerRes = unifyTask.applyTypeUnificationRules(hs, fc); + long smallerLen = smallerRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count(); + if (smallerLen == 0) return new Pair<>(-1, smallerRes); + else { + if (left instanceof WildcardType || right instanceof WildcardType) { + up = new UnifyPair(right, left, PairOperator.SMALLERDOTWC); + if (((left instanceof ExtendsType) + && (((ExtendsType)left).getExtendedType().getName().equals("java.util.Vector")) + && (((ReferenceType)((ExtendsType)left).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType)) || + ((right instanceof ExtendsType) + && (((ExtendsType)right).getExtendedType().getName().equals("java.util.Vector")) + && (((ReferenceType)((ExtendsType)right).getExtendedType()).getTypeParams().iterator().next() instanceof ExtendsType))) + { + System.out.println(""); + } + if (right instanceof SuperType) + { + System.out.println(""); + } + } + else { + up = new UnifyPair(right, left, PairOperator.SMALLERDOT); + } + //TypeUnifyTask unifyTask = new TypeUnifyTask(); + hs = new HashSet<>(); + hs.add(up); + Set greaterRes = unifyTask.applyTypeUnificationRules(hs, fc); + long greaterLen = greaterRes.stream().filter(x -> !(x.getLhsType() instanceof PlaceholderType && x.getRhsType() instanceof PlaceholderType)).count(); + if (greaterLen == 0) return new Pair<>(1, greaterRes); + else return new Pair<>(0, new HashSet<>()); + } + } + + /* TODO muss noch verifiziert werden PL 2018-03-21 + * (non-Javadoc) + * fuehrt zu Fehlern bei Arrays.sort (contract nicht erfuellt) + * @see com.google.common.collect.Ordering#compare(java.lang.Object, java.lang.Object) + */ + public int compare (Set leftpara, Set rightpara) { + + Set left = new HashSet<>(leftpara); + Set right = new HashSet<>(rightpara); + + /* + //pairop = PairOperator.SMALLERDOTWC; + List al = new ArrayList<>(); + PlaceholderType xx = PlaceholderType.freshPlaceholder(); + al.add(xx); + UnifyType t1 = new ExtendsType(new ReferenceType("Vector", new TypeParams(al))); + + //PlaceholderType yy =new PlaceholderType("yy"); + List alr = new ArrayList<>(); + UnifyType exx = new ExtendsType(xx); + alr.add(exx); + UnifyType t2 = new ExtendsType(new ReferenceType("Vector", new TypeParams(alr))); + + PlaceholderType a = PlaceholderType.freshPlaceholder(); + a.setInnerType(true); + UnifyPair p1 = new UnifyPair(a, t1, PairOperator.SMALLERDOTWC); + PlaceholderType b = PlaceholderType.freshPlaceholder(); + b.setInnerType(true); + UnifyPair p2 = new UnifyPair(b, t2, PairOperator.SMALLERDOTWC); + + List al3 = new ArrayList<>(); + al3.add(a); + + List al4 = new ArrayList<>(); + al4.add(b); + + UnifyPair p3 = new UnifyPair(new PlaceholderType("c"), new ReferenceType("Vector", new TypeParams(al3)), PairOperator.EQUALSDOT); + UnifyPair p4 = new UnifyPair(new PlaceholderType("c"), new ReferenceType("Vector", new TypeParams(al4)), PairOperator.EQUALSDOT); + + right = new HashSet<>(); + right.add(p1); + right.add(p3); + left = new HashSet<>(); + left.add(p2); + left.add(p4); + */ + + + Set lefteq = left.stream() + .filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)) + .collect(Collectors.toCollection(HashSet::new)); + Set righteq = right.stream() + .filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)) + .collect(Collectors.toCollection(HashSet::new)); + Set leftle = left.stream() + .filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType) + && x.getPairOp() == PairOperator.SMALLERDOT)) + .collect(Collectors.toCollection(HashSet::new)); + Set rightle = right.stream() + .filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType) + && x.getPairOp() == PairOperator.SMALLERDOT)) + .collect(Collectors.toCollection(HashSet::new)); + Set leftlewc = left.stream() + .filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType) + && x.getPairOp() == PairOperator.SMALLERDOTWC)) + .collect(Collectors.toCollection(HashSet::new)); + Set rightlewc = right.stream() + .filter(x -> ((x.getLhsType() instanceof PlaceholderType || x.getRhsType() instanceof PlaceholderType) + && x.getPairOp() == PairOperator.SMALLERDOTWC)) + .collect(Collectors.toCollection(HashSet::new)); + //System.out.println(left.toString()); + //Fall 2 + //if (lefteq.iterator().next().getLhsType().getName().equals("AJO")) { + // System.out.print(""); + //} + + //ODER-CONSTRAINT + Set leftBase = left.stream().map(x -> x.getGroundBasePair()).collect(Collectors.toCollection(HashSet::new)); + Set rightBase = right.stream().map(x -> x.getGroundBasePair()).collect(Collectors.toCollection(HashSet::new)); + + Set lefteqOder = left.stream() + .filter(x -> { UnifyPair y = x.getGroundBasePair(); + /*try { + ((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("y: " + y.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("y.getLhsType() : " + y.getLhsType() .toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("y.getRhsType(): " + y.getRhsType().toString() +"\n"); + ((FiniteClosure)fc).logFile.write("x.getPairOp(): " + x.getPairOp().toString() +"\n\n"); + } + catch (IOException ie) { + } */ + return (y.getLhsType() instanceof PlaceholderType && + !(y.getRhsType() instanceof PlaceholderType) && + x.getPairOp() == PairOperator.EQUALSDOT);}) + .collect(Collectors.toCollection(HashSet::new)); + left.removeAll(lefteqOder); + Set righteqOder = right.stream() + .filter(x -> { UnifyPair y = x.getGroundBasePair(); + return (y.getLhsType() instanceof PlaceholderType && + !(y.getRhsType() instanceof PlaceholderType) && + x.getPairOp() == PairOperator.EQUALSDOT);}) + .collect(Collectors.toCollection(HashSet::new)); + right.removeAll(righteqOder); + Set lefteqRet = left.stream() + .filter(x -> { UnifyPair y = x.getGroundBasePair(); + return (y.getRhsType() instanceof PlaceholderType && + ((PlaceholderType)y.getRhsType()).getOrCons() == (byte)-1);}) + .collect(Collectors.toCollection(HashSet::new)); + left.removeAll(lefteqRet); + Set righteqRet = right.stream() + .filter(x -> { UnifyPair y = x.getGroundBasePair(); + return (y.getRhsType() instanceof PlaceholderType && + ((PlaceholderType)y.getRhsType()).getOrCons() == (byte)-1);}) + .collect(Collectors.toCollection(HashSet::new)); + right.removeAll(righteqRet); + Set leftleOder = left.stream() + .filter(x -> (x.getPairOp() == PairOperator.SMALLERDOT)) + .collect(Collectors.toCollection(HashSet::new)); + Set rightleOder = right.stream() + .filter(x -> (x.getPairOp() == PairOperator.SMALLERDOT)) + .collect(Collectors.toCollection(HashSet::new)); + + /* + synchronized(this) { + try { + ((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("lefteqOder: " + lefteqOder.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("righteqOder: " + righteqOder.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("lefteqRet: " + lefteqRet.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("righteqRet: " + righteqRet.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("leftleOder: " + leftleOder.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("rightleOder: " + rightleOder.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.flush(); + } + catch (IOException ie) { + } + } + */ + + + Integer compareEq; + if (lefteqOder.size() == 1 && righteqOder.size() == 1 && lefteqRet.size() == 1 && righteqRet.size() == 1) { + Match m = new Match(); + if ((compareEq = compareEq(lefteqOder.iterator().next().getGroundBasePair(), righteqOder.iterator().next().getGroundBasePair())) == -1) { + ArrayList matchList = + rightleOder.stream().map(x -> { + UnifyPair leftElem = leftleOder.stream() + .filter(y -> y.getGroundBasePair().getLhsType().equals(x.getGroundBasePair().getLhsType())) + .findAny().get(); + return new UnifyPair(x.getRhsType(), leftElem.getRhsType(), PairOperator.EQUALSDOT);}) + .collect(Collectors.toCollection(ArrayList::new)); + if (m.match(matchList).isPresent()) { + //try { ((FiniteClosure)fc).logFile.write("result1: -1 \n\n"); } catch (IOException ie) {} + return -1; + } + else { + //try { ((FiniteClosure)fc).logFile.write("result1: 0 \n\n"); } catch (IOException ie) {} + return 0; + } + } else if (compareEq == 1) { + ArrayList matchList = + leftleOder.stream().map(x -> { + UnifyPair rightElem = rightleOder.stream() + .filter(y -> + y.getGroundBasePair().getLhsType().equals(x.getGroundBasePair().getLhsType())) + .findAny().get(); + return new UnifyPair(x.getRhsType(), rightElem.getRhsType(), PairOperator.EQUALSDOT);}) + .collect(Collectors.toCollection(ArrayList::new)); + if (m.match(matchList).isPresent()) { + //try { ((FiniteClosure)fc).logFile.write("result2: 1 \n\n"); } catch (IOException ie) {} + return 1; + } + else { + //try { ((FiniteClosure)fc).logFile.write("result2: 0 \n\n"); } catch (IOException ie) {} + return 0; + } + } else { + /* + synchronized(this) { + try { + ((FiniteClosure)fc).logFile.write("leftBase: " + leftBase.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("rightBase: " + rightBase.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("left: " + left.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("right: " + right.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("lefteqOder: " + lefteqOder.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("righteqOder: " + righteqOder.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("lefteqRet: " + lefteqRet.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("righteqRet: " + righteqRet.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("leftleOder: " + leftleOder.toString() +"\n"); + ((FiniteClosure)fc).logFile.write("rightleOder: " + rightleOder.toString() +"\n\n"); + ((FiniteClosure)fc).logFile.write("result3: 0 \n\n"); + ((FiniteClosure)fc).logFile.flush(); + } + catch (IOException ie) { + } + } + */ + return 0; + } + } + + + if (lefteq.size() == 1 && lefteq.iterator().next().getRhsType() instanceof ExtendsType && leftle.size() == 1 && righteq.size() == 0 && rightle.size() == 1) { + return 1; + } + //Fall 2 + if (lefteq.size() == 0 && leftle.size() == 1 && righteq.size() == 1 && righteq.iterator().next().getRhsType() instanceof ExtendsType && rightle.size() == 1) { + return -1; + } + //Fall 3 + if (lefteq.size() == 1 && lefteq.iterator().next().getRhsType() instanceof SuperType && leftle.size() == 1 && righteq.size() == 0 && rightle.size() == 1) { + return -1; + } + //Fall 3 + if (lefteq.size() == 0 && leftle.size() == 1 && righteq.size() == 1 && righteq.iterator().next().getRhsType() instanceof SuperType && rightle.size() == 1) { + return 1; + } + //Fall 5 + if (lefteq.size() == 1 && leftle.size() == 0 && righteq.size() == 1 && rightle.size() == 1) { + return -1; + } + //Fall 5 + if (lefteq.size() == 1 && leftle.size() == 1 && righteq.size() == 1 && rightle.size() == 0) { + return 1; + } + //Fall 5 + if (lefteq.size() == 1 && leftle.size() == 1 && righteq.size() == 1 && rightle.size() == 1) { + return 0; + } + // Nur Paare a =. Theta + if (leftle.size() == 0 && rightle.size() == 0 && leftlewc.size() == 0 && rightlewc.size() ==0) { + Stream lseq = lefteq.stream(); //left.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)); + Stream rseq = righteq.stream(); //right.filter(x -> (x.getLhsType() instanceof PlaceholderType && x.getPairOp() == PairOperator.EQUALSDOT)); + BinaryOperator> combiner = (x,y) -> { x.putAll(y); return x;}; + HashMap hm = rseq.reduce(new HashMap(), (x, y)-> { x.put(y.getLhsType(),y); return x; }, combiner); + lseq = lseq.filter(x -> !(hm.get(x.getLhsType()) == null));//NOCHMALS UEBERPRUEFEN!!!! + lseq = lseq.filter(x -> !x.equals(hm.get(x.getLhsType()))); //Elemente die gleich sind muessen nicht verglichen werden + Optional si = lseq.map(x -> compareEq(x, hm.get(x.getLhsType()))).reduce((x,y)-> { if (x == y) return x; else return 0; } ); + if (!si.isPresent()) return 0; + else return si.get(); + } + //Fall 1 und 4 + if (lefteq.size() >= 1 && righteq.size() >= 1 && (leftlewc.size() > 0 || rightlewc.size() > 0)) { + if (lefteq.iterator().next().getLhsType().getName().equals("D")) + System.out.print(""); + //Set varsleft = lefteq.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new)); + //Set varsright = righteq.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new)); + //filtern des Paares a = Theta, das durch a <. Thata' generiert wurde (nur im Fall 1 relevant) andere Substitutioen werden rausgefiltert + lefteq.removeIf(x -> (x.getBasePair()!=null) && !(x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName()) + ||x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())));//removeIf(x -> !varsright.contains(x.getLhsType())); + righteq.removeIf(x -> (x.getBasePair()!=null) && !(x.getLhsType().getName().equals(x.getBasePair().getLhsType().getName()) + ||x.getLhsType().getName().equals(x.getBasePair().getRhsType().getName())));//.removeIf(x -> !varsleft.contains(x.getLhsType())); + UnifyPair lseq = lefteq.iterator().next(); + UnifyPair rseq = righteq.iterator().next(); + if (lseq.getRhsType().getName().equals("Object")) { + if (rseq.getRhsType().getName().equals("Object")) return 0; + else return 1; + } + else { + if (rseq.getRhsType().getName().equals("Object")) return -1; + } + if (leftlewc.size() == rightlewc.size()) { + //TODO: Hier wird bei Wildcards nicht das richtige compare aufgerufen PL 18-04-20 + Pair> int_Unifier = compare(lseq.getRhsType(), rseq.getRhsType()); + Unifier uni = new Unifier(); + int_Unifier.getValue().get().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType())); + if (!lseq.getRhsType().getName().equals(rseq.getRhsType().getName()) + || leftlewc.size() == 0 || rightlewc.size() == 0) return int_Unifier.getKey(); + else { + Set lsleuni = leftlewc.stream().map(x -> uni.apply(x)).collect(Collectors.toCollection(HashSet::new)); + Set rsleuni = rightlewc.stream().map(x -> uni.apply(x)).collect(Collectors.toCollection(HashSet::new)); + BinaryOperator> combiner = (x,y) -> { x.putAll(y); return x;}; + + HashMap hm; + Optional si; + //1. Fall + if (leftlewc.iterator().next().getLhsType() instanceof PlaceholderType) { + hm = rsleuni.stream().reduce(new HashMap(), (x, y)-> { x.put(y.getLhsType(),y); return x; }, combiner); + Stream lslewcstr = lsleuni.stream().filter(x -> !(hm.get(x.getLhsType()) == null)); + si = lslewcstr.map(x -> fc.compare(x.getRhsType(), hm.get(x.getLhsType()).getRhsType(), PairOperator.SMALLERDOTWC)).reduce((x,y)-> { if (x == y) return x; else return 0; } ); + } + //4. Fall + else { + hm = rsleuni.stream().reduce(new HashMap(), (x, y)-> { x.put(y.getRhsType(),y); return x; }, combiner); + Stream lslewcstr = lsleuni.stream().filter(x -> !(hm.get(x.getRhsType()) == null)); + si = lslewcstr.map(x -> fc.compare(x.getLhsType(), hm.get(x.getRhsType()).getLhsType(), PairOperator.SMALLERDOTWC)).reduce((x,y)-> { if (x == y) return x; else return 0; } ); + } + if (!si.isPresent()) return 0; + else return si.get(); + } + } else { + if (leftlewc.size() > 0) { + Set subst; + subst = leftlewc.stream().map(x -> { + if (x.getLhsType() instanceof PlaceholderType) { + return new UnifyPair(x.getLhsType(), x.getRhsType(), PairOperator.EQUALSDOT); + } + else { + return new UnifyPair(x.getRhsType(), x.getLhsType(), PairOperator.EQUALSDOT); + }}).collect(Collectors.toCollection(HashSet::new)); + Unifier uni = new Unifier(); + lseq = uni.apply(lseq); + } + else { + Set subst; + subst = rightlewc.stream().map(x -> { + if (x.getLhsType() instanceof PlaceholderType) { + return new UnifyPair(x.getLhsType(), x.getRhsType(), PairOperator.EQUALSDOT); + } + else { + return new UnifyPair(x.getRhsType(), x.getLhsType(), PairOperator.EQUALSDOT); + }}).collect(Collectors.toCollection(HashSet::new)); + Unifier uni = new Unifier(); + subst.stream().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType())); + rseq = uni.apply(rseq); + } + return compareEq(lseq, rseq); + } + } + return 0; + } +} + diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/PairOperator.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/PairOperator.java new file mode 100644 index 0000000..ea323c7 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/PairOperator.java @@ -0,0 +1,49 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +/** + * Operators of pairs of the unification. + * @author Florian Steurer + */ +public enum PairOperator { + /** + * The smaller operator (T < P) is used to express a subtyping relation between + * T and P for example in the finite closure. It is necessarily true. + */ + SMALLER, + + /** + * The smallerdot operator (T <. P) is used to express a subtyping relation between + * of T and P in a CONSTRAINT during the unification. It is not necessarily true. + */ + SMALLERDOT, + + /** + * The smallernedot operator for arguments (T / ... with the Supertype Number + */ + SMALLERNEQDOT, + + /** + * The smallerdot operator for arguments (T <.? P) is used to express that + * T is an element of smArg(P) (or P is an element of grArg(T)) in a CONSTRAINT + * during the unification. It is not necessarily true. + */ + SMALLERDOTWC, + + /** + * The equalsdot operator (T =. P) is used to express that two types during the unification + * should be equal. It is not necessarily true. + */ + EQUALSDOT; + + @Override + public String toString() { + switch (this) { + case SMALLER: return "<"; + case SMALLERDOT: return "<."; + case SMALLERNEQDOT: return " EXISTING_PLACEHOLDERS = new ArrayList(); + + /** + * Prefix of auto-generated placeholder names. + */ + protected static String nextName = "gen_"; + + /** + * Random number generator used to generate fresh placeholder name. + */ + protected static Random rnd = new Random(43558747548978L); + + /** + * True if this object was auto-generated, false if this object was user-generated. + */ + private final boolean IsGenerated; + + + /** + * isWildcardable gibt an, ob ein Wildcardtyp dem PlaceholderType zugeordnet werden darf + */ + private boolean wildcardable = true; + + /** + * is innerType gibt an, ob der Type des PlaceholderType innerhalb eines Typkonstruktorsverwendet wird + */ + private boolean innerType = false; + + /** + * variance shows the variance of the pair + * -1: contravariant + * 1 covariant + * 0 invariant + * PL 2018-03-21 + */ + private int variance = 0; + + /* + * Fuer Oder-Constraints: + * orCons = 1: Receiver + * orCons = 0: Argument oder kein Oder-Constraint + * orCons = -1: RetType + */ + private byte orCons = 0; + + /** + * Creates a new placeholder type with the specified name. + */ + public PlaceholderType(String name) { + super(name, new TypeParams()); + EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names + IsGenerated = false; // This type is user generated + } + + /** + * Creates a new placeholdertype + * @param isGenerated true if this placeholder is auto-generated, false if it is user-generated. + */ + protected PlaceholderType(String name, boolean isGenerated) { + super(name, new TypeParams()); + EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names + IsGenerated = isGenerated; + } + + public UnifyType accept(UnifyTypeVisitor visitor, T ht) { + return visitor.visit(this, ht); + } + + /** + * Creates a fresh placeholder type with a name that does so far not exist. + * A user could later instantiate a type using the same name that is equivalent to this type. + * @return A fresh placeholder type. + */ + public synchronized static PlaceholderType freshPlaceholder() { + String name = nextName + (char) (rnd.nextInt(22) + 97); // Returns random char between 'a' and 'z' + // Add random chars while the name is in use. + while(EXISTING_PLACEHOLDERS.contains(name)) { + name += (char) (rnd.nextInt(22) + 97); // Returns random char between 'a' and 'z' + } + return new PlaceholderType(name, true); + } + + + /** + * True if this placeholder is auto-generated, false if it is user-generated. + */ + public boolean isGenerated() { + return IsGenerated; + } + + public void setVariance(int v) { + variance = v; + } + + public int getVariance() { + return variance; + } + + public void reversVariance() { + if (variance == 1) { + setVariance(-1); + } else { + if (variance == -1) { + setVariance(1); + }} + } + + public void setOrCons(byte i) { + orCons = i; + } + + public byte getOrCons() { + return orCons; + } + + public Boolean isWildcardable() { + return wildcardable; + } + public void disableWildcardtable() { + wildcardable = false; + } + + public void enableWildcardtable() { + wildcardable = true; + } + + public void setWildcardtable(Boolean wildcardable) { + this.wildcardable = wildcardable; + } + + public Boolean isInnerType() { + return innerType; + } + + public void setInnerType(Boolean innerType) { + this.innerType = innerType; + } + + @Override + Set smArg(IFiniteClosure fc, Set fBounded) { + return fc.smArg(this, fBounded); + } + + @Override + Set grArg(IFiniteClosure fc, Set fBounded) { + return fc.grArg(this, fBounded); + } + + @Override + public UnifyType setTypeParams(TypeParams newTp) { + return this; // Placeholders never have params. + } + + @Override + public int hashCode() { + return typeName.hashCode(); + } + + @Override + UnifyType apply(Unifier unif) { + if(unif.hasSubstitute(this)) { + UnifyType ret = unif.getSubstitute(this); + //PL 2018-05-17 Auskommentierung muesste korrekt sein, + //bereits in JavaTXComplier Variancen gesetzt werden. + //ret.accept(new distributeVariance(), this.getVariance()); + return ret; + } + return this; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof PlaceholderType)) + return false; + + return ((PlaceholderType) obj).getName().equals(typeName); + } + + + @Override + public Collection getInvolvedPlaceholderTypes() { + ArrayList ret = new ArrayList<>(); + ret.add(this); + return ret; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java new file mode 100644 index 0000000..62465b1 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/ReferenceType.java @@ -0,0 +1,100 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashMap; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; + +/** + * A reference type e.q. Integer or List. + * @author Florian Steurer + * + */ +public class ReferenceType extends UnifyType { + + /** + * The buffered hashCode + */ + private final int hashCode; + + /** + * gibt an, ob der ReferenceType eine generische Typvariable ist + */ + private final boolean genericTypeVar; + + + public UnifyType accept(UnifyTypeVisitor visitor, T ht) { + return visitor.visit(this, ht); + } + + public ReferenceType(String name, Boolean genericTypeVar) { + super(name, new TypeParams()); + hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); + this.genericTypeVar = genericTypeVar; + } + + public ReferenceType(String name, UnifyType... params) { + super(name, new TypeParams(params)); + hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); + genericTypeVar = false; + } + + public ReferenceType(String name, TypeParams params) { + super(name, params); + hashCode = 31 + 17 * typeName.hashCode() + 17 * typeParams.hashCode(); + genericTypeVar = false; + } + + public boolean isGenTypeVar () { + return genericTypeVar; + } + + @Override + Set smArg(IFiniteClosure fc, Set fBounded) { + return fc.smArg(this, fBounded); + } + + @Override + Set grArg(IFiniteClosure fc, Set fBounded) { + return fc.grArg(this, fBounded); + } + + @Override + UnifyType apply(Unifier unif) { + TypeParams newParams = typeParams.apply(unif); + + if(newParams.hashCode() == typeParams.hashCode() && newParams.equals(typeParams)) + return this; + + return new ReferenceType(typeName, newParams); + } + + @Override + public UnifyType setTypeParams(TypeParams newTp) { + if(newTp.hashCode() == typeParams.hashCode() && newTp.equals(typeParams)) + return this; // reduced the amount of objects created + return new ReferenceType(typeName, newTp); + } + + @Override + public int hashCode() { + return hashCode; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof ReferenceType)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + ReferenceType other = (ReferenceType) obj; + + if(!other.getName().equals(typeName)) + return false; + + return other.getTypeParams().equals(typeParams); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/SuperType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/SuperType.java new file mode 100644 index 0000000..50b8dcf --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -0,0 +1,88 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashMap; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; + +/** + * A super wildcard type e.g. ? super Integer. + * @author Florian Steurer + */ +public final class SuperType extends WildcardType { + + public UnifyType accept(UnifyTypeVisitor visitor, T ht) { + return visitor.visit(this, ht); + } + + /** + * Creates a new instance "? extends superedType" + * @param superedType The type that is supered e.g. Integer in "? super Integer" + */ + public SuperType(UnifyType superedType) { + super("? super " + superedType.getName(), superedType); + } + + /** + * The type that is supered e.g. Integer in "? super Integer" + */ + public UnifyType getSuperedType() { + return wildcardedType; + } + + @Override + public String toString() { + return "? super " + wildcardedType; + } + + /** + * Sets the type parameters of the wildcarded type and returns a new supertype that supers that type. + */ + @Override + public UnifyType setTypeParams(TypeParams newTp) { + UnifyType newType = wildcardedType.setTypeParams(newTp); + if(newType == wildcardedType) + return this; // Reduced the amount of objects created + return new SuperType(wildcardedType.setTypeParams(newTp)); + } + + @Override + Set smArg(IFiniteClosure fc, Set fBounded) { + return fc.smArg(this, fBounded); + } + + @Override + Set grArg(IFiniteClosure fc, Set fBounded) { + return fc.grArg(this, fBounded); + } + + @Override + UnifyType apply(Unifier unif) { + UnifyType newType = wildcardedType.apply(unif); + if(newType.hashCode() == wildcardedType.hashCode() && newType.equals(wildcardedType)) + return this; // Reduced the amount of objects created + return new SuperType(newType); + } + + @Override + public int hashCode() { + /* + * It is important that the prime that is added is different to the prime added in hashCode() of ExtendsType. + * Otherwise ? extends T and ? super T have the same hashCode() for every Type T. + */ + return wildcardedType.hashCode() + 3917; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof SuperType)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + SuperType other = (SuperType) obj; + return other.getSuperedType().equals(wildcardedType); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java new file mode 100644 index 0000000..f70cccb --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -0,0 +1,191 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.*; + + +/** + * The generic or non-generic parameters of a type e.g. for List + * @author Florian Steurer + */ +public final class TypeParams implements Iterable{ + /** + * The array which backs the type parameters. + */ + private final UnifyType[] typeParams; + + /** + * Hashcode calculation is expensive and must be cached. + */ + private final int hashCode; + + /** + * Creates a new set of type parameters. + * @param types The type parameters. + */ + public TypeParams(List types){ + typeParams = new UnifyType[types.size()]; + for(int i=0;i x instanceof PlaceholderType); + } + + /** + * Returns the number of the type parameters in this object. + * @return number of type parameters, always positive (including 0). + */ + public int size() { + return typeParams.length; + } + + /** + * Returns true if this object has size() of zero, false otherwise. + */ + public boolean empty() { + return typeParams.length == 0; + } + + /** + * Applies a unifier to every parameter in this object. + * @param unif The applied unifier. + * @return A new type parameter object, where the unifier was applied to every parameter. + */ + public TypeParams apply(Unifier unif) { + UnifyType[] newParams = new UnifyType[typeParams.length]; + + // If true, a type was modified and a new typeparams object has to be created. + // Otherwise it is enough to return this object, since it is immutable + // This reduced the needed TypeParams-Instances for the lambda14-Test from + // 130.000 to 30.000 without a decrease in speed. + boolean isNew = false; + + for(int i = 0; i < typeParams.length; i++) { + UnifyType newType = typeParams[i].apply(unif); + newParams[i] = newType; + if(!isNew && (newType.hashCode() != typeParams[i].hashCode() || !newType.equals(typeParams[i]))) + isNew = true; + } + + if(!isNew) + return this; + return new TypeParams(newParams); + } + + /** + * True if the PlaceholderType t is a parameter of this object, or if any parameter + * contains t (arbitrary depth of recursion), false otherwise. + */ + public boolean occurs(PlaceholderType t) { + for(UnifyType p : typeParams) + if(p instanceof PlaceholderType) {//PL 2018-01-31 dangeling else Problem { ... } eingefuegt. + if(p.equals(t)) + return true; + } + else { + if(p.getTypeParams().occurs(t)) + return true; } + return false; + } + + /** + * Returns the i-th parameter of this object. + */ + public UnifyType get(int i) { + return typeParams[i]; + } + + /** + * Returns the parameters of this object. + * PL 2018-03-17 + */ + public UnifyType[] get() { + return typeParams; + } + + /** + * Sets the the type t as the i-th parameter and returns a new object + * that equals this object, except for the i-th type. + */ + public TypeParams set(UnifyType t, int idx) { + // Reduce the creation of new objects for less memory + // Reduced the needed instances of TypeParams in the lambda14-Test from + // 150.000 to 130.000 + if(t.hashCode() == typeParams[idx].hashCode() && t.equals(typeParams[idx])) + return this; + UnifyType[] newparams = Arrays.copyOf(typeParams, typeParams.length); + newparams[idx] = t; + return new TypeParams(newparams); + } + + @Override + public Iterator iterator() { + return Arrays.stream(typeParams).iterator(); + } + + @Override + public int hashCode() { + return hashCode; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof TypeParams)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + TypeParams other = (TypeParams) obj; + + if(other.size() != this.size()) + return false; + + for(int i = 0; i < this.size(); i++){ + //if(this.get(i) == null) + //System.out.print("s"); + } + for(int i = 0; i < this.size(); i++) + if(!(this.get(i).equals(other.get(i)))) + return false; + + return true; + } + + @Override + public String toString() { + String res = ""; + for(UnifyType t : typeParams) + res += t + ","; + return "<" + res.substring(0, res.length()-1) + ">"; + } + + public Collection getInvolvedPlaceholderTypes() { + ArrayList ret = new ArrayList<>(); + for(UnifyType t : typeParams){ + ret.addAll(t.getInvolvedPlaceholderTypes()); + } + return ret; + } +} + diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Unifier.java new file mode 100644 index 0000000..8cfac64 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -0,0 +1,189 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Map.Entry; +import java.util.Set; +import java.util.function.Function; + +/** + * A set of substitutions (s -> t) that is an applicable function to types and pairs. + * @author Florian Steurer + */ +public class Unifier implements Function, Iterable> { + + /** + * The set of substitutions that unify a type-term + */ + private HashMap substitutions = new HashMap<>(); + + /** + * Creates a new instance with a single substitution (source -> target). + * @param The type that is replaced + * @param The type that replaces + */ + public Unifier(PlaceholderType source, UnifyType target) { + substitutions.put(source, target); + } + + /** + * Identity function as an "unifier". + */ + protected Unifier() { + + } + + /** + * Creates an unifier that is the identity function (thus has no substitutions). + */ + public static Unifier identity() { + return new Unifier(); + } + + /** + * Adds a substitution to the unifier from (source -> target) + * @param The type that is replaced + * @param The type that replaces + */ + public void add(PlaceholderType source, UnifyType target) { + Unifier tempU = new Unifier(source, target); + // Every new substitution must be applied to previously added substitutions + // otherwise the unifier needs to be applied multiple times to unify two terms + for(PlaceholderType pt : substitutions.keySet()) + substitutions.put(pt, substitutions.get(pt).apply(tempU)); + substitutions.put(source, target); + } + + @Override + public UnifyType apply(UnifyType t) { + return t.apply(this); + } + + /** + * Applies the unifier to the two terms of the pair. + * @return A new pair where the left and right-hand side are applied + */ + public UnifyPair apply(UnifyPair p) { + UnifyType newLhs = this.apply(p.getLhsType()); + UnifyType newRhs = this.apply(p.getRhsType()); + return new UnifyPair(newLhs, newRhs, p.getPairOp()); + } + + /** + * Applies the unifier to the two terms of the pair. + * works only for single subsitution + * @return A new pair where the left and right-hand side are applied + */ + public UnifyPair apply(UnifyPair thisAsPair, UnifyPair p) { + UnifyType newLhs = this.apply(p.getLhsType()); + UnifyType newRhs = this.apply(p.getRhsType()); + //Varianceweitergabe wird nicht benoetigt. + //PlaceholderType lhsph = (PlaceholderType)thisAsPair.getLhsType(); + //if (lhsph.getVariance() != 0) { + // if (p.getLhsType().equals(lhsph)) { + // if (p.getRhsType() instanceof PlaceholderType) { + // ((PlaceholderType)p.getRhsType()).setVariance(lhsph.getVariance()); + // } + // } + // if (p.getRhsType().equals(lhsph)) { + // if (p.getLhsType() instanceof PlaceholderType) { + // ((PlaceholderType)p.getLhsType()).setVariance(lhsph.getVariance()); + // } + // } + //} + if (!(p.getLhsType().equals(newLhs)) || !(p.getRhsType().equals(newRhs))) {//Die Anwendung von this hat was veraendert PL 2018-04-01 + Set suniUnifyPair = new HashSet<>(); + suniUnifyPair.addAll(thisAsPair.getAllSubstitutions()); + suniUnifyPair.add(thisAsPair); + if (p.getLhsType() instanceof PlaceholderType //&& newLhs instanceof PlaceholderType entfernt PL 2018-04-13 + && p.getPairOp() == PairOperator.EQUALSDOT) { + suniUnifyPair.add(p); //p koennte auch subsitution sein + } + return new UnifyPair(newLhs, newRhs, p.getPairOp(), suniUnifyPair, p); + } + return new UnifyPair(newLhs, newRhs, p.getPairOp(), p.getSubstitution(), p.getBasePair(), p.getfBounded()); + } + + /** + * Applies the unifier to the left terms of the pair. + * @return A new pair where the left and right-hand side are applied + */ + public UnifyPair applyleft(UnifyPair p) { + return new UnifyPair(this.apply(p.getLhsType()), p.getRhsType(), p.getPairOp()); + } + + /** + * True if the typevariable t will be substituted if the unifier is applied. + * false otherwise. + */ + public boolean hasSubstitute(PlaceholderType t) { + return substitutions.containsKey(t); + } + + /** + * Returns the type that will replace the typevariable t if the unifier is applied. + */ + public UnifyType getSubstitute(PlaceholderType t) { + return substitutions.get(t); + } + + /** + * The number of substitutions in the unifier. If zero, this is the identity function. + */ + public int size() { + return substitutions.size(); + } + + /** + * Garantuees that if there is a substitutions (a -> b) in this unifier, + * a is not an element of the targetParams. Substitutions that do not + * satisfy this condition, are swapped. + */ + public void swapPlaceholderSubstitutions(Iterable targetParams) { + for(UnifyType tph : targetParams) { + if(!(tph instanceof PlaceholderType)) + continue; + // Swap a substitutions (a -> b) if a is an element of the target params. + if(substitutions.containsKey(tph)) { + if((substitutions.get(tph) instanceof PlaceholderType)) { + PlaceholderType newLhs = (PlaceholderType) substitutions.get(tph); + substitutions.remove(tph); + substitutions.put(newLhs, tph); + } + } + } + } + + public void swapPlaceholderSubstitutionsReverse(Iterable sourceParams) { + for(UnifyType tph : sourceParams) { + if(!(tph instanceof PlaceholderType)) + continue; + if(substitutions.containsValue(tph)) { + UnifyType key = substitutions.values().stream().filter(x -> x.equals(tph)).findAny().get(); + if(key instanceof PlaceholderType) { + PlaceholderType newLhs = (PlaceholderType) tph; + substitutions.remove(key); + substitutions.put(newLhs, key); + } + } + } + } + + @Override + public String toString() { + String result = "{ "; + for(Entry entry : substitutions.entrySet()) + result += "(" + entry.getKey() + " -> " + entry.getValue() + "), "; + if(!substitutions.isEmpty()) + result = result.substring(0, result.length()-2); + result += " }"; + return result; + } + + @Override + public Iterator> iterator() { + return substitutions.entrySet().iterator(); + } +} + diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java new file mode 100644 index 0000000..497fd81 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java @@ -0,0 +1,247 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; + + +/** + * A pair which contains two types and an operator, e.q. (Integer <. a). + * @author Florian Steurer + */ +public class UnifyPair { + + /** + * The type on the left hand side of the pair. + */ + private final UnifyType lhs; + + /** + * The type on the right hand side of the pair. + */ + private final UnifyType rhs; + + /** + * The operator that determines the relation between the left and right hand side type. + */ + private PairOperator pairOp; + + private boolean undefinedPair = false; + + /** + * Unifier/substitute that generated this pair + * PL 2018-03-15 + */ + private Set substitution; + + /** + * Base on which the the unifier is applied + * PL 2018-03-15 + */ + private UnifyPair basePair; + + /** + * For pairs a <. Theta generated in the rule reduceTphSup + * to store the f-Bouned Elements to avoid endless recursion + * PL 2018-03-15 + */ + private Set fBounded = new HashSet<>(); + + private final int hashCode; + + /** + * Creates a new instance of the pair. + * @param lhs The type on the left hand side of the pair. + * @param rhs The type on the right hand side of the pair. + * @param op The operator that determines the relation between the left and right hand side type. + */ + public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op) { + this.lhs = lhs; + this.rhs = rhs; + pairOp = op; + substitution = new HashSet<>(); + + // Caching hashcode + hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode(); + } + + public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Set uni, UnifyPair base) { + this.lhs = lhs; + this.rhs = rhs; + pairOp = op; + substitution = uni; + basePair = base; + + + // Caching hashcode + hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode(); + } + + public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Set uni, UnifyPair base, Set fBounded) { + this(lhs, rhs, op, uni, base); + + this.fBounded = fBounded; + } + + /** + * Returns the type on the left hand side of the pair. + */ + public UnifyType getLhsType() { + return lhs; + } + + /** + * Returns the type on the right hand side of the pair. + */ + public UnifyType getRhsType() { + return rhs; + } + + /** + * Returns the operator that determines the relation between the left and right hand side type. + */ + public PairOperator getPairOp() { + return pairOp; + } + + public void setPairOp(PairOperator po) { + pairOp = po; + } + + public void addSubstitutions(Set sup) { + substitution.addAll(sup); + } + + public void setUndefinedPair() { + undefinedPair = true; + } + public Set getSubstitution() { + return new HashSet<>(substitution); + } + + public UnifyPair getBasePair() { + return basePair; + } + public boolean isUndefinedPair() { + return undefinedPair; + } + + public Set getAllSubstitutions () { + Set ret = new HashSet<>(); + ret.addAll(new ArrayList<>(getSubstitution())); + if (basePair != null) { + ret.addAll(new ArrayList<>(basePair.getAllSubstitutions())); + } + return ret; + } + + public Set getThisAndAllBases () { + Set ret = getAllBases(); + ret.add(this); + return ret; + } + public Set getAllBases () { + Set ret = new HashSet<>(); + if (basePair != null) { + ret.add(getBasePair()); + ret.addAll(basePair.getAllBases()); + } + return ret; + } + + public UnifyPair getGroundBasePair () { + if (basePair == null) { + return this; + } + if (basePair.getBasePair() == null) { + return basePair; + } + else { + return basePair.getGroundBasePair(); + } + } + + /** + * wenn in einem Paar bestehend aus 2 Typvariablen eine nicht wildcardtable ist, + * so beide auf nicht wildcardtable setzen + */ + public void disableCondWildcards() { + if (lhs instanceof PlaceholderType && rhs instanceof PlaceholderType + && (!((PlaceholderType)lhs).isWildcardable() || !((PlaceholderType)rhs).isWildcardable())) + { + ((PlaceholderType)lhs).disableWildcardtable(); + ((PlaceholderType)rhs).disableWildcardtable(); + } + + } + + public Boolean wrongWildcard() { + return lhs.wrongWildcard() || rhs.wrongWildcard(); + } + + public Set getfBounded() { + return this.fBounded; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof UnifyPair)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + UnifyPair other = (UnifyPair) obj; + + if (isUndefinedPair()) { + if (other.getBasePair() != basePair || (other.getBasePair() == null && basePair == null)) { + return false; + } + + if (!other.getBasePair().equals(basePair) || + !other.getAllSubstitutions().equals(getAllSubstitutions())) { + return false; + } + } + + + return other.getPairOp() == pairOp + && other.getLhsType().equals(lhs) + && other.getRhsType().equals(rhs); + } + + @Override + public int hashCode() { + return hashCode; + } + + @Override + public String toString() { + String ret = ""; + if (lhs instanceof PlaceholderType) { + ret = new Integer(((PlaceholderType)lhs).getVariance()).toString() + " " + + "WC: " + ((PlaceholderType)lhs).isWildcardable() + + ", IT: " + ((PlaceholderType)lhs).isInnerType(); + } + if (rhs instanceof PlaceholderType) { + ret = ret + ", " + new Integer(((PlaceholderType)rhs).getVariance()).toString() + " " + + "WC: " + ((PlaceholderType)rhs).isWildcardable() + + ", IT: " + ((PlaceholderType)rhs).isInnerType(); + } + return "(" + lhs + " " + pairOp + " " + rhs + ", " + ret + ")"; //+ ", [" + getfBounded().toString()+ "])"; + } + + /* + public List getInvolvedPlaceholderTypes() { + ArrayList ret = new ArrayList<>(); + ret.addAll(lhs.getInvolvedPlaceholderTypes()); + ret.addAll(rhs.getInvolvedPlaceholderTypes()); + return ret; + } + */ +} + + diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java new file mode 100644 index 0000000..be15065 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/UnifyType.java @@ -0,0 +1,119 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Set; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; + +/** + * Represents a java type. + * @author Florian Steurer + */ +public abstract class UnifyType { + + /** + * The name of the type e.q. "Integer", "? extends Integer" or "List" for (List) + */ + protected final String typeName; + + /** + * The type parameters of the type. + */ + protected final TypeParams typeParams; + + /** + * Creates a new instance + * @param name Name of the type (e.q. List for List, Integer or ? extends Integer) + * @param typeParams Parameters of the type (e.q. for List) + */ + protected UnifyType(String name, TypeParams p) { + typeName = name; + typeParams = p; + } + + + abstract public UnifyType accept(UnifyTypeVisitor visitor, T ht); + + /** + * Returns the name of the type. + * @return The name e.q. List for List, Integer or ? extends Integer + */ + public String getName() { + return typeName; + } + + /** + * The parameters of the type. + * @return Parameters of the type, e.q. for List. + */ + public TypeParams getTypeParams() { + return typeParams; + } + + /** + * Returns a new type that equals this type except for the type parameters. + * @param newTp The type params of the new type. + * @return A new type object. + */ + public abstract UnifyType setTypeParams(TypeParams newTp); + + /** + * Implementation of the visitor-pattern. Returns the set of smArg + * by calling the most specific overload in the FC. + * @param fc The FC that is called. + * @return The set that is smArg(this) + */ + abstract Set smArg(IFiniteClosure fc, Set fBounded); + + /** + * Implementation of the visitor-pattern. Returns the set of grArg + * by calling the most specific overload in the FC. + * @param fc The FC that is called. + * @return The set that is grArg(this) + */ + abstract Set grArg(IFiniteClosure fc, Set fBounded); + + /** + * Applies a unifier to this object. + * @param unif The unifier + * @return A UnifyType, that may or may not be a new object, that has its subtypes substituted. + */ + abstract UnifyType apply(Unifier unif); + + @Override + public String toString() { + String params = ""; + if(typeParams.size() != 0) { + for(UnifyType param : typeParams) + params += param.toString() + ","; + params = "<" + params.substring(0, params.length()-1) + ">"; + } + + return typeName + params; + } + + public Collection getInvolvedPlaceholderTypes() { + ArrayList ret = new ArrayList<>(); + ret.addAll(typeParams.getInvolvedPlaceholderTypes()); + return ret; + } + + public Boolean wrongWildcard() {//default + return false; + } + + @Override + public int hashCode() { + return this.toString().hashCode(); + } + + @Override + public boolean equals(Object obj) { + if(obj == null)return false; + return this.toString().equals(obj.toString()); + } +} \ No newline at end of file diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java new file mode 100644 index 0000000..ed706b2 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/WildcardType.java @@ -0,0 +1,72 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.ArrayList; +import java.util.Collection; + +/** + * A wildcard type that is either a ExtendsType or a SuperType. + * @author Florian Steurer + */ +public abstract class WildcardType extends UnifyType { + + /** + * The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself. + */ + protected UnifyType wildcardedType; + + /** + * Creates a new instance. + * @param name The name of the type, e.q. ? extends Integer + * @param wildcardedType The wildcarded type, e.q. Integer for ? extends Integer. Never a wildcard type itself. + */ + protected WildcardType(String name, UnifyType wildcardedType) { + super(name, wildcardedType.getTypeParams()); + this.wildcardedType = wildcardedType; + } + + /** + * Returns the wildcarded type, e.q. Integer for ? extends Integer. + * @return The wildcarded type. Never a wildcard type itself. + */ + public UnifyType getWildcardedType() { + return wildcardedType; + } + + /** + * Returns the type parameters of the WILDCARDED TYPE. + */ + @Override + public TypeParams getTypeParams() { + return wildcardedType.getTypeParams(); + } + + @Override + public Boolean wrongWildcard () {//This is an error + return (wildcardedType instanceof WildcardType); + } + + @Override + public int hashCode() { + return wildcardedType.hashCode() + getName().hashCode() + 17; + } + + @Override + public boolean equals(Object obj) { + if(!(obj instanceof WildcardType)) + return false; + + if(obj.hashCode() != this.hashCode()) + return false; + + WildcardType other = (WildcardType) obj; + return other.getWildcardedType().equals(wildcardedType); + } + + + @Override + public Collection getInvolvedPlaceholderTypes() { + ArrayList ret = new ArrayList<>(); + ret.addAll(wildcardedType.getInvolvedPlaceholderTypes()); + return ret; + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/model/hashKeyType.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/hashKeyType.java new file mode 100644 index 0000000..dedfcd8 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/model/hashKeyType.java @@ -0,0 +1,25 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +public class hashKeyType { + UnifyType realType; + + hashKeyType(UnifyType realType) { + this.realType= realType; + } + + @Override + public boolean equals(Object obj) { + if (obj instanceof hashKeyType) { + return realType.equals(((hashKeyType)obj).realType); + } + else + { + return false; + } + } + + @Override + public int hashCode() { + return realType.hashCode(); + } +} diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/visitUnifyTypeVisitor.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/visitUnifyTypeVisitor.java new file mode 100644 index 0000000..9ea3dc5 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/visitUnifyTypeVisitor.java @@ -0,0 +1,47 @@ +package de.dhbwstuttgart.typeinference.unify; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.HashMap; +import java.util.stream.Collectors; + +import de.dhbwstuttgart.typeinference.unify.interfaces.UnifyTypeVisitor; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.FunNType; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.ReferenceType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; + +public class visitUnifyTypeVisitor implements UnifyTypeVisitor { + + public ReferenceType visit(ReferenceType refty, T ht) { + return new ReferenceType(refty.getName(), + new TypeParams( + Arrays.stream(refty.getTypeParams().get()) + .map(x -> x.accept(this, ht)) + .collect(Collectors.toCollection(ArrayList::new)))); + } + + public PlaceholderType visit(PlaceholderType phty, T ht) { + return phty; + } + + public FunNType visit(FunNType funnty, T ht) { + return FunNType.getFunNType( + new TypeParams( + Arrays.stream(funnty.getTypeParams().get()) + .map(x -> x.accept(this, ht)) + .collect(Collectors.toCollection(ArrayList::new))) + ); + } + + public SuperType visit(SuperType suty, T ht) { + return new SuperType(suty.getWildcardedType().accept(this, ht)); + } + + public ExtendsType visit(ExtendsType extty, T ht) { + return new ExtendsType(extty.getWildcardedType().accept(this, ht)); + } +} diff --git a/src/main/java/de/dhbwstuttgart/util/BiRelation.java b/src/main/java/de/dhbwstuttgart/util/BiRelation.java new file mode 100644 index 0000000..ba4eec5 --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/util/BiRelation.java @@ -0,0 +1,19 @@ +package de.dhbwstuttgart.util; + +import java.util.ArrayList; + +public class BiRelation extends ArrayList>{ + + public void put(X x, Y y) { + this.add(new Pair<>(x,y)); + } + + public void put(Pair p) { + this.add(p); + } + + + public void putAll(BiRelation br) { + this.addAll(br); + } +} diff --git a/src/main/java/de/dhbwstuttgart/util/Pair.java b/src/main/java/de/dhbwstuttgart/util/Pair.java new file mode 100644 index 0000000..3046afd --- /dev/null +++ b/src/main/java/de/dhbwstuttgart/util/Pair.java @@ -0,0 +1,25 @@ +package de.dhbwstuttgart.util; + +import java.util.Optional; + +public class Pair { + private final T key; + private final T1 value; + + public Pair(T a, T1 b) { + this.value = b; + this.key = a; + } + + public Optional getValue() { + return Optional.of(value); + } + + public T getKey() { + return key; + } + + public String toString() { + return "(" + key.toString() + "," + value.toString() + ")\n"; + } +} diff --git a/src/test/java/UnifyTest.java b/src/test/java/UnifyTest.java new file mode 100644 index 0000000..6f75a89 --- /dev/null +++ b/src/test/java/UnifyTest.java @@ -0,0 +1,85 @@ +import de.dhbwstuttgart.typeinference.constraints.Constraint; +import de.dhbwstuttgart.typeinference.constraints.ConstraintSet; +import de.dhbwstuttgart.typeinference.constraints.Pair; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; +import de.dhbwstuttgart.typeinference.unify.UnifyResultModel; +import de.dhbwstuttgart.typeinference.unify.UnifyTaskModel; +import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.*; +import org.apache.commons.io.output.NullWriter; +import org.junit.Test; + +import java.util.ArrayList; +import java.util.HashSet; + +import java.util.List; +import java.util.Set; + +public class UnifyTest { + + public static final String rootDirectory = System.getProperty("user.dir")+"/resources/javFiles/"; + + private UnifyPair genPairListOfInteger(String name){ + + UnifyType type1 = new PlaceholderType(name); + UnifyType type2 = new ReferenceType("List", new TypeParams(new ReferenceType("Integer"))); + UnifyPair pair1 = new UnifyPair(type2, type1, PairOperator.SMALLERDOT); + + return pair1; + } + private UnifyPair genPairListOfString(String name){ + + PlaceholderType type1 = new PlaceholderType(name); + UnifyType type2 = new ReferenceType("List", new TypeParams(new ReferenceType("String"))); + UnifyPair pair1 = new UnifyPair(type2, type1, PairOperator.SMALLERDOT); + + return pair1; + } + @Test + public void unifyTest(){ + UnifyType type1; + UnifyType type2; + + Set undConstraints = new HashSet<>(); + undConstraints.add(genPairListOfInteger("a")); + undConstraints.add(genPairListOfString("a")); + + undConstraints.add(genPairListOfInteger("b")); + undConstraints.add(genPairListOfString("b")); + undConstraints.add(genPairListOfInteger("c")); + undConstraints.add(genPairListOfString("c")); + undConstraints.add(genPairListOfInteger("d")); + undConstraints.add(genPairListOfString("d")); + undConstraints.add(genPairListOfInteger("e")); + undConstraints.add(genPairListOfString("e")); + undConstraints.add(genPairListOfInteger("e1")); + undConstraints.add(genPairListOfString("e1")); + undConstraints.add(genPairListOfInteger("e2")); + undConstraints.add(genPairListOfString("e2")); + undConstraints.add(genPairListOfInteger("e3")); + undConstraints.add(genPairListOfString("e3")); + + List>> oderConstraints = new ArrayList<>(); + + Set constraints = new HashSet<>(); + type1 = new ReferenceType("Object"); + type2 = new ReferenceType("List", new TypeParams(new PlaceholderType("X"))); + constraints.add(new UnifyPair(type2, type1, PairOperator.SMALLER)); + type1 = new ReferenceType("Object"); + type2 = new ReferenceType("Integer"); + constraints.add(new UnifyPair(type2, type1, PairOperator.SMALLER)); + type1 = new ReferenceType("Object"); + type2 = new ReferenceType("String"); + constraints.add(new UnifyPair(type2, type1, PairOperator.SMALLER)); + + IFiniteClosure finiteClosure = new FiniteClosure(constraints, new NullWriter()); + + TypeUnify unifyAlgo = new TypeUnify(); + ConstraintSet cons = new ConstraintSet<>(); + UnifyResultModel urm = new UnifyResultModel(cons, finiteClosure); + UnifyTaskModel tasks = new UnifyTaskModel(); + Set> solution = unifyAlgo.unify(undConstraints, oderConstraints, finiteClosure, new NullWriter(), false, urm, tasks); + System.out.println(solution.size()); + //System.out.println(solution); + }} +