Work in Prograss. Added step2
This commit is contained in:
Andreas Stadelmeier
parent
ae933b05c1
commit
9bea1b1eeb
@ -1,17 +1,29 @@
|
||||
package unify.algorithm
|
||||
|
||||
import unify.model.{ExtendsRelations, LessDot}
|
||||
|
||||
import unify.model.{ConstraintSet, ExtendsRelations, LessDot}
|
||||
import unify.model.*
|
||||
|
||||
import java.lang.reflect.WildcardType
|
||||
|
||||
class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: WildcardEnvironment, fc: ExtendsRelations):
|
||||
class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFactory):
|
||||
private def eraseCircleRule() = {
|
||||
val alessb = cs.getALessDotBCons
|
||||
val circle = alessb.map(cons => findCircle(cons.left.asInstanceOf[TypeVariable], alessb)).find(!_.isEmpty)
|
||||
if (circle.isDefined) {
|
||||
cs.removeAll(circle.get)
|
||||
cs.addAll(circle.get.map(c => EqualsDot(c.left, c.right)))
|
||||
}
|
||||
}
|
||||
private def crunch(refType: RefType): RefType = {
|
||||
val newWcs = WildcardEnvironment(refType.wildcards.getWCBounds.filter(wcb => wcb.upper == wcb.lower))
|
||||
val map: Map[Type, Type] = refType.wildcards.getWCBounds.filter(wcb => wcb.upper == wcb.lower).map(wcb => (Wildcard(wcb.name) -> wcb.upper)).toMap
|
||||
RefType(newWcs, refType.name, refType.params.map(_.substitute(map)))
|
||||
}
|
||||
def applyRules(tvFactory: TypeVariableFactory, fc: ExtendsRelations): Unit = {
|
||||
def applyRules() = {
|
||||
while
|
||||
eraseCircleRule()
|
||||
cs.hasChanged()
|
||||
do (cs.hasChanged())
|
||||
cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
|
||||
cons match {
|
||||
case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
|
||||
@ -33,9 +45,9 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
case EqualsDot(WTypeVariable(a), right) => //Subst-WC
|
||||
cs.remove(cons)
|
||||
cs.substitute(cons.right, cons.left)
|
||||
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(Wildcard(w), right: RefType) => tameRule(cons)
|
||||
case EqualsDot(Wildcard(w), right: Wildcard) => tameRule(cons)
|
||||
case EqualsDot(Wildcard(w), right: TypeVariable) => tameRule(cons)
|
||||
case EqualsDot(left: RefType, right: RefType) => // Equals rule
|
||||
if (left.params.size == right.params.size && left.name == right.name) {
|
||||
cs.remove(cons)
|
||||
@ -56,30 +68,33 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
case LessDot(a, b, _) if a == b => cs.remove(cons) //Erase
|
||||
case LessDot(left: Wildcard, right: (RefType | TypeVariable | Wildcard), cc) => // Upper
|
||||
cs.remove(cons)
|
||||
cs.add(LessDot(wildcardEnvironment.getUpperBound(left), right, cc))
|
||||
cs.add(LessDot(cs.wildcardEnv.getUpperBound(left), right, cc))
|
||||
case LessDot(left: (RefType | Wildcard), right: Wildcard, cc) => // Lower
|
||||
cs.remove(cons)
|
||||
cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
|
||||
case LessDot(left: TypeVariable, right: Wildcard, cc) if !deltaIn.contains(right) => // Lower
|
||||
cs.add(LessDot(left, cs.wildcardEnv.getLowerBound(right)))
|
||||
case LessDot(left: TypeVariable, right: Wildcard, cc) // if !deltaIn.contains(right)
|
||||
=> // Lower
|
||||
cs.remove(cons)
|
||||
cs.add(LessDot(left, wildcardEnvironment.getLowerBound(right)))
|
||||
cs.add(LessDot(left, cs.wildcardEnv.getLowerBound(right)))
|
||||
case LessDot(left: BotType, right: Type, _) => cs.remove(cons) //Bot
|
||||
case LessDot(left: (RefType | Wildcard), right: BotType, _) => // TODO: insolvable constraint set!
|
||||
case LessDot(left: TypePlaceholder, right: BotType, _) =>
|
||||
cs.remove(cons)
|
||||
cs.add(EqualsDot(left, right))
|
||||
/*
|
||||
case LessDot(left: TypePlaceholder, right: TypePlaceholder, _) =>
|
||||
val circle = findCircle(cons.left.asInstanceOf[TypeVariable], cs.getALessDotBCons)
|
||||
if (!circle.isEmpty) {
|
||||
cs.removeAll(circle)
|
||||
cs.addAll(circle.map(c => EqualsDot(c.left, c.right)))
|
||||
}
|
||||
*/
|
||||
case LessDot(left: TypePlaceholder, right: RefType, cc) =>
|
||||
val alessdotc = cs.getALessDotCCons
|
||||
//match rule:
|
||||
alessdotc.find(ic => (ic != cons && cons.left.equals(cons.left))).map(ic => {
|
||||
if (fc.isPossibleSupertype(cons.right.asInstanceOf[RefType].name, ic.right.asInstanceOf[RefType].name)) {
|
||||
matchRule(cons, ic, cs, tvFactory)
|
||||
matchRule(cons, ic)
|
||||
} else {
|
||||
//TODO: insolvable constraint set!
|
||||
}
|
||||
@ -87,6 +102,8 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
//adopt rule:
|
||||
cs.getALessDotBCons.find(_.right == left).map(blessa => {
|
||||
cs.getALessDotCCons.find(_.left == blessa.left).map(blessN => {
|
||||
//TODO: Check if adopt rule got already applied
|
||||
// different approach: Do the adopt and circle rule at the beginning of the algorithm. Then never again
|
||||
cs.add(LessDot(blessN.left, cons.right))
|
||||
})
|
||||
})
|
||||
@ -94,7 +111,7 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
cs.remove (cons)
|
||||
cs.add (LessDot (left, crunch (right), cc) )
|
||||
}
|
||||
case LessDot(RefType(wc, n, params), right: RefType, cc) if right.fvs().diff(deltaIn).isEmpty | cc > 0 => // Capture und Prepare
|
||||
case LessDot(RefType(wc, n, params), right: RefType, cc) if right.fvs().isEmpty | cc > 0 => // Capture und Prepare
|
||||
cs.remove(cons)
|
||||
cs.add(LessDot(RefType(emptyWCs(), n, params), right))
|
||||
case LessDot(RefType(wc1, n1, p1), RefType(wc2, n2, p2), cc) =>
|
||||
@ -126,7 +143,7 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
* @param c2 a <. D
|
||||
* It's important that C < D
|
||||
*/
|
||||
private def matchRule(c1: LessDot, c2: LessDot, cs: ConstraintSet, tvFactory: TypeVariableFactory) = {
|
||||
private def matchRule(c1: LessDot, c2: LessDot) = {
|
||||
cs.remove(c1)
|
||||
cs.remove(c2)
|
||||
|
||||
@ -173,18 +190,14 @@ class Rules(cs: ConstraintSet, deltaIn: Set[Wildcard], wildcardEnvironment: Wild
|
||||
cs.add(EqualsDot(cons.right, cons.left))
|
||||
}
|
||||
|
||||
def tameRule(cons: EqualsDot, cs: ConstraintSet) = {
|
||||
def tameRule(cons: EqualsDot) = {
|
||||
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))
|
||||
cs.add(EqualsDot(cs.wildcardEnv.getUpperBound(left), right))
|
||||
cs.add(EqualsDot(cs.wildcardEnv.getLowerBound(left), right))
|
||||
}
|
||||
def adaptRule(cons: LessDot, cs: ConstraintSet, fc: ExtendsRelations) = {
|
||||
|
||||
}
|
||||
|
||||
def substRule(c: EqualsDot, cs: ConstraintSet): Unit = {
|
||||
def substRule(c: EqualsDot): Unit = {
|
||||
cs.remove(c)
|
||||
cs.substitute(c.right, c.left)
|
||||
}
|
||||
|
||||
127
src/main/scala/unify/algorithm/Unify.scala
Normal file
127
src/main/scala/unify/algorithm/Unify.scala
Normal file
@ -0,0 +1,127 @@
|
||||
package unify.algorithm
|
||||
|
||||
import unify.model.{ConstraintSet, EqualsDot, ExtendsRelations, LessDot, RefType, TypeVariable, UnifySolution, Wildcard, WildcardBound, WildcardEnvironment, WildcardFactory, emptyWCs}
|
||||
|
||||
import java.util.concurrent.{CompletableFuture, ExecutorService, Future}
|
||||
import scala.collection.mutable
|
||||
|
||||
class Unify {
|
||||
|
||||
/**
|
||||
* The steps transforming the constraint set (including substitution)
|
||||
* but without branching into multiple constraint sets
|
||||
* @param cs
|
||||
* @param fc
|
||||
*/
|
||||
def step1(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFactory) = {
|
||||
val rules = new Rules(cs, fc, tvFactory)
|
||||
while
|
||||
rules.applyRules()
|
||||
cs.hasChanged()
|
||||
do ()
|
||||
}
|
||||
|
||||
def step3(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFactory) = {
|
||||
val ret: mutable.Set[ConstraintSet] = mutable.Set()
|
||||
cs.getLessDotCons.find(cons => cons match {
|
||||
case LessDot(RefType(w, n, p), TypeVariable(a), _) => true
|
||||
case _ => false
|
||||
}).map(cons => cons match {
|
||||
case LessDot(RefType(w, n, p), TypeVariable(a), _) => {
|
||||
//Same rule
|
||||
//TODO
|
||||
|
||||
//General rule
|
||||
val cs3: ConstraintSet = cs.copy()
|
||||
|
||||
val wcFactory = new WildcardFactory()
|
||||
val freshWCs = p.map(_ => WildcardBound(wcFactory.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))
|
||||
//cs3.addAll(freshWCs.map(w => LessDot(cs3.getLowerBound(w), cs3.getUpperBound(w))))
|
||||
//Set upper bound to Object: //TODO: take the real upper bound (therefore ExtendsRelations has to be changed)
|
||||
cs3.addAll(freshWCs.map(w => LessDot(w.upper, RefType(emptyWCs(), "Object", List.empty))))
|
||||
ret.add(cs3)
|
||||
|
||||
//Super rule
|
||||
//Object is the exception, which does not have a supertype
|
||||
if(!cons.left.asInstanceOf[RefType].name.equals("Object")){
|
||||
val cs4: ConstraintSet = cs.copy()
|
||||
cs4.remove(cons)
|
||||
val cType = cons.left.asInstanceOf[RefType]
|
||||
val paramMap = fc.supertype(cType.name)._1.params.zip(cType.params).toMap
|
||||
val superType = fc.supertype(cType.name)._2
|
||||
|
||||
val newSuperType = RefType(cType.wildcards, superType.name, superType.params.map(p => p.substitute(paramMap)))
|
||||
cs4.add(LessDot(newSuperType, cons.right))
|
||||
ret.add(cs4)
|
||||
}
|
||||
}
|
||||
|
||||
case _ => {}
|
||||
})
|
||||
cs.getALessDotCCons.map(cons => cons match {
|
||||
case LessDot(TypeVariable(a), RefType(wc, n, ps), _) => {
|
||||
cs.getALessDotBCons.find(c => c.left.equals(TypeVariable(a))).map(_.right).map(b => {
|
||||
//Lower rule:
|
||||
val csLower: ConstraintSet = cs.copy()
|
||||
csLower.remove(LessDot(TypeVariable(a), RefType(wc, n, ps)))
|
||||
csLower.add(LessDot(b, RefType(wc, n, ps)))
|
||||
ret.add(csLower)
|
||||
//Raise rule:
|
||||
val csRaise: ConstraintSet = cs.copy()
|
||||
csRaise.remove(LessDot(TypeVariable(a), b))
|
||||
csRaise.add(LessDot(RefType(wc, n, ps), b))
|
||||
ret.add(csRaise)
|
||||
})
|
||||
|
||||
}
|
||||
case _ => {}
|
||||
})
|
||||
/*
|
||||
cs.getALessDotCCons().filter(cons => !cs.fv(cons.right).isEmpty).map(cons => {
|
||||
//Force
|
||||
val csForce: ConstraintSet = cs.copy()
|
||||
val fvs = cs.fv(cons.right)
|
||||
if(fvs.find(t => !t.isInstanceOf[Wildcard]).isEmpty){
|
||||
val freeWildcards = fvs.map(_.asInstanceOf[Wildcard])
|
||||
val oldRight = cons.right.asInstanceOf[RefType]
|
||||
val newCons = freeWildcards.map(wc => LessDot(cs.getUpperBound(wc), cs.getLowerBound(wc))) ++ freeWildcards.map(wc => LessDot(cs.getLowerBound(wc), cs.getUpperBound(wc)))
|
||||
csForce.remove(cons)
|
||||
csForce.add(LessDot(cons.left, RefType(oldRight.wildcards ++ freeWildcards, oldRight.name, oldRight.params)))
|
||||
csForce.addAll(newCons)
|
||||
ret.add(csForce)
|
||||
}
|
||||
})
|
||||
*/
|
||||
ret.toSet
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns a constraintset in solved form on success
|
||||
* @param cs
|
||||
* @return
|
||||
*/
|
||||
def step4(cs: ConstraintSet): Option[UnifySolution] = {
|
||||
//Clean up step
|
||||
|
||||
//Ground rule
|
||||
val alessT = cs.getALessDotCCons.filter(c => cs.isOnlyLowerBound(c.left.asInstanceOf[TypeVariable]))
|
||||
if(alessT.size > 0) {
|
||||
alessT.map(cons => {
|
||||
cs.groundRule(cons)
|
||||
})
|
||||
}
|
||||
//SubElim rule
|
||||
cs.getALessDotBCons.map(cons => {
|
||||
cs.remove(cons)
|
||||
cs.substitute(cons.left, cons.right)
|
||||
cs.addUnifier(EqualsDot(cons.right, cons.left))
|
||||
})
|
||||
if(cs.isSolvedForm){
|
||||
cs.solvedForm()
|
||||
}else{
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -3,14 +3,25 @@ package unify.model
|
||||
class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
|
||||
private var lessdot: Set[LessDot] = Set(),
|
||||
private var equalsdot: Set[EqualsDot] = Set(),
|
||||
private var bounds: WildcardEnvironment,
|
||||
private var bounds: WildcardEnvironment = emptyWCs(),
|
||||
private var processed: Set[(TypePlaceholder, TypePlaceholder)] = Set(),
|
||||
private var changed: Boolean = false) {
|
||||
def notProcessed(a: TypePlaceholder, b: TypePlaceholder): Boolean = !processed.contains((a,b))
|
||||
|
||||
def setProcessedByAdopt(a: TypePlaceholder, b: TypePlaceholder): Unit = {
|
||||
processed = processed + ((a, b))
|
||||
}
|
||||
def wildcardEnv = bounds
|
||||
/*
|
||||
The Subtype-Constraints flagged as capture constraints are saved in lessdotCC.
|
||||
lessdotCC is a list. there can be multiple T <c S constraints. Removing one leaves the other one in the set.
|
||||
This is intentional
|
||||
*/
|
||||
def hasChanged(): Boolean = {
|
||||
val ret = changed
|
||||
changed = false
|
||||
ret
|
||||
}
|
||||
|
||||
def getEqualsDotCons = equalsdot
|
||||
|
||||
@ -69,5 +80,16 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
|
||||
EqualsDot(substitute(c.left), substitute(c.right))
|
||||
})
|
||||
this.bounds = WildcardEnvironment(this.bounds.map(substituteWCB))
|
||||
changed = true
|
||||
}
|
||||
|
||||
def copy(): ConstraintSet = {
|
||||
val ret = ConstraintSet()
|
||||
ret.processed = processed
|
||||
ret.lessdot = lessdot
|
||||
ret.equalsdot = equalsdot
|
||||
ret.unifier = unifier
|
||||
ret.bounds = new WildcardEnvironment(bounds.getWCBounds)
|
||||
ret
|
||||
}
|
||||
}
|
||||
|
||||
@ -6,8 +6,9 @@ class ExtendsRelations(val extendsRelations : Set[(RefType, RefType)]):
|
||||
|
||||
def isPossibleSupertype(of: String, superType: String): Boolean = {
|
||||
if (of.equals(superType)) return true
|
||||
extendsRelations.map(p => {
|
||||
//TODO
|
||||
})
|
||||
false
|
||||
if(extendsRelations.contains(of)){
|
||||
isPossibleSupertype(superType(of), superType)
|
||||
}else{
|
||||
false
|
||||
}
|
||||
}
|
||||
|
||||
10
src/main/scala/unify/model/UnifySolution.scala
Normal file
10
src/main/scala/unify/model/UnifySolution.scala
Normal file
@ -0,0 +1,10 @@
|
||||
package unify.model
|
||||
|
||||
class UnifySolution(delta: WildcardEnvironment, sigma: Map[TypeVariable, Type]) {
|
||||
def getDelta() = delta
|
||||
override def toString: String =
|
||||
"Δ = " + delta.map(wc => wc._1.name + ":["+wc._2._1.toString + ".."+wc._2._2.toString + "]").mkString("{",", ", "}") +
|
||||
", σ = " + sigma.toString()
|
||||
|
||||
def getSigma = sigma
|
||||
}
|
||||
@ -1,10 +1,13 @@
|
||||
package unify.model
|
||||
|
||||
import unify.algorithm.TypeVariableFactory
|
||||
|
||||
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 getWCBounds = bounds.map(b => WildcardBound(b._1, b._2._1, b._2._2)).toSet
|
||||
|
||||
def isEmpty = wcBounds.isEmpty
|
||||
|
||||
def getUpperBound(wc: Wildcard): Type = bounds(wc.name)._1
|
||||
|
||||
Loading…
Reference in New Issue
Block a user