diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index 92dd941d8..1f73b5508 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -1,5 +1,6 @@ package de.dhbwstuttgart.typeinference.unify.interfaces; +import java.util.Optional; import java.util.Set; import de.dhbwstuttgart.typeinference.unifynew.Unifier; @@ -10,5 +11,5 @@ import de.dhbwstuttgart.typinference.unify.model.MPair; * @author Florian Steurer */ public interface IUnify { - public Set unify(Set terms); + public Optional> unify(Set terms); } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 89e02cbbe..0f626010b 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -11,6 +11,7 @@ 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.PlaceholderType; import de.dhbwstuttgart.typinference.unify.model.Type; import de.dhbwstuttgart.typinference.unify.model.TypeParams; @@ -21,7 +22,7 @@ import de.dhbwstuttgart.typinference.unify.model.TypeParams; public class MartelliMontanariUnify implements IUnify { @Override - public Set unify(Set terms) { + public Optional> unify(Set terms) { Queue termsQ = new LinkedList<>(terms); Set result = new HashSet<>(); @@ -35,7 +36,7 @@ public class MartelliMontanariUnify implements IUnify { Optional> optSet = decompose(pair); if(optSet == null) - return new HashSet<>(); // Unification failed + return Optional.empty(); // Unification failed if(optSet.isPresent()) { termsQ.addAll(optSet.get()); @@ -55,13 +56,16 @@ public class MartelliMontanariUnify implements IUnify { 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? + // TODO occurs check notwendig? + if(!check(pair)) // Occurs-Check + return Optional.empty(); } - return result; + return Optional.of(result); } private boolean delete(MPair pair) { @@ -96,6 +100,9 @@ public class MartelliMontanariUnify implements IUnify { 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(); } diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java index 0428a84ef..db821905e 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unifier.java @@ -40,4 +40,10 @@ public class Unifier implements Function { public Type getTarget() { return target; } + + @Override + public String toString() { + return source.toString() + " -> " + target.toString(); + } } + diff --git a/test/unify/StandardUnifyTest.java b/test/unify/StandardUnifyTest.java new file mode 100644 index 000000000..41aff15f8 --- /dev/null +++ b/test/unify/StandardUnifyTest.java @@ -0,0 +1,74 @@ +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.unifynew.MartelliMontanariUnify; +import de.dhbwstuttgart.typinference.unify.model.MPair; +import de.dhbwstuttgart.typinference.unify.model.Type; +import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator; + +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 z = tf.getPlaceholderType("z"); + Type f = tf.getSimpleType("f", x); + + // {x =. z, 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(terms).get()); + + // {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()); + + /* + * Negative Tests + */ + + // {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()); + + // {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()); + + // {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()); + } +}