Checkpoint

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("univ/2") -> Univ(args[0], args[1])
 
                     // Arithmetic
                     Functor.of("inf/0") -> Integer(Int.MAX_VALUE)

src/parser/grammars/TermsGrammar.kt

@@ -87,7 +87,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))
     }

src/parser/grammars/Tokens.kt

@@ -20,6 +20,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,25 @@ 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 headResult = headToGoalSubs.filterKeys { key ->
-                                goalToHeadSubs.any {
-                                    occurs(
-                                        key as Variable,
-                                        it.value
-                                    )
-                                }
-                            }
-                            yield(Result.success(goalToHeadResult + headResult))
+                            val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
+                            yield(Result.success(goalResult + 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) }
-                                    yield(Result.failure(AppliedCut(result)))
+                                    val goalResult = goalToHeadSubs.mapValues {
+                                        applySubstitution(it.value, error.subs)
+                                    }
+                                    yield(Result.failure(AppliedCut(goalResult + headResult)))
                                 } 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.
@@ -66,15 +69,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 (argument in t.arguments) {
+                for ((count, argument) in t.arguments.withIndex()) {
                     unifyLazy(value, argument, subs).forEach { result ->
                         result.map {
                             val sub = arg to Integer(count + 1)
                             yield(Result.success(it + sub))
                         }
                     }
-                    count++
                 }
 
             }
@@ -94,6 +95,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 +125,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 +146,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 +161,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 +173,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/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/logic/unification.kt

@@ -7,11 +7,15 @@ 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.*
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
@@ -97,6 +101,31 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
             }
         }
 
+        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))
+                                }
+                            }
+                        }
+                    }
+                }
+            }
+        }
+
         else -> {}
     }
 }
@@ -122,6 +151,21 @@ fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
         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
     }
 }