|
|
|
@ -23,14 +23,17 @@ import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.FunNType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.ReferenceType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair;
|
|
|
|
|
import de.dhbwstuttgart.typeinference.unify.model.Pair;
|
|
|
|
|
|
|
|
|
|
import java.io.File;
|
|
|
|
|
import java.io.FileWriter;
|
|
|
|
@ -82,7 +85,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
|
|
|
|
|
Integer noAllErasedElements = 0;
|
|
|
|
|
|
|
|
|
|
Integer noBacktracking = 0;
|
|
|
|
|
static int noBacktracking;
|
|
|
|
|
|
|
|
|
|
public TypeUnifyTask() {
|
|
|
|
|
rules = new RuleSet();
|
|
|
|
@ -555,6 +558,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
/* auskommentiert um alle Max und min Betrachtung auszuschalten ENDE */
|
|
|
|
|
|
|
|
|
|
if (isUndefinedPairSetSet(res)) {
|
|
|
|
|
int nofstred= 0;
|
|
|
|
|
Set<UnifyPair> abhSubst = res.stream()
|
|
|
|
|
.map(b ->
|
|
|
|
|
b.stream()
|
|
|
|
@ -566,23 +570,41 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
.filter(x -> b.contains(x))
|
|
|
|
|
//.filter(y -> abhSubst.contains(y))
|
|
|
|
|
.collect(Collectors.toCollection(HashSet::new));
|
|
|
|
|
Set<PlaceholderType> vars = durchschnitt.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new));
|
|
|
|
|
//Set<PlaceholderType> vars = durchschnitt.stream().map(x -> (PlaceholderType)x.getLhsType()).collect(Collectors.toCollection(HashSet::new));
|
|
|
|
|
int len = nextSetasList.size();
|
|
|
|
|
Set<UnifyPair> undefRes = res.stream().reduce((y,z) -> { y.addAll(z); return y;}).get(); //flatten aller undef results
|
|
|
|
|
Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair = undefRes.stream()
|
|
|
|
|
.map(x -> { Set<UnifyPair> su = x.getAllSubstitutions(); //alle benutzten Substitutionen
|
|
|
|
|
su.add(x.getGroundBasePair()); // urspruengliches Paar
|
|
|
|
|
su.removeAll(durchschnitt); //alle aktuell genänderten Paare entfernen
|
|
|
|
|
return new Pair<>(su, x.getGroundBasePair());})
|
|
|
|
|
.collect(Collectors.toCollection(HashSet::new));
|
|
|
|
|
if (res.size() > 1) {
|
|
|
|
|
System.out.println();
|
|
|
|
|
}
|
|
|
|
|
nextSetasList = nextSetasList.stream().filter(x -> {
|
|
|
|
|
//Boolean ret = false;
|
|
|
|
|
//for (PlaceholderType var : vars) {
|
|
|
|
|
// ret = ret || x.stream().map(b -> b.getLhsType().equals(var)).reduce((c,d) -> c || d).get();
|
|
|
|
|
//}
|
|
|
|
|
return (!x.containsAll(durchschnitt));
|
|
|
|
|
}).collect(Collectors.toCollection(ArrayList::new));
|
|
|
|
|
})//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) //fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10
|
|
|
|
|
.collect(Collectors.toCollection(ArrayList::new));
|
|
|
|
|
nofstred = nextSetasList.size();
|
|
|
|
|
//NOCH NICHT korrekt PL 2018-10-12
|
|
|
|
|
//nextSetasList = nextSetasList.stream().filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y))
|
|
|
|
|
// .collect(Collectors.toCollection(ArrayList::new));
|
|
|
|
|
writeLog("res (undef): " + res.toString());
|
|
|
|
|
writeLog("abhSubst: " + abhSubst.toString());
|
|
|
|
|
writeLog("a: " + a.toString());
|
|
|
|
|
writeLog("Durchschnitt: " + durchschnitt.toString());
|
|
|
|
|
writeLog("nextSet: " + nextSet.toString());
|
|
|
|
|
writeLog("nextSetasList: " + nextSetasList.toString());
|
|
|
|
|
writeLog("Number first erased Elements (undef): " + (len - nofstred));
|
|
|
|
|
writeLog("Number second erased Elements (undef): " + (nofstred- nextSetasList.size()));
|
|
|
|
|
writeLog("Number erased Elements (undef): " + (len - nextSetasList.size()));
|
|
|
|
|
noAllErasedElements = noAllErasedElements + (len - nextSetasList.size());
|
|
|
|
|
writeLog("Number erased Elements (undef): " + noAllErasedElements.toString());
|
|
|
|
|
writeLog("Number of all erased Elements (undef): " + noAllErasedElements.toString());
|
|
|
|
|
noBacktracking++;
|
|
|
|
|
writeLog("Number of Backtracking: " + noBacktracking);
|
|
|
|
|
System.out.println("");
|
|
|
|
@ -598,6 +620,94 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|
|
|
|
return result;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
protected boolean couldBecorrect(Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set<UnifyPair> nextElem) {
|
|
|
|
|
return reducedUndefResSubstGroundedBasePair.stream()
|
|
|
|
|
.map(pair -> {
|
|
|
|
|
Set<UnifyPair> reducedAbhSubst = pair.getKey();
|
|
|
|
|
reducedAbhSubst.addAll(nextElem);
|
|
|
|
|
Optional<Set<UnifyPair>> substRes = rules.subst(reducedAbhSubst);
|
|
|
|
|
if (!substRes.isPresent()) {
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
//PL 2018-10-12
|
|
|
|
|
//Evtl. zurest applyTypeUnification aufrufen
|
|
|
|
|
//evtl auch unify aufrufen
|
|
|
|
|
else {
|
|
|
|
|
UnifyPair checkPair = substRes.get().stream()
|
|
|
|
|
.filter(x -> x.getGroundBasePair().equals(pair.getValue().get())).findFirst().get();
|
|
|
|
|
if (((checkPair.getLhsType() instanceof PlaceholderType) || (checkPair.getRhsType() instanceof PlaceholderType))
|
|
|
|
|
&& (checkPair.getPairOp() == PairOperator.SMALLERDOT || checkPair.getPairOp() == PairOperator.SMALLERDOTWC))
|
|
|
|
|
{
|
|
|
|
|
/*
|
|
|
|
|
Set<UnifyPair> setCheckPair = new HashSet<>();
|
|
|
|
|
setCheckPair.add(checkPair);
|
|
|
|
|
Set<UnifyPair> setReturnCheckPair = applyTypeUnificationRules(setCheckPair, fc);
|
|
|
|
|
UnifyPair checkPair1 = setReturnCheckPair.iterator().next();
|
|
|
|
|
Set<UnifyPair> up = new HashSet<>();
|
|
|
|
|
up.add(checkPair1);
|
|
|
|
|
Set<UnifyPair> undef = new HashSet<>();
|
|
|
|
|
*/
|
|
|
|
|
PairOperator pairOp = checkPair.getPairOp();
|
|
|
|
|
UnifyType lhsType = checkPair.getLhsType();
|
|
|
|
|
UnifyType rhsType = checkPair.getRhsType();
|
|
|
|
|
///* Case 1: (a <. Theta')
|
|
|
|
|
if ((((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.SMALLERNEQDOT)) && lhsType instanceof PlaceholderType)
|
|
|
|
|
// Case 2: (a <.? ? ext Theta')
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
|
|
|
|
|
// Case 3: (a <.? ? sup Theta')
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
|
|
|
|
|
|
|
|
|
|
// Case 4 was replaced by an inference rule
|
|
|
|
|
// Case 4: (a <.? Theta')
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
|
|
|
|
|
// Case 5: (Theta <. a)
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOT) && rhsType instanceof PlaceholderType)
|
|
|
|
|
// Case 6 was replaced by an inference rule.
|
|
|
|
|
// Case 6: (? ext Theta <.? a)
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
|
|
|
|
|
// Case 7 was replaced by an inference rule
|
|
|
|
|
// Case 7: (? sup Theta <.? a)
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
|
|
|
|
|
// Case 8: (Theta <.? a)
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
|
|
|
|
|
//reduceWildcardLow
|
|
|
|
|
|| (pairOp == PairOperator.SMALLERDOTWC && (lhsType instanceof ExtendsType) && (rhsType instanceof ExtendsType))
|
|
|
|
|
//reduceWildcardLowRight
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof ExtendsType))
|
|
|
|
|
//reduceWildcardUp
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && (rhsType instanceof SuperType))
|
|
|
|
|
//reduceWildcardUpRight
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ReferenceType) && (rhsType instanceof SuperType))
|
|
|
|
|
//reduceFunN
|
|
|
|
|
|| (((pairOp == PairOperator.SMALLERDOT) || (pairOp == PairOperator.EQUALSDOT))
|
|
|
|
|
//PL 2017-10-03 hinzugefuegt
|
|
|
|
|
//da Regel auch fuer EQUALSDOT anwendbar
|
|
|
|
|
&& (lhsType instanceof FunNType) && (rhsType instanceof FunNType))
|
|
|
|
|
//greaterFunN
|
|
|
|
|
|| ((pairOp== PairOperator.SMALLERDOT) && (lhsType instanceof FunNType) && (rhsType instanceof PlaceholderType))
|
|
|
|
|
//smallerFunN
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOT) && (lhsType instanceof PlaceholderType && rhsType instanceof FunNType))
|
|
|
|
|
//reduceTph
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof PlaceholderType && rhsType instanceof ReferenceType))
|
|
|
|
|
//reduceTphExt
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof ExtendsType) && rhsType instanceof PlaceholderType)
|
|
|
|
|
//reduceTphSup
|
|
|
|
|
|| ((pairOp == PairOperator.SMALLERDOTWC) && (lhsType instanceof SuperType) && rhsType instanceof PlaceholderType)) {
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
// 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 {
|
|
|
|
|
writeLog("Second erase:" +checkPair.toString());
|
|
|
|
|
return false;
|
|
|
|
|
}
|
|
|
|
|
//*/
|
|
|
|
|
} else {
|
|
|
|
|
//Pair type <. ? extends ? extends type betrachten TODO PL 2018-10-09
|
|
|
|
|
}}
|
|
|
|
|
return true;}).reduce((xx, yy) -> xx || yy).get();
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
protected boolean isUndefinedPairSet(Set<UnifyPair> s) {
|
|
|
|
|
if (s.size() >= 1 ) {
|
|
|
|
|