forked from JavaTX/JavaCompilerCore
Start with unify refactoring
This commit is contained in:
JanUlrich
commit
9a0de3f193
998
src/main/java/de/dhbwstuttgart/unify2/RuleSet.java
Normal file
998
src/main/java/de/dhbwstuttgart/unify2/RuleSet.java
Normal file
@ -0,0 +1,998 @@
|
||||
package de.dhbwstuttgart.unify2;
|
||||
|
||||
import de.dhbwstuttgart.exceptions.DebugException;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.unify.distributeVariance;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.*;
|
||||
import org.antlr.v4.tool.Rule;
|
||||
import org.apache.commons.io.output.NullOutputStream;
|
||||
|
||||
import java.io.IOException;
|
||||
import java.io.OutputStreamWriter;
|
||||
import java.io.Writer;
|
||||
import java.util.*;
|
||||
import java.util.function.Function;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
/**
|
||||
* Implementation of the type inference rules.
|
||||
* @author Florian Steurer
|
||||
*
|
||||
*/
|
||||
public class RuleSet {
|
||||
|
||||
/**
|
||||
* Repeatedly applies type unification rules to a set of equations.
|
||||
* This is step one of the unification algorithm.
|
||||
* @return The set of pairs that results from repeated application of the inference rules.
|
||||
*/
|
||||
protected Set<UnifyPair> applyTypeUnificationRules(Set<UnifyPair> eq, IFiniteClosure fc) {
|
||||
|
||||
/*
|
||||
* Rule Application Strategy:
|
||||
*
|
||||
* 1. Swap all pairs and erase all erasable pairs
|
||||
* 2. Apply all possible rules to a single pair, then move it to the result set.
|
||||
* Iterating over pairs first, then iterating over rules prevents the application
|
||||
* of rules to a "finished" pair over and over.
|
||||
* 2.1 Apply all rules repeatedly except for erase rules. If
|
||||
* the application of a rule creates new pairs, check immediately
|
||||
* against the erase rules.
|
||||
*/
|
||||
|
||||
|
||||
LinkedHashSet<UnifyPair> targetSet = new LinkedHashSet<UnifyPair>();
|
||||
LinkedList<UnifyPair> eqQueue = new LinkedList<>();
|
||||
|
||||
/*
|
||||
* Swap all pairs and erase all erasable pairs
|
||||
*/
|
||||
eq.forEach(x -> swapAddOrErase(x, fc, eqQueue));
|
||||
|
||||
/*
|
||||
* Apply rules until the queue is empty
|
||||
*/
|
||||
while(!eqQueue.isEmpty()) {
|
||||
UnifyPair pair = eqQueue.pollFirst();
|
||||
|
||||
// ReduceUp, ReduceLow, ReduceUpLow
|
||||
Optional<UnifyPair> opt = RuleSet.reduceUpLow(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceLow(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceUp(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceWildcardLow(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceWildcardLowRight(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceWildcardUp(pair);
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceWildcardUpRight(pair);
|
||||
//PL 2018-03-06 auskommentiert muesste falsch sein vgl. JAVA_BSP/Wildcard6.java
|
||||
//opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair);
|
||||
//opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair);
|
||||
//opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair);
|
||||
|
||||
// Reduce TPH
|
||||
opt = opt.isPresent() ? opt : RuleSet.reduceTph(pair);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(opt.isPresent()) {
|
||||
swapAddOrErase(opt.get(), fc, eqQueue);
|
||||
continue;
|
||||
}
|
||||
|
||||
// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
|
||||
//try {
|
||||
// logFile.write("PAIR1 " + pair + "\n");
|
||||
// logFile.flush();
|
||||
//}
|
||||
//catch (IOException e) { }
|
||||
|
||||
Optional<Set<UnifyPair>> optSet = RuleSet.reduce1(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduce2(pair);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceExt(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceSup(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceEq(pair);
|
||||
|
||||
// ReduceTphExt, ReduceTphSup
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceTphExt(pair);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceTphSup(pair);
|
||||
|
||||
|
||||
// FunN Rules
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.reduceFunN(pair);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.greaterFunN(pair);
|
||||
optSet = optSet.isPresent() ? optSet : RuleSet.smallerFunN(pair);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(optSet.isPresent()) {
|
||||
optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue));
|
||||
continue;
|
||||
}
|
||||
|
||||
// Adapt, AdaptExt, AdaptSup
|
||||
//try {
|
||||
// logFile.write("PAIR2 " + pair + "\n");
|
||||
// logFile.flush();
|
||||
//}
|
||||
//catch (IOException e) { }
|
||||
opt = RuleSet.adapt(pair, fc);
|
||||
opt = opt.isPresent() ? opt : RuleSet.adaptExt(pair, fc);
|
||||
opt = opt.isPresent() ? opt : RuleSet.adaptSup(pair, fc);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(opt.isPresent()) {
|
||||
swapAddOrErase(opt.get(), fc, eqQueue);
|
||||
continue;
|
||||
}
|
||||
|
||||
// None of the rules has been applied
|
||||
targetSet.add(pair);
|
||||
}
|
||||
|
||||
return targetSet;
|
||||
}
|
||||
|
||||
/**
|
||||
* Applies the rule swap to a pair if possible. Then adds the pair to the set if no erase rule applies.
|
||||
* If an erase rule applies, the pair is not added (erased).
|
||||
* @param pair The pair to swap and add or erase.
|
||||
* @param collection The collection to which the pairs are added.
|
||||
*/
|
||||
static void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection<UnifyPair> collection) {
|
||||
Optional<UnifyPair> opt = RuleSet.swap(pair);
|
||||
UnifyPair pair2 = opt.isPresent() ? opt.get() : pair;
|
||||
|
||||
if(RuleSet.erase1(pair2, fc) || RuleSet.erase3(pair2) || RuleSet.erase2(pair2, fc))
|
||||
return;
|
||||
|
||||
collection.add(pair2);
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceUp(UnifyPair pair) {
|
||||
// Check if reduce up is applicable
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(rhsType instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
// Rule is applicable, unpack the SuperType
|
||||
return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceLow(UnifyPair pair) {
|
||||
// Check if rule is applicable
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
if(!(lhsType instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
// Rule is applicable, unpack the ExtendsType
|
||||
return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceUpLow(UnifyPair pair) {
|
||||
// Check if rule is applicable
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
if(!(lhsType instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(rhsType instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
// Rule is applicable, unpack both sides
|
||||
return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceExt(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType x = pair.getLhsType();
|
||||
UnifyType sTypeX;
|
||||
|
||||
if(x instanceof ReferenceType)
|
||||
sTypeX = x;
|
||||
else if(x instanceof ExtendsType)
|
||||
sTypeX = ((ExtendsType) x).getExtendedType();
|
||||
else
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType extY = pair.getRhsType();
|
||||
|
||||
if(!(extY instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
|
||||
|
||||
if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
|
||||
return Optional.empty();
|
||||
|
||||
if(x instanceof ExtendsType)
|
||||
xFromFc = new ExtendsType(xFromFc);
|
||||
|
||||
UnifyType extYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
|
||||
|
||||
if(extYFromFc == null || extYFromFc.getTypeParams() != xFromFc.getTypeParams())
|
||||
return Optional.empty();
|
||||
|
||||
TypeParams extYParams = extY.getTypeParams();
|
||||
TypeParams xParams = x.getTypeParams();
|
||||
|
||||
int[] pi = pi(xParams, extYParams);
|
||||
|
||||
if(pi.length == 0)
|
||||
return Optional.empty();
|
||||
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
for(int rhsIdx = 0; rhsIdx < extYParams.size(); rhsIdx++)
|
||||
result.add(new UnifyPair(xParams.get(pi[rhsIdx]), extYParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceSup(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType x = pair.getLhsType();
|
||||
UnifyType sTypeX;
|
||||
|
||||
if(x instanceof ReferenceType)
|
||||
sTypeX = x;
|
||||
else if(x instanceof SuperType)
|
||||
sTypeX = ((SuperType) x).getSuperedType();
|
||||
else
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType supY = pair.getRhsType();
|
||||
|
||||
if(!(supY instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
|
||||
|
||||
if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
|
||||
return Optional.empty();
|
||||
|
||||
if(x instanceof SuperType)
|
||||
xFromFc = new SuperType(xFromFc);
|
||||
|
||||
UnifyType supYFromFc = fc.grArg(xFromFc, new HashSet<>()).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
|
||||
|
||||
if(supYFromFc == null || supYFromFc.getTypeParams() != xFromFc.getTypeParams())
|
||||
return Optional.empty();
|
||||
|
||||
TypeParams supYParams = supY.getTypeParams();
|
||||
TypeParams xParams = x.getTypeParams();
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
int[] pi = pi(xParams, supYParams);
|
||||
|
||||
if(pi.length == 0)
|
||||
return Optional.empty();
|
||||
|
||||
for(int rhsIdx = 0; rhsIdx < supYParams.size(); rhsIdx++)
|
||||
result.add(new UnifyPair(supYParams.get(rhsIdx), xParams.get(pi[rhsIdx]), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceEq(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
if(lhsType instanceof PlaceholderType || lhsType.getTypeParams().empty())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
if(!rhsType.getName().equals(lhsType.getName()))
|
||||
return Optional.empty();
|
||||
|
||||
if(rhsType instanceof PlaceholderType || lhsType instanceof PlaceholderType || rhsType.getTypeParams().empty())
|
||||
return Optional.empty();
|
||||
|
||||
if(rhsType.getTypeParams().size() != lhsType.getTypeParams().size())
|
||||
return Optional.empty();
|
||||
|
||||
// Keine Permutation wie im Paper nötig
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
TypeParams lhsTypeParams = lhsType.getTypeParams();
|
||||
TypeParams rhsTypeParams = rhsType.getTypeParams();
|
||||
|
||||
for(int i = 0; i < lhsTypeParams.size(); i++)
|
||||
result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduce1(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType c = pair.getLhsType();
|
||||
if(!(c instanceof ReferenceType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType d = pair.getRhsType();
|
||||
if(!(d instanceof ReferenceType))
|
||||
return Optional.empty();
|
||||
|
||||
ReferenceType lhsSType = (ReferenceType) c;
|
||||
ReferenceType rhsSType = (ReferenceType) d;
|
||||
|
||||
//try {
|
||||
// logFile.write("PAIR Rules: " + pair + "\n");
|
||||
// logFile.flush();
|
||||
//}
|
||||
//catch (IOException e) { }
|
||||
|
||||
if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null);
|
||||
//2018-02-23: liefert Vector<Vector<Integer>>: Das kann nicht sein.
|
||||
|
||||
//NOCHMAL UEBERPRUEFEN
|
||||
//PL 18-02-09 Eingfuegt Anfang
|
||||
//C und D koennen auch gleich sein.
|
||||
if (c.getName().equals(d.getName())) {
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
TypeParams rhsTypeParams = d.getTypeParams();
|
||||
TypeParams lhsTypeParams = c.getTypeParams();
|
||||
for(int rhsIdx = 0; rhsIdx < c.getTypeParams().size(); rhsIdx++)
|
||||
result.add(new UnifyPair(lhsTypeParams.get(rhsIdx), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
//PL 18-02-09 Eingfuegt ENDE
|
||||
|
||||
//try {
|
||||
// logFile.write("cFromFc: " + cFromFc);
|
||||
// logFile.flush();
|
||||
//}
|
||||
//catch (IOException e) { }
|
||||
|
||||
if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null);
|
||||
|
||||
//try {
|
||||
// logFile.write("cFromFc: " + cFromFc);
|
||||
// logFile.flush();
|
||||
//}
|
||||
//catch (IOException e) { }
|
||||
|
||||
if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size())
|
||||
return Optional.empty();
|
||||
//System.out.println("cFromFc: " + cFromFc);
|
||||
//System.out.println("dFromFc: " + dFromFc);
|
||||
int[] pi = pi(cFromFc.getTypeParams(), dFromFc.getTypeParams());
|
||||
|
||||
if(pi.length == 0)
|
||||
return Optional.empty();
|
||||
|
||||
TypeParams rhsTypeParams = d.getTypeParams();
|
||||
TypeParams lhsTypeParams = c.getTypeParams();
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
for(int rhsIdx = 0; rhsIdx < rhsTypeParams.size(); rhsIdx++)
|
||||
result.add(new UnifyPair(lhsTypeParams.get(pi[rhsIdx]), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduce2(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.EQUALSDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
ReferenceType lhsSType;
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
ReferenceType rhsSType;
|
||||
|
||||
if ((lhsType instanceof ReferenceType) && (rhsType instanceof ReferenceType)) {
|
||||
lhsSType = (ReferenceType) lhsType;
|
||||
rhsSType = (ReferenceType) rhsType;
|
||||
}
|
||||
else if (((lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType))
|
||||
|| ((lhsType instanceof SuperType) && (rhsType instanceof SuperType))) {
|
||||
UnifyType lhsSTypeRaw = ((WildcardType) lhsType).getWildcardedType();
|
||||
UnifyType rhsSTypeRaw = ((WildcardType) rhsType).getWildcardedType();
|
||||
if ((lhsSTypeRaw instanceof ReferenceType) && (rhsSTypeRaw instanceof ReferenceType)) {
|
||||
lhsSType = (ReferenceType) lhsSTypeRaw;
|
||||
rhsSType = (ReferenceType) rhsSTypeRaw;
|
||||
}
|
||||
else
|
||||
return Optional.empty();
|
||||
}
|
||||
else
|
||||
return Optional.empty();
|
||||
|
||||
if(lhsSType.getTypeParams().empty())
|
||||
return Optional.empty();
|
||||
|
||||
if(!rhsSType.getName().equals(lhsSType.getName()))
|
||||
return Optional.empty();
|
||||
|
||||
if(!(lhsSType.getTypeParams().size()==rhsSType.getTypeParams().size()))throw new DebugException("Fehler in Unifizierung"+ " " + lhsSType.toString() + " " + rhsSType.toString());
|
||||
//if(rhsSType.getTypeParams().size() != lhsSType.getTypeParams().size())
|
||||
// return Optional.empty();
|
||||
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
|
||||
TypeParams rhsTypeParams = rhsSType.getTypeParams();
|
||||
TypeParams lhsTypeParams = lhsSType.getTypeParams();
|
||||
for(int i = 0; i < rhsTypeParams.size(); i++)
|
||||
result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static boolean erase1(UnifyPair pair, IFiniteClosure fc) {
|
||||
if((pair.getPairOp() != PairOperator.SMALLERDOT) && (pair.getPairOp() != PairOperator.SMALLERNEQDOT))
|
||||
return false;
|
||||
|
||||
if (pair.getPairOp() == PairOperator.SMALLERNEQDOT) {
|
||||
UnifyType lhs = pair.getLhsType();
|
||||
UnifyType rhs = pair.getRhsType();
|
||||
if (lhs instanceof WildcardType) {
|
||||
lhs = ((WildcardType)lhs).getWildcardedType();
|
||||
}
|
||||
if (rhs instanceof WildcardType) {
|
||||
rhs = ((WildcardType)rhs).getWildcardedType();
|
||||
}
|
||||
|
||||
if (lhs.equals(rhs)){
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
if(!(lhsType instanceof ReferenceType) && !(lhsType instanceof PlaceholderType))
|
||||
return false;
|
||||
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType))
|
||||
return false;
|
||||
|
||||
return fc.greater(lhsType, new HashSet<>()).contains(rhsType);
|
||||
}
|
||||
|
||||
static boolean erase2(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return false;
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
return fc.grArg(lhsType, new HashSet<>()).contains(rhsType);
|
||||
}
|
||||
|
||||
static boolean erase3(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.EQUALSDOT)
|
||||
return false;
|
||||
|
||||
return pair.getLhsType().equals(pair.getRhsType());
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> swap(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.EQUALSDOT)
|
||||
return Optional.empty();
|
||||
|
||||
if(pair.getLhsType() instanceof PlaceholderType)
|
||||
return Optional.empty();
|
||||
|
||||
if(!(pair.getRhsType() instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(pair.getRhsType(), pair.getLhsType(), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> adapt(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeD = pair.getLhsType();
|
||||
if(!(typeD instanceof ReferenceType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeDs = pair.getRhsType();
|
||||
if(!(typeDs instanceof ReferenceType))
|
||||
return Optional.empty();
|
||||
|
||||
/*if(typeD.getTypeParams().size() == 0 || typeDs.getTypeParams().size() == 0)
|
||||
return Optional.empty();*/
|
||||
|
||||
if(typeD.getName().equals(typeDs.getName()))
|
||||
return Optional.empty();
|
||||
|
||||
|
||||
Optional<UnifyType> opt = fc.getLeftHandedType(typeD.getName());
|
||||
if(!opt.isPresent())
|
||||
return Optional.empty();
|
||||
|
||||
// The generic Version of Type D (D<a1, a2, a3, ... >)
|
||||
UnifyType typeDgen = opt.get();
|
||||
|
||||
// Actually greater+ because the types are ensured to have different names
|
||||
Set<UnifyType> greater = fc.getAncestors(typeDgen);
|
||||
opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();
|
||||
|
||||
if(!opt.isPresent())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType newLhs = opt.get();
|
||||
|
||||
TypeParams typeDParams = typeD.getTypeParams();
|
||||
TypeParams typeDgenParams = typeDgen.getTypeParams();
|
||||
|
||||
Unifier unif = Unifier.identity();
|
||||
for(int i = 0; i < typeDParams.size(); i++) {
|
||||
//System.out.println("ADAPT" +typeDgenParams);
|
||||
if (typeDgenParams.get(i) instanceof PlaceholderType)
|
||||
unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
|
||||
else System.out.println("ERROR");
|
||||
}
|
||||
return Optional.of(new UnifyPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> adaptExt(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeD = pair.getLhsType();
|
||||
if(!(typeD instanceof ReferenceType) && !(typeD instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeExtDs = pair.getRhsType();
|
||||
if(!(typeExtDs instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
if(typeD.getTypeParams().size() == 0 || typeExtDs.getTypeParams().size() == 0)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeDgen;
|
||||
if(typeD instanceof ReferenceType)
|
||||
typeDgen = fc.getLeftHandedType(typeD.getName()).orElse(null);
|
||||
else {
|
||||
Optional<UnifyType> opt = fc.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName());
|
||||
typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null;
|
||||
}
|
||||
|
||||
if(typeDgen == null)
|
||||
return Optional.empty();
|
||||
|
||||
Set<UnifyType> grArg = fc.grArg(typeDgen, new HashSet<>());
|
||||
|
||||
Optional<UnifyType> opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny();
|
||||
|
||||
if(!opt.isPresent())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType newLhs = ((ExtendsType) opt.get()).getExtendedType();
|
||||
|
||||
TypeParams typeDParams = typeD.getTypeParams();
|
||||
TypeParams typeDgenParams = typeDgen.getTypeParams();
|
||||
|
||||
Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
|
||||
for(int i = 1; i < typeDParams.size(); i++)
|
||||
unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
|
||||
|
||||
return Optional.of(new UnifyPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> adaptSup(UnifyPair pair, IFiniteClosure fc) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeDs = pair.getLhsType();
|
||||
if(!(typeDs instanceof ReferenceType) && !(typeDs instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeSupD = pair.getRhsType();
|
||||
if(!(typeSupD instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
if(typeDs.getTypeParams().size() == 0 || typeSupD.getTypeParams().size() == 0)
|
||||
return Optional.empty();
|
||||
|
||||
|
||||
Optional<UnifyType> opt = fc.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName());
|
||||
|
||||
if(!opt.isPresent())
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType typeDgen = opt.get();
|
||||
UnifyType typeSupDgen = new SuperType(typeDgen);
|
||||
|
||||
// Use of smArg instead of grArg because
|
||||
// a in grArg(b) => b in smArg(a)
|
||||
Set<UnifyType> smArg = fc.smArg(typeSupDgen, new HashSet<>());
|
||||
opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();
|
||||
|
||||
if(!opt.isPresent())
|
||||
return Optional.empty();
|
||||
|
||||
// New RHS
|
||||
UnifyType newRhs = null;
|
||||
if(typeDs instanceof ReferenceType)
|
||||
newRhs = new ExtendsType(typeDs);
|
||||
else
|
||||
newRhs = new ExtendsType(((SuperType) typeDs).getSuperedType());
|
||||
|
||||
// New LHS
|
||||
UnifyType newLhs = opt.get();
|
||||
TypeParams typeDParams = typeSupD.getTypeParams();
|
||||
TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams();
|
||||
|
||||
Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0));
|
||||
for(int i = 1; i < typeDParams.size(); i++)
|
||||
unif.add((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i));
|
||||
|
||||
return Optional.of(new UnifyPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Finds the permutation pi of the type arguments of two types based on the finite closure
|
||||
* @param cArgs The type which arguments are permuted
|
||||
* @param dArgs The other type
|
||||
* @return An array containing the values of pi for every type argument of C or an empty array if the search failed.
|
||||
*/
|
||||
private static int[] pi(TypeParams cArgs, TypeParams dArgs) {
|
||||
if(!(cArgs.size()==dArgs.size()))throw new DebugException("Fehler in Unifizierung");
|
||||
|
||||
int[] permutation = new int[dArgs.size()];
|
||||
|
||||
boolean succ = true;
|
||||
for (int dArgIdx = 0; dArgIdx < dArgs.size() && succ; dArgIdx++) {
|
||||
UnifyType dArg = dArgs.get(dArgIdx);
|
||||
succ = false;
|
||||
for (int pi = 0; pi < cArgs.size(); pi++)
|
||||
if (cArgs.get(pi).getName().equals(dArg.getName())) {
|
||||
permutation[dArgIdx] = pi;
|
||||
succ = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
return succ ? permutation : new int[0];
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs) {
|
||||
return subst(pairs, new ArrayList<>());
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> subst(Set<UnifyPair> pairs, List<Set<Constraint<UnifyPair>>> oderConstraints) {
|
||||
HashMap<UnifyType, Integer> typeMap = new HashMap<>();
|
||||
|
||||
Stack<UnifyType> occuringTypes = new Stack<>();
|
||||
|
||||
for(UnifyPair pair : pairs) {
|
||||
occuringTypes.push(pair.getLhsType());
|
||||
occuringTypes.push(pair.getRhsType());
|
||||
}
|
||||
|
||||
while(!occuringTypes.isEmpty()) {
|
||||
UnifyType t1 = occuringTypes.pop();
|
||||
if(!typeMap.containsKey(t1))
|
||||
typeMap.put(t1, 0);
|
||||
typeMap.put(t1, typeMap.get(t1)+1);
|
||||
|
||||
if(t1 instanceof ExtendsType)
|
||||
occuringTypes.push(((ExtendsType) t1).getExtendedType());
|
||||
if(t1 instanceof SuperType)
|
||||
occuringTypes.push(((SuperType) t1).getSuperedType());
|
||||
else
|
||||
t1.getTypeParams().forEach(x -> occuringTypes.push(x));
|
||||
}
|
||||
|
||||
Queue<UnifyPair> result1 = new LinkedList<UnifyPair>(pairs);
|
||||
ArrayList<UnifyPair> result = new ArrayList<UnifyPair>();
|
||||
boolean applied = false;
|
||||
|
||||
while(!result1.isEmpty()) {
|
||||
UnifyPair pair = result1.poll();
|
||||
PlaceholderType lhsType = null;
|
||||
UnifyType rhsType;
|
||||
|
||||
if(pair.getPairOp() == PairOperator.EQUALSDOT
|
||||
&& pair.getLhsType() instanceof PlaceholderType)
|
||||
lhsType = (PlaceholderType) pair.getLhsType();
|
||||
rhsType = pair.getRhsType(); //PL eingefuegt 2017-09-29 statt !((rhsType = pair.getRhsType()) instanceof PlaceholderType)
|
||||
if(lhsType != null
|
||||
//&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType) //PL geloescht am 2017-09-29 Begründung: auch Typvariablen muessen ersetzt werden.
|
||||
&& typeMap.get(lhsType) > 1 // The type occurs in more pairs in the set than just the recent pair.
|
||||
&& !rhsType.getTypeParams().occurs(lhsType)
|
||||
&& !((rhsType instanceof WildcardType) && ((WildcardType)rhsType).getWildcardedType().equals(lhsType))) //PL eigefuegt 2018-02-18
|
||||
{
|
||||
Unifier uni = new Unifier(lhsType, rhsType);
|
||||
result = result.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(ArrayList::new));
|
||||
result1 = result1.stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(LinkedList::new));
|
||||
|
||||
Function<? super Constraint<UnifyPair>,? extends Constraint<UnifyPair>> applyUni = b -> b.stream().map(
|
||||
x -> uni.apply(pair,x)).collect(Collectors.toCollection((b.getExtendConstraint() != null)
|
||||
? () -> new Constraint<UnifyPair>(
|
||||
b.isInherited(),
|
||||
b.getExtendConstraint().stream().map(x -> uni.apply(pair,x)).collect(Collectors.toCollection(Constraint::new)))
|
||||
: () -> new Constraint<UnifyPair>(b.isInherited())
|
||||
));
|
||||
oderConstraints.replaceAll(oc -> oc.stream().map(applyUni).collect(Collectors.toCollection(HashSet::new)));
|
||||
/*
|
||||
oderConstraints = oderConstraints.stream().map(
|
||||
a -> a.stream().map(applyUni
|
||||
//b -> b.stream().map(
|
||||
// x -> uni.apply(pair,x)).collect(Collectors.toCollection(HashSet::new) )
|
||||
).collect(Collectors.toCollection(HashSet::new))
|
||||
).collect(Collectors.toList(ArrayList::new));
|
||||
}
|
||||
*/
|
||||
applied = true;
|
||||
}
|
||||
result.add(pair);
|
||||
}
|
||||
|
||||
return applied ? Optional.of(new HashSet<>(result)) : Optional.empty();
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceWildcardLow(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceWildcardLowRight(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof ExtendsType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceWildcardUp(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof SuperType) || !(rhsType instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), ((SuperType) lhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceWildcardUpRight(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof SuperType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), lhsType, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceFunN(UnifyPair pair) {
|
||||
if((pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
&& (pair.getPairOp() != PairOperator.EQUALSDOT)) //PL 2017-10-03 hinzugefuegt
|
||||
//da Regel auch fuer EQUALSDOT anwendbar
|
||||
//TODO: fuer allen anderen Relationen noch pruefen
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
if(!(lhsType instanceof FunNType) || !(rhsType instanceof FunNType))
|
||||
return Optional.empty();
|
||||
|
||||
FunNType funNLhsType = (FunNType) lhsType;
|
||||
FunNType funNRhsType = (FunNType) rhsType;
|
||||
|
||||
if(funNLhsType.getN() != funNRhsType.getN())
|
||||
return Optional.empty();
|
||||
|
||||
Set<UnifyPair> result = new HashSet<UnifyPair>();
|
||||
if (pair.getPairOp() == PairOperator.SMALLERDOT) {
|
||||
result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
|
||||
result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
}
|
||||
else {// pair.getPairOp() == PairOperator.EQUALDOT
|
||||
result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
|
||||
result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
}
|
||||
result.stream().forEach(x -> { UnifyType l = x.getLhsType();
|
||||
if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); }
|
||||
UnifyType r = x.getRhsType();
|
||||
if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
|
||||
} );
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> greaterFunN(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
if(!(lhsType instanceof FunNType) || !(rhsType instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
FunNType funNLhsType = (FunNType) lhsType;
|
||||
|
||||
Set<UnifyPair> result = new HashSet<UnifyPair>();
|
||||
|
||||
Integer variance = ((PlaceholderType)rhsType).getVariance();
|
||||
Integer inversVariance = distributeVariance.inverseVariance(variance);
|
||||
|
||||
UnifyType[] freshPlaceholders = new UnifyType[funNLhsType.getTypeParams().size()];
|
||||
for(int i = 0; i < freshPlaceholders.length-1; i++) {
|
||||
freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
|
||||
((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance);
|
||||
}
|
||||
freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder();
|
||||
((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance);
|
||||
result.add(new UnifyPair(funNLhsType.getTypeParams().get(funNLhsType.getTypeParams().size()-1), freshPlaceholders[funNLhsType.getTypeParams().size()-1], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
for(int i = 0; i < funNLhsType.getTypeParams().size()-1; i++) {
|
||||
result.add(new UnifyPair(freshPlaceholders[i], funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
result.add(new UnifyPair(rhsType, funNLhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
result.stream().forEach(x -> { UnifyType l = x.getLhsType();
|
||||
if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); }
|
||||
UnifyType r = x.getRhsType();
|
||||
if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
|
||||
} );
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> smallerFunN(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOT)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof FunNType))
|
||||
return Optional.empty();
|
||||
|
||||
FunNType funNRhsType = (FunNType) rhsType;
|
||||
|
||||
Set<UnifyPair> result = new HashSet<UnifyPair>();
|
||||
|
||||
Integer variance = ((PlaceholderType)lhsType).getVariance();
|
||||
Integer inversVariance = distributeVariance.inverseVariance(variance);
|
||||
|
||||
UnifyType[] freshPlaceholders = new UnifyType[funNRhsType.getTypeParams().size()];
|
||||
for(int i = 0; i < freshPlaceholders.length-1; i++) {
|
||||
freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
|
||||
((PlaceholderType)freshPlaceholders[i]).setVariance(inversVariance);
|
||||
}
|
||||
freshPlaceholders[freshPlaceholders.length-1] = PlaceholderType.freshPlaceholder();
|
||||
((PlaceholderType)freshPlaceholders[freshPlaceholders.length-1]).setVariance(variance);
|
||||
|
||||
result.add(new UnifyPair(freshPlaceholders[funNRhsType.getTypeParams().size()-1], funNRhsType.getTypeParams().get(funNRhsType.getTypeParams().size()-1), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
for(int i = 0; i < funNRhsType.getTypeParams().size()-1; i++) {
|
||||
result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), freshPlaceholders[i], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
result.add(new UnifyPair(lhsType, funNRhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
|
||||
result.stream().forEach(x -> { UnifyType l = x.getLhsType();
|
||||
if (l instanceof PlaceholderType) { ((PlaceholderType)l).disableWildcardtable(); }
|
||||
UnifyType r = x.getRhsType();
|
||||
if (r instanceof PlaceholderType) { ((PlaceholderType)r).disableWildcardtable(); }
|
||||
} );
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<UnifyPair> reduceTph(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof ReferenceType))
|
||||
return Optional.empty();
|
||||
|
||||
return Optional.of(new UnifyPair(lhsType, rhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceTphExt(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType extendedType = ((ExtendsType)lhsType).getExtendedType();
|
||||
|
||||
if (extendedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? extends a <.? a
|
||||
|
||||
boolean isGen = extendedType instanceof PlaceholderType && !((PlaceholderType) extendedType).isGenerated();
|
||||
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
if(isGen)
|
||||
result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
else {
|
||||
UnifyType freshTph = PlaceholderType.freshPlaceholder();
|
||||
result.add(new UnifyPair(rhsType, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
result.add(new UnifyPair(extendedType, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
}
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
static Optional<Set<UnifyPair>> reduceTphSup(UnifyPair pair) {
|
||||
if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
if(!(lhsType instanceof SuperType) || !(rhsType instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
UnifyType superedType = ((SuperType)lhsType).getSuperedType();
|
||||
|
||||
if (superedType.equals(rhsType)) return Optional.empty(); //PL 2019-02-18 eingefügt ? super a <.? a
|
||||
|
||||
boolean isGen = superedType instanceof PlaceholderType && !((PlaceholderType) superedType).isGenerated();
|
||||
|
||||
Set<UnifyPair> result = new HashSet<>();
|
||||
if(isGen)
|
||||
result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
else {
|
||||
UnifyType freshTph = PlaceholderType.freshPlaceholder();
|
||||
result.add(new UnifyPair(rhsType, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
|
||||
Set<UnifyType> fBounded = pair.getfBounded();
|
||||
fBounded.add(lhsType);
|
||||
result.add(new UnifyPair(freshTph, superedType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair(), fBounded));
|
||||
}
|
||||
|
||||
return Optional.of(result);
|
||||
}
|
||||
}
|
||||
375
src/main/java/de/dhbwstuttgart/unify2/TypeUnify.java
Normal file
375
src/main/java/de/dhbwstuttgart/unify2/TypeUnify.java
Normal file
@ -0,0 +1,375 @@
|
||||
package de.dhbwstuttgart.unify2;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.unify.UnifyResultModel;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.*;
|
||||
import de.dhbwstuttgart.unify2.model.UnifyConstraintSet;
|
||||
import de.dhbwstuttgart.unify2.model.UnifyConstraintSetBuilder;
|
||||
import de.dhbwstuttgart.unify2.model.UnifyOderConstraint;
|
||||
|
||||
import java.util.*;
|
||||
import java.util.stream.Collectors;
|
||||
import java.util.stream.Stream;
|
||||
|
||||
public class TypeUnify {
|
||||
|
||||
public void unifyOrConstraints(UnifyConstraintSet eq, FiniteClosure fc){
|
||||
|
||||
eq.cartesianProductParallel().map(eqPrime -> unify(eqPrime, fc));
|
||||
}
|
||||
|
||||
public Optional<UnifyResultModel> unify(Set<UnifyPair> eq, FiniteClosure fc){
|
||||
/*
|
||||
TODO: Hier könnte man prüfen, ob es überhaupt einen Sinn macht mit eq weiterzumachen
|
||||
Es könnte eine über threads geteiltes Objekt geben (Feld in TypeUnify), welches unmögliche Klauseln lernt
|
||||
*/
|
||||
|
||||
//Apply Reduce und Apply rules
|
||||
Set<UnifyPair> res = applyTypeUnificationRules(eq, fc);
|
||||
//Split result
|
||||
|
||||
UnifyConstraintSet constraintSet = step4(res, fc);
|
||||
return constraintSet.cartesianProductParallel().map(toSubst -> {
|
||||
//TODO: try subst
|
||||
toSubst = toSubst; //hier substituieren
|
||||
//if it changed:
|
||||
if (true) {
|
||||
return unify(toSubst, fc);
|
||||
}else{
|
||||
//TODO: return the result
|
||||
return Optional.<UnifyResultModel>empty();
|
||||
}
|
||||
}).filter(it -> it.isPresent()).map(Optional::get).findAny();
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Repeatedly applies type unification rules to a set of equations.
|
||||
* This is step one of the unification algorithm.
|
||||
* @return The set of pairs that results from repeated application of the inference rules.
|
||||
*/
|
||||
protected Set<UnifyPair> applyTypeUnificationRules(Set<UnifyPair> eq, FiniteClosure fc) {
|
||||
|
||||
/*
|
||||
* Rule Application Strategy:
|
||||
*
|
||||
* 1. Swap all pairs and erase all erasable pairs
|
||||
* 2. Apply all possible rules to a single pair, then move it to the result set.
|
||||
* Iterating over pairs first, then iterating over rules prevents the application
|
||||
* of rules to a "finished" pair over and over.
|
||||
* 2.1 Apply all rules repeatedly except for erase rules. If
|
||||
* the application of a rule creates new pairs, check immediately
|
||||
* against the erase rules.
|
||||
*/
|
||||
|
||||
|
||||
LinkedHashSet<UnifyPair> targetSet = new LinkedHashSet<UnifyPair>();
|
||||
LinkedList<UnifyPair> eqQueue = new LinkedList<>();
|
||||
|
||||
/*
|
||||
* Swap all pairs and erase all erasable pairs
|
||||
*/
|
||||
eq.forEach(x -> swapAddOrErase(x, fc, eqQueue));
|
||||
|
||||
/*
|
||||
* Apply rules until the queue is empty
|
||||
*/
|
||||
while(!eqQueue.isEmpty()) {
|
||||
UnifyPair pair = eqQueue.pollFirst();
|
||||
|
||||
// ReduceUp, ReduceLow, ReduceUpLow
|
||||
Optional<UnifyPair> opt = rules.reduceUpLow(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceLow(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceUp(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardLow(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardLowRight(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardUp(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardUpRight(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardLowUp(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardUpLow(pair);
|
||||
opt = opt.isPresent() ? opt : rules.reduceWildcardLeft(pair);
|
||||
|
||||
// Reduce TPH
|
||||
opt = opt.isPresent() ? opt : rules.reduceTph(pair);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(opt.isPresent()) {
|
||||
swapAddOrErase(opt.get(), fc, eqQueue);
|
||||
continue;
|
||||
}
|
||||
|
||||
// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
|
||||
Optional<Set<UnifyPair>> optSet = rules.reduce1(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc);
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair);
|
||||
|
||||
// ReduceTphExt, ReduceTphSup
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceTphExt(pair);
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceTphSup(pair);
|
||||
|
||||
|
||||
// FunN Rules
|
||||
optSet = optSet.isPresent() ? optSet : rules.reduceFunN(pair);
|
||||
optSet = optSet.isPresent() ? optSet : rules.greaterFunN(pair);
|
||||
optSet = optSet.isPresent() ? optSet : rules.smallerFunN(pair);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(optSet.isPresent()) {
|
||||
optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue));
|
||||
continue;
|
||||
}
|
||||
|
||||
// Adapt, AdaptExt, AdaptSup
|
||||
opt = rules.adapt(pair, fc);
|
||||
opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc);
|
||||
opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc);
|
||||
|
||||
// One of the rules has been applied
|
||||
if(opt.isPresent()) {
|
||||
swapAddOrErase(opt.get(), fc, eqQueue);
|
||||
continue;
|
||||
}
|
||||
|
||||
// None of the rules has been applied
|
||||
targetSet.add(pair);
|
||||
}
|
||||
|
||||
return targetSet;
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates sets of pairs specified in the fourth step. Does not calculate cartesian products.
|
||||
* @return The set of the eight cases (without empty sets). Each case is a set, containing sets generated
|
||||
* from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements
|
||||
* (as in case 1 where sigma is added to the innermost set).
|
||||
*/
|
||||
protected UnifyConstraintSet step4(Set<UnifyPair> eq2s, FiniteClosure fc) {
|
||||
Set<UnifyOderConstraint> result = new HashSet<>(8);
|
||||
|
||||
for(UnifyPair pair : eq2s) {
|
||||
PairOperator pairOp = pair.getPairOp();
|
||||
UnifyType lhsType = pair.getLhsType();
|
||||
UnifyType rhsType = pair.getRhsType();
|
||||
|
||||
// Case 1: (a <. Theta')
|
||||
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
|
||||
result.add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
|
||||
|
||||
// Case 2: (a <.? ? ext Theta')
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
|
||||
result.add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
|
||||
|
||||
// Case 3: (a <.? ? sup Theta')
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
|
||||
result.add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
|
||||
|
||||
// Case 4 was replaced by an inference rule
|
||||
// Case 4: (a <.? Theta')
|
||||
//else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
|
||||
// result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc));
|
||||
|
||||
// Case 5: (Theta <. a)
|
||||
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
|
||||
result.add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
|
||||
|
||||
// Case 6 was replaced by an inference rule.
|
||||
// Case 6: (? ext Theta <.? a)
|
||||
//else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
|
||||
// result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));
|
||||
|
||||
// Case 7 was replaced by an inference rule
|
||||
// Case 7: (? sup Theta <.? a)
|
||||
//else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
|
||||
// result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc));
|
||||
|
||||
// Case 8: (Theta <.? a)
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
|
||||
result.add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
|
||||
// Case unknown: If a pair fits no other case, then the type unification has failed.
|
||||
// Through application of the rules, every pair should have one of the above forms.
|
||||
// Pairs that do not have one of the aboves form are contradictory.
|
||||
else {
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
// Filter empty sets or sets that only contain an empty set.
|
||||
//Andi: Why? Should they exist? this should be an error then
|
||||
return new UnifyConstraintSet(result);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Cartesian product Case 1: (a <. Theta')
|
||||
*/
|
||||
protected UnifyOderConstraint unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
|
||||
Set<Set<UnifyPair>> result = new HashSet<>();
|
||||
|
||||
boolean allGen = thetaPrime.getTypeParams().size() > 0;
|
||||
for(UnifyType t : thetaPrime.getTypeParams())
|
||||
if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
|
||||
allGen = false;
|
||||
break;
|
||||
}
|
||||
|
||||
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 = stdUnify.unify(tqp, thetaPrime);
|
||||
if (!opt.isPresent())
|
||||
continue;
|
||||
|
||||
Unifier unifier = opt.get();
|
||||
unifier.swapPlaceholderSubstitutions(thetaPrime.getTypeParams());
|
||||
Set<UnifyPair> substitutionSet = new HashSet<>();
|
||||
for (Entry<PlaceholderType, UnifyType> sigma : unifier)
|
||||
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<>();
|
||||
|
||||
for(int i = 0; !allGen && 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));
|
||||
}
|
||||
|
||||
if(allGen)
|
||||
resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
|
||||
else
|
||||
resultPrime.add(new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT));
|
||||
resultPrime.addAll(substitutionSet);
|
||||
result.add(resultPrime);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
return new UnifyOderConstraint(result);
|
||||
}
|
||||
|
||||
/**
|
||||
* Cartesian Product Case 2: (a <.? ? ext Theta')
|
||||
*/
|
||||
private UnifyOderConstraint unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
|
||||
Set<Set<UnifyPair>> result = new HashSet<>();
|
||||
|
||||
UnifyType aPrime = PlaceholderType.freshPlaceholder();
|
||||
UnifyType extAPrime = new ExtendsType(aPrime);
|
||||
UnifyType thetaPrime = extThetaPrime.getExtendedType();
|
||||
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);
|
||||
return new UnifyOderConstraint(result);
|
||||
}
|
||||
|
||||
/**
|
||||
* Cartesian Product Case 3: (a <.? ? sup Theta')
|
||||
*/
|
||||
private UnifyOderConstraint unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
|
||||
Set<Set<UnifyPair>> result = new HashSet<>();
|
||||
|
||||
UnifyType aPrime = PlaceholderType.freshPlaceholder();
|
||||
UnifyType supAPrime = new SuperType(aPrime);
|
||||
UnifyType thetaPrime = subThetaPrime.getSuperedType();
|
||||
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);
|
||||
|
||||
return new UnifyOderConstraint(result);
|
||||
}
|
||||
|
||||
/**
|
||||
* Cartesian Product Case 5: (Theta <. a)
|
||||
*/
|
||||
private UnifyOderConstraint unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
|
||||
Set<Set<UnifyPair>> result = new HashSet<>();
|
||||
|
||||
boolean allGen = theta.getTypeParams().size() > 0;
|
||||
for(UnifyType t : theta.getTypeParams())
|
||||
if(!(t instanceof PlaceholderType) || !((PlaceholderType) t).isGenerated()) {
|
||||
allGen = false;
|
||||
break;
|
||||
}
|
||||
|
||||
for(UnifyType thetaS : fc.greater(theta)) {
|
||||
Set<UnifyPair> resultPrime = new HashSet<>();
|
||||
|
||||
UnifyType[] freshTphs = new UnifyType[thetaS.getTypeParams().size()];
|
||||
for(int i = 0; !allGen && i < freshTphs.length; i++) {
|
||||
freshTphs[i] = PlaceholderType.freshPlaceholder();
|
||||
resultPrime.add(new UnifyPair(thetaS.getTypeParams().get(i), freshTphs[i], PairOperator.SMALLERDOTWC));
|
||||
}
|
||||
|
||||
if(allGen)
|
||||
resultPrime.add(new UnifyPair(a, thetaS, PairOperator.EQUALSDOT));
|
||||
else
|
||||
resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT));
|
||||
result.add(resultPrime);
|
||||
}
|
||||
|
||||
return new UnifyOderConstraint(result);
|
||||
}
|
||||
|
||||
/**
|
||||
* Cartesian Product Case 8: (Theta <.? a)
|
||||
*/
|
||||
private UnifyOderConstraint 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, 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 new UnifyOderConstraint(result);
|
||||
}
|
||||
|
||||
}
|
||||
@ -0,0 +1,124 @@
|
||||
package de.dhbwstuttgart.unify2.model;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.*;
|
||||
import java.util.function.BinaryOperator;
|
||||
import java.util.function.Consumer;
|
||||
import java.util.stream.Collectors;
|
||||
import java.util.stream.Stream;
|
||||
import java.util.stream.StreamSupport;
|
||||
|
||||
/*
|
||||
OrC1 OrC2 OrC3 -> Constraints
|
||||
Step4: OrC1 OrC2/c OrC3 OrC4
|
||||
|
||||
Tiefensuche, neue UnifyConstraints erstellen
|
||||
|
||||
Wie wird ConstraintSet geändert?
|
||||
|
||||
wird nicht gebraucht:
|
||||
( map -> bei subst
|
||||
Alle Constraints ändern, neues ConstraintSet zurückgeben )
|
||||
|
||||
Step 4 bildet anschließend das karthesische Produkt und muss über alle Möglichkeiten iterieren
|
||||
die erste möglichkeit vom karthesischen produkt nehmen, subst schritt ausführen und mit dem Ergebnis (einzelnes Constraint Set) weiterarbeiten
|
||||
|
||||
*/
|
||||
|
||||
public class UnifyConstraintSet {
|
||||
Set<UnifyOderConstraint> oderConstraints = new HashSet<>();
|
||||
|
||||
public UnifyConstraintSet(Set<UnifyOderConstraint> constraints){
|
||||
if(constraints.isEmpty())throw new RuntimeException("Empty constraint set");
|
||||
this.oderConstraints = constraints;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString(){
|
||||
BinaryOperator<String> b = (x, y) -> x+y;
|
||||
return "ODER:" + this.oderConstraints.stream().reduce("", (x,y) -> x.toString()+ "\n" +y, b);
|
||||
}
|
||||
|
||||
/*
|
||||
Cartesian product als optimierter Stream
|
||||
|
||||
- Ein Split teilt das Set so auf, dass der zweite Thread jedes zweite Element behandelt
|
||||
- Ein thread der jedes zweite element behandelt wird gesplittet indem
|
||||
|
||||
1 2 1 2 1 2 1 2 => (o = 0, n = 2), (o = 1, n = 2)
|
||||
1 2 1 3 1 2 1 3 => (o = 0, n = 2), (o = 1, n = 4), (o = 3, n = 4)
|
||||
|
||||
*/
|
||||
private class ConstraintSpliterator implements Spliterator<Set<UnifyPair>> {
|
||||
private List<UnifyOderConstraint> constraints;
|
||||
private long i = 0;
|
||||
private long iterationFactor = 1;
|
||||
private long max = 0;
|
||||
private List<Integer> sizes;
|
||||
private List<Long> bases = new ArrayList<>();
|
||||
|
||||
ConstraintSpliterator(List<UnifyOderConstraint> constraints){
|
||||
this.constraints = constraints;
|
||||
sizes = constraints.stream().map(UnifyOderConstraint::getSize).collect(Collectors.toList());
|
||||
long base = 1;
|
||||
for(int size : sizes){
|
||||
bases.add(base);
|
||||
base *= size;
|
||||
}
|
||||
i = 0;
|
||||
max = estimateSize() - 1;
|
||||
}
|
||||
|
||||
ConstraintSpliterator(List<UnifyOderConstraint> constraints, long start, long factor){
|
||||
this(constraints);
|
||||
i = start;
|
||||
this.iterationFactor = factor;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean tryAdvance(Consumer<? super Set<UnifyPair>> consumer) {
|
||||
if(i > max) return false;
|
||||
consumer.accept(get(i));
|
||||
i++;
|
||||
return true;
|
||||
}
|
||||
|
||||
private Set<UnifyPair> get(long num){
|
||||
Set<UnifyPair> ret = new HashSet<>();
|
||||
Iterator<Long> baseIt = bases.iterator();
|
||||
for(UnifyOderConstraint constraint : constraints){
|
||||
ret.addAll(constraint.get((int) ((num/baseIt.next())%constraint.getSize())));
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
@Override
|
||||
public Spliterator<Set<UnifyPair>> trySplit() {
|
||||
if(max - (i+iterationFactor * 2) < 0) return null;
|
||||
long iNext = i + iterationFactor;
|
||||
iterationFactor *= 2;
|
||||
return new UnifyConstraintSet.ConstraintSpliterator(constraints, iNext, iterationFactor);
|
||||
}
|
||||
|
||||
@Override
|
||||
public long estimateSize() {
|
||||
long ret = 1;
|
||||
for (int size : sizes)ret*=size;
|
||||
return ret;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int characteristics() {
|
||||
return ORDERED | SIZED | IMMUTABLE | NONNULL;
|
||||
}
|
||||
}
|
||||
|
||||
public Stream<Set<UnifyPair>> cartesianProductParallel(){
|
||||
return StreamSupport.stream(new UnifyConstraintSet.ConstraintSpliterator(oderConstraints.stream().collect(Collectors.toList())), true);
|
||||
}
|
||||
|
||||
public Stream<Set<UnifyPair>> cartesianProductParallel(Comparator<Set<UnifyPair>> prioritiser){
|
||||
return StreamSupport.stream(new UnifyConstraintSet.ConstraintSpliterator(oderConstraints.stream().collect(Collectors.toList())), true);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,30 @@
|
||||
package de.dhbwstuttgart.unify2.model;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
public class UnifyConstraintSetBuilder {
|
||||
|
||||
private Set<UnifyPair> undConstraints = new HashSet<>();
|
||||
private Set<UnifyOderConstraint> oderConstraints = new HashSet<>();
|
||||
private boolean done = false;
|
||||
|
||||
public void addUndConstraint(UnifyPair p){
|
||||
undConstraints.add(p);
|
||||
}
|
||||
|
||||
public void addOderConstraint(UnifyOderConstraint orConstraint) {
|
||||
oderConstraints.add(orConstraint);
|
||||
}
|
||||
|
||||
public UnifyConstraintSet build(){
|
||||
if(done)throw new RuntimeException("Trying to build cartesian product twice");
|
||||
this.done = true;
|
||||
if(!undConstraints.isEmpty())
|
||||
oderConstraints.add(new UnifyOderConstraint(Set.of(undConstraints)));
|
||||
return new UnifyConstraintSet(oderConstraints);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,27 @@
|
||||
package de.dhbwstuttgart.unify2.model;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class UnifyOderConstraint {
|
||||
|
||||
private final List<Set<UnifyPair>> cons;
|
||||
public UnifyOderConstraint(Set<Set<UnifyPair>> orCons){
|
||||
if(orCons.isEmpty())throw new RuntimeException("Empty constraint set");
|
||||
for(Set<UnifyPair> c : orCons){
|
||||
if(c.isEmpty())throw new RuntimeException("Empty constraint set");
|
||||
}
|
||||
this.cons = orCons.stream().collect(Collectors.toList());
|
||||
}
|
||||
|
||||
public int getSize(){
|
||||
return cons.size();
|
||||
}
|
||||
|
||||
public Set<UnifyPair> get(int l) {
|
||||
return cons.get(l);
|
||||
}
|
||||
}
|
||||
@ -40,7 +40,7 @@ public class AllgemeinTest {
|
||||
//String className = "FCTest3";
|
||||
//String className = "Var";
|
||||
//String className = "Put";
|
||||
String className = "Twice";
|
||||
String className = "Cycle";
|
||||
//PL 2019-10-24: genutzt fuer unterschiedliche Tests
|
||||
path = System.getProperty("user.dir")+"/src/test/resources/AllgemeinTest/" + className + ".jav";
|
||||
//path = System.getProperty("user.dir")+"/src/test/resources/AllgemeinTest/Overloading_Generics.jav";
|
||||
|
||||
@ -6,6 +6,7 @@ import de.dhbwstuttgart.bytecode.insertGenerics.*;
|
||||
import org.junit.Test;
|
||||
import static org.junit.Assert.assertEquals;
|
||||
|
||||
import java.io.BufferedReader;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashMap;
|
||||
import java.util.List;
|
||||
|
||||
62
src/test/java/typeinference/UnifyConstraintSetTests.java
Normal file
62
src/test/java/typeinference/UnifyConstraintSetTests.java
Normal file
@ -0,0 +1,62 @@
|
||||
package typeinference;
|
||||
|
||||
import de.dhbwstuttgart.parser.NullToken;
|
||||
import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSetBuilder;
|
||||
import de.dhbwstuttgart.typeinference.constraints.OderConstraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import org.junit.Test;
|
||||
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class UnifyConstraintSetTests {
|
||||
@Test
|
||||
public void cartesianProductTestSingleConstraint(){
|
||||
ConstraintSetBuilder builder = new ConstraintSetBuilder();
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()))));
|
||||
List<Set<Pair>> result = builder.build().cartesianProductParallel().collect(Collectors.toList());
|
||||
assert result.size() == 1;
|
||||
}
|
||||
|
||||
@Test
|
||||
public void cartesianProductTestSingleOderConstraint(){
|
||||
ConstraintSetBuilder builder = new ConstraintSetBuilder();
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
List<Set<Pair>> result = builder.build().cartesianProductParallel().collect(Collectors.toList());
|
||||
assert result.size() == 2;
|
||||
}
|
||||
|
||||
@Test
|
||||
public void cartesianProductTestTwoOderConstraint(){
|
||||
ConstraintSetBuilder builder = new ConstraintSetBuilder();
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
List<Set<Pair>> result = builder.build().cartesianProductParallel().collect(Collectors.toList());
|
||||
assert result.size() == 4;
|
||||
}
|
||||
|
||||
@Test
|
||||
public void cartesianProductTestThreeOderConstraint(){
|
||||
ConstraintSetBuilder builder = new ConstraintSetBuilder();
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
builder.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()))));
|
||||
List<Set<Pair>> result = builder.build().cartesianProductParallel().collect(Collectors.toList());
|
||||
assert result.size() == 4;
|
||||
|
||||
ConstraintSetBuilder builder2 = new ConstraintSetBuilder();
|
||||
builder2.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
builder2.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
builder2.addOderConstraint(new OderConstraint(Set.of(Set.of(generatePair()), Set.of(generatePair()))));
|
||||
List<Set<Pair>> result2 = builder2.build().cartesianProductParallel().collect(Collectors.toList());
|
||||
|
||||
assert result2.stream().map( a -> a.stream().map(p -> p.TA1.toString()).reduce("", (x, y)-> x+" "+y)).collect(Collectors.toSet()).size() == 8;
|
||||
assert result2.size() == 8;
|
||||
}
|
||||
|
||||
public Pair generatePair(){
|
||||
return new Pair(TypePlaceholder.fresh(new NullToken()), TypePlaceholder.fresh(new NullToken()));
|
||||
}
|
||||
}
|
||||
11
src/test/resources/AllgemeinTest/Cycle.jav
Normal file
11
src/test/resources/AllgemeinTest/Cycle.jav
Normal file
@ -0,0 +1,11 @@
|
||||
class Cycle{
|
||||
|
||||
<A> A und(A a, A b){
|
||||
return a;
|
||||
}
|
||||
|
||||
m(a){
|
||||
return und(m(m(a)), a);
|
||||
}
|
||||
|
||||
}
|
||||
5
src/test/resources/AllgemeinTest/Twice.jav
Normal file
5
src/test/resources/AllgemeinTest/Twice.jav
Normal file
@ -0,0 +1,5 @@
|
||||
class Twice{
|
||||
m(x, f){
|
||||
return f.apply(f.apply(x));
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user