Add Unifier interfaces and tests

Author: Virtlink

disjointmap/src/main/kotlin/net/pelsmaeker/unifiers/CyclicTermException.kt

@@ -0,0 +1,16 @@
+package net.pelsmaeker.unifiers
+
+/**
+ * An exception that is thrown when a cyclic term is detected during unification.
+ *
+ * @property term The term that caused the cyclic term exception.
+ * @property variable The variable that caused the cyclic term exception.
+ * @param message The message to include in the exception; or `null` to use the default message.
+ * @param cause The cause of the exception; or `null` if there is no cause.
+ */
+class CyclicTermException(
+    val term: Any,
+    val variable: Any,
+    message: String? = null,
+    cause: Throwable? = null,
+): Exception(message ?: "Occurs check failed for $term and $variable", cause)

disjointmap/src/main/kotlin/net/pelsmaeker/unifiers/MutableUnifier.kt

@@ -0,0 +1,46 @@
+package net.pelsmaeker.unifiers
+
+
+/**
+ * A mutable unifier.
+ */
+interface MutableUnifier<T, V: T>: Unifier<T, V> {
+
+    /**
+     * Changes this unifier to be the composition of this unifier with another unifier.
+     *
+     * @param other The other unifier to compose with.
+     * @return `true` if the composition was successful; otherwise, `false`.
+     * @throws CyclicTermException If the composition created a cyclic term.
+     */
+    fun composeWith(other: Unifier<T, V>): Boolean
+
+    /**
+     * Changes this unifier to include the given substitution.
+     *
+     * @param v The variable to add.
+     * @param term The term to add.
+     * @return `true` if the addition was successful; otherwise, `false`.
+     * @throws CyclicTermException If the addition created a cyclic term.
+     */
+    fun add(v: V, term: T): Boolean
+
+    /**
+     * Changes this unifier to include the given substitutions.
+     *
+     * @param map The map of substitutions to add.
+     * @return `true` if the additions were successful; otherwise, `false`.
+     * @throws CyclicTermException If the addition created a cyclic term.
+     */
+    fun addAll(map: Map<V, T>): Boolean
+
+    /**
+     * Changes this unifier such that the given terms are equal.
+     *
+     * @param term1 The first term to unify.
+     * @param term2 The second term to unify.
+     * @return `true` if the unification was successful; otherwise, `false`.
+     * @throws CyclicTermException If the unification created a cyclic term.
+     */
+    fun unify(term1: T, term2: T): Boolean
+}

disjointmap/src/main/kotlin/net/pelsmaeker/unifiers/PersistentUnifier.kt

@@ -0,0 +1,71 @@
+package net.pelsmaeker.unifiers
+
+
+/**
+ * A persistent unifier.
+ */
+interface PersistentUnifier<T, V: T>: Unifier<T, V> {
+
+    /**
+     * Returns a new unifier that is the composition of this unifier with another unifier.
+     *
+     * @param other The other unifier to compose with.
+     * @return The new unifier if the composition was successful; otherwise, `null`.
+     * @throws CyclicTermException If the composition created a cyclic term.
+     */
+    fun composeWith(other: Unifier<T, V>): PersistentUnifier<T, V>?
+            = mutate { composeWith(other) }
+
+    /**
+     * Returns a new unifier that includes the given substitution.
+     *
+     * @param v The variable to add.
+     * @param term The term to add.
+     * @return The new unifier if the addition was successful; otherwise, `null`.
+     * @throws CyclicTermException If the addition created a cyclic term.
+     */
+    fun add(v: V, term: T): PersistentUnifier<T, V>?
+            = mutate { add(v, term) }
+
+    /**
+     * Returns a new unifier that includes the given substitutions.
+     *
+     * @param map The map of substitutions to add.
+     * @return The new unifier if the additions were successful; otherwise, `null`.
+     * @throws CyclicTermException If the addition created a cyclic term.
+     */
+    fun addAll(map: Map<V, T>): PersistentUnifier<T, V>?
+            = mutate { addAll(map) }
+
+    /**
+     * Returns a new unifier such that the given terms are equal.
+     *
+     * @param term1 The first term to unify.
+     * @param term2 The second term to unify.
+     * @return The new unifier if the unification was successful; otherwise, `false`.
+     * @throws CyclicTermException If the unification created a cyclic term.
+     */
+    fun unify(term1: T, term2: T): Unifier<T, V>?
+            = mutate { unify(term1, term2) }
+
+    /**
+     * Obtain a builder with the same contents as this unifier.
+     *
+     * The builder can be used to efficiently perform multiple modification operations.
+     * Call the builder's [build] method to create a new unifier with the modifications.
+     *
+     * @return A new builder with the same contents as this unifier.
+     */
+    fun builder(): Builder<T, V>
+
+    /**
+     * A generic builder of a persistent unifier.
+     * The builder exposes its modification operations through the [MutableUnifier] interface.
+     *
+     * Builders are reusable, that is, its [build] method can be called multiple times with modifications
+     * between these calls. However, applied modifications do not affect previously built instances.
+     */
+    interface Builder<T, V: T>: MutableUnifier<T, V> {
+        fun build(): PersistentUnifier<T, V>?
+    }
+}

