fix: Mib

src/interpreter/Preprocessor.kt

@@ -65,6 +65,7 @@ open class Preprocessor {
                     Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body)
                     Functor.of("atomic/1") -> AtomicOp(args[0])
                     Functor.of("compound/1") -> CompoundOp(args[0])
+                    Functor.of("=../2") -> Univ(args[0], args[1])
 
                     // Arithmetic
                     Functor.of("inf/0") -> Integer(Int.MAX_VALUE)

src/parser/grammars/TermsGrammar.kt

@@ -5,8 +5,11 @@ import com.github.h0tk3y.betterParse.grammar.parser
 import com.github.h0tk3y.betterParse.parser.Parser
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
+import prolog.ast.lists.List
 import prolog.ast.terms.*
 import prolog.builtins.Dynamic
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 
 /**
  * Precedence is based on the following table:
@@ -65,6 +68,7 @@ open class TermsGrammar : Tokens() {
     // Base terms (atoms, compounds, variables, numbers)
     protected val baseTerm: Parser<Term> by (dummy
             or (-leftParenthesis * parser(::term) * -rightParenthesis)
+            or parser(::list)
             or compound
             or atom
             or variable
@@ -87,7 +91,7 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
-    protected val op700: Parser<String> by (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
+    protected val op700: Parser<String> by (univOp or equivalent or notEquivalent or equals or notEquals or isOp) use { text }
     protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
         if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
     }
@@ -112,6 +116,20 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
+    // Lists
+    protected val list: Parser<List> by (-leftBracket * separated(
+        parser(::termNoConjunction),
+        comma,
+        acceptZero = true
+    ) * -rightBracket) use {
+        var list: List = Empty
+        // Construct the list in reverse order
+        for (term in this.terms.reversed()) {
+            list = Cons(term, list)
+        }
+        list
+    }
+
     // Term - highest level expression
     protected val term: Parser<Term> by term1200
     protected val termNoConjunction: Parser<Term> by term700

src/parser/grammars/Tokens.kt

@@ -10,6 +10,8 @@ import com.github.h0tk3y.betterParse.lexer.token
 abstract class Tokens : Grammar<Any>() {
     protected val leftParenthesis: Token by literalToken("(")
     protected val rightParenthesis: Token by literalToken(")")
+    protected val leftBracket: Token by literalToken("[")
+    protected val rightBracket: Token by literalToken("]")
     protected val exclamation: Token by literalToken("!")
     // 1200
     protected val neck by literalToken(":-")
@@ -20,6 +22,7 @@ abstract class Tokens : Grammar<Any>() {
     // 1000
     protected val comma: Token by literalToken(",")
     // 700
+    protected val univOp: Token by literalToken("=..")
     protected val notEquivalent: Token by literalToken("\\==")
     protected val equivalent: Token by literalToken("==")
     protected val equals: Token by literalToken("=")

src/prolog/ast/lists/List.kt

@@ -0,0 +1,57 @@
+package prolog.ast.lists
+
+import prolog.Substitutions
+import prolog.ast.terms.Term
+import prolog.ast.arithmetic.Integer
+
+sealed class List : Term {
+    abstract val head: Term
+    open val tail: List? = null
+    val size: Integer
+        get() = when (this) {
+            is Empty -> Integer(0)
+            is Cons -> Integer(1 + tail.size.value)
+        }
+
+    fun isEmpty(): Boolean = this is Empty
+
+    /**
+     * The empty list []
+     */
+    object Empty : List() {
+        override val head = this
+        override fun applySubstitution(subs: Substitutions): Empty = this
+        override fun toString(): String = "[]"
+    }
+
+    class Cons(override val head: Term, override var tail: List) : List() {
+        override fun applySubstitution(subs: Substitutions): List {
+            val newHead = head.applySubstitution(subs)
+            val newTail = tail.applySubstitution(subs) as List
+            return Cons(newHead, newTail)
+        }
+
+        override fun toString(): String {
+            val values = mutableListOf<Term>()
+            var current: List? = this
+            while (current != null && current !is Empty) {
+                values.add(current.head)
+                current = current.tail
+            }
+            return "[${values.joinToString(", ")}]"
+        }
+    }
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other == null) return false
+        if (other !is List) return false
+        if (this is Empty && other is Empty) return true
+        if (this is Cons && other is Cons) {
+            return this.head == other.head && this.tail == other.tail
+        }
+        return false
+    }
+
+    override fun hashCode(): Int = super.hashCode()
+}

