Merge branch 'feature/examples' of gitlab.com:pika-lab/courses/as/pro…

…jects/sa-project-rizzato-1920 into feature/examples

examples/src/main/kotlin/it/unibo/tuprolog/examples/core/substitution/Application.kt

@@ -0,0 +1,19 @@
+package it.unibo.tuprolog.examples.core.substitution
+
+import it.unibo.tuprolog.core.*
+
+/**
+ *
+ *
+ * @author Lorenzo
+ */
+fun main() {
+    Scope.empty {
+        val term = structOf("father", varOf("X"), atomOf("isaac"))
+        val substitution = Substitution.Companion.of(varOf("X") to atomOf("abraham"))
+
+        val result = substitution.applyTo(term)
+
+        println(result)
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/core/substitution/Chain.kt

@@ -0,0 +1,23 @@
+package it.unibo.tuprolog.examples.core.substitution
+
+import it.unibo.tuprolog.core.Scope
+import it.unibo.tuprolog.core.Substitution
+
+/**
+ *
+ *
+ * @author Lorenzo
+ */
+fun main() {
+    Scope.empty {
+        val substitution = Substitution.of(
+                varOf("X") to varOf("Y"),
+                varOf("Y") to varOf("Z")
+        )
+
+        val originalZ = substitution.getOriginal(varOf("Z"))
+
+        println(substitution)
+        println(originalZ)
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/core/substitution/Composition.kt

@@ -0,0 +1,23 @@
+package it.unibo.tuprolog.examples.core.substitution
+
+import it.unibo.tuprolog.core.Scope
+import it.unibo.tuprolog.core.Substitution
+
+/**
+ *
+ *
+ * @author Lorenzo
+ */
+fun main() {
+    Scope.empty {
+        val term = structOf("father", varOf("X"), varOf("Y"))
+
+        val sub1 = Substitution.of(varOf("X"), atomOf("abraham"))
+        val sub2 = Substitution.of(varOf("Y"), atomOf("isaac"))
+
+        val substitution = sub1 + sub2
+
+        val result = substitution.applyTo(term)
+        println(result)
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/core/substitution/Contradiction.kt

@@ -0,0 +1,24 @@
+package it.unibo.tuprolog.examples.core.substitution
+
+import it.unibo.tuprolog.core.Scope
+import it.unibo.tuprolog.core.Substitution
+
+/**
+ *
+ *
+ * @author Lorenzo
+ */
+fun main() {
+    Scope.empty {
+        val term = structOf("father", varOf("X"), atomOf("isaac"))
+
+        val sub1 = Substitution.of(varOf("X"), atomOf("abraham"))
+        val sub2 = Substitution.of(varOf("X"), atomOf("nahor"))
+
+        val substitution = sub1 + sub2 // contradiction!
+        val result = substitution.applyTo(term) // father(X_0, isaac) (substitution could not be performed)
+
+        println(substitution)
+        println(result)
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/core/substitution/Creation.kt

@@ -0,0 +1,20 @@
+package it.unibo.tuprolog.examples.core.substitution
+
+import it.unibo.tuprolog.core.Scope
+import it.unibo.tuprolog.core.Substitution
+
+/**
+ *
+ *
+ * @author Lorenzo
+ */
+fun main() {
+    Scope.empty {
+        val substitution = Substitution.of(
+            varOf("X") to atomOf("abraham"),
+            varOf("Y") to atomOf("isaac")
+        )
+
+        println(substitution)
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/Caching.kt

@@ -0,0 +1,20 @@
+package it.unibo.tuprolog.examples.unify
+
+import it.unibo.tuprolog.core.*
+import it.unibo.tuprolog.unify.Unificator
+
+fun main() {
+    val unificator = Unificator.default
+    val cached = Unificator.cached(unificator, capacity = 5)
+
+    val term = Struct.of("father", Atom.of("abraham"), Atom.of("isaac"))
+    val template = Struct.of("father", Var.of("X"), Atom.of("isaac"))
+
+    val substitution: Substitution = cached.mgu(term, template)
+    val match: Boolean = cached.match(term, template)
+    val unified: Term? = cached.unify(term, template)
+
+    println(substitution) // {X_0=abraham}
+    println(match)        // true
+    println(unified)      // father(abraham, isaac)
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/Failure.kt

@@ -0,0 +1,23 @@
+package it.unibo.tuprolog.examples.unify
+
+import it.unibo.tuprolog.core.Atom
+import it.unibo.tuprolog.core.Struct
+import it.unibo.tuprolog.core.Substitution
+import it.unibo.tuprolog.core.Term
+import it.unibo.tuprolog.unify.Unificator
+
+fun main() {
+    val unificator = Unificator.default
+
+    val term = Struct.of("father", Atom.of("abraham"), Atom.of("isaac"))
+    val template = Struct.of("father", Atom.of("isaac"), Atom.of("abraham"))
+
+    val substitution: Substitution = unificator.mgu(term, template)
+    val match: Boolean = unificator.match(term, template)
+    val unified: Term? = unificator.unify(term, template)
+
+    println(substitution is Substitution.Fail)  // true
+    println(substitution.isFailed)              // true
+    println(match)                              // false
+    println(unified)                            // null
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/OccursCheck.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
+        }
+    }
+}

examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/UnificationExample.kt → examples/src/main/kotlin/it/unibo/tuprolog/examples/unify/Success.kt

@@ -1,20 +1,19 @@
 package it.unibo.tuprolog.examples.unify
 
-import it.unibo.tuprolog.core.Atom
-import it.unibo.tuprolog.core.Struct
-import it.unibo.tuprolog.core.Var
+import it.unibo.tuprolog.core.*
 import it.unibo.tuprolog.unify.Unificator
 
 fun main() {
     val unificator = Unificator.default
+
     val term = Struct.of("father", Atom.of("abraham"), Atom.of("isaac"))
     val template = Struct.of("father", Var.of("X"), Atom.of("isaac"))
 
-    val substitution = unificator.mgu(term, template)
-    val match = unificator.match(term, template)
-    val unified = unificator.unify(term, template)
+    val substitution: Substitution = unificator.mgu(term, template)
+    val match: Boolean = unificator.match(term, template)
+    val unified: Term? = unificator.unify(term, template)
 
     println(substitution) // {X_0=abraham}
     println(match)        // true
-    println(unified)  // father(abraham, isaac)
+    println(unified)      // father(abraham, isaac)
 }