+ unification w/o occurs-check example

tuProlog · May 7, 2020 · b59daf3 · b59daf3
1 parent 374937f
commit b59daf3
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 2 deletions.
diff --git a/examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/UnificationExample.kt b/examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/UnificationExample.kt
@@ -3,8 +3,6 @@ package it.unibo.tuprolog.examples.unify
 import it.unibo.tuprolog.core.*
 import it.unibo.tuprolog.unify.Unificator
 
-// TODO: with/without occurs-check
-
 fun main() {
     val unificator = Unificator.default
 

diff --git a/examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/UnificationOccursCheckExample.kt b/examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/UnificationOccursCheckExample.kt
@@ -0,0 +1,19 @@
+package it.unibo.tuprolog.examples.unify
+
+import it.unibo.tuprolog.core.Scope
+import it.unibo.tuprolog.dsl.unify.prolog
+import it.unibo.tuprolog.unify.Unificator
+
+fun main() {
+    prolog {
+        Scope.empty {
+            val term = "g"("X", "Y")
+            val otherTerm = "g"("f"("X"), "a")
+
+            val unificator = Unificator.default
+
+            val mgu = unificator.mgu(term, otherTerm, occurCheckEnabled = false)
+            println(mgu)    // {X_0=f(X_0), Y_1=a} => WRONG
+        }
+    }
+}