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

Add Lessdot Crunch, finish normal transform rules

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-20 21:40:45 +01:00
parent 7df80a1c18
commit ae933b05c1
1 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -6,15 +6,18 @@ import unify.model.*
import java.lang.reflect.WildcardType
class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
private def crunch(refType: RefType): RefType = {
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)))
}
def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
cons match {
case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
case EqualsDot(left: TypeVariable, RefType(wcs, n, params)) if wcs.getWCBounds.filter(wcb => wcb.upper == wcb.lower).nonEmpty =>
cs.remove(cons)
val newWcs = WildcardEnvironment(wcs.getWCBounds.filter(wcb => wcb.upper == wcb.lower))
val map: Map[Type, Type] = wcs.getWCBounds.filter(wcb => wcb.upper == wcb.lower).map(wcb => (Wildcard(wcb.name) -> wcb.upper)).toMap
cs.add(EqualsDot(left, RefType(newWcs, n, params.map(_.substitute(map)))))
cs.add(EqualsDot(left, crunch(RefType(wcs, n, params))))
case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Remove
if (right.wtvs().isEmpty) { //Subst
if (!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty) {
@ -61,7 +64,6 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
cs.remove(cons)
cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
case LessDot(left: BotType, right: Type, _) => cs.remove(cons) //Bot
case LessDot(left, right: BotType, _) => // TODO: insolvable constraint set!
case LessDot(left: (RefType | Wildcard), right: BotType, _) => // TODO: insolvable constraint set!
case LessDot(left: TypePlaceholder, right: BotType, _) =>
cs.remove(cons)
@ -88,6 +90,10 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
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().diff(deltaIn).isEmpty | cc > 0 => // Capture und Prepare
cs.remove(cons)
cs.add(LessDot(RefType(emptyWCs(), n, params), right))