From 2d5c86300861da604de50345d90f713ff41022cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Pl=C3=BCmicke?= Date: Wed, 7 Feb 2018 14:38:45 +0100 Subject: [PATCH] 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 --- src/de/dhbwstuttgart/core/JavaTXCompiler.java | 4 +- .../typeinference/unify/Match.java | 89 +++++++++++++++++++ .../typeinference/unify/TypeUnifyTask.java | 53 ++++++++--- .../unify/interfaces/IMatch.java | 35 ++++++++ .../unify/model/FiniteClosure.java | 25 +++++- .../typeinference/unify/model/Node.java | 3 +- .../typeinference/unify/model/TypeParams.java | 8 +- .../typeinference/unify/model/Unifier.java | 8 ++ test/javFiles/Matrix.jav | 28 +++--- 9 files changed, 218 insertions(+), 35 deletions(-) create mode 100644 src/de/dhbwstuttgart/typeinference/unify/Match.java create mode 100644 src/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java diff --git a/src/de/dhbwstuttgart/core/JavaTXCompiler.java b/src/de/dhbwstuttgart/core/JavaTXCompiler.java index e8d74cb6..8d381e37 100644 --- a/src/de/dhbwstuttgart/core/JavaTXCompiler.java +++ b/src/de/dhbwstuttgart/core/JavaTXCompiler.java @@ -102,8 +102,8 @@ public class JavaTXCompiler { System.out.println(xConsSet); Set> 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()); diff --git a/src/de/dhbwstuttgart/typeinference/unify/Match.java b/src/de/dhbwstuttgart/typeinference/unify/Match.java new file mode 100644 index 00000000..78f7360f --- /dev/null +++ b/src/de/dhbwstuttgart/typeinference/unify/Match.java @@ -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 match(ArrayList 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 result = new HashSet<>(); + + // f<...> = g<...> with f != g are not unifiable + if(!rhsType.getName().equals(lhsType.getName())) + return Optional.empty(); // conflict + // f = f 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); + } +} diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java index 2005a387..e51679e2 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java +++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java @@ -34,6 +34,7 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyType; public class TypeUnifyTask extends RecursiveTask>> { 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>> { /* * Step 1: Repeated application of reduce, adapt, erase, swap */ + //System.out.println("Unifikation: " + eq); Set eq0 = applyTypeUnificationRules(eq, fc); /* @@ -97,6 +99,8 @@ public class TypeUnifyTask extends RecursiveTask>> { // cartesian product of the sets created by pattern matching. List>> 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> wrap = new HashSet<>(); wrap.add(eq1s); @@ -134,12 +138,16 @@ public class TypeUnifyTask extends RecursiveTask>> { // Sub cartesian products of the second level (pattern matched) sets // "the big (x)" for(Set>> secondLevelSet : secondLevelSets) { + //System.out.println("secondLevelSet "+secondLevelSet.size()); List>> secondLevelSetList = new ArrayList<>(secondLevelSet); Set>> cartResult = setOps.cartesianProduct(secondLevelSetList); - + //System.out.println("CardResult: "+cartResult.size()); // Flatten and add to top level sets Set> flat = new HashSet<>(); + int j = 0; for(List> s : cartResult) { + j++; + //System.out.println("s from CardResult: "+cartResult.size() + " " + j); Set flat1 = new HashSet<>(); for(Set s1 : s) flat1.addAll(s1); @@ -164,6 +172,7 @@ public class TypeUnifyTask extends RecursiveTask>> { /* * Step 5: Substitution */ + System.out.println("vor Subst: " + eqPrime); Optional> eqPrimePrime = rules.subst(eqPrime); /* @@ -176,11 +185,13 @@ public class TypeUnifyTask extends RecursiveTask>> { //(!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>> { 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> 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>> { break; } - Set cs = fc.getAllTypesByName(thetaPrime.getName()); - cs.add(thetaPrime); + Set cs = fc.getAllTypesByName(thetaPrime.getName());//cs= [java.util.Vector, java.util.Vector>, ????java.util.Vector???] + + //PL 18-02-06 entfernt, kommt durch unify wieder rein + //cs.add(thetaPrime); + //PL 18-02-06 entfernt for(UnifyType c : cs) { - Set 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 thetaQs = fc.smaller(c).stream().collect(Collectors.toCollection(HashSet::new)); + //Set 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'> werden entfernt + thetaQs = thetaQs.stream().filter(ut -> ut.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new)); + //PL 18-02-06: eingefuegt + Set thetaQPrimes = new HashSet<>(); TypeParams cParams = c.getTypeParams(); if(cParams.size() == 0) @@ -464,6 +489,11 @@ public class TypeUnifyTask extends RecursiveTask>> { } for(UnifyType tqp : thetaQPrimes) { + //System.out.println(tqp.toString()); + //i++; + //System.out.println(i); + //if (i == 62) + // System.out.println(tqp.toString()); Optional opt = stdUnify.unify(tqp, thetaPrime); if (!opt.isPresent()) continue; @@ -474,10 +504,11 @@ public class TypeUnifyTask extends RecursiveTask>> { for (Entry sigma : unifier) substitutionSet.add(new UnifyPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT)); - List freshTphs = new ArrayList<>(); + //List freshTphs = new ArrayList<>(); PL 18-02-06 in die For-Schleife verschoben for (UnifyType tq : thetaQs) { - Set smaller = fc.smaller(unifier.apply(tq)); + Set smaller = fc.smaller(unifier.apply(tq)); for(UnifyType theta : smaller) { + List freshTphs = new ArrayList<>(); Set resultPrime = new HashSet<>(); for(int i = 0; !allGen && i < theta.getTypeParams().size(); i++) { diff --git a/src/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java new file mode 100644 index 00000000..5e201dd7 --- /dev/null +++ b/src/de/dhbwstuttgart/typeinference/unify/interfaces/IMatch.java @@ -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 match(ArrayList 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. + */ + + +} diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java index aba3d3f6..dcffbee6 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java @@ -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(pair.getLhsType())); @@ -93,7 +104,9 @@ public class FiniteClosure implements IFiniteClosure { private Set computeSmaller(Set types) { HashSet 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> candidates = strInheritanceGraph.get(t.getName()); + Set> candidates = strInheritanceGraph.get(t.getName()); //cadidates= [???Node(java.util.Vector>)??? + // , Node(java.util.Vector) + //] for(Node candidate : candidates) { UnifyType theta2 = candidate.getContent(); - Optional optSigma = unify.unify(theta2, t); + //PL 18-02-05 Unifier durch Matcher ersetzt ANFANG + ArrayList termList= new ArrayList(); + termList.add(new UnifyPair(theta2,t, PairOperator.EQUALSDOT)); + Optional optSigma = match.match(termList); + //PL 18-02-05 Unifier durch Matcher ersetzt ENDE if(!optSigma.isPresent()) continue; diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Node.java b/src/de/dhbwstuttgart/typeinference/unify/model/Node.java index c6aa9b3e..aa375c09 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Node.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Node.java @@ -94,6 +94,7 @@ class Node { @Override public String toString() { - return "Node(" + content.toString() + ")\n"; + return "Elem: Node(" + content.toString() + ")\nPrec: " + getContentOfPredecessors().toString() + + "\nDesc: " + getContentOfDescendants().toString() + "\n\n"; } } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java index dc90847b..34501716 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/TypeParams.java @@ -98,12 +98,12 @@ public final class TypeParams implements Iterable{ */ 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; } diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java index 2dd7c83f..061ba588 100644 --- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java +++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java @@ -66,6 +66,14 @@ public class Unifier implements Function, Iterable> { mul(m) { var ret = new Matrix(); var i = 0; - while(i < size()) { + //while(i < size()) { var v1 = this.elementAt(i); - var v2 = new Vector(); - 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(); + //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; } }