disjointmap/src/main/kotlin/net/pelsmaeker/unifiers/Unifier.kt

@@ -0,0 +1,113 @@
+package net.pelsmaeker.unifiers
+
+
+/**
+ * A unifier is the substitution that makes terms equal.
+ *
+ * @param T The type of terms.
+ * @param V The type of variables.
+ */
+interface Unifier<T, V: T> {
+
+//    /** The number of entries in this unifier. */
+//    val size: Int
+
+    /**
+     * Determines whether this unifier is empty.
+     *
+     * @return `true` when this unifier is empty; otherwise, `false`.
+     */
+    fun isEmpty(): Boolean
+
+    /**
+     * Determines whether this unifier is not empty.
+     *
+     * @return `true` when this unifier is not empty; otherwise, `false`.
+     */
+    fun isNotEmpty(): Boolean = !isEmpty()
+
+//    /** The entries of this unifier. */
+//    val entries: Map<V, T>
+
+    /**
+     * Find the representative variable for the given variable.
+     *
+     * @param v The variable to find the representative for.
+     * @return The representative variable; or `null` when the variable is not in the unifier.
+     */
+    fun find(v: V): V?
+
+    /**
+     * Find the representative term for the given term.
+     *
+     * @param term The term to find the representative for.
+     * @return The representative term if [term] is a term variable and occurs in this unifier;
+     * otherwise, [term] itself.
+     */
+    operator fun get(term: T): T
+
+    /**
+     * Determines whether the unifier contains the specified variable.
+     *
+     * @param v The variable to check.
+     * @return `true` when the unifier contains the specified variable;
+     * otherwise, `false`.
+     */
+    operator fun contains(v: V): Boolean = find(v) != null
+
+    /**
+     * Checks whether the given term is equal to another term.
+     *
+     * This method checks whether the two terms are equal after applying the unifier.
+     *
+     * @param term1 The first term to check.
+     * @param term2 The second term to check.
+     * @return `true` if the terms are equal after applying the unifier; otherwise, `false`.
+     */
+    fun same(term1: T, term2: T): Boolean
+
+    /**
+     * Recursively instantiate the given term using this unifier.
+     *
+     * This method replaces all variables in the term with their corresponding terms
+     * from the unifier.
+     *
+     * @param term The term to instantiate.
+     * @return The recursively instantiated term.
+     * @throws UnsupportedOperationException If the term is cyclic.
+     */
+    fun instantiate(term: T): T
+
+    /**
+     * Gets the set of free variables in the given term relative to this unifier.
+     *
+     * This method returns the set of variables that are not fully instantiated
+     * by this unifier.
+     *
+     * @param term The term to check.
+     * @return The set of variables in the term.
+     */
+    fun getFreeVars(term: T): Set<V>
+
+    /**
+     * Checks whether the given term is a ground term relative to this unifier.
+     *
+     * A ground term is a term that contains no variables.
+     *
+     * @param term The term to check.
+     * @return `true` if the term is a ground term; otherwise, `false`.
+     */
+    fun isGround(term: T): Boolean
+
+    /**
+     * Checks whether the given term is cyclic relative to this unifier.
+     *
+     * A cyclic term is a term that contains itself as a subterm.
+     *
+     * @param term The term to check.
+     * @return `true` if the term is cyclic; otherwise, `false`.
+     */
+    fun isCyclic(term: T): Boolean
+
+    // TODO: Add empty() unifier
+}

disjointmap/src/main/kotlin/net/pelsmaeker/unifiers/extensions.kt

@@ -0,0 +1,16 @@
+package net.pelsmaeker.unifiers
+
+
+/**
+ * Returns the result of applying the provided modifications on this unifier.
+ *
+ * The mutable unifier passed to the [mutator] closure has the same contents as this persistent unifier.
+ *
+ * @receiver The persistent unifier to mutate.
+ * @param mutator A function that mutates the unifier.
+ * @return A new persistent unifier with the provided modifications applied if the modifications were successful;
+ * otherwise this instance if no modifications were made in the result of this operation;
+ * otherwise, `null`.
+ */
+inline fun <T, V: T> PersistentUnifier<T, V>.mutate(mutator: (MutableUnifier<T, V>) -> Unit): PersistentUnifier<T, V>?
+        = builder().apply(mutator).build()