Unify, only call step 2 once. substitute beforehand

README.md

@@ -1,13 +1,7 @@
-# Typeinference for Featherweight Java
-
-## Getting started
+## Typeinference for Featherweight Java
 
 [Try it here](https://janulrich.github.io/FeatherweightTypeInference/)
 
-## Building
-
-```sbt fullLinkJS```
-
 ### Input Examples
 
 ```
@@ -28,7 +22,7 @@ class Overloading extends Object{
 
 class TestOverloading extends Object{
   test(a){
-    return new Overloading().m(this,a);
+    return new Test().m(this,a);
   }
 }
 ```

src/main/scala/hb/dhbw/CartesianProduct.scala

@@ -1,18 +1,18 @@
 package hb.dhbw
 
-class CartesianProductBuilder[A](){
-  var ret : Set[Set[A]] = Set()
-  def build() : CartesianProduct[A] = new CartesianProduct[A](ret)
-
-  def addSingleton(a:A){
-    ret += Set(a)
-  }
-  def add(as : Set[A]): Unit ={
-    ret += as
-  }
-}
-
 class CartesianProduct[A](private val setOfSets: List[List[A]]){
+  def productWith(product: CartesianProduct[A]) = {
+    val ret = new CartesianProduct[A](setOfSets ++ product.setOfSets)
+    var base: Long = 1
+    ret.sizes = ret.setOfSets.map(_.size)
+    ret.sizes.foreach(size => {
+      base = base * size
+    })
+    ret.max = base
+    ret.i = i
+    ret
+  }
+
   private var sizes: List[Int] = null
   private var max: Long = 1
   private var i: Long = 0

src/main/scala/hb/dhbw/EqSet.scala

@@ -0,0 +1,8 @@
+package hb.dhbw
+
+class EqSet {
+
+  def addAndConstraint(cons: Set[Constraint]) {}
+
+}
+

src/main/scala/hb/dhbw/FJTypeinference.scala

@@ -41,23 +41,26 @@ object FJTypeinference {
   ).map(it => (convertRefType(it._1), convertRefType(it._2))).toSet)
   private def cToUnifyType(c: Class): UnifyRefType = UnifyRefType(c.name, c.genericParams.map(it => convertType(it._1)))
 
-  /*
-  Die generics sind für alle Methoden die gleichen. Falls dies der Fall ist, kann man einfach nach Sub typen in den Parametern und return-Typ filtern
-   */
   private def removeOverloadedSubtypeMethods(in: Class, finiteClosure: FiniteClosure) = {
     def convertToFJType(in: Type): FJNamedType = in match {
       case GenericType(name) => FJNamedType(name, List())
       case RefType(n, p) => FJNamedType(n,p.map(convertToFJType))
     }
     def methodIsSupertype(m : Method, superMethod: Method) = {
-      if(m.genericParams.equals(superMethod.genericParams)) {
-        val returnIsSub = finiteClosure.aIsSubtypeOfb(convertToFJType(m.retType), convertToFJType(superMethod.retType))
+      def getBound(t: Type): Type = t match {
+        case GenericType(x) =>
+          (in.genericParams ++ m.genericParams.map(c => (c.asInstanceOf[LessDot].l, c.asInstanceOf[LessDot].r)))
+          .find(p => p._1.equals(GenericType(x))).map(_._2).map(getBound).get
+        case x => x
+      }
+      if(m.params.size != superMethod.params.size){
+        false
+      }else{
+        val returnIsSub = finiteClosure.aIsSubtypeOfb(convertToFJType(getBound(m.retType)), convertToFJType(getBound(superMethod.retType)))
         val paramsAreSup = m.params.zip(superMethod.params).foldLeft(true)((isSub, m2) => {
-          isSub && finiteClosure.aIsSubtypeOfb(convertToFJType(m2._2._1), convertToFJType(m2._1._1))
+          isSub && finiteClosure.aIsSubtypeOfb(convertToFJType(getBound(m2._2._1)), convertToFJType(getBound(m2._1._1)))
         })
         returnIsSub && paramsAreSup
-      }else{
-        false
       }
     }
 
@@ -75,16 +78,10 @@ object FJTypeinference {
     Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
   }
 
-  def removeLessDotGenericConstraints(unifyResult: Set[Set[UnifyConstraint]], generics: Set[String]) :Set[Set[UnifyConstraint]] =
-    unifyResult.map(_.map( _ match { //
-      case UnifyLessDot(UnifyTV(a), UnifyRefType(name, List())) =>
-        if(generics.contains(name))
-            UnifyEqualsDot(UnifyTV(a), UnifyRefType(name, List()))
-          else
-            UnifyLessDot(UnifyTV(a), UnifyRefType(name, List()))
-      case x => x
-    }
-  ))
+  def sigmaReplace(sigma:Map[String, Type], unifyType: UnifyType): Type = unifyType match {
+    case UnifyRefType(n, ps) => RefType(n, ps.map(it => sigmaReplace(sigma, it)))
+    case UnifyTV(a) => sigma(a)
+  }
 
   def typeinference(str: String): Either[String, List[Class]] = {
     val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
@@ -92,13 +89,12 @@ object FJTypeinference {
     ast.map(ast => {
       ast.foldLeft(List[Class]())((cOld, c) => {
         val newClassList = cOld :+ c
-        val fc = generateFC(newClassList)
-        val typeResult = TYPE.generateConstraints(newClassList, fc)
+        val typeResult = TYPE.generateConstraints(newClassList, generateFC(newClassList))
         val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
 
-        val postProcessed = removeLessDotGenericConstraints(unifyResult, c.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
         //Insert intersection types
-        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(postProcessed, c), fc)
+        //val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
+        val typeInsertedC = InsertTypes.applyUnifyResult(unifyResult, c)
         typedClasses = typedClasses :+ typeInsertedC
         cOld :+ typeInsertedC
       })

src/main/scala/hb/dhbw/FiniteClosure.scala

@@ -28,14 +28,10 @@ class FiniteClosure(val extendsRelations : Set[(FJNamedType, FJNamedType)]){
     ref.result()
   }
   private def superClassTypes(of: FJNamedType) = {
-    def paramSubst(param : FJType, paramMap : Map[FJType, FJType]): FJType = param match{
-      case FJNamedType(n, params) => FJNamedType(n, params.map(paramSubst(_, paramMap)))
-      case typeVariable => paramMap.get(typeVariable).get
-    }
     val extendsRelation = extendsRelations.filter(pair => pair._1.name.equals(of.name))
     extendsRelation.map(p => {
       val paramMap = p._1.params.zip(of.params).toMap
-      (of,FJNamedType(p._2.name, p._2.params.map(paramSubst(_, paramMap))))
+      (of,FJNamedType(p._2.name, p._2.params.map(paramMap)))
     })
   }
   private def superClassTypes(of: Set[(FJNamedType, FJNamedType)]) : Set[(FJNamedType, FJNamedType)] ={

src/main/scala/hb/dhbw/InsertTypes.scala

@@ -5,21 +5,20 @@ object InsertTypes {
 
   // Unify step 6:
   //TODO: a <. X must be replaced by X -> sigma(a) = GenericType(X) in that case
-  private class UnifyResult(solvedCons: Set[UnifyConstraint], genericNames: Set[String]){
+  private class UnifyResult(solvedCons: Set[UnifyConstraint]){
     def sigma(x: Type): Type = x match {
       case TypeVariable(n) => sigma(UnifyTV(x.asInstanceOf[TypeVariable].name))
       case v => v
     }
     def sigma(x: UnifyType): Type = { x match {
-        case UnifyTV(_) =>
+        case UnifyTV(n) => {
           val to = solvedCons.find(_.left == x).get
           to match {
-            case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x)
-            case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, List())) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
+            case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x))
             case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_)))
             case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x)
           }
-        case UnifyRefType(n, List()) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
+        }
         case UnifyRefType(n, ps) => RefType(n, ps.map(sigma))
       }
 
@@ -35,7 +34,7 @@ object InsertTypes {
   def applyUnifyResult(eq: Set[Set[UnifyConstraint]], into: Class) = {
     val newMethods = into.methods.flatMap(m => {
       eq.map(req => {
-        val result = new UnifyResult(req, into.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
+        val result = new UnifyResult(req)
         Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
       })
     })
@@ -109,6 +108,22 @@ object InsertTypes {
 
     val constraints = flatted.map(_.map(refTypeInConsToGenerics(_)))
 
+    /*
+
+    def extractTVNames(unifyType: UnifyType): Set[String] = unifyType match {
+      case UnifyTV(name) => Set(name)
+      case UnifyRefType(_, params) => params.flatMap(extractTVNames(_)).toSet
+    }
+
+    val genericNames:Set[String] = into.genericParams.map(_._1).flatMap(_ match {
+      case GenericType(name) => Some(name)
+      case _ => None
+    }).toSet ++ unifyResult.flatMap(_.flatMap(_ match{
+      case UnifyLessDot(a,b) => Set(a, b)
+      case UnifyEqualsDot(a,b) => Set(a,b)
+    })).flatMap(extractTVNames(_))
+    val constraints = normalized.map(_.map(replaceRefTypeWithGeneric(_, genericNames)))
+ */
     val newMethods = into.methods.flatMap(m => constraints.map(cons => insert(cons, m)))
     Class(into.name, into.genericParams, into.superType, into.fields, newMethods)
   }

src/main/scala/hb/dhbw/Parser.scala

@@ -45,16 +45,13 @@ object Parser {
 
   def constructor[_: P]: P[ParserExpr] = P( kw("new") ~ methodCall).map(m => PConstructor(m.name,m.params))
 
-  def classDefinition[_: P]: P[ParserClass] = P(kw("class") ~ ident ~ genericParamList.? ~ kw("extends") ~ typeParser ~ "{" ~ field.rep(0) ~ constructorDef.? ~ method.rep(0) ~ "}")
-    .map(ite => ParserClass(ite._1, ite._2.getOrElse(List()),ite._3,  ite._4.toList, ite._6.toList))
-  def constructorDef[_:P] = P(ident ~ methodParameters ~ "{" ~ fieldAssign.rep ~ "}")
-  def fieldAssign[_:P]:P[_] = P("this." ~ ident.! ~"=" ~ ident.! ~ ";")
+  def classDefinition[_: P]: P[ParserClass] = P(kw("class") ~ ident ~ genericParamList.? ~ kw("extends") ~ typeParser ~ "{" ~ field.rep(0) ~ method.rep(0) ~ "}")
+    .map(ite => ParserClass(ite._1, ite._2.getOrElse(List()),ite._3,  ite._4.toList, ite._5.toList))
   def field[_: P]: P[(NType, String)] = P(typeParser ~ ident ~ ";")
   def parameterDef[_ : P]: P[(Option[NType], String)] = P((typeParser.? ~ ident) | ident.map((None, _)))
-  def methodParameters[_ : P] : P[List[(Option[NType],String)]] = ("("~")").map(it => List()) | ("(" ~ parameterDef ~ ("," ~ parameterDef).rep(0) ~ ")")
-    .map(ite => (ite._1, ite._2) +: ite._3.toList)
   def method[_: P]: P[ParserMethod] =
-    P(parameterDef ~ methodParameters
+    P(parameterDef ~ (("("~")").map(it => List()) | ("(" ~ parameterDef ~ ("," ~ parameterDef).rep(0) ~ ")")
+      .map(ite => (ite._1, ite._2) +: ite._3.toList))
     ~ "{" ~ kw("return") ~ expr ~ ";" ~ "}")
     .map(ite => ParserMethod(ite._1, ite._2, ite._3, ite._4))
   def genericParamList[_: P]: P[List[(NType,NType)]] =

src/main/scala/hb/dhbw/Unify.scala

@@ -1,5 +1,6 @@
 package hb.dhbw
 
+
 sealed abstract class UnifyConstraint(val left: UnifyType, val right: UnifyType)
 final case class UnifyLessDot(override val left: UnifyType, override val right: UnifyType) extends UnifyConstraint(left, right)
 final case class UnifyEqualsDot(override val left: UnifyType, override val right: UnifyType) extends UnifyConstraint(left, right)
@@ -8,6 +9,17 @@ sealed abstract class UnifyType
 final case class UnifyRefType(name: String, params: List[UnifyType]) extends UnifyType
 final case class UnifyTV(name: String) extends UnifyType
 
+/*
+sealed abstract class ResultType
+final case class ResultTV(name: String) extends ResultType
+final case class ResultRefType(name: String, params: List[ResultType]) extends ResultType
+sealed abstract class UnifyResultConstraint
+final case class AExtendsB(a: TypeVariable, b: TypeVariable) extends UnifyResultConstraint
+final case class AExtendsN(a: TypeVariable, n: ResultRefType) extends UnifyResultConstraint
+final case class AEqualsB(a: TypeVariable, b: TypeVariable) extends UnifyResultConstraint
+final case class AEqualsN(a: TypeVariable, n: ResultRefType) extends UnifyResultConstraint
+*/
+
 object Unify {
 
   sealed trait Step4Result{
@@ -23,45 +35,40 @@ object Unify {
     override def result: Set[UnifyConstraint] = eq
   }
 
-  def postProcessing(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
+  def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
     var ret = eq
-    var ruleResult = subElimRule(ret)
-    while(ruleResult.isDefined){
-      ret = ruleResult.get
-      ruleResult = subElimRule(ruleResult.get)
-    }
-    ret
-  }
-
-  def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = {
-    eq.find(_ match{
+    val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{
       case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
       case _ => false
-    }).map(it => {
-      subst(it.right.asInstanceOf[UnifyTV], it.left, eq.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left))
     })
+    ret = ret.filter(it => !alessdotb.contains(it))
+    alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
+    /*
+    .filter(_ match{
+      case UnifyEqualsDot(UnifyTV(a), UnifyTV(b)) => a != b
+      case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => false
+      case _ => true
+    })
+     */
+    ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)})
   }
 
   def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
     def getNext[A](from: Set[CartesianProduct[A]])=
       from.find(_.hasNext()).map(it => it.nextProduct())
 
-    var eqSets: Set[CartesianProduct[Set[UnifyConstraint]]] =
+    val eqSets: Set[CartesianProduct[Set[UnifyConstraint]]] =
       Set(new CartesianProduct[Set[UnifyConstraint]](orCons))
     var it: Option[Set[Set[UnifyConstraint]]] = getNext(eqSets)
     var results: Set[Set[UnifyConstraint]] = Set()
     while(it.isDefined){
       val eqSet = it.get
-      val rulesResult = applyRules(fc)(eqSet.flatten)
+      val rulesResult = applyRules(fc, eqSet.flatten)
       val step2Result = step2(rulesResult, fc)
       while(step2Result.hasNext()){
-        val substResult = substStep(step2Result.nextProduct().flatten)
-        substResult match{
-          case UnchangedSet(eq) => if(isSolvedForm(eq)){
-            results = results + postProcessing(eq)
-          }
-          case ChangedSet(eq) =>
-            eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))
+        val substResult = step2Result.nextProduct().flatten
+        if(isSolvedForm(substResult)){
+            results = results + removeALessdotB(substResult)
         }
       }
       it = getNext(eqSets)
@@ -69,61 +76,106 @@ object Unify {
     results
   }
 
-  def expandLB(lowerBound: UnifyLessDot, upperBound: UnifyLessDot, fc: FiniteClosure): Set[Set[UnifyConstraint]] ={
-    val b:UnifyTV = lowerBound.right.asInstanceOf[UnifyTV]
-    val lowerBoundType : UnifyRefType = lowerBound.left.asInstanceOf[UnifyRefType]
-    val upperBoundType : UnifyRefType = upperBound.right.asInstanceOf[UnifyRefType]
-    fc.superTypes(convertRefType(lowerBoundType)).filter(t => fc.aIsSubtypeOfb(t, convertRefType(upperBoundType)))
-      .map(t => Set(UnifyEqualsDot(b, convertNamedType(t))))
+  /*
+  def unify(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
+    val eqSets = cartesianProduct(orCons)
+    val step2Results = eqSets.flatMap(eqSet => {
+      val rulesResult = applyRules(fc)(eqSet.flatten)
+      step2(rulesResult, fc)
+    })
+    step2Results.flatMap(eqSet => {
+      val (substResult, unifier) = substStep(eqSet)
+      if(!unifier.isDefined){
+        if(isSolvedForm(substResult))
+          Set(substResult)
+        else Set()
+      }else{
+        unify(Set(Set(substResult)), fc).map(s => s + unifier.get)
+      }
+    })
   }
-
-  private def getUpperBoundOrSetUpperBoundToObject(forTV: UnifyTV, eq: Set[UnifyConstraint]) = eq.find(_ match {
-    case UnifyLessDot(UnifyTV(a), UnifyRefType(n, params)) => UnifyTV(a).eq(forTV)
-    case _ => false
-  }).getOrElse(UnifyLessDot(forTV, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot]
-
+*/
   def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={
-    val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]()
-    val aUnifyLessDota = eq.filter(c => c match{
+    val eq1 = eq.filter(c => c match{
+      case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
+      case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true
+      case _ => false
+    })
+    val cUnifyLessDotACons: Set[Set[Set[UnifyConstraint]]] = eq.map(c => c match{
+      case UnifyLessDot(UnifyRefType(name,params), UnifyTV(a)) =>
+        getSuperTypes(UnifyRefType(name,params), fc)
+          .map(superType => Set(UnifyEqualsDot(UnifyTV(a), superType).asInstanceOf[UnifyConstraint]))
+      case _ => null
+    }).filter(s => s!=null)
+
+    val aUnifyLessDota = eq1.filter(c => c match{
       case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
       case _ => false
     }).asInstanceOf[Set[UnifyLessDot]]
 
-    eq.foreach(cons => cons match {
-      case UnifyLessDot(UnifyRefType(n, ps), UnifyTV(a)) =>
-        val lowerBound = UnifyLessDot(UnifyRefType(n, ps), UnifyTV(a))
-        val upperBound = getUpperBoundOrSetUpperBoundToObject(lowerBound.right.asInstanceOf[UnifyTV], eq)
-        cpBuilder.add(expandLB(lowerBound, upperBound, fc))
-      case UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps)) =>
-        getLinks(UnifyTV(a), aUnifyLessDota)
-          .map(b => {
-            val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq)
-            val lowerBound = UnifyLessDot(UnifyRefType(n, ps), b)
-            //ExpandLB and add to return constraint set + {b <. C<T>} constraint
-            cpBuilder.add(expandLB(lowerBound, upperBound, fc) + Set(UnifyLessDot(b, b)))
-          })
-        cpBuilder.addSingleton(Set(UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps))))
-        //the upper bound constraint remains in the constraint set:
-        cpBuilder.addSingleton(Set(UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps))))
-      case cons => cpBuilder.addSingleton(Set(cons))
+    val aUnifyLessDotCConsAndBs: Set[(UnifyLessDot,Option[UnifyTV])] = eq.map(c => c match{
+      case UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)) =>{
+        val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]]
+          .filter(c => !a.equals(c) && isLinked(UnifyTV(a), c, aUnifyLessDota))
+        if(bs.isEmpty){
+          Set((UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)),None))
+        }else{
+          bs.map(b => (UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)),Some(b)))
+        }
+      }
+      case _ => null
+    }).filter(s => s!=null).flatten
+
+    val aUnifyLessDotCCons =  aUnifyLessDotCConsAndBs.map{
+      case (ac:UnifyLessDot,Some(b)) =>
+        Set(Set(UnifyLessDot(b, ac.right))) ++
+          getSuperTypes(ac.right.asInstanceOf[UnifyRefType], fc)
+            .map(superType => Set(UnifyEqualsDot(b, superType)))
+      case (ac, None) => null
+    }.filter(c => c != null).asInstanceOf[Set[Set[Set[UnifyConstraint]]]]
+
+    val eq2 = eq.filter(c => c match{
+      case UnifyLessDot(UnifyTV(_), UnifyRefType(_,_)) => true
+      case UnifyEqualsDot(UnifyTV(_), UnifyRefType(_,_)) => true
+      case UnifyEqualsDot(UnifyRefType(_,_),UnifyTV(_)) => true
+      case UnifyEqualsDot(UnifyRefType(_,_),UnifyRefType(_,_)) => true
+      case UnifyLessDot(UnifyRefType(_,_),UnifyRefType(_,_)) => true
+      case _ => false
     })
