Start LessDot-Rules

src/main/scala/unify/algorithm/Rules.scala

@@ -3,8 +3,9 @@ package unify.algorithm
 import unify.model.{ExtendsRelations, LessDot}
 
 import unify.model.*
+import java.lang.reflect.WildcardType
 
-class Rules(cs: ConstraintSet, deltaIn: WildcardEnvironment, wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
+class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
   def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
     cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
       cons match {
@@ -44,16 +45,93 @@ class Rules(cs: ConstraintSet, deltaIn: WildcardEnvironment, wildcardEnvironment
       }
     })
     cs.getLessDotCons.foreach(cons => cons match {
-      case LessDot(left: Wildcard, right: (RefType|TypeVariable|Wildcard)) =>
+      case LessDot(a, b, _) if a == b => cs.remove(cons) //Erase
+      case LessDot(left: Wildcard, right: (RefType|TypeVariable|Wildcard), cc) => // Upper
         cs.remove(cons)
-        cs.add(LessDot(wildcardEnvironment.getUpperBound(left), right))
-      case LessDot(left: (RefType|TypeVariable|Wildcard), right: Wildcard) if !deltaIn.getWildcards().contains(right) =>
+        cs.add(LessDot(wildcardEnvironment.getUpperBound(left), right, cc))
+      case LessDot(left: (RefType | Wildcard), right: Wildcard, cc) => // Lower
         cs.remove(cons)
         cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
+      case LessDot(left: TypeVariable, right: Wildcard, cc) if !deltaIn.contains(right) => // Lower
+        cs.remove(cons)
+        cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
+      case LessDot(left: BotType, right: Type, _) => cs.remove(cons) //Bot
+      case LessDot(left, right: BotType, _) => // TODO: insolvable constraint set!
+      case LessDot(left : (RefType | Wildcard), right: BotType, _) => // TODO: insolvable constraint set!
+      case LessDot(left : TypePlaceholder, right : BotType, _) =>
+        cs.remove(cons)
+        cs.add(EqualsDot(left, right))
+      case LessDot(left : TypePlaceholder, right : TypePlaceholder, _) =>
+        val circle = findCircle(cons.left.asInstanceOf[TypeVariable], cs.getALessDotBCons)
+        if (!circle.isEmpty) {
+          cs.removeAll(circle)
+          cs.addAll(circle.map(c => EqualsDot(c.left, c.right)))
+        }
+      case LessDot(left: TypePlaceholder, right: RefType, cc) =>
+        val alessdotc = cs.getALessDotCCons
+          //match rule:
+          alessdotc.find(ic => (ic != cons && cons.left.equals(cons.left))).map(ic =>{
+            if(fc.isPossibleSupertype(cons.right.asInstanceOf[RefType].name, ic.right.asInstanceOf[RefType].name)){
+              matchRule(cons, ic, cs, tvFactory)
+            }else{
+              //TODO: insolvable constraint set!
+            }
+          })
+      case LessDot(RefType(wc, n, params), right: RefType, cc) if right.fvs().diff(deltaIn).isEmpty | cc > 0 => // Capture und Prepare
+        cs.remove(cons)
+        cs.add(LessDot(RefType(emptyWCs(), n, params), right, cc))
+          
         
     })
   }
 
