From f31f96addea6bb4e576d40cfce48941f56e96157 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Tue, 13 Feb 2024 22:24:52 +0100
Subject: [PATCH] WildcardEnvironment map. Add subst rule

---
 src/main/scala/unify/algorithm/Rules.scala    |  5 +++
 .../scala/unify/model/ConstraintSet.scala     | 42 ++++++++++++++++++-
 src/main/scala/unify/model/Type.scala         | 11 ++++-
 .../unify/model/WildcardEnvironment.scala     |  8 +++-
 4 files changed, 61 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala
index 1401132..68a5bf4 100644
--- a/src/main/scala/unify/algorithm/Rules.scala
+++ b/src/main/scala/unify/algorithm/Rules.scala
@@ -60,3 +60,8 @@ object Rules:
 
   }
 
+  def substRule(c: EqualsDot, cs: ConstraintSet): Unit = {
+    cs.remove(c)
+    cs.substitute(c.right, c.left)
+  }
+
diff --git a/src/main/scala/unify/model/ConstraintSet.scala b/src/main/scala/unify/model/ConstraintSet.scala
index fcaa86a..b820e57 100644
--- a/src/main/scala/unify/model/ConstraintSet.scala
+++ b/src/main/scala/unify/model/ConstraintSet.scala
@@ -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)
+  }
 }
diff --git a/src/main/scala/unify/model/Type.scala b/src/main/scala/unify/model/Type.scala
index e901af2..b4ffe86 100644
--- a/src/main/scala/unify/model/Type.scala
+++ b/src/main/scala/unify/model/Type.scala
@@ -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 + "?"
 }
\ No newline at end of file
diff --git a/src/main/scala/unify/model/WildcardEnvironment.scala b/src/main/scala/unify/model/WildcardEnvironment.scala
index 9b05c98..f9991da 100644
--- a/src/main/scala/unify/model/WildcardEnvironment.scala
+++ b/src/main/scala/unify/model/WildcardEnvironment.scala
@@ -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))
+  }
 }