unify case 1

This commit is contained in:
Florian Steurer 2016-03-17 16:35:33 +01:00
parent d19a79bd63
commit fa9627b883
3 changed files with 36 additions and 31 deletions

View File

@ -144,6 +144,7 @@ public class FiniteClosure implements IFiniteClosure {
return new HashSet<Type>();
Set<Type> result = new HashSet<Type>();
result.add(type);
Type t = type.getExtendedType();
@ -158,6 +159,7 @@ public class FiniteClosure implements IFiniteClosure {
return new HashSet<Type>();
Set<Type> result = new HashSet<Type>();
result.add(type);
Type t = type.getSuperedType();
@ -194,6 +196,7 @@ public class FiniteClosure implements IFiniteClosure {
return new HashSet<Type>();
Set<Type> result = new HashSet<Type>();
result.add(type);
Type t = type.getExtendedType();
@ -213,6 +216,7 @@ public class FiniteClosure implements IFiniteClosure {
return new HashSet<Type>();
Set<Type> result = new HashSet<Type>();
result.add(type);
Type t = type.getSuperedType();

View File

@ -232,38 +232,39 @@ public class Unify {
Set<MPair> set = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
//Set<Type> cs = fc.getAllTypes(rhsType.getName());
Type c = rhsType;
Set<Type> cs = fc.getAllTypes(rhsType.getName());
//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()]);
Set<Type> thetaQs = cs.stream().flatMap(
x -> fc.smaller(x).stream().filter(y -> y.getTypeParams().arePlaceholders())
).collect(Collectors.toCollection(HashSet::new));
for(Type c : cs) {
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(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));
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));
}
}
}
}

View File

@ -38,7 +38,7 @@ public class UnifyTest extends Unify {
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("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.getPlaceholderType("A"), 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));