extended all cases / fixed random placeholder generation

This commit is contained in:
Florian Steurer 2016-04-09 15:07:41 +02:00
parent d080eb4a0a
commit 23e0be2572
3 changed files with 244 additions and 111 deletions

View File

@ -119,22 +119,26 @@ public class Unify {
}
IRuleSet rules = new RuleSet(fc);
Set<Set<UnifyPair>> changed = new HashSet<>();
Set<Set<UnifyPair>> restartSet = new HashSet<>();
Set<Set<UnifyPair>> eqPrimePrimeSet = new HashSet<>();
for(Set<UnifyPair> eqPrime : eqPrimeSetFlat) {
Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
if(eqPrime.equals(eq))
/*if (eqPrime.equals(eq))
eqPrimePrimeSet.add(eqPrime);
else if(eqPrimePrime.isPresent())
eqPrimePrimeSet.addAll(this.unify(eqPrimePrime.get(), fc));
else if(eqPrimePrime.isPresent()) {
Set<Set<UnifyPair>> subUnifyResult = unify(eqPrimePrime.get(), fc);
eqPrimePrimeSet.addAll(subUnifyResult);
}
else
eqPrimePrimeSet.addAll(this.unify(eqPrime, fc));
/*if(eqPrimePrime.isPresent())
changed.add(eqPrimePrime.get());
eqPrimePrimeSet.addAll(this.unify(eqPrime, fc));*/
if(eqPrimePrime.isPresent())
restartSet.add(eqPrimePrime.get());
else if(!isSolvedForm(eqPrime))
restartSet.add(eqPrime);
else
eqPrimePrimeSet.add(eqPrime);*/
eqPrimePrimeSet.add(eqPrime);
}
/*
@ -142,7 +146,7 @@ public class Unify {
* b) Build the union over everything
*/
for(Set<UnifyPair> eqss : changed)
for(Set<UnifyPair> eqss : restartSet)
eqPrimePrimeSet.addAll(this.unify(eqss, fc));
/*
@ -326,16 +330,36 @@ public class Unify {
IUnify unify = new MartelliMontanariUnify();
Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
cs.add(thetaPrime);
for(UnifyType c : cs) {
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
thetaQs.add(thetaPrime);
Set<UnifyType> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
thetaQPrimes.add(c);
else {
ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
/*
* TODO Optimierungsmöglichkeit:
*
* An dieser Stelle gibt es Raum für Optimierung.
* Z.B. resultiert (a <. C<Integer>) durch Permutation der Parameter mit grArg in:
* (a = C<b'>, b' <.? ? extends Number)
* (a = C<b'>, b' <.? ? extends Integer)
* (a = C<b'>, b' <.? Integer)
* usw...
*
* Der erste Fall ist am allgemeinsten und schließt alle anderen Fälle mit ein. Jeder Fall resultiert in einem
* rekursiven Aufruf des Unify. Es würde reichen nur den allgemeinsten Fall zu betrachten da dieser den Lösungraum
* der anderen Fälle miteinschließt.
*
* (Gibt es einen einzigen maximalen fall? Wsl. ? super x (x möglichst klein) und ? ext y (y möglichst groß))
*/
for(UnifyType param : cParams)
candidateParams.add(fc.grArg(param));
@ -354,18 +378,20 @@ public class Unify {
for (Entry<PlaceholderType, UnifyType> sigma : unifier.getSubstitutions())
substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
List<UnifyType> freshTphs = new ArrayList<>();
for (UnifyType tq : thetaQs) {
Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
for(UnifyType theta : smaller) {
Set<UnifyPair> resultPrime = new HashSet<>();
UnifyType[] freshTphs = new UnifyType[theta.getTypeParams().size()];
for(int i = 0; i < freshTphs.length; i++) {
freshTphs[i] = PlaceholderType.freshPlaceholder();
resultPrime.add(new UnifyPair(freshTphs[i], theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC));
//UnifyType[] freshTphs = new UnifyType[theta.getTypeParams().size()];
for(int i = 0; i < theta.getTypeParams().size(); i++) {
if(freshTphs.size()-1 < i)
freshTphs.add(PlaceholderType.freshPlaceholder());
resultPrime.add(new UnifyPair(freshTphs.get(i), theta.getTypeParams().get(i), PairOperator.SMALLERDOTWC));
}
UnifyType freshTheta = theta.setTypeParams(new TypeParams(freshTphs));
UnifyType freshTheta = theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0])));
resultPrime.add(new UnifyPair(a, freshTheta, PairOperator.EQUALSDOT));
resultPrime.addAll(substitutionSet);
result.add(resultPrime);
@ -380,53 +406,74 @@ public class Unify {
protected Set<Set<UnifyPair>> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
Set<Set<UnifyPair>> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
UnifyType aPrime = PlaceholderType.freshPlaceholder();
UnifyType extAPrime = new ExtendsType(aPrime);
UnifyType thetaPrime = extThetaPrime.getExtendedType();
Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
for(UnifyType c : cs) {
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
Set<UnifyType> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
thetaQPrimes.add(c);
else {
ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
for(UnifyType param : cParams)
candidateParams.add(fc.grArg(param));
//for(UnifyType theta : fc.smArg(subThetaPrime)) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, aPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT));
result.add(resultPrime);
for(TypeParams tp : permuteParams(candidateParams))
thetaQPrimes.add(c.setTypeParams(tp));
}
for(UnifyType tqp : thetaQPrimes) {
Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
if (!opt.isPresent())
continue;
Unifier unifier = opt.get();
Set<UnifyPair> substitutionSet = new HashSet<>();
for (Entry<PlaceholderType, UnifyType> sigma : unifier.getSubstitutions())
substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
for (UnifyType tq : thetaQs) {
ExtendsType extTq = new ExtendsType(tq);
Set<UnifyType> smArg = fc.smArg(unifier.apply(extTq));
for(UnifyType theta : smArg) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
resultPrime.addAll(substitutionSet);
result.add(resultPrime);
}
}
}
}
resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT));
result.add(resultPrime);
//}
return result;
// Set<Set<UnifyPair>> result = new HashSet<>();
// IUnify unify = new MartelliMontanariUnify();
//
// UnifyType thetaPrime = extThetaPrime.getExtendedType();
// Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
// cs.add(thetaPrime);
//
// for(UnifyType c : cs) {
// Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
// thetaQs.add(thetaPrime);
//
// Set<UnifyType> thetaQPrimes = new HashSet<>();
// TypeParams cParams = c.getTypeParams();
// if(cParams.size() == 0)
// thetaQPrimes.add(c);
// else {
// ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
// for(UnifyType param : cParams)
// candidateParams.add(fc.grArg(param));
//
// for(TypeParams tp : permuteParams(candidateParams))
// thetaQPrimes.add(c.setTypeParams(tp));
// }
//
// for(UnifyType tqp : thetaQPrimes) {
// Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
// if (!opt.isPresent())
// continue;
//
// Unifier unifier = opt.get();
//
// Set<UnifyPair> substitutionSet = new HashSet<>();
// for (Entry<PlaceholderType, UnifyType> sigma : unifier.getSubstitutions())
// substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
//
// for (UnifyType tq : thetaQs) {
// ExtendsType extTq = new ExtendsType(tq);
// Set<UnifyType> smArg = fc.smArg(unifier.apply(extTq));
// for(UnifyType theta : smArg) {
// Set<UnifyPair> resultPrime = new HashSet<>();
// resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
// resultPrime.addAll(substitutionSet);
// result.add(resultPrime);
// }
// }
//
// }
// }
//
// return result;
}
protected Set<Set<UnifyPair>> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
@ -494,62 +541,89 @@ public class Unify {
protected Set<Set<UnifyPair>> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
Set<Set<UnifyPair>> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
UnifyType aPrime = PlaceholderType.freshPlaceholder();
UnifyType supAPrime = new SuperType(aPrime);
UnifyType theta = supTheta.getSuperedType();
Set<UnifyType> cs = fc.getAllTypesByName(theta.getName());
for(UnifyType c : cs) {
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
Set<UnifyType> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
thetaQPrimes.add(c);
else {
ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
for(UnifyType param : cParams)
candidateParams.add(fc.grArg(param));
for(TypeParams tp : permuteParams(candidateParams))
thetaQPrimes.add(c.setTypeParams(tp));
}
for(UnifyType tqp : thetaQPrimes) {
Optional<Unifier> opt = unify.unify(tqp, theta);
if (!opt.isPresent())
continue;
Unifier unifier = opt.get();
Set<UnifyPair> substitutionSet = new HashSet<>();
for (Entry<PlaceholderType, UnifyType> sigma : unifier.getSubstitutions())
substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
for (UnifyType tq : thetaQs) {
Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
for(UnifyType thetaPrime : smaller) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, new SuperType(thetaPrime), PairOperator.EQUALSDOT));
resultPrime.addAll(substitutionSet);
result.add(resultPrime);
}
}
}
}
//for(UnifyType theta : fc.smArg(subThetaPrime)) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(aPrime, theta, PairOperator.SMALLERDOT));
result.add(resultPrime);
//}
return result;
// Set<Set<UnifyPair>> result = new HashSet<>();
// IUnify unify = new MartelliMontanariUnify();
//
// UnifyType theta = supTheta.getSuperedType();
// Set<UnifyType> cs = fc.getAllTypesByName(theta.getName());
// cs.add(theta);
//
// for(UnifyType c : cs) {
// Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
// thetaQs.add(theta);
//
// Set<UnifyType> thetaQPrimes = new HashSet<>();
// TypeParams cParams = c.getTypeParams();
// if(cParams.size() == 0)
// thetaQPrimes.add(c);
// else {
// ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
// for(UnifyType param : cParams)
// candidateParams.add(fc.grArg(param));
//
// for(TypeParams tp : permuteParams(candidateParams))
// thetaQPrimes.add(c.setTypeParams(tp));
// }
//
// for(UnifyType tqp : thetaQPrimes) {
// Optional<Unifier> opt = unify.unify(tqp, theta);
// if (!opt.isPresent())
// continue;
//
// Unifier unifier = opt.get();
//
// Set<UnifyPair> substitutionSet = new HashSet<>();
// for (Entry<PlaceholderType, UnifyType> sigma : unifier.getSubstitutions())
// substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
//
// for (UnifyType tq : thetaQs) {
// Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
//
// for(UnifyType thetaPrime : smaller) {
// Set<UnifyPair> resultPrime = new HashSet<>();
// resultPrime.add(new UnifyPair(a, new SuperType(thetaPrime), PairOperator.EQUALSDOT));
// resultPrime.addAll(substitutionSet);
// result.add(resultPrime);
// }
// }
//
// }
// }
//
// return result;
}
protected Set<Set<UnifyPair>> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
Set<Set<UnifyPair>> result = new HashSet<>();
for(UnifyType thetaS : fc.grArg(theta)) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT));
result.add(resultPrime);
}
//for(UnifyType thetaS : fc.grArg(theta)) {
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
result.add(resultPrime);
UnifyType freshTph = PlaceholderType.freshPlaceholder();
resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT));
result.add(resultPrime);
resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT));
result.add(resultPrime);
//}
return result;
}

