From 93f7edf467a741c9c657d6d581cadd460fb9f93c Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 11 Apr 2022 17:32:18 +0200 Subject: [PATCH 01/25] Rafactoring: Remove unused code. Add duplicated method filtering --- src/main/scala/hb/dhbw/EqSet.scala | 8 ------ src/main/scala/hb/dhbw/FJTypeinference.scala | 29 ++++++++------------ src/main/scala/hb/dhbw/InsertTypes.scala | 16 ----------- src/main/scala/hb/dhbw/Unify.scala | 26 ------------------ src/test/scala/IntegrationTest.scala | 2 +- 5 files changed, 12 insertions(+), 69 deletions(-) delete mode 100644 src/main/scala/hb/dhbw/EqSet.scala diff --git a/src/main/scala/hb/dhbw/EqSet.scala b/src/main/scala/hb/dhbw/EqSet.scala deleted file mode 100644 index 67f28f9..0000000 --- a/src/main/scala/hb/dhbw/EqSet.scala +++ /dev/null @@ -1,8 +0,0 @@ -package hb.dhbw - -class EqSet { - - def addAndConstraint(cons: Set[Constraint]) {} - -} - diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala index ee6d80f..d8fc68a 100644 --- a/src/main/scala/hb/dhbw/FJTypeinference.scala +++ b/src/main/scala/hb/dhbw/FJTypeinference.scala @@ -41,26 +41,23 @@ 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) = { - 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))) + if(m.genericParams.equals(superMethod.genericParams)) { + val returnIsSub = finiteClosure.aIsSubtypeOfb(convertToFJType(m.retType), convertToFJType(superMethod.retType)) val paramsAreSup = m.params.zip(superMethod.params).foldLeft(true)((isSub, m2) => { - isSub && finiteClosure.aIsSubtypeOfb(convertToFJType(getBound(m2._2._1)), convertToFJType(getBound(m2._1._1))) + isSub && finiteClosure.aIsSubtypeOfb(convertToFJType(m2._2._1), convertToFJType(m2._1._1)) }) returnIsSub && paramsAreSup + }else{ + false } } @@ -78,23 +75,19 @@ 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 typeResult = TYPE.generateConstraints(newClassList, generateFC(newClassList)) + val fc = generateFC(newClassList) + val typeResult = TYPE.generateConstraints(newClassList, fc) 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 = InsertTypes.applyUnifyResult(unifyResult, c) + val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(unifyResult, c), fc) typedClasses = typedClasses :+ typeInsertedC cOld :+ typeInsertedC }) diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala index 451b779..667b58c 100644 --- a/src/main/scala/hb/dhbw/InsertTypes.scala +++ b/src/main/scala/hb/dhbw/InsertTypes.scala @@ -108,22 +108,6 @@ 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) } diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 9eea652..ede9ef8 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -43,13 +43,6 @@ 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)}) } @@ -80,25 +73,6 @@ 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 diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index aca588b..b844f16 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -22,7 +22,7 @@ class IntegrationTest extends FunSuite { test("ListAddDefinition"){ val result = FJTypeinference.typeinference("class List extends Object{\n add(a){\n return this;\n}\n}") - println(result) + println(result.map(Main.prettyPrintAST(_))) } /* test("PaperExample"){ From 6340672a274548f558e4cca4a0558efc86ad00ba Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 12 Apr 2022 17:05:58 +0200 Subject: [PATCH 02/25] Remove comments --- src/main/scala/hb/dhbw/Unify.scala | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index ede9ef8..25a2864 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -9,17 +9,6 @@ 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{ From 0267a2df24adaed17460a096ca2d9c2d3edbb068 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 12 Apr 2022 19:50:35 +0200 Subject: [PATCH 03/25] fix sub-elim (removeALessdotB) function --- src/main/scala/hb/dhbw/Unify.scala | 8 ++++++-- src/test/scala/UnifyTest.scala | 9 ++++++++- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 25a2864..ab3387d 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -31,8 +31,12 @@ object Unify { case _ => false }) ret = ret.filter(it => !alessdotb.contains(it)) - alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret)) - ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)}) + var newADotEqB : Set[UnifyConstraint] = Set() + alessdotb.foreach(it => { + ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret) + newADotEqB = newADotEqB ++ Set(UnifyEqualsDot(it.right, it.left)) + }) + ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)}) ++ newADotEqB } def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = { diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index c20da32..0090605 100644 --- a/src/test/scala/UnifyTest.scala +++ b/src/test/scala/UnifyTest.scala @@ -1,5 +1,5 @@ -import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV} +import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV} import org.scalatest.FunSuite class UnifyTest extends FunSuite { @@ -9,6 +9,13 @@ 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.removeALessdotB(input) + println(result) + assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b")))) + assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a")))) + } /* test("Unify.step2") { From 93af1d12f68c7b2b4e434a0f204ae0c1d75d5138 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sat, 16 Apr 2022 15:44:59 +0200 Subject: [PATCH 04/25] add subElimRule --- src/main/scala/hb/dhbw/Unify.scala | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index ede9ef8..9796afd 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -37,13 +37,22 @@ object Unify { def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = { var ret = eq - val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{ + var ruleResult = subElimRule(ret) + while(ruleResult.isDefined){ + ret = ruleResult.get + ruleResult = subElimRule(ruleResult.get) + } + ret + } + + def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = { + var ret = eq + eq.find(_ match{ case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true case _ => false + }).map(it => { + subst(it.left.asInstanceOf[UnifyTV], it.right, ret) ++ Set(UnifyEqualsDot(it.right, it.left)) }) - ret = ret.filter(it => !alessdotb.contains(it)) - alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret)) - ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)}) } def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = { From 37ae27a521dc99b70fac583829745b63bdfdaef4 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sat, 16 Apr 2022 15:54:36 +0200 Subject: [PATCH 05/25] Fix subElim rule, Fix type insert --- src/main/scala/hb/dhbw/InsertTypes.scala | 2 +- src/main/scala/hb/dhbw/Unify.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala index 667b58c..bc9b65d 100644 --- a/src/main/scala/hb/dhbw/InsertTypes.scala +++ b/src/main/scala/hb/dhbw/InsertTypes.scala @@ -14,7 +14,7 @@ object InsertTypes { case UnifyTV(n) => { val to = solvedCons.find(_.left == x).get to match { - case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x)) + case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x) case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_))) case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x) } diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 9796afd..85be72d 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -51,7 +51,7 @@ object Unify { case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true case _ => false }).map(it => { - subst(it.left.asInstanceOf[UnifyTV], it.right, ret) ++ Set(UnifyEqualsDot(it.right, it.left)) + subst(it.left.asInstanceOf[UnifyTV], it.right, ret.filter(it != _)) ++ Set(UnifyEqualsDot(it.left, it.right), UnifyEqualsDot(it.right, it.right)) }) } From df9f34c739d6ae44873ab20401d52d992fe2f1d7 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 4 May 2022 16:56:14 +0200 Subject: [PATCH 06/25] Change a <. B to a =. B if B is a generic --- src/main/scala/hb/dhbw/FJTypeinference.scala | 14 +++++++++++++- src/main/scala/hb/dhbw/InsertTypes.scala | 6 ++++-- src/main/scala/hb/dhbw/Unify.scala | 4 ++-- src/test/scala/IntegrationTest.scala | 6 ++++++ src/test/scala/UnifyTest.scala | 15 ++++++++++++++- 5 files changed, 39 insertions(+), 6 deletions(-) diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala index d8fc68a..5e62062 100644 --- a/src/main/scala/hb/dhbw/FJTypeinference.scala +++ b/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 }) diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala index bc9b65d..94ec681 100644 --- a/src/main/scala/hb/dhbw/InsertTypes.scala +++ b/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) }) }) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 85be72d..a9c2324 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/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))) diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index b844f16..3ecfb2e 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/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 extends Object{\n A element;\n List 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 extends Object{ diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index c20da32..e0458a4 100644 --- a/src/test/scala/UnifyTest.scala +++ b/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") { From 3018c060f44befed0b016370e1466fd12714cb42 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Mon, 25 Apr 2022 15:59:43 +0200 Subject: [PATCH 07/25] Fix sub-elim rule --- src/main/scala/hb/dhbw/Unify.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index a9c2324..6d994df 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -51,7 +51,7 @@ object Unify { case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true case _ => false }).map(it => { - subst(it.left.asInstanceOf[UnifyTV], it.right, ret.filter(it != _)) ++ Set(UnifyEqualsDot(it.left, it.right), UnifyEqualsDot(it.right, it.right)) + subst(it.right.asInstanceOf[UnifyTV], it.left, ret.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left)) }) } From d26363ec1934d6d0b21b1393168b6f56dcff9e08 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sun, 15 May 2022 23:38:55 +0200 Subject: [PATCH 08/25] Add optional constructor to parser --- src/main/scala/hb/dhbw/Parser.scala | 11 +++++++---- src/test/scala/ParserTest.scala | 7 +++++++ 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/main/scala/hb/dhbw/Parser.scala b/src/main/scala/hb/dhbw/Parser.scala index d11378d..2959b50 100644 --- a/src/main/scala/hb/dhbw/Parser.scala +++ b/src/main/scala/hb/dhbw/Parser.scala @@ -45,13 +45,16 @@ 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) ~ method.rep(0) ~ "}") - .map(ite => ParserClass(ite._1, ite._2.getOrElse(List()),ite._3, ite._4.toList, ite._5.toList)) + 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 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 ~ (("("~")").map(it => List()) | ("(" ~ parameterDef ~ ("," ~ parameterDef).rep(0) ~ ")") - .map(ite => (ite._1, ite._2) +: ite._3.toList)) + P(parameterDef ~ methodParameters ~ "{" ~ kw("return") ~ expr ~ ";" ~ "}") .map(ite => ParserMethod(ite._1, ite._2, ite._3, ite._4)) def genericParamList[_: P]: P[List[(NType,NType)]] = diff --git a/src/test/scala/ParserTest.scala b/src/test/scala/ParserTest.scala index 1366c3c..0858a58 100644 --- a/src/test/scala/ParserTest.scala +++ b/src/test/scala/ParserTest.scala @@ -62,4 +62,11 @@ class ParserTest extends FunSuite { println(fastparse.parse("class List extends Object{asd(){ return this; }get(){ return this.head;}}" , hb.dhbw.Parser.program(_))) } + + test("Konstruktor"){ + val parsed = fastparse.parse("class Pair 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) + } } From f88da9e736dc2176fa7f0dc81e91f08adecaef9e Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 17 May 2022 11:51:18 +0200 Subject: [PATCH 09/25] Remove comments --- src/test/scala/IntegrationTest.scala | 101 --------------------------- 1 file changed, 101 deletions(-) diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index 3ecfb2e..2674000 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -24,44 +24,6 @@ class IntegrationTest extends FunSuite { val result = FJTypeinference.typeinference("class List extends Object{\n add(a){\n return this;\n}\n}") println(result.map(Main.prettyPrintAST(_))) } - /* - test("PaperExample"){ - val result = FJTypeinference.typeinference("class List 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 extends Object{\nA a;\n\nget(){ return this.a;\n\n}\n}\n\n\nclass Test extends Object{\nList 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 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 extends Object{\nA f;\n add(a){\n return new List(a);\n}\n}" @@ -114,67 +76,4 @@ class IntegrationTest extends FunSuite { val result = FJTypeinference.typeinference(input) println(result.map(it => Main.prettyPrintAST(it))) } - /* - -class List extends Object{ - A head; - List tail; - add( a){ - return new List(a, this); - } - get(){ - return this.head; - } -} - -class PrincipleType extends Object { - function(a){ - return a.add(this).get(); - } -} - - -class Function extends Object{ -B b; -B apply(A a){ -return this.b; -} -} - - -class Box extends Object { -S val ; -map( f ) { -return new Box(f.apply(this.val)) ; -} -} - -class Function 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);} -} - - */ } From 58261b1fc487f4c1e37bd2f37f01b800ed3d4fb8 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 17 May 2022 12:22:02 +0200 Subject: [PATCH 10/25] Add assertions to IntegrationTest --- src/test/scala/IntegrationTest.scala | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index 2674000..75925e1 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -7,73 +7,86 @@ 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) } 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 extends Object{\n add(a){\n return this;\n}\n}") + assert(result.isRight) println(result.map(Main.prettyPrintAST(_))) } test("constructor.FieldInitialization") { val input = "class List 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 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 extends Object{\n A head;\n List 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 extends Object{\nA a;\nA b;\nB c;\nget(){return this.c;}\n}\nclass Function 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 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 extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n}\n\n\nclass Box 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 extends Object{\n A head;\n List 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 extends Object{\n A element;\n List 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))) } } From a24faf8f2defb43c2697611ba51235687eb47008 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 17 May 2022 12:22:21 +0200 Subject: [PATCH 11/25] remove uncessary variable --- src/main/scala/hb/dhbw/Unify.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 006071b..2de7e72 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -35,12 +35,11 @@ object Unify { } def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = { - var ret = eq eq.find(_ match{ case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true case _ => false }).map(it => { - subst(it.right.asInstanceOf[UnifyTV], it.left, ret.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left)) + subst(it.right.asInstanceOf[UnifyTV], it.left, eq.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left)) }) } From fdf3c03eb86b47d0df0445f9e6c224442d449a10 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 17 May 2022 12:22:40 +0200 Subject: [PATCH 12/25] Add Building comment to README --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index c86c4b1..b551f16 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,13 @@ -## Typeinference for Featherweight Java +# Typeinference for Featherweight Java + +## Getting started [Try it here](https://janulrich.github.io/FeatherweightTypeInference/) +## Building + +```sbt fullLinkJS``` + ### Input Examples ``` From 43ad1c4964adac377a575f360d94bbc6cd939c8f Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Mon, 30 May 2022 14:36:41 +0200 Subject: [PATCH 13/25] Cleanup --- src/main/scala/hb/dhbw/CartesianProduct.scala | 12 +----------- src/test/scala/CartesianProductTest.scala | 11 ----------- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/src/main/scala/hb/dhbw/CartesianProduct.scala b/src/main/scala/hb/dhbw/CartesianProduct.scala index b075424..4220891 100644 --- a/src/main/scala/hb/dhbw/CartesianProduct.scala +++ b/src/main/scala/hb/dhbw/CartesianProduct.scala @@ -1,17 +1,7 @@ package hb.dhbw 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 - } + //def addPossibilities(Set[A]) //TODO private var sizes: List[Int] = null private var max: Long = 1 diff --git a/src/test/scala/CartesianProductTest.scala b/src/test/scala/CartesianProductTest.scala index e6281dc..8249796 100644 --- a/src/test/scala/CartesianProductTest.scala +++ b/src/test/scala/CartesianProductTest.scala @@ -8,15 +8,4 @@ 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) - } - } From 3ae2bc2d61c43ed0f8d17538c3ff0aa049e4ca87 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Mon, 30 May 2022 14:37:32 +0200 Subject: [PATCH 14/25] Refactor unify. work in progress --- src/main/scala/hb/dhbw/Unify.scala | 45 +++++++++++++++++++++++++++--- 1 file changed, 41 insertions(+), 4 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 2de7e72..0e3f22f 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -70,12 +70,52 @@ object Unify { results } + def expandLB(lowerBound: UnifyLessDot, upperBound: UnifyLessDot, fc: FiniteClosure): Set[UnifyEqualsDot] ={ + 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 => UnifyEqualsDot(b, convertNamedType(t))) + } + def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={ val eq1 = eq.filter(c => c match{ case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true case _ => false }) + val eqRest = eq.filter(_ match { + case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => false + case _ => true + }) + val lowerBoundConstraints : Set[UnifyLessDot] = eq.filter(_ match { + case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => true + case _ => false + }).asInstanceOf[Set[UnifyLessDot]] + val lowerAndUpperBoundConstraints = lowerBoundConstraints.map(lowerBound => { + val upperBound = eq.find(_ match { + case UnifyLessDot(UnifyTV(a), UnifyRefType(n, params)) => UnifyTV(a).eq(lowerBound.right) + case _ => false + }).getOrElse(UnifyLessDot(lowerBound.right, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot] + (lowerBound, upperBound) + }) + val expandLBOrConstraints = lowerAndUpperBoundConstraints.map(bounds => expandLB(bounds._1, bounds._2, fc)) + val cartesianProductOfOrCons = new CartesianProduct(expandLBOrConstraints.map(_.map(Set(_)))) + + val tvInLowerBoundConstraints = lowerBoundConstraints.map(_.right.asInstanceOf[UnifyTV]) + val aUnifyLessDota = eq1.filter(c => c match{ + case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true + case _ => false + }).asInstanceOf[Set[UnifyLessDot]] + + tvInLowerBoundConstraints.map(tv => { + val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]] + .filter(variable => !variable.equals(tv) && isLinked(tv, variable, aUnifyLessDota)) + bs.map(b => { + //expandLB() + }) + }) + val cUnifyLessDotACons: Set[Set[Set[UnifyConstraint]]] = eq.map(c => c match{ case UnifyLessDot(UnifyRefType(name,params), UnifyTV(a)) => getSuperTypes(UnifyRefType(name,params), fc) @@ -83,10 +123,7 @@ object Unify { case _ => null }).filter(s => s!=null) - val aUnifyLessDota = eq1.filter(c => c match{ - case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true - case _ => false - }).asInstanceOf[Set[UnifyLessDot]] + val aUnifyLessDotCConsAndBs: Set[(UnifyLessDot,Option[UnifyTV])] = eq.map(c => c match{ case UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)) =>{ From 0e648ce11225e64b0f1c3053a9762efdb2d57209 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 1 Jun 2022 00:56:35 +0200 Subject: [PATCH 15/25] Unfinished state --- src/main/scala/hb/dhbw/Unify.scala | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 0e3f22f..9482246 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -78,6 +78,11 @@ object Unify { .map(t => UnifyEqualsDot(b, convertNamedType(t))) } + private def getUpperBound(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 eq1 = eq.filter(c => c match{ case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true @@ -93,10 +98,7 @@ object Unify { case _ => false }).asInstanceOf[Set[UnifyLessDot]] val lowerAndUpperBoundConstraints = lowerBoundConstraints.map(lowerBound => { - val upperBound = eq.find(_ match { - case UnifyLessDot(UnifyTV(a), UnifyRefType(n, params)) => UnifyTV(a).eq(lowerBound.right) - case _ => false - }).getOrElse(UnifyLessDot(lowerBound.right, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot] + val upperBound = getUpperBound(lowerBound.right.asInstanceOf[UnifyTV], eq) (lowerBound, upperBound) }) val expandLBOrConstraints = lowerAndUpperBoundConstraints.map(bounds => expandLB(bounds._1, bounds._2, fc)) @@ -108,11 +110,14 @@ object Unify { case _ => false }).asInstanceOf[Set[UnifyLessDot]] - tvInLowerBoundConstraints.map(tv => { + lowerBoundConstraints.map(lowerBound => { + val tv = lowerBound.right.asInstanceOf[UnifyTV] val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]] .filter(variable => !variable.equals(tv) && isLinked(tv, variable, aUnifyLessDota)) bs.map(b => { - //expandLB() + val upperBound = getUpperBound(b, eq) + //Result: + Set(expandLB(lowerBound, upperBound, fc), Set(UnifyLessDot(b, lowerBound.left))) }) }) From 66a589faabc917712e265b7f72a86ce0530e09e4 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Thu, 2 Jun 2022 15:55:22 +0200 Subject: [PATCH 16/25] Add extends Test --- src/test/scala/IntegrationTest.scala | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index 75925e1..37dee87 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -89,4 +89,11 @@ class IntegrationTest extends FunSuite { assert(result.isRight) println(result.map(it => Main.prettyPrintAST(it))) } + + test("extendsWithComplexType") { + val input = "class Pair extends Object {}\n\nclass Test extends Pair,A> {\n\nm(a){return this;}\n\n\n}" + val result = FJTypeinference.typeinference(input) + assert(result.isRight) + println(result.map(it => Main.prettyPrintAST(it))) + } } From 2d128362624dc527f8485a233ca7ca1462e5934d Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Tue, 14 Jun 2022 11:17:02 +0200 Subject: [PATCH 17/25] Add Test --- src/test/scala/UnifyTest.scala | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index 9351937..95624c8 100644 --- a/src/test/scala/UnifyTest.scala +++ b/src/test/scala/UnifyTest.scala @@ -25,6 +25,18 @@ class UnifyTest extends FunSuite { 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) + //assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b")))) + //assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a")))) + } /* test("Unify.step2") { var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")), From 8d3c6992ac36faaf361eec07c1bdd38f0f3dbe67 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Tue, 14 Jun 2022 17:36:11 +0200 Subject: [PATCH 18/25] Add Test --- src/main/scala/hb/dhbw/InsertTypes.scala | 3 +-- src/test/scala/IntegrationTest.scala | 7 +++++++ src/test/scala/UnifyTest.scala | 2 -- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala index 94ec681..c4d9622 100644 --- a/src/main/scala/hb/dhbw/InsertTypes.scala +++ b/src/main/scala/hb/dhbw/InsertTypes.scala @@ -11,7 +11,7 @@ object InsertTypes { case v => v } def sigma(x: UnifyType): Type = { x match { - case UnifyTV(n) => { + case UnifyTV(n) => val to = solvedCons.find(_.left == x).get to match { case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x) @@ -19,7 +19,6 @@ object InsertTypes { 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)) } diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index 37dee87..5d865dc 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -96,4 +96,11 @@ class IntegrationTest extends FunSuite { assert(result.isRight) println(result.map(it => Main.prettyPrintAST(it))) } + + test("pairAdd.twoTimes") { + val input = "class Pair 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))) + } } diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index 95624c8..b76418d 100644 --- a/src/test/scala/UnifyTest.scala +++ b/src/test/scala/UnifyTest.scala @@ -34,8 +34,6 @@ class UnifyTest extends FunSuite { 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) - //assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b")))) - //assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a")))) } /* test("Unify.step2") { From 84ee7b260a887fe8165405dceeea7ea9d80fe1fc Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Tue, 14 Jun 2022 19:07:48 +0200 Subject: [PATCH 19/25] Finish part 1 of step 2 --- src/main/scala/hb/dhbw/CartesianProduct.scala | 9 ++++ src/main/scala/hb/dhbw/Unify.scala | 43 ++++++++++--------- 2 files changed, 32 insertions(+), 20 deletions(-) diff --git a/src/main/scala/hb/dhbw/CartesianProduct.scala b/src/main/scala/hb/dhbw/CartesianProduct.scala index 4220891..a13440e 100644 --- a/src/main/scala/hb/dhbw/CartesianProduct.scala +++ b/src/main/scala/hb/dhbw/CartesianProduct.scala @@ -1,5 +1,14 @@ package hb.dhbw +class CartesianProductBuilder[A](){ + def addSingleton(a:A){ + throw new NotImplementedError() + } + def add(as : Set[A]): Unit ={ + throw new NotImplementedError() + } +} + class CartesianProduct[A](private val setOfSets: List[List[A]]){ //def addPossibilities(Set[A]) //TODO diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 9482246..8a0685d 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -70,39 +70,41 @@ object Unify { results } - def expandLB(lowerBound: UnifyLessDot, upperBound: UnifyLessDot, fc: FiniteClosure): Set[UnifyEqualsDot] ={ + 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 => UnifyEqualsDot(b, convertNamedType(t))) + Set(fc.superTypes(convertRefType(lowerBoundType)).filter(t => fc.aIsSubtypeOfb(t, convertRefType(upperBoundType))) + .map(t => UnifyEqualsDot(b, convertNamedType(t)))) } - private def getUpperBound(forTV: UnifyTV, eq: Set[UnifyConstraint]) = eq.find(_ match { + 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 eq1 = eq.filter(c => c match{ - case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true - case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true - case _ => false - }) - val eqRest = eq.filter(_ match { - case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => false - case _ => true - }) + //Part one: use expandLB on lower Bound constraints: + val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]() val lowerBoundConstraints : Set[UnifyLessDot] = eq.filter(_ match { case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => true case _ => false }).asInstanceOf[Set[UnifyLessDot]] val lowerAndUpperBoundConstraints = lowerBoundConstraints.map(lowerBound => { - val upperBound = getUpperBound(lowerBound.right.asInstanceOf[UnifyTV], eq) + val upperBound = getUpperBoundOrSetUpperBoundToObject(lowerBound.right.asInstanceOf[UnifyTV], eq) (lowerBound, upperBound) }) - val expandLBOrConstraints = lowerAndUpperBoundConstraints.map(bounds => expandLB(bounds._1, bounds._2, fc)) - val cartesianProductOfOrCons = new CartesianProduct(expandLBOrConstraints.map(_.map(Set(_)))) + //Add part one: + lowerAndUpperBoundConstraints.map(bounds => cpBuilder.add(expandLB(bounds._1, bounds._2, fc))) + + // Part two: a <. Type, a <.* b constraints: + //TODO + + val eq1 = eq.filter(c => c match{ + case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true + case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true + case _ => false + }) val tvInLowerBoundConstraints = lowerBoundConstraints.map(_.right.asInstanceOf[UnifyTV]) val aUnifyLessDota = eq1.filter(c => c match{ @@ -110,15 +112,16 @@ object Unify { case _ => false }).asInstanceOf[Set[UnifyLessDot]] - lowerBoundConstraints.map(lowerBound => { + lowerBoundConstraints.flatMap(lowerBound => { val tv = lowerBound.right.asInstanceOf[UnifyTV] val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]] .filter(variable => !variable.equals(tv) && isLinked(tv, variable, aUnifyLessDota)) - bs.map(b => { - val upperBound = getUpperBound(b, eq) + val ret : Set[CartesianProduct[UnifyConstraint]] = bs.map(b => { + val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq) //Result: - Set(expandLB(lowerBound, upperBound, fc), Set(UnifyLessDot(b, lowerBound.left))) + new CartesianProduct(Set[Set[Set[UnifyConstraint]]](Set(expandLB(lowerBound, upperBound, fc)), Set(Set(UnifyLessDot(b, lowerBound.left))))) }) + ret }) val cUnifyLessDotACons: Set[Set[Set[UnifyConstraint]]] = eq.map(c => c match{ From 09c7c1457fa5c2c342f45ba1061cf32d0cdc3b2d Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 15 Jun 2022 20:47:16 +0200 Subject: [PATCH 20/25] Implement Cartesian Product Builder and Unify.step2 --- src/main/scala/hb/dhbw/CartesianProduct.scala | 7 +- src/main/scala/hb/dhbw/Unify.scala | 106 ++++++++---------- src/test/scala/IntegrationTest.scala | 1 + 3 files changed, 54 insertions(+), 60 deletions(-) diff --git a/src/main/scala/hb/dhbw/CartesianProduct.scala b/src/main/scala/hb/dhbw/CartesianProduct.scala index a13440e..a544495 100644 --- a/src/main/scala/hb/dhbw/CartesianProduct.scala +++ b/src/main/scala/hb/dhbw/CartesianProduct.scala @@ -1,11 +1,14 @@ package hb.dhbw class CartesianProductBuilder[A](){ + var ret : Set[Set[A]] = Set() + def build() : CartesianProduct[A] = new CartesianProduct[A](ret) + def addSingleton(a:A){ - throw new NotImplementedError() + ret += Set(a) } def add(as : Set[A]): Unit ={ - throw new NotImplementedError() + ret += as } } diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 8a0685d..5b81f54 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -1,5 +1,7 @@ package hb.dhbw +import hb.dhbw.Unify.getLinks + 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) @@ -84,8 +86,9 @@ object Unify { }).getOrElse(UnifyLessDot(forTV, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot] def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={ + /* + //Part one: use expandLB on lower Bound constraints: - val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]() val lowerBoundConstraints : Set[UnifyLessDot] = eq.filter(_ match { case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => true case _ => false @@ -99,72 +102,51 @@ object Unify { // Part two: a <. Type, a <.* b constraints: //TODO - - val eq1 = eq.filter(c => c match{ + val aUnifyLessDota = eq.filter(c => c match{ case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true - case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true case _ => false - }) + }).asInstanceOf[Set[UnifyLessDot]] + eq.filter(_ match { + case UnifyLessDot(UnifyTV(_), UnifyRefType(_, _)) => true + case _ => false + }).map(cons => { + val tv : UnifyTV = cons.left.asInstanceOf[UnifyTV] + getLinks(tv, aUnifyLessDota) + .map(b => { + val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq) + val lowerBound = UnifyLessDot(cons.right, b) + //ExpandLB and add to return constraint set + cpBuilder.add(expandLB(lowerBound, upperBound, fc) + Set(UnifyLessDot(b,b))) - val tvInLowerBoundConstraints = lowerBoundConstraints.map(_.right.asInstanceOf[UnifyTV]) - val aUnifyLessDota = eq1.filter(c => c match{ + }) + }) + */ + val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]() + val aUnifyLessDota = eq.filter(c => c match{ case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true case _ => false }).asInstanceOf[Set[UnifyLessDot]] - lowerBoundConstraints.flatMap(lowerBound => { - val tv = lowerBound.right.asInstanceOf[UnifyTV] - val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]] - .filter(variable => !variable.equals(tv) && isLinked(tv, variable, aUnifyLessDota)) - val ret : Set[CartesianProduct[UnifyConstraint]] = bs.map(b => { - val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq) - //Result: - new CartesianProduct(Set[Set[Set[UnifyConstraint]]](Set(expandLB(lowerBound, upperBound, fc)), Set(Set(UnifyLessDot(b, lowerBound.left))))) - }) - ret - }) - - 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 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))) - } + 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 _ => 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 + 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} 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 eqSet = new CartesianProduct[Set[UnifyConstraint]]( - Set(Set(eq1)) ++ Set(Set(eq2)) ++ aUnifyLessDotCCons ++ cUnifyLessDotACons) - eqSet + cpBuilder.build() } private def getAUnifyLessDotC(from: Set[UnifyConstraint]) = from.filter(c => c match{ @@ -250,6 +232,14 @@ object Unify { case _ => true }) + /** + * Every 'b' with a <.* b + */ + private 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)) diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala index 5d865dc..74f7b41 100644 --- a/src/test/scala/IntegrationTest.scala +++ b/src/test/scala/IntegrationTest.scala @@ -15,6 +15,7 @@ class IntegrationTest extends FunSuite { 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"){ From c176dfdc9fae617e9f9e16e9efae4521c3b22179 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 15 Jun 2022 21:21:52 +0200 Subject: [PATCH 21/25] Fix expandLB --- src/main/scala/hb/dhbw/Unify.scala | 52 +++--------------------------- src/test/scala/UnifyTest.scala | 6 ++++ 2 files changed, 10 insertions(+), 48 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 5b81f54..a099608 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -76,8 +76,8 @@ object Unify { val b:UnifyTV = lowerBound.right.asInstanceOf[UnifyTV] val lowerBoundType : UnifyRefType = lowerBound.left.asInstanceOf[UnifyRefType] val upperBoundType : UnifyRefType = upperBound.right.asInstanceOf[UnifyRefType] - Set(fc.superTypes(convertRefType(lowerBoundType)).filter(t => fc.aIsSubtypeOfb(t, convertRefType(upperBoundType))) - .map(t => UnifyEqualsDot(b, convertNamedType(t)))) + fc.superTypes(convertRefType(lowerBoundType)).filter(t => fc.aIsSubtypeOfb(t, convertRefType(upperBoundType))) + .map(t => Set(UnifyEqualsDot(b, convertNamedType(t)))) } private def getUpperBoundOrSetUpperBoundToObject(forTV: UnifyTV, eq: Set[UnifyConstraint]) = eq.find(_ match { @@ -86,41 +86,6 @@ object Unify { }).getOrElse(UnifyLessDot(forTV, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot] def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={ - /* - - //Part one: use expandLB on lower Bound constraints: - val lowerBoundConstraints : Set[UnifyLessDot] = eq.filter(_ match { - case UnifyLessDot(UnifyRefType(_,_), UnifyTV(_)) => true - case _ => false - }).asInstanceOf[Set[UnifyLessDot]] - val lowerAndUpperBoundConstraints = lowerBoundConstraints.map(lowerBound => { - val upperBound = getUpperBoundOrSetUpperBoundToObject(lowerBound.right.asInstanceOf[UnifyTV], eq) - (lowerBound, upperBound) - }) - //Add part one: - lowerAndUpperBoundConstraints.map(bounds => cpBuilder.add(expandLB(bounds._1, bounds._2, fc))) - - // Part two: a <. Type, a <.* b constraints: - //TODO - val aUnifyLessDota = eq.filter(c => c match{ - case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true - case _ => false - }).asInstanceOf[Set[UnifyLessDot]] - eq.filter(_ match { - case UnifyLessDot(UnifyTV(_), UnifyRefType(_, _)) => true - case _ => false - }).map(cons => { - val tv : UnifyTV = cons.left.asInstanceOf[UnifyTV] - getLinks(tv, aUnifyLessDota) - .map(b => { - val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq) - val lowerBound = UnifyLessDot(cons.right, b) - //ExpandLB and add to return constraint set - cpBuilder.add(expandLB(lowerBound, upperBound, fc) + Set(UnifyLessDot(b,b))) - - }) - }) - */ val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]() val aUnifyLessDota = eq.filter(c => c match{ case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true @@ -128,11 +93,10 @@ object Unify { }).asInstanceOf[Set[UnifyLessDot]] eq.foreach(cons => cons match { - case UnifyLessDot(UnifyRefType(n, ps), UnifyTV(a)) => { + 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 => { @@ -235,7 +199,7 @@ object Unify { /** * Every 'b' with a <.* b */ - private def getLinks(a: UnifyTV, aUnifyLessDota: Set[UnifyLessDot]): Set[UnifyTV] = + 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)) @@ -366,13 +330,5 @@ object Unify { eqNew } - 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 - } - - } diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index b76418d..89d4304 100644 --- a/src/test/scala/UnifyTest.scala +++ b/src/test/scala/UnifyTest.scala @@ -35,6 +35,12 @@ class UnifyTest extends FunSuite { 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")), From 880fbdd905c10d21aee947f9d15dd0c38bd00ec3 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sun, 26 Jun 2022 23:15:15 +0200 Subject: [PATCH 22/25] Rework equalsRule. Fix circle detection --- src/main/scala/hb/dhbw/Unify.scala | 40 ++++++++++++++---------------- 1 file changed, 18 insertions(+), 22 deletions(-) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index a099608..053c667 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -218,33 +218,29 @@ 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]] - val circle = findCircles(aUnifyLessDota).find(!_.isEmpty) + 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) if(circle.isDefined){ val newEq = eq -- circle.get Some(newEq ++ (circle.get.map(c => UnifyEqualsDot(c.left, c.right)))) From 3c8cd302842bd036d490c9043fbbc376b2e4fec4 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Mon, 27 Jun 2022 22:23:12 +0200 Subject: [PATCH 23/25] Fix FC getSuperTypes --- src/main/scala/hb/dhbw/FiniteClosure.scala | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/main/scala/hb/dhbw/FiniteClosure.scala b/src/main/scala/hb/dhbw/FiniteClosure.scala index b1b9bec..f4bba31 100644 --- a/src/main/scala/hb/dhbw/FiniteClosure.scala +++ b/src/main/scala/hb/dhbw/FiniteClosure.scala @@ -28,10 +28,14 @@ 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(paramMap))) + (of,FJNamedType(p._2.name, p._2.params.map(paramSubst(_, paramMap)))) }) } private def superClassTypes(of: Set[(FJNamedType, FJNamedType)]) : Set[(FJNamedType, FJNamedType)] ={ From 6f48d04a7e13e1454b99ee5fd3e5d45088db2c2b Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 28 Jun 2022 19:28:02 +0200 Subject: [PATCH 24/25] Fix match rule --- src/main/scala/hb/dhbw/InsertTypes.scala | 2 +- src/main/scala/hb/dhbw/Unify.scala | 17 ++++++++++++----- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala index c4d9622..ce446f1 100644 --- a/src/main/scala/hb/dhbw/InsertTypes.scala +++ b/src/main/scala/hb/dhbw/InsertTypes.scala @@ -11,7 +11,7 @@ object InsertTypes { case v => v } def sigma(x: UnifyType): Type = { x match { - case UnifyTV(n) => + case UnifyTV(_) => val to = solvedCons.find(_.left == x).get to match { case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 053c667..d8078af 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -120,12 +120,13 @@ object Unify { def matchRule(eq : Set[UnifyConstraint], fc: FiniteClosure) = { val aUnifyLessDotC = getAUnifyLessDotC(eq) - (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)) + (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)) if(smallerC.isEmpty){ - c + List(c) }else{ - UnifyLessDot(smallerC.get.right, c.right) + val list = smallerC.toList + UnifyLessDot(list.head.right, c.right) :: list.tail } } ) @@ -321,7 +322,13 @@ object Unify { 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(matchRule(adoptRule(adaptRule(eqNew, fc), fc), fc)))) + 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 }while(!eqNew.equals(eqFinish)) eqNew } From 0e0c096d0fac73af4a53557509fc0cb3a116feaa Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 29 Jun 2022 15:20:59 +0200 Subject: [PATCH 25/25] Cleanup comments --- src/main/scala/hb/dhbw/CartesianProduct.scala | 2 -- src/main/scala/hb/dhbw/FJTypeinference.scala | 1 - src/main/scala/hb/dhbw/Unify.scala | 3 --- 3 files changed, 6 deletions(-) diff --git a/src/main/scala/hb/dhbw/CartesianProduct.scala b/src/main/scala/hb/dhbw/CartesianProduct.scala index a544495..b620f55 100644 --- a/src/main/scala/hb/dhbw/CartesianProduct.scala +++ b/src/main/scala/hb/dhbw/CartesianProduct.scala @@ -13,8 +13,6 @@ class CartesianProductBuilder[A](){ } class CartesianProduct[A](private val setOfSets: List[List[A]]){ - //def addPossibilities(Set[A]) //TODO - private var sizes: List[Int] = null private var max: Long = 1 private var i: Long = 0 diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala index 5e62062..fc76fb7 100644 --- a/src/main/scala/hb/dhbw/FJTypeinference.scala +++ b/src/main/scala/hb/dhbw/FJTypeinference.scala @@ -98,7 +98,6 @@ object FJTypeinference { 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(postProcessed, c), fc) typedClasses = typedClasses :+ typeInsertedC cOld :+ typeInsertedC diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index d8078af..dadf14e 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -1,8 +1,5 @@ package hb.dhbw -import hb.dhbw.Unify.getLinks - - 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)