Implement Subst, Remove, Subst-WC

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

@@ -6,19 +6,26 @@ import unify.model.*
 
 class Rules(cs: ConstraintSet, wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
   def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
-    cs.getEqualsDotCons.foreach(cons => {
+    cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
       if (cons.left.equals(cons.right)) { //erase rule
         cs.remove(cons)
-        return
+      } else if(cons.left.isInstanceOf[TypeVariable] && cons.right.wtvs().isEmpty){ //Subst rule
+        val left = cons.left.asInstanceOf[TypeVariable]
+        if(!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty){
+          cs.remove(cons)
+          cs.substitute(cons.right, cons.left)
+          cs.addUnifier(cons)
+        }else{
+          // TODO: insolvable
+        }
+      } else if(cons.left.isInstanceOf[TypeVariable] && !cons.right.wtvs().isEmpty) { //Remove rule
+        cons.right.wtvs().foreach(wtv => cs.substitute(tvFactory.freshTV(), wtv))
+      } else if(cons.left.isInstanceOf[WTypeVariable]){ // Subst-WC rule
+        cs.remove(cons)
+        cs.substitute(cons.right, cons.left)
       }
-      else if (cons.left.isInstanceOf[Wildcard] && cons.right.isInstanceOf[Wildcard]) {
-        normalizeRule(cons, cs)
-        return
-      }
-      else if (cons.left.isInstanceOf[Wildcard] && !cons.right.isInstanceOf[WTypeVariable]) {
-      //Tame rule:
-      tameRule(cons, cs)
-      return
+      else if (cons.left.isInstanceOf[Wildcard] && !cons.right.isInstanceOf[WTypeVariable]) { //Tame rule:
+        tameRule(cons, cs)
       }else if(cons.left.isInstanceOf[RefType] && cons.right.isInstanceOf[RefType]){
         val left = cons.left.asInstanceOf[RefType]
         val right = cons.right.asInstanceOf[RefType]
@@ -60,15 +67,6 @@ class Rules(cs: ConstraintSet, wildcardEnvironment: WildcardEnvironment, fc: Ext
     })
   }
 
-  private def normalizeRule(cons: EqualsDot, cs: ConstraintSet): Unit = {
-    cs.remove(cons)
-    val left = cons.left.asInstanceOf[Wildcard]
-    val right = cons.right.asInstanceOf[Wildcard]
-    cs.add(EqualsDot(wildcardEnvironment.getLowerBound(left), wildcardEnvironment.getUpperBound(left)))
-    cs.add(EqualsDot(wildcardEnvironment.getLowerBound(right), wildcardEnvironment.getUpperBound(right)))
-    cs.add(EqualsDot(wildcardEnvironment.getLowerBound(left), wildcardEnvironment.getUpperBound(right)))
-  }
-
   def tameRule(cons: EqualsDot, cs: ConstraintSet) = {
     cs.remove(cons)
     val left = cons.left.asInstanceOf[Wildcard]

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

@@ -26,7 +26,10 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
     }
     changed = true
   }
-
+  def addUnifier(c: EqualsDot) = {
+    changed = true
+    unifier = unifier + c
+  }
   def substitute(withType: Type, toSubstitute: Type): Unit = {
     def substituteWCB(wcb: WildcardBound) =
       WildcardBound(wcb.name, substitute(wcb.upper), substitute(wcb.upper))

src/main/scala/unify/model/ExtendsRelations.scala

@@ -7,7 +7,7 @@ class ExtendsRelations(val extendsRelations : Set[(RefType, RefType)]):
   def isPossibleSupertype(of: String, superType: String): Boolean = {
     if (of.equals(superType)) return true
     extendsRelations.map(p => {
-      return false
+      //TODO
     })
     false
   }

src/main/scala/unify/model/Type.scala

@@ -1,17 +1,30 @@
 package unify.model
 
 sealed abstract class Type:
-  def tvs(t: Type): Set[TypeVariable] = t match {
+  def tvs(): Set[TypeVariable] = this match {
     case TypeVariable(a) => Set(TypeVariable(a))
-    case RefType(wildcards, name, params) => params.flatMap(tvs).toSet
+    case RefType(wildcards, name, params) => params.flatMap(_.tvs()).toSet
     case _ => Set()
   }
-  def wtvs(t: Type): Set[WTypeVariable] = t match {
+  def wtvs(): Set[WTypeVariable] = this match {
     case WTypeVariable(a) => Set(WTypeVariable(a))
-    case RefType(wildcards, name, params) => params.flatMap(wtvs).toSet
+    case RefType(wildcards, name, params) => params.flatMap(_.wtvs()).toSet
     case _ => Set()
   }
 
+  def fvs(): Set[Wildcard] = {
+    def wildcards(t: Type): Set[Wildcard] = t match {
+      case Wildcard(name) => Set(Wildcard(name))
+      case RefType(_, _, params) => params.flatMap(wildcards).toSet
+      case _ => Set()
+    }
+    this match {
+      case RefType(wcs, name, params) => wildcards(this) -- wcs.getWildcards()
+      case Wildcard(name) => Set(Wildcard(name))
+      case _ => Set()
+    }
+  }
+
 final case class RefType(wildcards: WildcardEnvironment, name: String, params: List[Type]) extends Type{
   override def toString: String = {
     var ret = ""

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

@@ -13,4 +13,6 @@ class WildcardEnvironment(wcBounds: Set[WildcardBound]) {
   def map(f : WildcardBound => WildcardBound): WildcardEnvironment = {
     WildcardEnvironment(wcBounds.map(f))
   }
+
+  def getWildcards() = wcBounds.map(wcb => Wildcard(wcb.name))
 }