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

add Crunch rule

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-20 16:51:48 +01:00
parent 5625583309
commit 7df80a1c18
2 changed files with 16 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10,6 +10,11 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
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)))))
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) {
@ -86,15 +91,19 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
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))
case LessDot(RefType(wcNull, n1, p1), RefType(wcs, n2, p2), cc) =>
if (wcNull.isEmpty & n1 == n2 & p1.size == p2.size) {//Reduce
case LessDot(RefType(wc1, n1, p1), RefType(wc2, n2, p2), cc) =>
if (wc1.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
val freshTVMap: Map[Type, Type] = wc2.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))))
cs.addAll(wc2.map(wcb => LessDot(Wildcard(wcb.name).substitute(freshTVMap), wcb.upper.substitute(freshTVMap))))
cs.addAll(wc2.map(wcb => LessDot(wcb.lower.substitute(freshTVMap), Wildcard(wcb.name).substitute(freshTVMap))))
} else if(fc.isPossibleSupertype(n1, n2)) { //Adapt
//TODO
val subtypeRelation = fc.supertype(n1) // C<X> <. D<N>
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)))
} else {
// TODO: Insolvable Constraint set
}

1
src/main/scala/unify/model/WildcardEnvironment.scala
View File

@ -2,6 +2,7 @@ package unify.model
case class WildcardBound(name: String, upper: Type, lower: Type){}
class WildcardEnvironment(wcBounds: Set[WildcardBound]) {
def getWCBounds = bounds.map(b => WildcardBound(b._1, b._2._1, b._2._2)).toSet
val bounds: Map[String, (Type, Type)] = wcBounds.map(b => (b.name -> (b.upper, b.lower))).toMap
def isEmpty = wcBounds.isEmpty