made the ruleSet interface functional (added fc in arguments)

This commit is contained in:
Florian Steurer 2016-04-13 11:13:20 +02:00
parent d8e7df425d
commit ae9220c04b
3 changed files with 49 additions and 60 deletions

View File

@ -30,17 +30,7 @@ import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
* @author Florian Steurer * @author Florian Steurer
* *
*/ */
public class RuleSet implements IRuleSet{ public class RuleSet implements IRuleSet{
protected IFiniteClosure finiteClosure;
/**
* Creates a new instance that uses the specified FC for greater, grArg, etc.
* @param fc The FC that is used for greater, grArg, etc.
*/
public RuleSet(IFiniteClosure fc) {
finiteClosure = fc;
}
@Override @Override
public Optional<UnifyPair> reduceUp(UnifyPair pair) { public Optional<UnifyPair> reduceUp(UnifyPair pair) {
@ -97,7 +87,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair) { public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOTWC) if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
return Optional.empty(); return Optional.empty();
@ -119,7 +109,7 @@ public class RuleSet implements IRuleSet{
if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size()) if(x.getTypeParams().empty() || extY.getTypeParams().size() != x.getTypeParams().size())
return Optional.empty(); return Optional.empty();
UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
return Optional.empty(); return Optional.empty();
@ -127,7 +117,7 @@ public class RuleSet implements IRuleSet{
if(x instanceof ExtendsType) if(x instanceof ExtendsType)
xFromFc = new ExtendsType(xFromFc); xFromFc = new ExtendsType(xFromFc);
UnifyType extYFromFc = finiteClosure.grArg(xFromFc).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); UnifyType extYFromFc = fc.grArg(xFromFc).stream().filter(t -> t.getName().equals(extY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
if(extYFromFc == null || extYFromFc.getTypeParams() != xFromFc.getTypeParams()) if(extYFromFc == null || extYFromFc.getTypeParams() != xFromFc.getTypeParams())
return Optional.empty(); return Optional.empty();
@ -149,7 +139,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair) { public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOTWC) if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
return Optional.empty(); return Optional.empty();
@ -171,7 +161,7 @@ public class RuleSet implements IRuleSet{
if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size()) if(x.getTypeParams().empty() || supY.getTypeParams().size() != x.getTypeParams().size())
return Optional.empty(); return Optional.empty();
UnifyType xFromFc = finiteClosure.getLeftHandedType(sTypeX.getName()).orElse(null); UnifyType xFromFc = fc.getLeftHandedType(sTypeX.getName()).orElse(null);
if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders()) if(xFromFc == null || !xFromFc.getTypeParams().arePlaceholders())
return Optional.empty(); return Optional.empty();
@ -179,7 +169,7 @@ public class RuleSet implements IRuleSet{
if(x instanceof SuperType) if(x instanceof SuperType)
xFromFc = new SuperType(xFromFc); xFromFc = new SuperType(xFromFc);
UnifyType supYFromFc = finiteClosure.grArg(xFromFc).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null); UnifyType supYFromFc = fc.grArg(xFromFc).stream().filter(t -> t.getName().equals(supY.getName())).filter(t -> t.getTypeParams().arePlaceholders()).findAny().orElse(null);
if(supYFromFc == null || supYFromFc.getTypeParams() != xFromFc.getTypeParams()) if(supYFromFc == null || supYFromFc.getTypeParams() != xFromFc.getTypeParams())
return Optional.empty(); return Optional.empty();
@ -231,7 +221,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<Set<UnifyPair>> reduce1(UnifyPair pair) { public Optional<Set<UnifyPair>> reduce1(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOT) if(pair.getPairOp() != PairOperator.SMALLERDOT)
return Optional.empty(); return Optional.empty();
@ -249,12 +239,12 @@ public class RuleSet implements IRuleSet{
if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size()) if(lhsSType.getTypeParams().empty() || lhsSType.getTypeParams().size() != rhsSType.getTypeParams().size())
return Optional.empty(); return Optional.empty();
UnifyType cFromFc = finiteClosure.getLeftHandedType(c.getName()).orElse(null); UnifyType cFromFc = fc.getLeftHandedType(c.getName()).orElse(null);
if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders()) if(cFromFc == null || !cFromFc.getTypeParams().arePlaceholders())
return Optional.empty(); return Optional.empty();
UnifyType dFromFc = finiteClosure.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null); UnifyType dFromFc = fc.getAncestors(cFromFc).stream().filter(x -> x.getName().equals(d.getName())).findAny().orElse(null);
if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size()) if(dFromFc == null || !dFromFc.getTypeParams().arePlaceholders() || dFromFc.getTypeParams().size() != cFromFc.getTypeParams().size())
return Optional.empty(); return Optional.empty();
@ -330,7 +320,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public boolean erase1(UnifyPair pair) { public boolean erase1(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOT) if(pair.getPairOp() != PairOperator.SMALLERDOT)
return false; return false;
@ -342,18 +332,18 @@ public class RuleSet implements IRuleSet{
if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType)) if(!(rhsType instanceof ReferenceType) && !(rhsType instanceof PlaceholderType))
return false; return false;
return finiteClosure.greater(lhsType).contains(rhsType); return fc.greater(lhsType).contains(rhsType);
} }
@Override @Override
public boolean erase2(UnifyPair pair) { public boolean erase2(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOTWC) if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
return false; return false;
UnifyType lhsType = pair.getLhsType(); UnifyType lhsType = pair.getLhsType();
UnifyType rhsType = pair.getRhsType(); UnifyType rhsType = pair.getRhsType();
return finiteClosure.grArg(lhsType).contains(rhsType); return fc.grArg(lhsType).contains(rhsType);
} }
@Override @Override
@ -379,7 +369,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<UnifyPair> adapt(UnifyPair pair) { public Optional<UnifyPair> adapt(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOT) if(pair.getPairOp() != PairOperator.SMALLERDOT)
return Optional.empty(); return Optional.empty();
@ -398,7 +388,7 @@ public class RuleSet implements IRuleSet{
return Optional.empty(); return Optional.empty();
Optional<UnifyType> opt = finiteClosure.getLeftHandedType(typeD.getName()); Optional<UnifyType> opt = fc.getLeftHandedType(typeD.getName());
if(!opt.isPresent()) if(!opt.isPresent())
return Optional.empty(); return Optional.empty();
@ -406,7 +396,7 @@ public class RuleSet implements IRuleSet{
UnifyType typeDgen = opt.get(); UnifyType typeDgen = opt.get();
// Actually greater+ because the types are ensured to have different names // Actually greater+ because the types are ensured to have different names
Set<UnifyType> greater = finiteClosure.getAncestors(typeDgen); Set<UnifyType> greater = fc.getAncestors(typeDgen);
opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); opt = greater.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();
if(!opt.isPresent()) if(!opt.isPresent())
@ -425,7 +415,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<UnifyPair> adaptExt(UnifyPair pair) { public Optional<UnifyPair> adaptExt(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOTWC) if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
return Optional.empty(); return Optional.empty();
@ -442,16 +432,16 @@ public class RuleSet implements IRuleSet{
UnifyType typeDgen; UnifyType typeDgen;
if(typeD instanceof ReferenceType) if(typeD instanceof ReferenceType)
typeDgen = finiteClosure.getLeftHandedType(typeD.getName()).orElse(null); typeDgen = fc.getLeftHandedType(typeD.getName()).orElse(null);
else { else {
Optional<UnifyType> opt = finiteClosure.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName()); Optional<UnifyType> opt = fc.getLeftHandedType(((ExtendsType) typeD).getExtendedType().getName());
typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null; typeDgen = opt.isPresent() ? new ExtendsType(opt.get()) : null;
} }
if(typeDgen == null) if(typeDgen == null)
return Optional.empty(); return Optional.empty();
Set<UnifyType> grArg = finiteClosure.grArg(typeDgen); Set<UnifyType> grArg = fc.grArg(typeDgen);
Optional<UnifyType> opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny(); Optional<UnifyType> opt = grArg.stream().filter(x -> x.getName().equals(typeExtDs.getName())).findAny();
@ -471,7 +461,7 @@ public class RuleSet implements IRuleSet{
} }
@Override @Override
public Optional<UnifyPair> adaptSup(UnifyPair pair) { public Optional<UnifyPair> adaptSup(UnifyPair pair, IFiniteClosure fc) {
if(pair.getPairOp() != PairOperator.SMALLERDOTWC) if(pair.getPairOp() != PairOperator.SMALLERDOTWC)
return Optional.empty(); return Optional.empty();
@ -487,7 +477,7 @@ public class RuleSet implements IRuleSet{
return Optional.empty(); return Optional.empty();
Optional<UnifyType> opt = finiteClosure.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName()); Optional<UnifyType> opt = fc.getLeftHandedType(((SuperType) typeSupD).getSuperedType().getName());
if(!opt.isPresent()) if(!opt.isPresent())
return Optional.empty(); return Optional.empty();
@ -497,7 +487,7 @@ public class RuleSet implements IRuleSet{
// Use of smArg instead of grArg because // Use of smArg instead of grArg because
// a in grArg(b) => b in smArg(a) // a in grArg(b) => b in smArg(a)
Set<UnifyType> smArg = finiteClosure.smArg(typeSupDgen); Set<UnifyType> smArg = fc.smArg(typeSupDgen);
opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny(); opt = smArg.stream().filter(x -> x.getName().equals(typeDs.getName())).findAny();
if(!opt.isPresent()) if(!opt.isPresent())

View File

@ -33,7 +33,9 @@ import de.dhbwstuttgart.typeinference.unify.model.Unifier;
public class Unify { public class Unify {
protected ISetOperations setOps = new GuavaSetOperations(); protected ISetOperations setOps = new GuavaSetOperations();
protected IUnify stdUnify = new MartelliMontanariUnify();
protected IRuleSet rules = new RuleSet();
public Set<Set<UnifyPair>> unify(Set<UnifyPair> eq, IFiniteClosure fc) { public Set<Set<UnifyPair>> unify(Set<UnifyPair> eq, IFiniteClosure fc) {
/* /*
* Step 1: Repeated application of reduce, adapt, erase, swap * Step 1: Repeated application of reduce, adapt, erase, swap
@ -123,7 +125,6 @@ public class Unify {
eqPrimeSetFlat.add(buffer); eqPrimeSetFlat.add(buffer);
} }
IRuleSet rules = new RuleSet(fc);
Set<Set<UnifyPair>> restartSet = new HashSet<>(); Set<Set<UnifyPair>> restartSet = new HashSet<>();
Set<Set<UnifyPair>> eqPrimePrimeSet = new HashSet<>(); Set<Set<UnifyPair>> eqPrimePrimeSet = new HashSet<>();
@ -193,12 +194,11 @@ public class Unify {
LinkedHashSet<UnifyPair> targetSet = new LinkedHashSet<UnifyPair>(); LinkedHashSet<UnifyPair> targetSet = new LinkedHashSet<UnifyPair>();
LinkedList<UnifyPair> eqQueue = new LinkedList<>(); LinkedList<UnifyPair> eqQueue = new LinkedList<>();
IRuleSet rules = new RuleSet(fc);
/* /*
* Swap all pairs and erase all erasable pairs * Swap all pairs and erase all erasable pairs
*/ */
eq.forEach(x -> swapAddOrErase(x, rules, eqQueue)); eq.forEach(x -> swapAddOrErase(x, fc, eqQueue));
/* /*
* Apply rules until the queue is empty * Apply rules until the queue is empty
@ -220,31 +220,31 @@ public class Unify {
// One of the rules has been applied // One of the rules has been applied
if(opt.isPresent()) { if(opt.isPresent()) {
swapAddOrErase(opt.get(), rules, eqQueue); swapAddOrErase(opt.get(), fc, eqQueue);
continue; continue;
} }
// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq // Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
Optional<Set<UnifyPair>> optSet = rules.reduce1(pair); Optional<Set<UnifyPair>> optSet = rules.reduce1(pair, fc);
optSet = optSet.isPresent() ? optSet : rules.reduce2(pair); optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair); optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair, fc);
optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair); optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair, fc);
optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair); optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair);
// One of the rules has been applied // One of the rules has been applied
if(optSet.isPresent()) { if(optSet.isPresent()) {
optSet.get().forEach(x -> swapAddOrErase(x, rules, eqQueue)); optSet.get().forEach(x -> swapAddOrErase(x, fc, eqQueue));
continue; continue;
} }
// Adapt, AdaptExt, AdaptSup // Adapt, AdaptExt, AdaptSup
opt = rules.adapt(pair); opt = rules.adapt(pair, fc);
opt = opt.isPresent() ? opt : rules.adaptExt(pair); opt = opt.isPresent() ? opt : rules.adaptExt(pair, fc);
opt = opt.isPresent() ? opt : rules.adaptSup(pair); opt = opt.isPresent() ? opt : rules.adaptSup(pair, fc);
// One of the rules has been applied // One of the rules has been applied
if(opt.isPresent()) { if(opt.isPresent()) {
swapAddOrErase(opt.get(), rules, eqQueue); swapAddOrErase(opt.get(), fc, eqQueue);
continue; continue;
} }
@ -255,11 +255,11 @@ public class Unify {
return targetSet; return targetSet;
} }
protected void swapAddOrErase(UnifyPair pair, IRuleSet rules, Collection<UnifyPair> collection) { protected void swapAddOrErase(UnifyPair pair, IFiniteClosure fc, Collection<UnifyPair> collection) {
Optional<UnifyPair> opt = rules.swap(pair); Optional<UnifyPair> opt = rules.swap(pair);
UnifyPair pair2 = opt.isPresent() ? opt.get() : pair; UnifyPair pair2 = opt.isPresent() ? opt.get() : pair;
if(rules.erase1(pair2) || rules.erase3(pair2) || rules.erase2(pair2)) if(rules.erase1(pair2, fc) || rules.erase3(pair2) || rules.erase2(pair2, fc))
return; return;
collection.add(pair2); collection.add(pair2);
@ -332,8 +332,7 @@ public class Unify {
protected Set<Set<UnifyPair>> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) { protected Set<Set<UnifyPair>> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
Set<Set<UnifyPair>> result = new HashSet<>(); Set<Set<UnifyPair>> result = new HashSet<>();
IUnify unify = new MartelliMontanariUnify();
Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName()); Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
cs.add(thetaPrime); cs.add(thetaPrime);
@ -375,7 +374,7 @@ public class Unify {
} }
for(UnifyType tqp : thetaQPrimes) { for(UnifyType tqp : thetaQPrimes) {
Optional<Unifier> opt = unify.unify(tqp, thetaPrime); Optional<Unifier> opt = stdUnify.unify(tqp, thetaPrime);
if (!opt.isPresent()) if (!opt.isPresent())
continue; continue;

View File

@ -14,10 +14,10 @@ public interface IRuleSet {
public Optional<UnifyPair> reduceUp(UnifyPair pair); public Optional<UnifyPair> reduceUp(UnifyPair pair);
public Optional<UnifyPair> reduceLow(UnifyPair pair); public Optional<UnifyPair> reduceLow(UnifyPair pair);
public Optional<UnifyPair> reduceUpLow(UnifyPair pair); public Optional<UnifyPair> reduceUpLow(UnifyPair pair);
public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair); public Optional<Set<UnifyPair>> reduceExt(UnifyPair pair, IFiniteClosure fc);
public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair); public Optional<Set<UnifyPair>> reduceSup(UnifyPair pair, IFiniteClosure fc);
public Optional<Set<UnifyPair>> reduceEq(UnifyPair pair); public Optional<Set<UnifyPair>> reduceEq(UnifyPair pair);
public Optional<Set<UnifyPair>> reduce1(UnifyPair pair); public Optional<Set<UnifyPair>> reduce1(UnifyPair pair, IFiniteClosure fc);
public Optional<Set<UnifyPair>> reduce2(UnifyPair pair); public Optional<Set<UnifyPair>> reduce2(UnifyPair pair);
/* /*
@ -42,13 +42,13 @@ public interface IRuleSet {
* Checks whether the erase1-Rule applies to the pair. * Checks whether the erase1-Rule applies to the pair.
* @return True if the pair is erasable, false otherwise. * @return True if the pair is erasable, false otherwise.
*/ */
public boolean erase1(UnifyPair pair); public boolean erase1(UnifyPair pair, IFiniteClosure fc);
/** /**
* Checks whether the erase2-Rule applies to the pair. * Checks whether the erase2-Rule applies to the pair.
* @return True if the pair is erasable, false otherwise. * @return True if the pair is erasable, false otherwise.
*/ */
public boolean erase2(UnifyPair pair); public boolean erase2(UnifyPair pair, IFiniteClosure fc);
/** /**
* Checks whether the erase3-Rule applies to the pair. * Checks whether the erase3-Rule applies to the pair.
@ -58,9 +58,9 @@ public interface IRuleSet {
public Optional<UnifyPair> swap(UnifyPair pair); public Optional<UnifyPair> swap(UnifyPair pair);
public Optional<UnifyPair> adapt(UnifyPair pair); public Optional<UnifyPair> adapt(UnifyPair pair, IFiniteClosure fc);
public Optional<UnifyPair> adaptExt(UnifyPair pair); public Optional<UnifyPair> adaptExt(UnifyPair pair, IFiniteClosure fc);
public Optional<UnifyPair> adaptSup(UnifyPair pair); public Optional<UnifyPair> adaptSup(UnifyPair pair, IFiniteClosure fc);
/** /**
* Applies the subst-Rule to a set of pairs (usually Eq'). * Applies the subst-Rule to a set of pairs (usually Eq').