diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala index e313976..1eb8fd9 100644 --- a/src/main/scala/unify/algorithm/Rules.scala +++ b/src/main/scala/unify/algorithm/Rules.scala @@ -32,10 +32,10 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact cs.add(EqualsDot(left, crunch(RefType(wcs, n, params)))) case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Remove if (right.wtvs().isEmpty) { //Subst - if (!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty) { + if (!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty && cs.notProcessed(left)) { cs.remove(cons) cs.substitute(cons.right, cons.left) - cs.addUnifier(cons) + cs.addProcessedUnifier(left) } else { // TODO: insolvable } diff --git a/src/main/scala/unify/algorithm/Unify.scala b/src/main/scala/unify/algorithm/Unify.scala index 4796c73..91b64ad 100644 --- a/src/main/scala/unify/algorithm/Unify.scala +++ b/src/main/scala/unify/algorithm/Unify.scala @@ -1,12 +1,11 @@ package unify.algorithm -import unify.model.{ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, Wildcard, WildcardBound, WildcardEnvironment, WildcardFactory, emptyWCs} +import unify.model.{BotType, ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, Wildcard, WildcardBound, WildcardEnvironment, WildcardFactory, emptyWCs} import java.util.concurrent.{CompletableFuture, ExecutorService, Future} import scala.collection.mutable class Unify { - /** * The steps transforming the constraint set (including substitution) * but without branching into multiple constraint sets @@ -106,22 +105,20 @@ class Unify { //Clean up step //Ground rule - val alessT = cs.getALessDotCCons.filter(c => cs.isOnlyLowerBound(c.left.asInstanceOf[TypeVariable])) - if(alessT.size > 0) { - alessT.map(cons => { - cs.groundRule(cons) - }) - } + val alessT = cs.getALessDotCCons.filter(c => { + cs.isOnlyLowerBound(c.left.asInstanceOf[TypeVariable]) + }).map(cons => { + cs.remove(cons) + cs.substitute(BotType(), cons.left) + cs.add(EqualsDot(cons.left, BotType())) + }) + //SubElim rule cs.getALessDotBCons.map(cons => { cs.remove(cons) cs.substitute(cons.left, cons.right) - cs.addUnifier(EqualsDot(cons.right, cons.left)) + cs.add(EqualsDot(cons.right, cons.left)) }) - if(cs.isSolvedForm){ - cs.solvedForm() - }else{ - None - } + cs.solvedForm() } } diff --git a/src/main/scala/unify/model/ConstraintSet.scala b/src/main/scala/unify/model/ConstraintSet.scala index ff77ac4..4b2be79 100644 --- a/src/main/scala/unify/model/ConstraintSet.scala +++ b/src/main/scala/unify/model/ConstraintSet.scala @@ -1,15 +1,16 @@ package unify.model -class ConstraintSet( private var unifier: Set[EqualsDot] = Set(), +class ConstraintSet( private var processedUnifier: Set[TypeVariable] = Set(), private var lessdot: Set[LessDot] = Set(), private var equalsdot: Set[EqualsDot] = Set(), private var bounds: WildcardEnvironment = emptyWCs(), - private var processed: Set[(TypePlaceholder, TypePlaceholder)] = Set(), + private var processedAdopt: Set[(TypePlaceholder, TypePlaceholder)] = Set(), private var changed: Boolean = false) { - def notProcessed(a: TypePlaceholder, b: TypePlaceholder): Boolean = !processed.contains((a,b)) + def notProcessed(a: TypePlaceholder, b: TypePlaceholder): Boolean = !processedAdopt.contains((a,b)) + def notProcessed(a: TypeVariable): Boolean = !processedUnifier.contains(a) def setProcessedByAdopt(a: TypePlaceholder, b: TypePlaceholder): Unit = { - processed = processed + ((a, b)) + processedAdopt = processedAdopt + ((a, b)) } def wildcardEnv = bounds /* @@ -31,6 +32,8 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(), def getALessDotCCons: Set[LessDot] = getLessDotCons.filter(c => c.left.isInstanceOf[TypeVariable] && c.right.isInstanceOf[RefType]) + def getAllConstraints: Set[Constraint] = getLessDotCons ++ getEqualsDotCons + def removeAll(cons: Iterable[Constraint]) : Unit = cons.foreach(remove(_)) def remove(cons: Constraint): Unit = { cons match { @@ -47,9 +50,8 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(), } changed = true } - def addUnifier(c: EqualsDot) = { - changed = true - unifier = unifier + c + def addProcessedUnifier(a: TypeVariable) = { + processedUnifier += a } def substitute(withType: Type, toSubstitute: Type): Unit = { def substituteWCB(wcb: WildcardBound) = @@ -76,20 +78,68 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(), lessdot = getLessDotCons.map(c => { LessDot(substitute(c.left), substitute(c.right)) }) - unifier = unifier.map(c => { - EqualsDot(substitute(c.left), substitute(c.right)) - }) this.bounds = WildcardEnvironment(this.bounds.map(substituteWCB)) changed = true } + /** + * Checks if a type variable is used as lower bound and nowhere else + * This means, that the type variable is only present in a <. T constraints on the left side + * and not used as an upper bound in wildcards + */ + def isOnlyLowerBound(tv: TypeVariable): Boolean = { + val alessdotT: Set[Constraint] = getLessDotCons.filter(cons => cons.left.equals(tv) && !cons.right.tvs().contains(tv)).toSet + val tvIsOnlyInAlessdotTCons = getAllConstraints.filter(!alessdotT.contains(_)).find(cons => cons.left.tvs().contains(tv) || cons.right.tvs().contains(tv)).isEmpty + bounds.map(_.lower.tvs()).flatten.contains(tv) && tvIsOnlyInAlessdotTCons && !bounds.map(_.upper.tvs()).flatten.contains(tv) + } + def copy(): ConstraintSet = { val ret = ConstraintSet() - ret.processed = processed + ret.processedUnifier = processedUnifier ret.lessdot = lessdot ret.equalsdot = equalsdot - ret.unifier = unifier + ret.processedAdopt = processedAdopt ret.bounds = new WildcardEnvironment(bounds.getWCBounds) ret } + def solvedForm(): Option[UnifySolution] = { + var sigma = Map[TypeVariable, Type]() + var delta: Set[WildcardBound] = Set() + + //GenDelta + while + getLessDotCons.filter(_.left.isInstanceOf[TypePlaceholder]).find(c => c.right.tvs().isEmpty && c.right.wtvs().isEmpty + && c.right.fvs().filter(wc => delta.find(_.name == wc.name).isEmpty).isEmpty //No free Variables (except those in Delta) + && (c.left.isInstanceOf[WTypeVariable] || !sigma.contains(c.left.asInstanceOf[TypeVariable])) + ).map(c => { + if(c.left.isInstanceOf[WTypeVariable]){ //GenDelta' + val B = Wildcard("X" + c.left.asInstanceOf[WTypeVariable].name) + delta += WildcardBound(B.name, c.right, BotType()) + this.remove(c) + this.substitute(B, c.left) + }else{ + val B = Wildcard("X" + c.left.asInstanceOf[TypeVariable].name) + sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> B) + delta += WildcardBound(B.name, c.right, BotType()) + this.remove(c) + this.substitute(B, c.left) + } + }).isDefined + do () + + + //GenSigma + val toRemove = getEqualsDotCons.filter(_.left.isInstanceOf[TypeVariable]).find(c => c.right.tvs().isEmpty && c.right.wtvs().isEmpty + && sigma.contains(c.left.asInstanceOf[TypeVariable])).map(c => { + sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> c.right) + this.remove(c) + }) + + if (this.getAllConstraints.isEmpty) { + val ret = new UnifySolution(WildcardEnvironment(delta), sigma) + Some(ret) + } else { + None + } + } } diff --git a/src/main/scala/unify/model/ExtendsRelations.scala b/src/main/scala/unify/model/ExtendsRelations.scala index 6f7fb71..5d373ef 100644 --- a/src/main/scala/unify/model/ExtendsRelations.scala +++ b/src/main/scala/unify/model/ExtendsRelations.scala @@ -6,9 +6,7 @@ class ExtendsRelations(val extendsRelations : Set[(RefType, RefType)]): def isPossibleSupertype(of: String, superType: String): Boolean = { if (of.equals(superType)) return true - if(extendsRelations.contains(of)){ - isPossibleSupertype(superType(of), superType) - }else{ - false - } + extendsRelations.find(r => r._1.name.equals(of)) // check if supertype exists + .map(_ => isPossibleSupertype(supertype(of)._2.name, superType)) + .getOrElse(false) } diff --git a/src/main/scala/unify/model/UnifySolution.scala b/src/main/scala/unify/model/UnifySolution.scala index 442abab..56d104f 100644 --- a/src/main/scala/unify/model/UnifySolution.scala +++ b/src/main/scala/unify/model/UnifySolution.scala @@ -3,7 +3,7 @@ package unify.model class UnifySolution(delta: WildcardEnvironment, sigma: Map[TypeVariable, Type]) { def getDelta() = delta override def toString: String = - "Δ = " + delta.map(wc => wc._1.name + ":["+wc._2._1.toString + ".."+wc._2._2.toString + "]").mkString("{",", ", "}") + + "Δ = " + delta.map(wc => wc.name + ":["+wc.lower + ".."+wc.upper + "]").mkString("{",", ", "}") + ", σ = " + sigma.toString() def getSigma = sigma