HEAD detached at 2f994cdf

Changes to be committed:
Aenderungen am Unify: Fehler behoben und Vereinfachung

	modified:   src/de/dhbwstuttgart/core/JavaTXCompiler.java
	new file:   src/de/dhbwstuttgart/typeinference/unify/Match.java
	modified:   src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
	new file:   src/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java
	modified:   src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
	modified:   src/de/dhbwstuttgart/typeinference/unify/model/Node.java
	modified:   src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java
	modified:   src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
	modified:   test/javFiles/Matrix.jav
This commit is contained in:
Martin Plümicke 2018-02-07 14:38:45 +01:00
parent 2f994cdfa8
commit 2d5c863008
9 changed files with 218 additions and 35 deletions

View File

@ -102,8 +102,8 @@ public class JavaTXCompiler {
System.out.println(xConsSet);
Set<Set<UnifyPair>> result = unify.unify(xConsSet, finiteClosure);
System.out.println("RESULT: " + result);
results.addAll(result);
System.out.println("RESULT: " + result.size());
//results.addAll(result);
}
return results.stream().map((unifyPairs ->
new ResultSet(UnifyTypeFactory.convert(unifyPairs, generateTPHMap(cons))))).collect(Collectors.toList());

View File

@ -0,0 +1,89 @@
package de.dhbwstuttgart.typeinference.unify;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Optional;
import java.util.Set;
import java.util.stream.Collectors;
import de.dhbwstuttgart.typeinference.unify.interfaces.IMatch;
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
/**
* Implementation of match derived from unification algorithm.
* @author Martin Pluemicke
*/
public class Match implements IMatch {
@Override
public Optional<Unifier> match(ArrayList<UnifyPair> termsList) {
// Start with the identity unifier. Substitutions will be added later.
Unifier mgu = Unifier.identity();
// Apply rules while possible
int idx = 0;
while(idx < termsList.size()) {
UnifyPair pair = termsList.get(idx);
UnifyType rhsType = pair.getRhsType();
UnifyType lhsType = pair.getLhsType();
TypeParams rhsTypeParams = rhsType.getTypeParams();
TypeParams lhsTypeParams = lhsType.getTypeParams();
// REDUCE - Rule
if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)) {
Set<UnifyPair> result = new HashSet<>();
// f<...> = g<...> with f != g are not unifiable
if(!rhsType.getName().equals(lhsType.getName()))
return Optional.empty(); // conflict
// f<t1,...,tn> = f<s1,...,sm> are not unifiable
if(rhsTypeParams.size() != lhsTypeParams.size())
return Optional.empty(); // conflict
// f = g is not unifiable (cannot be f = f because erase rule would have been applied)
//if(rhsTypeParams.size() == 0)
//return Optional.empty();
// Unpack the arguments
for(int i = 0; i < rhsTypeParams.size(); i++)
result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
termsList.remove(idx);
termsList.addAll(result);
continue;
}
// DELETE - Rule
if(pair.getRhsType().equals(pair.getLhsType())) {
termsList.remove(idx);
continue;
}
// SWAP - Rule
if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
return Optional.empty(); // conflict
}
// OCCURS-CHECK
//deleted
// SUBST - Rule
if(lhsType instanceof PlaceholderType) {
mgu.add((PlaceholderType) lhsType, rhsType);
termsList = termsList.stream().map(mgu::applyleft).collect(Collectors.toCollection(ArrayList::new));
idx = idx+1 == termsList.size() ? 0 : idx+1;
continue;
}
idx++;
}
return Optional.of(mgu);
}
}

View File

