Add Reduce rule. Add substitute to Type. Change map of WildcardEnvironment

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

@@ -80,8 +80,12 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
       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))
-          
-        
+      case LessDot(RefType(wcNull, n1, p1), RefType(wcs, n2, p2), cc) if wcNull.isEmpty & n1 == n2 & p1.size == p2.size =>
+        cs.remove(cons)
+        val freshTVMap: Map[Type,Type] = wcs.map(wcb => (Wildcard(wcb.name) -> tvFactory.freshWTV())).toMap
+        cs.addAll(p1.zip(p2.map(_.substitute(freshTVMap))).map(p => EqualsDot(p._1, p._2)))
+        cs.addAll(wcs.map(wcb => LessDot(Wildcard(wcb.name).substitute(freshTVMap), wcb.upper.substitute(freshTVMap))))
+        cs.addAll(wcs.map(wcb => LessDot(wcb.lower.substitute(freshTVMap), Wildcard(wcb.name).substitute(freshTVMap))))
     })
   }
 

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

@@ -50,7 +50,7 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
       inType match {
         case RefType(wildcards, name, params) =>
           RefType(
-            wildcards.map(substituteWCB), name, params.map(substitute))
+            WildcardEnvironment(wildcards.map(substituteWCB)), name, params.map(substitute))
         case t => t
       }
     }
@@ -68,6 +68,6 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
     unifier = unifier.map(c => {
       EqualsDot(substitute(c.left), substitute(c.right))
     })
-    this.bounds = this.bounds.map(substituteWCB)
+    this.bounds = WildcardEnvironment(this.bounds.map(substituteWCB))
   }
 }

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

@@ -24,7 +24,22 @@ sealed abstract class Type:
       case _ => Set()
     }
   }
+  def substitute(substMap: Map[Type,Type]): Type = {
+    def substituteWCB(wcb: WildcardBound) =
+      WildcardBound(wcb.name, wcb.upper.substitute(substMap), wcb.lower.substitute(substMap))
 
+    val replace = substMap.get(this)
+    if (replace.isDefined) {
+      replace.get
+    } else {
+      this match {
+        case RefType(wildcards, name, params) =>
+          RefType(
+            WildcardEnvironment(wildcards.map(substituteWCB)), name, params.map(_.substitute(substMap)))
+        case t => t
+      }
+    }
+  }
 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

@@ -4,16 +4,15 @@ case class WildcardBound(name: String, upper: Type, lower: Type){}
 class WildcardEnvironment(wcBounds: Set[WildcardBound]) {
   val bounds: Map[String, (Type, Type)] = wcBounds.map(b => (b.name -> (b.upper, b.lower))).toMap
 
+  def isEmpty = wcBounds.isEmpty
+
   def getUpperBound(wc: Wildcard): Type = bounds(wc.name)._1
 
   def getLowerBound(wc: Wildcard): Type = bounds(wc.name)._2
 
   override def toString: String = bounds.map(_._1).mkString("", ",", ".")
 
-  def map(f : WildcardBound => WildcardBound): WildcardEnvironment = {
-    WildcardEnvironment(wcBounds.map(f))
-  }
-
+  def map[R](f : WildcardBound => R) = wcBounds.map(f)
   def getWildcards() = wcBounds.map(wcb => Wildcard(wcb.name))
 }