Cleanup 2

src/interpreter/Preprocessor.kt

@@ -3,7 +3,6 @@ package interpreter
 import io.Logger
 import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Integer
-import prolog.ast.lists.List as PList
 import prolog.ast.logic.Clause
 import prolog.ast.logic.Fact
 import prolog.ast.logic.LogicOperand
@@ -64,9 +63,9 @@ open class Preprocessor {
                     Functor.of("functor/3") -> FunctorOp(args[0], args[1], args[2])
                     Functor.of("arg/3") -> Arg(args[0], args[1], args[2])
                     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])
+                    Functor.of("numbervars/1") -> NumberVars(args[0])
+                    Functor.of("numbervars/3") -> NumberVars(args[0], args[1] as Integer, args[2])
 
                     // Arithmetic
                     Functor.of("inf/0") -> Integer(Int.MAX_VALUE)
@@ -156,7 +155,8 @@ open class Preprocessor {
                     Functor.of("read/1") -> Read(args[0])
 
                     // Lists
-                    Functor.of("member/2") -> Member(args[0], args[1] as PList)
+                    Functor.of("member/2") -> Member(args[0], args[1])
+                    Functor.of("append/3") -> Append(args[0], args[1], args[2])
 
                     // Meta
                     Functor.of("call/1") -> Call(args[0])
@@ -172,6 +172,12 @@ open class Preprocessor {
                     Functor.of("==/2") -> Equivalent(args[0], args[1])
                     Functor.of("\\==/2") -> NotEquivalent(args[0], args[1])
 
+                    // Verification
+                    Functor.of("atomic/1") -> Atomic(args[0])
+                    Functor.of("compound/1") -> Compound(args[0])
+                    Functor.of("nonvar/1") -> NonVar(args[0])
+                    Functor.of("var/1") -> Var(args[0])
+
                     Functor.of(":-/2") -> Rule(args[0] as Head, args[1] as Body)
 
                     else -> {

src/prolog/ast/arithmetic/ArithmeticOperator.kt

@@ -4,4 +4,7 @@ import prolog.ast.terms.Atom
 import prolog.ast.terms.Operator
 
 abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) :
-    Operator(symbol, leftOperand, rightOperand), Expression
+    Operator(symbol, leftOperand, rightOperand), Expression {
+    constructor(symbol: String, leftOperand: Expression, rightOperand: Expression) :
+            this(Atom(symbol), leftOperand, rightOperand)
+}

src/prolog/ast/lists/List.kt

@@ -6,11 +6,18 @@ import prolog.ast.arithmetic.Integer
 
 sealed class List : Term {
     abstract val head: Term
-    open val tail: List? = null
+    open val tail: Term? = null
+
+    operator fun component1(): Term = head
+    operator fun component2(): Term? = tail
+
     val size: Integer
         get() = when (this) {
             is Empty -> Integer(0)
-            is Cons -> Integer(1 + tail.size.value)
+            is Cons -> {
+                val tailSize = if (tail is List) { (tail as List).size.value } else 0
+                Integer(1 + tailSize)
+            }
         }
 
     fun isEmpty(): Boolean = this is Empty
@@ -24,7 +31,7 @@ sealed class List : Term {
         override fun toString(): String = "[]"
     }
 
-    class Cons(override val head: Term, override var tail: List) : List() {
+    class Cons(override val head: Term, override var tail: Term) : List() {
         override fun applySubstitution(subs: Substitutions): List {
             val newHead = head.applySubstitution(subs)
             val newTail = tail.applySubstitution(subs) as List
@@ -33,11 +40,12 @@ sealed class List : Term {
 
         override fun toString(): String {
             val values = mutableListOf<Term>()
-            var current: List? = this
+            var current: Term? = this
-            while (current != null && current !is Empty) {
+            while (current != null && current is Cons) {
                 values.add(current.head)
                 current = current.tail
             }
+            if (current != null && current !is Empty) values.add(current)
             return "[${values.joinToString(", ")}]"
         }
     }

src/prolog/ast/logic/LogicOperator.kt

@@ -10,5 +10,8 @@ abstract class LogicOperator(
     leftOperand: LogicOperand? = null,
     rightOperand: LogicOperand
 ) : Operator(symbol, leftOperand, rightOperand), Satisfiable {
+    constructor(symbol: String, leftOperand: LogicOperand? = null, rightOperand: LogicOperand) :
+            this(Atom(symbol), leftOperand, rightOperand)
+
     abstract override fun satisfy(subs: Substitutions): Answers
 }

src/prolog/ast/terms/Functor.kt

@@ -4,6 +4,8 @@ import prolog.Substitutions
 import prolog.ast.arithmetic.Integer
 
 data class Functor(val name: Atom, val arity: Integer) : Term {
+    constructor(name: String, arity: Int) : this(Atom(name), Integer(arity))
+
     companion object {
         fun of(functor: String): Functor {
             // Split the functor string into name and arity, by splitting the last "/"

src/prolog/ast/terms/Operator.kt

@@ -7,6 +7,9 @@ abstract class Operator(
     private val leftOperand: Operand? = null,
     private val rightOperand: Operand
 ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Term {
+    constructor(symbol: String, leftOperand: Operand? = null, rightOperand: Operand) :
+            this(Atom(symbol), leftOperand, rightOperand)
+
     override fun toString(): String {
         return when (leftOperand) {
             null -> "${symbol.name} $rightOperand"

src/prolog/ast/terms/Structure.kt

@@ -12,6 +12,8 @@ typealias Argument = Term
 typealias CompoundTerm = Structure
 
 open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
+    constructor(name: String, vararg arguments: Argument) : this(Atom(name), arguments.asList())
+
     override val functor: Functor = Functor(name, Integer(arguments.size))
 
     override fun solve(goal: Goal, subs: Substitutions): Answers {

src/prolog/builtins/analysisOperators.kt

@@ -1,5 +1,6 @@
 package prolog.builtins
 
+import com.sun.tools.javac.resources.CompilerProperties.Fragments.Anonymous
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.Database.Program
@@ -16,9 +17,11 @@ import prolog.ast.lists.List.Cons
  *
  * If Term is a [Variable] it is unified with a new term whose arguments are all different variables.
  * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term.
+ *
+ * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3)
  */
 class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) :
-    Structure(Atom("functor"), listOf(term, functorName, functorArity)) {
+    Structure("functor", term, functorName, functorArity) {
     override fun satisfy(subs: Substitutions): Answers {
         return when {
             nonvariable(term, subs) -> {
@@ -54,7 +57,7 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v
 }
 
 class Arg(private val arg: Term, private val term: Term, private val value: Term) :
-    Structure(Atom("arg"), listOf(arg, term, value)) {
+    Structure("arg", arg, term, value) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" }
         require(compound(term, subs)) {
@@ -115,7 +118,7 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
  * [SWI-Prolog Operator clause/2](https://www.swi-prolog.org/pldoc/doc_for?object=clause/2)
  */
 class ClauseOp(private val head: Head, private val body: Body) :
-    Structure(Atom("clause"), listOf(head, body)) {
+    Structure("clause", head, body) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" }
 
@@ -154,31 +157,7 @@ class ClauseOp(private val head: Head, private val body: Body) :
     )
 }
 
-class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
+open class Univ(private val term: Term, private val list: Term) : Operator("=..", term, list) {
-    override fun satisfy(subs: Substitutions): Answers {
-        return if (atomic(term, subs)) {
-            sequenceOf(Result.success(emptyMap()))
-        } else {
-            emptySequence()
-        }
-    }
-
-    override fun applySubstitution(subs: Substitutions): AtomicOp = AtomicOp(term.applySubstitution(subs))
-}
-
-class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term) {
-    override fun satisfy(subs: Substitutions): Answers {
-        return if (compound(term, subs)) {
-            sequenceOf(Result.success(emptyMap()))
-        } else {
-            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) -> {
@@ -210,11 +189,14 @@ open class Univ(private val term: Term, private val list: Term) : Operator(Atom(
             list.size.value > 1 -> {
                 val head = list.head
                 val arguments = mutableListOf<Term>()
-                var tail: List? = list.tail
+                var tail: Term? = list.tail
-                while (tail != null && tail !is Empty) {
+                while (tail != null && tail is Cons) {
                     arguments.add(tail.head)
                     tail = tail.tail
                 }
+                if (tail != null && tail !is Empty) {
+                    arguments.add(tail)
+                }
                 Structure(head as Atom, arguments)
             }
 
@@ -246,3 +228,23 @@ open class Univ(private val term: Term, private val list: Term) : Operator(Atom(
         list.applySubstitution(subs)
     )
 }
+
+class NumberVars(private val term: Term, private val start: Integer, private val end: Term) :
+    Structure("numbervars", term, start, end) {
+    private var yieldEnd: Boolean = true
+
+    constructor(term: Term) : this(term, Integer(0), AnonymousVariable.create()) {
+        yieldEnd = false
+    }
+
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        val (newEnd, newSubs) = numbervars(term, start.value, subs)
+        unifyLazy(end, Integer(newEnd), subs).forEach { endResult ->
+            endResult.map { endSubs ->
+                val result = if (yieldEnd) (newSubs + endSubs) else newSubs
+                yield(Result.success(result))
+            }
+
+        }
+    }
+}

src/prolog/builtins/arithmeticOperators.kt

@@ -22,7 +22,7 @@ import prolog.logic.*
  * True if expression Expr1 evaluates to a number non-equal to Expr2.
  */
 class EvaluatesToDifferent(private val left: Expression, private val right: Expression) :
-    Operator(Atom("=\\="), left, right), Satisfiable {
+    Operator("=\\=", left, right), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
         val t1 = left.simplify(subs)
         val t2 = right.simplify(subs)
@@ -49,7 +49,7 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
  * True if Expr1 evaluates to a number equal to Expr2.
  */
 class EvaluatesTo(private val left: Expression, private val right: Expression) :
-    Operator(Atom("=:="), left, right) {
+    Operator("=:=", left, right) {
     override fun satisfy(subs: Substitutions): Answers {
         val t1 = left.simplify(subs)
         val t2 = right.simplify(subs)
@@ -72,7 +72,7 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
  * True when Number is the value to which Expr evaluates.
  */
 class Is(val number: Expression, val expr: Expression) :
-    Operator(Atom("is"), number, expr), Satisfiable {
+    Operator("is", number, expr), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
         val t1 = number.simplify(subs)
         val t2 = expr.simplify(subs)
@@ -108,7 +108,7 @@ class Positive(operand: Expression) : Add(Integer(0), operand)
  * Result = Expr1 + Expr2
  */
 open class Add(private val expr1: Expression, private val expr2: Expression) :
-    ArithmeticOperator(Atom("+"), expr1, expr2) {
+    ArithmeticOperator("+", expr1, expr2) {
     override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = plus(expr1, expr2, result, subs)
@@ -126,7 +126,7 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
  * Result = Expr1 - Expr2
  */
 open class Subtract(private val expr1: Expression, private val expr2: Expression) :
-    ArithmeticOperator(Atom("-"), expr1, expr2) {
+    ArithmeticOperator("-", expr1, expr2) {
     override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = plus(expr2, result, expr1, subs)
@@ -144,7 +144,7 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
  * Result = Expr1 * Expr2
  */
 class Multiply(val expr1: Expression, val expr2: Expression) :
-    ArithmeticOperator(Atom("*"), expr1, expr2) {
+    ArithmeticOperator("*", expr1, expr2) {
     override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = mul(expr1, expr2, result, subs)
@@ -159,7 +159,7 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
 }
 
 class Divide(private val expr1: Expression, private val expr2: Expression) :
-    ArithmeticOperator(Atom("/"), expr1, expr2) {
+    ArithmeticOperator("/", expr1, expr2) {
     override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = div(expr1, expr2, result, subs)
@@ -178,7 +178,7 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
 // TODO Expr rem Expr
 
 class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) :
-    CompoundTerm(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable {
+    CompoundTerm("between", expr1, expr2, expr3), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
         val e1 = expr1.simplify(subs)
         val e2 = expr2.simplify(subs)
@@ -210,6 +210,6 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
 }
 
 class Successor(private val expr1: Expression, private val expr2: Expression) :
-    CompoundTerm(Atom("succ"), listOf(expr1, expr2)), Satisfiable {
+    CompoundTerm("succ", expr1, expr2), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs)
 }

src/prolog/builtins/controlOperators.kt

@@ -48,7 +48,7 @@ class Cut() : Atom("!") {
  * Conjunction (and). True if both Goal1 and Goal2 are true.
  */
 open class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
-    LogicOperator(Atom(","), left, right) {
+    LogicOperator(",", left, right) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         fun satisfyRight(leftSubs: Substitutions): Answers = sequence {
             right.satisfy(subs + leftSubs).forEach { right ->
@@ -123,7 +123,7 @@ open class Conjunction(val left: LogicOperand, private val right: LogicOperand)
  * Disjunction (or). True if either Goal1 or Goal2 succeeds.
  */
 open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) :
-    LogicOperator(Atom(";"), left, right) {
+    LogicOperator(";", left, right) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         left.satisfy(subs).forEach { left ->
             left.fold(
@@ -158,7 +158,7 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l
 /**
  * True if 'Goal' cannot be proven.
  */
-class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) {
+open class Not(private val goal: Goal) : LogicOperator("\\+", rightOperand = goal) {
     override fun satisfy(subs: Substitutions): Answers {
         // If the goal can be proven, return an empty sequence
         val goalResults = goal.satisfy(subs).iterator()

src/prolog/builtins/databaseOperators.kt

@@ -49,7 +49,7 @@ class Assert(clause: Clause) : AssertZ(clause) {
 /**
  * Assert a [Clause] as a first clause of the [Predicate] into the [Program].
  */
-class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
+class AssertA(val clause: Clause) : Operator("asserta", rightOperand = clause) {
     override fun satisfy(subs: Substitutions): Answers {
         // Add clause to the program
         val evaluatedClause = applySubstitution(clause, subs) as Clause
@@ -64,7 +64,7 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
 /**
  * Assert a [Clause] as a last clause of the [Predicate] into the [Program].
  */
-open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) {
+open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clause) {
     override fun satisfy(subs: Substitutions): Answers {
         // Add clause to the program
         val evaluatedClause = applySubstitution(clause, subs) as Clause
@@ -82,7 +82,7 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
  *
  * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1)
  */
-open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
+open class Retract(val term: Term) : Operator("retract", rightOperand = term) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         // Check that term is a structure or atom
         if (term !is Structure && term !is Atom) {

src/prolog/builtins/delimitedContinuationsOperators.kt

@@ -23,7 +23,7 @@ import prolog.logic.unifyLazy
  * return, unifying Cont with a Goal that represents the continuation after shift.
  */
 class Reset(private val goal: Goal, private val ball: Term, private val cont: Term) :
-    Structure(Atom("reset"), listOf(goal, ball, cont)) {
+    Structure("reset", goal, ball, cont) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         goal.satisfy(subs).forEach { goalResult ->
             goalResult.fold(
@@ -63,7 +63,7 @@ class Reset(private val goal: Goal, private val ball: Term, private val cont: Te
 /**
  * Variables that have been bound during the procedure called by reset/3 stay bound after a shift/1:
  */
-class Shift(private val ball: Term) : Structure(Atom("shift"), listOf(ball)) {
+class Shift(private val ball: Term) : Structure("shift", ball) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         val shift = AppliedShift(
             subs = subs,

src/prolog/builtins/ioOperators.kt

@@ -16,7 +16,7 @@ import prolog.logic.unifyLazy
 /**
  * Write [Term] to the current output, using brackets and operators where appropriate.
  */
-class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
+class Write(private val term: Term) : Operator("write", rightOperand = term), Satisfiable {
     constructor(message: String) : this(Atom(message))
 
     override fun satisfy(subs: Substitutions): Answers {

src/prolog/builtins/listOperators.kt

@@ -5,18 +5,28 @@ 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.Body
 import prolog.ast.terms.Operator
+import prolog.ast.terms.Structure
 import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
 import prolog.logic.applySubstitution
+import prolog.logic.unifyLazy
 
-class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
+class Member(private val element: Term, private val list: Term) : Operator("member", element, list) {
-    private var solution: Operator = when (list) {
+    private var solution: Body = when (list) {
-        is Empty -> Disjunction(Fail, Fail)
+        is Empty -> Fail
         is Cons -> Disjunction(
             Unify(element, list.head),
             Member(element, list.tail)
         )
+
+        else -> {
+            // Generate a sequence of lists that have anonymous variables in them.
+            // Place element at each index
+            // TODO Fix this
+            Unify(element, list)
+        }
     }
 
     override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs)
@@ -28,3 +38,41 @@ class Member(private val element: Term, private val list: List) : Operator(Atom(
 
     override fun toString(): String = "$element ∈ $list"
 }
+
+class Append(private val list1: Term, private val list2: Term, private val list3: Term) :
+    Structure("append", list1, list2, list3) {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        val l1 = applySubstitution(list1, subs)
+        val l2 = applySubstitution(list2, subs)
+        val l3 = applySubstitution(list3, subs)
+
+        if (l1 is Empty) {
+            yieldAll(unifyLazy(l2, l3, subs))
+        }
+
+        val head1 = if (l1 is Cons) l1.head else Variable("Head1")
+        val tail1 = if (l1 is Cons) l1.tail else Variable("Tail1")
+        val head3 = if (l3 is Cons) l3.head else Variable("Head3")
+        val tail3 = if (l3 is Cons) l3.tail else Variable("Tail3")
+
+        unifyLazy(head1, head3, subs).forEach { headResult ->
+            headResult.map { headSubs ->
+                val newSubs = subs + headSubs
+                Append(tail1, list2, tail3).satisfy(newSubs).forEach { tailResult ->
+                    tailResult.map { tailSubs ->
+                        val result = headSubs + tailSubs
+                        yield(Result.success(result))
+                    }
+                }
+            }
+        }
+
+        TODO("This does not return the expected results, especially when using variables for the lists.")
+    }
+
+    override fun applySubstitution(subs: Substitutions): Append = Append(
+        applySubstitution(list1, subs),
+        applySubstitution(list2, subs),
+        applySubstitution(list3, subs)
+    )
+}

src/prolog/builtins/metaOperators.kt

@@ -9,7 +9,7 @@ import prolog.ast.terms.Term
 import prolog.flags.AppliedCut
 import prolog.logic.applySubstitution
 
-class Call(private val goal: Term) : Operator(Atom("call"), null, goal) {
+class Call(private val goal: Term) : Operator("call", rightOperand = goal) {
     override fun satisfy(subs: Substitutions): Answers {
         val appliedGoal = applySubstitution(goal, subs) as Goal
         return appliedGoal.satisfy(subs)
@@ -19,7 +19,7 @@ class Call(private val goal: Term) : Operator(Atom("call"), null, goal) {
 /**
  * Calls [Goal] once, but succeeds, regardless of whether Goal succeeded or not.
  */
-class Ignore(goal: Goal) : Operator(Atom("ignore"), null, goal) {
+class Ignore(goal: Goal) : Operator("ignore", rightOperand = goal) {
     private val disjunction = Disjunction(
         Conjunction(Call(goal), Cut()),
         True

src/prolog/builtins/other.kt

@@ -3,18 +3,15 @@ package prolog.builtins
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
-import prolog.ast.terms.Atom
 import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Goal
-import prolog.ast.terms.Operand
-import prolog.ast.terms.Operator
 
-class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) {
+class Initialization(val goal: LogicOperand) : LogicOperator(":-", rightOperand = goal) {
     override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1)
     override fun toString(): String = goal.toString()
 }
 
-class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
+class Query(val query: LogicOperand) : LogicOperator("?-", rightOperand = query) {
     override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs)
 }
 
@@ -24,7 +21,8 @@ class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
  *
  * @see [SWI-Prolog Predicate forall/2](https://www.swi-prolog.org/pldoc/doc_for?object=forall/2)
  */
-class ForAll(condition: LogicOperand, action: Goal) : Operator(Atom("forall"), condition, action) {
+class ForAll(private val condition: LogicOperand, private val action: Goal) :
-    private val not = Not(Conjunction(condition, Not(action)))
+    Not(Conjunction(condition, Not(action))) {
-    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+    override fun toString() = "forall($condition, $action)"
 }
+

src/prolog/builtins/unificationOperators.kt

@@ -7,7 +7,6 @@ package prolog.builtins
 
 import prolog.Answers
 import prolog.Substitutions
-import prolog.ast.terms.Atom
 import prolog.ast.terms.Operator
 import prolog.ast.terms.Term
 import prolog.logic.applySubstitution
@@ -17,7 +16,7 @@ import prolog.logic.unifyLazy
 /**
  * Unify Term1 with Term2. True if the unification succeeds.
  */
-class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="), term1, term2) {
+class Unify(private val term1: Term, private val term2: Term): Operator("=", term1, term2) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
@@ -31,16 +30,11 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
     )
 }
 
-class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) {
+class NotUnify(private val term1: Term, private val term2: Term) : Not(Unify(term1, term2)) {
-    private val not = Not(Unify(term1, term2))
+    override fun toString(): String = "($term1 \\= $term2)"
-    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
-    override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
 }
 
-class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
+class Equivalent(private val term1: Term, private val term2: Term) : Operator("==", term1, term2) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
@@ -56,11 +50,6 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
     )
 }
 
-class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) {
+class NotEquivalent(private val term1: Term, private val term2: Term) : Not(Equivalent(term1, term2)) {
-    private val not = Not(Equivalent(term1, term2))
+    override fun toString(): String = "($term1 \\== $term2)"
-    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
-    override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
 }

src/prolog/builtins/verificationOperators.kt

@@ -0,0 +1,52 @@
+package prolog.builtins
+
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.terms.Operator
+import prolog.ast.terms.Term
+import prolog.logic.*
+
+class Atomic(private val term: Term) : Operator("atomic", rightOperand = term) {
+    override fun satisfy(subs: Substitutions): Answers {
+        if (atomic(term, subs)) {
+            return sequenceOf(Result.success(emptyMap()))
+        }
+        return emptySequence()
+    }
+
+    override fun applySubstitution(subs: Substitutions): Atomic = Atomic(applySubstitution(term, subs))
+}
+
+class Compound(private val term: Term) : Operator("compound", rightOperand = term) {
+    override fun satisfy(subs: Substitutions): Answers {
+        if (compound(term, subs)) {
+            return sequenceOf(Result.success(emptyMap()))
+        }
+        return emptySequence()
+    }
+
+    override fun applySubstitution(subs: Substitutions): Compound = Compound(applySubstitution(term, subs))
+}
+
+class NonVar(private val term: Term) : Operator("nonvar", rightOperand = term) {
+    override fun satisfy(subs: Substitutions): Answers {
+        if (nonvariable(term, subs)) {
+            return sequenceOf(Result.success(emptyMap()))
+        }
+
+        return emptySequence()
+    }
+
+    override fun applySubstitution(subs: Substitutions): NonVar = NonVar(applySubstitution(term, subs))
+}
+
+class Var(private val term: Term) : Operator("var", rightOperand = term) {
+    override fun satisfy(subs: Substitutions): Answers {
+        if (variable(term, subs)) {
+            return sequenceOf(Result.success(emptyMap()))
+        }
+        return emptySequence()
+    }
+
+    override fun applySubstitution(subs: Substitutions): Var = Var(applySubstitution(term, subs))
+}

src/prolog/logic/terms.kt

@@ -1,29 +1,10 @@
 package prolog.logic
 
 import prolog.Substitutions
-import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
 
-/**
- * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose
- * arguments are all different variables (such a term is called a skeleton). If Term is atomic, Arity will be unified
- * with the integer 0, and Name will be unified with Term. Raises instantiation_error() if Term is unbound and
- * Name/Arity is insufficiently instantiated.
- *
- * SWI-Prolog also supports terms with arity 0, as in a() (see
- * [section 5](https://www.swi-prolog.org/pldoc/man?section=extensions)). Such terms must be processed using functor/4
- * or compound_name_arity/3. The predicate functor/3 and =../2 raise a domain_error when faced with these terms.
- * Without this precaution a round trip of a term with arity 0 over functor/3 would create an atom.
- *
- * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3)
- */
-fun functor(term: Term, name: Atom, arity: Int): Boolean {
-    // TODO Implement
-    return true
-}
-
 /**
  * Unify the free variables in Term with a term $VAR(N), where N is the number of the variable.
  * Counting starts at Start.

tests/interpreter/ParserPreprocessorIntegrationTests.kt

@@ -41,10 +41,7 @@ class ParserPreprocessorIntegrationTests {
             val parsed = parser.parseToEnd("X is $input") as Term
 
             assertEquals(
-                Structure(Atom("is"), listOf(
+                Structure("is", Variable("X"), Structure("-",number)),
-                    Variable("X"),
-                    Structure(Atom("-"), listOf(number)),
-                )),
                 parsed
             )
 
@@ -74,7 +71,7 @@ class ParserPreprocessorIntegrationTests {
             val result = parser.parseToEnd(input) as Term
 
             assertEquals(
-                Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))),
+                Structure("is", Variable("X"), Structure("-", Integer(1), Integer(2))),
                 result
             )
 

tests/interpreter/PreprocessorTests.kt

@@ -37,7 +37,7 @@ class PreprocessorTests {
 
     @Test
     fun `multiple anonymous variables should be unique`() {
-        val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_")))
+        val input = CompoundTerm("foo", Variable("_"), Variable("_"))
 
         val result = preprocessor.preprocess(input)
 
@@ -68,7 +68,7 @@ class PreprocessorTests {
         for (argument in inner.arguments) {
             if ((argument as Variable).name != "Name") {
                 assertTrue(
-                    (argument as Variable).name.matches("_\\d+".toRegex()),
+                    argument.name.matches("_\\d+".toRegex()),
                     "Expected anonymous variable name, but got ${argument.name}"
                 )
             }
@@ -83,27 +83,13 @@ class PreprocessorTests {
             test(
                 mapOf(
                     Atom("=\\=") to Atom("=\\="),
-                    CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()),
+                    CompoundTerm("=\\=") to CompoundTerm("=\\="),
                     Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"),
-                    CompoundTerm(Atom("EvaluatesToDifferent"), emptyList()) to CompoundTerm(
+                    CompoundTerm("EvaluatesToDifferent") to CompoundTerm("EvaluatesToDifferent"),
-                        Atom("EvaluatesToDifferent"),
+                    CompoundTerm("=\\=", Atom("a")) to CompoundTerm("=\\=", Atom("a")),
-                        emptyList()
+                    CompoundTerm("=\\=", Integer(1)) to CompoundTerm("=\\=", Integer(1)),
-                    ),
+                    CompoundTerm("=\\=", Atom("=\\=")) to CompoundTerm("=\\=", Atom("=\\=")),
-                    CompoundTerm(Atom("=\\="), listOf(Atom("a"))) to CompoundTerm(
+                    CompoundTerm("=\\=", Integer(1), Integer(2)) to EvaluatesToDifferent(Integer(1), Integer(2))
-                        Atom("=\\="),
-                        listOf(Atom("a"))
-                    ),
-                    CompoundTerm(Atom("=\\="), listOf(Integer(1))) to CompoundTerm(
-                        Atom("=\\="),
-                        listOf(Integer(1))
-                    ),
-                    CompoundTerm(Atom("=\\="), listOf(Atom("=\\="))) to CompoundTerm(
-                        Atom("=\\="),
-                        listOf(Atom("=\\="))
-                    ),
-                    CompoundTerm(Atom("=\\="), listOf(Integer(1), Integer(2))) to EvaluatesToDifferent(
-                        Integer(1), Integer(2)
-                    )
                 )
             )
         }
@@ -113,7 +99,7 @@ class PreprocessorTests {
             test(
                 mapOf(
                     Atom("=:=") to Atom("=:="),
-                    CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()),
+                    CompoundTerm("=:=") to CompoundTerm("=:="),
                     Atom("EvaluatesTo") to Atom("EvaluatesTo"),
                     CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm(
                         Atom("EvaluatesTo"),

tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt

@@ -12,8 +12,6 @@ import prolog.ast.logic.Rule
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
-import java.io.ByteArrayOutputStream
-import java.io.PrintStream
 
 class DelimitedContinuationsOperatorsTests {
     @BeforeEach

tests/prolog/builtins/ListOperatorsTests.kt

@@ -1,5 +1,6 @@
 package prolog.builtins
 
+import com.sun.source.tree.EmptyStatementTree
 import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.Assertions.assertTrue
 import org.junit.jupiter.api.Disabled
@@ -7,6 +8,7 @@ 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.Term
 import prolog.ast.terms.Variable
 
 class ListOperatorsTests {
@@ -70,4 +72,161 @@ class ListOperatorsTests {
         assertTrue(result[0].isSuccess, "Expected success")
         assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom")
     }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `appended empty lists is an empty list`() {
+        val append = Append(Empty, Empty, Empty)
+
+        val result = append.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")
+    }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `appending two empty lists gives an empty list`() {
+        val list1 = Empty
+        val list2 = Empty
+        val list12 = Variable("Result")
+
+        val append = Append(list1, list2, list12)
+
+        val result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(Empty, subs[list12], "Expected result to be empty list")
+    }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `appending an empty list to another list gives that list`() {
+        val nonempty = Cons(Atom("a"), Empty)
+
+        var append = Append(nonempty, Empty, Empty)
+        var result = append.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")
+
+        append = Append(Empty, nonempty, Empty)
+        result = append.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")
+
+        val variable = Variable("List1AndList2")
+
+        append = Append(Empty, nonempty, variable)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        var subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(nonempty, subs[variable], "Expected result to be nonempty list")
+
+        append = Append(nonempty, Empty, variable)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+    }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `appending two lists gives combined list`() {
+        val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty))
+        val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty))
+        val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty))))
+        val list4 = Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("a"), Cons(Atom("b"), Empty))))
+
+        var append = Append(list1, list2, list3)
+        var result = append.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")
+
+        val variable = Variable("List1AndList2")
+
+        append = Append(list1, list2, variable)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        var subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(list3, subs[variable], "Expected result to be combined list")
+
+        append = Append(list2, list1, variable)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(list4, subs[variable], "Expected result to be combined list")
+    }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `you can find the appended list`() {
+        val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty))
+        val list2: Term = Variable("List2")
+        val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty))))
+
+        var append = Append(list1, list2, list1)
+        var result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        var subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(Empty, subs[list2], "Expected result to be empty list")
+
+        append = Append(list1, list2, list3)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(Cons(Atom("c"), Cons(Atom("d"), Empty)), subs[list2], "Expected result to be list with c and d")
+    }
+
+    @Disabled("Not implemented yet")
+    @Test
+    fun `you can find the prepended list`() {
+        val list1 = Variable("List1")
+        val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty))
+        val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty))))
+
+        var append = Append(list1, list2, list2)
+        var result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        var subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(Empty, subs[list1], "Expected result to be empty list")
+
+        append = Append(list1, list2, list3)
+        result = append.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertEquals(Cons(Atom("a"), Cons(Atom("b"), Empty)), subs[list1], "Expected result to be list with a and b")
+    }
 }

tests/prolog/logic/TermAnalysisConstructionTest.kt

@@ -1,9 +1,9 @@
 package prolog.logic
 
-import org.junit.jupiter.api.Assertions.assertFalse
+import org.junit.jupiter.api.Assertions.*
-import org.junit.jupiter.api.Assertions.assertTrue
 import org.junit.jupiter.api.Test
 import prolog.ast.terms.Atom
+import prolog.ast.terms.Functor
 import prolog.ast.terms.Structure
 
 /**
@@ -19,12 +19,12 @@ class TermAnalysisConstructionTest {
         assertTrue(atomic(atom))
         assertFalse(compound(atom))
 
-        assertTrue(functor(atom, Atom("foo"), 0))
+        assertEquals(Functor("foo", 0), atom.functor)
     }
 
     @Test
     fun compound_arity_0_properties() {
-        val structure = Structure(Atom("foo"), emptyList())
+        val structure = Structure("foo")
 
         assertFalse(atomic(structure))
         assertTrue(compound(structure))
@@ -32,11 +32,11 @@ class TermAnalysisConstructionTest {
 
     @Test
     fun compound_arity_1_properties() {
-        val structure = Structure(Atom("foo"), listOf(Atom("bar")))
+        val structure = Structure("foo", Atom("bar"))
 
         assertFalse(atomic(structure))
         assertTrue(compound(structure))
 
-        assertTrue(functor(structure, Atom("foo"), 1))
+        assertEquals(Functor("foo", 1), structure.functor)
     }
 }