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

Exchange if-else with match-case

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-14 19:19:33 +01:00
parent 0181ab942a
commit 1b3f3f4b8c
1 changed files with 46 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4,78 +4,59 @@ import unify.model.{ExtendsRelations, LessDot}
import unify.model.*
class Rules(cs: ConstraintSet, wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
class Rules(cs: ConstraintSet, deltaIn: WildcardEnvironment, wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
cons match { //TODO:
case EqualsDot(t: Type, WTypeVariable(a)) => {}
}
if (cons.left.equals(cons.right)) { //erase rule
cs.remove(cons)
} else if(cons.left.isInstanceOf[TypeVariable] && cons.right.wtvs().isEmpty){ //Subst rule
val left = cons.left.asInstanceOf[TypeVariable]
if(!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty){
cons match {
case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
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) {
cs.remove(cons)
cs.substitute(cons.right, cons.left)
cs.addUnifier(cons)
} else {
// TODO: insolvable
}
}else{ //Remove
cons.right.wtvs().foreach(wtv => cs.substitute(tvFactory.freshTV(), wtv))
}
case EqualsDot(WTypeVariable(a), right) => //Subst-WC
cs.remove(cons)
cs.substitute(cons.right, cons.left)
cs.addUnifier(cons)
}else{
// TODO: insolvable
}
} else if(cons.left.isInstanceOf[TypeVariable] && !cons.right.wtvs().isEmpty) { //Remove rule
cons.right.wtvs().foreach(wtv => cs.substitute(tvFactory.freshTV(), wtv))
} else if(cons.left.isInstanceOf[WTypeVariable]){ // Subst-WC rule
cs.remove(cons)
cs.substitute(cons.right, cons.left)
} else if (cons.left.isInstanceOf[Wildcard] && !cons.right.isInstanceOf[WTypeVariable]) { //Tame rule:
tameRule(cons, cs)
}else if(cons.left.isInstanceOf[RefType] && cons.right.isInstanceOf[RefType]){ //equals rule
val left = cons.left.asInstanceOf[RefType]
val right = cons.right.asInstanceOf[RefType]
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(_)
case EqualsDot(Wildcard(w), right: RefType) => tameRule(cons, cs)
case EqualsDot(Wildcard(w), right: Wildcard) => tameRule(cons, cs)
case EqualsDot(Wildcard(w), right: TypeVariable) => tameRule(cons, cs)
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(_)
}
} else {
//TODO: insolvable constraint set!
}
}else{
//TODO: insolvable constraint set!
}
} else if(cons.right.isInstanceOf[Wildcard]) { //swap
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
} else if(cons.right.isInstanceOf[WTypeVariable]) { //swap
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
} else if(cons.right.isInstanceOf[TypeVariable]) {
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
case EqualsDot(left: (RefType|TypeVariable), right: Wildcard) => swap(cons)
case EqualsDot(left: Type, right: WTypeVariable) => swap(cons)
case EqualsDot(left: RefType, right: TypeVariable) => swap(cons)
case EqualsDot(left: BotType, right: Type) => throw RuntimeException("Bot type in =. constraint")
case EqualsDot(left: Type, right: BotType) => throw RuntimeException("Bot type in =. constraint")
}
/*
else if (cons.left.isInstanceOf[RefType] && cons.right.isInstanceOf[Wildcard]) {
//Swap rule:
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
return
}
else if (!cons.left.isInstanceOf[TypeVariable] && cons.right.isInstanceOf[TypeVariable]) {
//swap rule:
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
return
}
else if ((cons.left.isInstanceOf[RefType] || cons.left.isInstanceOf[Wildcard]) && cons.right.isInstanceOf[WTypeVariable]) {
//swap rule:
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
return
}
else if (cons.left.isInstanceOf[RefType] && cons.right.isInstanceOf[RefType]
&& cons.left.asInstanceOf[RefType].name.equals(cons.right.asInstanceOf[RefType].name)
&& cons.left.asInstanceOf[RefType].wildcards.equals(cons.right.asInstanceOf[RefType].wildcards)) {
reduceEqRule(cons, cs, tvFactory)
return
}
*/
})
cs.getLessDotCons.foreach(cons => cons match {
case LessDot(left: Wildcard, right: (RefType|TypeVariable|Wildcard)) =>
cs.remove(cons)
cs.add(LessDot(wildcardEnvironment.getUpperBound(left), right))
case LessDot(left: (RefType|TypeVariable|Wildcard), right: Wildcard) if !deltaIn.getWildcards().contains(right) =>
cs.remove(cons)
cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
})
}
def swap(cons: EqualsDot) = {
cs.remove(cons)
cs.add(EqualsDot(cons.right, cons.left))
}
def tameRule(cons: EqualsDot, cs: ConstraintSet) = {