+  /**
+   * @param c1 a <. C
+   * @param c2 a <. D
+   *           It's important that C < D
+   */
+  private def matchRule(c1: LessDot, c2: LessDot, cs: ConstraintSet, tvFactory: TypeVariableFactory) = {
+    cs.remove(c1)
+    cs.remove(c2)
+
+    val wcFactory = new WildcardFactory()
+    val freshWildcards = c1.right.asInstanceOf[RefType].params.map(_ => WildcardBound(wcFactory.freshName(), tvFactory.freshTV(), tvFactory.freshTV()))
+    cs.addAll(freshWildcards.map(wc => LessDot(wc.lower, wc.upper)))
+    val freshSubtype = RefType(new WildcardEnvironment(freshWildcards.toSet),
+      c1.right.asInstanceOf[RefType].name,
+      freshWildcards.map(wc => Wildcard(wc.name)))
+    cs.add(LessDot(c1.left, freshSubtype))
+    cs.add(LessDot(freshSubtype, c1.right))
+    cs.add(LessDot(freshSubtype, c2.right))
+  }
+
+  private def findCircle(start: TypeVariable, aUnifyLessDota: Set[LessDot]): List[LessDot]
+  = findCircleRec(start, Set(start), aUnifyLessDota)
+
+  private def findCircleRec(next: TypeVariable, visited: Set[TypeVariable], aUnifyLessDota: Set[LessDot]): List[LessDot]
+  = {
+    def getRightSides(of: TypeVariable) = {
+      aUnifyLessDota.filter(c => c.left.equals(of))
+    }
+
+    val rightSides = getRightSides(next).iterator
+    while (rightSides.hasNext) { //Deep search
+      val rightSide = rightSides.next()
+      val nextTV = rightSide.right.asInstanceOf[TypeVariable]
+      if (visited.contains(nextTV)) {
+        return List(rightSide) //
+      } else {
+        val circle = findCircleRec(nextTV, visited + nextTV, aUnifyLessDota)
+        if (circle.isEmpty) {
+          return List() // empty list means there are no circles
+        } else {
+          return rightSide :: circle
+        }
+      }
+    }
+    List() // empty list means there are no circles
+  }
+
   def swap(cons: EqualsDot) = {
     cs.remove(cons)
     cs.add(EqualsDot(cons.right, cons.left))

src/main/scala/unify/model/Constraint.scala

@@ -1,12 +1,9 @@
 package unify.model
 
 sealed abstract class Constraint(val left: Type, val right: Type)
-final case class LessDot(override val left: Type, override val right: Type) extends Constraint(left, right){
+sealed case class LessDot(override val left: Type, override val right: Type, ccNum : Int = 0) extends Constraint(left, right){
   override def toString: String = left.toString + " <. " + right.toString
 }
-final case class LessDotCC(override val left: Type, override val right: Type) extends Constraint(left, right){
-  override def toString: String = left.toString + " <c " + right.toString
-}
 final case class EqualsDot(override val left: Type, override val right: Type) extends Constraint(left, right){
   override def toString: String = left.toString + " =. " + right.toString
 }

src/main/scala/unify/model/ConstraintSet.scala

@@ -4,25 +4,35 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
                      private var lessdot: Set[LessDot] = Set(),
                      private var equalsdot: Set[EqualsDot] = Set(),
                      private var bounds: WildcardEnvironment,
-                     private var lessdotCC : List[LessDotCC] = List(),
                      private var changed: Boolean = false) {
 
+  /*
+  The Subtype-Constraints flagged as capture constraints are saved in lessdotCC.
+  lessdotCC is a list. there can be multiple T <c S constraints. Removing one leaves the other one in the set.
+  This is intentional
+   */
+
   def getEqualsDotCons = equalsdot
+
   def getLessDotCons: Set[LessDot] = lessdot
 
+  def getALessDotBCons: Set[LessDot] = getLessDotCons.filter(c => c.left.isInstanceOf[TypeVariable] && c.right.isInstanceOf[TypeVariable])
+
+  def getALessDotCCons: Set[LessDot] = getLessDotCons.filter(c => c.left.isInstanceOf[TypeVariable] && c.right.isInstanceOf[RefType])
+
+  def removeAll(cons: Iterable[Constraint]) : Unit = cons.foreach(remove(_))
   def remove(cons: Constraint): Unit = {
     cons match {
       case EqualsDot(l, r) => equalsdot -= (EqualsDot(l, r))
-      case LessDot(l, r) => lessdot -= LessDot(l, r)
-      case LessDotCC(left, right) => lessdotCC.diff(List(LessDotCC(left, right)))
+      case LessDot(l, r, cc) => lessdot -= LessDot(l, r, cc)
     }
     changed = true
   }
+  def addAll(cons: Iterable[Constraint]) : Unit = cons.foreach(add(_))
   def add(cons: Constraint): Unit = {
     cons match {
       case EqualsDot(l, r) => equalsdot += (EqualsDot(l, r))
-      case LessDot(l, r) => lessdot += (LessDot(l, r))
-      case LessDotCC(l, r) => lessdotCC = LessDotCC(l,r) :: lessdotCC
+      case LessDot(l, r, cc) => lessdot += (LessDot(l, r, cc))
     }
     changed = true
   }

src/main/scala/unify/model/WildcardEnvironment.scala

@@ -16,3 +16,5 @@ class WildcardEnvironment(wcBounds: Set[WildcardBound]) {
 
   def getWildcards() = wcBounds.map(wcb => Wildcard(wcb.name))
 }
+
+def emptyWCs() : WildcardEnvironment = new WildcardEnvironment(Set())

src/main/scala/unify/model/WildcardFactory.scala

@@ -0,0 +1,13 @@
+package unify.model
+
+import java.util.concurrent.atomic.AtomicInteger
+
+class WildcardFactory {
+
+  val tpvNum = new AtomicInteger()
+
+  def freshName() = {
+    val current = tpvNum.incrementAndGet()
+    current.toString
+  }
+}