From b576d90f9aa6a6758dcacef38e690123d7efd119 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 13 Oct 2021 16:58:27 +0200 Subject: [PATCH] Unify v1 --- build.sbt | 1 + src/main/scala/hb/dhbw/Main.scala | 38 +++++---- src/main/scala/hb/dhbw/Unify.scala | 128 +++++++++++++++++++++-------- src/test/scala/UnifyTest.scala | 30 +++++++ 4 files changed, 147 insertions(+), 50 deletions(-) create mode 100644 src/test/scala/UnifyTest.scala diff --git a/build.sbt b/build.sbt index e69de29..1333753 100644 --- a/build.sbt +++ b/build.sbt @@ -0,0 +1 @@ +libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.8" % Test \ No newline at end of file diff --git a/src/main/scala/hb/dhbw/Main.scala b/src/main/scala/hb/dhbw/Main.scala index c2b699c..94b1216 100644 --- a/src/main/scala/hb/dhbw/Main.scala +++ b/src/main/scala/hb/dhbw/Main.scala @@ -9,37 +9,47 @@ object Main { val fcPair1 = (RefType("ArrayList", List(TypeVariable("A"))), RefType("List", List(TypeVariable("A")))) val fcPair3 = (RefType("List", List(TypeVariable("A"))), RefType("Object", List())) val fcPair2 = (RefType("MyMap", List(TypeVariable("A"), TypeVariable("B"))), RefType("Map", List(RefType("String", List(TypeVariable("A"))), TypeVariable("B")))) - val cTest = Set(Set(1,2), Set(4,3)) + val cTest: Set[Set[Int]] = Set(Set(1,2), Set(4,3)) val fc = new FiniteClosure(Set(fcPair1, fcPair2, fcPair3)) - val cart = Unify.cartesianProduct(cTest) - println(cart) + //val cart = Unify.cartesianProduct(cTest) + //println(cart) - val superTypes = fc.superTypes(RefType("List", List(RefType("Object", List())))) - println(superTypes) + //val superTypes = fc.superTypes(RefType("List", List(RefType("Object", List())))) + //println(superTypes) - val step1 = Unify.step1(Set(LessDot(TypeVariable("a"), TypeVariable("b")), - LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc) - println(step1) + //val step1 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")), + // LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc) + //println(step1) - println(fc.isPossibleSupertype("MyMap", "List")) + //val step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")), + // LessDot(RefType("List", List(RefType("Object", List()))), TypeVariable("a"))), fc) + //println(step2) + + //println(fc.isPossibleSupertype("MyMap", "List")) val eqMatchTest = Set(LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("a"), RefType("ArrayList", List(RefType("Object", List()))))) - println(Unify.matchRule(eqMatchTest.asInstanceOf[Set[Unify.Constraint]], fc)) + //println(Unify.matchRule(eqMatchTest.asInstanceOf[Set[Unify.Constraint]], fc)) val eqEqualsTest : Set[Constraint] = Set(LessDot(TypeVariable("a"), TypeVariable("b")),LessDot(TypeVariable("b"), TypeVariable("c")), LessDot(TypeVariable("c"), TypeVariable("a"))) - println(Unify.equalsRule(eqEqualsTest)) + //println(Unify.equalsRule(eqEqualsTest)) //val eqIsLinkedTest = Set(LessDot(TypeVariable("a"), TypeVariable("c")), LessDot(TypeVariable("b"), TypeVariable("c"))) //println(Unify.isLinked(TypeVariable("a"), TypeVariable("b"), eqIsLinkedTest)) val eqAdoptTest = Set(LessDot(TypeVariable("b"), TypeVariable("a")),LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("b"), RefType("ArrayList", List(RefType("Object", List()))))) - println(Unify.adoptRule(eqAdoptTest.asInstanceOf[Set[Constraint]], fc)) + //println(Unify.adoptRule(eqAdoptTest.asInstanceOf[Set[Constraint]], fc)) val eqAdaptTest: Set[Constraint] = Set(EqualsDot(TypeVariable("a"), TypeVariable("b")),LessDot(RefType("ArrayList",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List()))))) - println(Unify.adaptRule(eqAdaptTest, fc)) + //println(Unify.adaptRule(eqAdaptTest, fc)) val eqReduceTest : Set[Constraint] = Set(EqualsDot(RefType("List",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List()))))) - println(Unify.reduceRule(eqReduceTest)) + //println(Unify.reduceRule(eqReduceTest)) + + val applyRulesTest = eqMatchTest ++ eqEqualsTest ++ eqAdoptTest ++ eqAdaptTest ++ eqReduceTest + //println(Unify.applyRules(fc)(applyRulesTest)) + + println(Unify.unify(Set(Set(applyRulesTest)), fc)) + //val replacedType = fc.replaceParams(RefType("List", List(TypePlaceholder("A"))), RefType("ArrayList", List(RefType("String", List())))) //println(replacedType) //val replacedType2 = fc.replaceParams(RefType("Map", List(RefType("String", List(TypePlaceholder("A"))), TypePlaceholder("B"))), RefType("MyMap", List(RefType("String", List()), RefType("Integer", List())))) diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala index 2818419..383f0a9 100644 --- a/src/main/scala/hb/dhbw/Unify.scala +++ b/src/main/scala/hb/dhbw/Unify.scala @@ -3,15 +3,27 @@ package hb.dhbw object Unify { - sealed abstract class Constraint - final case class LessDot(left: Type, right: Type) extends Constraint - final case class EqualsDot(left: Type, right: Type) extends Constraint - - def unify(finiteClosure: FiniteClosure): Unit ={ + sealed abstract class Constraint(val left: Type, val right: Type) + final case class LessDot(override val left: Type, override val right: Type) extends Constraint(left, right) + final case class EqualsDot(override val left: Type, override val right: Type) extends Constraint(left, right) + def unify(orCons: Set[Set[Set[Constraint]]], fc: FiniteClosure) : Set[Set[Constraint]] = { + 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){ + Set(substResult) + }else{ + unify(Set(Set(substResult)), fc).map(s => s + unifier.get) + } + }) } - def step1(eq : Set[Constraint], fc: FiniteClosure) ={ + def step2(eq : Set[Constraint], fc: FiniteClosure) ={ val eq1 = eq.filter(c => c match{ case LessDot(TypeVariable(_), TypeVariable(_)) => true case EqualsDot(TypeVariable(_), TypeVariable(_)) => true @@ -23,26 +35,40 @@ object Unify { .map(superType => Set(EqualsDot(TypeVariable(a), superType).asInstanceOf[Constraint])) case _ => null }).filter(s => s!=null) - //val mutatedCLessdotACons = cartesianProduct(cLessdotACons) - val aLessdotCCons: Set[Set[Set[Constraint]]] = eq.map(c => c match{ + + val alessdota = eq1.filter(c => c match{ + case LessDot(TypeVariable(_), TypeVariable(_)) => true + case _ => false + }).asInstanceOf[Set[LessDot]] + + val aLessdotCConsAndBs: Set[(LessDot,Option[TypeVariable])] = eq.map(c => c match{ case LessDot(TypeVariable(a),RefType(name,params)) =>{ - val bs = eq1.filter(c => c match{ - case LessDot(TypeVariable(leftSide), TypeVariable(_)) => leftSide.equals(a) - case _ => false - }).map(p => p.asInstanceOf[LessDot].right).asInstanceOf[Set[TypeVariable]] - bs.map(b => { - val allSuperTypes = fc.superTypes(RefType(name,params)) - .map(superType => Set(EqualsDot(b, superType).asInstanceOf[Constraint])) - Set(Set(LessDot(b, RefType(name,params))) ++ allSuperTypes - ) - }) - fc.superTypes(RefType(name,params)) - .map(superType => Set(EqualsDot(TypeVariable(a), superType).asInstanceOf[Constraint])) + val bs = alessdota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[TypeVariable]] + .filter(c => !a.equals(c) && isLinked(TypeVariable(a), c, alessdota)) + if(bs.isEmpty){ + Set((LessDot(TypeVariable(a),RefType(name,params)),None)) + }else{ + bs.map(b => (LessDot(TypeVariable(a),RefType(name,params)),Some(b))) + } } case _ => null - }).filter(s => s!=null) - //val mutadedALessdotCCons = cartesianProduct(aLessdotCCons) - val eqSet = cartesianProduct(Set(Set(eq1)) ++ aLessdotCCons ++ cLessdotACons) + }).filter(s => s!=null).flatten + + val aLessdotCCons = aLessdotCConsAndBs.map{ + case (ac:LessDot,Some(b)) => + Set(Set(LessDot(b, ac.right))) ++ + fc.superTypes(ac.right.asInstanceOf[RefType]) + .map(superType => Set(EqualsDot(b, superType))) + case (ac, None) => null + }.filter(c => c != null).asInstanceOf[Set[Set[Set[Constraint]]]] + + val eq2 = eq.filter(c => c match{ + case LessDot(TypeVariable(_), RefType(_,_)) => true + case EqualsDot(TypeVariable(_), RefType(_,_)) => true + case EqualsDot(RefType(_,_),TypeVariable(_)) => true + case _ => false + }) + val eqSet = cartesianProduct(Set(Set(eq1)) ++ Set(Set(eq2)) ++ aLessdotCCons ++ cLessdotACons) eqSet.map( s => s.flatten) } @@ -155,25 +181,55 @@ object Unify { val circle = findCircles(aLessdota).find(!_.isEmpty) if(circle.isDefined){ val newEq = eq -- circle.get - newEq ++ (circle.get.map(c => EqualsDot(c.left, c.right))) + Some(newEq ++ (circle.get.map(c => EqualsDot(c.left, c.right)))) }else{ - eq + None } } - def applyRules(fc: FiniteClosure) ={ + private def paramsContain(tv: TypeVariable, inParams: RefType): Boolean = + inParams.params.find(t => t match { + case TypeVariable(a) => tv.equals(TypeVariable(a)) + case RefType(a,p) => paramsContain(tv, RefType(a,p)) + }).isDefined + def substStep(eq: Set[Constraint]) = eq.find(c => c match { + case EqualsDot(TypeVariable(a), RefType(n, p)) => !paramsContain(TypeVariable(a), RefType(n,p)) + case _ => false + }).map(c => (subst(c.left.asInstanceOf[TypeVariable], c.right.asInstanceOf[RefType], eq), Some(c))).getOrElse((eq, None)) + + private def subst(a: TypeVariable, withType: RefType,in: Type) :Type = in match { + case RefType(n, p) => RefType(n,p.map(t => subst(a, withType, t)).asInstanceOf[List[Type]]) + case TypeVariable(n) => + if(a.equals(in)){withType}else{in} } - def cartesianProduct[A](lists : Set[Set[A]]) : Set[Set[A]] ={ - def listMultiply[A](inFront: Set[A], list: Set[Set[A]]) = list.flatMap(s => inFront.map(element => s + element)) - - if(lists.size == 1) { - lists.head.map(it => Set(it)) - } - else{ - listMultiply(lists.head, cartesianProduct(lists.tail)) - } - + def subst(a: TypeVariable, refType: RefType,eq: Set[Constraint]): Set[Constraint] = { + eq.map(c => c match { + case LessDot(left, right) => LessDot(subst(a, refType, left), subst(a, refType, right)) + case EqualsDot(left, right) => EqualsDot(subst(a, refType, left), subst(a, refType, right)) + }) } + + private def doWhileSome(fun: Set[Constraint]=>Option[Set[Constraint]], eqTemp: Set[Constraint]): Set[Constraint] = + fun(eqTemp).map(eqTemp2 => doWhileSome(fun,eqTemp2)).getOrElse(eqTemp) + + def applyRules(fc: FiniteClosure) = (eq: Set[Constraint]) => { + var eqNew: Set[Constraint] = null + var eqFinish: Set[Constraint] = eq + do{ + eqNew = doWhileSome(Unify.equalsRule,eqFinish) + eqFinish = reduceRule(matchRule(adaptRule(adaptRule(eqNew, fc), fc), fc)) + }while(!eqNew.equals(eqFinish)) + 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 new file mode 100644 index 0000000..1edc62b --- /dev/null +++ b/src/test/scala/UnifyTest.scala @@ -0,0 +1,30 @@ + +import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify} +import hb.dhbw.Unify.LessDot +import org.scalatest.FunSuite + +class UnifyTest extends FunSuite { + val fcPair1 = (RefType("ArrayList", List(TypeVariable("A"))), RefType("List", List(TypeVariable("A")))) + val fcPair3 = (RefType("List", List(TypeVariable("A"))), RefType("Object", List())) + val fcPair2 = (RefType("MyMap", List(TypeVariable("A"), TypeVariable("B"))), RefType("Map", List(RefType("String", List(TypeVariable("A"))), TypeVariable("B")))) + + val fc = new FiniteClosure(Set(fcPair1, fcPair2, fcPair3)) + + test("Unify.step2.alinkedb"){ + var step2 = Unify.step2(Set(LessDot(TypeVariable("c"), TypeVariable("b")), + LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc) + assert(step2.head.size == 2) + } + + test("Unify.step2") { + var step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")), + LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc) + println(step2) + assert(!step2.isEmpty) + + step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")), + LessDot(RefType("List", List(RefType("Object", List()))), TypeVariable("a"))), fc) + println(step2) + } + +}