From 8d6c5add7e9cfc1d0150c94058ebdb1e8a944030 Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Mon, 19 Aug 2024 21:46:50 +0200
Subject: [PATCH] Introduce support for unbound variables within a Term;
 MPSCR-155

---
 .../mps/logic/reactor/core/Occurrence.kt      | 31 ++++++++++++-------
 .../reactor/core/internal/LogicalState.kt     |  4 ++-
 .../src/jetbrains/mps/unification/Term.java   | 11 +++++++
 3 files changed, 34 insertions(+), 12 deletions(-)

diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Occurrence.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Occurrence.kt
index 6d7c6d3d..5898b810 100644
--- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/Occurrence.kt
+++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/Occurrence.kt
@@ -17,12 +17,16 @@
 package jetbrains.mps.logic.reactor.core
 
 import jetbrains.mps.logic.reactor.core.internal.FeedbackStatus
+import jetbrains.mps.logic.reactor.core.internal.push
 import jetbrains.mps.logic.reactor.evaluation.ConstraintOccurrence
 
 import jetbrains.mps.logic.reactor.logical.Logical
 import jetbrains.mps.logic.reactor.logical.LogicalContext
 import jetbrains.mps.logic.reactor.program.Constraint
 import jetbrains.mps.logic.reactor.program.Rule
+import jetbrains.mps.logic.reactor.util.Id
+import jetbrains.mps.unification.Term
+import java.util.LinkedList
 
 
 /**
@@ -56,23 +60,28 @@ class Occurrence(val constraint: Constraint,
     override fun reactivate(controller: Controller) = doReactivate(controller)
 
     fun terminate(observable: LogicalStateObservable) {
-        for (a in arguments) {
-            if (a is Logical<*>) {
-                observable.removeReactivatable(a, this)
-            }
-        }
+        forEachUnboundLogical { observable.removeReactivatable(it, this) }
         alive = false
     }
 
     fun revive(observable: LogicalStateObservable) {
-        if (!alive) {
-            for (a in HashSet(arguments)) { // avoid duplicate subscriptions
-                if (a is Logical<*>) {
-                    observable.addReactivatable(a, this)
-                }
+        forEachUnboundLogical { observable.addReactivatable(it, this) }
+        alive = true
+    }
+
+    private fun forEachUnboundLogical(block: (Logical<*>) -> Unit) {
+        val logicals = hashSetOf<Id<Logical<*>>>()   // avoid duplicate subscriptions
+        // NB! Don't use "findRoot" for these are stored using an identity map
+        val queue = LinkedList(arguments)
+        while (queue.isNotEmpty()) {
+            val next = queue.removeFirst()
+            when (next) {
+                is Logical<*>   ->  if (next.isBound) queue.addLast(next.findRoot().value())
+                                    else logicals.add(Id(next))
+                is Term         ->  next.unboundLogicals().forEach { logicals.add(Id(it)) }
             }
         }
-        alive = true
+        logicals.forEach{ block(it.wrapped) }
     }
 
     private fun doReactivate(controller: Controller) {
diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt
index f3c00a37..3b2aa707 100644
--- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt
+++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/LogicalState.kt
@@ -50,7 +50,9 @@ class LogicalState : LogicalStateObservable, LogicalObserver
         if (!observers.containsKey(logical)) {
             logical.addObserver(this)
         }
-        observers.getOrPut(logical) { arrayListOf() }.add(reactivatable)
+        val list = observers.getOrPut(logical) { arrayListOf() }
+        // TODO this check may be inefficient, but it's necessary
+        if (!list.contains(reactivatable)) list.add(reactivatable)
     }
 
     override fun removeReactivatable(logical: Logical<*>, reactivatable: Reactivatable) {
diff --git a/reactor/Core/src/jetbrains/mps/unification/Term.java b/reactor/Core/src/jetbrains/mps/unification/Term.java
index 7cfd6eb6..c27bc194 100644
--- a/reactor/Core/src/jetbrains/mps/unification/Term.java
+++ b/reactor/Core/src/jetbrains/mps/unification/Term.java
@@ -16,9 +16,12 @@
 
 package jetbrains.mps.unification;
 
+import jetbrains.mps.logic.reactor.logical.Logical;
+import jetbrains.mps.logic.reactor.logical.LogicalOwner;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.Collection;
+import java.util.Collections;
 
 /**
  * Represents a node in a term graph. The graph may contain cycles. A node in a term
@@ -45,6 +48,14 @@ public interface Term extends Comparable<Term> {
      */
     Collection<? extends Term> arguments();
 
+    /**
+     * A collection of all instances of {@link jetbrains.mps.logic.reactor.logical.Logical}
+     * within this term that have not been assigned a value.
+     */
+    default Collection<Logical<?>> unboundLogicals() {
+        return Collections.emptyList();
+    }
+
     /**
      * For a reference term, returns the term this term is referring to.
      * For function and variable terms return this term.