From e71e5001fe508c3104084416e2a897d101534f79 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Sat, 10 Aug 2024 10:13:34 +0200
Subject: [PATCH] Fixes and add Same rule

---
 src/main/scala/unify/algorithm/Rules.scala |  8 +++++---
 src/main/scala/unify/algorithm/Unify.scala | 19 ++++++++++++++++---
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala
index d53c184..a0d5bca 100644
--- a/src/main/scala/unify/algorithm/Rules.scala
+++ b/src/main/scala/unify/algorithm/Rules.scala
@@ -26,11 +26,13 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
     do ()
     cs.getEqualsDotCons.foreach(cons => { //Hint: cannot be executed in parallel!
       cons match {
-        case EqualsDot(a, b) if a == b => cs.remove(cons) //Erase
+        //Erase
+        case EqualsDot(a, b) if a == b => cs.remove(cons)
+        //Crunch
         case EqualsDot(left: TypeVariable, RefType(wcs, n, params)) if wcs.getWCBounds.filter(wcb => wcb.upper == wcb.lower).nonEmpty =>
           cs.remove(cons)
           cs.add(EqualsDot(left, crunch(RefType(wcs, n, params))))
-        case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Remove
+        case EqualsDot(left: TypeVariable, right: (RefType|TypeVariable)) => //Subst and Exclude
           if (right.wtvs().isEmpty) { //Subst
             if (!cons.right.tvs().contains(left) && cons.right.fvs().isEmpty && cs.notProcessed(left)) {
               cs.remove(cons)
@@ -39,7 +41,7 @@ class Rules(cs: ConstraintSet, fc: ExtendsRelations, tvFactory: TypeVariableFact
             } else {
               // TODO: insolvable
             }
-          }else{ //Remove
+          }else{ //Exclude
             cons.right.wtvs().foreach(wtv => cs.substitute(tvFactory.freshTV(), wtv))
           }
         case EqualsDot(WTypeVariable(a), right) => //Subst-WC
diff --git a/src/main/scala/unify/algorithm/Unify.scala b/src/main/scala/unify/algorithm/Unify.scala
index f6e29d8..bdece42 100644
--- a/src/main/scala/unify/algorithm/Unify.scala
+++ b/src/main/scala/unify/algorithm/Unify.scala
@@ -48,11 +48,13 @@ class Unify {
       }).map(cons => cons match {
         case LessDot(RefType(w, n, p), TypeVariable(a), _) =>
           //Same rule
-          //TODO
+          val cs1 : ConstraintSet = cs.copy()
+          cs1.remove(cons)
+          cs1.add(EqualsDot(TypeVariable(a), RefType(w,n,p)))
+          ret.add(cs1)
 
           //General rule
           val cs3: ConstraintSet = cs.copy()
-
           val freshWCs = p.map(_ => WildcardBound(tvFactory.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))
@@ -75,7 +77,18 @@ class Unify {
             ret.add(cs4)
           }
         case LessDot(RefType(w, n, p), WTypeVariable(a), _) => {
-          //TODO: SameW
+          //Same rule
+          val cs1 : ConstraintSet = cs.copy()
+          cs1.remove(cons)
+          cs1.add(EqualsDot(WTypeVariable(a), RefType(w,n,p)))
+          ret.add(cs1)
+
+          val cs2 : ConstraintSet = cs.copy()
+          cs2.remove(cons)
+          //TODO:
+          // the fewer branches the better. should wildcard variables be ignored?
+          // constraints of the form T <. a? <. T' could be kept in the constraint set. Unify does not spawn type solutions for them anyway
+          // Process normal type placeholders first. then wildcard placeholders!
         }
         case _ => {}
       })