From bdd018d922e0f11933ad1e99e91102da6f63fd9b Mon Sep 17 00:00:00 2001 From: Florian Steurer Date: Sun, 27 Dec 2015 15:01:59 +0100 Subject: [PATCH] =?UTF-8?q?regel=204=20f=C3=BCr=20paare=20(a=20<.=20Theta'?= =?UTF-8?q?)=20(funktioniert=20zu=2099=20Prozent=20noch=20nicht=20richtig)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../unify/interfaces/IFiniteClosure.java | 1 + .../unify/interfaces/IUnify.java | 3 ++ .../unify/model/FiniteClosure.java | 8 +++++ .../unifynew/MartelliMontanariUnify.java | 8 ++++- .../typeinference/unifynew/Unify.java | 36 ++++++++++++++++++- test/unify/UnifyTest.java | 6 ++-- 6 files changed, 58 insertions(+), 4 deletions(-) diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java index 3e8d8d7d..62b65b27 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IFiniteClosure.java @@ -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/IUnify.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java index 05b7e8da..d3c8b6d7 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IUnify.java @@ -4,6 +4,7 @@ import java.util.Optional; import java.util.Set; import de.dhbwstuttgart.typeinference.unify.model.MPair; +import de.dhbwstuttgart.typeinference.unify.model.Type; import de.dhbwstuttgart.typeinference.unifynew.Unifier; /** @@ -12,4 +13,6 @@ import de.dhbwstuttgart.typeinference.unifynew.Unifier; */ public interface IUnify { public Optional> unify(Set terms); + + public Optional> unify(Type t1, Type t2); } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index 9899bef4..e618482d 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -4,6 +4,7 @@ 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.typeinference.unify.model.MPair.PairOperator; @@ -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/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java index 12666fe4..900af874 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java @@ -5,7 +5,6 @@ import java.util.LinkedList; import java.util.Optional; import java.util.Queue; import java.util.Set; -import java.util.Stack; import java.util.stream.Collectors; import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify; @@ -21,6 +20,13 @@ 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); diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java index 800ce767..94ee1f0d 100644 --- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java +++ b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java @@ -16,6 +16,7 @@ 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.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; @@ -223,7 +224,36 @@ public class Unify { // Case 1: (a <. Theta') if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) { - // TODO + IUnify unify = new MartelliMontanariUnify(); + + Set possibleCs = fc.getAllTypes(rhsType.getName()); + Set possibleThetas = possibleCs.stream() + .flatMap(x -> fc.smaller(x).stream()) + .collect(Collectors.toCollection(HashSet::new)); + Set possibleThetaPrimes = possibleThetas.stream() + .flatMap(x -> getAllInstantiations(x).stream()) + .collect(Collectors.toCollection(HashSet::new)); + + Set unifiers = possibleThetaPrimes.stream() + .map(x -> unify.unify(x, rhsType)) + .filter(x -> x.isPresent()) + .flatMap(x -> x.get().stream()) + .map(x -> new Unifier(x.getLhsType(), x.getRhsType())) + .collect(Collectors.toCollection(HashSet::new)); + + Set thetas = new HashSet<>(); + + for(Unifier sigma : unifiers) + for(Type thetaQuer : possibleThetas) + thetas.addAll(fc.smaller(sigma.apply(thetaQuer))); + + Set resultSet = new HashSet<>(); + thetas.forEach(x -> resultSet.add(new MPair(lhsType, x, PairOperator.EQUALSDOT))); + unifiers.forEach(x -> resultSet.add(new MPair(x.getSource(), x.getTarget(), PairOperator.EQUALSDOT))); + + 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 } // Case 2: (a <.? ? ext Theta') @@ -278,4 +308,8 @@ public class Unify { return result; } + + private Set getAllInstantiations(Type t) { + return new HashSet<>(); + } } diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java index b1580d75..3c27ea0d 100644 --- a/test/unify/UnifyTest.java +++ b/test/unify/UnifyTest.java @@ -27,13 +27,15 @@ public class UnifyTest extends Unify { // Vector <. Vector // Vector // 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.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.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT)); - eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), 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)); System.out.println(this.unify(eq, fc));