From fec83c3a6261bf1ef2e09f91dce4b6046d04e9dc Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Tue, 12 Jan 2021 21:27:44 +0100 Subject: [PATCH 1/6] modified: src/main/java/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java Fuer den Receiver wieder = eingefuegt. modified: src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java Kommentierung begonnen --- .../typeinference/typeAlgo/TYPEStmt.java | 10 ++-- .../typeinference/unify/TypeUnifyTask.java | 48 ++++++++++++------- 2 files changed, 38 insertions(+), 20 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java b/src/main/java/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java index c3c23079..b557e211 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/typeAlgo/TYPEStmt.java @@ -587,9 +587,13 @@ public class TYPEStmt implements StatementVisitor{ */ RefTypeOrTPHOrWildcardOrGeneric retType = assumption.getReceiverType(resolver); - methodConstraint.add(forMethod.name.equals("apply") ? //PL 2019-11-29: Tenaerer Operator eingefügt, weil bei Lambda-Ausdrücken keine Suntype FunN$$ existiert - new Pair(forMethod.receiver.getType(), retType, PairOperator.EQUALSDOT) - : new Pair(forMethod.receiver.getType(), retType, PairOperator.SMALLERDOT)); + methodConstraint.add(new Pair(forMethod.receiver.getType(), retType, + PairOperator.EQUALSDOT));//PL 2020-03-17 SMALLERDOT in EQUALSDOT umgewandelt, weil alle geerbten Methoden in den jeweilen Klassen enthalten sind. + + //Fuer Bytecodegenerierung PL 2020-03-09 wird derzeit nicht benutzt ANFANG + //methodConstraint.add(new Pair(forMethod.receiverType, retType, + // PairOperator.EQUALSDOT)); + //Fuer Bytecodegenerierung PL 2020-03-09 wird derzeit nicht benutzt ENDE methodConstraint.add(new Pair(assumption.getReturnType(resolver), forMethod.getType(), PairOperator.EQUALSDOT)); diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 6de6b9de..66ceb6d0 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -457,7 +457,7 @@ public class TypeUnifyTask extends RecursiveTask>> { //Aufruf von computeCartesianRecursive ANFANG //writeLog("topLevelSets: " + topLevelSets.toString()); - return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult); + return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult); } @@ -587,10 +587,21 @@ public class TypeUnifyTask extends RecursiveTask>> { } - - Set> computeCartesianRecursive(Set> fstElems, ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) { + /** + * Computes the cartesian product of topLevelSets step by step. + * @param topLevelSets List of Sets of Sets, where a cartesian product have to be built + * Ex.: [{{a =. Integer}, {a = Object}}, {{a = Vector, b =. Integer}, {a = Vector, b =. Object}}] + * @param eq Original set of equations which should be unified + * @param oderConstraints Remaining or-constraints + * @param fc The finite closure + * @param parallel If the algorithm should be parallelized run + * @param rekTiefe Deep of recursive calls + * @param finalresult Gives if unify is not called from checkA + * @return The set of all principal type unifiers + */ + Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) { //ArrayList>> remainingSets = new ArrayList<>(topLevelSets); - + Set> fstElems = new HashSet<>(); fstElems.addAll(topLevelSets.stream() .filter(x -> x.size()==1) .map(y -> y.stream().findFirst().get()) @@ -617,6 +628,12 @@ public class TypeUnifyTask extends RecursiveTask>> { Set> result = new HashSet<>(); int variance = 0; + /* Varianzbestimmung Anfang + * Oderconstraint, wenn entweder kein Basepair oder unterschiedliche Basepairs => oderConstraint = true; + * Varianz = 1 => Argumentvariable + * Varianz = -1 => Rückgabevariable + * Varianz = 0 => unklar + * Varianz = 2 => Operatoren oderConstraints */ ArrayList zeroNextElem = new ArrayList<>(nextSetasList.get(0)); UnifyPair fstBasePair = zeroNextElem.remove(0).getBasePair(); Boolean oderConstraint = false; @@ -639,16 +656,15 @@ public class TypeUnifyTask extends RecursiveTask>> { } } else { - //variance = 2; oderConstraint = true; } } else { - //variance = 2; oderConstraint = true; } - if (oderConstraint) {//Varianz-Bestimmung Oder-Constraints + //Varianz-Bestimmung Oder-Constraints + if (oderConstraint) { if (printtag) System.out.println("nextSetasList " + nextSetasList); Optional optVariance = nextSetasList.iterator() @@ -661,20 +677,18 @@ public class TypeUnifyTask extends RecursiveTask>> { ((PlaceholderType)x.getGroundBasePair().getLhsType()).getVariance()) .findAny(); //Fuer Operatorenaufrufe wird variance auf 2 gesetzt. - //da kein Receiver existiert also keon x.getGroundBasePair().getLhsType() instanceof PlaceholderType - //Es werden alle Elemente des Kartesischen Produkts abgearbeitet + //da kein Receiver existiert also kein x.getGroundBasePair().getLhsType() instanceof PlaceholderType + //Bei Varianz = 2 werden alle Elemente des Kartesischen Produkts abgearbeitet variance = optVariance.isPresent() ? optVariance.get() : 2; } + /* Varianzbestimmung Ende */ - if (!nextSetasList.iterator().hasNext()) - System.out.print(""); - if (nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("D")).findFirst().isPresent() && nextSetasList.size()>1) - System.out.print(""); //writeLog("nextSetasList: " + nextSetasList.toString()); Set nextSetElem = nextSetasList.get(0); //writeLog("BasePair1: " + nextSetElem + " " + nextSetElem.iterator().next().getBasePair()); - /* sameEqSet-Bestimmung: Wenn a = ty \in nextSet dann enthaelt sameEqSet alle Paare a < ty1 oder ty2 < a aus fstElems */ + /* sameEqSet-Bestimmung: Wenn a = ty \in nextSet dann enthaelt sameEqSet + * alle Paare a < ty1 oder ty2 < a aus fstElems */ Set sameEqSet = new HashSet<>(); Optional optOrigPair = null; //if (variance != 2) { @@ -710,14 +724,14 @@ public class TypeUnifyTask extends RecursiveTask>> { /* sameEqSet-Bestimmung Ende */ Set a = null; - while (nextSetasList.size() > 0) { //(nextSetasList.size() != 0) { + while (nextSetasList.size() > 0) { Set a_last = a; - //Liste der Faelle für die parallele Verarbeitung + //Liste der Faelle für die parallele Verarbeitung List> nextSetasListRest = new ArrayList<>(); //Liste der Faelle, bei dem Receiver jeweils "? extends" enthaelt bzw. nicht enthaelt - //In der Regel ein Element + //In der Regel is dies ein Element List> nextSetasListOderConstraints = new ArrayList<>(); writeLog("nextSet: " + nextSet.toString()); From e00d76ce3b1cdfdf12997e05b726a35c1fcd4400 Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Wed, 13 Jan 2021 19:39:01 +0100 Subject: [PATCH 2/6] Occurs-Check mit Abbruch eingebaut finalResult zum Attribut der Klasse gemacht --- .../typeinference/unify/RuleSet.java | 2 +- .../typeinference/unify/TypeUnify2Task.java | 2 +- .../typeinference/unify/TypeUnifyTask.java | 59 ++++++++++++++----- src/test/java/AllgemeinTest.java | 3 +- 4 files changed, 47 insertions(+), 19 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java index 93f33d08..50ea9a2e 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/RuleSet.java @@ -655,7 +655,6 @@ public class RuleSet implements IRuleSet{ else t1.getTypeParams().forEach(x -> occuringTypes.push(x)); } - Queue result1 = new LinkedList(pairs); ArrayList result = new ArrayList(); boolean applied = false; @@ -669,6 +668,7 @@ public class RuleSet implements IRuleSet{ && 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. diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java index 798c6f05..317f3660 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java @@ -34,7 +34,7 @@ public class TypeUnify2Task extends TypeUnifyTask { System.out.println("two"); } one = true; - Set> res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField, true); + Set> res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField); /*if (isUndefinedPairSetSet(res)) { return new HashSet<>(); } else diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 66ceb6d0..580fee5c 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -110,6 +110,9 @@ public class TypeUnifyTask extends RecursiveTask>> { protected boolean parallel; + //Gives if unify is not called from checkA + private boolean finalresult = true; + int rekTiefeField; Integer nOfUnify = 0; @@ -257,7 +260,7 @@ public class TypeUnifyTask extends RecursiveTask>> { ArrayList>> remainingOderconstraints = oderConstraintsField.stream() .filter(x -> x.size()>1) .collect(Collectors.toCollection(ArrayList::new)); - Set> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField, true); + Set> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField); noOfThread--; try { logFile.close(); @@ -299,7 +302,7 @@ public class TypeUnifyTask extends RecursiveTask>> { * @param fc The finite closure * @return The set of all principal type unifiers */ - protected Set> unify(final Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) { + protected Set> unify(final Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) { //Set aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT) // ).collect(Collectors.toCollection(HashSet::new)); //writeLog(nOfUnify.toString() + " AA: " + aas.toString()); @@ -308,9 +311,7 @@ public class TypeUnifyTask extends RecursiveTask>> { //} //.collect(Collectors.toCollection(HashSet::new))); - /* - * Step 1: Repeated application of reduce, adapt, erase, swap - */ + synchronized (usedTasks) { if (this.myIsCancelled()) { return new HashSet<>(); @@ -339,6 +340,29 @@ public class TypeUnifyTask extends RecursiveTask>> { return ret; } + /* + * Occurs-Check durchfuehren + */ + + Set ocurrPairs = eq.stream().filter(x -> { + UnifyType lhs, rhs; + return (lhs = x.getLhsType()) instanceof PlaceholderType + && !((rhs = x.getRhsType()) instanceof PlaceholderType) + && rhs.getTypeParams().occurs((PlaceholderType)lhs);}) + .map(x -> { x.setUndefinedPair(); return x;}) + .collect(Collectors.toCollection(HashSet::new)); + writeLog("ocurrPairs: " + ocurrPairs); + if (ocurrPairs.size() > 0) { + Set> ret = new HashSet<>(); + ret.add(ocurrPairs); + return ret; + } + + + + /* + * Step 1: Repeated application of reduce, adapt, erase, swap + */ Set eq0; Set eq0Prime; Optional> eqSubst = Optional.of(eq); @@ -457,12 +481,12 @@ public class TypeUnifyTask extends RecursiveTask>> { //Aufruf von computeCartesianRecursive ANFANG //writeLog("topLevelSets: " + topLevelSets.toString()); - return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult); + return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe); } - Set> unify2(Set> setToFlatten, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) { + Set> unify2(Set> setToFlatten, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) { //Aufruf von computeCartesianRecursive ENDE //keine Ahnung woher das kommt @@ -551,12 +575,12 @@ public class TypeUnifyTask extends RecursiveTask>> { } } else if(eqPrimePrime.isPresent()) { - Set> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe, finalresult); + Set> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe); eqPrimePrimeSet.addAll(unifyres); } else { - Set> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe, finalresult); + Set> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe); eqPrimePrimeSet.addAll(unifyres); @@ -596,10 +620,9 @@ public class TypeUnifyTask extends RecursiveTask>> { * @param fc The finite closure * @param parallel If the algorithm should be parallelized run * @param rekTiefe Deep of recursive calls - * @param finalresult Gives if unify is not called from checkA * @return The set of all principal type unifiers */ - Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) { + Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) { //ArrayList>> remainingSets = new ArrayList<>(topLevelSets); Set> fstElems = new HashSet<>(); fstElems.addAll(topLevelSets.stream() @@ -610,7 +633,7 @@ public class TypeUnifyTask extends RecursiveTask>> { .filter(x -> x.size()>1) .collect(Collectors.toCollection(ArrayList::new)); if (remainingSets.isEmpty()) {//Alle Elemente sind 1-elementig - Set> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe, finalresult); + Set> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe); return result; } Set> nextSet = remainingSets.remove(0); @@ -1173,7 +1196,7 @@ public class TypeUnifyTask extends RecursiveTask>> { } else { //parallel = false; //Wenn MaxNoOfThreads erreicht ist, 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, finalresult); + res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe); }}} if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) { //wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen @@ -1523,7 +1546,9 @@ public class TypeUnifyTask extends RecursiveTask>> { unitedSubst.addAll(sameEq.getAllSubstitutions()); unitedSubst.addAll(sameEq.getAllBases()); localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); - Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false); + finalresult = false; + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0); + finalresult = true; if (isUndefinedPairSetSet(localRes)) { if (result.isEmpty() || isUndefinedPairSetSet(result)) { result.addAll(localRes); @@ -1539,7 +1564,9 @@ public class TypeUnifyTask extends RecursiveTask>> { unitedSubst.addAll(sameEq.getAllSubstitutions()); unitedSubst.addAll(sameEq.getAllBases()); localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); - Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false); + finalresult = false; + Set> localRes = unify(localEq, new ArrayList<>(), fc, false, 0); + finalresult = true; if (isUndefinedPairSetSet(localRes)) { if (result.isEmpty() || isUndefinedPairSetSet(result)) { result.addAll(localRes); @@ -2519,7 +2546,7 @@ public class TypeUnifyTask extends RecursiveTask>> { void writeLog(String str) { synchronized ( this ) { - if (log) { + if (log && finalresult) { try { logFile.write("Thread no.:" + thNo + "\n"); logFile.write("noOfThread:" + noOfThread + "\n"); diff --git a/src/test/java/AllgemeinTest.java b/src/test/java/AllgemeinTest.java index c937035e..50a67b38 100644 --- a/src/test/java/AllgemeinTest.java +++ b/src/test/java/AllgemeinTest.java @@ -40,7 +40,8 @@ public class AllgemeinTest { //String className = "FCTest3"; //String className = "Var"; //String className = "Put"; - String className = "Twice"; + //String className = "Twice"; + String className = "TestSubTypless"; //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"; From d8ac25234fa58ca0fb1d7de5da6a5f49f2d5787c Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Thu, 14 Jan 2021 10:38:32 +0100 Subject: [PATCH 3/6] modified: ../src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java vor entfernung von Remaining --- .../typeinference/unify/TypeUnifyTask.java | 43 +++++++++++-------- 1 file changed, 25 insertions(+), 18 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 580fee5c..a2667a85 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -623,15 +623,20 @@ public class TypeUnifyTask extends RecursiveTask>> { * @return The set of all principal type unifiers */ Set> computeCartesianRecursive(ArrayList>> topLevelSets, Set eq, List>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) { - //ArrayList>> remainingSets = new ArrayList<>(topLevelSets); + + //fstElems: Alle 1-elementigen Mengen, die nur ein Paar + //a <. theta, theta <. a oder a =. theta enthalten Set> fstElems = new HashSet<>(); fstElems.addAll(topLevelSets.stream() .filter(x -> x.size()==1) .map(y -> y.stream().findFirst().get()) .collect(Collectors.toCollection(HashSet::new))); + + //remainingSets: Alle mehrelementigen Mengen ArrayList>> remainingSets = topLevelSets.stream() .filter(x -> x.size()>1) .collect(Collectors.toCollection(ArrayList::new)); + writeLog("Anzahl der Elemente von Remaining: " + remainingSets.size()); if (remainingSets.isEmpty()) {//Alle Elemente sind 1-elementig Set> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe); return result; @@ -713,8 +718,9 @@ public class TypeUnifyTask extends RecursiveTask>> { /* sameEqSet-Bestimmung: Wenn a = ty \in nextSet dann enthaelt sameEqSet * alle Paare a < ty1 oder ty2 < a aus fstElems */ Set sameEqSet = new HashSet<>(); + + //optOrigPair enthaelt ggf. das Paar a = ty \in nextSet Optional optOrigPair = null; - //if (variance != 2) { if (!oderConstraint) { optOrigPair = nextSetElem.stream().filter(x -> ( //x.getBasePair() != null && ist gegeben wenn variance != 2 @@ -750,11 +756,18 @@ public class TypeUnifyTask extends RecursiveTask>> { while (nextSetasList.size() > 0) { Set a_last = a; - //Liste der Faelle für die parallele Verarbeitung + /* Liste der Faelle für die parallele Verarbeitung + * Enthaelt Elemente, die nicht in Relation zu aktuellem Fall in der + * Variablen a stehen. Diese muesse auf alle Faelle bearbeitet werden, + * Deshalb wird ihre Berechnung parallel angestossen. + */ List> nextSetasListRest = new ArrayList<>(); - //Liste der Faelle, bei dem Receiver jeweils "? extends" enthaelt bzw. nicht enthaelt - //In der Regel is dies ein Element + /* Liste der Faelle, bei dem Receiver jeweils "? extends" enthaelt bzw. nicht enthaelt + * In der Regel ist dies genau ein Element + * Dieses Element wird später aus nextSetasList geloescht, wenn das jeweils andere Element zum Erfolg + * gefuehrt hat. + */ List> nextSetasListOderConstraints = new ArrayList<>(); writeLog("nextSet: " + nextSet.toString()); @@ -777,6 +790,7 @@ public class TypeUnifyTask extends RecursiveTask>> { } //Alle maximale Elemente in nextSetasListRest bestimmen + //nur für diese wird parallele Berechnung angestossen. nextSetasListRest = oup.maxElements(nextSetasListRest); } else if (variance == -1) { @@ -797,10 +811,13 @@ public class TypeUnifyTask extends RecursiveTask>> { } } //Alle minimalen Elemente in nextSetasListRest bestimmen + //nur für diese wird parallele Berechnung angestossen. nextSetasListRest = oup.minElements(nextSetasListRest); } else if (variance == 2) { a = nextSetasList.remove(0); + + //Fuer alle Elemente wird parallele Berechnung angestossen. nextSetasListRest = new ArrayList<>(nextSetasList); } else if (variance == 0) { @@ -826,20 +843,10 @@ public class TypeUnifyTask extends RecursiveTask>> { } } } - //writeLog("nextSet: " + nextSetasList.toString()+ "\n"); - //nextSetasList.remove(a); - //PL 2018-03-01 - //TODO: 1. Maximum und Minimum unterscheiden - //TODO: 2. compare noch für alle Elmemente die nicht X =. ty sind erweitern - //for(Set a : newSet) { i++; Set> elems = new HashSet>(fstElems); writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n"); - //elems.add(a); PL 2019-01-20 Muss weg, weil das in jeweiligen Thread erfolgen muss. Fuer den sequentiellen Fall - //im else-Zweig - //if (remainingSets.isEmpty()) {//muss immer gegeben sein, weil nur 1 Element der topLevelSets mehr als ein Elemet enthaelt - //writeLog("Vor unify2 Aufruf: " + elems.toString()); Set> res = new HashSet<>(); Set>> add_res = new HashSet<>(); Set> aParDef = new HashSet<>(); @@ -1553,7 +1560,7 @@ public class TypeUnifyTask extends RecursiveTask>> { if (result.isEmpty() || isUndefinedPairSetSet(result)) { result.addAll(localRes); } - //writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); + writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); return false; } } @@ -1571,12 +1578,12 @@ public class TypeUnifyTask extends RecursiveTask>> { if (result.isEmpty() || isUndefinedPairSetSet(result)) { result.addAll(localRes); } - //writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); + writeLog("FALSE: " + aPair + "sameEqSet: " + sameEqSet); return false; } } } - //writeLog("TRUE: " + aPair + "sameEqSet: " + sameEqSet); + writeLog("TRUE: " + aPair + "sameEqSet: " + sameEqSet); return true; } From 1cf22d2602206e8421d1e45e4c4bcc7deabdc717 Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Thu, 14 Jan 2021 11:27:19 +0100 Subject: [PATCH 4/6] modified: ../src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java remaingSet entfernt fstElems in oneElems umbenannt --- .../typeinference/unify/TypeUnifyTask.java | 35 +++++++++---------- 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index a2667a85..aa2e25a0 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -626,22 +626,21 @@ public class TypeUnifyTask extends RecursiveTask>> { //fstElems: Alle 1-elementigen Mengen, die nur ein Paar //a <. theta, theta <. a oder a =. theta enthalten - Set> fstElems = new HashSet<>(); - fstElems.addAll(topLevelSets.stream() + Set> oneElems = new HashSet<>(); + oneElems.addAll(topLevelSets.stream() .filter(x -> x.size()==1) .map(y -> y.stream().findFirst().get()) .collect(Collectors.toCollection(HashSet::new))); - //remainingSets: Alle mehrelementigen Mengen - ArrayList>> remainingSets = topLevelSets.stream() - .filter(x -> x.size()>1) - .collect(Collectors.toCollection(ArrayList::new)); - writeLog("Anzahl der Elemente von Remaining: " + remainingSets.size()); - if (remainingSets.isEmpty()) {//Alle Elemente sind 1-elementig - Set> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe); + //optNextSet: Eine mehrelementige Menge, wenn vorhanden + Optional>> optNextSet = topLevelSets.stream().filter(x -> x.size()>1).findAny(); + + if (!optNextSet.isPresent()) {//Alle Elemente sind 1-elementig + Set> result = unify2(oneElems, eq, oderConstraints, fc, parallel, rekTiefe); return result; } - Set> nextSet = remainingSets.remove(0); + + Set> nextSet = optNextSet.get(); //writeLog("nextSet: " + nextSet.toString()); List> nextSetasList =new ArrayList<>(nextSet); /* @@ -716,7 +715,7 @@ public class TypeUnifyTask extends RecursiveTask>> { //writeLog("BasePair1: " + nextSetElem + " " + nextSetElem.iterator().next().getBasePair()); /* sameEqSet-Bestimmung: Wenn a = ty \in nextSet dann enthaelt sameEqSet - * alle Paare a < ty1 oder ty2 < a aus fstElems */ + * alle Paare a < ty1 oder ty2 < a aus oneElems */ Set sameEqSet = new HashSet<>(); //optOrigPair enthaelt ggf. das Paar a = ty \in nextSet @@ -744,7 +743,7 @@ public class TypeUnifyTask extends RecursiveTask>> { tyVar = origPair.getRhsType(); } UnifyType tyVarEF = tyVar; - sameEqSet = fstElems.stream().map(xx -> xx.iterator().next()) + sameEqSet = oneElems.stream().map(xx -> xx.iterator().next()) .filter(x -> (((x.getLhsType().equals(tyVarEF) && !(x.getRhsType() instanceof PlaceholderType)) || (x.getRhsType().equals(tyVarEF) && !(x.getLhsType() instanceof PlaceholderType))))) .collect(Collectors.toCollection(HashSet::new)); @@ -845,7 +844,7 @@ public class TypeUnifyTask extends RecursiveTask>> { } i++; - Set> elems = new HashSet>(fstElems); + Set> elems = new HashSet>(oneElems); writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n"); Set> res = new HashSet<>(); Set>> add_res = new HashSet<>(); @@ -853,6 +852,8 @@ public class TypeUnifyTask extends RecursiveTask>> { /* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ if (!oderConstraint && !sameEqSet.isEmpty()) { + //optAPair enthaelt ggf. das Paar a = ty' \in a + //unterscheidet sich von optOrigPair, da dort a = ty Optional optAPair = a.stream().filter(x -> ( //x.getBasePair() != null && ist gegeben wenn variance != 2 //x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT) && @@ -871,7 +872,7 @@ public class TypeUnifyTask extends RecursiveTask>> { 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); + writeLog("variance: " + variance + "sameEqSet:" + sameEqSet); if (!checkA(aPair, sameEqSet, elems, result)) { a = null; noShortendElements++; @@ -1291,7 +1292,7 @@ public class TypeUnifyTask extends RecursiveTask>> { } else { //alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden - writeLog("RES Fst: reuslt: " + result.toString() + " res: " + res.toString()); + writeLog("RES Fst: result: " + result.toString() + " res: " + res.toString()); result.addAll(res); } } @@ -1303,10 +1304,6 @@ public class TypeUnifyTask extends RecursiveTask>> { //} } - //} - //else {//duerfte gar nicht mehr vorkommen PL 2018-04-03 - //result.addAll(computeCartesianRecursive(elems, remainingSets, eq, fc, parallel)); - //} if (parallel) { for (Set> par_res : add_res) { if (!isUndefinedPairSetSet(par_res) && isUndefinedPairSetSet(result)) { 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 5/6] 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 aa2e25a0..8377edd6 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) { From 95f48ffcb73ec7e1f938da7f9ac74e81c1ca3da1 Mon Sep 17 00:00:00 2001 From: "pl@gohorb.ba-horb.de" Date: Thu, 14 Jan 2021 15:29:06 +0100 Subject: [PATCH 6/6] modified: ../src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java ckeckA druch checkNoContradiction ersetzt --- .../typeinference/unify/TypeUnifyTask.java | 160 +++--------------- 1 file changed, 25 insertions(+), 135 deletions(-) diff --git a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 8377edd6..5abacf70 100644 --- a/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -859,37 +859,10 @@ public class TypeUnifyTask extends RecursiveTask>> { /* 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 - Optional optAPair = a.stream().filter(x -> ( - //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()); - } + if (!oderConstraint && !sameEqSet.isEmpty() && !checkNoContradiction(a, sameEqSet, result)) { + a = null; + noShortendElements++; + continue; } /* Wenn parallel gearbeitet wird, wird je nach Varianz ein neuer Thread @@ -923,38 +896,14 @@ public class TypeUnifyTask extends RecursiveTask>> { writeLog("1 RM" + nSaL.toString()); } - /* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ - if (!oderConstraint) {//weiss nicht ob das wirklich stimmt - Optional optAPair = nSaL.stream().filter(x -> ( - //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: " + 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()); + if (!oderConstraint) { + //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht + if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) { + nSaL = null; + noShortendElements++; + continue; } } - /* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ else { nextSetasListOderConstraints.add(((Constraint)nSaL).getExtendConstraint()); } @@ -1046,38 +995,14 @@ public class TypeUnifyTask extends RecursiveTask>> { writeLog("-1 RM" + nSaL.toString()); } - if (!oderConstraint) {//weiss nicht ob das wirklich stimmt - /* PL 2019-03-13 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ - Optional optAPair = nSaL.stream().filter(x -> ( - //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: " + 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()); + if (!oderConstraint) { + //ueberpruefung ob zu a =. ty \in nSaL in sameEqSet ein Widerspruch besteht + if (!sameEqSet.isEmpty() && !checkNoContradiction(nSaL, sameEqSet, result)) { + nSaL = null; + noShortendElements++; + continue; } } - /* PL 2019-03-13 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */ else { nextSetasListOderConstraints.add(((Constraint)nSaL).getExtendConstraint()); } @@ -1560,7 +1485,15 @@ public class TypeUnifyTask extends RecursiveTask>> { return result; } - protected Boolean newCheckA(Set a, Set sameEqSet, Set> 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 a, Set sameEqSet, Set> result) { //optAPair enthaelt ggf. das Paar a = ty' \in a //unterscheidet sich von optOrigPair, da dort a = ty @@ -1620,49 +1553,6 @@ public class TypeUnifyTask extends RecursiveTask>> { return true; } - protected Boolean checkA (UnifyPair aPair, Set sameEqSet, Set> elems, Set> result) { - 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; - } protected boolean couldBecorrect(Set, UnifyPair>> reducedUndefResSubstGroundedBasePair, Set nextElem) { return reducedUndefResSubstGroundedBasePair.stream()