From a2417d277a84f63ecb9a866d6762033c8b4f20f8 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Thu, 15 Aug 2024 17:03:27 +0200 Subject: [PATCH] Change extends Relation --- src/main/scala/unify/algorithm/Rules.scala | 17 +++---- src/main/scala/unify/algorithm/Unify.scala | 46 +++++++------------ .../scala/unify/model/ExtendsRelations.scala | 20 ++++++-- src/test/scala/UnifyTest.scala | 18 ++++++-- 4 files changed, 56 insertions(+), 45 deletions(-) diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala index a0d5bca..fb9d6e0 100644 --- a/src/main/scala/unify/algorithm/Rules.scala +++ b/src/main/scala/unify/algorithm/Rules.scala @@ -19,6 +19,10 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact val map: Map[Type, Type] = refType.wildcards.getWCBounds.filter(wcb => wcb.upper == wcb.lower).map(wcb => (Wildcard(wcb.name) -> wcb.upper)).toMap RefType(newWcs, refType.name, refType.params.map(_.substitute(map))) } + + /* + We treat wildcards as wildcards. The paper describes Wildcards and Generic variables as the same. This is not necessary here, because method type parameters appear in the extends Relation and are RefTypes + */ def applyRules() = { while eraseCircleRule() @@ -67,7 +71,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact }) cs.getLessDotCons.foreach(f = cons => cons match { case LessDot(a, b, _) if a == b => cs.remove(cons) //Erase - case LessDot(left: Wildcard, right: (RefType | TypeVariable | Wildcard), cc) => // Upper + case LessDot(left: Wildcard, right: (RefType | TypeVariable | Wildcard | WTypeVariable), cc) => // Upper cs.remove(cons) cs.add(LessDot(cs.wildcardEnv.getUpperBound(left), right, cc)) case LessDot(left: (RefType | Wildcard), right: Wildcard, cc) => // Lower @@ -131,10 +135,10 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact cs.addAll(wc2.map(wcb => LessDot(wcb.lower.substitute(freshTVMap), Wildcard(wcb.name).substitute(freshTVMap)))) } else if(fc.isPossibleSupertype(n1, n2)) { //Adapt val subtypeRelation = fc.supertype(n1) // C <. D - val paramMap = subtypeRelation._1.params.zip(p1).toMap - val newParams = subtypeRelation._2.params.map(_.substitute(paramMap)) + val paramMap:Map[Type,Type] = subtypeRelation.params.zip(p1).toMap + val newParams = subtypeRelation.superTyp.params.map(_.substitute(paramMap)) cs.remove(cons) - cs.add(LessDot(RefType(wc1, subtypeRelation._2.name, newParams), RefType(wc2, n2, p2))) + cs.add(LessDot(RefType(wc1, subtypeRelation.superTyp.name, newParams), RefType(wc2, n2, p2))) } else { // TODO: Insolvable Constraint set } @@ -144,6 +148,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact val nWcs = WildcardEnvironment(wcs.bounds.filter(b => toRemove.contains(Wildcard(b._1))).map(b => WildcardBound(b._1, b._2._1, b._2._2)).toSet) cs.add(LessDot(RefType(nWcs, n, params), right, cc)) case LessDot(left: TypePlaceholder, right: TypePlaceholder, _) => // do nothing + case LessDot(left: RefType, right: TypePlaceholder, _) => // do nothing -> those are processed in step 2 }) } @@ -205,8 +210,4 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact cs.add(EqualsDot(cs.wildcardEnv.getUpperBound(left), right)) cs.add(EqualsDot(cs.wildcardEnv.getLowerBound(left), right)) } - def substRule(c: EqualsDot): Unit = { - cs.remove(c) - cs.substitute(c.right, c.left) - } diff --git a/src/main/scala/unify/algorithm/Unify.scala b/src/main/scala/unify/algorithm/Unify.scala index bdece42..68eedcb 100644 --- a/src/main/scala/unify/algorithm/Unify.scala +++ b/src/main/scala/unify/algorithm/Unify.scala @@ -1,6 +1,6 @@ package unify.algorithm -import unify.model.{BotType, ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, WTypeVariable, Wildcard, WildcardBound, WildcardEnvironment, emptyWCs} +import unify.model.* import java.util.concurrent.{CompletableFuture, ExecutorService, Future} import scala.collection.mutable @@ -42,10 +42,7 @@ class Unify { def step2(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFactory) = { val ret: mutable.Set[ConstraintSet] = mutable.Set() - cs.getLessDotCons.find(cons => cons match { - case LessDot(RefType(w, n, p), TypeVariable(a), _) => true - case _ => false - }).map(cons => cons match { + cs.getLessDotCons.map(cons => cons match { case LessDot(RefType(w, n, p), TypeVariable(a), _) => //Same rule val cs1 : ConstraintSet = cs.copy() @@ -69,8 +66,8 @@ class Unify { val cs4: ConstraintSet = cs.copy() cs4.remove(cons) val cType = cons.left.asInstanceOf[RefType] - val paramMap = fc.supertype(cType.name)._1.params.zip(cType.params).toMap - val superType = fc.supertype(cType.name)._2 + val paramMap: Map[Type,Type] = fc.supertype(cType.name).params.zip(cType.params).toMap + val superType = fc.supertype(cType.name).superTyp val newSuperType = RefType(cType.wildcards, superType.name, superType.params.map(p => p.substitute(paramMap))) cs4.add(LessDot(newSuperType, cons.right)) @@ -83,12 +80,19 @@ class Unify { cs1.add(EqualsDot(WTypeVariable(a), RefType(w,n,p))) ret.add(cs1) - val cs2 : ConstraintSet = cs.copy() - cs2.remove(cons) - //TODO: - // the fewer branches the better. should wildcard variables be ignored? - // constraints of the form T <. a? <. T' could be kept in the constraint set. Unify does not spawn type solutions for them anyway - // Process normal type placeholders first. then wildcard placeholders! + //Super rule + //Object is the exception, which does not have a supertype + if(!cons.left.asInstanceOf[RefType].name.equals("Object")){ + val cs4: ConstraintSet = cs.copy() + cs4.remove(cons) + val cType = cons.left.asInstanceOf[RefType] + val paramMap: Map[Type,Type] = fc.supertype(cType.name).params.zip(cType.params).toMap + val superType = fc.supertype(cType.name).superTyp + + val newSuperType = RefType(cType.wildcards, superType.name, superType.params.map(p => p.substitute(paramMap))) + cs4.add(LessDot(newSuperType, cons.right)) + ret.add(cs4) + } } case _ => {} }) @@ -110,22 +114,6 @@ class Unify { } case _ => {} }) - /* - cs.getALessDotCCons().filter(cons => !cs.fv(cons.right).isEmpty).map(cons => { - //Force - val csForce: ConstraintSet = cs.copy() - val fvs = cs.fv(cons.right) - if(fvs.find(t => !t.isInstanceOf[Wildcard]).isEmpty){ - val freeWildcards = fvs.map(_.asInstanceOf[Wildcard]) - val oldRight = cons.right.asInstanceOf[RefType] - val newCons = freeWildcards.map(wc => LessDot(cs.getUpperBound(wc), cs.getLowerBound(wc))) ++ freeWildcards.map(wc => LessDot(cs.getLowerBound(wc), cs.getUpperBound(wc))) - csForce.remove(cons) - csForce.add(LessDot(cons.left, RefType(oldRight.wildcards ++ freeWildcards, oldRight.name, oldRight.params))) - csForce.addAll(newCons) - ret.add(csForce) - } - }) - */ ret.toSet } diff --git a/src/main/scala/unify/model/ExtendsRelations.scala b/src/main/scala/unify/model/ExtendsRelations.scala index 5d373ef..59e9a34 100644 --- a/src/main/scala/unify/model/ExtendsRelations.scala +++ b/src/main/scala/unify/model/ExtendsRelations.scala @@ -1,12 +1,24 @@ package unify.model -class ExtendsRelations(val extendsRelations : Set[(RefType, RefType)]): +/** + * + * @param subtypeName + * @param params - Reftypes of the form Reftype(Empty, "X", Empty) + * @param paramUpperBounds - Upper types + * @param superTyp - and the supertype. Both can use the Reftypes stated in params + */ +sealed class ExtendsRelation(val subtypeName: String, val params: List[RefType], val paramUpperBounds: List[RefType], val superTyp: RefType) - def supertype(of: String): (RefType, RefType) = extendsRelations.find(r => r._1.name.equals(of)).get +class ExtendsRelations(val extendsRelations : Set[ExtendsRelation]): + + def supertype(of: String): ExtendsRelation = { + System.out.println(of) + extendsRelations.find(r => r.subtypeName.equals(of)).get + } def isPossibleSupertype(of: String, superType: String): Boolean = { if (of.equals(superType)) return true - extendsRelations.find(r => r._1.name.equals(of)) // check if supertype exists - .map(_ => isPossibleSupertype(supertype(of)._2.name, superType)) + extendsRelations.find(r => r.subtypeName.equals(of)) // check if supertype exists + .map(_ => isPossibleSupertype(supertype(of).superTyp.name, superType)) .getOrElse(false) } diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala index 7c14244..cf86176 100644 --- a/src/test/scala/UnifyTest.scala +++ b/src/test/scala/UnifyTest.scala @@ -1,12 +1,14 @@ import unify.algorithm.Unify -import unify.model.{ConstraintSet, ExtendsRelations, LessDot, RefType, TypeVariable, WTypeVariable, emptyWCs} +import unify.model.{ConstraintSet, ExtendsRelation, ExtendsRelations, LessDot, RefType, TypeVariable, WTypeVariable, emptyWCs} class UnifyTest extends munit.FunSuite { + def typeParam(name: String) = RefType(emptyWCs(), name, List.empty) + def objectRefType() = RefType(emptyWCs(), "Object", List()) def standardFC() = { - val listType = RefType(emptyWCs(), "List", List(RefType(emptyWCs(), "X", List.empty))) - val objectType = RefType(emptyWCs(), "Object", List.empty) - new ExtendsRelations(Set((listType, objectType))) + val arrayExtList = ExtendsRelation("ArrayList", List(typeParam("X")), List(objectRefType()), RefType(emptyWCs(), "List", List(typeParam("X")))) + val listExtObject = ExtendsRelation("List", List(typeParam("X")), List(objectRefType()), objectRefType()) + new ExtendsRelations(Set(arrayExtList, listExtObject)) } test("Match Test") { @@ -30,4 +32,12 @@ class UnifyTest extends munit.FunSuite { assert(result.nonEmpty) } + test("General rule test") { + val start: ConstraintSet = new ConstraintSet() + start.add(LessDot(RefType(emptyWCs(), "ArrayList", List(TypeVariable("x"))), TypeVariable("a"))) + + val result = new Unify().unifyIterative(start, standardFC()) + System.out.println(result) + assert(result.nonEmpty) + } }