forked from JavaTX/JavaCompilerCore
Merge branch 'unify' of ssh://gohorb.ba-horb.de/bahome/projekt/git/JavaCompilerCore into refactoring
This commit is contained in:
JanUlrich
commit
a8d8dec899
@ -3,11 +3,11 @@ package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
|
||||
public interface IFiniteClosure {
|
||||
|
||||
@ -50,4 +50,5 @@ public interface IFiniteClosure {
|
||||
public Set<Type> smArg(PlaceholderType type);
|
||||
|
||||
public Optional<Type> getGenericType(String typeName);
|
||||
public Set<Type> getAllTypes(String typeName);
|
||||
}
|
||||
|
||||
@ -3,8 +3,7 @@ package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
|
||||
public interface IRuleSet {
|
||||
|
||||
@ -27,5 +26,5 @@ public interface IRuleSet {
|
||||
public Optional<MPair> adaptExt(MPair pair);
|
||||
public Optional<MPair> adaptSup(MPair pair);
|
||||
|
||||
public Set<MPair> subst(Set<MPair> pair);
|
||||
public Optional<Set<MPair>> subst(Set<MPair> pair);
|
||||
}
|
||||
|
||||
@ -1,7 +0,0 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.Menge;
|
||||
|
||||
public interface ITypeMapper<T> {
|
||||
|
||||
}
|
||||
@ -1,14 +1,23 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.interfaces;
|
||||
|
||||
import java.util.Arrays;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
|
||||
/**
|
||||
* Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari, Ruzicka-Privara or Suciu)
|
||||
* Standard unification algorithm (e.g. Robinson, Paterson-Wegman, Martelli-Montanari)
|
||||
* @author Florian Steurer
|
||||
*/
|
||||
public interface IUnify {
|
||||
public Unifier unify(Set<MPair> terms);
|
||||
|
||||
public Optional<Unifier> unify(Set<Type> terms);
|
||||
|
||||
default public Optional<Unifier> unify(Type... terms) {
|
||||
return unify(Arrays.stream(terms).collect(Collectors.toSet()));
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -1,18 +1,32 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
/**
|
||||
* An extends wildcard type "? extends T".
|
||||
*/
|
||||
public final class ExtendsType extends Type {
|
||||
|
||||
/**
|
||||
* The extended type
|
||||
*/
|
||||
private Type extendedType;
|
||||
|
||||
/**
|
||||
* Creates a new extends wildcard type.
|
||||
* @param extendedType The extended type e.g. Integer in "? extends Integer"
|
||||
*/
|
||||
public ExtendsType(Type extendedType) {
|
||||
super("? extends " + extendedType.getName(), extendedType.getTypeParams());
|
||||
this.extendedType = extendedType;
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the type extended by this wildcard e.g. "Integer" for "? extends Integer"
|
||||
* @return The extended type.
|
||||
*/
|
||||
public Type getExtendedType() {
|
||||
return extendedType;
|
||||
}
|
||||
@ -23,20 +37,25 @@ public final class ExtendsType extends Type {
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return "? extends " + extendedType;
|
||||
public Type setTypeParams(TypeParams newTp) {
|
||||
return new ExtendsType(extendedType.setTypeParams(newTp));
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> smArg(IFiniteClosure fc) {
|
||||
Set<Type> smArg(IFiniteClosure fc) {
|
||||
return fc.smArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> grArg(IFiniteClosure fc) {
|
||||
Set<Type> grArg(IFiniteClosure fc) {
|
||||
return fc.grArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
Type apply(Unifier unif) {
|
||||
return new ExtendsType(extendedType.apply(unif));
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return extendedType.hashCode() + 17;
|
||||
@ -52,7 +71,7 @@ public final class ExtendsType extends Type {
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Unifier unif) {
|
||||
return new ExtendsType(extendedType.apply(unif));
|
||||
public String toString() {
|
||||
return "? extends " + extendedType;
|
||||
}
|
||||
}
|
||||
@ -1,12 +1,13 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
|
||||
public class FiniteClosure implements IFiniteClosure {
|
||||
|
||||
@ -205,4 +206,11 @@ public class FiniteClosure implements IFiniteClosure {
|
||||
|
||||
return Optional.empty();
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> getAllTypes(String typeName) {
|
||||
if(!strInheritanceGraph.containsKey(typeName))
|
||||
return new HashSet<>();
|
||||
return strInheritanceGraph.get(typeName).stream().map(x -> x.getContent()).collect(Collectors.toCollection(HashSet::new));
|
||||
}
|
||||
}
|
||||
@ -1,4 +1,4 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
public class MPair {
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
@ -1,9 +1,8 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
public final class PlaceholderType extends Type{
|
||||
|
||||
@ -12,20 +11,32 @@ public final class PlaceholderType extends Type{
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> smArg(IFiniteClosure fc) {
|
||||
Set<Type> smArg(IFiniteClosure fc) {
|
||||
return fc.smArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> grArg(IFiniteClosure fc) {
|
||||
Set<Type> grArg(IFiniteClosure fc) {
|
||||
return fc.grArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type setTypeParams(TypeParams newTp) {
|
||||
return this;
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return typeName.hashCode();
|
||||
}
|
||||
|
||||
@Override
|
||||
Type apply(Unifier unif) {
|
||||
if(unif.hasSubstitute(this))
|
||||
return unif.getSubstitute(this);
|
||||
return this;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object obj) {
|
||||
if(!(obj instanceof PlaceholderType))
|
||||
@ -33,12 +44,4 @@ public final class PlaceholderType extends Type{
|
||||
|
||||
return ((PlaceholderType) obj).getName().equals(typeName);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Unifier unif) {
|
||||
if(this.equals(unif.getSource()))
|
||||
return unif.getTarget();
|
||||
|
||||
return this;
|
||||
}
|
||||
}
|
||||
@ -1,9 +1,8 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
public final class SimpleType extends Type {
|
||||
public SimpleType(String name, Type... typeParams) {
|
||||
@ -15,15 +14,25 @@ public final class SimpleType extends Type {
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> smArg(IFiniteClosure fc) {
|
||||
Set<Type> smArg(IFiniteClosure fc) {
|
||||
return fc.smArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> grArg(IFiniteClosure fc) {
|
||||
Set<Type> grArg(IFiniteClosure fc) {
|
||||
return fc.grArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
Type apply(Unifier unif) {
|
||||
return new SimpleType(typeName, typeParams.apply(unif));
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type setTypeParams(TypeParams newTp) {
|
||||
return new SimpleType(new String(typeName), newTp);
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return typeName.hashCode();
|
||||
@ -41,12 +50,4 @@ public final class SimpleType extends Type {
|
||||
|
||||
return other.getTypeParams().equals(typeParams);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Unifier unif) {
|
||||
if(this.equals(unif.getSource()))
|
||||
return unif.getTarget();
|
||||
|
||||
return new SimpleType(typeName, typeParams.apply(unif));
|
||||
}
|
||||
}
|
||||
@ -1,9 +1,8 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
public final class SuperType extends Type {
|
||||
|
||||
@ -29,15 +28,25 @@ public final class SuperType extends Type {
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> smArg(IFiniteClosure fc) {
|
||||
public Type setTypeParams(TypeParams newTp) {
|
||||
return new SuperType(superedType.setTypeParams(newTp));
|
||||
}
|
||||
|
||||
@Override
|
||||
Set<Type> smArg(IFiniteClosure fc) {
|
||||
return fc.smArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<Type> grArg(IFiniteClosure fc) {
|
||||
Set<Type> grArg(IFiniteClosure fc) {
|
||||
return fc.grArg(this);
|
||||
}
|
||||
|
||||
@Override
|
||||
Type apply(Unifier unif) {
|
||||
return new SuperType(superedType.apply(unif));
|
||||
}
|
||||
|
||||
@Override
|
||||
public int hashCode() {
|
||||
return superedType.hashCode() + 17;
|
||||
@ -51,9 +60,4 @@ public final class SuperType extends Type {
|
||||
SuperType other = (SuperType) obj;
|
||||
return other.getSuperedType().equals(superedType);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Unifier unif) {
|
||||
return new SuperType(superedType.apply(unif));
|
||||
}
|
||||
}
|
||||
@ -1,9 +1,8 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
public abstract class Type {
|
||||
|
||||
@ -28,11 +27,13 @@ public abstract class Type {
|
||||
return typeParams;
|
||||
}
|
||||
|
||||
public abstract Set<Type> smArg(IFiniteClosure fc);
|
||||
public abstract Type setTypeParams(TypeParams newTp);
|
||||
|
||||
public abstract Set<Type> grArg(IFiniteClosure fc);
|
||||
abstract Set<Type> smArg(IFiniteClosure fc);
|
||||
|
||||
public abstract Type apply(Unifier unif);
|
||||
abstract Set<Type> grArg(IFiniteClosure fc);
|
||||
|
||||
abstract Type apply(Unifier unif);
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
@ -1,10 +1,8 @@
|
||||
package de.dhbwstuttgart.typinference.unify.model;
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.Arrays;
|
||||
import java.util.Iterator;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unifier;
|
||||
|
||||
public final class TypeParams implements Iterable<Type>{
|
||||
private final Type[] typeParams;
|
||||
|
||||
@ -42,6 +40,17 @@ public final class TypeParams implements Iterable<Type>{
|
||||
return new TypeParams(newParams);
|
||||
}
|
||||
|
||||
public boolean occurs(PlaceholderType t) {
|
||||
for(Type p : typeParams)
|
||||
if(p instanceof PlaceholderType)
|
||||
if(p.equals(t))
|
||||
return true;
|
||||
else
|
||||
if(p.getTypeParams().occurs(t))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
public boolean contains(Type t) {
|
||||
for(Type t1 : typeParams)
|
||||
if(t1.equals(t1))
|
||||
@ -53,6 +62,13 @@ public final class TypeParams implements Iterable<Type>{
|
||||
return typeParams[i];
|
||||
}
|
||||
|
||||
public TypeParams set(Type t, int idx) {
|
||||
Type[] newparams = Arrays.copyOf(typeParams, typeParams.length);
|
||||
newparams[idx] = t;
|
||||
return new TypeParams(newparams);
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
public Iterator<Type> iterator() {
|
||||
return Arrays.stream(typeParams).iterator();
|
||||
63
src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
Normal file
63
src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
Normal file
@ -0,0 +1,63 @@
|
||||
package de.dhbwstuttgart.typeinference.unify.model;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.Map.Entry;
|
||||
import java.util.Set;
|
||||
import java.util.function.Function;
|
||||
|
||||
public class Unifier implements Function<Type, Type> {
|
||||
private HashMap<PlaceholderType, Type> substitutions = new HashMap<>();
|
||||
|
||||
public static Unifier IDENTITY = new Unifier();
|
||||
|
||||
public Unifier(PlaceholderType source, Type target) {
|
||||
substitutions.put(source, target);
|
||||
}
|
||||
|
||||
/**
|
||||
* Identity function as an "unifier".
|
||||
*/
|
||||
public Unifier() {
|
||||
|
||||
}
|
||||
|
||||
public void Add(PlaceholderType source, Type target) {
|
||||
Unifier tempU = new Unifier(source, target);
|
||||
for(PlaceholderType pt : substitutions.keySet())
|
||||
substitutions.put(pt, substitutions.get(pt).apply(tempU));
|
||||
substitutions.put(source, target);
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Type t) {
|
||||
return t.apply(this);
|
||||
}
|
||||
|
||||
public MPair apply(MPair p) {
|
||||
return new MPair(this.apply(p.getLhsType()), this.apply(p.getRhsType()), p.getPairOp());
|
||||
}
|
||||
|
||||
public boolean hasSubstitute(PlaceholderType t) {
|
||||
return substitutions.containsKey(t);
|
||||
}
|
||||
|
||||
public Type getSubstitute(Type t) {
|
||||
return substitutions.get(t);
|
||||
}
|
||||
|
||||
public Set<Entry<PlaceholderType, Type>> getSubstitutions() {
|
||||
return substitutions.entrySet();
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
String result = "{ ";
|
||||
for(Entry<PlaceholderType, Type> entry : substitutions.entrySet())
|
||||
result += "(" + entry.getKey() + " -> " + entry.getValue() + "), ";
|
||||
if(!substitutions.isEmpty())
|
||||
result = result.substring(0, result.length()-2);
|
||||
result += " }";
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
@ -2,68 +2,89 @@ package de.dhbwstuttgart.typeinference.unifynew;
|
||||
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType;
|
||||
import de.dhbwstuttgart.syntaxtree.type.FunN;
|
||||
import de.dhbwstuttgart.syntaxtree.type.RefType;
|
||||
import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType;
|
||||
import de.dhbwstuttgart.syntaxtree.type.Type;
|
||||
import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
|
||||
import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
|
||||
|
||||
/**
|
||||
* First three bits indicate the meta type:
|
||||
* 000b = 0 = Simpletype
|
||||
* 001b = 1 = Extends
|
||||
* 010b = 2 = Super
|
||||
* 011b = 3 = Type Placeholder
|
||||
* 100b = 4 = Function
|
||||
*
|
||||
* @author DH10STF
|
||||
*
|
||||
*/
|
||||
public class Mapping {
|
||||
|
||||
private static final int ST_MASK = 0;
|
||||
private static final int EXTENDS_MASK = 536870912;
|
||||
private static final int SUPER_MASK = 1073741824;
|
||||
private static final int TPH_MASK = 1610612736;
|
||||
private static final int FUN_MASK = -2147483648;
|
||||
private HashMap<de.dhbwstuttgart.typeinference.unify.model.Type, de.dhbwstuttgart.syntaxtree.type.Type> backwardMap = new HashMap<>();
|
||||
private HashMap<de.dhbwstuttgart.syntaxtree.type.Type, de.dhbwstuttgart.typeinference.unify.model.Type> forwardMap = new HashMap<>();
|
||||
private Set<de.dhbwstuttgart.typeinference.unify.model.Type> irreversible = new HashSet<>();
|
||||
|
||||
private static HashMap<Type, Type> mapping;
|
||||
|
||||
public Set<Type> createMapping(Iterable<Type> types) {
|
||||
mapping = new HashMap<>();
|
||||
|
||||
Iterator<Type> iterator = types.iterator();
|
||||
while(iterator.hasNext() && mapping.size() <= 536870911)
|
||||
createMapping(iterator.next());
|
||||
|
||||
return mapping.keySet();
|
||||
public Mapping(Set<de.dhbwstuttgart.syntaxtree.type.Type> types) {
|
||||
for(de.dhbwstuttgart.syntaxtree.type.Type t : types) {
|
||||
}
|
||||
}
|
||||
|
||||
private void createMapping(Type type) {
|
||||
/*if(type instanceof RefType) {
|
||||
Set<Type> params = ((RefType) type).get_ParaList();
|
||||
params.stream().forEach(x -> createMapping(x));
|
||||
public de.dhbwstuttgart.typeinference.unify.model.Type map(de.dhbwstuttgart.syntaxtree.type.Type type) {
|
||||
return forwardMap.get(type);
|
||||
}
|
||||
|
||||
public de.dhbwstuttgart.typeinference.unify.model.MPair map(de.dhbwstuttgart.typeinference.Pair pair) {
|
||||
return new de.dhbwstuttgart.typeinference.unify.model.MPair(forwardMap.get(pair.TA1), forwardMap.get(pair.TA2), mapOp(pair.GetOperator()));
|
||||
}
|
||||
|
||||
public Set<de.dhbwstuttgart.typeinference.unify.model.Type> mapTypeSet(Set<de.dhbwstuttgart.syntaxtree.type.Type> types) {
|
||||
return types.stream().map(this::map).collect(Collectors.toCollection(HashSet::new));
|
||||
}
|
||||
|
||||
public Set<de.dhbwstuttgart.typeinference.unify.model.MPair> mapPairSet(Set<de.dhbwstuttgart.typeinference.Pair> pairs) {
|
||||
return pairs.stream().map(this::map).collect(Collectors.toCollection(HashSet::new));
|
||||
}
|
||||
|
||||
public Optional<de.dhbwstuttgart.syntaxtree.type.Type> unmap(de.dhbwstuttgart.typeinference.unify.model.Type type) {
|
||||
return irreversible.contains(type) ? Optional.of(backwardMap.get(type)) : Optional.empty();
|
||||
}
|
||||
|
||||
public Optional<de.dhbwstuttgart.typeinference.Pair> unmap(de.dhbwstuttgart.typeinference.unify.model.MPair mpair) {
|
||||
de.dhbwstuttgart.typeinference.unify.model.Type lhs = mpair.getLhsType();
|
||||
de.dhbwstuttgart.typeinference.unify.model.Type rhs = mpair.getRhsType();
|
||||
|
||||
if(irreversible.contains(lhs) || irreversible.contains(rhs))
|
||||
return Optional.empty();
|
||||
return Optional.of(new de.dhbwstuttgart.typeinference.Pair(backwardMap.get(lhs), backwardMap.get(rhs), unmapOp(mpair.getPairOp())));
|
||||
}
|
||||
|
||||
public Optional<Set<de.dhbwstuttgart.syntaxtree.type.Type>> unmapTypeSet(Set<de.dhbwstuttgart.typeinference.unify.model.Type> types) {
|
||||
Set<de.dhbwstuttgart.syntaxtree.type.Type> result = types.stream().map(this::unmap).filter(x -> x.isPresent()).map(x -> x.get()).collect(Collectors.toCollection(HashSet::new));
|
||||
return result.size() == types.size() ? Optional.of(result) : Optional.empty();
|
||||
}
|
||||
|
||||
public Optional<Set<de.dhbwstuttgart.typeinference.Pair>> unmapPairSet(Set<de.dhbwstuttgart.typeinference.unify.model.MPair> pairs) {
|
||||
Set<de.dhbwstuttgart.typeinference.Pair> result = pairs.stream().map(this::unmap).filter(x -> x.isPresent()).map(x -> x.get()).collect(Collectors.toCollection(HashSet::new));
|
||||
return result.size() == pairs.size() ? Optional.of(result) : Optional.empty();
|
||||
}
|
||||
|
||||
private de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator mapOp(de.dhbwstuttgart.typeinference.Pair.PairOperator op) {
|
||||
/*
|
||||
* TODO
|
||||
* Warum hat der PairOp nur drei Werte? Wie wird SMALLERDOTWC etc im anderen Pair geregelt?
|
||||
*/
|
||||
int typeId = mapping.size();
|
||||
|
||||
if(type instanceof RefType)
|
||||
typeId |= ST_MASK;
|
||||
else if(type instanceof SuperWildcardType)
|
||||
typeId |= SUPER_MASK;
|
||||
else if(type instanceof ExtendsWildcardType)
|
||||
typeId |= EXTENDS_MASK;
|
||||
else if(type instanceof TypePlaceholder)
|
||||
typeId |= TPH_MASK;
|
||||
else if(type instanceof FunN)
|
||||
typeId |= FUN_MASK;
|
||||
switch(op) {
|
||||
case Equal:
|
||||
return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.EQUALS;
|
||||
case Smaller:
|
||||
return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.SMALLER;
|
||||
case SmallerExtends:
|
||||
return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.SMALLERDOT;
|
||||
default:
|
||||
return de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator.EQUALS;
|
||||
}
|
||||
}
|
||||
|
||||
//mapping.put(new MType())
|
||||
private de.dhbwstuttgart.typeinference.Pair.PairOperator unmapOp(de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator op) {
|
||||
switch(op) {
|
||||
case EQUALS:
|
||||
return de.dhbwstuttgart.typeinference.Pair.PairOperator.Equal;
|
||||
case SMALLER:
|
||||
return de.dhbwstuttgart.typeinference.Pair.PairOperator.Smaller;
|
||||
case SMALLERDOT:
|
||||
return de.dhbwstuttgart.typeinference.Pair.PairOperator.SmallerExtends;
|
||||
default:
|
||||
return de.dhbwstuttgart.typeinference.Pair.PairOperator.Equal;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -1,13 +1,21 @@
|
||||
package de.dhbwstuttgart.typeinference.unifynew;
|
||||
|
||||
import java.util.AbstractMap;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.Map.Entry;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
|
||||
/**
|
||||
* Implementation of the Martelli-Montanari unification algorithm.
|
||||
@ -16,65 +24,114 @@ import de.dhbwstuttgart.typinference.unify.model.TypeParams;
|
||||
public class MartelliMontanariUnify implements IUnify {
|
||||
|
||||
@Override
|
||||
public Unifier unify(Set<MPair> terms) {
|
||||
// TODO Auto-generated method stub
|
||||
return null;
|
||||
public Optional<Unifier> unify(Set<Type> terms) {
|
||||
if(terms.size() < 2)
|
||||
return Optional.of(Unifier.IDENTITY);
|
||||
|
||||
ArrayList<MPair> termsQ = new ArrayList<MPair>();
|
||||
Iterator<Type> iter = terms.iterator();
|
||||
Type prev = iter.next();
|
||||
while(iter.hasNext()) {
|
||||
Type next = iter.next();
|
||||
termsQ.add(new MPair(prev, next, PairOperator.EQUALS));
|
||||
prev = next;
|
||||
}
|
||||
|
||||
Unifier mgu = Unifier.IDENTITY;
|
||||
|
||||
int idx = 0;
|
||||
while(idx < termsQ.size()) {
|
||||
MPair pair = termsQ.get(idx);
|
||||
|
||||
if(delete(pair)) {
|
||||
termsQ.remove(idx);
|
||||
continue;
|
||||
}
|
||||
|
||||
Optional<Set<MPair>> optSet = decompose(pair);
|
||||
|
||||
if(optSet == null)
|
||||
return Optional.empty(); // Unification failed
|
||||
|
||||
if(optSet.isPresent()) {
|
||||
termsQ.addAll(optSet.get());
|
||||
idx = idx+1 == termsQ.size() ? 0 : idx+1;
|
||||
continue;
|
||||
}
|
||||
|
||||
Optional<MPair> optPair = swap(pair);
|
||||
|
||||
if(optPair.isPresent()) {
|
||||
termsQ.add(optPair.get());
|
||||
idx = idx+1 == termsQ.size() ? 0 : idx+1;
|
||||
continue;
|
||||
}
|
||||
|
||||
// Occurs-Check
|
||||
if(pair.getLhsType() instanceof PlaceholderType
|
||||
&& pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType()))
|
||||
return Optional.empty();
|
||||
|
||||
Optional<Entry<PlaceholderType, Type>> optUni = eliminate(pair);
|
||||
|
||||
if(optUni.isPresent()) {
|
||||
Entry<PlaceholderType, Type> substitution = optUni.get();
|
||||
mgu.Add(substitution.getKey(), substitution.getValue());
|
||||
termsQ = termsQ.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new));
|
||||
idx = idx+1 == termsQ.size() ? 0 : idx+1;
|
||||
continue;
|
||||
}
|
||||
|
||||
idx++;
|
||||
}
|
||||
|
||||
return Optional.of(mgu);
|
||||
}
|
||||
|
||||
private boolean delete(MPair pair) {
|
||||
return pair.getRhsType().equals(pair.getLhsType());
|
||||
}
|
||||
|
||||
private Set<MPair> decompose(MPair pair) {
|
||||
private Optional<Set<MPair>> decompose(MPair pair) {
|
||||
Set<MPair> result = new HashSet<>();
|
||||
|
||||
Type rhs = pair.getRhsType();
|
||||
Type lhs = pair.getLhsType();
|
||||
|
||||
if(!rhs.getName().equals(lhs.getName()) || rhs.getTypeParams().size() != lhs.getTypeParams().size())
|
||||
return null; // conflict
|
||||
|
||||
TypeParams rhsTypeParams = rhs.getTypeParams();
|
||||
TypeParams lhsTypeParams = lhs.getTypeParams();
|
||||
|
||||
if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
|
||||
return Optional.empty();
|
||||
|
||||
if(!rhs.getName().equals(lhs.getName()) || rhsTypeParams.size() != lhsTypeParams.size())
|
||||
return null; // conflict
|
||||
|
||||
for(int i = 0; i < rhsTypeParams.size(); i++)
|
||||
result.add(new MPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
|
||||
|
||||
return result;
|
||||
return Optional.of(result);
|
||||
}
|
||||
|
||||
private MPair swap(MPair pair) {
|
||||
private Optional<MPair> swap(MPair pair) {
|
||||
Type rhs = pair.getRhsType();
|
||||
Type lhs = pair.getLhsType();
|
||||
|
||||
if(lhs.getTypeParams().size() != 0 && rhs.getTypeParams().size() == 0)
|
||||
return new MPair(rhs, lhs, PairOperator.EQUALSDOT);
|
||||
return pair;
|
||||
if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType))
|
||||
return Optional.of(new MPair(rhs, lhs, PairOperator.EQUALSDOT));
|
||||
|
||||
return Optional.empty();
|
||||
}
|
||||
|
||||
private Unifier eliminate(MPair pair) {
|
||||
private Optional<Entry<PlaceholderType, Type>> eliminate(MPair pair) {
|
||||
Type rhs = pair.getRhsType();
|
||||
Type lhs = pair.getLhsType();
|
||||
|
||||
TypeParams rhsTypeParams = rhs.getTypeParams();
|
||||
// TODO only apply when lhs is element of vars(termsQ)?
|
||||
|
||||
for(Type t : rhsTypeParams)
|
||||
if(lhs.equals(t))
|
||||
return new Unifier(); //identity-"unifier"
|
||||
if(!(lhs instanceof PlaceholderType))
|
||||
return Optional.empty();
|
||||
|
||||
return new Unifier(lhs, rhs);
|
||||
}
|
||||
|
||||
private boolean check(MPair pair) {
|
||||
Type rhs = pair.getRhsType();
|
||||
Type lhs = pair.getLhsType();
|
||||
|
||||
TypeParams rhsTypeParams = rhs.getTypeParams();
|
||||
|
||||
for(Type t : rhsTypeParams)
|
||||
if(lhs.equals(t))
|
||||
return false;
|
||||
|
||||
return true;
|
||||
return Optional.of(new AbstractMap.SimpleImmutableEntry<PlaceholderType, Type>((PlaceholderType) lhs, rhs));
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,22 +1,27 @@
|
||||
package de.dhbwstuttgart.typeinference.unifynew;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashMap;
|
||||
import java.util.HashSet;
|
||||
import java.util.LinkedList;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
import java.util.Queue;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import junit.framework.Assert;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
|
||||
import de.dhbwstuttgart.typinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
|
||||
public class RuleSet implements IRuleSet{
|
||||
|
||||
@ -342,11 +347,11 @@ public class RuleSet implements IRuleSet{
|
||||
TypeParams typeDParams = typeD.getTypeParams();
|
||||
TypeParams typeDgenParams = typeDgen.getTypeParams();
|
||||
|
||||
Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0));
|
||||
Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
|
||||
for(int i = 1; i < typeDParams.size(); i++)
|
||||
unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
|
||||
unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)));
|
||||
|
||||
return Optional.of(new MPair(newLhs.apply(unif), typeDs, PairOperator.SMALLERDOT));
|
||||
return Optional.of(new MPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT));
|
||||
}
|
||||
|
||||
@Override
|
||||
@ -388,11 +393,11 @@ public class RuleSet implements IRuleSet{
|
||||
TypeParams typeDParams = typeD.getTypeParams();
|
||||
TypeParams typeDgenParams = typeDgen.getTypeParams();
|
||||
|
||||
Unifier unif = new Unifier(typeDgenParams.get(0), typeDParams.get(0));
|
||||
Unifier unif = new Unifier((PlaceholderType) typeDgenParams.get(0), typeDParams.get(0));
|
||||
for(int i = 1; i < typeDParams.size(); i++)
|
||||
unif.andThen(new Unifier(typeDgenParams.get(i), typeDParams.get(i)));
|
||||
unif.andThen(new Unifier((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i)));
|
||||
|
||||
return Optional.of(new MPair(newLhs.apply(unif), typeExtDs, PairOperator.SMALLERDOTWC));
|
||||
return Optional.of(new MPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC));
|
||||
}
|
||||
|
||||
@Override
|
||||
@ -440,11 +445,11 @@ public class RuleSet implements IRuleSet{
|
||||
TypeParams typeDParams = typeSupD.getTypeParams();
|
||||
TypeParams typeSupDsgenParams = typeSupDgen.getTypeParams();
|
||||
|
||||
Unifier unif = new Unifier(typeSupDsgenParams.get(0), typeDParams.get(0));
|
||||
Unifier unif = new Unifier((PlaceholderType) typeSupDsgenParams.get(0), typeDParams.get(0));
|
||||
for(int i = 1; i < typeDParams.size(); i++)
|
||||
unif.andThen(new Unifier(typeSupDsgenParams.get(i), typeDParams.get(i)));
|
||||
unif.andThen(new Unifier((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i)));
|
||||
|
||||
return Optional.of(new MPair(newLhs.apply(unif), newRhs, PairOperator.SMALLERDOTWC));
|
||||
return Optional.of(new MPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC));
|
||||
}
|
||||
|
||||
/**
|
||||
@ -516,9 +521,42 @@ public class RuleSet implements IRuleSet{
|
||||
}
|
||||
|
||||
@Override
|
||||
public Set<MPair> subst(Set<MPair> pair) {
|
||||
// TODO Auto-generated method stub
|
||||
return null;
|
||||
public Optional<Set<MPair>> subst(Set<MPair> pairs) {
|
||||
HashMap<Type, Integer> typeMap = new HashMap<>();
|
||||
|
||||
for(MPair pair : pairs) {
|
||||
Type t1 = pair.getLhsType();
|
||||
Type t2 = pair.getRhsType();
|
||||
if(!typeMap.containsKey(t1))
|
||||
typeMap.put(t1, 0);
|
||||
if(!typeMap.containsKey(t2))
|
||||
typeMap.put(t2, 0);
|
||||
typeMap.put(t1, typeMap.get(t1)+1);
|
||||
typeMap.put(t2, typeMap.get(t2)+1);
|
||||
}
|
||||
|
||||
ArrayList<MPair> result = new ArrayList<MPair>(pairs);
|
||||
|
||||
boolean applied = false;
|
||||
|
||||
for(int i = 0; i < result.size(); i++) {
|
||||
MPair pair = result.get(i);
|
||||
PlaceholderType lhsType = null;
|
||||
Type rhsType;
|
||||
|
||||
if(pair.getPairOp() == PairOperator.EQUALSDOT
|
||||
&& pair.getLhsType() instanceof PlaceholderType)
|
||||
lhsType = (PlaceholderType) pair.getLhsType();
|
||||
if(lhsType != null
|
||||
&& !((rhsType = pair.getRhsType()) instanceof PlaceholderType)
|
||||
&& typeMap.get(lhsType) > 1 // The type occurs in more pairs in the set than just the recent pair.
|
||||
&& !rhsType.getTypeParams().occurs(lhsType)) {
|
||||
Unifier uni = new Unifier(lhsType, rhsType);
|
||||
result = result.stream().map(uni::apply).collect(Collectors.toCollection(ArrayList::new));
|
||||
applied = true;
|
||||
}
|
||||
}
|
||||
|
||||
return applied ? Optional.of(new HashSet<>(result)) : Optional.empty();
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,36 +0,0 @@
|
||||
package de.dhbwstuttgart.typeinference.unifynew;
|
||||
|
||||
import java.util.function.Function;
|
||||
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typinference.unify.model.TypeParams;
|
||||
|
||||
public class Unifier implements Function<Type, Type> {
|
||||
private Type source;
|
||||
private Type target;
|
||||
|
||||
public Unifier(Type source, Type target) {
|
||||
this.source = source;
|
||||
this.target = target;
|
||||
}
|
||||
|
||||
/**
|
||||
* Identity function as an "unifier".
|
||||
*/
|
||||
public Unifier() {
|
||||
|
||||
}
|
||||
|
||||
@Override
|
||||
public Type apply(Type t) {
|
||||
return t.apply(this);
|
||||
}
|
||||
|
||||
public Type getSource() {
|
||||
return source;
|
||||
}
|
||||
|
||||
public Type getTarget() {
|
||||
return target;
|
||||
}
|
||||
}
|
||||
@ -1,11 +1,13 @@
|
||||
package de.dhbwstuttgart.typeinference.unifynew;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.Arrays;
|
||||
import java.util.Collection;
|
||||
import java.util.HashSet;
|
||||
import java.util.LinkedHashSet;
|
||||
import java.util.LinkedList;
|
||||
import java.util.List;
|
||||
import java.util.Map.Entry;
|
||||
import java.util.Optional;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
@ -16,12 +18,15 @@ import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
|
||||
import de.dhbwstuttgart.typinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Unifier;
|
||||
|
||||
|
||||
/**
|
||||
@ -30,7 +35,7 @@ import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
*/
|
||||
public class Unify {
|
||||
|
||||
public Menge<Menge<Pair>> unify(Set<MPair> eq, IFiniteClosure fc) {
|
||||
public Set<Set<MPair>> unify(Set<MPair> eq, IFiniteClosure fc) {
|
||||
/*
|
||||
* Step 1: Repeated application of reduce, adapt, erase, swap
|
||||
*/
|
||||
@ -47,14 +52,13 @@ public class Unify {
|
||||
|
||||
/*
|
||||
* Step 4: Create possible typings
|
||||
*
|
||||
* "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c)
|
||||
* mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
|
||||
*/
|
||||
|
||||
// Sets that originate from pair pattern matching
|
||||
// Sets of the "second level"
|
||||
List<List<Set<MPair>>> pairSetsSet = calculatePairSets(eq2s, fc);
|
||||
|
||||
// The sets of the "first level"
|
||||
Set<Set<?>> sets = new HashSet<Set<?>>();
|
||||
// All Sets
|
||||
List<Set<MPair>> sets = new ArrayList<Set<MPair>>();
|
||||
|
||||
if(eq1s.size() != 0)
|
||||
sets.add(eq1s); // Add Eq1'
|
||||
@ -67,41 +71,58 @@ public class Unify {
|
||||
if(bufferSet.size() != 0)
|
||||
sets.add(bufferSet);
|
||||
|
||||
// Sets that originate from pair pattern matching
|
||||
// Sets of the "second level"
|
||||
|
||||
sets.addAll(calculatePairSets(eq2s, fc));
|
||||
|
||||
/* Up to here, no cartesian products are calculated.
|
||||
* Around here, filters for pairs and sets can be applied */
|
||||
|
||||
ISetOperations setOps = new GuavaSetOperations();
|
||||
|
||||
// Calculate the inner cartesian products
|
||||
// Cartesian products of the second level
|
||||
// Calculate the cartesian products
|
||||
Set<Set<MPair>> result = setOps.cartesianProduct(sets).stream()
|
||||
.map(x -> new HashSet<MPair>(x)).collect(Collectors.toCollection(HashSet::new));
|
||||
//System.out.println(result);
|
||||
|
||||
// AddAll -> nur add
|
||||
for(List<Set<MPair>> pairSets : pairSetsSet) // Prüfen ob addAll stimmt oder ob hier eigentlich nur 1 set sein sollte
|
||||
sets.add(setOps.cartesianProduct(pairSets).stream().map(x -> new HashSet<>(x)).collect(Collectors.toSet()));
|
||||
|
||||
System.out.println(sets);
|
||||
|
||||
// Calculate the outer cartesian products
|
||||
// Cartesian products of the first level
|
||||
Set<List<Object>> eqsSet = setOps.cartesianProduct(new ArrayList<>(sets));
|
||||
|
||||
|
||||
System.out.println(eqsSet);
|
||||
/*
|
||||
* Step 5: Substitution
|
||||
*/
|
||||
|
||||
|
||||
/*
|
||||
* Step 6: a) Restart for pairs where subst was applied
|
||||
* b) Union over everything
|
||||
* TODO
|
||||
* Im Paper wird Eq'' genannt, es wird also von einer Menge in einer Menge in einer Menge ausgegangen.
|
||||
* Durch das flache Kartesische Produkt gibt es hier aber nur Mengen in Mengen.
|
||||
* Richtig so?
|
||||
*/
|
||||
|
||||
IRuleSet rules = new RuleSet(fc);
|
||||
Set<Set<MPair>> changed = new HashSet<>();
|
||||
Set<Set<MPair>> unchanged = new HashSet<>();
|
||||
|
||||
for(Set<MPair> eqss : result) {
|
||||
Optional<Set<MPair>> newEqss = rules.subst(eqss);
|
||||
if(newEqss.isPresent())
|
||||
changed.add(newEqss.get());
|
||||
else
|
||||
unchanged.add(eqss);
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* Step 7: Filter result for solved pairs
|
||||
* Step 6 a) Restart for pairs where subst was applied
|
||||
* b) Build the union over everything
|
||||
*/
|
||||
|
||||
return null;
|
||||
for(Set<MPair> eqss : changed)
|
||||
unchanged.addAll(this.unify(eqss, fc));
|
||||
|
||||
/*
|
||||
* Step 7: Filter result for solved pairs TODO wie?
|
||||
*/
|
||||
|
||||
return unchanged;
|
||||
|
||||
}
|
||||
|
||||
@ -196,11 +217,8 @@ public class Unify {
|
||||
}
|
||||
|
||||
|
||||
protected List<List<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
|
||||
List<List<Set<MPair>>> result = new ArrayList<List<Set<MPair>>>();
|
||||
for(int i = 0; i < 8; i++)
|
||||
result.add(new ArrayList<Set<MPair>>());
|
||||
|
||||
protected List<Set<MPair>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
|
||||
List<Set<MPair>> result = new ArrayList<Set<MPair>>();
|
||||
|
||||
for(MPair pair : eq2s) {
|
||||
|
||||
@ -210,12 +228,52 @@ public class Unify {
|
||||
|
||||
// Case 1: (a <. Theta')
|
||||
if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
|
||||
// TODO
|
||||
Type thetaPrime = pair.getRhsType();
|
||||
Set<MPair> set = new HashSet<>();
|
||||
IUnify unify = new MartelliMontanariUnify();
|
||||
|
||||
//Set<Type> cs = fc.getAllTypes(rhsType.getName());
|
||||
Type c = rhsType;
|
||||
|
||||
//Set<Type> thetaQs = cs.stream().flatMap(x -> fc.smaller(x).stream()).collect(Collectors.toCollection(HashSet::new));
|
||||
Set<Type> thetaQs = fc.smaller(c);
|
||||
|
||||
Set<Type> thetaQPrimes = new HashSet<>();
|
||||
|
||||
TypeParams cParams = c.getTypeParams();
|
||||
if(cParams.size() == 0)
|
||||
thetaQPrimes.add(c);
|
||||
else {
|
||||
ArrayList<Set<Type>> candidateParams = new ArrayList<>();
|
||||
for(Type param : cParams)
|
||||
candidateParams.add(fc.grArg(param));
|
||||
Set<TypeParams> permutations = new HashSet<TypeParams>();
|
||||
permuteParams(candidateParams, 0, permutations, new Type[candidateParams.size()]);
|
||||
|
||||
for(TypeParams tp : permutations)
|
||||
thetaQPrimes.add(c.setTypeParams(tp));
|
||||
}
|
||||
|
||||
for(Type tqp : thetaQPrimes) {
|
||||
Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
|
||||
if(opt.isPresent()) {
|
||||
Unifier unifier = opt.get();
|
||||
Set<Entry<PlaceholderType, Type>> substitutions = unifier.getSubstitutions();
|
||||
for(Entry<PlaceholderType, Type> sigma : substitutions)
|
||||
set.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
|
||||
for(Type tq : thetaQs) {
|
||||
Set<Type> smaller = fc.smaller(unifier.apply(tq));
|
||||
smaller.stream().map(x -> new MPair(lhsType, x, PairOperator.EQUALSDOT)).forEach(x -> set.add(x));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
result.add(set);
|
||||
}
|
||||
|
||||
// Case 2: (a <.? ? ext Theta')
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType){
|
||||
// TODO
|
||||
throw new NotImplementedException(); // TODO
|
||||
}
|
||||
|
||||
// Case 3: (a <.? ? sup Theta')
|
||||
@ -223,15 +281,14 @@ public class Unify {
|
||||
Set<MPair> set = new HashSet<>();
|
||||
for(Type theta : fc.smArg(rhsType))
|
||||
set.add(new MPair(lhsType, theta, PairOperator.EQUALSDOT));
|
||||
|
||||
result.get(2).add(set);
|
||||
result.add(set);
|
||||
}
|
||||
|
||||
// Case 4: (a <.? Theta')
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType) {
|
||||
Set<MPair> set = new HashSet<>();
|
||||
set.add(new MPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.EQUALSDOT));
|
||||
result.get(3).add(set);
|
||||
set.add(new MPair(lhsType, rhsType, PairOperator.EQUALSDOT));
|
||||
result.add(set);
|
||||
}
|
||||
|
||||
// Case 5: (Theta <. a)
|
||||
@ -239,7 +296,7 @@ public class Unify {
|
||||
Set<MPair> set = new HashSet<>();
|
||||
for(Type thetaS : fc.greater(lhsType))
|
||||
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
|
||||
result.get(4).add(set);
|
||||
result.add(set);
|
||||
}
|
||||
|
||||
// Case 6: (? ext Theta <.? a)
|
||||
@ -247,12 +304,12 @@ public class Unify {
|
||||
Set<MPair> set = new HashSet<>();
|
||||
for(Type thetaS : fc.grArg(lhsType))
|
||||
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
|
||||
result.get(5).add(set);
|
||||
result.add(set);
|
||||
}
|
||||
|
||||
// Case 7: (? sup Theta <.? a)
|
||||
else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType) {
|
||||
// TODO
|
||||
throw new NotImplementedException(); // TODO
|
||||
}
|
||||
|
||||
// Case 8: (Theta <.? a)
|
||||
@ -260,10 +317,33 @@ public class Unify {
|
||||
Set<MPair> set = new HashSet<>();
|
||||
for(Type thetaS : fc.grArg(lhsType))
|
||||
set.add(new MPair(rhsType, thetaS, PairOperator.EQUALSDOT));
|
||||
result.get(7).add(set);
|
||||
result.add(set);
|
||||
}
|
||||
}
|
||||
|
||||
return result.stream().filter(x -> !x.isEmpty()).collect(Collectors.toList());
|
||||
return result;
|
||||
}
|
||||
|
||||
protected void permuteParams(ArrayList<Set<Type>> candidates, int idx, Set<TypeParams> result, Type[] current) {
|
||||
if(candidates.size() == idx) {
|
||||
result.add(new TypeParams(Arrays.copyOf(current, current.length)));
|
||||
return;
|
||||
}
|
||||
|
||||
Set<Type> localCandidates = candidates.get(idx);
|
||||
|
||||
for(Type t : localCandidates) {
|
||||
current[idx] = t;
|
||||
permuteParams(candidates, idx+1, result, current);
|
||||
}
|
||||
}
|
||||
|
||||
private Set<Type> getAllInstantiations(Type t, IFiniteClosure fc) {
|
||||
Set<Type> result = new HashSet<>();
|
||||
result.add(t);
|
||||
return result;
|
||||
|
||||
// TODO
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -4,10 +4,10 @@ import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typinference.unify.model.FiniteClosure;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
|
||||
public class FiniteClosureBuilder {
|
||||
|
||||
|
||||
@ -6,8 +6,9 @@ import java.util.Set;
|
||||
import org.junit.Test;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
|
||||
public class FiniteClosureTest {
|
||||
|
||||
@ -54,4 +55,10 @@ public class FiniteClosureTest {
|
||||
System.out.println("SmArg(? extends List<T>) = " + fc.smArg(tf.getExtendsType(tf.getSimpleType("List", "T"))));
|
||||
System.out.println("SmArg(? super List<T>) = " + fc.smArg(tf.getSuperType(tf.getSimpleType("List", "T"))));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void testGetGenericType() {
|
||||
|
||||
// TODO
|
||||
}
|
||||
}
|
||||
|
||||
@ -9,12 +9,12 @@ import junit.framework.Assert;
|
||||
import org.junit.Test;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.RuleSet;
|
||||
import de.dhbwstuttgart.typinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SuperType;
|
||||
|
||||
|
||||
public class RuleSetTest {
|
||||
|
||||
66
test/unify/StandardUnifyTest.java
Normal file
66
test/unify/StandardUnifyTest.java
Normal file
@ -0,0 +1,66 @@
|
||||
package unify;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
import junit.framework.Assert;
|
||||
|
||||
import org.junit.Test;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify;
|
||||
|
||||
public class StandardUnifyTest {
|
||||
|
||||
@Test
|
||||
public void testUnify() {
|
||||
IUnify unify = new MartelliMontanariUnify();
|
||||
TypeFactory tf = new TypeFactory();
|
||||
|
||||
/*
|
||||
* Positive Tests
|
||||
*/
|
||||
|
||||
Type x = tf.getPlaceholderType("x");
|
||||
Type y = tf.getPlaceholderType("y");
|
||||
Type f = tf.getSimpleType("f", x);
|
||||
|
||||
// {f<x> = y}
|
||||
Set<MPair> terms = new HashSet<MPair>();
|
||||
|
||||
System.out.println(unify.unify(f, y).get());
|
||||
|
||||
// TODO ist das ergebnis { (x -> ? extends a), (y -> g<x>) } in der richtigen form oder
|
||||
// muss es { (x -> ? extends a), (y -> g<? extends a>) } sein?
|
||||
// {f<g<x>,x> = f<y, ? extends a>}
|
||||
Type g = tf.getSimpleType("g", "x");
|
||||
Type f1 = tf.getSimpleType("f", g, x);
|
||||
Type a = tf.getExtendsType(tf.getPlaceholderType("a"));
|
||||
Type f2 = tf.getSimpleType("f", y, a);
|
||||
|
||||
terms = new HashSet<>();
|
||||
|
||||
System.out.println(unify.unify(f1, f2).get());
|
||||
|
||||
/*
|
||||
* Negative Tests
|
||||
*/
|
||||
|
||||
// {f(x) =. x}
|
||||
f = tf.getSimpleType("f", x);
|
||||
Assert.assertFalse(unify.unify(f, x).isPresent());
|
||||
|
||||
// {f(x) =. f(x,y)}
|
||||
f1 = tf.getSimpleType("f", "x");
|
||||
f2 = tf.getSimpleType("f", "x", "y");
|
||||
Assert.assertFalse(unify.unify(f1, f2).isPresent());
|
||||
|
||||
// {f(x) =. g(x)}
|
||||
f1 = tf.getSimpleType("f", "x");
|
||||
f2 = tf.getSimpleType("g", "x");
|
||||
Assert.assertFalse(unify.unify(f1, f2).isPresent());
|
||||
}
|
||||
}
|
||||
@ -3,11 +3,11 @@ package unify;
|
||||
import java.util.Arrays;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
import de.dhbwstuttgart.typinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SimpleType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.SuperType;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
|
||||
public class TypeFactory {
|
||||
|
||||
|
||||
@ -1,14 +1,17 @@
|
||||
package unify;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
import org.junit.Test;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.Type;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
|
||||
import de.dhbwstuttgart.typeinference.unifynew.Unify;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair;
|
||||
import de.dhbwstuttgart.typinference.unify.model.MPair.PairOperator;
|
||||
|
||||
public class UnifyTest extends Unify {
|
||||
|
||||
@ -18,25 +21,29 @@ public class UnifyTest extends Unify {
|
||||
FiniteClosureBuilder fcb = new FiniteClosureBuilder();
|
||||
Set<MPair> eq = new HashSet<MPair>();
|
||||
|
||||
fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object"));
|
||||
//fcb.add(tf.getSimpleType("Number"), tf.getSimpleType("Object"));
|
||||
fcb.add(tf.getSimpleType("Integer"), tf.getSimpleType("Number"));
|
||||
fcb.add(tf.getSimpleType("Double"), tf.getSimpleType("Number"));
|
||||
//fcb.add(tf.getSimpleType("List", "T"));
|
||||
|
||||
IFiniteClosure fc = fcb.getCollectionExample();
|
||||
|
||||
// Vector<Integer> <. Vector<A>
|
||||
// Vector<Integer <. Vector<C>
|
||||
// A <. Number
|
||||
// A <. Integer
|
||||
// Number <. A
|
||||
// Double <. B
|
||||
// B <. Object
|
||||
eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
|
||||
eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT));
|
||||
eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("Number"), PairOperator.SMALLERDOT));
|
||||
//eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Number")), tf.getSimpleType("Vector", "A"), PairOperator.SMALLERDOT));
|
||||
//eq.add(new MPair(tf.getSimpleType("Vector", tf.getSimpleType("Integer")), tf.getSimpleType("Vector", "C"), PairOperator.SMALLERDOT));
|
||||
eq.add(new MPair(tf.getPlaceholderType("A"), tf.getSimpleType("List", tf.getSimpleType("Number")), PairOperator.SMALLERDOT));
|
||||
//eq.add(new MPair(tf.getSimpleType("Number"), tf.getPlaceholderType("A"), PairOperator.SMALLERDOT));
|
||||
//eq.add(new MPair(tf.getPlaceholderType("A"), tf.getPlaceholderType("C"), PairOperator.SMALLERDOT));
|
||||
eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT));
|
||||
eq.add(new MPair(tf.getPlaceholderType("B"), tf.getSimpleType("Object"), PairOperator.EQUALSDOT));
|
||||
//eq.add(new MPair(tf.getSimpleType("Double"), tf.getPlaceholderType("B"), PairOperator.SMALLERDOT));
|
||||
//eq.add(new MPair(tf.getPlaceholderType("B"), tf.getSimpleType("Object"), PairOperator.EQUALSDOT));
|
||||
|
||||
this.unify(eq, fc);
|
||||
System.out.println(this.unify(eq, fc));
|
||||
|
||||
}
|
||||
|
||||
@ -50,4 +57,32 @@ public class UnifyTest extends Unify {
|
||||
|
||||
}
|
||||
|
||||
@Test
|
||||
public void permuteParamsTest() {
|
||||
TypeFactory tf = new TypeFactory();
|
||||
ArrayList<Set<Type>> candidates = new ArrayList<>();
|
||||
|
||||
Set<Type> p1 = new HashSet<>();
|
||||
p1.add(tf.getPlaceholderType("p11"));
|
||||
p1.add(tf.getExtendsType(tf.getSimpleType("p12")));
|
||||
p1.add(tf.getSimpleType("p13"));
|
||||
|
||||
Set<Type> p2 = new HashSet<>();
|
||||
p2.add(tf.getPlaceholderType("p21"));
|
||||
p2.add(tf.getPlaceholderType("p22"));
|
||||
|
||||
Set<Type> p3 = new HashSet<>();
|
||||
p3.add(tf.getSimpleType("p31", "T"));
|
||||
p3.add(tf.getSimpleType("p32"));
|
||||
|
||||
candidates.add(p1);
|
||||
candidates.add(p2);
|
||||
candidates.add(p3);
|
||||
|
||||
Set<TypeParams> result = new HashSet<>();
|
||||
permuteParams(candidates, 0, result, new Type[candidates.size()]);
|
||||
|
||||
System.out.println(result);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user