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

Fixes and add Same rule

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-08-10 10:13:34 +02:00
parent 990dbdf21c
commit e71e5001fe
2 changed files with 21 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -26,11 +26,13 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
do ()
cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
cons match {
case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
//Erase
case EqualsDot(a, b) if a == b => cs.remove(cons)
//Crunch
case EqualsDot(left: TypeVariable, RefType(wcs, n, params)) if wcs.getWCBounds.filter(wcb => wcb.upper == wcb.lower).nonEmpty =>
cs.remove(cons)
cs.add(EqualsDot(left, crunch(RefType(wcs, n, params))))
case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Remove
case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Exclude
if (right.wtvs().isEmpty) { //Subst
if (!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty && cs.notProcessed(left)) {
cs.remove(cons)
@ -39,7 +41,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
} else {
// TODO: insolvable
}
}else{ //Remove
}else{ //Exclude
cons.right.wtvs().foreach(wtv => cs.substitute(tvFactory.freshTV(), wtv))
}
case EqualsDot(WTypeVariable(a), right) => //Subst-WC

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

@ -48,11 +48,13 @@ class Unify {
}).map(cons => cons match {
case LessDot(RefType(w, n, p), TypeVariable(a), _) =>
//Same rule
//TODO
val cs1 : ConstraintSet = cs.copy()
cs1.remove(cons)
cs1.add(EqualsDot(TypeVariable(a), RefType(w,n,p)))
ret.add(cs1)
//General rule
val cs3: ConstraintSet = cs.copy()
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))
@ -75,7 +77,18 @@ class Unify {
ret.add(cs4)
}
case LessDot(RefType(w, n, p), WTypeVariable(a), _) => {
//TODO: SameW
//Same rule
val cs1 : ConstraintSet = cs.copy()
cs1.remove(cons)
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!
}
case _ => {}
})