forked from i21017/JavaCompilerCore
109 lines
3.6 KiB
Java
109 lines
3.6 KiB
Java
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.IUnify;
|
|
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 the Martelli-Montanari unification algorithm.
|
|
* @author Florian Steurer
|
|
*/
|
|
public class MartelliMontanariUnify implements IUnify {
|
|
|
|
@Override
|
|
public Optional<Unifier> unify(Set<UnifyType> terms) {
|
|
// Sets with less than 2 terms are trivially unified
|
|
if(terms.size() < 2)
|
|
return Optional.of(Unifier.identity());
|
|
|
|
// For the the set of terms {t1,...,tn},
|
|
// build a list of equations {(t1 = t2), (t2 = t3), (t3 = t4), ....}
|
|
ArrayList<UnifyPair> termsList = new ArrayList<UnifyPair>();
|
|
Iterator<UnifyType> iter = terms.iterator();
|
|
UnifyType prev = iter.next();
|
|
while(iter.hasNext()) {
|
|
UnifyType next = iter.next();
|
|
termsList.add(new UnifyPair(prev, next, PairOperator.EQUALSDOT));
|
|
prev = next;
|
|
}
|
|
|
|
// 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(rhsTypeParams.get(i), lhsTypeParams.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)) {
|
|
termsList.remove(idx);
|
|
termsList.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT));
|
|
continue;
|
|
}
|
|
|
|
// OCCURS-CHECK
|
|
if(pair.getLhsType() instanceof PlaceholderType
|
|
&& pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType()))
|
|
return Optional.empty();
|
|
|
|
// SUBST - Rule
|
|
if(lhsType instanceof PlaceholderType) {
|
|
mgu.add((PlaceholderType) lhsType, rhsType);
|
|
//PL 2018-04-01 nach checken, ob es richtig ist, dass keine Substitutionen uebergeben werden muessen.
|
|
termsList.replaceAll(mgu::apply);
|
|
idx = idx+1 == termsList.size() ? 0 : idx+1;
|
|
continue;
|
|
}
|
|
|
|
idx++;
|
|
}
|
|
|
|
return Optional.of(mgu);
|
|
}
|
|
}
|