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

ckeckA druch checkNoContradiction ersetzt
This commit is contained in:
pl@gohorb.ba-horb.de 2021-01-14 15:29:06 +01:00
parent 163f0f3047
commit 95f48ffcb7

View File

@ -859,37 +859,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
/* Wenn bei (a \in theta) \in a zu Widerspruch in oneElems wird /* Wenn bei (a \in theta) \in a zu Widerspruch in oneElems wird
* a verworfen und zu nächstem Element von nextSetasList gegangen * a verworfen und zu nächstem Element von nextSetasList gegangen
*/ */
if (!oderConstraint && !sameEqSet.isEmpty()) { if (!oderConstraint && !sameEqSet.isEmpty() && !checkNoContradiction(a, sameEqSet, result)) {
//optAPair enthaelt ggf. das Paar a = ty' \in a a = null;
//unterscheidet sich von optOrigPair, da dort a = ty noShortendElements++;
Optional<UnifyPair> optAPair = a.stream().filter(x -> ( continue;
//x.getBasePair() != null && ist gegeben wenn variance != 2
//x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT) &&
(x.getPairOp().equals(PairOperator.EQUALSDOT)
/*
(x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))
|| (x.getBasePair().getRhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getRhsType())
*/
))).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("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());
}
} }
/* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread /* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread
@ -923,38 +896,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
writeLog("1 RM" + nSaL.toString()); writeLog("1 RM" + nSaL.toString());
} }
/* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ if (!oderConstraint) {
if (!oderConstraint) {//weiss nicht ob das wirklich stimmt //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht
Optional<UnifyPair> optAPair = nSaL.stream().filter(x -> ( if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) {
//x.getBasePair() != null && ist gegeben wenn variance != 2 nSaL = null;
//x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT) && noShortendElements++;
(x.getPairOp().equals(PairOperator.EQUALSDOT) continue;
/*
(x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))
|| (x.getBasePair().getRhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getRhsType())
*/
))).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("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 */
else { else {
nextSetasListOderConstraints.add(((Constraint<UnifyPair>)nSaL).getExtendConstraint()); nextSetasListOderConstraints.add(((Constraint<UnifyPair>)nSaL).getExtendConstraint());
} }
@ -1046,38 +995,14 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
writeLog("-1 RM" + nSaL.toString()); writeLog("-1 RM" + nSaL.toString());
} }
if (!oderConstraint) {//weiss nicht ob das wirklich stimmt if (!oderConstraint) {
/* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht
Optional<UnifyPair> optAPair = nSaL.stream().filter(x -> ( if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) {
//x.getBasePair() != null && ist gegeben wenn variance != 2 nSaL = null;
//x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT) && noShortendElements++;
(x.getPairOp().equals(PairOperator.EQUALSDOT) continue;
/*
(x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))
|| (x.getBasePair().getRhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getRhsType())
*/
))).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("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 */
else { else {
nextSetasListOderConstraints.add(((Constraint<UnifyPair>)nSaL).getExtendConstraint()); nextSetasListOderConstraints.add(((Constraint<UnifyPair>)nSaL).getExtendConstraint());
} }
@ -1560,7 +1485,15 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
return result; return result;
} }
protected Boolean newCheckA(Set<UnifyPair> a, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> result) { /**
* checks if there is for (a = ty) \in a in sameEqSet a constradiction
* @param a Set of actual element of constraints with a =. ty \in a
* @param sameEqSet Set of constraints where a <. ty' and ty' <. a
* @param result set of results which contains correct solution s and the
* the error constraints. Error constraints are added
* @result contradiction of (a = ty) in sameEqSet
*/
protected Boolean checkNoContradiction(Set<UnifyPair> a, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> result) {
//optAPair enthaelt ggf. das Paar a = ty' \in a //optAPair enthaelt ggf. das Paar a = ty' \in a
//unterscheidet sich von optOrigPair, da dort a = ty //unterscheidet sich von optOrigPair, da dort a = ty
@ -1620,49 +1553,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
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) {
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;
}
protected boolean couldBecorrect(Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set<UnifyPair> nextElem) { protected boolean couldBecorrect(Set<Pair<Set<UnifyPair>, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set<UnifyPair> nextElem) {
return reducedUndefResSubstGroundedBasePair.stream() return reducedUndefResSubstGroundedBasePair.stream()