@ -34,6 +34,7 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
private static final long serialVersionUID = 1L;
private static int i = 0;
/**
* The implementation of setOps that will be used during the unification
@ -77,6 +78,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
/*
* Step 1: Repeated application of reduce, adapt, erase, swap
*/
//System.out.println("Unifikation: " + eq);
Set<UnifyPair> eq0 = applyTypeUnificationRules(eq, fc);
/*
@ -97,6 +99,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
// cartesian product of the sets created by pattern matching.
List<Set<Set<UnifyPair>>> topLevelSets = new ArrayList<>();
System.out.println(eq2s);
if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
Set<Set<UnifyPair>> wrap = new HashSet<>();
wrap.add(eq1s);
@ -134,12 +138,16 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
// Sub cartesian products of the second level (pattern matched) sets
// "the big (x)"
for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
//System.out.println("secondLevelSet "+secondLevelSet.size());
List<Set<Set<UnifyPair>>> secondLevelSetList = new ArrayList<>(secondLevelSet);
Set<List<Set<UnifyPair>>> cartResult = setOps.cartesianProduct(secondLevelSetList);
//System.out.println("CardResult: "+cartResult.size());
// Flatten and add to top level sets
Set<Set<UnifyPair>> flat = new HashSet<>();
int j = 0;
for(List<Set<UnifyPair>> s : cartResult) {
j++;
//System.out.println("s from CardResult: "+cartResult.size() + " " + j);
Set<UnifyPair> flat1 = new HashSet<>();
for(Set<UnifyPair> s1 : s)
flat1.addAll(s1);
@ -164,6 +172,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
/*
* Step 5: Substitution
*/
System.out.println("vor Subst: " + eqPrime);
Optional<Set<UnifyPair>> eqPrimePrime = rules.subst(eqPrime);
/*
@ -176,11 +185,13 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
//(!eqPrimePrime.isPresent()) erfolgt ist, ist das Ergebnis erzielt.
eqPrimePrimeSet.add(eqPrime);
else if(eqPrimePrime.isPresent()) {
System.out.println("nextStep: " + eqPrimePrime.get());
TypeUnifyTask fork = new TypeUnifyTask(eqPrimePrime.get(), fc, true);
forks.add(fork);
fork.fork();
}
else {
System.out.println("nextStep: " + eqPrime);
TypeUnifyTask fork = new TypeUnifyTask(eqPrime, fc, true);
forks.add(fork);
fork.fork();
@ -381,9 +392,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
UnifyType rhsType = pair.getRhsType();
// Case 1: (a <. Theta')
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
System.out.println(pair);
Set<Set<UnifyPair>> x1 = unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc);
System.out.println(x1);
result.get(0).add(x1);
}
// Case 2: (a <.? ? ext Theta')
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
@ -442,13 +456,24 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
break;
}
Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
cs.add(thetaPrime);
Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());//cs= [java.util.Vector<NP>, java.util.Vector<java.util.Vector<java.lang.Integer>>, ????java.util.Vector<gen_hv>???]
//PL 18-02-06 entfernt, kommt durch unify wieder rein
//cs.add(thetaPrime);
//PL 18-02-06 entfernt
for(UnifyType c : cs) {
Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
thetaQs.add(thetaPrime); //PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert,
//da children offensichtlich ein echtes kleiner und kein kleinergleich ist
//PL 18-02-05 getChildren durch smaller ersetzt in getChildren werden die Varianlen nicht ersetzt.
Set<UnifyType> thetaQs = fc.smaller(c).stream().collect(Collectors.toCollection(HashSet::new));
//Set<UnifyType> thetaQs = fc.getChildren(c).stream().collect(Collectors.toCollection(HashSet::new));
//thetaQs.add(thetaPrime); //PL 18-02-05 wieder geloescht
//PL 2017-10-03: War auskommentiert habe ich wieder einkommentiert,
//da children offensichtlich ein echtes kleiner und kein kleinergleich ist
//PL 18-02-06: eingefuegt, thetaQs der Form V<V<...>> <. V'<V<...>> werden entfernt
thetaQs = thetaQs.stream().filter(ut -> ut.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
//PL 18-02-06: eingefuegt
Set<UnifyType> thetaQPrimes = new HashSet<>();
TypeParams cParams = c.getTypeParams();
if(cParams.size() == 0)
@ -464,6 +489,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
}
for(UnifyType tqp : thetaQPrimes) {
//System.out.println(tqp.toString());
//i++;
//System.out.println(i);
//if (i == 62)
// System.out.println(tqp.toString());
Optional<Unifier> opt = stdUnify.unify(tqp, thetaPrime);
if (!opt.isPresent())
continue;
@ -474,10 +504,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
for (Entry<PlaceholderType, UnifyType> sigma : unifier)
substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
List<UnifyType> freshTphs = new ArrayList<>();
//List<UnifyType> freshTphs = new ArrayList<>(); PL 18-02-06 in die For-Schleife verschoben
for (UnifyType tq : thetaQs) {
Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
for(UnifyType theta : smaller) {
List<UnifyType> freshTphs = new ArrayList<>();
Set<UnifyPair> resultPrime = new HashSet<>();
for(int i = 0; !allGen && i < theta.getTypeParams().size(); i++) {

View File

@ -0,0 +1,35 @@
package de.dhbwstuttgart.typeinference.unify.interfaces;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Optional;
import java.util.Set;
import java.util.stream.Collectors;
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
/**
* Match
* @author Martin Pluemicke
*/
public interface IMatch {
/**
* Finds the most general unifier sigma of the set {t1,...,tn} so that
* sigma(t1) = sigma(t2) = ... = sigma(tn).
* @param terms The set of terms to be unified
* @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
*/
public Optional<Unifier> match(ArrayList<UnifyPair> termsList);
/**
* Finds the most general unifier sigma of the set {t1,...,tn} so that
* sigma(t1) = sigma(t2) = ... = sigma(tn).
* @param terms The set of terms to be unified
* @return An optional of the most general unifier if it exists or an empty optional if there is no unifier.
*/
}