View File

@ -31,7 +31,7 @@ public final class PlaceholderType extends UnifyType{
String name = nextName + randomChar();
while(EXISTING_PLACEHOLDERS.contains(name));
nextName += randomChar();
name += randomChar();
return new PlaceholderType(name, true);
}

View File

@ -157,6 +157,7 @@ public class UnifyTest extends Unify {
addAsSet(expected, new UnifyPair(tphA, supNumber, PairOperator.EQUALSDOT));
actual = unify(eq, fc);
actual = filterGeneratedTPHsMultiple(actual);
Assert.assertEquals(expected, actual);
@ -199,6 +200,7 @@ public class UnifyTest extends Unify {
addAsSet(expected, new UnifyPair(tphA, number, PairOperator.EQUALSDOT));
actual = unify(eq, fc);
actual = filterGeneratedTPHsMultiple(actual);
Assert.assertEquals(expected, actual);
@ -309,7 +311,7 @@ public class UnifyTest extends Unify {
Set<Set<UnifyPair>> expected = new HashSet<>();
Set<Set<UnifyPair>> actual = unify(eq, fc);
System.out.println(actual);
//System.out.println(actual);
//Assert.assertEquals(actual, expected);
@ -343,8 +345,8 @@ public class UnifyTest extends Unify {
expected = new HashSet<>();
actual = unify(eq, fc);
//System.out.println(actual);
System.out.println(actual);
//Assert.assertEquals(actual, expected);
/*
@ -384,8 +386,10 @@ public class UnifyTest extends Unify {
UnifyType object = tf.getSimpleType("Object");
UnifyType integer = tf.getSimpleType("Integer");
UnifyType doubl = tf.getSimpleType("Double");
UnifyType mygeneric = tf.getSimpleType("MyGeneric", "T");
//fcb.add(number, object);
fcb.add(mygeneric, object);
fcb.add(integer, number);
//fcb.add(doubl, number);
@ -433,9 +437,21 @@ public class UnifyTest extends Unify {
*
* This is a test for th extension of case 2 of the cartesian product of step 4.
*
* TODO
* (a <.? ? ext b)
* (b =. Number)
*/
eq = new HashSet<>();
eq.add(new UnifyPair(tphA, extB, PairOperator.SMALLERDOTWC));
eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT));
expected = new HashSet<>();
actual = unify(eq, fc);
System.out.println("Case 2");
System.out.println(actual);
/*
* Test 3:
* This is a test for the extension of case 3 of the cartesian product of step 4.
@ -453,6 +469,8 @@ public class UnifyTest extends Unify {
actual = unify(eq, fc);
System.out.println("Case 3");
System.out.println(actual);
//Assert.assertEquals(expected, actual);
@ -498,6 +516,47 @@ public class UnifyTest extends Unify {
System.out.println(actual);
//Assert.assertEquals(expected, actual);
/*
* Test 7:
* This is a test for the extension of case 7 of the cartesian product of step 4.
*
* ? sup b <.? a
* b =. Number
*/
eq = new HashSet<>();
eq.add(new UnifyPair(supB, tphA, PairOperator.SMALLERDOTWC));
eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT));
expected = new HashSet<>();
actual = unify(eq, fc);
System.out.println("Case 7");
System.out.println(actual);
//Assert.assertEquals(expected, actual);
/*
* Test 8:
* This is a test for the extension of case 8 of the cartesian product of step 4.
*
* MyGeneric<? extends b> <.? a
* b =. Integer
*/
eq = new HashSet<>();
eq.add(new UnifyPair(tf.getSimpleType("MyGeneric", extB), tphA, PairOperator.SMALLERDOTWC));
eq.add(new UnifyPair(tphB, number, PairOperator.EQUALSDOT));
expected = new HashSet<>();
actual = unify(eq, fc);
System.out.println("Case 8:");
System.out.println(actual);
//Assert.assertEquals(expected, actual);
}
@Test