diff --git a/src/de/dhbwstuttgart/syntaxtree/Class.java b/src/de/dhbwstuttgart/syntaxtree/Class.java index 10ea63f1..c7c38d09 100755 --- a/src/de/dhbwstuttgart/syntaxtree/Class.java +++ b/src/de/dhbwstuttgart/syntaxtree/Class.java @@ -49,7 +49,7 @@ import de.dhbwstuttgart.typeinference.exceptions.DebugException; import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException; import de.dhbwstuttgart.typeinference.typedeployment.TypeInsertPoint; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; import org.apache.commons.bcel6.generic.*; import org.apache.commons.bcel6.classfile.*; diff --git a/src/de/dhbwstuttgart/syntaxtree/SourceFile.java b/src/de/dhbwstuttgart/syntaxtree/SourceFile.java index bc4c39ef..533fe929 100755 --- a/src/de/dhbwstuttgart/syntaxtree/SourceFile.java +++ b/src/de/dhbwstuttgart/syntaxtree/SourceFile.java @@ -53,7 +53,7 @@ import de.dhbwstuttgart.typeinference.assumptions.ParameterAssumption; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.DebugException; import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure; import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; @@ -263,7 +263,7 @@ public class SourceFile //Unmögliche ConstraintsSets aussortieren durch Unifizierung Function,Menge>> unifier = (pairs)->{ Menge> retValue = new Menge<>(); - Set> unifiedPairs = new Unify().unify(pairs, finiteClosure); + Set> unifiedPairs = new TypeUnify().unify(pairs, finiteClosure); return retValue;}; //oderConstraints.filterWrongConstraints(unifier); @@ -360,7 +360,7 @@ public class SourceFile }); */ typinferenzLog.debug("\nUnifiziere Constraints:\n"+constraints, Section.TYPEINFERENCE); - Set> unifyResult = new Unify().unify(constraints, finiteClosure); + Set> unifyResult = new TypeUnify().unify(constraints, finiteClosure); Menge> convertedResult = unifyResult.parallelStream().>map((Set resultSet)->{ Menge innerConvert = resultSet.stream().map((UnifyPair mp)->UnifyTypeFactory.convert(mp)) diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/AddOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/AddOp.java index b1b4e4b6..d56b6ac2 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/AddOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/AddOp.java @@ -17,7 +17,7 @@ import de.dhbwstuttgart.typeinference.ConstraintsSet; import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.DebugException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/EqualOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/EqualOp.java index 184a8501..c49f3957 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/EqualOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/EqualOp.java @@ -13,7 +13,7 @@ import de.dhbwstuttgart.syntaxtree.statement.Expr; import de.dhbwstuttgart.syntaxtree.statement.Null; import de.dhbwstuttgart.syntaxtree.type.RefType; import de.dhbwstuttgart.typeinference.Pair; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/LogOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/LogOp.java index 40c4d0c3..54ceff3b 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/LogOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/LogOp.java @@ -20,7 +20,7 @@ import de.dhbwstuttgart.typeinference.ConstraintsSet; import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.DebugException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/MulOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/MulOp.java index d031b647..6abb1d5d 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/MulOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/MulOp.java @@ -15,7 +15,7 @@ import de.dhbwstuttgart.syntaxtree.type.Type; import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.DebugException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; // ino.class.MulOp.24231.declaration public abstract class MulOp extends Operator diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/NotEqualOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/NotEqualOp.java index 7cbe3936..50c9fdfc 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/NotEqualOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/NotEqualOp.java @@ -12,7 +12,7 @@ import de.dhbwstuttgart.syntaxtree.statement.Expr; import de.dhbwstuttgart.syntaxtree.statement.Null; import de.dhbwstuttgart.syntaxtree.type.RefType; import de.dhbwstuttgart.typeinference.Pair; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; // ino.class.NotEqualOp.24241.declaration public class NotEqualOp extends RelOp diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/Operator.java b/src/de/dhbwstuttgart/syntaxtree/operator/Operator.java index f4534b45..7e87ff73 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/Operator.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/Operator.java @@ -22,7 +22,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.UndConstraint; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; public abstract class Operator extends SyntaxTreeNode diff --git a/src/de/dhbwstuttgart/syntaxtree/operator/RelOp.java b/src/de/dhbwstuttgart/syntaxtree/operator/RelOp.java index eb9178d7..dae2941b 100755 --- a/src/de/dhbwstuttgart/syntaxtree/operator/RelOp.java +++ b/src/de/dhbwstuttgart/syntaxtree/operator/RelOp.java @@ -16,7 +16,7 @@ import de.dhbwstuttgart.syntaxtree.type.Type; import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.DebugException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; // ino.class.RelOp.24299.declaration public abstract class RelOp extends Operator // ino.end diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/Assign.java b/src/de/dhbwstuttgart/syntaxtree/statement/Assign.java index 19132759..f2086ec3 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/Assign.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/Assign.java @@ -36,7 +36,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/ExprStmt.java b/src/de/dhbwstuttgart/syntaxtree/statement/ExprStmt.java index ec7afd19..1a657afb 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/ExprStmt.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/ExprStmt.java @@ -12,7 +12,7 @@ import de.dhbwstuttgart.core.MyCompiler; import de.dhbwstuttgart.syntaxtree.type.Type; import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder; import de.dhbwstuttgart.typeinference.Pair; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; // ino.class.ExprStmt.25265.declaration public abstract class ExprStmt extends Statement diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/ForStmt.java b/src/de/dhbwstuttgart/syntaxtree/statement/ForStmt.java index 7168da1b..c402a83a 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/ForStmt.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/ForStmt.java @@ -36,7 +36,7 @@ import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/IfStmt.java b/src/de/dhbwstuttgart/syntaxtree/statement/IfStmt.java index 23131b42..351cfbef 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/IfStmt.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/IfStmt.java @@ -47,7 +47,7 @@ import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/InstVar.java b/src/de/dhbwstuttgart/syntaxtree/statement/InstVar.java index 7bc5b1bc..1c2ad306 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/InstVar.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/InstVar.java @@ -31,7 +31,7 @@ import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.UndConstraint; import de.dhbwstuttgart.typeinference.assumptions.FieldAssumption; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/NegativeExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/NegativeExpr.java index 82a0cfec..f9c46865 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/NegativeExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/NegativeExpr.java @@ -28,7 +28,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/NotExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/NotExpr.java index 8cf996db..4d822b6f 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/NotExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/NotExpr.java @@ -28,7 +28,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/PostDecExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/PostDecExpr.java index 0893b076..69751b09 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/PostDecExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/PostDecExpr.java @@ -28,7 +28,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/PostIncExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/PostIncExpr.java index 672e5cde..85a06e38 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/PostIncExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/PostIncExpr.java @@ -33,7 +33,7 @@ import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.UndConstraint; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/PreDecExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/PreDecExpr.java index bce1dc97..cfabbed9 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/PreDecExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/PreDecExpr.java @@ -28,7 +28,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/PreIncExpr.java b/src/de/dhbwstuttgart/syntaxtree/statement/PreIncExpr.java index 8ef55b9a..36c4b514 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/PreIncExpr.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/PreIncExpr.java @@ -28,7 +28,7 @@ import de.dhbwstuttgart.typeinference.Pair; import de.dhbwstuttgart.typeinference.ResultSet; import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/syntaxtree/statement/WhileStmt.java b/src/de/dhbwstuttgart/syntaxtree/statement/WhileStmt.java index 35a18dc7..e29f45f6 100755 --- a/src/de/dhbwstuttgart/syntaxtree/statement/WhileStmt.java +++ b/src/de/dhbwstuttgart/syntaxtree/statement/WhileStmt.java @@ -32,7 +32,7 @@ import de.dhbwstuttgart.typeinference.TypeinferenceResultSet; import de.dhbwstuttgart.typeinference.UndConstraint; import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions; import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; diff --git a/src/de/dhbwstuttgart/typeinference/UndMenge.java b/src/de/dhbwstuttgart/typeinference/UndMenge.java index fa300765..8782d70a 100644 --- a/src/de/dhbwstuttgart/typeinference/UndMenge.java +++ b/src/de/dhbwstuttgart/typeinference/UndMenge.java @@ -1,6 +1,6 @@ package de.dhbwstuttgart.typeinference; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; import java.util.Collection; import java.util.Iterator; import java.util.Set; diff --git a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java index 45e52133..80dabce6 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java @@ -57,8 +57,7 @@ public class MartelliMontanariUnify implements IUnify { } // REDUCE - Rule - if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType) - && (rhsTypeParams.size() != 0 || lhsTypeParams.size() != 0)) { + if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) { Set result = new HashSet<>(); // f<...> = g<...> with f != g are not unifiable @@ -67,7 +66,10 @@ public class MartelliMontanariUnify implements IUnify { // 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)); diff --git a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java index 8fb5ddf2..a9f82eff 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java @@ -30,17 +30,7 @@ import de.dhbwstuttgart.typeinference.unify.model.PairOperator; * @author Florian Steurer * */ -public class RuleSet implements IRuleSet{ - - protected IFiniteClosure finiteClosure; - - /** - * Creates a new instance that uses the specified FC for greater, grArg, etc. - * @param fc The FC that is used for greater, grArg, etc. - */ - public RuleSet(IFiniteClosure fc) { - finiteClosure = fc; - } +public class RuleSet implements IRuleSet{ @Override public Optional reduceUp(UnifyPair pair) { @@ -97,7 +87,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional> reduceExt(UnifyPair pair) { + public Optional> reduceExt(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOTWC) return Optional.empty(); @@ -119,7 +109,7 @@ public class RuleSet implements IRuleSet{ if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size()) return Optional.empty(); - UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); + UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null); if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); @@ -127,7 +117,7 @@ public class RuleSet implements IRuleSet{ if(x instanceof ExtendsType) xFromFc = new ExtendsType(xFromFc); - UnifyType extYFromFc = finiteClosure.grArg(xFromFc).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); + UnifyType extYFromFc = fc.grArg(xFromFc).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(); @@ -149,7 +139,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional> reduceSup(UnifyPair pair) { + public Optional> reduceSup(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOTWC) return Optional.empty(); @@ -171,7 +161,7 @@ public class RuleSet implements IRuleSet{ if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size()) return Optional.empty(); - UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); + UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null); if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); @@ -179,7 +169,7 @@ public class RuleSet implements IRuleSet{ if(x instanceof SuperType) xFromFc = new SuperType(xFromFc); - UnifyType supYFromFc = finiteClosure.grArg(xFromFc).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); + UnifyType supYFromFc = fc.grArg(xFromFc).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(); @@ -231,7 +221,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional> reduce1(UnifyPair pair) { + public Optional> reduce1(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOT) return Optional.empty(); @@ -249,12 +239,12 @@ public class RuleSet implements IRuleSet{ if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size()) return Optional.empty(); - UnifyType cFromFc = finiteClosure.getLeftHandedType(c.getName()).orElse(null); + UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null); if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders()) return Optional.empty(); - UnifyType dFromFc = finiteClosure.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null); + UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null); if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size()) return Optional.empty(); @@ -330,7 +320,7 @@ public class RuleSet implements IRuleSet{ } @Override - public boolean erase1(UnifyPair pair) { + public boolean erase1(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOT) return false; @@ -342,18 +332,18 @@ public class RuleSet implements IRuleSet{ if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType)) return false; - return finiteClosure.greater(lhsType).contains(rhsType); + return fc.greater(lhsType).contains(rhsType); } @Override - public boolean erase2(UnifyPair pair) { + public boolean erase2(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOTWC) return false; UnifyType lhsType = pair.getLhsType(); UnifyType rhsType = pair.getRhsType(); - return finiteClosure.grArg(lhsType).contains(rhsType); + return fc.grArg(lhsType).contains(rhsType); } @Override @@ -379,7 +369,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional adapt(UnifyPair pair) { + public Optional adapt(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOT) return Optional.empty(); @@ -398,7 +388,7 @@ public class RuleSet implements IRuleSet{ return Optional.empty(); - Optional opt = finiteClosure.getLeftHandedType(typeD.getName()); + Optional opt = fc.getLeftHandedType(typeD.getName()); if(!opt.isPresent()) return Optional.empty(); @@ -406,7 +396,7 @@ public class RuleSet implements IRuleSet{ UnifyType typeDgen = opt.get(); // Actually greater+ because the types are ensured to have different names - Set greater = finiteClosure.getAncestors(typeDgen); + Set greater = fc.getAncestors(typeDgen); opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); if(!opt.isPresent()) @@ -425,7 +415,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional adaptExt(UnifyPair pair) { + public Optional adaptExt(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOTWC) return Optional.empty(); @@ -442,16 +432,16 @@ public class RuleSet implements IRuleSet{ UnifyType typeDgen; if(typeD instanceof ReferenceType) - typeDgen = finiteClosure.getLeftHandedType(typeD.getName()).orElse(null); + typeDgen = fc.getLeftHandedType(typeD.getName()).orElse(null); else { - Optional opt = finiteClosure.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName()); + Optional opt = fc.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName()); typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null; } if(typeDgen == null) return Optional.empty(); - Set grArg = finiteClosure.grArg(typeDgen); + Set grArg = fc.grArg(typeDgen); Optional opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny(); @@ -471,7 +461,7 @@ public class RuleSet implements IRuleSet{ } @Override - public Optional adaptSup(UnifyPair pair) { + public Optional adaptSup(UnifyPair pair, IFiniteClosure fc) { if(pair.getPairOp() != PairOperator.SMALLERDOTWC) return Optional.empty(); @@ -487,7 +477,7 @@ public class RuleSet implements IRuleSet{ return Optional.empty(); - Optional opt = finiteClosure.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName()); + Optional opt = fc.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName()); if(!opt.isPresent()) return Optional.empty(); @@ -497,7 +487,7 @@ public class RuleSet implements IRuleSet{ // Use of smArg instead of grArg because // a in grArg(b) => b in smArg(a) - Set smArg = finiteClosure.smArg(typeSupDgen); + Set smArg = fc.smArg(typeSupDgen); opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); if(!opt.isPresent()) diff --git a/src/de/dhbwstuttgart/typeinference/unify/Unify.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java similarity index 81% rename from src/de/dhbwstuttgart/typeinference/unify/Unify.java rename to src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java index 71734187..7f1c857b 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnify.java @@ -30,21 +30,38 @@ import de.dhbwstuttgart.typeinference.unify.model.Unifier; * Implementation of the type unification algorithm * @author Florian Steurer */ -public class Unify { +public class TypeUnify { + /** + * 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 = new RuleSet(); + + /** + * 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 + */ public Set> unify(Set eq, IFiniteClosure fc) { /* * Step 1: Repeated application of reduce, adapt, erase, swap */ - Set eq0 = applyTypeUnificationRules(eq, fc); /* * 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); @@ -60,7 +77,7 @@ public class Unify { // cartesian product of the sets created by pattern matching. List>> topLevelSets = new ArrayList<>(); - if(eq1s.size() != 0) { + 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' @@ -71,7 +88,7 @@ public class Unify { .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) .collect(Collectors.toSet()); - if(bufferSet.size() != 0) { + 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); @@ -92,10 +109,13 @@ public class Unify { * filters for pairs and sets can be applied here */ // Sub cartesian products of the second level (pattern matched) sets + // "the big (x)" + // TODO Optimierungsmöglichkeit: Parallelisierung der Schleife möglich for(Set>> secondLevelSet : secondLevelSets) { List>> secondLevelSetList = new ArrayList<>(secondLevelSet); Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); + // Flatten and add to top level sets Set> flat = new HashSet<>(); for(List> s : cartResult) { Set flat1 = new HashSet<>(); @@ -112,10 +132,8 @@ public class Unify { .collect(Collectors.toCollection(HashSet::new)); //System.out.println(result); - /* - * Step 5: Substitution - */ - + // Flatten the cartesian product + // TODO parallelisierung möglich Set> eqPrimeSetFlat = new HashSet<>(); for(Set> setToFlatten : eqPrimeSet) { Set buffer = new HashSet<>(); @@ -123,7 +141,10 @@ public class Unify { eqPrimeSetFlat.add(buffer); } - IRuleSet rules = new RuleSet(fc); + + /* + * Step 5: Substitution + */ Set> restartSet = new HashSet<>(); Set> eqPrimePrimeSet = new HashSet<>(); @@ -150,7 +171,7 @@ public class Unify { * Step 6 a) Restart for pairs where subst was applied * b) Build the union over everything */ - + // TODO parallelisierung möglich (lohnt sich vermutlich) for(Set eqss : restartSet) eqPrimePrimeSet.addAll(this.unify(eqss, fc)); @@ -161,6 +182,11 @@ public class Unify { } + /** + * 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(); @@ -169,13 +195,18 @@ public class Unify { 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. + */ protected Set applyTypeUnificationRules(Set eq, IFiniteClosure fc) { /* @@ -193,12 +224,11 @@ public class Unify { LinkedHashSet targetSet = new LinkedHashSet(); LinkedList eqQueue = new LinkedList<>(); - IRuleSet rules = new RuleSet(fc); /* * Swap all pairs and erase all erasable pairs */ - eq.forEach(x -> swapAddOrErase(x, rules, eqQueue)); + eq.forEach(x -> swapAddOrErase(x, fc, eqQueue)); /* * Apply rules until the queue is empty @@ -220,31 +250,31 @@ public class Unify { // One of the rules has been applied if(opt.isPresent()) { - swapAddOrErase(opt.get(), rules, eqQueue); + swapAddOrErase(opt.get(), fc, eqQueue); continue; } // Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq - Optional> optSet = rules.reduce1(pair); + Optional> optSet = rules.reduce1(pair, fc); optSet = optSet.isPresent() ? optSet : rules.reduce2(pair); - optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair); - optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair); + optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc); + optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc); optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair); // One of the rules has been applied if(optSet.isPresent()) { - optSet.get().forEach(x -> swapAddOrErase(x, rules, eqQueue)); + optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue)); continue; } // Adapt, AdaptExt, AdaptSup - opt = rules.adapt(pair); - opt = opt.isPresent() ? opt : rules.adaptExt(pair); - opt = opt.isPresent() ? opt : rules.adaptSup(pair); + 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(), rules, eqQueue); + swapAddOrErase(opt.get(), fc, eqQueue); continue; } @@ -255,16 +285,29 @@ public class Unify { return targetSet; } - protected void swapAddOrErase(UnifyPair pair, IRuleSet rules, Collection collection) { + /** + * 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) || rules.erase3(pair2) || rules.erase2(pair2)) + 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) @@ -273,16 +316,21 @@ public class Unify { 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, IFiniteClosure fc, Set undefined) { - List>>> result = new ArrayList<>(); + List>>> result = new ArrayList<>(8); // Init all 8 cases for(int i = 0; i < 8; i++) result.add(new HashSet<>()); for(UnifyPair pair : eq2s) { - PairOperator pairOp = pair.getPairOp(); UnifyType lhsType = pair.getLhsType(); UnifyType rhsType = pair.getRhsType(); @@ -323,17 +371,19 @@ public class Unify { // Pairs that do not have one of the aboves form are contradictory. else undefined.add(pair); - } + // 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)); } + /** + * Cartesian product Case 1: (a <. Theta') + */ protected Set> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { Set> result = new HashSet<>(); - IUnify unify = new MartelliMontanariUnify(); - + Set cs = fc.getAllTypesByName(thetaPrime.getName()); cs.add(thetaPrime); @@ -375,7 +425,7 @@ public class Unify { } for(UnifyType tqp : thetaQPrimes) { - Optional opt = unify.unify(tqp, thetaPrime); + Optional opt = stdUnify.unify(tqp, thetaPrime); if (!opt.isPresent()) continue; @@ -411,6 +461,9 @@ public class Unify { return result; } + /** + * Cartesian Product Case 2: (a <.? ? ext Theta') + */ protected Set> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) { Set> result = new HashSet<>(); @@ -483,6 +536,9 @@ public class Unify { // return result; } + /** + * Cartesian Product Case 3: (a <.? ? sup Theta') + */ protected Set> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) { Set> result = new HashSet<>(); @@ -504,6 +560,9 @@ public class Unify { return result; } + /** + * Cartesian Product Case 4: (a <.? Theta') + */ protected Set> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { Set> result = new HashSet<>(); Set resultPrime = new HashSet<>(); @@ -513,6 +572,9 @@ public class Unify { return result; } + /** + * Cartesian Product Case 5: (Theta <. a) + */ protected Set> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); for(UnifyType thetaS : fc.greater(theta)) { @@ -531,6 +593,9 @@ public class Unify { return result; } + /** + * Cartesian Product Case 6: (? ext Theta <.? a) + */ protected Set> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); //for(UnifyType thetaS : fc.smaller(extTheta.getExtendedType())) { @@ -546,6 +611,9 @@ public class Unify { return result; } + /** + * Cartesian Product Case 7: (? sup Theta <.? a) + */ protected Set> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); @@ -613,6 +681,9 @@ public class Unify { // return result; } + /** + * Cartesian Product Case 8: (Theta <.? a) + */ protected Set> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) { Set> result = new HashSet<>(); //for(UnifyType thetaS : fc.grArg(theta)) { @@ -635,12 +706,25 @@ public class Unify { 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))); diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java index 26ea0dce..714cb989 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java @@ -14,10 +14,10 @@ public interface IRuleSet { public Optional reduceUp(UnifyPair pair); public Optional reduceLow(UnifyPair pair); public Optional reduceUpLow(UnifyPair pair); - public Optional> reduceExt(UnifyPair pair); - public Optional> reduceSup(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); + public Optional> reduce1(UnifyPair pair, IFiniteClosure fc); public Optional> reduce2(UnifyPair pair); /* @@ -42,13 +42,13 @@ public interface IRuleSet { * Checks whether the erase1-Rule applies to the pair. * @return True if the pair is erasable, false otherwise. */ - public boolean erase1(UnifyPair pair); + 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); + public boolean erase2(UnifyPair pair, IFiniteClosure fc); /** * Checks whether the erase3-Rule applies to the pair. @@ -58,9 +58,9 @@ public interface IRuleSet { public Optional swap(UnifyPair pair); - public Optional adapt(UnifyPair pair); - public Optional adaptExt(UnifyPair pair); - public Optional adaptSup(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'). diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 1ad6f28b..17fbb240 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -8,20 +8,35 @@ import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; -import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +/** + * The finite closure for the type unification + * @author Florian Steurer + */ public class FiniteClosure implements IFiniteClosure { - - private HashMap> inheritanceGraph; - private HashMap>> strInheritanceGraph; - private Set pairs; - //private Set basicTypes; - //TODO im konstruktor mitgeben um typenabzuhandeln die keine extends beziehung haben. (Damit die FC diese Typen auch kennt) - //(ALternative: immer die extends zu object beziehung einfügen) + /** + * 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; + + //TODO Prüfen: Typen ohne Kante im Graph als extra Menge im Konstruktor mitgeben? + /** + * Creates a new instance using the inheritance tree defined in the pairs. + */ public FiniteClosure(Set pairs) { this.pairs = new HashSet<>(pairs); inheritanceGraph = new HashMap>(); @@ -49,7 +64,6 @@ public class FiniteClosure implements IFiniteClosure { } // Build the alternative representation with strings as keys - strInheritanceGraph = new HashMap<>(); for(UnifyType key : inheritanceGraph.keySet()) { if(!strInheritanceGraph.containsKey(key.getName())) @@ -71,7 +85,12 @@ public class FiniteClosure implements IFiniteClosure { return computeSmaller(type); } + /** + * Computes the smaller functions for every type except FunNTypes. + */ private Set computeSmaller(UnifyType type) { + // Base Case: The type is in the inheritance tree. Add all children. + // This is Case 1 in the definition of the subtyping relation. if(inheritanceGraph.containsKey(type)) { Set result = new HashSet<>(); result.add(type); @@ -85,22 +104,22 @@ public class FiniteClosure implements IFiniteClosure { // if T = T' then T <=* T' result1.add(type); + // Permute all params with values that are in smArg() of that type. + // This corresponds to Case 3 in the definition of the subtyping relation. {ArrayList> paramCandidates = new ArrayList<>(); for (UnifyType param : type.getTypeParams()) paramCandidates.add(smArg(param)); - - Set permResult = permuteParams(paramCandidates); - - for (TypeParams newParams : permResult) - result1.add(type.setTypeParams(newParams));} - + permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));} + + // This is case 2 of the definition of the subtyping relation. Set result2 = new HashSet<>(); if (strInheritanceGraph.containsKey(type.getName())) { HashSet candidates = new HashSet<>(); + // All types with the same name strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent())); - for(UnifyType typePrime : result1) { for (UnifyType theta2 : candidates) { + // Find the substitution Optional sigma2Opt = unify.unify(typePrime, theta2); if (!sigma2Opt.isPresent()) continue; @@ -120,6 +139,8 @@ public class FiniteClosure implements IFiniteClosure { else result2 = result1; + // Permute the params again. + // This corresponds again to Case 3 of the definition of the subtyping relation. Set result3 = new HashSet<>(); for(UnifyType t : result2) { ArrayList> paramCandidates = new ArrayList<>(); @@ -141,22 +162,23 @@ public class FiniteClosure implements IFiniteClosure { return result3; } + /** + * Computes the smaller-Function for FunNTypes. + */ private Set computeSmallerFunN(FunNType type) { 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))); for (int i = 1; i < type.getTypeParams().size(); i++) - paramCandidates.add(greater(type.getTypeParams().get(i))); + paramCandidates.add(greater(type.getTypeParams().get(i))); - Set permResult = permuteParams(paramCandidates); - - for (TypeParams newParams : permResult) - result.add(type.setTypeParams(newParams)); - + permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x))); return result; } @@ -170,40 +192,44 @@ public class FiniteClosure implements IFiniteClosure { return computeGreaterFunN((FunNType) type); return computeGreater(type); } - + + /** + * Computes the greater function for all types except function types. + */ protected Set computeGreater(UnifyType type) { IUnify unify = new MartelliMontanariUnify(); Set result1 = new HashSet<>(); + // The type is in the inheritance tree. Add all children. + // This is Case 1 in the definition of the subtyping relation. if(inheritanceGraph.containsKey(type)) result1.addAll(inheritanceGraph.get(type).getContentOfPredecessors()); // if T = T' then T <=* T' result1.add(type); + // Permute all params with values that are in smArg() of that type. + // This corresponds to Case 3 in the definition of the subtyping relation. {ArrayList> paramCandidates = new ArrayList<>(); for (UnifyType param : type.getTypeParams()) paramCandidates.add(grArg(param)); - - Set permResult = new HashSet<>(); - permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]); - - for (TypeParams newParams : permResult) - result1.add(type.setTypeParams(newParams));} + permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));} + // This is case 2 of the definition of the subtyping relation. Set result2 = new HashSet<>(); if (strInheritanceGraph.containsKey(type.getName()) && !inheritanceGraph.containsKey(type)) { HashSet candidates = new HashSet<>(); + // All types with the same name strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent())); for(UnifyType typePrime : result1) { for (UnifyType theta2 : candidates) { + // Find the substitution Optional sigma2Opt = unify.unify(typePrime, theta2); if (!sigma2Opt.isPresent()) continue; if(type.equals(theta2)) continue; - Unifier sigma2 = sigma2Opt.get(); sigma2.swapPlaceholderSubstitutions(typePrime.getTypeParams()); Set theta1s = greater(theta2); @@ -216,18 +242,17 @@ public class FiniteClosure implements IFiniteClosure { } } - result2.addAll(result1); + result2.addAll(result1); + // Permute the params again. + // This corresponds again to Case 3 of the definition of the subtyping relation. Set result3 = new HashSet<>(); for(UnifyType t : result2) { ArrayList> paramCandidates = new ArrayList<>(); for (UnifyType param : t.getTypeParams()) paramCandidates.add(grArg(param)); - Set permResult = new HashSet<>(); - permuteParams(paramCandidates, 0, permResult, new UnifyType[paramCandidates.size()]); - - for (TypeParams newParams : permResult) { + for (TypeParams newParams : permuteParams(paramCandidates)) { UnifyType tPrime = t.setTypeParams(newParams); if(tPrime.equals(t)) result3.add(t); @@ -240,22 +265,22 @@ public class FiniteClosure implements IFiniteClosure { return result3; } + /** + * Computes the greater function for FunN-Types + */ protected Set computeGreaterFunN(FunNType type) { 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))); for (int i = 1; i < type.getTypeParams().size(); i++) paramCandidates.add(smaller(type.getTypeParams().get(i))); - - Set permResult = permuteParams(paramCandidates); - - for (TypeParams newParams : permResult) - result.add(type.setTypeParams(newParams)); - + permuteParams(paramCandidates).forEach(x -> result.add(type.setTypeParams(x))); return result; } @@ -267,29 +292,29 @@ public class FiniteClosure implements IFiniteClosure { @Override public Set grArg(ReferenceType type) { - Set result = new HashSet(); - + Set result = new HashSet(); result.add(type); smaller(type).forEach(x -> result.add(new SuperType(x))); greater(type).forEach(x -> result.add(new ExtendsType(x))); - return result; } @Override public Set grArg(FunNType type) { - throw new NotImplementedException(); + // TODO ist das richtig? + Set result = new HashSet(); + result.add(type); + smaller(type).forEach(x -> result.add(new SuperType(x))); + greater(type).forEach(x -> result.add(new ExtendsType(x))); + return result; } @Override public Set grArg(ExtendsType type) { Set result = new HashSet(); - result.add(type); - + result.add(type); UnifyType t = type.getExtendedType(); - greater(t).forEach(x -> result.add(new ExtendsType(x))); - return result; } @@ -297,20 +322,15 @@ public class FiniteClosure implements IFiniteClosure { public Set grArg(SuperType type) { Set result = new HashSet(); result.add(type); - - UnifyType t = type.getSuperedType(); - + UnifyType t = type.getSuperedType(); smaller(t).forEach(x -> result.add(new SuperType(x))); - return result; } @Override public Set grArg(PlaceholderType type) { HashSet result = new HashSet<>(); - result.add(type); - //result.add(new SuperType(type)); - //result.add(new ExtendsType(type)); + result.add(type); return result; } @@ -321,30 +341,29 @@ public class FiniteClosure implements IFiniteClosure { @Override public Set smArg(ReferenceType type) { - Set result = new HashSet(); - + Set result = new HashSet(); result.add(type); return result; } @Override public Set smArg(FunNType type) { - throw new NotImplementedException(); + // TODO ist das richtig? + Set result = new HashSet(); + result.add(type); + return result; } @Override public Set smArg(ExtendsType type) { Set result = new HashSet(); result.add(type); - UnifyType t = type.getExtendedType(); - result.add(t); smaller(t).forEach(x -> { result.add(new ExtendsType(x)); result.add(x); }); - return result; } @@ -352,16 +371,13 @@ public class FiniteClosure implements IFiniteClosure { @Override public Set smArg(SuperType type) { Set result = new HashSet(); - result.add(type); - + result.add(type); UnifyType t = type.getSuperedType(); - result.add(t); greater(t).forEach(x -> { result.add(new SuperType(x)); result.add(x); }); - return result; } @@ -409,12 +425,25 @@ public class FiniteClosure implements IFiniteClosure { 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))); diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 40382a61..ebae5e0a 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -8,7 +8,7 @@ import java.util.stream.Collectors; import org.junit.Test; -import de.dhbwstuttgart.typeinference.unify.Unify; +import de.dhbwstuttgart.typeinference.unify.TypeUnify; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.model.UnifyPair; import de.dhbwstuttgart.typeinference.unify.model.PairOperator; @@ -17,7 +17,7 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType; import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import junit.framework.Assert; -public class UnifyTest extends Unify { +public class UnifyTest extends TypeUnify { /** * Testing the unification for cases with (n)one pair and without generics.