src/prolog/ast/logic/Clause.kt

@@ -39,28 +39,26 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
                 // Filter the substitutions to only include those that map from head to goal
                 val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values }
                 val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
+                val headResult = headToGoalSubs.filterKeys { key ->
+                    goalToHeadSubs.any { occurs(key as Variable, it.value) }
+                }
                 val newSubs = headRenaming + headToGoalSubs
                 body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
                         onSuccess = { bodySubs ->
                             // If the body can be proven, yield the (combined) substitutions
-                            val goalToHeadResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
+                            val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
-                            val headResult = headToGoalSubs.filterKeys { key ->
+                            val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
-                                goalToHeadSubs.any {
+                            yield(Result.success(goalResult + headResult + bodyResult))
-                                    occurs(
-                                        key as Variable,
-                                        it.value
-                                    )
-                                }
-                            }
-                            yield(Result.success(goalToHeadResult + headResult))
                         },
                         onFailure = { error ->
                             if (error is AppliedCut) {
                                 // Find single solution and return immediately
                                 if (error.subs != null) {
-                                    var result = goalToHeadSubs.mapValues { applySubstitution(it.value, error.subs) }
+                                    val bodySubs = error.subs
-                                    yield(Result.failure(AppliedCut(result)))
+                                    val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
+                                    val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
+                                    yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult)))
                                 } else {
                                     yield(Result.failure(AppliedCut()))
                                 }

src/prolog/ast/terms/Atom.kt

