From 163f0f304763a26533abd0a57d89a48442cd8106 Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Thu, 14 Jan 2021 14:59:20 +0100 Subject: [PATCH] modified: ../src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java vor Loeschung von checkA --- .../typeinference/unify/TypeUnifyTask.java | 90 +++++++++++++++++-- 1 file changed, 85 insertions(+), 5 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index aa2e25a0c..8377edd6a 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -624,7 +624,7 @@ public class TypeUnifyTask extends RecursiveTask>> { */ Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> 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> oneElems = new HashSet<>(); oneElems.addAll(topLevelSets.stream() @@ -846,11 +846,19 @@ public class TypeUnifyTask extends RecursiveTask>> { i++; Set> elems = new HashSet>(oneElems); writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n"); + + //Ergebnisvariable für den aktuelle Thread Set> res = new HashSet<>(); + + //Menge der Ergebnisse der geforkten Threads Set>> add_res = new HashSet<>(); + + Set> 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>> { 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 forks = new HashSet<>(); Set newEqOrig = new HashSet<>(eq); @@ -931,11 +944,14 @@ public class TypeUnifyTask extends RecursiveTask>> { 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>> { 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>> { }; } //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>> { return result; } + protected Boolean newCheckA(Set a, Set sameEqSet, Set> result) { + + //optAPair enthaelt ggf. das Paar a = ty' \in a + //unterscheidet sich von optOrigPair, da dort a = ty + Optional 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 localEq = new HashSet<>(); + Set 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> 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 localEq = new HashSet<>(); + Set 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> 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 sameEqSet, Set> elems, Set> result) { writeLog("checkA: " + aPair + "sameEqSet: " + sameEqSet); for (UnifyPair sameEq : sameEqSet) {