From 06644406958183e6b0161009bf23810ae168a571 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Thu, 8 Feb 2024 17:20:22 +0100
Subject: [PATCH] Add Equals rule

---
 src/main/scala/unify/algorithm/Rules.scala    | 96 +++++++++++--------
 .../scala/unify/model/ConstraintSet.scala     |  8 ++
 2 files changed, 66 insertions(+), 38 deletions(-)

diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala
index 1401132..91c8e87 100644
--- a/src/main/scala/unify/algorithm/Rules.scala
+++ b/src/main/scala/unify/algorithm/Rules.scala
@@ -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) = {
 
   }
diff --git a/src/main/scala/unify/model/ConstraintSet.scala b/src/main/scala/unify/model/ConstraintSet.scala
index fcaa86a..114e070 100644
--- a/src/main/scala/unify/model/ConstraintSet.scala
+++ b/src/main/scala/unify/model/ConstraintSet.scala
@@ -17,4 +17,12 @@ class ConstraintSet( private var unifier: Set[EqualsDot] = Set(),
     }
     changed = true
   }
+
+  def add(cons: LessDot): Unit = {
+
+  }
+
+  def add(cons: EqualsDot): Unit = {
+
+  }
 }