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

Add Equals rule

Browse Source
This commit is contained in:
JanUlrich 2024-02-08 17:20:22 +01:00
parent e299fd681a
commit 0664440695
2 changed files with 66 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4,58 +4,78 @@ import unify.model.{ExtendsRelations, LessDot}
import unify.model.*
object Rules:
def applyRules(cs: ConstraintSet, tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
class Rules(cs: ConstraintSet, wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
cs.getEqualsDotCons.foreach(cons => {
if (cons.left.equals(cons.right)) { //erase rule
cs.remove(cons)
return
}
/*
else if (cons.left.isInstanceOf[Wildcard] && cons.right.isInstanceOf[Wildcard]) {
normalizeRule(cons, cs)
return
}
else if (cons.left.isInstanceOf[Wildcard] && !cons.right.isInstanceOf[WTypeVariable]) {
//Tame rule:
tameRule(cons, cs)
return
//Tame rule:
tameRule(cons, cs)
return
}else if(cons.left.isInstanceOf[RefType] && cons.right.isInstanceOf[RefType]){
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(_)
}
}else{
//TODO: insolvable constraint set!
}
}
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] &&
cs.fv(cons.left).isEmpty && cs.fv(cons.right).isEmpty) { // reduceEq rule
cs.remove(cons)
cs.add(LessDot(cons.left, cons.right))
cs.add(LessDot(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
}
*/
/*
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
}
*/
})
}
private def normalizeRule(cons: EqualsDot, cs: ConstraintSet): Unit = {
cs.remove(cons)
val left = cons.left.asInstanceOf[Wildcard]
val right = cons.right.asInstanceOf[Wildcard]
cs.add(EqualsDot(wildcardEnvironment.getLowerBound(left), wildcardEnvironment.getUpperBound(left)))
cs.add(EqualsDot(wildcardEnvironment.getLowerBound(right), wildcardEnvironment.getUpperBound(right)))
cs.add(EqualsDot(wildcardEnvironment.getLowerBound(left), wildcardEnvironment.getUpperBound(right)))
}
def tameRule(cons: EqualsDot, cs: ConstraintSet) = {
cs.remove(cons)
val left = cons.left.asInstanceOf[Wildcard]
val right = cons.right
cs.add(EqualsDot(wildcardEnvironment.getUpperBound(left), right))
cs.add(EqualsDot(wildcardEnvironment.getLowerBound(left), right))
}
def adaptRule(cons: LessDot, cs: ConstraintSet, fc: ExtendsRelations) = {
}

8
src/main/scala/unify/model/ConstraintSet.scala
View File

@ -17,4 +17,12 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
}
changed = true
}
def add(cons: LessDot): Unit = {
}
def add(cons: EqualsDot): Unit = {
}
}