diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index 0601d70f..62b65b27 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -3,11 +3,11 @@ package de.dhbwstuttgart.typeinference.unify.interfaces; import java.util.Optional; import java.util.Set; -import de.dhbwstuttgart.typinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typinference.unify.model.SimpleType; -import de.dhbwstuttgart.typinference.unify.model.SuperType; -import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.SimpleType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.Type; public interface IFiniteClosure { @@ -50,4 +50,5 @@ public interface IFiniteClosure { public Set smArg(PlaceholderType type); public Optional getGenericType(String typeName); + public Set getAllTypes(String typeName); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java index 02611fd9..840d7259 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IRuleSet.java @@ -3,8 +3,7 @@ package de.dhbwstuttgart.typeinference.unify.interfaces; import java.util.Optional; import java.util.Set; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; -import de.dhbwstuttgart.typinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.MPair; public interface IRuleSet { @@ -27,5 +26,5 @@ public interface IRuleSet { public Optional adaptExt(MPair pair); public Optional adaptSup(MPair pair); - public Set subst(Set pair); + public Optional> subst(Set pair); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/ITypeMapper.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/ITypeMapper.java deleted file mode 100644 index 85efc20a..00000000 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/ITypeMapper.java +++ /dev/null @@ -1,7 +0,0 @@ -package de.dhbwstuttgart.typeinference.unify.interfaces; - -import de.dhbwstuttgart.typeinference.Menge; - -public interface ITypeMapper { - -} diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index 34e39738..f286e3b6 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -1,14 +1,23 @@ 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.unifynew.Unifier; -import de.dhbwstuttgart.typinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; /** - * Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari, Ruzicka-Privara or Suciu) + * Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari) * @author Florian Steurer */ public interface IUnify { - public Unifier unify(Set terms); + + public Optional unify(Set terms); + + default public Optional unify(Type... terms) { + return unify(Arrays.stream(terms).collect(Collectors.toSet())); + } + } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/ExtendsType.java b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java similarity index 58% rename from src/de/dhbwstuttgart/typinference/unify/model/ExtendsType.java rename to src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java index 2b0facaf..9fb3e454 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/ExtendsType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/ExtendsType.java @@ -1,18 +1,32 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; +/** + * An extends wildcard type "? extends T". + */ public final class ExtendsType extends Type { + + /** + * The extended type + */ private Type extendedType; + /** + * Creates a new extends wildcard type. + * @param extendedType The extended type e.g. Integer in "? extends Integer" + */ public ExtendsType(Type extendedType) { super("? extends " + extendedType.getName(), extendedType.getTypeParams()); this.extendedType = extendedType; } + /** + * Gets the type extended by this wildcard e.g. "Integer" for "? extends Integer" + * @return The extended type. + */ public Type getExtendedType() { return extendedType; } @@ -23,19 +37,24 @@ public final class ExtendsType extends Type { } @Override - public String toString() { - return "? extends " + extendedType; + public Type setTypeParams(TypeParams newTp) { + return new ExtendsType(extendedType.setTypeParams(newTp)); } @Override - public Set smArg(IFiniteClosure fc) { + Set smArg(IFiniteClosure fc) { return fc.smArg(this); } @Override - public Set grArg(IFiniteClosure fc) { + Set grArg(IFiniteClosure fc) { return fc.grArg(this); } + + @Override + Type apply(Unifier unif) { + return new ExtendsType(extendedType.apply(unif)); + } @Override public int hashCode() { @@ -50,9 +69,9 @@ public final class ExtendsType extends Type { ExtendsType other = (ExtendsType) obj; return other.getExtendedType().equals(extendedType); } - + @Override - public Type apply(Unifier unif) { - return new ExtendsType(extendedType.apply(unif)); + public String toString() { + return "? extends " + extendedType; } } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java similarity index 89% rename from src/de/dhbwstuttgart/typinference/unify/model/FiniteClosure.java rename to src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index ae36f465..e618482d 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -1,12 +1,13 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.HashMap; import java.util.HashSet; import java.util.Optional; import java.util.Set; +import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; public class FiniteClosure implements IFiniteClosure { @@ -205,4 +206,11 @@ public class FiniteClosure implements IFiniteClosure { return Optional.empty(); } + + @Override + public Set getAllTypes(String typeName) { + if(!strInheritanceGraph.containsKey(typeName)) + return new HashSet<>(); + return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new)); + } } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/MPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/MPair.java similarity index 92% rename from src/de/dhbwstuttgart/typinference/unify/model/MPair.java rename to src/de/dhbwstuttgart/typeinference/unify/model/MPair.java index 9a76f2a9..6b740c46 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/MPair.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/MPair.java @@ -1,4 +1,4 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; public class MPair { diff --git a/src/de/dhbwstuttgart/typinference/unify/model/Node.java b/src/de/dhbwstuttgart/typeinference/unify/model/Node.java similarity index 91% rename from src/de/dhbwstuttgart/typinference/unify/model/Node.java rename to src/de/dhbwstuttgart/typeinference/unify/model/Node.java index e42a2608..7010ec32 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/Node.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Node.java @@ -1,4 +1,4 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.HashSet; import java.util.Set; diff --git a/src/de/dhbwstuttgart/typinference/unify/model/PlaceholderType.java b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java similarity index 61% rename from src/de/dhbwstuttgart/typinference/unify/model/PlaceholderType.java rename to src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java index 7b7503ee..5a3d5341 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/PlaceholderType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java @@ -1,9 +1,8 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; public final class PlaceholderType extends Type{ @@ -12,20 +11,32 @@ public final class PlaceholderType extends Type{ } @Override - public Set smArg(IFiniteClosure fc) { + Set smArg(IFiniteClosure fc) { return fc.smArg(this); } @Override - public Set grArg(IFiniteClosure fc) { + Set grArg(IFiniteClosure fc) { return fc.grArg(this); } + @Override + public Type setTypeParams(TypeParams newTp) { + return this; + } + @Override public int hashCode() { return typeName.hashCode(); } + @Override + Type apply(Unifier unif) { + if(unif.hasSubstitute(this)) + return unif.getSubstitute(this); + return this; + } + @Override public boolean equals(Object obj) { if(!(obj instanceof PlaceholderType)) @@ -33,12 +44,4 @@ public final class PlaceholderType extends Type{ return ((PlaceholderType) obj).getName().equals(typeName); } - - @Override - public Type apply(Unifier unif) { - if(this.equals(unif.getSource())) - return unif.getTarget(); - - return this; - } } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/SimpleType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java similarity index 69% rename from src/de/dhbwstuttgart/typinference/unify/model/SimpleType.java rename to src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java index 8e9e8a3f..ef01652a 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/SimpleType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java @@ -1,9 +1,8 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; public final class SimpleType extends Type { public SimpleType(String name, Type... typeParams) { @@ -15,15 +14,25 @@ public final class SimpleType extends Type { } @Override - public Set smArg(IFiniteClosure fc) { + Set smArg(IFiniteClosure fc) { return fc.smArg(this); } @Override - public Set grArg(IFiniteClosure fc) { + Set grArg(IFiniteClosure fc) { return fc.grArg(this); } + @Override + Type apply(Unifier unif) { + return new SimpleType(typeName, typeParams.apply(unif)); + } + + @Override + public Type setTypeParams(TypeParams newTp) { + return new SimpleType(new String(typeName), newTp); + } + @Override public int hashCode() { return typeName.hashCode(); @@ -41,12 +50,4 @@ public final class SimpleType extends Type { return other.getTypeParams().equals(typeParams); } - - @Override - public Type apply(Unifier unif) { - if(this.equals(unif.getSource())) - return unif.getTarget(); - - return new SimpleType(typeName, typeParams.apply(unif)); - } } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/SuperType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java similarity index 73% rename from src/de/dhbwstuttgart/typinference/unify/model/SuperType.java rename to src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java index 15c432d2..2503e748 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/SuperType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SuperType.java @@ -1,9 +1,8 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; public final class SuperType extends Type { @@ -29,15 +28,25 @@ public final class SuperType extends Type { } @Override - public Set smArg(IFiniteClosure fc) { + public Type setTypeParams(TypeParams newTp) { + return new SuperType(superedType.setTypeParams(newTp)); + } + + @Override + Set smArg(IFiniteClosure fc) { return fc.smArg(this); } @Override - public Set grArg(IFiniteClosure fc) { + Set grArg(IFiniteClosure fc) { return fc.grArg(this); } + @Override + Type apply(Unifier unif) { + return new SuperType(superedType.apply(unif)); + } + @Override public int hashCode() { return superedType.hashCode() + 17; @@ -51,9 +60,4 @@ public final class SuperType extends Type { SuperType other = (SuperType) obj; return other.getSuperedType().equals(superedType); } - - @Override - public Type apply(Unifier unif) { - return new SuperType(superedType.apply(unif)); - } } diff --git a/src/de/dhbwstuttgart/typinference/unify/model/Type.java b/src/de/dhbwstuttgart/typeinference/unify/model/Type.java similarity index 72% rename from src/de/dhbwstuttgart/typinference/unify/model/Type.java rename to src/de/dhbwstuttgart/typeinference/unify/model/Type.java index a9e94862..3c179110 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/Type.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Type.java @@ -1,9 +1,8 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; public abstract class Type { @@ -28,11 +27,13 @@ public abstract class Type { return typeParams; } - public abstract Set smArg(IFiniteClosure fc); + public abstract Type setTypeParams(TypeParams newTp); - public abstract Set grArg(IFiniteClosure fc); + abstract Set smArg(IFiniteClosure fc); - public abstract Type apply(Unifier unif); + abstract Set grArg(IFiniteClosure fc); + + abstract Type apply(Unifier unif); @Override public String toString() { diff --git a/src/de/dhbwstuttgart/typinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java similarity index 73% rename from src/de/dhbwstuttgart/typinference/unify/model/TypeParams.java rename to src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index d723395d..966a561b 100644 --- a/src/de/dhbwstuttgart/typinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -1,10 +1,8 @@ -package de.dhbwstuttgart.typinference.unify.model; +package de.dhbwstuttgart.typeinference.unify.model; import java.util.Arrays; import java.util.Iterator; -import de.dhbwstuttgart.typeinference.unifynew.Unifier; - public final class TypeParams implements Iterable{ private final Type[] typeParams; @@ -42,6 +40,17 @@ public final class TypeParams implements Iterable{ return new TypeParams(newParams); } + public boolean occurs(PlaceholderType t) { + for(Type p : typeParams) + if(p instanceof PlaceholderType) + if(p.equals(t)) + return true; + else + if(p.getTypeParams().occurs(t)) + return true; + return false; + } + public boolean contains(Type t) { for(Type t1 : typeParams) if(t1.equals(t1)) @@ -52,6 +61,13 @@ public final class TypeParams implements Iterable{ public Type get(int i) { return typeParams[i]; } + + public TypeParams set(Type t, int idx) { + Type[] newparams = Arrays.copyOf(typeParams, typeParams.length); + newparams[idx] = t; + return new TypeParams(newparams); + } + @Override public Iterator iterator() { diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java new file mode 100644 index 00000000..0a1fde25 --- /dev/null +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -0,0 +1,63 @@ +package de.dhbwstuttgart.typeinference.unify.model; + +import java.util.HashMap; +import java.util.Map.Entry; +import java.util.Set; +import java.util.function.Function; + +public class Unifier implements Function { + private HashMap substitutions = new HashMap<>(); + + public static Unifier IDENTITY = new Unifier(); + + public Unifier(PlaceholderType source, Type target) { + substitutions.put(source, target); + } + + /** + * Identity function as an "unifier". + */ + public Unifier() { + + } + + public void Add(PlaceholderType source, Type target) { + Unifier tempU = new Unifier(source, target); + for(PlaceholderType pt : substitutions.keySet()) + substitutions.put(pt, substitutions.get(pt).apply(tempU)); + substitutions.put(source, target); + } + + @Override + public Type apply(Type t) { + return t.apply(this); + } + + public MPair apply(MPair p) { + return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp()); + } + + public boolean hasSubstitute(PlaceholderType t) { + return substitutions.containsKey(t); + } + + public Type getSubstitute(Type t) { + return substitutions.get(t); + } + + public Set> getSubstitutions() { + return substitutions.entrySet(); + } + + @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; + } +} + diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java b/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java index d21c5b60..c8996dc8 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java @@ -2,68 +2,89 @@ package de.dhbwstuttgart.typeinference.unifynew; import java.util.HashMap; import java.util.HashSet; -import java.util.Iterator; +import java.util.Optional; import java.util.Set; +import java.util.stream.Collectors; -import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType; -import de.dhbwstuttgart.syntaxtree.type.FunN; -import de.dhbwstuttgart.syntaxtree.type.RefType; -import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType; -import de.dhbwstuttgart.syntaxtree.type.Type; -import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder; -import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; - -/** - * First three bits indicate the meta type: - * 000b = 0 = Simpletype - * 001b = 1 = Extends - * 010b = 2 = Super - * 011b = 3 = Type Placeholder - * 100b = 4 = Function - * - * @author DH10STF - * - */ public class Mapping { - private static final int ST_MASK = 0; - private static final int EXTENDS_MASK = 536870912; - private static final int SUPER_MASK = 1073741824; - private static final int TPH_MASK = 1610612736; - private static final int FUN_MASK = -2147483648; + private HashMap backwardMap = new HashMap<>(); + private HashMap forwardMap = new HashMap<>(); + private Set irreversible = new HashSet<>(); - private static HashMap mapping; - - public Set createMapping(Iterable types) { - mapping = new HashMap<>(); - - Iterator iterator = types.iterator(); - while(iterator.hasNext() && mapping.size() <= 536870911) - createMapping(iterator.next()); - - return mapping.keySet(); + public Mapping(Set types) { + for(de.dhbwstuttgart.syntaxtree.type.Type t : types) { + } } - private void createMapping(Type type) { - /*if(type instanceof RefType) { - Set params = ((RefType) type).get_ParaList(); - params.stream().forEach(x -> createMapping(x)); + public de.dhbwstuttgart.typeinference.unify.model.Type map(de.dhbwstuttgart.syntaxtree.type.Type type) { + return forwardMap.get(type); + } + + public de.dhbwstuttgart.typeinference.unify.model.MPair map(de.dhbwstuttgart.typeinference.Pair pair) { + return new de.dhbwstuttgart.typeinference.unify.model.MPair(forwardMap.get(pair.TA1), forwardMap.get(pair.TA2), mapOp(pair.GetOperator())); + } + + public Set mapTypeSet(Set types) { + return types.stream().map(this::map).collect(Collectors.toCollection(HashSet::new)); + } + + public Set mapPairSet(Set pairs) { + return pairs.stream().map(this::map).collect(Collectors.toCollection(HashSet::new)); + } + + public Optional unmap(de.dhbwstuttgart.typeinference.unify.model.Type type) { + return irreversible.contains(type) ? Optional.of(backwardMap.get(type)) : Optional.empty(); + } + + public Optional unmap(de.dhbwstuttgart.typeinference.unify.model.MPair mpair) { + de.dhbwstuttgart.typeinference.unify.model.Type lhs = mpair.getLhsType(); + de.dhbwstuttgart.typeinference.unify.model.Type rhs = mpair.getRhsType(); + + if(irreversible.contains(lhs) || irreversible.contains(rhs)) + return Optional.empty(); + return Optional.of(new de.dhbwstuttgart.typeinference.Pair(backwardMap.get(lhs), backwardMap.get(rhs), unmapOp(mpair.getPairOp()))); + } + + public Optional> unmapTypeSet(Set types) { + Set result = types.stream().map(this::unmap).filter(x -> x.isPresent()).map(x -> x.get()).collect(Collectors.toCollection(HashSet::new)); + return result.size() == types.size() ? Optional.of(result) : Optional.empty(); + } + + public Optional> unmapPairSet(Set pairs) { + Set result = pairs.stream().map(this::unmap).filter(x -> x.isPresent()).map(x -> x.get()).collect(Collectors.toCollection(HashSet::new)); + return result.size() == pairs.size() ? Optional.of(result) : Optional.empty(); + } + + private de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator mapOp(de.dhbwstuttgart.typeinference.Pair.PairOperator op) { + /* + * TODO + * Warum hat der PairOp nur drei Werte? Wie wird SMALLERDOTWC etc im anderen Pair geregelt? + */ + + switch(op) { + case Equal: + return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.EQUALS; + case Smaller: + return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.SMALLER; + case SmallerExtends: + return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.SMALLERDOT; + default: + return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.EQUALS; + } + } + + private de.dhbwstuttgart.typeinference.Pair.PairOperator unmapOp(de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator op) { + switch(op) { + case EQUALS: + return de.dhbwstuttgart.typeinference.Pair.PairOperator.Equal; + case SMALLER: + return de.dhbwstuttgart.typeinference.Pair.PairOperator.Smaller; + case SMALLERDOT: + return de.dhbwstuttgart.typeinference.Pair.PairOperator.SmallerExtends; + default: + return de.dhbwstuttgart.typeinference.Pair.PairOperator.Equal; } - */ - int typeId = mapping.size(); - - if(type instanceof RefType) - typeId |= ST_MASK; - else if(type instanceof SuperWildcardType) - typeId |= SUPER_MASK; - else if(type instanceof ExtendsWildcardType) - typeId |= EXTENDS_MASK; - else if(type instanceof TypePlaceholder) - typeId |= TPH_MASK; - else if(type instanceof FunN) - typeId |= FUN_MASK; - - //mapping.put(new MType()) } } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 3631ed24..6db1a512 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -1,13 +1,21 @@ package de.dhbwstuttgart.typeinference.unifynew; +import java.util.AbstractMap; +import java.util.ArrayList; import java.util.HashSet; +import java.util.Iterator; +import java.util.Map.Entry; +import java.util.Optional; import java.util.Set; +import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; -import de.dhbwstuttgart.typinference.unify.model.Type; -import de.dhbwstuttgart.typinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; /** * Implementation of the Martelli-Montanari unification algorithm. @@ -16,65 +24,114 @@ import de.dhbwstuttgart.typinference.unify.model.TypeParams; public class MartelliMontanariUnify implements IUnify { @Override - public Unifier unify(Set terms) { - // TODO Auto-generated method stub - return null; + public Optional unify(Set terms) { + if(terms.size() < 2) + return Optional.of(Unifier.IDENTITY); + + ArrayList termsQ = new ArrayList(); + Iterator iter = terms.iterator(); + Type prev = iter.next(); + while(iter.hasNext()) { + Type next = iter.next(); + termsQ.add(new MPair(prev, next, PairOperator.EQUALS)); + prev = next; + } + + Unifier mgu = Unifier.IDENTITY; + + int idx = 0; + while(idx < termsQ.size()) { + MPair pair = termsQ.get(idx); + + if(delete(pair)) { + termsQ.remove(idx); + continue; + } + + Optional> optSet = decompose(pair); + + if(optSet == null) + return Optional.empty(); // Unification failed + + if(optSet.isPresent()) { + termsQ.addAll(optSet.get()); + idx = idx+1 == termsQ.size() ? 0 : idx+1; + continue; + } + + Optional optPair = swap(pair); + + if(optPair.isPresent()) { + termsQ.add(optPair.get()); + idx = idx+1 == termsQ.size() ? 0 : idx+1; + continue; + } + + // Occurs-Check + if(pair.getLhsType() instanceof PlaceholderType + && pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType())) + return Optional.empty(); + + Optional> optUni = eliminate(pair); + + if(optUni.isPresent()) { + Entry substitution = optUni.get(); + mgu.Add(substitution.getKey(), substitution.getValue()); + termsQ = termsQ.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new)); + idx = idx+1 == termsQ.size() ? 0 : idx+1; + continue; + } + + idx++; + } + + return Optional.of(mgu); } private boolean delete(MPair pair) { return pair.getRhsType().equals(pair.getLhsType()); } - private Set decompose(MPair pair) { + private Optional> decompose(MPair pair) { Set result = new HashSet<>(); Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); - - if(!rhs.getName().equals(lhs.getName()) || rhs.getTypeParams().size() != lhs.getTypeParams().size()) - return null; // conflict - + TypeParams rhsTypeParams = rhs.getTypeParams(); TypeParams lhsTypeParams = lhs.getTypeParams(); + + if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0) + return Optional.empty(); + + if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size()) + return null; // conflict for(int i = 0; i < rhsTypeParams.size(); i++) result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT)); - return result; + return Optional.of(result); } - private MPair swap(MPair pair) { + private Optional swap(MPair pair) { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); - if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0) - return new MPair(rhs, lhs, PairOperator.EQUALSDOT); - return pair; + if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType)) + return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT)); + + return Optional.empty(); } - - private Unifier eliminate(MPair pair) { + + private Optional> eliminate(MPair pair) { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); - TypeParams rhsTypeParams = rhs.getTypeParams(); + // TODO only apply when lhs is element of vars(termsQ)? - for(Type t : rhsTypeParams) - if(lhs.equals(t)) - return new Unifier(); //identity-"unifier" - - return new Unifier(lhs, rhs); - } - - private boolean check(MPair pair) { - Type rhs = pair.getRhsType(); - Type lhs = pair.getLhsType(); - - TypeParams rhsTypeParams = rhs.getTypeParams(); - - for(Type t : rhsTypeParams) - if(lhs.equals(t)) - return false; - - return true; + if(!(lhs instanceof PlaceholderType)) + return Optional.empty(); + + return Optional.of(new AbstractMap.SimpleImmutableEntry((PlaceholderType) lhs, rhs)); } } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java index 3dff9384..e41525f5 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java @@ -1,22 +1,27 @@ package de.dhbwstuttgart.typeinference.unifynew; 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.stream.Collectors; import junit.framework.Assert; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; -import de.dhbwstuttgart.typinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; -import de.dhbwstuttgart.typinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typinference.unify.model.SimpleType; -import de.dhbwstuttgart.typinference.unify.model.SuperType; -import de.dhbwstuttgart.typinference.unify.model.Type; -import de.dhbwstuttgart.typinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.SimpleType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; public class RuleSet implements IRuleSet{ @@ -342,11 +347,11 @@ public class RuleSet implements IRuleSet{ TypeParams typeDParams = typeD.getTypeParams(); TypeParams typeDgenParams = typeDgen.getTypeParams(); - Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0)); + Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0)); for(int i = 1; i < typeDParams.size(); i++) - unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i))); + unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), typeDs, PairOperator.SMALLERDOT)); + return Optional.of(new MPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT)); } @Override @@ -388,11 +393,11 @@ public class RuleSet implements IRuleSet{ TypeParams typeDParams = typeD.getTypeParams(); TypeParams typeDgenParams = typeDgen.getTypeParams(); - Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0)); + Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0)); for(int i = 1; i < typeDParams.size(); i++) - unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i))); + unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), typeExtDs, PairOperator.SMALLERDOTWC)); + return Optional.of(new MPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC)); } @Override @@ -440,11 +445,11 @@ public class RuleSet implements IRuleSet{ TypeParams typeDParams = typeSupD.getTypeParams(); TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams(); - Unifier unif = new Unifier(typeSupDsgenParams.get(0), typeDParams.get(0)); + Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0)); for(int i = 1; i < typeDParams.size(); i++) - unif.andThen(new Unifier(typeSupDsgenParams.get(i), typeDParams.get(i))); + unif.andThen(new Unifier((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i))); - return Optional.of(new MPair(newLhs.apply(unif), newRhs, PairOperator.SMALLERDOTWC)); + return Optional.of(new MPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC)); } /** @@ -516,9 +521,42 @@ public class RuleSet implements IRuleSet{ } @Override - public Set subst(Set pair) { - // TODO Auto-generated method stub - return null; + public Optional> subst(Set pairs) { + HashMap typeMap = new HashMap<>(); + + for(MPair pair : pairs) { + Type t1 = pair.getLhsType(); + Type t2 = pair.getRhsType(); + if(!typeMap.containsKey(t1)) + typeMap.put(t1, 0); + if(!typeMap.containsKey(t2)) + typeMap.put(t2, 0); + typeMap.put(t1, typeMap.get(t1)+1); + typeMap.put(t2, typeMap.get(t2)+1); + } + + ArrayList result = new ArrayList(pairs); + + boolean applied = false; + + for(int i = 0; i < result.size(); i++) { + MPair pair = result.get(i); + PlaceholderType lhsType = null; + Type rhsType; + + if(pair.getPairOp() == PairOperator.EQUALSDOT + && pair.getLhsType() instanceof PlaceholderType) + lhsType = (PlaceholderType) pair.getLhsType(); + if(lhsType != null + && !((rhsType = pair.getRhsType()) instanceof PlaceholderType) + && typeMap.get(lhsType) > 1 // The type occurs in more pairs in the set than just the recent pair. + && !rhsType.getTypeParams().occurs(lhsType)) { + Unifier uni = new Unifier(lhsType, rhsType); + result = result.stream().map(uni::apply).collect(Collectors.toCollection(ArrayList::new)); + applied = true; + } + } + + return applied ? Optional.of(new HashSet<>(result)) : Optional.empty(); } - } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java deleted file mode 100644 index 4528a934..00000000 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java +++ /dev/null @@ -1,36 +0,0 @@ -package de.dhbwstuttgart.typeinference.unifynew; - -import java.util.function.Function; - -import de.dhbwstuttgart.typinference.unify.model.Type; -import de.dhbwstuttgart.typinference.unify.model.TypeParams; - -public class Unifier implements Function { - private Type source; - private Type target; - - public Unifier(Type source, Type target) { - this.source = source; - this.target = target; - } - - /** - * Identity function as an "unifier". - */ - public Unifier() { - - } - - @Override - public Type apply(Type t) { - return t.apply(this); - } - - public Type getSource() { - return source; - } - - public Type getTarget() { - return target; - } -} diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index d8354f53..548340b3 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -1,11 +1,13 @@ package de.dhbwstuttgart.typeinference.unifynew; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; import java.util.HashSet; 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.stream.Collectors; @@ -16,12 +18,15 @@ import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations; -import de.dhbwstuttgart.typinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; -import de.dhbwstuttgart.typinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typinference.unify.model.SuperType; -import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; +import de.dhbwstuttgart.typeinference.unify.model.Unifier; /** @@ -30,7 +35,7 @@ import de.dhbwstuttgart.typinference.unify.model.Type; */ public class Unify { - public Menge> unify(Set eq, IFiniteClosure fc) { + public Set> unify(Set eq, IFiniteClosure fc) { /* * Step 1: Repeated application of reduce, adapt, erase, swap */ @@ -47,14 +52,13 @@ public class Unify { /* * 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 */ - // Sets that originate from pair pattern matching - // Sets of the "second level" - List>> pairSetsSet = calculatePairSets(eq2s, fc); - - // The sets of the "first level" - Set> sets = new HashSet>(); + // All Sets + List> sets = new ArrayList>(); if(eq1s.size() != 0) sets.add(eq1s); // Add Eq1' @@ -67,41 +71,58 @@ public class Unify { if(bufferSet.size() != 0) sets.add(bufferSet); + // Sets that originate from pair pattern matching + // Sets of the "second level" + + sets.addAll(calculatePairSets(eq2s, fc)); + /* Up to here, no cartesian products are calculated. * Around here, filters for pairs and sets can be applied */ ISetOperations setOps = new GuavaSetOperations(); - // Calculate the inner cartesian products - // Cartesian products of the second level - - // AddAll -> nur add - for(List> pairSets : pairSetsSet) // Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte - sets.add(setOps.cartesianProduct(pairSets).stream().map(x -> new HashSet<>(x)).collect(Collectors.toSet())); - - System.out.println(sets); - - // Calculate the outer cartesian products - // Cartesian products of the first level - Set> eqsSet = setOps.cartesianProduct(new ArrayList<>(sets)); - - - System.out.println(eqsSet); + // Calculate the cartesian products + Set> result = setOps.cartesianProduct(sets).stream() + .map(x -> new HashSet(x)).collect(Collectors.toCollection(HashSet::new)); + //System.out.println(result); + /* * Step 5: Substitution */ + /* + * TODO + * Im Paper wird Eq'' genannt, es wird also von einer Menge in einer Menge in einer Menge ausgegangen. + * Durch das flache Kartesische Produkt gibt es hier aber nur Mengen in Mengen. + * Richtig so? + */ + + IRuleSet rules = new RuleSet(fc); + Set> changed = new HashSet<>(); + Set> unchanged = new HashSet<>(); + + for(Set eqss : result) { + Optional> newEqss = rules.subst(eqss); + if(newEqss.isPresent()) + changed.add(newEqss.get()); + else + unchanged.add(eqss); + } + /* - * Step 6: a) Restart for pairs where subst was applied - * b) Union over everything + * Step 6 a) Restart for pairs where subst was applied + * b) Build the union over everything */ - + + for(Set eqss : changed) + unchanged.addAll(this.unify(eqss, fc)); + /* - * Step 7: Filter result for solved pairs + * Step 7: Filter result for solved pairs TODO wie? */ - return null; + return unchanged; } @@ -196,11 +217,8 @@ public class Unify { } - protected List>> calculatePairSets(Set eq2s, IFiniteClosure fc) { - List>> result = new ArrayList>>(); - for(int i = 0; i < 8; i++) - result.add(new ArrayList>()); - + protected List> calculatePairSets(Set eq2s, IFiniteClosure fc) { + List> result = new ArrayList>(); for(MPair pair : eq2s) { @@ -210,12 +228,52 @@ public class Unify { // Case 1: (a <. Theta') if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) { - // TODO + Type thetaPrime = pair.getRhsType(); + Set set = new HashSet<>(); + IUnify unify = new MartelliMontanariUnify(); + + //Set cs = fc.getAllTypes(rhsType.getName()); + Type c = rhsType; + + //Set thetaQs = cs.stream().flatMap(x -> fc.smaller(x).stream()).collect(Collectors.toCollection(HashSet::new)); + Set thetaQs = fc.smaller(c); + + Set thetaQPrimes = new HashSet<>(); + + TypeParams cParams = c.getTypeParams(); + if(cParams.size() == 0) + thetaQPrimes.add(c); + else { + ArrayList> candidateParams = new ArrayList<>(); + for(Type param : cParams) + candidateParams.add(fc.grArg(param)); + Set permutations = new HashSet(); + permuteParams(candidateParams, 0, permutations, new Type[candidateParams.size()]); + + for(TypeParams tp : permutations) + thetaQPrimes.add(c.setTypeParams(tp)); + } + + for(Type tqp : thetaQPrimes) { + Optional opt = unify.unify(tqp, thetaPrime); + if(opt.isPresent()) { + Unifier unifier = opt.get(); + Set> substitutions = unifier.getSubstitutions(); + for(Entry sigma : substitutions) + set.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); + for(Type tq : thetaQs) { + Set smaller = fc.smaller(unifier.apply(tq)); + smaller.stream().map(x -> new MPair(lhsType, x, PairOperator.EQUALSDOT)).forEach(x -> set.add(x)); + } + } + } + + result.add(set); } // Case 2: (a <.? ? ext Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){ - // TODO + throw new NotImplementedException(); // TODO } // Case 3: (a <.? ? sup Theta') @@ -223,15 +281,14 @@ public class Unify { Set set = new HashSet<>(); for(Type theta : fc.smArg(rhsType)) set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT)); - - result.get(2).add(set); + result.add(set); } // Case 4: (a <.? Theta') else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) { Set set = new HashSet<>(); - set.add(new MPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT)); - result.get(3).add(set); + set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT)); + result.add(set); } // Case 5: (Theta <. a) @@ -239,7 +296,7 @@ public class Unify { Set set = new HashSet<>(); for(Type thetaS : fc.greater(lhsType)) set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.get(4).add(set); + result.add(set); } // Case 6: (? ext Theta <.? a) @@ -247,12 +304,12 @@ public class Unify { Set set = new HashSet<>(); for(Type thetaS : fc.grArg(lhsType)) set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.get(5).add(set); + result.add(set); } // Case 7: (? sup Theta <.? a) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) { - // TODO + throw new NotImplementedException(); // TODO } // Case 8: (Theta <.? a) @@ -260,10 +317,33 @@ public class Unify { Set set = new HashSet<>(); for(Type thetaS : fc.grArg(lhsType)) set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT)); - result.get(7).add(set); + result.add(set); } } - return result.stream().filter(x -> !x.isEmpty()).collect(Collectors.toList()); + return result; } + + protected void permuteParams(ArrayList> candidates, int idx, Set result, Type[] current) { + if(candidates.size() == idx) { + result.add(new TypeParams(Arrays.copyOf(current, current.length))); + return; + } + + Set localCandidates = candidates.get(idx); + + for(Type t : localCandidates) { + current[idx] = t; + permuteParams(candidates, idx+1, result, current); + } + } + + private Set getAllInstantiations(Type t, IFiniteClosure fc) { + Set result = new HashSet<>(); + result.add(t); + return result; + + // TODO + } + } diff --git a/test/unify/FiniteClosureBuilder.java b/test/unify/FiniteClosureBuilder.java index 815d637d..20552468 100644 --- a/test/unify/FiniteClosureBuilder.java +++ b/test/unify/FiniteClosureBuilder.java @@ -4,10 +4,10 @@ import java.util.HashSet; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typinference.unify.model.FiniteClosure; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; -import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; public class FiniteClosureBuilder { diff --git a/test/unify/FiniteClosureTest.java b/test/unify/FiniteClosureTest.java index d3744abe..85819ecd 100644 --- a/test/unify/FiniteClosureTest.java +++ b/test/unify/FiniteClosureTest.java @@ -6,8 +6,9 @@ import java.util.Set; import org.junit.Test; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.Type; public class FiniteClosureTest { @@ -54,4 +55,10 @@ public class FiniteClosureTest { System.out.println("SmArg(? extends List) = " + fc.smArg(tf.getExtendsType(tf.getSimpleType("List", "T")))); System.out.println("SmArg(? super List) = " + fc.smArg(tf.getSuperType(tf.getSimpleType("List", "T")))); } + + @Test + public void testGetGenericType() { + + // TODO + } } diff --git a/test/unify/RuleSetTest.java b/test/unify/RuleSetTest.java index fa08b1e7..1fe1359d 100644 --- a/test/unify/RuleSetTest.java +++ b/test/unify/RuleSetTest.java @@ -9,12 +9,12 @@ import junit.framework.Assert; import org.junit.Test; import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.SimpleType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; import de.dhbwstuttgart.typeinference.unifynew.RuleSet; -import de.dhbwstuttgart.typinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; -import de.dhbwstuttgart.typinference.unify.model.SimpleType; -import de.dhbwstuttgart.typinference.unify.model.SuperType; public class RuleSetTest { diff --git a/test/unify/StandardUnifyTest.java b/test/unify/StandardUnifyTest.java new file mode 100644 index 00000000..e08176ed --- /dev/null +++ b/test/unify/StandardUnifyTest.java @@ -0,0 +1,66 @@ +package unify; + +import java.util.HashSet; +import java.util.Set; + +import junit.framework.Assert; + +import org.junit.Test; + +import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify; + +public class StandardUnifyTest { + + @Test + public void testUnify() { + IUnify unify = new MartelliMontanariUnify(); + TypeFactory tf = new TypeFactory(); + + /* + * Positive Tests + */ + + Type x = tf.getPlaceholderType("x"); + Type y = tf.getPlaceholderType("y"); + Type f = tf.getSimpleType("f", x); + + // {f = y} + Set terms = new HashSet(); + + System.out.println(unify.unify(f, y).get()); + + // TODO ist das ergebnis { (x -> ? extends a), (y -> g) } in der richtigen form oder + // muss es { (x -> ? extends a), (y -> g) } sein? + // {f,x> = f} + Type g = tf.getSimpleType("g", "x"); + Type f1 = tf.getSimpleType("f", g, x); + Type a = tf.getExtendsType(tf.getPlaceholderType("a")); + Type f2 = tf.getSimpleType("f", y, a); + + terms = new HashSet<>(); + + System.out.println(unify.unify(f1, f2).get()); + + /* + * Negative Tests + */ + + // {f(x) =. x} + f = tf.getSimpleType("f", x); + Assert.assertFalse(unify.unify(f, x).isPresent()); + + // {f(x) =. f(x,y)} + f1 = tf.getSimpleType("f", "x"); + f2 = tf.getSimpleType("f", "x", "y"); + Assert.assertFalse(unify.unify(f1, f2).isPresent()); + + // {f(x) =. g(x)} + f1 = tf.getSimpleType("f", "x"); + f2 = tf.getSimpleType("g", "x"); + Assert.assertFalse(unify.unify(f1, f2).isPresent()); + } +} diff --git a/test/unify/TypeFactory.java b/test/unify/TypeFactory.java index 46b6f7bf..7fb896ae 100644 --- a/test/unify/TypeFactory.java +++ b/test/unify/TypeFactory.java @@ -3,11 +3,11 @@ package unify; import java.util.Arrays; import java.util.stream.Collectors; -import de.dhbwstuttgart.typinference.unify.model.ExtendsType; -import de.dhbwstuttgart.typinference.unify.model.PlaceholderType; -import de.dhbwstuttgart.typinference.unify.model.SimpleType; -import de.dhbwstuttgart.typinference.unify.model.SuperType; -import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.ExtendsType; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; +import de.dhbwstuttgart.typeinference.unify.model.SimpleType; +import de.dhbwstuttgart.typeinference.unify.model.SuperType; +import de.dhbwstuttgart.typeinference.unify.model.Type; public class TypeFactory { diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 38d5a1b9..51e178f4 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -1,14 +1,17 @@ package unify; +import java.util.ArrayList; import java.util.HashSet; import java.util.Set; import org.junit.Test; import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure; +import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; +import de.dhbwstuttgart.typeinference.unify.model.Type; +import de.dhbwstuttgart.typeinference.unify.model.TypeParams; import de.dhbwstuttgart.typeinference.unifynew.Unify; -import de.dhbwstuttgart.typinference.unify.model.MPair; -import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; public class UnifyTest extends Unify { @@ -18,25 +21,29 @@ public class UnifyTest extends Unify { FiniteClosureBuilder fcb = new FiniteClosureBuilder(); Set eq = new HashSet(); - fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object")); + //fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object")); fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number")); fcb.add(tf.getSimpleType("Double"), tf.getSimpleType("Number")); + //fcb.add(tf.getSimpleType("List", "T")); IFiniteClosure fc = fcb.getCollectionExample(); // Vector <. Vector // Vector - // A <. Number + // A <. Integer + // Number <. A // Double <. B // B <. Object eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("Number"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT)); + eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", tf.getSimpleType("Number")), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getPlaceholderType("B"), tf.getSimpleType("Object"), PairOperator.EQUALSDOT)); + //eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT)); + //eq.add(new MPair(tf.getPlaceholderType("B"), tf.getSimpleType("Object"), PairOperator.EQUALSDOT)); - this.unify(eq, fc); + System.out.println(this.unify(eq, fc)); } @@ -50,4 +57,32 @@ public class UnifyTest extends Unify { } + @Test + public void permuteParamsTest() { + TypeFactory tf = new TypeFactory(); + ArrayList> candidates = new ArrayList<>(); + + Set p1 = new HashSet<>(); + p1.add(tf.getPlaceholderType("p11")); + p1.add(tf.getExtendsType(tf.getSimpleType("p12"))); + p1.add(tf.getSimpleType("p13")); + + Set p2 = new HashSet<>(); + p2.add(tf.getPlaceholderType("p21")); + p2.add(tf.getPlaceholderType("p22")); + + Set p3 = new HashSet<>(); + p3.add(tf.getSimpleType("p31", "T")); + p3.add(tf.getSimpleType("p32")); + + candidates.add(p1); + candidates.add(p2); + candidates.add(p3); + + Set result = new HashSet<>(); + permuteParams(candidates, 0, result, new Type[candidates.size()]); + + System.out.println(result); + } + }