Unify, only call step 2 once. substitute beforehand

2022-03-22 22:56:46 +01:00
9 changed files with 128 additions and 51 deletions
--- a/src/main/scala/hb/dhbw/AST.scala
+++ b/src/main/scala/hb/dhbw/AST.scala
@@ -14,7 +14,6 @@ final case class FieldVar(e: Expr, f: String) extends Expr
 final case class MethodCall(e: Expr, name: String, params: List[Expr]) extends Expr
 final case class Constructor(className: String, params: List[Expr]) extends Expr
 final case class Cast(to: Type, expr: Expr) extends Expr
-final case class Lambda(p: String, expr: Expr) extends Expr

 object ASTBuilder {
  def fromParseTree(toAst: List[ParserClass]) = new ASTBuilderMonad().fromParseTree(toAst)
@@ -38,7 +37,6 @@ object ASTBuilder {
      case PFieldVar(e, f) => FieldVar(fromParseExpr(e, genericNames), f)
      case PCast(ntype, e) => Cast(nTypeToType(ntype, genericNames), fromParseExpr(e, genericNames))
      case PLocalVar(n) => LocalVar(n)
-      case PLambda(p, e) => Lambda(p, fromParseExpr(e, genericNames))
    }

    private def freshTPV() = {
--- a/src/main/scala/hb/dhbw/EqSet.scala
+++ b/src/main/scala/hb/dhbw/EqSet.scala
@@ -0,0 +1,8 @@
+package hb.dhbw
+
+class EqSet {
+
+  def addAndConstraint(cons: Set[Constraint]) {}
+
+}
+
--- a/src/main/scala/hb/dhbw/FJTypeinference.scala
+++ b/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,19 +78,23 @@ object FJTypeinference {
    Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
  }

+  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(_))
    var typedClasses: List[Class] = List()
    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)

        //Insert intersection types
        //val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
-        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(unifyResult, c), fc)
+        val typeInsertedC = InsertTypes.applyUnifyResult(unifyResult, c)
        typedClasses = typedClasses :+ typeInsertedC
        cOld :+ typeInsertedC
      })
--- a/src/main/scala/hb/dhbw/InsertTypes.scala
+++ b/src/main/scala/hb/dhbw/InsertTypes.scala
@@ -108,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)
  }
