i21017/JavaCompilerCore
1
0
Fork 0
forked from JavaTX/JavaCompilerCore
Code Pull Requests Activity

modified: ../../../main/java/de/dhbwstuttgart/core/JavaTXCompiler.java

Browse Source 
modified:   ../../../main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
	modified:   ../../../main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
Die Ueberpruefung von a bzw. nSaL in Methode checkA ausgelagert und für die Faelle a <. th und ty <. a implementiert.
This commit is contained in:
Martin Plümicke 2019-03-14 00:20:19 +01:00
parent 75adbaf579
commit 44ed1d8e8d
4 changed files with 315 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/main/java/de/dhbwstuttgart/core/JavaTXCompiler.java
View File

@ -52,7 +52,7 @@ import org.antlr.v4.parse.ANTLRParser.throwsSpec_return;
public class JavaTXCompiler { public class JavaTXCompiler {
final CompilationEnvironment environment; final CompilationEnvironment environment;
Boolean resultmodel = false; Boolean resultmodel = true;
public final Map<File, SourceFile> sourceFiles = new HashMap<>(); public final Map<File, SourceFile> sourceFiles = new HashMap<>();
Boolean log = true; //gibt an ob ein Log-File nach System.getProperty("user.dir")+"src/test/java/logFiles" geschrieben werden soll? Boolean log = true; //gibt an ob ein Log-File nach System.getProperty("user.dir")+"src/test/java/logFiles" geschrieben werden soll?
@ -551,8 +551,8 @@ public class JavaTXCompiler {
} }
/* UnifyResultModel End */ /* UnifyResultModel End */
else { else {
//Set<Set<UnifyPair>> result = unify.unify(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure)); Set<Set<UnifyPair>> result = unify.unify(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure)); //Set<Set<UnifyPair>> result = unify.unifyOderConstraints(unifyCons.getUndConstraints(), oderConstraints, finiteClosure, logFile, log, new UnifyResultModel(cons, finiteClosure));
System.out.println("RESULT: " + result); System.out.println("RESULT: " + result);
logFile.write("RES: " + result.toString()+"\n"); logFile.write("RES: " + result.toString()+"\n");
logFile.flush(); logFile.flush();

22
src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
View File

@ -1,6 +1,7 @@
package de.dhbwstuttgart.typeinference.unify; package de.dhbwstuttgart.typeinference.unify;
import java.io.FileWriter; import java.io.FileWriter;
import java.io.IOException;
import java.io.Writer; import java.io.Writer;
import java.util.List; import java.util.List;
import java.util.Set; import java.util.Set;
@ -30,6 +31,13 @@ public class TypeUnify {
ForkJoinPool pool = new ForkJoinPool(); ForkJoinPool pool = new ForkJoinPool();
pool.invoke(unifyTask); pool.invoke(unifyTask);
Set<Set<UnifyPair>> res = unifyTask.join(); Set<Set<UnifyPair>> res = unifyTask.join();
try {
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements + "\n");
logFile.flush();
}
catch (IOException e) {
System.err.println("no log-File");
}
return res; return res;
} }
@ -67,6 +75,13 @@ public class TypeUnify {
ForkJoinPool pool = new ForkJoinPool(); ForkJoinPool pool = new ForkJoinPool();
pool.invoke(unifyTask); pool.invoke(unifyTask);
Set<Set<UnifyPair>> res = unifyTask.join(); Set<Set<UnifyPair>> res = unifyTask.join();
try {
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
logFile.flush();
}
catch (IOException e) {
System.err.println("no log-File");
}
return ret; return ret;
} }
@ -91,6 +106,13 @@ public class TypeUnify {
public Set<Set<UnifyPair>> unifyOderConstraints(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret) { public Set<Set<UnifyPair>> unifyOderConstraints(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, Writer logFile, Boolean log, UnifyResultModel ret) {
TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, ret); TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, ret);
Set<Set<UnifyPair>> res = unifyTask.compute(); Set<Set<UnifyPair>> res = unifyTask.compute();
try {
logFile.write("\nnoShortendElements: " + unifyTask.noShortendElements +"\n");
logFile.flush();
}
catch (IOException e) {
System.err.println("no log-File");
}
return res; return res;
} }

317
src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
View File

@ -115,6 +115,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
static int noBacktracking; static int noBacktracking;
Integer noShortendElements = 0;
public TypeUnifyTask() { public TypeUnifyTask() {
rules = new RuleSet(); rules = new RuleSet();
} }
@ -293,6 +295,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
} while (eqSubst.isPresent()); } while (eqSubst.isPresent());
eq0.forEach(x -> x.disableCondWildcards()); eq0.forEach(x -> x.disableCondWildcards());
writeLog(nOfUnify.toString() + " Unifikation nach applyTypeUnificationRules: " + eq.toString());
writeLog(nOfUnify.toString() + " Oderconstraints nach applyTypeUnificationRules: " + oderConstraints.toString());
/* /*
* Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs
@ -339,21 +344,16 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
if (printtag) System.out.println("eq2s " + eq2s); if (printtag) System.out.println("eq2s " + eq2s);
//writeLog("BufferSet: " + bufferSet.toString()+"\n"); //writeLog("BufferSet: " + bufferSet.toString()+"\n");
List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints); List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints);
Set<Set<UnifyPair>> collectErr = new HashSet<>(); Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput);
Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput, collectErr);
//PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer //PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer
//nicht ausgewertet Faculty Beispiel im 1. Schritt //nicht ausgewertet Faculty Beispiel im 1. Schritt
//PL 2017-10-03 geloest, muesste noch mit FCs mit kleineren //PL 2017-10-03 geloest, muesste noch mit FCs mit kleineren
//Typen getestet werden. //Typen getestet werden.
writeLog(nOfUnify.toString() + " Oderconstraints2: " + oderConstraintsOutput.toString()); writeLog(nOfUnify.toString() + " Oderconstraints2: " + oderConstraintsOutput.toString());
writeLog(nOfUnify.toString() + " collectErr: " + collectErr.toString());
if (printtag) System.out.println("secondLevelSets:" +secondLevelSets); if (printtag) System.out.println("secondLevelSets:" +secondLevelSets);
// If pairs occured that did not match one of the cartesian product cases, // If pairs occured that did not match one of the cartesian product cases,
// those pairs are contradictory and the unification is impossible. // those pairs are contradictory and the unification is impossible.
if(!undefinedPairs.isEmpty()) { if(!undefinedPairs.isEmpty()) {
Set<UnifyPair> flatCollectErr = new HashSet<>();
collectErr.forEach(x -> flatCollectErr.addAll(x));
undefinedPairs.addAll(flatCollectErr);
noUndefPair++; noUndefPair++;
for (UnifyPair up : undefinedPairs) { for (UnifyPair up : undefinedPairs) {
writeLog(noUndefPair.toString() + " UndefinedPairs; " + up); writeLog(noUndefPair.toString() + " UndefinedPairs; " + up);
@ -403,7 +403,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
//Aufruf von computeCartesianRecursive ANFANG //Aufruf von computeCartesianRecursive ANFANG
//writeLog("topLevelSets: " + topLevelSets.toString()); //writeLog("topLevelSets: " + topLevelSets.toString());
return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, collectErr, finalresult); return computeCartesianRecursive(new HashSet<>(), new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, finalresult);
} }
@ -527,7 +527,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<Set<Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set<Set<UnifyPair>> collectErr, Boolean finalresult) { Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<Set<Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Boolean finalresult) {
//ArrayList<Set<Set<UnifyPair>>> remainingSets = new ArrayList<>(topLevelSets); //ArrayList<Set<Set<UnifyPair>>> remainingSets = new ArrayList<>(topLevelSets);
fstElems.addAll(topLevelSets.stream() fstElems.addAll(topLevelSets.stream()
.filter(x -> x.size()==1) .filter(x -> x.size()==1)
@ -552,16 +552,35 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
} }
Set<Set<UnifyPair>> result = new HashSet<>(); Set<Set<UnifyPair>> result = new HashSet<>();
int variance = 0; int variance = 0;
Optional<Integer> xi = nextSetasList.stream().map(x -> x.stream().filter(y -> y.getLhsType() instanceof PlaceholderType)
.filter(z -> ((PlaceholderType)z.getLhsType()).getVariance() != 0) ArrayList<UnifyPair> zeroNextElem = new ArrayList<>(nextSetasList.get(0));
.map(c -> ((PlaceholderType)c.getLhsType()).getVariance()) UnifyPair fstBasePair = zeroNextElem.remove(0).getBasePair();
.reduce((a,b)-> {if (a==b) return a; else return 2; })) //2 kommt insbesondere bei Oder-Constraints vor
.filter(d -> d.isPresent()) if (fstBasePair != null) {
.map(e -> e.get()) Boolean sameBase = true;
.findAny(); for (UnifyPair ele : nextSetasList.get(0)) {//check ob a <. ty base oder ob Ueberladung
if (xi.isPresent()) { sameBase = sameBase && ele.getBasePair() != null && ele.getBasePair().equals(fstBasePair);
variance = xi.get(); }
} if (sameBase) {
Optional<Integer> xi = nextSetasList.stream().map(x -> x.stream().filter(y -> y.getLhsType() instanceof PlaceholderType)
.filter(z -> ((PlaceholderType)z.getLhsType()).getVariance() != 0)
.map(c -> ((PlaceholderType)c.getLhsType()).getVariance())
.reduce((a,b)-> {if (a==b) return a; else return 0; })) //2 kommt insbesondere bei Oder-Constraints vor
.filter(d -> d.isPresent())
.map(e -> e.get())
.findAny();
if (xi.isPresent()) {
variance = xi.get();
}
}
else {
variance = 2;
}
}
else {
variance = 2;
}
//if (variance == 1 && nextSetasList.size() > 1) { //if (variance == 1 && nextSetasList.size() > 1) {
// List<Set<UnifyPair>> al = new ArrayList<>(nextSetasList.size()); // List<Set<UnifyPair>> al = new ArrayList<>(nextSetasList.size());
// for (int ii = 0; ii < nextSetasList.size();ii++) { // for (int ii = 0; ii < nextSetasList.size();ii++) {
@ -592,6 +611,32 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
if (nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("D")).findFirst().isPresent() && nextSetasList.size()>1) if (nextSetasList.iterator().next().stream().filter(x -> x.getLhsType().getName().equals("D")).findFirst().isPresent() && nextSetasList.size()>1)
System.out.print(""); System.out.print("");
writeLog("nextSetasList: " + nextSetasList.toString()); writeLog("nextSetasList: " + nextSetasList.toString());
Set<UnifyPair> 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 */
Optional<UnifyPair> optOrigPair = nextSetElem.stream().filter(x -> (x.getBasePair() != null && 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())))
*/
)).findFirst();
Set<UnifyPair> sameEqSet = null;
if (optOrigPair.isPresent()) {
UnifyPair origPair = optOrigPair.get();
UnifyType tyVar;
if (!((tyVar = origPair.getLhsType()) instanceof PlaceholderType)) {
tyVar = origPair.getRhsType();
}
UnifyType tyVarEF = tyVar;
sameEqSet = fstElems.stream().map(xx -> xx.iterator().next())
.filter(x -> ((x.getLhsType().equals(tyVarEF) || x.getRhsType().equals(tyVarEF))))
.collect(Collectors.toCollection(HashSet::new));
}
/* sameEqSet-Bestimmung Ende */
Set<UnifyPair> a = null; Set<UnifyPair> a = null;
while (nextSetasList.size() > 0) { //(nextSetasList.size() != 0) { while (nextSetasList.size() > 0) { //(nextSetasList.size() != 0) {
Set<UnifyPair> a_last = a; Set<UnifyPair> a_last = a;
@ -699,6 +744,30 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Set<Set<UnifyPair>> res = new HashSet<>(); Set<Set<UnifyPair>> res = new HashSet<>();
Set<Set<Set<UnifyPair>>> add_res = new HashSet<>(); Set<Set<Set<UnifyPair>>> add_res = new HashSet<>();
Set<Set<UnifyPair>> aParDef = new HashSet<>(); Set<Set<UnifyPair>> aParDef = new HashSet<>();
/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
Optional<UnifyPair> optAPair = a.stream().filter(x -> (x.getBasePair() != null && 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())))
*/
)).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);
if (variance != 2 && !sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
a = null;
noShortendElements++;
continue;
}
}
/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) { if(parallel && (variance == 1) && noOfThread <= MaxNoOfThreads) {
Set<TypeUnify2Task> forks = new HashSet<>(); Set<TypeUnify2Task> forks = new HashSet<>();
Set<UnifyPair> newEqOrig = new HashSet<>(eq); Set<UnifyPair> newEqOrig = new HashSet<>(eq);
@ -721,6 +790,82 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
synchronized (this) { nextSetasList.remove(nSaL); synchronized (this) { nextSetasList.remove(nSaL);
writeLog("1 RM" + nSaL.toString()); writeLog("1 RM" + nSaL.toString());
} }
/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
&& ((x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))
|| (x.getBasePair().getRhsType() instanceof PlaceholderType
&& 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);
if (!sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
nSaL = null;
noShortendElements++;
continue;
}
}
/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
/* LOESCHEN, WENN KEINE FEHLER AUFTRETEN
optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null
&& x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))).findFirst();
if (optAPair.isPresent()) {
UnifyPair aPair = optAPair.get();
if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)) {
//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
// .filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
// .collect(Collectors.toCollection(HashSet::new));
//consideredElements.addAll(sameEqSet);
Boolean wrong = false;
writeLog("optOrigPair: " + optOrigPair + " " + "aPair: " + aPair+ " " + "aPair.basePair(): " + aPair.getBasePair());
writeLog("nSaL: " + nSaL + " " + nSaL.iterator().next().getBasePair());
for (UnifyPair sameEq : sameEqSet) {
//writeLog("x1 Original:\n" + x1.toString());
if (sameEq.getLhsType() instanceof PlaceholderType) {
//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
wrong = true;
break;
}
}
else {
//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
wrong = true;
break;
}
}
//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
}
if (wrong) {
nSaL = null;
noShortendElements++;
continue;
}
}}
*/
Set<UnifyPair> newEq = new HashSet<>(eq); Set<UnifyPair> newEq = new HashSet<>(eq);
Set<Set<UnifyPair>> newElems = new HashSet<>(elems); Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints); List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
@ -785,6 +930,81 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
synchronized (this) { nextSetasList.remove(nSaL); synchronized (this) { nextSetasList.remove(nSaL);
writeLog("-1 RM" + nSaL.toString()); writeLog("-1 RM" + nSaL.toString());
} }
/* PL 2019-03-11 Anfang eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null && x.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)
&& ((x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))
|| (x.getBasePair().getRhsType() instanceof PlaceholderType
&& 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);
if (variance != 2 && !sameEqSet.isEmpty() && !checkA(aPair, sameEqSet, elems, result)) {
nSaL = null;
noShortendElements++;
continue;
}
}
/* PL 2019-03-11 Ende eingefuegt Vergleich mit anderen Paaren ggf. loeschen */
/* LOESCHEN, WENN KEINE FEHLER AUFTRETEN
optAPair = nSaL.stream().filter(x -> (x.getBasePair() != null
&& x.getBasePair().getLhsType() instanceof PlaceholderType
&& x.getLhsType().equals(x.getBasePair().getLhsType()))).findFirst();
if (optAPair.isPresent()) {
UnifyPair aPair = optAPair.get();
if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT)) {
//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
// .filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
// .collect(Collectors.toCollection(HashSet::new));
//consideredElements.addAll(sameEqSet);
Boolean wrong = false;
for (UnifyPair sameEq : sameEqSet) {
//writeLog("x1 Original:\n" + x1.toString());
if (sameEq.getLhsType() instanceof PlaceholderType) {
//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
wrong = true;
break;
}
}
else {
//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
wrong = true;
break;
}
}
//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
}
if (wrong) {
nSaL = null;
noShortendElements++;
continue;
}
}}
*/
Set<UnifyPair> newEq = new HashSet<>(eq); Set<UnifyPair> newEq = new HashSet<>(eq);
Set<Set<UnifyPair>> newElems = new HashSet<>(elems); Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints); List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
@ -976,10 +1196,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
} }
else { else {
//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden //alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
writeLog("RES Fst:" + result.toString() + " " + res.toString() + " " + collectErr.toString()); writeLog("RES Fst:" + result.toString() + " " + res.toString());
if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result))) {//Wenn Fehlerfall: dann die Fehler aus calculatePairSets hinzufuegen
result.addAll(collectErr);
}
result.addAll(res); result.addAll(res);
} }
} }
@ -1010,9 +1227,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|| result.isEmpty()) { || result.isEmpty()) {
//alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden //alle Fehlerfaelle und alle korrekten Ergebnis jeweils adden
writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString()); writeLog("RES var1 ADD:" + result.toString() + " " + par_res.toString());
if ((isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result))) {//Wenn Fehlerfall: dann die Fehler aus calculatePairSets hinzufuegen
result.addAll(collectErr);
}
result.addAll(par_res); result.addAll(par_res);
} }
} }
@ -1229,6 +1443,51 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
return result; return result;
} }
protected Boolean checkA (UnifyPair aPair, Set<UnifyPair> sameEqSet, Set<Set<UnifyPair>> elems, Set<Set<UnifyPair>> result) {
//if (aPair.getBasePair().getPairOp().equals(PairOperator.SMALLERDOT))
//{
writeLog("checkA: " + aPair);
//Set<UnifyPair> sameEqSet = elems.stream().map(xx -> xx.iterator().next())
// .filter(x -> ((x.getLhsType().equals(aPair.getLhsType()) || x.getRhsType().equals(aPair.getLhsType()))))
// .collect(Collectors.toCollection(HashSet::new));
//consideredElements.addAll(sameEqSet);
Boolean wrong = false;
for (UnifyPair sameEq : sameEqSet) {
//writeLog("x1 Original:\n" + x1.toString());
if (sameEq.getLhsType() instanceof PlaceholderType) {
//UnifyPair type = a.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
return false;
}
}
else {
//UnifyPair type = y.stream().filter(z -> z.getLhsType().equals(lhsType)).findFirst().get();
Set<UnifyPair> localEq = new HashSet<>();
Set<UnifyPair> unitedSubst = new HashSet<>(aPair.getSubstitution());
unitedSubst.addAll(sameEq.getSubstitution());
localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, false);
if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) {
result.addAll(localRes);
}
return false;
}
}
//writeLog("x1 nach Loeschung von " + sameEq.toString()+" :\n" + x1.toString());
}
//}
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()
.map(pair -> { .map(pair -> {
@ -1502,7 +1761,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
* from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements
* (as in case 1 where sigma is added to the innermost set). * (as in case 1 where sigma is added to the innermost set).
*/ */
protected Set<Set<Set<Set<UnifyPair>>>> calculatePairSets(Set<UnifyPair> eq2s, List<Set<Set<UnifyPair>>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<Set<Set<UnifyPair>>> oderConstraintsOutput, Set<Set<UnifyPair>> collectErr) { protected Set<Set<Set<Set<UnifyPair>>>> calculatePairSets(Set<UnifyPair> eq2s, List<Set<Set<UnifyPair>>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<Set<Set<UnifyPair>>> oderConstraintsOutput) {
oderConstraintsOutput.addAll(oderConstraintsInput); oderConstraintsOutput.addAll(oderConstraintsInput);
List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9); List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9);
@ -1589,6 +1848,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
remElem.add(new UnifyPair(pair.getLhsType(), new SuperType(pair.getRhsType()), PairOperator.EQUALSDOT)); remElem.add(new UnifyPair(pair.getLhsType(), new SuperType(pair.getRhsType()), PairOperator.EQUALSDOT));
x1.remove(remElem); x1.remove(remElem);
} }
/* ZU LOESCHEN ANFANG
//System.out.println(x1); //System.out.println(x1);
Set<UnifyPair> sameEqSet = eq2sAsList.stream() Set<UnifyPair> sameEqSet = eq2sAsList.stream()
.filter(x -> ((x.getLhsType().equals(lhsType) || x.getRhsType().equals(lhsType)) && !x.equals(pair))) .filter(x -> ((x.getLhsType().equals(lhsType) || x.getRhsType().equals(lhsType)) && !x.equals(pair)))
@ -1651,7 +1911,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
x1ResPrime = x1Res; x1ResPrime = x1Res;
} }
result.get(0).add(x1ResPrime); result.get(0).add(x1ResPrime);
if (x1ResPrime.isEmpty()) { ZU LOESCHEN ENDE */
result.get(0).add(x1);
if (x1.isEmpty()) {
undefined.add(pair); //Theta ist nicht im FC => Abbruch undefined.add(pair); //Theta ist nicht im FC => Abbruch
} }
} }
@ -1758,7 +2020,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
} }
// Filter empty sets or sets that only contain an empty set. // Filter empty sets or sets that only contain an empty set.
writeLog("collectErr: " + collectErr);
return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new))) return result.stream().map(x -> x.stream().filter(y -> y.size() > 0).collect(Collectors.toCollection(HashSet::new)))
.filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new)); .filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
} }

2
src/test/resources/bytecode/javFiles/MatrixOP.jav
View File

@ -1,6 +1,6 @@
import java.util.Vector; import java.util.Vector;
import java.lang.Integer; import java.lang.Integer;
//import java.lang.Byte; import java.lang.Byte;
import java.lang.Boolean; import java.lang.Boolean;
public class MatrixOP extends Vector<Vector<Integer>> { public class MatrixOP extends Vector<Vector<Integer>> {