Change a <. B to a =. B if B is a generic

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

@@ -75,6 +75,17 @@ 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 typeinference(str: String): Either[String, List[Class]] = {
     val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
     var typedClasses: List[Class] = List()
@@ -85,9 +96,10 @@ object FJTypeinference {
         val typeResult = TYPE.generateConstraints(newClassList, fc)
         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 = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
-        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(unifyResult, c), fc)
+        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(postProcessed, c), fc)
         typedClasses = typedClasses :+ typeInsertedC
         cOld :+ typeInsertedC
       })

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

@@ -5,7 +5,7 @@ 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]){
+  private class UnifyResult(solvedCons: Set[UnifyConstraint], genericNames: Set[String]){
     def sigma(x: Type): Type = x match {
       case TypeVariable(n) => sigma(UnifyTV(x.asInstanceOf[TypeVariable].name))
       case v => v
@@ -15,10 +15,12 @@ object InsertTypes {
           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(_), 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))
       }
 
@@ -34,7 +36,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)
+        val result = new UnifyResult(req, into.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
         Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
       })
     })

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

@@ -35,7 +35,7 @@ object Unify {
     override def result: Set[UnifyConstraint] = eq
   }
 
-  def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
+  def postProcessing(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
     var ret = eq
     var ruleResult = subElimRule(ret)
     while(ruleResult.isDefined){
@@ -71,7 +71,7 @@ object Unify {
         val substResult = substStep(step2Result.nextProduct().flatten)
         substResult match{
           case UnchangedSet(eq) => if(isSolvedForm(eq)){
-            results = results + removeALessdotB(eq)
+            results = results + postProcessing(eq)
           }
           case ChangedSet(eq) =>
             eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))

src/test/scala/IntegrationTest.scala

@@ -108,6 +108,12 @@ class IntegrationTest extends FunSuite {
     val result = FJTypeinference.typeinference(input)
     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)
+    println(result.map(it => Main.prettyPrintAST(it)))
+  }
   /*
 
 class List<A extends Object> extends Object{

src/test/scala/UnifyTest.scala

@@ -1,5 +1,5 @@
 
-import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
+import hb.dhbw.{FJNamedType, FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
 import org.scalatest.FunSuite
 
 class UnifyTest extends FunSuite {
@@ -9,6 +9,19 @@ 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("Unify.step2") {