refactored standard unification

This commit is contained in:
Florian Steurer 2016-04-11 09:56:06 +02:00
parent 64247b689b
commit 5dd90cb30c
2 changed files with 31 additions and 71 deletions

View File

@ -42,27 +42,38 @@ public class MartelliMontanariUnify implements IUnify {
int idx = 0;
while(idx < termsQ.size()) {
UnifyPair pair = termsQ.get(idx);
UnifyType rhsType = pair.getRhsType();
UnifyType lhsType = pair.getLhsType();
TypeParams rhsTypeParams = rhsType.getTypeParams();
TypeParams lhsTypeParams = lhsType.getTypeParams();
if(delete(pair)) {
// DELETE
if(pair.getRhsType().equals(pair.getLhsType())) {
termsQ.remove(idx);
continue;
}
Optional<Set<UnifyPair>> optSet = decompose(pair);
if(optSet == null)
return Optional.empty(); // Unification failed
if(optSet.isPresent()) {
termsQ.addAll(optSet.get());
// REDUCE
if(!(rhsType instanceof PlaceholderType) && !(lhsType instanceof PlaceholderType)
&& (rhsTypeParams.size() != 0 || lhsTypeParams.size() != 0)) {
Set<UnifyPair> result = new HashSet<>();
if(!rhsType.getName().equals(lhsType.getName()))
return Optional.empty(); // conflict
if(rhsTypeParams.size() != lhsTypeParams.size())
return Optional.empty(); // conflict
for(int i = 0; i < rhsTypeParams.size(); i++)
result.add(new UnifyPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
termsQ.addAll(result);
idx = idx+1 == termsQ.size() ? 0 : idx+1;
continue;
}
Optional<UnifyPair> optPair = swap(pair);
if(optPair.isPresent()) {
termsQ.add(optPair.get());
// SWAP
if(!(lhsType instanceof PlaceholderType) && (rhsType instanceof PlaceholderType)) {
termsQ.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT));
idx = idx+1 == termsQ.size() ? 0 : idx+1;
continue;
}
@ -72,11 +83,9 @@ public class MartelliMontanariUnify implements IUnify {
&& pair.getRhsType().getTypeParams().occurs((PlaceholderType) pair.getLhsType()))
return Optional.empty();
Optional<Entry<PlaceholderType, UnifyType>> optUni = eliminate(pair);
if(optUni.isPresent()) {
Entry<PlaceholderType, UnifyType> substitution = optUni.get();
mgu.Add(substitution.getKey(), substitution.getValue());
// SUBST
if(lhsType instanceof PlaceholderType) {
mgu.Add((PlaceholderType) lhsType, rhsType);
termsQ = termsQ.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new));
idx = idx+1 == termsQ.size() ? 0 : idx+1;
continue;
@ -87,55 +96,4 @@ public class MartelliMontanariUnify implements IUnify {
return Optional.of(mgu);
}
private boolean delete(UnifyPair pair) {
return pair.getRhsType().equals(pair.getLhsType());
}
private Optional<Set<UnifyPair>> decompose(UnifyPair pair) {
Set<UnifyPair> result = new HashSet<>();
UnifyType rhs = pair.getRhsType();
UnifyType lhs = pair.getLhsType();
TypeParams rhsTypeParams = rhs.getTypeParams();
TypeParams lhsTypeParams = lhs.getTypeParams();
if(!(rhs instanceof PlaceholderType) && !(lhs instanceof PlaceholderType)) {
if(!rhs.getName().equals(lhs.getName()))
return null; // conflict
if(rhsTypeParams.size() != lhsTypeParams.size())
return null; // conflict;
}
if(rhsTypeParams.size() == 0 || lhsTypeParams.size() == 0)
return Optional.empty();
for(int i = 0; i < rhsTypeParams.size(); i++)
result.add(new UnifyPair(rhsTypeParams.get(i), lhsTypeParams.get(i), PairOperator.EQUALSDOT));
return Optional.of(result);
}
private Optional<UnifyPair> swap(UnifyPair pair) {
UnifyType rhs = pair.getRhsType();
UnifyType lhs = pair.getLhsType();
if(!(lhs instanceof PlaceholderType) && (rhs instanceof PlaceholderType))
return Optional.of(new UnifyPair(rhs, lhs, PairOperator.EQUALSDOT));
return Optional.empty();
}
private Optional<Entry<PlaceholderType, UnifyType>> eliminate(UnifyPair pair) {
UnifyType rhs = pair.getRhsType();
UnifyType lhs = pair.getLhsType();
// TODO only apply when lhs is element of vars(termsQ)?
if(!(lhs instanceof PlaceholderType))
return Optional.empty();
return Optional.of(new AbstractMap.SimpleImmutableEntry<PlaceholderType, UnifyType>((PlaceholderType) lhs, rhs));
}
}

View File

@ -347,7 +347,7 @@ public class Unify {
* TODO Optimierungsmöglichkeit:
*
* An dieser Stelle gibt es Raum für Optimierung.
* Z.B. resultiert (a <. C<Integer>) durch Permutation der Parameter mit grArg in:
* Z.B. resultiert (a <. C<Integer>) durch Permutation der Parameter mit grArg und smaller in:
* (a = C<b'>, b' <.? ? extends Number)
* (a = C<b'>, b' <.? ? extends Integer)
* (a = C<b'>, b' <.? Integer)
@ -357,7 +357,9 @@ public class Unify {
* rekursiven Aufruf des Unify. Es würde reichen nur den allgemeinsten Fall zu betrachten da dieser den Lösungraum
* der anderen Fälle miteinschließt.
*
* (Gibt es einen einzigen maximalen fall? Wsl. ? super x (x möglichst klein) und ? ext y (y möglichst groß))
* Prüfen:
* Gibt es einen einzigen maximalen Fall?
* Wahrscheinlich gibt es 2: ? super x (x möglichst klein) und ? ext y (y möglichst groß))
*/
for(UnifyType param : cParams)