Implemented wildcards in unifications and disequality constraints (#17)

klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt

@@ -39,7 +39,7 @@ interface Constraint<out T : Constraint<T>> {
  * The standard operation that applies this constraint is [Term.ineq].
  */
 data class InequalityConstraint internal constructor(
-    private val simplifiedConstraints: List<SingleInequalityConstraint<*>>
+    internal val simplifiedConstraints: List<SingleInequalityConstraint<*>>
 ) : Constraint<InequalityConstraint> {
     override fun verify(substitution: Substitution): ConstraintVerificationResult<InequalityConstraint> {
         if (simplifiedConstraints.isEmpty()) {
@@ -55,7 +55,7 @@ data class InequalityConstraint internal constructor(
             }
 
             // Simplify this inequality constraint according to difference in substitutions
-            val simplifiedConstraints = delta.entries.map {
+            val simplifiedConstraints = delta.map {
                 SingleInequalityConstraint(it.key, it.value.cast())
             }
             val singleConstraint = InequalityConstraint(simplifiedConstraints)
@@ -73,33 +73,23 @@ data class InequalityConstraint internal constructor(
 
         val firstSingleConstraint = remainingSimplifiedConstraints.first()
 
-        return unify(firstSingleConstraint.variable, firstSingleConstraint.term.cast())
+        return unify(firstSingleConstraint.unboundedValue, firstSingleConstraint.term.cast())
             ?.verify(remainingSimplifiedConstraints.subList(1, remainingSimplifiedConstraints.size))
     }
 
     override fun toString(): String = simplifiedConstraints.joinToString(separator = ", ", prefix = "[", postfix = "]")
 
     companion object {
-        fun <T : Term<T>> of(variable: Var<T>, term: Term<T>): InequalityConstraint =
-            InequalityConstraint(listOf(SingleInequalityConstraint(variable, term)))
-
-        // This method does not check that variable type equals to type of corresponding term,
-        // as it has to be in SingleInequalityConstraint, so it should be used very carefully
-        private fun unsafeOf(vararg pairs: Pair<Var<out Term<*>>, Term<*>>): InequalityConstraint {
-            val singleInequalityConstraints = pairs.map {
-                SingleInequalityConstraint(it.first, it.second.cast())
-            }
-
-            return InequalityConstraint(singleInequalityConstraints)
-        }
+        fun <T : Term<T>> of(unboundedValue: UnboundedValue<T>, term: Term<T>): InequalityConstraint =
+            InequalityConstraint(listOf(SingleInequalityConstraint(unboundedValue, term)))
     }
 
 
     /**
-     * Represents a simple inequality constraint - [variable] cannot be equal to [term] of the same type.
+     * Represents a simple inequality constraint - [unboundedValue] cannot be equal to [term] of the same type.
      */
-    data class SingleInequalityConstraint<T : Term<T>>(val variable: Var<T>, val term: Term<T>) {
-        override fun toString(): String = "$variable !== $term"
+    data class SingleInequalityConstraint<T : Term<T>>(val unboundedValue: UnboundedValue<T>, val term: Term<T>) {
+        override fun toString(): String = "$unboundedValue !== $term"
     }
 }
 

klogic-core/src/main/kotlin/org/klogic/core/Context.kt

@@ -21,7 +21,7 @@ open class RelationalContext : AutoCloseable {
     val nilStream: RecursiveStream<Nothing> = NilStream()
 
     /**
-     * The index of the last variable created in this context.
+     * The index of the last [Var] created in this context.
      */
     private var lastCreatedVariableIndex: Int = 0
 
@@ -59,6 +59,12 @@ open class RelationalContext : AutoCloseable {
      */
     fun <T : Term<T>> freshTypedVar(): Var<T> = (lastCreatedVariableIndex++).createTypedVar()
 
+    /**
+     * Returns a new [Wildcard] according to the specified type.
+     */
+    @Suppress("UNCHECKED_CAST")
+    fun <T : Term<T>> wildcard(): Term<T> = Wildcard as T
+
     /**
      * Returns a result of invoking [run] overloading with goals for the fresh variable created using the passed [state].
      * NOTE: [goals] must not be empty.

klogic-core/src/main/kotlin/org/klogic/core/State.kt

@@ -16,7 +16,7 @@ data class State(
     val constraints: PersistentSet<Constraint<*>> = persistentHashSetOf(),
 ) {
     constructor(
-        map: Map<Var<*>, Term<*>>,
+        map: Map<UnboundedValue<*>, Term<*>>,
         constraints: PersistentSet<Constraint<*>>,
     ) : this(Substitution(map), constraints)
 

klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt

@@ -10,8 +10,8 @@ import org.klogic.unify.toUnificationState
  * Represents an immutable association of [Var]s with arbitrary types and bounded [Term]s with corresponding types.
  */
 @JvmInline
-value class Substitution(private val innerSubstitution: PersistentMap<Var<*>, Term<*>> = persistentHashMapOf()) {
-    constructor(map: Map<Var<*>, Term<*>>) : this(map.toPersistentHashMap())
+value class Substitution(private val innerSubstitution: PersistentMap<UnboundedValue<*>, Term<*>> = persistentHashMapOf()) {
+    constructor(map: Map<UnboundedValue<*>, Term<*>>) : this(map.toPersistentHashMap())
 
     /**
      * Checks whether [InequalityConstraint] for [left] and [right] of the same type can be satisfied.
@@ -27,16 +27,17 @@ value class Substitution(private val innerSubstitution: PersistentMap<Var<*>, Te
      */
     fun <T : Term<T>> ineq(left: Term<T>, right: Term<T>): ConstraintVerificationResult<InequalityConstraint> {
         return toUnificationState().unify(left, right)?.let { unificationState ->
-            val delta = unificationState.substitutionDifference
+            // Filter out wildcards as they add no information
+            val delta = unificationState.substitutionDifference.filterNot { it.key is Wildcard || it.value is Wildcard }
             // If the substitution from unification does not differ from the current substitution,
             // it means that this constraint is violated.
             if (delta.isEmpty()) {
                 return ViolatedConstraintResult
             }
 
             // Otherwise, this constraint can be satisfied, and we can simplify it according to calculated substitution delta.
-            val simplifiedConstraints = delta.entries.map {
-                InequalityConstraint.SingleInequalityConstraint(it.key, it.value.cast())
+            val simplifiedConstraints = delta.map {
+                InequalityConstraint.SingleInequalityConstraint(it.key as Var<*>, it.value.cast())
             }
             val singleConstraint = InequalityConstraint(simplifiedConstraints)
 
@@ -55,7 +56,7 @@ value class Substitution(private val innerSubstitution: PersistentMap<Var<*>, Te
 
     fun isEmpty(): Boolean = innerSubstitution.isEmpty()
 
-    operator fun plus(pair: Pair<Var<*>, Term<*>>): Substitution =
+    operator fun plus(pair: Pair<UnboundedValue<*>, Term<*>>): Substitution =
         (innerSubstitution.put(pair.first, pair.second)).toSubstitution()
 
     operator fun minus(other: Substitution): Substitution =
@@ -74,4 +75,4 @@ value class Substitution(private val innerSubstitution: PersistentMap<Var<*>, Te
     }
 }
 
-fun Map<Var<*>, Term<*>>.toSubstitution(): Substitution = Substitution(this)
+fun Map<UnboundedValue<*>, Term<*>>.toSubstitution(): Substitution = Substitution(this)

klogic-core/src/main/kotlin/org/klogic/core/Term.kt

@@ -120,11 +120,17 @@ sealed interface Term<T : Term<T>> {
     }
 }
 
+/**
+ * Represents a logic term of the specific type
+ * that does not have a particular value before unifications - either [Var] or [Wildcard].
+ */
+sealed interface UnboundedValue<T : Term<T>> : Term<T>
+
 /**
  * Represents a symbolic term with the specified term that can be equal to any other [Term] of the same type.
  */
 @JvmInline
-value class Var<T : Term<T>>(val index: Int) : Term<T> {
+value class Var<T : Term<T>> internal constructor(val index: Int) : UnboundedValue<T> {
     override fun <R : Term<R>> occurs(variable: Var<R>): Boolean = this == variable
 
     override fun walk(substitution: Substitution): Term<T> = substitution[this]?.let {
@@ -136,11 +142,11 @@ value class Var<T : Term<T>>(val index: Int) : Term<T> {
             return unificationState
         }
 
-        if (walkedOther !is Var<T> && walkedOther.occurs(this)) {
+        if (walkedOther is CustomTerm && walkedOther.occurs(this)) {
             return null
         }
 
-        val newAssociation = this to walkedOther
+        val newAssociation = if (walkedOther is Wildcard) walkedOther to this else this to walkedOther
         unificationState.substitutionDifference[newAssociation.first] = newAssociation.second
 
         return unificationState.copy(substitution = unificationState.substitution + newAssociation)
@@ -154,10 +160,39 @@ value class Var<T : Term<T>>(val index: Int) : Term<T> {
     override fun toString(): String = "_.$index"
 
     companion object {
+        /**
+         * Manually creates a variable with [this] index.
+         * WARNING: use it very carefully as this method does not care about [RelationalContext.lastCreatedVariableIndex].
+         */
         fun <T :Term<T>> Int.createTypedVar(): Var<T> = Var(this)
     }
 }
 
+/**
+ * Represents all logic values of the specific type (in consideration of [InequalityConstraint]s).
+ * For more information [take a look at the paper](https://danyaberezun.github.io/publications/assets/mk-2022-wild.pdf).
+ */
+object Wildcard : UnboundedValue<Nothing> {
+    override fun <R : Term<R>> occurs(variable: Var<R>): Boolean = false
+
+    override fun walk(substitution: Substitution): Wildcard = this
+
+    override fun unifyImpl(walkedOther: Term<Nothing>, unificationState: UnificationState): UnificationState? {
+        if (walkedOther is Wildcard) {
+            return unificationState
+        }
+
+        return walkedOther.unifyImpl(this, unificationState)
+    }
+
+    @Suppress("UNCHECKED_CAST")
+    override fun <R : Term<R>> cast(): Term<R> = this as Term<R>
+
+    override fun asReified(): Nothing = error("Wildcard $this cannot be reified")
+
+    override fun toString(): String = "__"
+}
+
 /**
  * Represents a custom (i.e., defined by user) term.
  */
@@ -188,6 +223,10 @@ interface CustomTerm<T : CustomTerm<T>> : Term<T> {
     }
 
     override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? {
+        if (walkedOther is Wildcard) {
+            return unificationState
+        }
+
         if (walkedOther !is CustomTerm) {
             // This branch means that walkedOther is Var
             return walkedOther.unifyImpl(this, unificationState)

klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt

@@ -1,9 +1,6 @@
 package org.klogic.unify
 
-import org.klogic.core.State
-import org.klogic.core.Substitution
-import org.klogic.core.Term
-import org.klogic.core.Var
+import org.klogic.core.*
 
 /**
  * Represents a mutable state of unification process.
@@ -13,7 +10,7 @@ import org.klogic.core.Var
  */
 data class UnificationState(
     val substitution: Substitution = Substitution.empty,
-    val substitutionDifference: MutableMap<Var<*>, Term<*>> = mutableMapOf()
+    val substitutionDifference: MutableMap<UnboundedValue<*>, Term<*>> = mutableMapOf()
 ) {
     /**
      * Tries to unify two terms of the same type [left] and [right] using [substitution].

klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt

@@ -58,10 +58,11 @@ class InequalityTest {
             val goal = x `!==` `1`
 
             val run = run(2, x, goal)
+            val answer = run.single()
 
             val expectedConstraints = setOf(InequalityConstraint.of(x, `1`))
-            assertEquals(x, run.singleReifiedTerm)
-            assertEquals(expectedConstraints, run.singleReifiedTermConstraints)
+            assertEquals(x, answer.term)
+            assertEquals(expectedConstraints, answer.constraints)
         }
     }
 
@@ -163,9 +164,10 @@ class InequalityTest {
             val goals = arrayOf(`3` `!==` `4`)
 
             val run = run(2, q, goals)
+            val answer = run.single()
 
-            assertTrue(run.singleReifiedTermConstraints.isEmpty())
-            assertEquals(q, run.singleReifiedTerm)
+            assertTrue(answer.constraints.isEmpty())
+            assertEquals(q, answer.term)
         }
     }