chore: Naming conventions

tests/prolog/logic/VerificationTests.kt

@@ -0,0 +1,236 @@
+package prolog.logic
+
+import org.junit.jupiter.api.Assertions.assertFalse
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Test
+import prolog.Substitutions
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
+
+class VerificationTests {
+    @Test
+    fun unbound_variable_is_var() {
+        val variable = Variable("X")
+        assertTrue(variable(variable))
+    }
+
+    @Test
+    fun variable_bound_to_atom_is_not_var() {
+        val variable = Variable("X")
+
+        assertTrue(variable(variable))
+
+        val atom = Atom("a")
+
+        assertFalse(variable(variable, mapOf(variable to atom)))
+    }
+
+    @Test
+    fun variable_bound_to_compound_term_is_not_var() {
+        val variable = Variable("X")
+
+        assertTrue(variable(variable))
+
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+
+        assertFalse(variable(variable, mapOf(variable to structure)))
+    }
+
+    /**
+     * ?- X = X, var(X).
+     * true.
+     */
+    @Test
+    fun variable_bound_to_itself_is_var() {
+        val variable = Variable("X")
+        assertTrue(variable(variable, mapOf(variable to variable)))
+    }
+
+    /**
+     * ?- X = Y, var(X).
+     * X = Y.
+     */
+    @Test
+    fun variable_bound_to_another_variable_is_var() {
+        val variable1 = Variable("X")
+        val variable2 = Variable("Y")
+        assertTrue(variable(variable1, mapOf(variable1 to variable2)))
+    }
+
+    /**
+     * ?- Y = a, X = Y, var(X).
+     * false.
+     */
+    @Test
+    fun variable_bound_to_bound_variable_is_not_var() {
+        val variable1 = Variable("X")
+        val variable2 = Variable("Y")
+        val map: Substitutions = mapOf(
+            variable1 to variable2,
+            variable2 to Atom("a")
+        )
+        assertFalse(variable(variable1, map))
+    }
+
+    @Test
+    fun atom_is_not_var() {
+        val atom = Atom("a")
+        assertFalse(variable(atom))
+    }
+
+    @Test
+    fun compound_term_is_not_var() {
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+        assertFalse(variable(structure))
+    }
+
+    @Test
+    fun compound_term_with_var_is_not_var() {
+        val structure = Structure(Atom("a"), listOf(Variable("X")))
+        assertFalse(variable(structure))
+    }
+
+    @Test
+    fun unbound_variable_is_not_nonvar() {
+        val variable = Variable("X")
+        assertFalse(nonvariable(variable))
+    }
+
+    /**
+     * ?- A = a, nonvar(A).
+     * A = a.
+     */
+    @Test
+    fun variable_bound_to_atom_is_nonvar() {
+        val variable = Variable("X")
+
+        assertFalse(nonvariable(variable))
+
+        val atom = Atom("a")
+
+        assertTrue(nonvariable(variable, mapOf(variable to atom)))
+    }
+
+    /**
+     * ?- A = f(b), nonvar(A).
+     * A = f(b).
+     */
+    @Test
+    fun variable_bound_to_compound_term_is_nonvar() {
+        val variable = Variable("X")
+
+        assertFalse(nonvariable(variable))
+
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+
+        assertTrue(nonvariable(variable, mapOf(variable to structure)))
+    }
+
+    /**
+     * ?- X = X, nonvar(X).
+     * false.
+     */
+    @Test
+    fun variable_bound_to_itself_is_not_nonvar() {
+        val variable = Variable("X")
+        assertFalse(nonvariable(variable, mapOf(variable to variable)))
+    }
+
+    /**
+     * ?- X = Y, nonvar(X).
+     * false.
+     */
+    @Test
+    fun variable_bound_to_another_variable_is_not_nonvar() {
+        val variable1 = Variable("X")
+        val variable2 = Variable("Y")
+        assertFalse(nonvariable(variable1, mapOf(variable1 to variable2)))
+    }
+
+    @Test
+    fun atom_is_nonvar() {
+        val atom = Atom("a")
+        assertTrue(nonvariable(atom))
+    }
+
+    @Test
+    fun compound_term_is_nonvar() {
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+        assertTrue(nonvariable(structure))
+    }
+
+    @Test
+    fun compound_term_with_var_is_nonvar() {
+        val structure = Structure(Atom("a"), listOf(Variable("X")))
+        assertTrue(nonvariable(structure))
+    }
+
+    @Test
+    fun unbound_variable_is_not_compound() {
+        val variable = Variable("X")
+        assertFalse(compound(variable))
+    }
+
+    /**
+     * ?- A = a, compound(A).
+     * false.
+     */
+    @Test
+    fun bound_variable_to_atom_is_not_compound() {
+        val variable = Variable("X")
+        val atom = Atom("a")
+        assertFalse(compound(variable, mapOf(variable to atom)))
+    }
+
+    /**
+     * ?- A = f(b), compound(A).
+     * A = f(b).
+     */
+    @Test
+    fun bound_variable_to_compound_term_is_compound() {
+        val variable = Variable("X")
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+        assertTrue(compound(variable, mapOf(variable to structure)))
+    }
+
+    /**
+     * ?- Y = f(b), X = Y, compound(X).
+     * Y = X, X = f(b).
+     */
+    @Test
+    fun variable_bound_to_bound_variable_is_compound() {
+        val variable1 = Variable("X")
+        val variable2 = Variable("Y")
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+
+        val subs: Substitutions = mapOf(
+            variable1 to variable2,
+            variable2 to structure
+        )
+
+        assertTrue(compound(variable1, subs))
+    }
+
+    @Test
+    fun atom_is_not_compound() {
+        val atom = Atom("a")
+        assertFalse(compound(atom))
+    }
+
+    @Test
+    fun compound_term_is_compound() {
+        val structure = Structure(Atom("a"), listOf(Atom("b")))
+        assertTrue(compound(structure))
+    }
+
+    /**
+     * ?- compound(a()).
+     * true.
+     */
+    @Test
+    fun compound_term_with_no_arguments_is_compound() {
+        val structure = Structure(Atom("a"), emptyList())
+        assertTrue(compound(structure))
+    }
+}