modified: ../src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java

vor Loeschung von checkA
This commit is contained in:
pl@gohorb.ba-horb.de 2021-01-14 14:59:20 +01:00
parent 1cf22d2602
commit 163f0f3047

View File

@ -624,7 +624,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
*/
Set<Set<UnifyPair>> computeCartesianRecursive(ArrayList<Set<? extends Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
//fstElems: Alle 1-elementigen Mengen, die nur ein Paar
//oneElems: Alle 1-elementigen Mengen, die nur ein Paar
//a <. theta, theta <. a oder a =. theta enthalten
Set<Set<UnifyPair>> oneElems = new HashSet<>();
oneElems.addAll(topLevelSets.stream()
@ -846,11 +846,19 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
i++;
Set<Set<UnifyPair>> elems = new HashSet<Set<UnifyPair>>(oneElems);
writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n");
//Ergebnisvariable für den aktuelle Thread
Set<Set<UnifyPair>> res = new HashSet<>();
//Menge der Ergebnisse der geforkten Threads
Set<Set<Set<UnifyPair>>> add_res = new HashSet<>();
Set<Set<UnifyPair>> aParDef = new HashSet<>();
/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
/* Wenn bei (a \in theta) \in a zu Widerspruch in oneElems wird
* a verworfen und zu nächstem Element von nextSetasList gegangen
*/
if (!oderConstraint && !sameEqSet.isEmpty()) {
//optAPair enthaelt ggf. das Paar a = ty' \in a
//unterscheidet sich von optOrigPair, da dort a = ty
@ -873,15 +881,20 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
UnifyPair aPair = optAPair.get();
//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
writeLog("variance: " + variance + "sameEqSet:" + sameEqSet);
boolean newCheckA = newCheckA(a, sameEqSet, result);
if (!checkA(aPair, sameEqSet, elems, result)) {
writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
a = null;
noShortendElements++;
continue;
}
else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
}
}
/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
/* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread
* gestartet, der parallel weiterarbeitet.
*/
if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) {
Set<TypeUnify2Task> forks = new HashSet<>();
Set<UnifyPair> newEqOrig = new HashSet<>(eq);
@ -931,11 +944,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
UnifyPair aPair = optAPair.get();
//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
boolean newCheckA = newCheckA(nSaL, sameEqSet, result);
if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
nSaL = null;
noShortendElements++;
continue;
}
else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
}
}
/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
@ -1051,11 +1067,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
UnifyPair aPair = optAPair.get();
//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
writeLog("variance: " + new Integer(variance).toString() + "sameEqSet:" + sameEqSet);
boolean newCheckA = newCheckA(nSaL, sameEqSet, result);
if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
writeLog("newCheckA:" + new Boolean(newCheckA == false).toString());
nSaL = null;
noShortendElements++;
continue;
}
else writeLog("newCheckA:" + new Boolean(newCheckA == true).toString());
}
}
/* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
@ -1201,11 +1220,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
};
}
//noOfThread++;
} else {
//parallel = false; //Wenn MaxNoOfThreads erreicht ist, sequentiell weiterarbeiten
} else {//parallel = false oder MaxNoOfThreads ist erreicht, sequentiell weiterarbeiten
elems.add(a); //PL 2019-01-16 muss das wirklich hin steht schon in Zeile 859 ja braucht man siehe Zeile 859
res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe);
}}}
//Ab hier alle parallele Berechnungen wieder zusammengeführt.
if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) {
//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
result = res;
@ -1540,6 +1560,66 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
return result;
}
protected Boolean newCheckA(Set<UnifyPair> a, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> result) {
//optAPair enthaelt ggf. das Paar a = ty' \in a
//unterscheidet sich von optOrigPair, da dort a = ty
Optional<UnifyPair> optAPair =
a.stream().filter(x -> (x.getPairOp().equals(PairOperator.EQUALSDOT)))
.filter(x -> //Sicherstellen, dass bei a = ty a auch wirklich die gesuchte Typvariable ist
x.getLhsType().equals(x.getBasePair().getLhsType()) ||
x.getLhsType().equals(x.getBasePair().getRhsType()))
.findFirst();
if (optAPair.isPresent()) {//basepair ist entweder a <. Ty oder ty <. a
UnifyPair aPair = optAPair.get();
//writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
writeLog("checkA: " + aPair + "sameEqSet: " + sameEqSet);
for (UnifyPair sameEq : sameEqSet) {
if (sameEq.getLhsType() instanceof PlaceholderType) {
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getAllSubstitutions());
unitedSubst.addAll(aPair.getAllBases());
unitedSubst.addAll(sameEq.getAllSubstitutions());
unitedSubst.addAll(sameEq.getAllBases());
localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
finalresult = false;
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0);
finalresult = true;
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet);
return false;
}
}
else {
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getAllSubstitutions());
unitedSubst.addAll(aPair.getAllBases());
unitedSubst.addAll(sameEq.getAllSubstitutions());
unitedSubst.addAll(sameEq.getAllBases());
localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
finalresult = false;
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0);
finalresult = true;
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet);
return false;
}
}
}
writeLog("TRUE: " + aPair + "sameEqSet: " + sameEqSet);
return true;
}
return true;
}
protected Boolean checkA (UnifyPair aPair, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> elems, Set<Set<UnifyPair>> result) {
writeLog("checkA: " + aPair + "sameEqSet: " + sameEqSet);
for (UnifyPair sameEq : sameEqSet) {