cleaned up

This commit is contained in:
Florian Steurer 2016-04-19 11:42:15 +02:00
parent afc6bc7b89
commit 904ca01207

View File

@ -153,20 +153,10 @@ public class TypeUnify {
if (eqPrime.equals(eq))
eqPrimePrimeSet.add(eqPrime);
else if(eqPrimePrime.isPresent()) {
else if(eqPrimePrime.isPresent())
restartSet.add(eqPrimePrime.get());
/*Set<Set<UnifyPair>> subUnifyResult = unify(eqPrimePrime.get(), fc);
eqPrimePrimeSet.addAll(subUnifyResult);*/
}
else
restartSet.add(eqPrime);
//eqPrimePrimeSet.addAll(this.unify(eqPrime, fc));
/*if(eqPrimePrime.isPresent())
restartSet.add(eqPrimePrime.get());
else if(!isSolvedForm(eqPrime))
restartSet.add(eqPrime);
else
eqPrimePrimeSet.add(eqPrime);*/
}
/*
@ -176,7 +166,8 @@ public class TypeUnify {
// TODO parallelisierung möglich (lohnt sich vermutlich)
for(Set<UnifyPair> eqss : restartSet)
eqPrimePrimeSet.addAll(this.unify(eqss, fc));
/*restartSet.parallelStream().forEach(
x -> eqPrimePrimeSet.addAll(unify(x, fc)));*/
/*
* Step 7: Filter empty sets;
*/
@ -400,9 +391,8 @@ public class TypeUnify {
cs.add(thetaPrime);
for(UnifyType c : cs) {
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
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)
@ -410,25 +400,6 @@ public class TypeUnify {
else {
ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
/*
* TODO Optimierungsmöglichkeit:
*
* An dieser Stelle gibt es Raum für Optimierung.
* Z.B. resultiert (a <. C<? extends Integer>) durch Permutation der Parameter mit grArg und smaller in:
* (a = C<b'>, b' <.? ? extends Integer)
* (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.
*
* Prüfen:
* Gibt es einen einzigen maximalen Fall?
* Wahrscheinlich gibt es 2: ? super x (x möglichst klein) und ? ext y (y möglichst groß))
*/
for(UnifyType param : cParams)
candidateParams.add(fc.grArg(param));
@ -453,7 +424,6 @@ public class TypeUnify {
for(UnifyType theta : smaller) {
Set<UnifyPair> resultPrime = new HashSet<>();
//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());
@ -482,70 +452,15 @@ public class TypeUnify {
UnifyType aPrime = PlaceholderType.freshPlaceholder();
UnifyType extAPrime = new ExtendsType(aPrime);
UnifyType thetaPrime = extThetaPrime.getExtendedType();
//for(UnifyType theta : fc.smArg(subThetaPrime)) {
Set<UnifyPair> resultPrime = new HashSet<>();
//resultPrime.add(new UnifyPair(a, aPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT));
result.add(resultPrime);
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, thetaPrime, PairOperator.SMALLERDOT));
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);
//}
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;
}
/**
@ -557,17 +472,14 @@ public class TypeUnify {
UnifyType aPrime = PlaceholderType.freshPlaceholder();
UnifyType supAPrime = new SuperType(aPrime);
UnifyType thetaPrime = subThetaPrime.getSuperedType();
//for(UnifyType theta : fc.smArg(subThetaPrime)) {
Set<UnifyPair> resultPrime = new HashSet<>();
//resultPrime.add(new UnifyPair(a, aPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT));
result.add(resultPrime);
Set<UnifyPair> resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT));
result.add(resultPrime);
resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT));
result.add(resultPrime);
//}
resultPrime = new HashSet<>();
resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT));
result.add(resultPrime);
return result;
}
@ -610,7 +522,6 @@ public class TypeUnify {
*/
protected Set<Set<UnifyPair>> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
Set<Set<UnifyPair>> result = new HashSet<>();
//for(UnifyType thetaS : fc.smaller(extTheta.getExtendedType())) {
UnifyType freshTph = PlaceholderType.freshPlaceholder();
UnifyType extFreshTph = new ExtendsType(freshTph);
@ -618,7 +529,6 @@ public class TypeUnify {
resultPrime.add(new UnifyPair(a, extFreshTph, PairOperator.EQUALSDOT));
resultPrime.add(new UnifyPair(extTheta.getExtendedType(), freshTph, PairOperator.SMALLERDOT));
result.add(resultPrime);
//}
return result;
}
@ -632,65 +542,12 @@ public class TypeUnify {
UnifyType aPrime = PlaceholderType.freshPlaceholder();
UnifyType supAPrime = new SuperType(aPrime);
UnifyType theta = supTheta.getSuperedType();
//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);
//}
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;
}
/**