From df1750fee6d011f7f7baa67bc56a9a21f46b5284 Mon Sep 17 00:00:00 2001
From: Grigorii Kirgizov <grigorii.kirgizov@jetbrains.com>
Date: Fri, 6 Mar 2020 13:54:21 +0300
Subject: [PATCH] Add tests for unification of terms with var refs

---
 .../mps/unification/test/SolverTests.java     | 60 +++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
index 01d4b750..58f68646 100644
--- a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
+++ b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
@@ -319,6 +319,12 @@ public class SolverTests {
 
                 bind(var("X"), var("Y"))
         );
+        assertUnifiesWithBindings(
+                MockTermsParser.parseTerm("f{^X}"),
+                MockTermsParser.parseTerm("f{ Y}"),
+
+                bind(var("X"), var("Y"))
+        );
         assertUnifiesWithBindings(
                 MockTermsParser.parseTerm("a{b ^X}"),
                 MockTermsParser.parseTerm("a{b c{d}}"),
@@ -568,6 +574,60 @@ public class SolverTests {
         );
     }
 
+    @Test
+    public void testFailCyclicVarRef() throws Exception {
+//        assertUnificationFails(
+//                MockTermsParser.parseTerm("X"),
+//                MockTermsParser.parseTerm("f{^X}"),
+//
+//                CYCLE_DETECTED
+//        );
+//        assertUnificationFails(
+//                MockTermsParser.parseTerm("f{X}"),
+//                MockTermsParser.parseTerm("f{f{^X}}"),
+//
+//                CYCLE_DETECTED
+//        );
+//        assertUnificationFails(
+//                MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"),
+//                MockTermsParser.parseTerm("t {   f{X} X    }"),
+//
+//                CYCLE_DETECTED
+//        );
+//        assertUnificationFails(
+//                MockTermsParser.parseTerm("t { f{^X} X     }"),
+//                MockTermsParser.parseTerm("t { Y     g{^Y} }"),
+//
+//                CYCLE_DETECTED
+//        );
+
+        // pass
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t { ^X Y    }"),
+                MockTermsParser.parseTerm("t {  Y f{X} }"),
+
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t { X     Y }"),
+                MockTermsParser.parseTerm("t { f{Y} ^X }"),
+
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t { ^X    Y }"),
+                MockTermsParser.parseTerm("t { f{Y} ^X }"),
+
+                CYCLE_DETECTED
+        );
+        // fixme: infinitely cycles !!
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t { ^X ^Y    }"),
+                MockTermsParser.parseTerm("t {  Y f{X} }"),
+
+                CYCLE_DETECTED
+        );
+    }
 
     @Test
     public void joinedLogicals() throws Exception {