From 93af1d12f68c7b2b4e434a0f204ae0c1d75d5138 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Sat, 16 Apr 2022 15:44:59 +0200
Subject: [PATCH] add subElimRule

---
 src/main/scala/hb/dhbw/Unify.scala | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index ede9ef8..9796afd 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -37,13 +37,22 @@ object Unify {
 
   def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
     var ret = eq
-    val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{
+    var ruleResult = subElimRule(ret)
+    while(ruleResult.isDefined){
+      ret = ruleResult.get
+      ruleResult = subElimRule(ruleResult.get)
+    }
+    ret
+  }
+
+  def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = {
+    var ret = eq
+    eq.find(_ match{
       case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
       case _ => false
+    }).map(it => {
+      subst(it.left.asInstanceOf[UnifyTV], it.right, ret) ++ Set(UnifyEqualsDot(it.right, it.left))
     })
-    ret = ret.filter(it => !alessdotb.contains(it))
-    alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
-    ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)})
   }
 
   def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {