stan/FeatherweightTypeInference
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Unify, only call step 2 once. substitute beforehand

Browse Source
This commit is contained in:
JanUlrich 2022-03-22 22:56:46 +01:00
parent faef14cf05
commit c62a0e5dae
1 changed files with 47 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
src/main/scala/hb/dhbw/Unify.scala
View File

@ -57,22 +57,18 @@ object Unify {
def getNext[A](from: Set[CartesianProduct[A]])=
from.find(_.hasNext()).map(it => it.nextProduct())
var eqSets: Set[CartesianProduct[Set[UnifyConstraint]]] =
val eqSets: Set[CartesianProduct[Set[UnifyConstraint]]] =
Set(new CartesianProduct[Set[UnifyConstraint]](orCons))
var it: Option[Set[Set[UnifyConstraint]]] = getNext(eqSets)
var results: Set[Set[UnifyConstraint]] = Set()
while(it.isDefined){
val eqSet = it.get
val rulesResult = applyRules(fc)(eqSet.flatten)
val rulesResult = applyRules(fc, eqSet.flatten)
val step2Result = step2(rulesResult, fc)
while(step2Result.hasNext()){
val substResult = substStep(step2Result.nextProduct().flatten)
substResult match{
case UnchangedSet(eq) => if(isSolvedForm(eq)){
results = results + removeALessdotB(eq)
}
case ChangedSet(eq) =>
eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))
val substResult = step2Result.nextProduct().flatten
if(isSolvedForm(substResult)){
results = results + removeALessdotB(substResult)
}
}
it = getNext(eqSets)
@ -155,6 +151,10 @@ object Unify {
case UnifyLessDot(UnifyTV(_), UnifyRefType(_,_)) => true
case _ => false
}).asInstanceOf[Set[UnifyLessDot]]
private def getCUnifyLessDotA(from: Set[UnifyConstraint]) = from.filter(c => c match{
case UnifyLessDot(UnifyRefType(_, _), UnifyTV(_)) => true
case _ => false
}).asInstanceOf[Set[UnifyLessDot]]
def matchRule(eq : Set[UnifyConstraint], fc: FiniteClosure) = {
val aUnifyLessDotC = getAUnifyLessDotC(eq)
@ -168,6 +168,18 @@ object Unify {
}
)
}
def match2Rule(eq : Set[UnifyConstraint], fc: FiniteClosure) = {
val cUnifyLessDotA = getCUnifyLessDotA(eq) //C <. a
(eq -- cUnifyLessDotA) ++ cUnifyLessDotA.map(c => {
val smallerA = cUnifyLessDotA.find(c2 => c2 != c && c2.right.equals(c.right) && fc.isPossibleSupertype(c.left.asInstanceOf[UnifyRefType].name,c2.left.asInstanceOf[UnifyRefType].name))
if(smallerA.isEmpty){ //c2 = smallerA = D <. a C < D
c
}else{
UnifyLessDot(c.left, smallerA.get.left) // C <. D
}
}
)
}
def reduceRule(eq: Set[UnifyConstraint]) = eq.flatMap(c => c match {
case UnifyEqualsDot(UnifyRefType(an, ap), UnifyRefType(bn, bp)) => {
@ -208,7 +220,6 @@ object Unify {
case x => x
})
}
def adoptRule(eq: Set[UnifyConstraint], fc: FiniteClosure) ={
val aUnifyLessDota = eq.filter(c => c match{
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
@ -218,7 +229,7 @@ object Unify {
(eq -- aUnifyLessDotC) ++ aUnifyLessDotC.map(c => {
val smallerC = aUnifyLessDotC.find(c2 => c2 != c
&& isLinked(c2.left.asInstanceOf[UnifyTV], c.left.asInstanceOf[UnifyTV], aUnifyLessDota)
&& fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
&& fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
if(smallerC.isEmpty){
c
}else{
@ -227,6 +238,24 @@ object Unify {
}
)
}
def adopt2Rule(eq: Set[UnifyConstraint], fc: FiniteClosure) = {
val aUnifyLessDota = eq.filter(c => c match{
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
case _ => false
}).asInstanceOf[Set[UnifyLessDot]]
val cUnifyLessDotA = getCUnifyLessDotA(eq)
(eq -- cUnifyLessDotA) ++ cUnifyLessDotA.map(c => {
val smallerA = cUnifyLessDotA.find(c2 => c2 != c
&& isLinked(c2.right.asInstanceOf[UnifyTV], c.right.asInstanceOf[UnifyTV], aUnifyLessDota)
&& fc.isPossibleSupertype(c.left.asInstanceOf[UnifyRefType].name,c2.left.asInstanceOf[UnifyRefType].name))
if(smallerA.isEmpty){
c
}else{
UnifyLessDot(c.left, smallerA.get.left)
}
}
)
}
def eraseRule(eq: Set[UnifyConstraint]) =
eq.filter(_ match {
@ -350,14 +379,18 @@ object Unify {
private def doWhileSome(fun: Set[UnifyConstraint]=>Option[Set[UnifyConstraint]], eqTemp: Set[UnifyConstraint]): Set[UnifyConstraint] =
fun(eqTemp).map(eqTemp2 => doWhileSome(fun,eqTemp2)).getOrElse(eqTemp)
def applyRules(fc: FiniteClosure) = (eq: Set[UnifyConstraint]) => {
def applyRules(fc: FiniteClosure, eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
var eqNew: Set[UnifyConstraint] = null
var eqFinish: Set[UnifyConstraint] = eq
do{
eqNew = doWhileSome(Unify.equalsRule,eqFinish) //We have to apply equals rule first, to get rid of circles
eqFinish = eraseRule(swapRule(reduceRule(matchRule(adoptRule(adaptRule(eqNew, fc), fc), fc))))
eqFinish = eraseRule(swapRule(reduceRule(match2Rule(matchRule(adopt2Rule(adoptRule(adaptRule(eqNew, fc), fc), fc), fc), fc))))
}while(!eqNew.equals(eqFinish))
eqNew
val substResult = substStep(eqNew)
substResult match{
case UnchangedSet(_) => substResult.result
case ChangedSet(_) => applyRules(fc, substResult.result)
}
}
def cartesianProduct[T](xss: Set[Set[T]]): Set[Set[T]] =