modified: de/dhbwstuttgart/typeinference/unify/RuleSet.java
modified: de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java modified: de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java logFile eingefuegt
This commit is contained in:
parent
8e198679c7
commit
1c0fa6a820
@ -249,17 +249,17 @@ public class RuleSet implements IRuleSet{
|
|||||||
ReferenceType lhsSType = (ReferenceType) c;
|
ReferenceType lhsSType = (ReferenceType) c;
|
||||||
ReferenceType rhsSType = (ReferenceType) d;
|
ReferenceType rhsSType = (ReferenceType) d;
|
||||||
|
|
||||||
try {
|
//try {
|
||||||
logFile.write("PAIR Rules: " + pair + "\n");
|
// logFile.write("PAIR Rules: " + pair + "\n");
|
||||||
logFile.flush();
|
// logFile.flush();
|
||||||
}
|
//}
|
||||||
catch (IOException e) { }
|
//catch (IOException e) { }
|
||||||
|
|
||||||
if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size())
|
if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size())
|
||||||
return Optional.empty();
|
return Optional.empty();
|
||||||
|
|
||||||
UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null);
|
UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null);
|
||||||
2018-02-23: liefert Vector<Vector<Integer>>: Das kann nicht sein.
|
//2018-02-23: liefert Vector<Vector<Integer>>: Das kann nicht sein.
|
||||||
|
|
||||||
//NOCHMAL UEBERPRUEFEN
|
//NOCHMAL UEBERPRUEFEN
|
||||||
//PL 18-02-09 Eingfuegt Anfang
|
//PL 18-02-09 Eingfuegt Anfang
|
||||||
@ -275,22 +275,22 @@ public class RuleSet implements IRuleSet{
|
|||||||
}
|
}
|
||||||
//PL 18-02-09 Eingfuegt ENDE
|
//PL 18-02-09 Eingfuegt ENDE
|
||||||
|
|
||||||
try {
|
//try {
|
||||||
logFile.write("cFromFc: " + cFromFc);
|
// logFile.write("cFromFc: " + cFromFc);
|
||||||
logFile.flush();
|
// logFile.flush();
|
||||||
}
|
//}
|
||||||
catch (IOException e) { }
|
//catch (IOException e) { }
|
||||||
|
|
||||||
if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders())
|
if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders())
|
||||||
return Optional.empty();
|
return Optional.empty();
|
||||||
|
|
||||||
UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null);
|
UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null);
|
||||||
|
|
||||||
try {
|
//try {
|
||||||
logFile.write("cFromFc: " + cFromFc);
|
// logFile.write("cFromFc: " + cFromFc);
|
||||||
logFile.flush();
|
// logFile.flush();
|
||||||
}
|
//}
|
||||||
catch (IOException e) { }
|
//catch (IOException e) { }
|
||||||
|
|
||||||
if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size())
|
if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size())
|
||||||
return Optional.empty();
|
return Optional.empty();
|
||||||
|
@ -93,7 +93,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
/*
|
/*
|
||||||
* Step 1: Repeated application of reduce, adapt, erase, swap
|
* Step 1: Repeated application of reduce, adapt, erase, swap
|
||||||
*/
|
*/
|
||||||
if (printtag) System.out.println("Unifikation: " + eq);
|
writeLog("Unifikation: " + eq.toString());
|
||||||
Set<UnifyPair> eq0 = applyTypeUnificationRules(eq, fc);
|
Set<UnifyPair> eq0 = applyTypeUnificationRules(eq, fc);
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@ -138,6 +138,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
// Sets of the "second level"
|
// Sets of the "second level"
|
||||||
Set<UnifyPair> undefinedPairs = new HashSet<>();
|
Set<UnifyPair> undefinedPairs = new HashSet<>();
|
||||||
if (printtag) System.out.println("eq2s " + eq2s);
|
if (printtag) System.out.println("eq2s " + eq2s);
|
||||||
|
writeLog(bufferSet.toString()+"\n");
|
||||||
Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, fc, undefinedPairs);
|
Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, fc, undefinedPairs);
|
||||||
//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
|
||||||
@ -239,27 +240,27 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
}
|
}
|
||||||
else { // sequentiell (Step 6b is included)
|
else { // sequentiell (Step 6b is included)
|
||||||
if (printtag) System.out.println("nextStep: " + eqPrimePrime);
|
if (printtag) System.out.println("nextStep: " + eqPrimePrime);
|
||||||
if (eqPrime.equals(eq)) //PL 2017-09-29 auskommentiert und durch
|
if (eqPrime.equals(eq)) { //PL 2017-09-29 auskommentiert und durch
|
||||||
//(!eqPrimePrime.isPresent()) //PL 2071-09-29 dies ersetzt
|
//(!eqPrimePrime.isPresent()) //PL 2071-09-29 dies ersetzt
|
||||||
//Begruendung: Wenn in der Substitution keine Veraenderung
|
//Begruendung: Wenn in der Substitution keine Veraenderung
|
||||||
//(!eqPrimePrime.isPresent()) erfolgt ist, ist das Ergebnis erzielt.
|
//(!eqPrimePrime.isPresent()) erfolgt ist, ist das Ergebnis erzielt.
|
||||||
eqPrimePrimeSet.add(eqPrime);
|
|
||||||
else if(eqPrimePrime.isPresent()) {
|
|
||||||
Set<Set<UnifyPair>> unifyres = unify(eqPrimePrime.get(), fc, false);
|
|
||||||
try {
|
try {
|
||||||
logFile.write(unifyres.toString()+"\n");
|
if (isSolvedForm(eqPrime)) {
|
||||||
//logFile.flush();
|
logFile.write(eqPrime.toString()+"\n");
|
||||||
|
logFile.flush();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
catch (IOException e) { }
|
catch (IOException e) { }
|
||||||
|
eqPrimePrimeSet.add(eqPrime);
|
||||||
|
}
|
||||||
|
else if(eqPrimePrime.isPresent()) {
|
||||||
|
Set<Set<UnifyPair>> unifyres = unify(eqPrimePrime.get(), fc, false);
|
||||||
|
|
||||||
eqPrimePrimeSet.addAll(unifyres);
|
eqPrimePrimeSet.addAll(unifyres);
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
Set<Set<UnifyPair>> unifyres = unify(eqPrime, fc, false);
|
Set<Set<UnifyPair>> unifyres = unify(eqPrime, fc, false);
|
||||||
try {
|
|
||||||
//logFile.write(unifyres.toString()+"\n");
|
|
||||||
logFile.flush();
|
|
||||||
}
|
|
||||||
catch (IOException e) { }
|
|
||||||
|
|
||||||
eqPrimePrimeSet.addAll(unifyres);
|
eqPrimePrimeSet.addAll(unifyres);
|
||||||
}
|
}
|
||||||
@ -279,8 +280,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
/*
|
/*
|
||||||
* Step 7: Filter empty sets;
|
* Step 7: Filter empty sets;
|
||||||
*/
|
*/
|
||||||
return eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x)).collect(Collectors.toCollection(HashSet::new));
|
eqPrimePrimeSet = eqPrimePrimeSet.stream().filter(x -> isSolvedForm(x)).collect(Collectors.toCollection(HashSet::new));
|
||||||
|
return eqPrimePrimeSet;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@ -382,11 +383,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
|
// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
|
||||||
try {
|
//try {
|
||||||
logFile.write("PAIR1 " + pair + "\n");
|
// logFile.write("PAIR1 " + pair + "\n");
|
||||||
logFile.flush();
|
// logFile.flush();
|
||||||
}
|
//}
|
||||||
catch (IOException e) { }
|
//catch (IOException e) { }
|
||||||
|
|
||||||
Optional<Set<UnifyPair>> optSet = rules.reduce1(pair, fc);
|
Optional<Set<UnifyPair>> optSet = rules.reduce1(pair, fc);
|
||||||
optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
|
optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
|
||||||
@ -411,11 +412,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Adapt, AdaptExt, AdaptSup
|
// Adapt, AdaptExt, AdaptSup
|
||||||
try {
|
//try {
|
||||||
logFile.write("PAIR2 " + pair + "\n");
|
// logFile.write("PAIR2 " + pair + "\n");
|
||||||
logFile.flush();
|
// logFile.flush();
|
||||||
}
|
//}
|
||||||
catch (IOException e) { }
|
//catch (IOException e) { }
|
||||||
opt = rules.adapt(pair, fc);
|
opt = rules.adapt(pair, fc);
|
||||||
opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc);
|
opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc);
|
||||||
opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc);
|
opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc);
|
||||||
@ -486,7 +487,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
// Case 1: (a <. Theta')
|
// Case 1: (a <. Theta')
|
||||||
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
|
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
|
||||||
//System.out.println(pair);
|
//System.out.println(pair);
|
||||||
if (first) {if (printtag) System.out.println(pair);
|
if (first) { writeLog(pair.toString()+"\n");
|
||||||
Set<Set<UnifyPair>> x1 = unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc);
|
Set<Set<UnifyPair>> x1 = unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc);
|
||||||
//System.out.println(x1);
|
//System.out.println(x1);
|
||||||
result.get(0).add(x1);
|
result.get(0).add(x1);
|
||||||
@ -502,7 +503,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
}
|
}
|
||||||
// Case 2: (a <.? ? ext Theta')
|
// Case 2: (a <.? ? ext Theta')
|
||||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
|
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
|
||||||
if (first) {if (printtag) System.out.println(pair);
|
if (first) {writeLog(pair.toString()+"\n");
|
||||||
result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
|
result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
@ -515,7 +516,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
|
|
||||||
// Case 3: (a <.? ? sup Theta')
|
// Case 3: (a <.? ? sup Theta')
|
||||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
|
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
|
||||||
if (first) {if (printtag) System.out.println(pair);
|
if (first) {writeLog(pair.toString()+"\n");
|
||||||
result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
|
result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
@ -533,7 +534,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
|
|
||||||
// Case 5: (Theta <. a)
|
// Case 5: (Theta <. a)
|
||||||
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
|
else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
|
||||||
if (first) {if (printtag) System.out.println(pair);
|
if (first) {writeLog(pair.toString()+"\n");
|
||||||
result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
|
result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
@ -556,7 +557,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
|
|
||||||
// Case 8: (Theta <.? a)
|
// Case 8: (Theta <.? a)
|
||||||
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
|
else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
|
||||||
if (first) {if (printtag) System.out.println(pair);
|
if (first) {writeLog(pair.toString()+"\n");
|
||||||
result.get(7).add(
|
result.get(7).add(
|
||||||
unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
|
unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
|
||||||
}
|
}
|
||||||
@ -662,7 +663,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
else
|
else
|
||||||
resultPrime.add(new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, theta.setTypeParams(new TypeParams(freshTphs.toArray(new UnifyType[0]))), PairOperator.EQUALSDOT));
|
||||||
resultPrime.addAll(substitutionSet);
|
resultPrime.addAll(substitutionSet);
|
||||||
|
writeLog(substitutionSet.toString());
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -689,6 +692,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, extAPrime, PairOperator.EQUALSDOT));
|
||||||
resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT));
|
resultPrime.add(new UnifyPair(aPrime, thetaPrime, PairOperator.SMALLERDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -704,11 +708,13 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
Set<UnifyPair> resultPrime = new HashSet<>();
|
Set<UnifyPair> resultPrime = new HashSet<>();
|
||||||
resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT));
|
resultPrime.add(new UnifyPair(thetaPrime, a, PairOperator.SMALLERDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
|
|
||||||
resultPrime = new HashSet<>();
|
resultPrime = new HashSet<>();
|
||||||
resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, supAPrime, PairOperator.EQUALSDOT));
|
||||||
resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT));
|
resultPrime.add(new UnifyPair(thetaPrime, aPrime, PairOperator.SMALLERDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
|
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
@ -740,6 +746,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
else
|
else
|
||||||
resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, thetaS.setTypeParams(new TypeParams(freshTphs)), PairOperator.EQUALSDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
}
|
}
|
||||||
|
|
||||||
return result;
|
return result;
|
||||||
@ -754,17 +761,20 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
Set<UnifyPair> resultPrime = new HashSet<>();
|
Set<UnifyPair> resultPrime = new HashSet<>();
|
||||||
resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
|
|
||||||
UnifyType freshTph = PlaceholderType.freshPlaceholder();
|
UnifyType freshTph = PlaceholderType.freshPlaceholder();
|
||||||
resultPrime = new HashSet<>();
|
resultPrime = new HashSet<>();
|
||||||
resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, new ExtendsType(freshTph), PairOperator.EQUALSDOT));
|
||||||
resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT));
|
resultPrime.add(new UnifyPair(theta, freshTph, PairOperator.SMALLERDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
|
|
||||||
resultPrime = new HashSet<>();
|
resultPrime = new HashSet<>();
|
||||||
resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT));
|
resultPrime.add(new UnifyPair(a, new SuperType(freshTph), PairOperator.EQUALSDOT));
|
||||||
resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT));
|
resultPrime.add(new UnifyPair(freshTph, theta, PairOperator.SMALLERDOT));
|
||||||
result.add(resultPrime);
|
result.add(resultPrime);
|
||||||
|
writeLog(resultPrime.toString());
|
||||||
//}
|
//}
|
||||||
|
|
||||||
return result;
|
return result;
|
||||||
@ -802,4 +812,13 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
|
|||||||
permuteParams(candidates, idx+1, result, current);
|
permuteParams(candidates, idx+1, result, current);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void writeLog(String str) {
|
||||||
|
try {
|
||||||
|
logFile.write(str+"\n");
|
||||||
|
logFile.flush();
|
||||||
|
|
||||||
|
}
|
||||||
|
catch (IOException e) { }
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -37,7 +37,6 @@ public class FiniteClosure implements IFiniteClosure {
|
|||||||
* The initial pairs of that define the inheritance tree
|
* The initial pairs of that define the inheritance tree
|
||||||
*/
|
*/
|
||||||
private Set<UnifyPair> pairs;
|
private Set<UnifyPair> pairs;
|
||||||
2018-02-23: Muessten hier NUR die initiale Piars rein?
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new instance using the inheritance tree defined in the pairs.
|
* Creates a new instance using the inheritance tree defined in the pairs.
|
||||||
@ -370,7 +369,7 @@ public class FiniteClosure implements IFiniteClosure {
|
|||||||
return Optional.empty();
|
return Optional.empty();
|
||||||
|
|
||||||
for(UnifyPair pair : pairs)
|
for(UnifyPair pair : pairs)
|
||||||
if(pair.getLhsType().getName().equals(typeName))
|
if(pair.getLhsType().getName().equals(typeName) && pair.getLhsType().typeParams.arePlaceholders())
|
||||||
return Optional.of(pair.getLhsType());
|
return Optional.of(pair.getLhsType());
|
||||||
|
|
||||||
return Optional.empty();
|
return Optional.empty();
|
||||||
|
Loading…
Reference in New Issue
Block a user