diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index d3c8b6d7..a573b5d2 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -1,18 +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.unify.model.MPair; import de.dhbwstuttgart.typeinference.unify.model.Type; import de.dhbwstuttgart.typeinference.unifynew.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 Optional> unify(Set terms); - public Optional> unify(Type t1, Type t2); + 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/typeinference/unify/model/PlaceholderType.java b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java index 12ecac01..0514517d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java @@ -36,9 +36,8 @@ public final class PlaceholderType extends Type{ @Override public Type apply(Unifier unif) { - if(this.equals(unif.getSource())) - return unif.getTarget(); - + if(unif.hasSubstitute(this)) + return unif.getSubstitute(this); return this; } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java index 301d5d91..27581016 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/SimpleType.java @@ -44,9 +44,6 @@ public final class SimpleType extends Type { @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/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index d56a80b0..3fdd8679 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -52,6 +52,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/unifynew/Mapping.java b/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java index 97c2823f..c8996dc8 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java @@ -14,7 +14,6 @@ public class Mapping { public Mapping(Set types) { for(de.dhbwstuttgart.syntaxtree.type.Type t : types) { - // TODO } } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 900af874..101f861a 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -1,18 +1,20 @@ package de.dhbwstuttgart.typeinference.unifynew; +import java.util.AbstractMap; +import java.util.ArrayList; import java.util.HashSet; -import java.util.LinkedList; +import java.util.Iterator; +import java.util.Map.Entry; import java.util.Optional; -import java.util.Queue; import java.util.Set; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; 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.MPair.PairOperator; /** * Implementation of the Martelli-Montanari unification algorithm. @@ -21,23 +23,29 @@ import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator; public class MartelliMontanariUnify implements IUnify { @Override - public Optional> unify(Type t1, Type t2) { - Set terms = new HashSet(); - terms.add(new MPair(t1, t2, PairOperator.EQUALSDOT)); - return unify(terms); - } - - @Override - public Optional> unify(Set terms) { - Queue termsQ = new LinkedList<>(terms); - Set result = new HashSet<>(); + 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; + } - while(!termsQ.isEmpty()) { - MPair pair = termsQ.poll(); + Unifier mgu = Unifier.IDENTITY; + + int idx = 0; + while(idx < termsQ.size()) { + MPair pair = termsQ.get(idx); - if(delete(pair)) + if(delete(pair)) { + termsQ.remove(idx); continue; + } Optional> optSet = decompose(pair); @@ -46,6 +54,7 @@ public class MartelliMontanariUnify implements IUnify { if(optSet.isPresent()) { termsQ.addAll(optSet.get()); + idx = idx+1 == termsQ.size() ? 0 : idx+1; continue; } @@ -53,25 +62,27 @@ public class MartelliMontanariUnify implements IUnify { if(optPair.isPresent()) { termsQ.add(optPair.get()); + idx = idx+1 == termsQ.size() ? 0 : idx+1; continue; } - Optional optUni = eliminate(pair); - - if(optUni.isPresent()) { - Unifier uni = optUni.get(); - termsQ = termsQ.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new)); - result = result.stream().map(uni::apply).collect(Collectors.toCollection(HashSet::new)); - result.add(pair); - continue; - } - - // TODO occurs check notwendig? if(!check(pair)) // Occurs-Check 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(result); + return Optional.of(mgu); } private boolean delete(MPair pair) { @@ -103,28 +114,12 @@ public class MartelliMontanariUnify implements IUnify { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); - if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0) - return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT)); - if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType)) return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT)); return Optional.empty(); } - private Optional eliminate(MPair pair) { - Type rhs = pair.getRhsType(); - Type lhs = pair.getLhsType(); - - TypeParams rhsTypeParams = rhs.getTypeParams(); - - for(Type t : rhsTypeParams) - if(lhs.equals(t)) - return Optional.empty(); - - return Optional.of(new Unifier(lhs, rhs)); - } - private boolean check(MPair pair) { Type rhs = pair.getRhsType(); Type lhs = pair.getLhsType(); @@ -137,4 +132,16 @@ public class MartelliMontanariUnify implements IUnify { return true; } + + private Optional> eliminate(MPair pair) { + Type rhs = pair.getRhsType(); + Type lhs = pair.getLhsType(); + + // TODO only apply when lhs is element of vars(termsQ)? + + 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 a045a9d2..4c14cdaf 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java @@ -346,9 +346,9 @@ 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(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT)); } @@ -392,9 +392,9 @@ 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(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC)); } @@ -444,9 +444,9 @@ 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(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC)); } @@ -547,7 +547,7 @@ public class RuleSet implements IRuleSet{ && !((rhsType = pair.getRhsType()) instanceof PlaceholderType) && typeMap.get(lhsType) > 1 // The type occurs in more pairs in the set than just the recent pair. && !occurs(lhsType, rhsType)) { - Unifier uni = new Unifier(lhsType, rhsType); + Unifier uni = new Unifier((PlaceholderType) lhsType, rhsType); result = result.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new)); applied = true; } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java index 82e8d31e..8979575d 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java @@ -1,20 +1,20 @@ package de.dhbwstuttgart.typeinference.unifynew; -import java.util.Set; +import java.util.HashMap; +import java.util.Map.Entry; import java.util.function.Function; -import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType; import de.dhbwstuttgart.typeinference.unify.model.Type; -import de.dhbwstuttgart.typeinference.unify.model.TypeParams; public class Unifier implements Function { - private Type source; - private Type target; + private HashMap substitutions = new HashMap<>(); - public Unifier(Type source, Type target) { - this.source = source; - this.target = target; + public static Unifier IDENTITY = new Unifier(); + + public Unifier(PlaceholderType source, Type target) { + substitutions.put(source, target); } /** @@ -23,6 +23,10 @@ public class Unifier implements Function { public Unifier() { } + + public void Add(PlaceholderType source, Type target) { + substitutions.put(source, target); + } @Override public Type apply(Type t) { @@ -33,17 +37,23 @@ public class Unifier implements Function { return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp()); } - public Type getSource() { - return source; + public boolean hasSubstitute(PlaceholderType t) { + return substitutions.containsKey(t); } - public Type getTarget() { - return target; + public Type getSubstitute(Type t) { + return substitutions.get(t); } - + @Override public String toString() { - return source.toString() + " -> " + target.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/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 94ee1f0d..65193117 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -23,6 +23,7 @@ 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; /** @@ -231,10 +232,12 @@ public class Unify { .flatMap(x -> fc.smaller(x).stream()) .collect(Collectors.toCollection(HashSet::new)); Set possibleThetaPrimes = possibleThetas.stream() - .flatMap(x -> getAllInstantiations(x).stream()) + .flatMap(x -> getAllInstantiations(x, fc).stream()) .collect(Collectors.toCollection(HashSet::new)); - Set unifiers = possibleThetaPrimes.stream() + // TODO + + /*Set unifiers = possibleThetaPrimes.stream() .map(x -> unify.unify(x, rhsType)) .filter(x -> x.isPresent()) .flatMap(x -> x.get().stream()) @@ -254,6 +257,8 @@ public class Unify { result.add(resultSet); // TODO Speedup - Potenzial durch auschließen unmöglicher kombinationen (z.B. wenn in theta' eine Variable festgelegt ist) // TODO speedup durch pipelining mit streams + // TODO speedup teure berechnungen mit proxy rauszögern + */ } // Case 2: (a <.? ? ext Theta') @@ -309,7 +314,12 @@ public class Unify { return result; } - private Set getAllInstantiations(Type t) { - return new HashSet<>(); + private Set getAllInstantiations(Type t, IFiniteClosure fc) { + Set result = new HashSet<>(); + result.add(t); + return result; + + // TODO } + } diff --git a/test/unify/StandardUnifyTest.java b/test/unify/StandardUnifyTest.java index 33b4bde9..e08176ed 100644 --- a/test/unify/StandardUnifyTest.java +++ b/test/unify/StandardUnifyTest.java @@ -26,26 +26,24 @@ public class StandardUnifyTest { Type x = tf.getPlaceholderType("x"); Type y = tf.getPlaceholderType("y"); - Type z = tf.getPlaceholderType("z"); Type f = tf.getSimpleType("f", x); - // {x =. z, f = y} + // {f = y} Set terms = new HashSet(); - terms.add(new MPair(x, z, PairOperator.EQUALSDOT)); - terms.add(new MPair(f, y, PairOperator.EQUALSDOT)); + + System.out.println(unify.unify(f, y).get()); - System.out.println(unify.unify(terms).get()); - - // {f,x> = f} + // 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<>(); - terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT)); - - System.out.println(unify.unify(terms).get()); + + System.out.println(unify.unify(f1, f2).get()); /* * Negative Tests @@ -53,22 +51,16 @@ public class StandardUnifyTest { // {f(x) =. x} f = tf.getSimpleType("f", x); - terms = new HashSet<>(); - terms.add(new MPair(f, x, PairOperator.EQUALSDOT)); - Assert.assertFalse(unify.unify(terms).isPresent()); + Assert.assertFalse(unify.unify(f, x).isPresent()); // {f(x) =. f(x,y)} f1 = tf.getSimpleType("f", "x"); f2 = tf.getSimpleType("f", "x", "y"); - terms = new HashSet<>(); - terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT)); - Assert.assertFalse(unify.unify(terms).isPresent()); + Assert.assertFalse(unify.unify(f1, f2).isPresent()); // {f(x) =. g(x)} f1 = tf.getSimpleType("f", "x"); f2 = tf.getSimpleType("g", "x"); - terms = new HashSet<>(); - terms.add(new MPair(f1, f2, PairOperator.EQUALSDOT)); - Assert.assertFalse(unify.unify(terms).isPresent()); + Assert.assertFalse(unify.unify(f1, f2).isPresent()); } } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index 3c27ea0d..eb7f9f5b 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -33,7 +33,7 @@ public class UnifyTest extends Unify { 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("Integer"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), 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));