From 93af1d12f68c7b2b4e434a0f204ae0c1d75d5138 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sat, 16 Apr 2022 15:44:59 +0200 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 4/4] 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)) }) }