View File

@ -8,7 +8,11 @@ import java.util.Optional;
import java.util.Set;
import java.util.stream.Collectors;
//PL 18-02-05 Unifier durch Matcher ersetzt
//mus greater noch erstezt werden
import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
import de.dhbwstuttgart.typeinference.unify.Match;
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
@ -46,6 +50,13 @@ public class FiniteClosure implements IFiniteClosure {
if(pair.getPairOp() != PairOperator.SMALLER)
continue;
//VERSUCH PL 18-02-06
//koennte ggf. die FC reduzieren
//TO DO: Ueberpruefen, ob das sinnvll und korrekt ist
//if (!pair.getLhsType().getTypeParams().arePlaceholders()
// && !pair.getRhsType().getTypeParams().arePlaceholders())
// continue;
;
// Add nodes if not already in the graph
if(!inheritanceGraph.containsKey(pair.getLhsType()))
inheritanceGraph.put(pair.getLhsType(), new Node<UnifyType>(pair.getLhsType()));
@ -93,7 +104,9 @@ public class FiniteClosure implements IFiniteClosure {
private Set<UnifyType> computeSmaller(Set<UnifyType> types) {
HashSet<UnifyType> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
//PL 18-02-05 Unifier durch Matcher ersetzt
//IUnify unify = new MartelliMontanariUnify();
Match match = new Match();
for(UnifyType t : types) {
@ -112,10 +125,16 @@ public class FiniteClosure implements IFiniteClosure {
continue;
// if T <* T' then sigma(T) <* sigma(T')
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName()); //cadidates= [???Node(java.util.Vector<java.util.Vector<java.lang.Integer>>)???
// , Node(java.util.Vector<gen_hv>)
//]
for(Node<UnifyType> candidate : candidates) {
UnifyType theta2 = candidate.getContent();
Optional<Unifier> optSigma = unify.unify(theta2, t);
//PL 18-02-05 Unifier durch Matcher ersetzt ANFANG
ArrayList<UnifyPair> termList= new ArrayList<UnifyPair>();
termList.add(new UnifyPair(theta2,t, PairOperator.EQUALSDOT));
Optional<Unifier> optSigma = match.match(termList);
//PL 18-02-05 Unifier durch Matcher ersetzt ENDE
if(!optSigma.isPresent())
continue;

View File

@ -94,6 +94,7 @@ class Node<T> {
@Override
public String toString() {
return "Node(" + content.toString() + ")\n";
return "Elem: Node(" + content.toString() + ")\nPrec: " + getContentOfPredecessors().toString()
+ "\nDesc: " + getContentOfDescendants().toString() + "\n\n";
}
}

View File

@ -98,12 +98,12 @@ public final class TypeParams implements Iterable<UnifyType>{
*/
public boolean occurs(PlaceholderType t) {
for(UnifyType p : typeParams)
if(p instanceof PlaceholderType)
if(p instanceof PlaceholderType) {
if(p.equals(t))
return true;
else
return true; }
else {
if(p.getTypeParams().occurs(t))
return true;
return true; }
return false;
}

View File

@ -66,6 +66,14 @@ public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<P
return new UnifyPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp());
}
/**
* Applies the unifier to the left terms of the pair.
* @return A new pair where the left and right-hand side are applied
*/
public UnifyPair applyleft(UnifyPair p) {
return new UnifyPair(this.apply(p.getLhsType()), p.getRhsType(), p.getPairOp());
}
/**
* True if the typevariable t will be substituted if the unifier is applied.
* false otherwise.

View File

@ -6,21 +6,21 @@ class Matrix extends Vector<Vector<Integer>> {
mul(m) {
var ret = new Matrix();
var i = 0;
while(i < size()) {
//while(i < size()) {
var v1 = this.elementAt(i);
var v2 = new Vector<Integer>();
var j = 0;
while(j < v1.size()) {
var erg = 0;
var k = 0;
while(k < v1.size()) {
erg = erg + v1.elementAt(k)
* m.elementAt(k).elementAt(j);
k++; }
v2.addElement(new Integer(erg));
j++; }
ret.addElement(v2);
i++; }
//var v2 = new Vector<Integer>();
//var j = 0;
//while(j < v1.size()) {
//var erg = 0;
//var k = 0;
//while(k < v1.size()) {
//erg = erg + v1.elementAt(k)
// * m.elementAt(k).elementAt(j);
//k++; }
//v2.addElement(new Integer(erg));
//j++; }
//ret.addElement(v2);
//i++; }
return ret;
}
}