implemented step 4 (some cases still missing)

This commit is contained in:
Florian Steurer 2015-11-23 00:12:08 +01:00
parent e2ba4490b1
commit 4576efe3ec
2 changed files with 100 additions and 37 deletions

View File

@ -16,30 +16,26 @@ 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.typinference.unify.model.ExtendsType;
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.SuperType;
import de.dhbwstuttgart.typinference.unify.model.Type;
/**
* Implementierung des Unifikationsalgorithmus.
* Implementation of the type unification algorithm
* @author Florian Steurer
*/
public class Unify {
public Menge<Menge<Pair>> unify(Menge<Pair> eq, IFiniteClosure fc) {
/*
* Preparations: Create Mapping
*/
Set<MPair> eq0 = null;
public Menge<Menge<Pair>> unify(Menge<MPair> eq, IFiniteClosure fc) {
/*
* Step 1: Repeated application of reduce, adapt, erase, swap
*/
eq0 = applyTypeUnificationRules(eq0, fc);
Set<MPair> eq0 = applyTypeUnificationRules(eq, fc);
/*
@ -51,35 +47,34 @@ public class Unify {
splitEq(eq0, eq1s, eq2s);
/*
* Step 4: Magic
* Step 4: Create possible typings
*/
// Sets that originate from pair pattern matching
// Sets of the "second level"
Set<List<Set<MPair>>> pairSets = new HashSet<List<Set<MPair>>>();
for(MPair pair : eq2s)
pairSets.add(calculateSets(pair));
List<List<Set<MPair>>> pairSets = calculatePairSets(eq2s, fc);
// The sets of the "first level"
Set<Set<MPair>> sets = new HashSet<Set<MPair>>();
// Add Eq1'
sets.add(eq1s);
sets.add(eq1s); // Add Eq1'
// Add the set of [a =. Theta | (a=. Theta) in Eq2']
sets.add(eq2s.stream()
.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
.collect(Collectors.toSet()));
/*
* Around here, filters for pairs and sets can be applied
*/
/* Up to here, no cartesian products are calculated.
* Around here, filters for pairs and sets can be applied */
ISetOperations setOps = new GuavaSetOperations();
for(List<Set<MPair>> pairSet : pairSets)
setOps.cartesianProduct(pairSet).forEach(x -> sets.add(new HashSet<MPair>(x)));
// Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte
// Calculate the inner cartesian products
// Cartesian products of the second level
for(List<Set<MPair>> pairSet : pairSets) // Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte
setOps.cartesianProduct(pairSet).forEach(x -> sets.add(new HashSet<MPair>(x)));
// Calculate the outer cartesian products
// Cartesian products of the first level
Set<List<MPair>> eqsSet = setOps.cartesianProduct(new ArrayList<>(sets));
/*
@ -99,18 +94,6 @@ public class Unify {
throw new NotImplementedException();
}
protected List<Set<MPair>> calculateSets(MPair pair) {
return null;
}
protected void splitEq(Set<MPair> eq, Set<MPair> eq1s, Set<MPair> eq2s) {
for(MPair pair : eq)
if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType)
eq1s.add(pair);
else
eq2s.add(pair);
}
protected Set<MPair> applyTypeUnificationRules(Set<MPair> eq, IFiniteClosure fc) {
/*
@ -183,4 +166,84 @@ public class Unify {
collection.add(pair2);
}
protected void splitEq(Set<MPair> eq, Set<MPair> eq1s, Set<MPair> eq2s) {
for(MPair pair : eq)
if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType)
eq1s.add(pair);
else
eq2s.add(pair);
}
protected List<List<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
List<List<Set<MPair>>> result = new ArrayList<List<Set<MPair>>>();
for(int i = 0; i < 8; i++)
result.add(new ArrayList<Set<MPair>>());
for(MPair pair : eq2s) {
PairOperator pairOp = pair.getPairOp();
Type lhsType = pair.getLhsType();
Type rhsType = pair.getRhsType();
// Case 1: (a <. Theta')
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
// TODO
}
// Case 2: (a <.? ? ext Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){
// TODO
}
// Case 3: (a <.? ? sup Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType) {
Set<MPair> set = new HashSet<>();
for(Type theta : fc.smArg(rhsType))
set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT));
result.get(2).add(set);
}
// Case 4: (a <.? Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
set.add(new MPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT));
result.get(3).add(set);
}
// Case 5: (Theta <. a)
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.greater(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.get(4).add(set);
}
// Case 6: (? ext Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.grArg(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.get(5).add(set);
}
// Case 7: (? sup Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) {
// TODO
}
// Case 8: (Theta <.? a)
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType) {
Set<MPair> set = new HashSet<>();
for(Type thetaS : fc.grArg(lhsType))
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
result.get(7).add(set);
}
}
return result.stream().filter(x -> !x.isEmpty()).collect(Collectors.toList());
}
}