@@ -11,7 +11,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 
-    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
+    override fun applySubstitution(subs: Substitutions): Atom = this
 
     override fun toString(): String {
         return name

src/prolog/builtins/analysisOperators.kt

@@ -7,6 +7,9 @@ import prolog.ast.arithmetic.Integer
 import prolog.ast.terms.*
 import prolog.ast.logic.Clause
 import prolog.logic.*
+import prolog.ast.lists.List
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 
 /**
  * [True] when [Term] is a term with [Functor] Name/Arity.
@@ -32,10 +35,11 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v
                     "Arguments are not sufficiently instantiated"
                 }
 
+                val t = applySubstitution(term, subs)
                 val name = applySubstitution(functorName, subs) as Atom
                 val arity = applySubstitution(functorArity, subs) as Integer
                 val result = Structure(name, List(arity.value) { AnonymousVariable.create() })
-                sequenceOf(Result.success(mapOf(term to result)))
+                sequenceOf(Result.success(mapOf(t to result)))
             }
 
             else -> throw IllegalStateException()
@@ -66,15 +70,13 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
                 // Value will be unified with the successive arguments of term.
                 // On successful unification, arg is unified with the argument number.
                 // Backtracking yields alternative solutions.
-                var count = 0
+                for ((count, argument) in t.arguments.withIndex()) {
-                for (argument in t.arguments) {
                     unifyLazy(value, argument, subs).forEach { result ->
                         result.map {
                             val sub = arg to Integer(count + 1)
                             yield(Result.success(it + sub))
                         }
                     }
-                    count++
                 }
 
             }
@@ -94,6 +96,12 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
             }
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Arg = Arg(
+        arg.applySubstitution(subs),
+        term.applySubstitution(subs),
+        value.applySubstitution(subs)
+    )
 }
 
 /**
@@ -118,11 +126,14 @@ class ClauseOp(private val head: Head, private val body: Body) :
                 val clauseHead = clause.head
                 val clauseBody = clause.body
 
+                val appliedHead = applySubstitution(head, subs)
+                val appliedBody = applySubstitution(body, subs)
+
                 // Unify the head of the clause with the head of the goal
-                unifyLazy(clauseHead, head, subs).forEach { result ->
+                unifyLazy(clauseHead, appliedHead, subs).forEach { result ->
                     result.map { headSubs ->
                         // Unify the body of the clause with the body of the goal
-                        unifyLazy(clauseBody, body, headSubs).forEach { bodyResult ->
+                        unifyLazy(clauseBody, appliedBody, headSubs).forEach { bodyResult ->
                             bodyResult.map { bodySubs ->
                                 // Combine the substitutions from the head and body
                                 val combinedSubs = headSubs + bodySubs
@@ -136,6 +147,11 @@ class ClauseOp(private val head: Head, private val body: Body) :
             yield(Result.success(emptyMap()))
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): ClauseOp = ClauseOp(
+        head.applySubstitution(subs) as Head,
+        body.applySubstitution(subs) as Body
+    )
 }
 
 class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
@@ -146,6 +162,8 @@ class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
             emptySequence()
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): AtomicOp = AtomicOp(term.applySubstitution(subs))
 }
 
 class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term) {
@@ -156,4 +174,75 @@ class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term
             emptySequence()
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): CompoundOp = CompoundOp(term.applySubstitution(subs))
+}
+
+open class Univ(private val term: Term, private val list: Term) : Operator(Atom("=.."), term, list) {
+    override fun satisfy(subs: Substitutions): Answers {
+        return when {
+            nonvariable(term, subs) && nonvariable(list, subs) -> {
+                val t = applySubstitution(term, subs)
+                val l = applySubstitution(list, subs) as List
+                unifyLazy(t, listToTerm(l), subs)
+            }
+
+            variable(term, subs) && nonvariable(list, subs) -> {
+                val l = applySubstitution(list, subs) as List
+                val t = listToTerm(l)
+                unifyLazy(term, t, subs)
+            }
+
+            nonvariable(term, subs) && variable(list, subs) -> {
+                val t = applySubstitution(term, subs)
+                val l = termToList(t)
+                unifyLazy(l, list, subs)
+            }
+
+            else -> throw Exception("Arguments are not sufficiently instantiated")
+        }
+    }
+
+    protected open fun listToTerm(list: List): Term {
+        return when {
+            list.size.value == 1 -> list.head
+
+            list.size.value > 1 -> {
+                val head = list.head
+                val arguments = mutableListOf<Term>()
+                var tail: List? = list.tail
+                while (tail != null && tail !is Empty) {
+                    arguments.add(tail.head)
+                    tail = tail.tail
+                }
+                Structure(head as Atom, arguments)
+            }
+
+            else -> throw IllegalStateException("List is empty")
+        }
+    }
+
+    protected open fun termToList(term: Term): List {
+        return when (term) {
+            is Atom -> Cons(term, Empty)
+
+            is Structure -> {
+                val head = term.functor.name
+                val arguments = term.arguments
+                // Construct the list by iterating over the arguments in reverse
+                var tail: List = Empty
+                for (i in arguments.size - 1 downTo 0) {
+                    tail = Cons(arguments[i], tail)
+                }
+                return Cons(head, tail)
+            }
+
+            else -> throw IllegalStateException("Term is not a valid structure")
+        }
+    }
+
+    override fun applySubstitution(subs: Substitutions): Univ = Univ(
+        term.applySubstitution(subs),
+        list.applySubstitution(subs)
+    )
 }

src/prolog/builtins/controlOperators.kt

@@ -2,14 +2,15 @@ package prolog.builtins
 
 import prolog.Answers
 import prolog.Substitutions
+import prolog.ast.Database.Program
 import prolog.ast.logic.LogicOperand
 import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
-import prolog.ast.terms.Structure
 import prolog.flags.AppliedCut
 import prolog.logic.applySubstitution
+import prolog.logic.numbervars
 
 /**
  * Always fail.
@@ -53,8 +54,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             left.fold(
                 // If it succeeds, satisfy the right part with the updated substitutions and return all results
                 onSuccess = { leftSubs ->
-                    right.satisfy(subs + leftSubs).forEach {
+                    right.satisfy(subs + leftSubs).forEach { right ->
-                        it.fold(
+                        right.fold(
                             // If the right part succeeds, yield the result with the left substitutions
                             onSuccess = { rightSubs ->
                                 yield(Result.success(leftSubs + rightSubs))

src/prolog/builtins/listOperators.kt

@@ -0,0 +1,27 @@
+package prolog.builtins
+
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.lists.List
+import prolog.ast.lists.List.Cons
+import prolog.ast.lists.List.Empty
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Operator
+import prolog.ast.terms.Term
+
+class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
+    private var solution: Operator = if (list is Empty) {
+        Unify(element, list)
+    } else if (list is Cons) {
+        Disjunction(
+            Unify(element, list.head),
+            Member(element, list.tail)
+        )
+    } else {
+        throw IllegalArgumentException("Invalid list type: ${list::class.simpleName}")
+    }
+
+    override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs)
+
+    override fun toString(): String = "$element ∈ $list"
+}

src/prolog/builtins/unificationOperators.kt

@@ -22,7 +22,7 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        yieldAll(unifyLazy(t1, t2, subs))
+        yieldAll(unifyLazy(t1, t2, emptyMap()))
     }
 
     override fun applySubstitution(subs: Substitutions): Unify = Unify(
@@ -45,7 +45,7 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        if (equivalent(t1, t2, subs)) {
+        if (equivalent(t1, t2, emptyMap())) {
             yield(Result.success(emptyMap()))
         }
     }

src/prolog/logic/unification.kt

@@ -7,10 +7,11 @@ import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
 import prolog.ast.arithmetic.Number
-import prolog.ast.logic.Clause
+import prolog.ast.lists.List
+import prolog.ast.lists.List.Cons
+import prolog.ast.lists.List.Empty
 import prolog.ast.logic.Fact
 import prolog.ast.logic.LogicOperator
-import prolog.ast.logic.Rule
 import prolog.ast.terms.*
 
 // Apply substitutions to a term
@@ -58,7 +59,10 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
     val t2 = applySubstitution(term2, subs)
 
     when {
-        equivalent(t1, t2, subs) -> yield(Result.success(emptyMap()))
+        equivalent(t1, t2, subs) -> {
+            yield(Result.success(emptyMap()))
+        }
+
         variable(t1, subs) -> {
             val variable = t1 as Variable
             if (!occurs(variable, t2, subs)) {
@@ -81,18 +85,32 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
                 val args1 = structure1.arguments
                 val args2 = structure2.arguments
                 if (args1.size == args2.size) {
-                    val results = args1.zip(args2).map { (arg1, arg2) ->
+                    yieldAll(unifyArgs(args1, args2, subs))
-                        unifyLazy(arg1, arg2, subs)
+                }
+            }
+        }
+
+        t1 is List && t2 is List -> {
+            if (equivalent(t1, t2, subs)) {
+                yield(Result.success(emptyMap()))
+            } else if (t1.size == t2.size) {
+                val head1 = t1.head
+                val head2 = t2.head
+
+                unifyLazy(head1, head2, subs).forEach { headSubs ->
+                    headSubs.map { headResult ->
+                        if (t1 is Empty && t2 is Empty) {
+                            yield(Result.success(headResult))
+                        } else if (t1 is Cons && t2 is Cons) {
+                            val tail1 = t1.tail
+                            val tail2 = t2.tail
+                            unifyLazy(tail1, tail2, headResult).forEach { tailSubs ->
+                                tailSubs.map { tailResult ->
+                                    yield(Result.success(headResult + tailResult))
+                                }
                             }
-                    // Combine the results of all unifications
-                    val combinedResults = results.reduce { acc, result ->
-                        acc.flatMap { a ->
-                            result.map { b ->
-                                if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
                         }
-                        }.map { Result.success(it) }
                     }
-                    yieldAll(combinedResults)
                 }
             }
         }
@@ -101,6 +119,32 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
     }
 }
 
+private fun unifyArgs(
+    args1: kotlin.collections.List<Argument>,
+    args2: kotlin.collections.List<Argument>,
+    subs: Substitutions
+): Answers = sequence {
+    // Using the current subs, unify the first argument of each list
+    val arg1 = applySubstitution(args1[0], subs)
+    val arg2 = applySubstitution(args2[0], subs)
+    unifyLazy(arg1, arg2, subs).forEach { headResult ->
+        // Use the resulting substitutions to unify the rest of the arguments
+        headResult.map { headSubs ->
+            val rest1 = args1.drop(1).map { applySubstitution(it, headSubs) }
+            val rest2 = args2.drop(1).map { applySubstitution(it, headSubs) }
+            if (rest1.isEmpty() && rest2.isEmpty()) {
+                yield(Result.success(headSubs))
+            } else if (rest1.isNotEmpty() && rest2.isNotEmpty()) {
+                unifyArgs(rest1, rest2, subs).forEach { tailResult ->
+                    tailResult.map { tailSubs ->
+                        yield(Result.success(headSubs + tailSubs))
+                    }
+                }
+            }
+        }
+    }
+}
+
 fun unify(term1: Term, term2: Term): Answer {
     val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
     return if (substitutions.hasNext()) {
@@ -116,12 +160,32 @@ fun unify(term1: Term, term2: Term): Answer {
 fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
     return when {
         term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0
-        term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0
+        term1 is Structure && term2 is Structure -> {
+            term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) ->
+                equivalent(arg1, arg2, subs)
+            }
+        }
+
         term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
         term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0
         term1 is Variable && term2 is Variable -> term1 == term2
         term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
         term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
+        term1 is List && term2 is List -> {
+            if (term1.isEmpty() && term2.isEmpty()) {
+                true
+            } else if (term1.isEmpty() || term2.isEmpty()) {
+                false
+            } else {
+                require(term1 is Cons && term2 is Cons)
+                val head1 = term1.head
+                val tail1 = term1.tail
+                val head2 = term2.head
+                val tail2 = term2.tail
+                equivalent(head1, head2, subs) && equivalent(tail1, tail2, subs)
+            }
+        }
+
         else -> false
     }
 }

tests/parser/grammars/TermsGrammarTests.kt

@@ -19,6 +19,8 @@ import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
 import prolog.builtins.Is
 import prolog.logic.equivalent
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 
 class TermsGrammarTests {
     private lateinit var parser: Grammar<Term>
@@ -352,4 +354,49 @@ class TermsGrammarTests {
             )
         }
     }
+
+    @Nested
+    class Lists {
+        private lateinit var parser: Grammar<Term>
+
+        @BeforeEach
+        fun setup() {
+            parser = TermsGrammar() as Grammar<Term>
+        }
+
+        @Test
+        fun `parse empty list`() {
+            val input = "[]"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(Empty, result, "Expected empty list")
+        }
+
+        @Test
+        fun `parse non-empty list`() {
+            val input = "[a, b, c]"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Empty))),
+                result,
+                "Expected non-empty list"
+            )
+        }
+
+        @Test
+        fun `parse nested lists`() {
+            val input = "[a, [b, c], d]"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Cons(Atom("a"), Cons(Cons(Atom("b"), Cons(Atom("c"), Empty)), Cons(Atom("d"), Empty))),
+                result,
+                "Expected nested lists"
+            )
+        }
+    }
 }

tests/prolog/EvaluationTests.kt

@@ -15,7 +15,10 @@ import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.ast.Database.Program
 import prolog.ast.arithmetic.Integer
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 import prolog.ast.terms.AnonymousVariable
+import prolog.builtins.Unify
 
 class EvaluationTests {
     @BeforeEach
@@ -479,4 +482,20 @@ class EvaluationTests {
         assertEquals(1, subs3c.size, "Expected 1 substitution")
         assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
     }
+
+    @Test
+    fun `foo(emptyList) = foo(X)`() {
+        val list = Empty
+        val left = Structure(Atom("foo"), listOf(list))
+        val right = Structure(Atom("foo"), listOf(Variable("X")))
+
+        val unific = Unify(left, right)
+        val result = unific.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected 1 substitution")
+        assertEquals(list, subs[Variable("X")], "Expected X to be list(1, 2)")
+    }
 }

tests/prolog/builtins/AnalysisOperatorsTests.kt

@@ -7,13 +7,13 @@ import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.assertThrows
 import prolog.ast.Database.Program
 import prolog.ast.arithmetic.Integer
+import prolog.ast.lists.List
+import prolog.ast.lists.List.Cons
+import prolog.ast.lists.List.Empty
 import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
-import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.*
-import prolog.ast.terms.AnonymousVariable
+import prolog.logic.equivalent
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Variable
 
 class AnalysisOperatorsTests {
     @Test
@@ -401,4 +401,246 @@ class AnalysisOperatorsTests {
             )
         }
     }
+
+    @Nested
+    class `Univ operator` {
+        @Test
+        fun `univ without variables`() {
+            val univ = Univ(Atom("foo"), Cons(Atom("foo"), Empty))
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertTrue(subs.isEmpty(), "Expected empty substitutions")
+        }
+
+        @Test
+        fun `univ with variable list`() {
+            val list = Variable("List")
+            val univ = Univ(
+                CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))),
+                list
+            )
+            val expected = Cons(Atom("foo"), Cons(Atom("a"), Cons(Atom("b"), Empty)))
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(expected, subs[list], "Expected List to be $expected")
+        }
+
+        @Test
+        fun `univ with variable in compound`() {
+            val list = Variable("List")
+            val univ = Univ(
+                CompoundTerm(Atom("foo"), listOf(Variable("X"))),
+                list
+            )
+            val expected = Cons(Atom("foo"), Cons(Variable("X"), Empty))
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(expected, subs[list], "Expected List to be $expected")
+        }
+
+        @Test
+        fun `univ with var foo`() {
+            val univ = Univ(
+                Variable("Term"),
+                Cons(Atom("foo"), Empty)
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(Atom("foo"), subs[Variable("Term")], "Expected Term to be foo")
+        }
+
+        @Test
+        fun `univ with var foo(a)`() {
+            val univ = Univ(
+                Variable("Term"),
+                Cons(Atom("foo"), Cons(Atom("a"), Empty))
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(
+                Structure(Atom("foo"), listOf(Atom("a"))),
+                subs[Variable("Term")],
+                "Expected Term to be foo(a)"
+            )
+        }
+
+        @Test
+        fun `univ with var foo(X)`() {
+            val univ = Univ(
+                Variable("Term"),
+                Cons(Atom("foo"), Cons(Variable("X"), Empty))
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(
+                Structure(Atom("foo"), listOf(Variable("X"))),
+                subs[Variable("Term")],
+                "Expected Term to be foo(X)"
+            )
+        }
+
+        @Test
+        fun `univ with var foo(a, b(X), c)`() {
+            val univ = Univ(
+                Variable("Term"),
+                Cons(
+                    Atom("foo"),
+                    Cons(Atom("a"), Cons(CompoundTerm(Atom("b"), listOf(Variable("X"))), Cons(Atom("c"), Empty)))
+                )
+            )
+            val expected = CompoundTerm(
+                Atom("foo"),
+                listOf(Atom("a"), CompoundTerm(Atom("b"), listOf(Variable("X"))), Atom("c"))
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(expected, subs[Variable("Term")], "Expected Term to be $expected")
+        }
+
+        @Test
+        fun `univ with unified var should return substitution`() {
+            val univ = Univ(
+                CompoundTerm(
+                    Atom("foo"), listOf(
+                        Atom("a"),
+                        CompoundTerm(Atom("bar"), listOf(Variable("X"))),
+                        Atom("c")
+                    )
+                ),
+                Cons(
+                    Atom("foo"),
+                    Cons(Atom("a"), Cons(CompoundTerm(Atom("bar"), listOf(Atom("b"))), Cons(Atom("c"), Empty)))
+                )
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result")
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution")
+            assertEquals(Atom("b"), subs[Variable("X")], "Expected X to be b")
+        }
+
+        @Test
+        fun `univ of incompatible structures should fail`() {
+            val univ = Univ(
+                CompoundTerm(Atom("foo"), listOf(Atom("a"))),
+                Cons(Atom("bar"), Empty)
+            )
+
+            val result = univ.satisfy(emptyMap()).toList()
+
+            assertEquals(0, result.size, "Expected 0 results")
+        }
+
+        @Test
+        fun `univ with two vars should throw`() {
+            val univ = Univ(Variable("X"), Variable("Y"))
+
+            val exception = assertThrows<Exception> {
+                univ.satisfy(emptyMap()).toList()
+            }
+            assertEquals("Arguments are not sufficiently instantiated", exception.message)
+        }
+
+        class OpenUniv(term: Term, list: Term) : Univ(term, list) {
+            public override fun listToTerm(list: List): Term = super.listToTerm(list)
+            public override fun termToList(term: Term): List = super.termToList(term)
+        }
+
+        @Test
+        fun `a to term`() {
+            val univ = OpenUniv(Atom(""), Empty)
+
+            val originalList = Cons(Atom("a"), Empty)
+            val originalTerm = Atom("a")
+
+            val term = univ.listToTerm(originalList)
+            assertEquals(originalTerm, term, "Expected term to be a")
+
+            val list = univ.termToList(term)
+            assertEquals(originalList, list, "Expected list to be [a]")
+        }
+
+        @Test
+        fun `foo, bar to compound`() {
+            val univ = OpenUniv(Atom(""), Empty)
+
+            val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Empty))
+            val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar")))
+
+            val term = univ.listToTerm(originalList)
+            assertEquals(originalTerm, term)
+
+            val list = univ.termToList(term)
+            assertEquals(originalList, list)
+        }
+
+        @Test
+        fun `foo, bar, baz to compound`() {
+            val univ = OpenUniv(Atom(""), Empty)
+
+            val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Atom("baz"), Empty)))
+            val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar"), Atom("baz")))
+
+            val term = univ.listToTerm(originalList)
+            assertEquals(originalTerm, term)
+
+            val list = univ.termToList(term)
+            assertEquals(originalList, list)
+        }
+
+        @Test
+        fun `foo, bar, (baz, bar) to compound with list`() {
+            val univ = OpenUniv(Atom(""), Empty)
+
+            val originalList =
+                Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
+            val originalTerm = CompoundTerm(
+                Atom("foo"),
+                listOf(Atom("bar"), Cons(Atom("baz"), Cons(Atom("bar"), Empty)))
+            )
+
+            val term = univ.listToTerm(originalList)
+            assertTrue(equivalent(originalTerm, term, emptyMap()), "Expected term to be foo(bar, [baz, bar]))")
+
+            val list = univ.termToList(term)
+            assertTrue(equivalent(originalList, list, emptyMap()), "Expected list to be [foo, bar, [baz, bar]]")
+        }
+    }
 }

tests/prolog/builtins/ListOperatorsTests.kt

@@ -0,0 +1,73 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import prolog.ast.lists.List.Cons
+import prolog.ast.lists.List.Empty
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Variable
+
+class ListOperatorsTests {
+    @Test
+    fun `size empty list is 0`() {
+        assertEquals(0, Empty.size.value, "Expected size of empty list to be 0")
+    }
+
+    @Test
+    fun `size of singleton is 1`() {
+        val list = Cons(Atom("a"), Empty)
+
+        assertEquals(1, list.size.value, "Expected size of singleton list to be 1")
+    }
+
+    @Test
+    fun `size of list with five elements is 5`() {
+        val list = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("e"), Empty)))))
+
+        assertEquals(5, list.size.value, "Expected size of list with five elements to be 5")
+    }
+
+    @Test
+    fun `member(a, list of a)`() {
+        val atom = Atom("a")
+        val list = Cons(atom, Empty)
+
+        val member = Member(atom, list)
+
+        val result = member.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
+    }
+
+    @Test
+    fun `member should only check shallow`() {
+        val list = Cons(Atom("a"), Cons(Cons(Atom("b"), Empty), Empty))
+
+        var result = Member(Atom("a"), list).satisfy(emptyMap()).toList()
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
+
+        result = Member(Atom("b"), list).satisfy(emptyMap()).toList()
+        assertEquals(0, result.size, "Expected no solution")
+    }
+
+    @Test
+    fun `member with variable in list`() {
+        val atom = Atom("a")
+        val variable = Variable("X")
+        val list = Cons(variable, Empty)
+
+        val member = Member(atom, list)
+
+        val result = member.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom")
+    }
+}

tests/prolog/logic/UnificationTests.kt

@@ -10,13 +10,16 @@ import prolog.ast.terms.Variable
 import prolog.builtins.Add
 import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Nested
+import prolog.ast.lists.List
+import prolog.ast.lists.List.Empty
+import prolog.ast.lists.List.Cons
 
 /*
  * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
  */
 class UnificationTests {
     @Nested
-    class `unify` {
+    class `unify logic` {
         @Test
         fun identical_atoms_unify() {
             val atom1 = Atom("a")
@@ -330,7 +333,7 @@ class UnificationTests {
     }
 
     @Nested
-    class `applySubstitution` {
+    class `applySubstitution logic` {
         @Test
         fun `apply substitution without sub`() {
             val term = Variable("X")
@@ -367,4 +370,120 @@ class UnificationTests {
             assertEquals(Integer(35), result)
         }
     }
+
+    @Nested
+    class `equivalent logic` {
+        @Test
+        fun `empty lists are equivalent`() {
+            var eq = equivalent(Empty, Empty, emptyMap())
+            assertTrue(eq, "Empty lists should be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(Empty, variable, mapOf(variable to Empty))
+            assertTrue(eq, "Empty list and variable should be equivalent")
+
+            eq = equivalent(variable, Empty, mapOf(variable to Empty))
+            assertTrue(eq, "Variable and empty list should be equivalent")
+        }
+
+        @Test
+        fun `singletons are equivalent`() {
+            val atom = Atom("a")
+            val list1 = Cons(atom, Empty)
+            val list2 = Cons(atom, Empty)
+
+            var eq = equivalent(list1, list2, emptyMap())
+            assertTrue(eq, "Singleton lists should be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(list1, variable, mapOf(variable to list2))
+            assertTrue(eq, "Singleton list and variable should be equivalent")
+
+            eq = equivalent(variable, list1, mapOf(variable to list2))
+            assertTrue(eq, "Variable and singleton list should be equivalent")
+        }
+
+        @Test
+        fun `singleton and empty list are not equivalent`() {
+            val atom = Atom("a")
+            val list1 = Cons(atom, Empty)
+            val list2 = Empty
+
+            var eq = equivalent(list1, list2, emptyMap())
+            assertFalse(eq, "Singleton and empty lists should not be equivalent")
+
+            eq = equivalent(list2, list1, emptyMap())
+            assertFalse(eq, "Empty and singleton lists should not be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(list1, variable, mapOf(variable to list2))
+            assertFalse(eq, "Singleton list and variable should not be equivalent")
+
+            eq = equivalent(variable, list1, mapOf(variable to list2))
+            assertFalse(eq, "Variable and singleton list should not be equivalent")
+        }
+
+        @Test
+        fun `identical lists are equivalent`() {
+            val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty))
+            val list2 = Cons(Atom("a"), Cons(Atom("b"), Empty))
+
+            var eq = equivalent(list1, list2, emptyMap())
+            assertTrue(eq, "Identical lists should be equivalent")
+
+            eq = equivalent(list2, list1, emptyMap())
+            assertTrue(eq, "Identical lists should be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(list1, variable, mapOf(variable to list2))
+            assertTrue(eq, "Identical lists should be equivalent")
+
+            eq = equivalent(variable, list2, mapOf(variable to list1))
+            assertTrue(eq, "Identical lists should be equivalent")
+        }
+
+        @Test
+        fun `identical nested lists are equivalent`() {
+            val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
+            val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
+
+            var eq = equivalent(list1, list2, emptyMap())
+            assertTrue(eq, "Identical nested lists should be equivalent")
+
+            eq = equivalent(list2, list1, emptyMap())
+            assertTrue(eq, "Identical nested lists should be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(list1, variable, mapOf(variable to list2))
+            assertTrue(eq, "Identical nested lists should be equivalent")
+
+            eq = equivalent(variable, list2, mapOf(variable to list1))
+            assertTrue(eq, "Identical nested lists should be equivalent")
+        }
+
+        @Test
+        fun `lists with different nests are not equivalent`() {
+            val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("bar"), Cons(Atom("baz"), Empty)), Empty)))
+            val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
+
+            var eq = equivalent(list1, list2, emptyMap())
+            assertFalse(eq, "Lists with different nests should not be equivalent")
+
+            eq = equivalent(list2, list1, emptyMap())
+            assertFalse(eq, "Lists with different nests should not be equivalent")
+
+            val variable = Variable("X")
+
+            eq = equivalent(list1, variable, mapOf(variable to list2))
+            assertFalse(eq, "Lists with different nests should not be equivalent")
+
+            eq = equivalent(variable, list2, mapOf(variable to list1))
+            assertFalse(eq, "Lists with different nests should not be equivalent")
+        }
+    }
 }