cartesische produkte überarbeitet

This commit is contained in:
Florian Steurer 2016-03-20 18:05:34 +01:00
parent 299f8f56ca
commit 21c6aef7fd
2 changed files with 65 additions and 52 deletions

View File

@ -57,33 +57,48 @@ public class Unify {
* mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
*/ */
// All Sets // There are up to 10 toplevel set. 8 of 10 are the result of the
List<Set<MPair>> sets = new ArrayList<Set<MPair>>(); // cartesian product of the sets created by pattern matching.
List<Set<Set<MPair>>> topLevelSets = new ArrayList<>();
if(eq1s.size() != 0) if(eq1s.size() != 0) {
sets.add(eq1s); // Add Eq1' Set<Set<MPair>> wrap = new HashSet<>();
wrap.add(eq1s);
topLevelSets.add(wrap); // Add Eq1'
}
// Add the set of [a =. Theta | (a=. Theta) in Eq2'] // Add the set of [a =. Theta | (a=. Theta) in Eq2']
Set<MPair> bufferSet = eq2s.stream() Set<MPair> bufferSet = eq2s.stream()
.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType) .filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
.collect(Collectors.toSet()); .collect(Collectors.toSet());
if(bufferSet.size() != 0) if(bufferSet.size() != 0) {
sets.add(bufferSet); Set<Set<MPair>> wrap = new HashSet<>();
wrap.add(bufferSet);
topLevelSets.add(wrap);
}
// Sets that originate from pair pattern matching // Sets that originate from pair pattern matching
// Sets of the "second level" // Sets of the "second level"
Set<Set<Set<MPair>>> secondLevelSets = calculatePairSets(eq2s, fc);
sets.addAll(calculatePairSets(eq2s, fc));
/* Up to here, no cartesian products are calculated. /* Up to here, no cartesian products are calculated.
* Around here, filters for pairs and sets can be applied */ * filters for pairs and sets can be applied here */
ISetOperations setOps = new GuavaSetOperations(); ISetOperations setOps = new GuavaSetOperations();
// Calculate the cartesian products // Sub cartesian products of the second level (pattern matched) sets
Set<Set<MPair>> result = setOps.cartesianProduct(sets).stream() for(Set<Set<MPair>> secondLevelSet : secondLevelSets) {
.map(x -> new HashSet<MPair>(x)).collect(Collectors.toCollection(HashSet::new)); List<Set<MPair>> secondLevelSetList = new ArrayList<>(secondLevelSet);
topLevelSets.add(setOps.cartesianProduct(secondLevelSetList)
.stream().map(x -> new HashSet<>(x))
.collect(Collectors.toCollection(HashSet::new)));
}
// Cartesian product over all (up to 10) top level sets
Set<Set<Set<MPair>>> eqPrimeSet = setOps.cartesianProduct(topLevelSets)
.stream().map(x -> new HashSet<>(x))
.collect(Collectors.toCollection(HashSet::new));
//System.out.println(result); //System.out.println(result);
/* /*
@ -91,38 +106,41 @@ public class Unify {
*/ */
/* /*
* TODO * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht)
* 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?
*/ */
Set<Set<MPair>> eqPrimeSetFlat = new HashSet<>();
for(Set<Set<MPair>> setToFlatten : eqPrimeSet) {
Set<MPair> buffer = new HashSet<>();
setToFlatten.stream().forEach(x -> buffer.addAll(x));
eqPrimeSetFlat.add(buffer);
}
IRuleSet rules = new RuleSet(fc); IRuleSet rules = new RuleSet(fc);
Set<Set<MPair>> changed = new HashSet<>(); Set<Set<MPair>> changed = new HashSet<>();
Set<Set<MPair>> unchanged = new HashSet<>(); Set<Set<MPair>> eqPrimePrimeSet = new HashSet<>();
for(Set<MPair> eqss : result) { for(Set<MPair> eqPrime : eqPrimeSetFlat) {
Optional<Set<MPair>> newEqss = rules.subst(eqss); Optional<Set<MPair>> eqPrimePrime = rules.subst(eqPrime);
if(newEqss.isPresent())
changed.add(newEqss.get()); if(eqPrimePrime.isPresent())
else changed.add(eqPrimePrime.get());
unchanged.add(eqss); else
eqPrimePrimeSet.add(eqPrime);
} }
/* /*
* Step 6 a) Restart for pairs where subst was applied * Step 6 a) Restart for pairs where subst was applied
* b) Build the union over everything * b) Build the union over everything
*/ */
for(Set<MPair> eqss : changed) for(Set<MPair> eqss : changed) {
unchanged.addAll(this.unify(eqss, fc)); eqPrimePrimeSet.addAll(this.unify(eqss, fc));
}
/* /*
* Step 7: Filter result for solved pairs TODO wie? * Step 7: Filter result for solved pairs
*/ */
return eqPrimePrimeSet;
return unchanged;
} }
@ -217,8 +235,12 @@ public class Unify {
} }
protected List<Set<MPair>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) { protected Set<Set<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
List<Set<MPair>> result = new ArrayList<Set<MPair>>(); List<Set<Set<MPair>>> result = new ArrayList<>();
// Init all 8 cases
for(int i = 0; i < 8; i++)
result.add(new HashSet<>());
for(MPair pair : eq2s) { for(MPair pair : eq2s) {
@ -228,38 +250,38 @@ public class Unify {
// Case 1: (a <. Theta') // Case 1: (a <. Theta')
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
result.add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc)); result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
// Case 2: (a <.? ? ext Theta') // Case 2: (a <.? ? ext Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
result.add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc)); result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
// Case 3: (a <.? ? sup Theta') // Case 3: (a <.? ? sup Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
result.add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc)); result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
// Case 4: (a <.? Theta') // Case 4: (a <.? Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
result.add(unifyCase4((PlaceholderType) lhsType, rhsType, fc)); result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc));
// Case 5: (Theta <. a) // Case 5: (Theta <. a)
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
result.add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc)); result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
// Case 6: (? ext Theta <.? a) // Case 6: (? ext Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
result.add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc)); result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));
// Case 7: (? sup Theta <.? a) // Case 7: (? sup Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
result.add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc)); result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc));
// Case 8: (Theta <.? a) // Case 8: (Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc)); result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
} }
return result; return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
} }
protected Set<MPair> unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) { protected Set<MPair> unifyCase1(PlaceholderType a, Type thetaPrime, IFiniteClosure fc) {
@ -456,13 +478,4 @@ public class Unify {
permuteParams(candidates, idx+1, result, current); permuteParams(candidates, idx+1, result, current);
} }
} }
private Set<Type> getAllInstantiations(Type t, IFiniteClosure fc) {
Set<Type> result = new HashSet<>();
result.add(t);
return result;
// TODO
}
} }

View File

@ -36,10 +36,10 @@ public class UnifyTest extends Unify {
// Number <. A // Number <. A
// Double <. B // Double <. B
// B <. Object // 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", "A"), 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("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.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT));
eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "A"), PairOperator.SMALLERDOT)); //eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", "A"), 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.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));