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

Add Trim and Adopt rules

Browse Source
This commit is contained in:
JanUlrich 2024-03-20 16:05:30 +01:00
parent 255397f6d6
commit 5625583309
1 changed files with 35 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -44,9 +44,9 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
case EqualsDot(left: Type, right: BotType) => throw RuntimeException("Bot type in =. constraint")
}
})
cs.getLessDotCons.foreach(cons => cons match {
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), cc) => // Upper
cs.remove(cons)
cs.add(LessDot(wildcardEnvironment.getUpperBound(left), right, cc))
case LessDot(left: (RefType | Wildcard), right: Wildcard, cc) => // Lower
@ -57,11 +57,11 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
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, _) =>
case LessDot(left: (RefType | Wildcard), right: BotType, _) => // TODO: insolvable constraint set!
case LessDot(left: TypePlaceholder, right: BotType, _) =>
cs.remove(cons)
cs.add(EqualsDot(left, right))
case LessDot(left : TypePlaceholder, right : TypePlaceholder, _) =>
case LessDot(left: TypePlaceholder, right: TypePlaceholder, _) =>
val circle = findCircle(cons.left.asInstanceOf[TypeVariable], cs.getALessDotBCons)
if (!circle.isEmpty) {
cs.removeAll(circle)
@ -69,23 +69,40 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
}
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 =>{
if(fc.isPossibleSupertype(cons.right.asInstanceOf[RefType].name, ic.right.asInstanceOf[RefType].name)){
matchRule(cons, ic, cs, tvFactory)
}else{
//TODO: insolvable constraint set!
}
//match rule:
alessdotc.find(ic => (ic != cons && cons.left.equals(cons.left))).map(ic => {
if (fc.isPossibleSupertype(cons.right.asInstanceOf[RefType].name, ic.right.asInstanceOf[RefType].name)) {
matchRule(cons, ic, cs, tvFactory)
} else {
//TODO: insolvable constraint set!
}
})
//adopt rule:
cs.getALessDotBCons.find(_.right == left).map(blessa => {
cs.getALessDotCCons.find(_.left == blessa.left).map(blessN => {
cs.add(LessDot(blessN.left, cons.right))
})
})
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, cc))
case LessDot(RefType(wcNull, n1, p1), RefType(wcs, n2, p2), cc) if wcNull.isEmpty & n1 == n2 & p1.size == p2.size =>
cs.add(LessDot(RefType(emptyWCs(), n, params), right))
case LessDot(RefType(wcNull, n1, p1), RefType(wcs, n2, p2), cc) =>
if (wcNull.isEmpty & n1 == n2 & p1.size == p2.size) {//Reduce
cs.remove(cons)
val freshTVMap: Map[Type, Type] = wcs.map(wcb => (Wildcard(wcb.name) -> tvFactory.freshWTV())).toMap
cs.addAll(p1.zip(p2.map(_.substitute(freshTVMap))).map(p => EqualsDot(p._1, p._2)))
cs.addAll(wcs.map(wcb => LessDot(Wildcard(wcb.name).substitute(freshTVMap), wcb.upper.substitute(freshTVMap))))
cs.addAll(wcs.map(wcb => LessDot(wcb.lower.substitute(freshTVMap), Wildcard(wcb.name).substitute(freshTVMap))))
} else if(fc.isPossibleSupertype(n1, n2)) { //Adapt
//TODO
} else {
// TODO: Insolvable Constraint set
}
case LessDot(RefType(wcs, n, params), right: Type, cc) if wcs.getWildcards().diff(params.flatMap(_.fvs()).toSet).nonEmpty => //Trim
cs.remove(cons)
val freshTVMap: Map[Type,Type] = wcs.map(wcb => (Wildcard(wcb.name) -> tvFactory.freshWTV())).toMap
cs.addAll(p1.zip(p2.map(_.substitute(freshTVMap))).map(p => EqualsDot(p._1, p._2)))
cs.addAll(wcs.map(wcb => LessDot(Wildcard(wcb.name).substitute(freshTVMap), wcb.upper.substitute(freshTVMap))))
cs.addAll(wcs.map(wcb => LessDot(wcb.lower.substitute(freshTVMap), Wildcard(wcb.name).substitute(freshTVMap))))
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))
})
}