stan/WildFJ-Typeinference
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fixes. Match Test runs now

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-27 19:50:02 +01:00
parent 6538be956f
commit 059217974d
5 changed files with 91 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/main/scala/unify/algorithm/Rules.scala
View File

@ -15,7 +15,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
}
}
private def crunch(refType: RefType): RefType = {
val newWcs = WildcardEnvironment(refType.wildcards.getWCBounds.filter(wcb => wcb.upper == wcb.lower))
val newWcs = WildcardEnvironment(refType.wildcards.getWCBounds.filter(wcb => wcb.upper != wcb.lower))
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)))
}
@ -23,7 +23,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
while
eraseCircleRule()
cs.hasChanged()
do (cs.hasChanged())
do ()
cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
cons match {
case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
@ -51,9 +51,8 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
case EqualsDot(left: RefType, right: RefType) => // Equals rule
if (left.params.size == right.params.size && left.name == right.name) {
cs.remove(cons)
left.params.zip(right.params).map(pp => EqualsDot(pp._1, pp._2)) foreach {
cs.add(_)
}
cs.add(LessDot(cons.left, cons.right))
cs.add(LessDot(cons.right, cons.left))
} else {
//TODO: insolvable constraint set!
}
@ -92,7 +91,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
case LessDot(left: TypePlaceholder, right: RefType, cc) =>
val alessdotc = cs.getALessDotCCons
//match rule:
alessdotc.find(ic => (ic != cons && cons.left.equals(cons.left))).map(ic => {
alessdotc.find(ic => (ic != cons && ic.left.equals(cons.left))).map(ic => {
if (fc.isPossibleSupertype(cons.right.asInstanceOf[RefType].name, ic.right.asInstanceOf[RefType].name)) {
matchRule(cons, ic)
} else {
@ -102,18 +101,25 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
//adopt rule:
cs.getALessDotBCons.find(_.right == left).map(blessa => {
cs.getALessDotCCons.find(_.left == blessa.left).map(blessN => {
if(cs.notProcessed(blessa.left.asInstanceOf[TypePlaceholder], blessa.right.asInstanceOf[TypePlaceholder])){
cs.add(LessDot(blessN.left, cons.right))
cs.setProcessedByAdopt(blessa.left.asInstanceOf[TypePlaceholder], blessa.right.asInstanceOf[TypePlaceholder])
}
//TODO: Check if adopt rule got already applied
// different approach: Do the adopt and circle rule at the beginning of the algorithm. Then never again
cs.add(LessDot(blessN.left, cons.right))
})
})
if(right.wildcards.getWCBounds.filter(wcb => wcb.upper == wcb.lower).nonEmpty){ //Crunch
cs.remove (cons)
cs.add (LessDot (left, crunch (right), cc) )
}
case LessDot(RefType(wc, n, params), right: RefType, cc) if right.fvs().isEmpty | cc > 0 => // Capture und Prepare
case LessDot(RefType(wc, n, params), right: RefType, cc) if (right.fvs().isEmpty | cc > 0) & !wc.isEmpty => // Capture und Prepare
cs.remove(cons)
cs.add(LessDot(RefType(emptyWCs(), n, params), right))
val freshWCs = wc.map(wcb => WildcardBound(tvFactory.freshName(), wcb.upper, wcb.lower))
val wcMap: Map[Type,Type] = wc.map(wcb => Wildcard(wcb.name)).zip(freshWCs.map(wcb => Wildcard(wcb.name))).toMap
cs.addWildcards(new WildcardEnvironment(freshWCs.map(wcb => WildcardBound(wcb.name, wcb.upper.substitute(wcMap), wcb.lower.substitute(wcMap)))))
cs.add(LessDot(RefType(emptyWCs(), n, params.map(_.substitute(wcMap))), right))
case LessDot(RefType(wc1, n1, p1), RefType(wc2, n2, p2), cc) =>
if (wc1.isEmpty & n1 == n2 & p1.size == p2.size) {//Reduce
cs.remove(cons)
@ -126,7 +132,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
val paramMap = subtypeRelation._1.params.zip(p1).toMap
val newParams = subtypeRelation._2.params.map(_.substitute(paramMap))
cs.remove(cons)
cs.add(LessDot(RefType(wc1, n1, newParams), RefType(wc2, n2, p2)))
cs.add(LessDot(RefType(wc1, subtypeRelation._2.name, newParams), RefType(wc2, n2, p2)))
} else {
// TODO: Insolvable Constraint set
}
@ -135,6 +141,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
val toRemove = wcs.getWildcards().diff(params.flatMap(_.fvs()).toSet)
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
})
}
@ -147,8 +154,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
cs.remove(c1)
cs.remove(c2)
val wcFactory = new WildcardFactory()
val freshWildcards = c1.right.asInstanceOf[RefType].params.map(_ => WildcardBound(wcFactory.freshName(), tvFactory.freshTV(), tvFactory.freshTV()))
val freshWildcards = c1.right.asInstanceOf[RefType].params.map(_ => WildcardBound(tvFactory.freshName(), tvFactory.freshTV(), tvFactory.freshTV()))
cs.addAll(freshWildcards.map(wc => LessDot(wc.lower, wc.upper)))
val freshSubtype = RefType(new WildcardEnvironment(freshWildcards.toSet),
c1.right.asInstanceOf[RefType].name,

41
src/main/scala/unify/algorithm/Unify.scala
View File

@ -1,11 +1,31 @@
package unify.algorithm
import unify.model.{BotType, ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, Wildcard, WildcardBound, WildcardEnvironment, WildcardFactory, emptyWCs}
import unify.model.{BotType, ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, Wildcard, WildcardBound, WildcardEnvironment, emptyWCs}
import java.util.concurrent.{CompletableFuture, ExecutorService, Future}
import scala.collection.mutable
class Unify {
def unifyIterative(start: ConstraintSet, fc: ExtendsRelations): Set[UnifySolution] = {
var solved: Set[UnifySolution] = Set()
var css: Set[ConstraintSet] = Set(start) //the working queue
val tvFactory: TypeVariableFactory = new TypeVariableFactory()
while (!css.isEmpty) {
val sorted = css //.toList.sortBy(c => c.getLessDotCons.size)
val cs: ConstraintSet = sorted.head
css = sorted.tail.toSet
while
//apply Rules (step 1)
step1(cs, fc, tvFactory)
// Step 3 add all new constraint sets in the working queue css
val step2Additions = step2(cs, fc, tvFactory)
css = css ++ step2Additions
cs.hasChanged()
do ()
step4(cs).map(s => solved = solved + s)
}
solved
}
/**
* The steps transforming the constraint set (including substitution)
* but without branching into multiple constraint sets
@ -20,7 +40,7 @@ class Unify {
do ()
}
def step3(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFactory) = {
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
@ -33,8 +53,7 @@ class Unify {
//General rule
val cs3: ConstraintSet = cs.copy()
val wcFactory = new WildcardFactory()
val freshWCs = p.map(_ => WildcardBound(wcFactory.freshName(), tvFactory.freshTV(), tvFactory.freshTV()))
val freshWCs = p.map(_ => WildcardBound(tvFactory.freshName(), tvFactory.freshTV(), tvFactory.freshTV()))
val freshC = RefType(new WildcardEnvironment(freshWCs.toSet), n, freshWCs.map(wcb => Wildcard(wcb.name)))
cs3.add(EqualsDot(cons.right, freshC))
//cs3.addAll(freshWCs.map(w => LessDot(cs3.getLowerBound(w), cs3.getUpperBound(w))))
@ -114,11 +133,15 @@ class Unify {
})
//SubElim rule
cs.getALessDotBCons.map(cons => {
cs.remove(cons)
cs.substitute(cons.left, cons.right)
cs.add(EqualsDot(cons.right, cons.left))
})
while
cs.getALessDotBCons.nonEmpty
do {
val cons = cs.getALessDotBCons.head
cs.remove(cons)
cs.substitute(cons.left, cons.right)
cs.add(EqualsDot(cons.right, cons.left))
}
cs.solvedForm()
}
}

13
src/main/scala/unify/model/ConstraintSet.scala
View File

@ -24,6 +24,7 @@ class ConstraintSet( private var processedUnifier: Set[TypeVariable] = Set(),
ret
}
def addWildcards(env: WildcardEnvironment) = bounds = WildcardEnvironment(bounds.getWCBounds ++ env.getWCBounds)
def getEqualsDotCons = equalsdot
def getLessDotCons: Set[LessDot] = lessdot
@ -129,11 +130,13 @@ class ConstraintSet( private var processedUnifier: Set[TypeVariable] = Set(),
//GenSigma
val toRemove = getEqualsDotCons.filter(_.left.isInstanceOf[TypeVariable]).find(c => c.right.tvs().isEmpty && c.right.wtvs().isEmpty
&& sigma.contains(c.left.asInstanceOf[TypeVariable])).map(c => {
sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> c.right)
this.remove(c)
})
while
getEqualsDotCons.filter(_.left.isInstanceOf[TypeVariable]).find(c => c.right.tvs().isEmpty && c.right.wtvs().isEmpty
&& !sigma.contains(c.left.asInstanceOf[TypeVariable])).map(c => {
sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> c.right)
this.remove(c)
}).isDefined
do()
if (this.getAllConstraints.isEmpty) {
val ret = new UnifySolution(WildcardEnvironment(delta), sigma)

13
src/main/scala/unify/model/WildcardFactory.scala
View File

@ -1,13 +0,0 @@
package unify.model
import java.util.concurrent.atomic.AtomicInteger
class WildcardFactory {
val tpvNum = new AtomicInteger()
def freshName() = {
val current = tpvNum.incrementAndGet()
current.toString
}
}

33
src/test/scala/UnifyTest.scala Normal file
View File

@ -0,0 +1,33 @@
import unify.algorithm.Unify
import unify.model.{ConstraintSet, ExtendsRelations, LessDot, RefType, TypeVariable, WTypeVariable, emptyWCs}
class UnifyTest extends munit.FunSuite {
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)))
}
test("Unify should fail") {
val start: ConstraintSet = ConstraintSet()
start.add(LessDot(TypeVariable("a"), RefType(emptyWCs(), "String", List())))
start.add(LessDot(TypeVariable("a"), RefType(emptyWCs(), "Object", List())))
val result = new Unify().unifyIterative(start, standardFC())
assert(result.isEmpty)
}
test("Unify should pass example 1" ) {
val start: ConstraintSet = new ConstraintSet()
start.add(LessDot(TypeVariable("la"), RefType(emptyWCs(), "List", List(WTypeVariable("y")))))
start.add(LessDot(WTypeVariable("y"), TypeVariable("a")))
//start.add(LessDot(TypeVariable("lb"), TypeVariable("la")))
start.add(LessDot(TypeVariable("la"), RefType(emptyWCs(), "List", List(WTypeVariable("z")))))
start.add(LessDot(TypeVariable("a"), WTypeVariable("z")))
start.add(LessDot(WTypeVariable("y"), RefType(emptyWCs(), "Object", List())))
start.add(LessDot(WTypeVariable("z"), RefType(emptyWCs(), "Object", List())))
val result = new Unify().unifyIterative(start, standardFC())
assert(result.nonEmpty)
}
}