Add GenDelta, AddSigma

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
             }

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()
   }
 }

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
+    }
+  }
 }

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)
   }

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