--- a/src/main/scala/hb/dhbw/Main.scala
+++ b/src/main/scala/hb/dhbw/Main.scala
@@ -53,7 +53,6 @@ object Main {
      case FieldVar(e, f) => prettyPrintExpr(e)+"."+f
      case MethodCall(e, name, params) => prettyPrintExpr(e)+"."+name+"("+params.map(prettyPrintExpr(_)).mkString(", ")+")"
      case Constructor(className, params) => "new "+className+"(" + params.map(prettyPrintExpr(_)).mkString(", ") +")"
-      case Lambda(a, expr) => "(" + a + ") -> " + prettyPrintExpr(expr)
    }
    def prettyPrintType(l: Type): String = l match {
      case RefType(name, List()) => name
--- a/src/main/scala/hb/dhbw/Parser.scala
+++ b/src/main/scala/hb/dhbw/Parser.scala
@@ -12,7 +12,6 @@ final case class PFieldVar(e: ParserExpr, f: String) extends ParserExpr
 final case class PMethodCall(e: ParserExpr, name: String, params: List[ParserExpr]) extends ParserExpr
 final case class PConstructor(className: String, params: List[ParserExpr]) extends ParserExpr
 final case class PCast(to: NType, expr: ParserExpr) extends ParserExpr
-final case class PLambda(param: String, expr: ParserExpr) extends ParserExpr

 final case class NType(name: String, params: List[NType])

@@ -36,7 +35,7 @@ object Parser {
    .map(ite => ite._2.map(params => params._1 :: params._2).getOrElse(List.empty))
  def variable[_: P]: P[ParserExpr] = P(ident).map(PLocalVar)
  def cast[_: P]: P[ParserExpr] = P("(" ~ typeParser ~ ")" ~ expr).map(x => PCast(x._1, x._2))
-  def expr[_: P]: P[ParserExpr] = P( (variable | lambdaExpr | constructor | cast)~ (prefixMethodCall | fieldVar).rep.map(_.toList) )
+  def expr[_: P]: P[ParserExpr] = P( (variable | constructor | cast)~ (prefixMethodCall | fieldVar).rep.map(_.toList) )
    .map(ite => ite._2.foldLeft(ite._1) { (e1 : ParserExpr, e2 : ParserExpr) =>
      e2 match{
        case PMethodCall(_, name, e3) => PMethodCall(e1, name, e3)
@@ -44,8 +43,6 @@ object Parser {
      }
    })

-  def lambdaExpr[_: P]: P[PLambda] = P( "(" ~ ident ~ ")" ~ "->" ~ expr).map(it => PLambda(it._1, it._2))
-
  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) ~ method.rep(0) ~ "}")
--- a/src/main/scala/hb/dhbw/TYPE.scala
+++ b/src/main/scala/hb/dhbw/TYPE.scala
@@ -94,14 +94,6 @@ object TYPE {
        val (rty, cons) = TYPEExpr(expr, localVars, ast)
        (casttype, cons)
      }
-      case Lambda(p, expr) => {
-        val t = freshTPV()
-        val a = freshTPV()
-        val b = freshTPV()
-        val typeRet = TYPEExpr(expr, (t, p) :: localVars, ast)
-        val cons = typeRet._2 ++ List(LessDot(t, a), LessDot(typeRet._1, b))
-        (RefType("Function", List(a, b)), cons)
-      }
    }

    private def findMethods(m: String, numParams: Int, ast: List[Class]) =
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -9,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{
@@ -32,6 +43,13 @@ object Unify {
    })
    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)})
  }

@@ -39,22 +57,18 @@ object Unify {
    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 + removeALessdotB(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)
@@ -62,6 +76,25 @@ object Unify {
    results
  }

+  /*
+  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)
+      }
+    })
+  }
+*/
  def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={
    val eq1 = eq.filter(c => c match{
      case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
@@ -118,6 +151,10 @@ object Unify {
    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)
@@ -131,11 +168,18 @@ object Unify {
    }
    )
  }
-
-  def eraseFRule(eq: Set[UnifyConstraint]): Set[UnifyConstraint]= eq.filter(_ match {
-    case UnifyLessDot(UnifyRefType("Function", _), UnifyRefType("Object", _)) => false
-    case _ => true
-  })
+  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
+      }
+    }
+    )
+  }

  def reduceRule(eq: Set[UnifyConstraint]) =  eq.flatMap(c => c match {
    case UnifyEqualsDot(UnifyRefType(an, ap), UnifyRefType(bn, bp)) => {
@@ -176,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
@@ -186,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{
@@ -195,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 {
@@ -318,14 +379,18 @@ 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
-      eqFinish = eraseRule(swapRule(reduceRule(eraseFRule(matchRule(adoptRule(adaptRule(eqNew, fc), fc), fc)))))
+      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]] =
--- a/src/test/scala/IntegrationTest.scala
+++ b/src/test/scala/IntegrationTest.scala
@@ -22,12 +22,7 @@ class IntegrationTest extends FunSuite {

  test("ListAddDefinition"){
    val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n  add(a){\n  return this;\n}\n}")
-    println(result.map(Main.prettyPrintAST(_)))
-  }
-
-  test("lambdaIdentity"){
-    val result = FJTypeinference.typeinference("class Test extends Object{\ntest(){\nreturn (a) -> a;\n}\n}")
-    println(result.map(Main.prettyPrintAST(_)))
+    println(result)
  }
  /*
  test("PaperExample"){