-    cpBuilder.build()
+    val eqSet = new CartesianProduct[Set[UnifyConstraint]](
+      Set(Set(eq1)) ++ Set(Set(eq2)) ++ aUnifyLessDotCCons ++ cUnifyLessDotACons)
+    eqSet
   }
 
   private def getAUnifyLessDotC(from: Set[UnifyConstraint]) = from.filter(c => c match{
     case UnifyLessDot(UnifyTV(_), UnifyRefType(_,_)) => true
     case _ => false
   }).asInstanceOf[Set[UnifyLessDot]]
+  private def getCUnifyLessDotA(from: Set[UnifyConstraint]) = from.filter(c => c match{
+    case UnifyLessDot(UnifyRefType(_, _), UnifyTV(_)) => true
+    case _ => false
+  }).asInstanceOf[Set[UnifyLessDot]]
 
   def matchRule(eq : Set[UnifyConstraint], fc: FiniteClosure) = {
     val aUnifyLessDotC = getAUnifyLessDotC(eq)
-    (eq -- aUnifyLessDotC) ++ aUnifyLessDotC.flatMap(c => {
-      val smallerC = aUnifyLessDotC.filter(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
+    (eq -- aUnifyLessDotC) ++ aUnifyLessDotC.map(c => {
+      val smallerC = aUnifyLessDotC.find(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
       if(smallerC.isEmpty){
-        List(c)
+        c
       }else{
-        val list = smallerC.toList
-        UnifyLessDot(list.head.right, c.right) :: list.tail
+        UnifyLessDot(smallerC.get.right, c.right)
+      }
+    }
+    )
+  }
+  def match2Rule(eq : Set[UnifyConstraint], fc: FiniteClosure) = {
+    val cUnifyLessDotA = getCUnifyLessDotA(eq) //C <. a
+    (eq -- cUnifyLessDotA) ++ cUnifyLessDotA.map(c => {
+      val smallerA = cUnifyLessDotA.find(c2 => c2 != c && c2.right.equals(c.right) && fc.isPossibleSupertype(c.left.asInstanceOf[UnifyRefType].name,c2.left.asInstanceOf[UnifyRefType].name))
+      if(smallerA.isEmpty){ //c2 = smallerA = D <. a  C < D
+        c
+      }else{
+        UnifyLessDot(c.left, smallerA.get.left) // C <. D
       }
     }
     )
@@ -168,7 +220,6 @@ object Unify {
       case x => x
     })
   }
-
   def adoptRule(eq: Set[UnifyConstraint], fc: FiniteClosure) ={
     val aUnifyLessDota = eq.filter(c => c match{
       case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
@@ -178,7 +229,7 @@ object Unify {
     (eq -- aUnifyLessDotC) ++ aUnifyLessDotC.map(c => {
       val smallerC = aUnifyLessDotC.find(c2 => c2 != c
         && isLinked(c2.left.asInstanceOf[UnifyTV], c.left.asInstanceOf[UnifyTV], aUnifyLessDota)
-      && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
+        && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
       if(smallerC.isEmpty){
         c
       }else{
@@ -187,6 +238,24 @@ object Unify {
     }
     )
   }
+  def adopt2Rule(eq: Set[UnifyConstraint], fc: FiniteClosure) = {
+    val aUnifyLessDota = eq.filter(c => c match{
+      case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
+      case _ => false
+    }).asInstanceOf[Set[UnifyLessDot]]
+    val cUnifyLessDotA = getCUnifyLessDotA(eq)
+    (eq -- cUnifyLessDotA) ++ cUnifyLessDotA.map(c => {
+      val smallerA = cUnifyLessDotA.find(c2 => c2 != c
+        && isLinked(c2.right.asInstanceOf[UnifyTV], c.right.asInstanceOf[UnifyTV], aUnifyLessDota)
+      && fc.isPossibleSupertype(c.left.asInstanceOf[UnifyRefType].name,c2.left.asInstanceOf[UnifyRefType].name))
+      if(smallerA.isEmpty){
+        c
+      }else{
+        UnifyLessDot(c.left, smallerA.get.left)
+      }
+    }
+    )
+  }
 
   def eraseRule(eq: Set[UnifyConstraint]) =
     eq.filter(_ match {
@@ -194,14 +263,6 @@ object Unify {
       case _ => true
     })
 
-  /**
-   * Every 'b' with a <.* b
-   */
-  def getLinks(a: UnifyTV, aUnifyLessDota: Set[UnifyLessDot]): Set[UnifyTV] =
-    aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(a.name))
-      .flatMap(cons => Set(cons.right.asInstanceOf[UnifyTV]) ++ getLinks(cons.right.asInstanceOf[UnifyTV], aUnifyLessDota))
-
-
   private def isLinked(a: UnifyTV, b: UnifyTV, aUnifyLessDota: Set[UnifyLessDot]): Boolean = {
     def getRightSides(of: UnifyTV) ={
       aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
@@ -216,29 +277,33 @@ object Unify {
     }
   }
 
+  private def findCircles(aUnifyLessDota: Set[UnifyLessDot]) ={
+    def getRightSides(of: UnifyTV) ={
+      aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
+    }
+    def findCircle(graph: List[UnifyLessDot]): List[UnifyLessDot] = {
+      val newAdditions = getRightSides(graph.last.right.asInstanceOf[UnifyTV])
+      var circle: List[UnifyLessDot] = List()
+      val iterator = newAdditions.iterator
+      while(iterator.hasNext && circle.isEmpty){
+        val newAdd = iterator.next()
+        if(newAdd.right.equals(graph.head.left)){
+          circle = graph :+ newAdd
+        }else{
+          circle = findCircle(graph ++ List(newAdd))
+        }
+      }
+      circle
+    }
+    aUnifyLessDota.view.map(c => findCircle(List(c)))
+  }
+
   def equalsRule(eq: Set[UnifyConstraint]) ={
     val aUnifyLessDota = eq.filter(c => c match{
       case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
       case _ => false
     }).asInstanceOf[Set[UnifyLessDot]]
-    def getRightSides(of: UnifyTV) ={
-      aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
-    }
-    def findCircle(start: UnifyTV) : List[UnifyLessDot] = findCircleRec(start, Set(start))
-    def findCircleRec(next: UnifyTV, visited: Set[UnifyTV]): List[UnifyLessDot] = {
-      val rightSides = getRightSides(next).iterator
-      while(rightSides.hasNext){ //Deep search
-        val rightSide = rightSides.next()
-        val nextTV = rightSide.right.asInstanceOf[UnifyTV]
-        if(visited.contains(nextTV)){
-          return List(rightSide)
-        }else{
-          return rightSide :: findCircleRec(nextTV, visited + nextTV)
-        }
-      }
-      List() // empty list means there are no circles
-    }
-    val circle = aUnifyLessDota.map(cons => findCircle(cons.left.asInstanceOf[UnifyTV])).find(!_.isEmpty)
+    val circle = findCircles(aUnifyLessDota).find(!_.isEmpty)
     if(circle.isDefined){
       val newEq = eq -- circle.get
       Some(newEq ++ (circle.get.map(c => UnifyEqualsDot(c.left, c.right))))
@@ -314,21 +379,27 @@ object Unify {
   private def doWhileSome(fun: Set[UnifyConstraint]=>Option[Set[UnifyConstraint]], eqTemp: Set[UnifyConstraint]): Set[UnifyConstraint] =
     fun(eqTemp).map(eqTemp2 => doWhileSome(fun,eqTemp2)).getOrElse(eqTemp)
 
-  def applyRules(fc: FiniteClosure) = (eq: Set[UnifyConstraint]) => {
+  def applyRules(fc: FiniteClosure, eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
     var eqNew: Set[UnifyConstraint] = null
     var eqFinish: Set[UnifyConstraint] = eq
     do{
       eqNew = doWhileSome(Unify.equalsRule,eqFinish) //We have to apply equals rule first, to get rid of circles
-      val adaptRuleResult = adaptRule(eqNew, fc)
-      val adoptRuleResult = adoptRule(adaptRuleResult, fc)
-      val matchRuleResult = matchRule(adoptRuleResult, fc)
-      val reduceRuleResult = reduceRule(matchRuleResult)
-      val swapRuleResult = swapRule(reduceRuleResult)
-      val eraseRuleResult = eraseRule(swapRuleResult)
-      eqFinish = eraseRuleResult
+      eqFinish = eraseRule(swapRule(reduceRule(match2Rule(matchRule(adopt2Rule(adoptRule(adaptRule(eqNew, fc), fc), fc), fc), fc))))
     }while(!eqNew.equals(eqFinish))
-    eqNew
+    val substResult = substStep(eqNew)
+    substResult match{
+      case UnchangedSet(_) => substResult.result
+      case ChangedSet(_) => applyRules(fc, substResult.result)
+    }
   }
 
+  def cartesianProduct[T](xss: Set[Set[T]]): Set[Set[T]] =
+    if(xss.isEmpty){
+      Set(Set())
+    } else{
+      for(xh <- xss.head; xt <- cartesianProduct(xss.tail)) yield xt + xh
+    }
+
+
 }
 

src/test/scala/CartesianProductTest.scala

@@ -8,4 +8,15 @@ class CartesianProductTest extends FunSuite{
     val result = List(1,2,3,4).map( _ => test.nextProduct())
     assert(result.contains(Set(1,4)))
   }
+
+  test("productWith"){
+    val test = new CartesianProduct[Int](Set(Set(1,2),Set(4,3)))
+    val test2 = new CartesianProduct[Int](Set(Set(5,6), Set(7,8)))
+    val test3 = test.productWith(test2)
+    val result = for( i <- 1 to 16) yield test3.nextProduct()
+    assert(result.contains(Set(2,3,6,8)))
+    assert(result.toSet.size == 16)
+    println(result)
+  }
+
 }

src/test/scala/IntegrationTest.scala

@@ -7,101 +7,168 @@ class IntegrationTest extends FunSuite {
     val ast = (fastparse.parse(("e.m(a)"), hb.dhbw.Parser.classDefinition(_)))
     //hb.dhbw.TYPE.TYPEClass(ast.get)
     val result = FJTypeinference.typeinference("class Test extends Object {\n\n}")
-    assert(result.isRight)
     println(result)
   }
 
   test("IdMethod"){
     val result = FJTypeinference.typeinference("class Test extends Object {\nObject f;\nm(a){return a;}\n}")
-    assert(result.isRight)
     println(result)
-    println(result.map(Main.prettyPrintAST(_)))
   }
 
   test("IdMethodRecursive"){
     val result = FJTypeinference.typeinference("class Test extends Object {\n   Object f;\n   m(a, b){return this.m(b, a); }\n}")
-    assert(result.isRight)
     println(result)
   }
 
   test("ListAddDefinition"){
     val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n  add(a){\n  return this;\n}\n}")
-    assert(result.isRight)
-    println(result.map(Main.prettyPrintAST(_)))
+    println(result)
   }
+  /*
+  test("PaperExample"){
+    val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n  add( a){\n  return this;\n}\n}\nclass Test extends Object{\nm(a){ return a.add(this);}\n}")
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("GenericVar"){
+    val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\nA a;\n\nget(){ return this.a;\n\n}\n}\n\n\nclass Test extends Object{\nList<String> test;\n\nm(a){\n   return this.test.get();\n}\n\n}")
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("IdentCallExample"){
+    val result = FJTypeinference.typeinference("class Test extends Object{\n\n  m(a,b){return this.m(a);\n}\nm(a){return a;}\n}")
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("IdentRecursive"){
+    val result = FJTypeinference.typeinference("class Test extends Object{\n\nm(a){\nreturn this.m(a);\n}\n}")
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("GetMethods"){
+    val result = FJTypeinference.typeinference("class Test extends Object{\nget(){ return this.get().get();}\n}\n\nclass Test2 extends Object{\nget(){ return this;}\n}" )
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("constructorTest"){
+    val input= "class Test extends Object{m(){ return new Test();}}"
+    val result = FJTypeinference.typeinference(input )
+    println(result.map(Main.prettyPrint(_)))
+  }
+
+  test("fieldVar access"){
+    val input ="class List<A extends Object> extends Object{\nA f;\nget(){ return this.f; }\n}\n\nclass Test2 extends Object{\nget(){ return new List(this).get();}\n}"
+    val result = FJTypeinference.typeinference(input )
+    println(result.map(Main.prettyPrint(_)))
+  }
+   */
 
   test("constructor.FieldInitialization") {
     val input = "class List<A extends Object> extends Object{\nA f;\n  add(a){\n  return new List(a);\n}\n}"
     val result = FJTypeinference.typeinference(input )
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
   test("list.add") {
     val input = "class List<A extends Object> extends Object{\nA f;\n  add( a){\n  return new List(a);\n}\n}\nclass Test extends Object{\n\nm(a){return a.add(this);}\n}"
     val result = FJTypeinference.typeinference(input )
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
   test("list.add.2") {
     val input = "class List<A extends Object> extends Object{\n  A head;\n  List<A> tail;\n  add( a){\n  return new List(a, this);\n}\nget(){\nreturn this.head;\n}\n}\n\nclass Test extends Object{\nm(a){\nreturn a.add(this).get();\n}\n}"
     val result = FJTypeinference.typeinference(input )
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("functionClass") {
     val input = "class SameType<A extends Object, B extends Object> extends Object{\nA a;\nA b;\nB c;\nget(){return this.c;}\n}\nclass Function<A extends Object, B extends Object> extends Object{\nA ret;\nB param;\napply(a){\nreturn new SameType(this.param, a, this).get().ret;\n}\n\n}"
     val result = FJTypeinference.typeinference(input )
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("TwoRecursiveMethods") {
     val input = "class RecursiveMethods extends Object{\n\na1(x){ return this.a2(x);}\na2(y){ return this.a1(y);}}"
     val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("Function.typeAnnotaded") {
     val input = "\nclass Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n\n}"
     val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("Box.Map") {
     val input = "class Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n}\n\n\nclass Box<S extends Object> extends Object {\nS val ;\nmap( f ) {\nreturn new Box(f.apply(this.val)) ;\n}\n}"
     val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("PrincipalType") {
     val input = "\nclass List<A extends Object> extends Object{\n  A head;\n  List<A> tail;\n  add( a){\n    return new List(a, this);\n  }\n  get(){\n    return this.head;\n  }\n}\n\nclass PrincipleType extends Object {\n  function(a){\n    return a.add(this).get();\n  }\n}"
     val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
+  /*
 
-  test("ListExample") {
-    val input = "\n\nclass List<A extends Object> extends Object{\n    A element;\n    List<A> succ; \n    add(a){\n       return new List(a, this);\n    }\n\n}\n\nclass Example extends Object{\n\n    test(a){\n        return a.add(this);\n    }\n}"
-    val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
-    println(result.map(it => Main.prettyPrintAST(it)))
+class List<A extends Object> extends Object{
+  A head;
+  List<A> tail;
+  add( a){
+    return new List(a, this);
   }
-
-  test("extendsWithComplexType") {
-    val input = "class Pair<A extends Object, B extends Object> extends Object {}\n\nclass Test<A extends Object> extends Pair<Pair<A,A>,A> {\n\nm(a){return this;}\n\n\n}"
-    val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
-    println(result.map(it => Main.prettyPrintAST(it)))
-  }
-
-  test("pairAdd.twoTimes") {
-    val input = "class Pair<A extends Object> extends Object{\n    A fst;\n    \n    setfst(p) {\n      return p;\n    }\n  }\n\n  class Example extends Object{\n\n    m(p){\n      return p.setfst(p.setfst(this));\n    }\n  }"
-    val result = FJTypeinference.typeinference(input)
-    assert(result.isRight)
-    println(result.map(it => Main.prettyPrintAST(it)))
+  get(){
+    return this.head;
   }
 }
+
+class PrincipleType extends Object {
+  function(a){
+    return a.add(this).get();
+  }
+}
+
+
+class Function<A extends Object, B extends Object> extends Object{
+B b;
+B apply(A a){
+return this.b;
+}
+}
+
+
+class Box<S extends Object> extends Object {
+S val ;
+map( f ) {
+return new Box(f.apply(this.val)) ;
+}
+}
+
+class Function<A extends Object, B extends Object> extends Object{
+B b;
+B apply(A a){
+return this.b;
+}
+
+}
+
+
+class RecursiveMethods extends Object{
+
+a1(x){ return this.a2(x);}
+a2(y){ return this.a1(y);}
+}
+   */
+    /*
+  Additional Tests:
+
+class Test extends Object{
+ m(a, b){return a;}
+m(a,b){return b;}
+}
+
+class Test2 extends Object{
+test(a){return new Test().m(this,a);}
+}
+
+   */
+}

src/test/scala/ParserTest.scala

@@ -62,11 +62,4 @@ class ParserTest extends FunSuite {
     println(fastparse.parse("class List<A extends Object> extends Object{asd(){ return this;  }get(){ return this.head;}}"
       , hb.dhbw.Parser.program(_)))
   }
-
-  test("Konstruktor"){
-    val parsed = fastparse.parse("class Pair<X extends Object, Y extends Object> extends Object{\n  X fst;\n  Y snd;\n  Pair(fst, snd) {\n    this.fst=fst;\n    this.snd=snd;\n  }\n}"
-      , hb.dhbw.Parser.program(_))
-    assert(parsed.isSuccess)
-    println(parsed.get)
-  }
 }

src/test/scala/UnifyTest.scala

@@ -1,6 +1,5 @@
 
-
-import hb.dhbw.{FJNamedType, FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
+import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
 import org.scalatest.FunSuite
 
 class UnifyTest extends FunSuite {
@@ -10,37 +9,7 @@ class UnifyTest extends FunSuite {
 
   val fc = new FiniteClosure(Set())
 
-  test("sub-elim rule"){
-    val input : Set[UnifyConstraint] = Set(UnifyLessDot(UnifyTV("a"), UnifyTV("b")), UnifyEqualsDot(UnifyTV("a"), UnifyRefType("a", List())))
-    val result = Unify.postProcessing(input)
-    println(result)
-    assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b"))))
-    assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a"))))
-  }
 
-  test("error"){
-    val input : Set[Set[Set[UnifyConstraint]]]= Set(Set(Set(UnifyLessDot(UnifyTV("1"), UnifyTV("B")), UnifyLessDot(UnifyTV("1"), UnifyTV("2")),
-      UnifyLessDot(UnifyRefType("Test", List()), UnifyTV("2")))))
-    val result = Unify.unifyIterative(input, new FiniteClosure(Set((FJNamedType("Test", List()), FJNamedType("Object", List())))))
-    println(result)
-  }
-
-  test("example"){
-    val input : Set[UnifyConstraint] = Set(UnifyEqualsDot(UnifyTV("b"), UnifyTV("y")),
-      UnifyLessDot(UnifyRefType("Pair", List(UnifyRefType("X", List()), UnifyRefType("Y", List()))), UnifyRefType("Pair", List(UnifyTV("w"), UnifyTV("y")))),
-      UnifyLessDot(UnifyRefType("Pair", List(UnifyTV("d"), UnifyTV("e"))), UnifyTV("A")),
-      UnifyLessDot(UnifyTV("F"), UnifyTV("d")),
-      UnifyLessDot(UnifyTV("b"), UnifyTV("e")),
-      UnifyLessDot(UnifyTV("F"), UnifyRefType("Object", List())))
-    val result = Unify.unifyIterative(Set(Set(input)), new FiniteClosure(Set((FJNamedType("Pair", List(FJNamedType("X", List()),FJNamedType("X", List()))), FJNamedType("Object", List())))))
-    println(result)
-  }
-
-  test("getLinks.emptySet"){
-    val input : Set[UnifyLessDot] = Set()
-    val ret = Unify.getLinks(UnifyTV("a"), input)
-    assert(ret.equals(Set.empty))
-  }
   /*
   test("Unify.step2") {
     var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")),