WildcardEnvironment map. Add subst rule

This commit is contained in:
Andreas Stadelmeier 2024-02-13 22:24:52 +01:00
parent e299fd681a
commit f31f96adde
4 changed files with 61 additions and 5 deletions

View File

@ -60,3 +60,8 @@ object Rules:
}
def substRule(c: EqualsDot, cs: ConstraintSet): Unit = {
cs.remove(c)
cs.substitute(c.right, c.left)
}

View File

@ -4,10 +4,11 @@ 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 lessdotCC : List[LessDot] = List(),
private var lessdotCC : List[LessDotCC] = List(),
private var changed: Boolean = false) {
def getEqualsDotCons = equalsdot
def getLessDotCons: Set[LessDot] = lessdot
def remove(cons: Constraint): Unit = {
cons match {
@ -17,4 +18,43 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
}
changed = true
}
def add(cons: Constraint): Unit = {
cons match {
case EqualsDot(l, r) => equalsdot += (EqualsDot(l, r))
case LessDot(l, r) => lessdot += (LessDot(l, r))
case LessDotCC(l, r) => lessdotCC = LessDotCC(l,r) :: lessdotCC
}
changed = true
}
def substitute(withType: Type, toSubstitute: Type): Unit = {
def substituteWCB(wcb: WildcardBound) =
WildcardBound(wcb.name, substitute(wcb.upper), substitute(wcb.upper))
def substitute(inType: Type): Type = if (inType.equals(toSubstitute)) {
withType
} else {
inType match {
case RefType(wildcards, name, params) =>
RefType(
wildcards.map(substituteWCB), name, params.map(substitute))
case t => t
}
}
getEqualsDotCons.foreach(c => {
val subst = EqualsDot(substitute(c.left), substitute(c.right))
if (!c.equals(subst)) {
remove(c)
add(subst)
}
})
lessdot = getLessDotCons.map(c => {
LessDot(substitute(c.left), substitute(c.right))
})
unifier = unifier.map(c => {
EqualsDot(substitute(c.left), substitute(c.right))
})
this.bounds = this.bounds.map(substituteWCB)
}
}

View File

@ -6,6 +6,11 @@ sealed abstract class Type:
case RefType(wildcards, name, params) => params.flatMap(tvs).toSet
case _ => Set()
}
def wtvs(t: Type): Set[WTypeVariable] = t match {
case WTypeVariable(a) => Set(WTypeVariable(a))
case RefType(wildcards, name, params) => params.flatMap(wtvs).toSet
case _ => Set()
}
final case class RefType(wildcards: WildcardEnvironment, name: String, params: List[Type]) extends Type{
override def toString: String = {
@ -18,12 +23,14 @@ final case class RefType(wildcards: WildcardEnvironment, name: String, params: L
}
final case class BotType() extends Type {}
final case class TypeVariable(name: String) extends Type{
sealed abstract class TypePlaceholder(name: String) extends Type
final case class TypeVariable(name: String) extends TypePlaceholder(name){
override def toString: String = name
}
final case class Wildcard(name: String) extends Type {
override def toString: String = name // + "^" + upperBound.toString + "_" + lowerBound.toString
}
final case class WTypeVariable(name: String) extends Type {
final case class WTypeVariable(name: String) extends TypePlaceholder(name) {
override def toString: String = name + "?"
}

View File

@ -1,7 +1,7 @@
package unify.model
case class WildcardBounds(name: String, upper: Type, lower: Type){}
class WildcardEnvironment(wcBounds: Set[WildcardBounds]) {
case class WildcardBound(name: String, upper: Type, lower: Type){}
class WildcardEnvironment(wcBounds: Set[WildcardBound]) {
val bounds: Map[String, (Type, Type)] = wcBounds.map(b => (b.name -> (b.upper, b.lower))).toMap
def getUpperBound(wc: Wildcard): Type = bounds(wc.name)._1
@ -9,4 +9,8 @@ class WildcardEnvironment(wcBounds: Set[WildcardBounds]) {
def getLowerBound(wc: Wildcard): Type = bounds(wc.name)._2
override def toString: String = bounds.map(_._1).mkString("", ",", ".")
def map(f : WildcardBound => WildcardBound): WildcardEnvironment = {
WildcardEnvironment(wcBounds.map(f))
}
}