Clause

src/interpreter/Preprocessor.kt

@@ -48,70 +48,93 @@ open class Preprocessor {
     }
 
     protected open fun preprocess(term: Term, nested: Boolean = false): Term {
-        val prepped = when (term) {
-            Atom("true") -> True
-            Structure(Atom("true"), emptyList()) -> True
-            Atom("false") -> False
-            Structure(Atom("false"), emptyList()) -> False
-            Atom("fail") -> Fail
-            Structure(Atom("fail"), emptyList()) -> Fail
-            Atom("!") -> Cut()
-            Structure(Atom("!"), emptyList()) -> Cut()
-            Atom("inf") -> Integer(Int.MAX_VALUE)
-            Atom("nl") -> Nl
-            Variable("_") -> AnonymousVariable.create()
-            is Structure -> {
-                // Preprocess the arguments first to recognize builtins
-                val args = term.arguments.map { preprocess(it, nested = true) }
-
-                when {
         // TODO Remove hardcoding by storing the functors as constants in operators?
 
-                    term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body )
+        val prepped = when {
+            term == Variable("_") -> AnonymousVariable.create()
+            term is Atom || term is Structure -> {
+                // Preprocess the arguments first to recognize builtins
+                val args = if (term is Structure) {
+                    term.arguments.map { preprocess(it, nested = true) }
+                } else emptyList()
 
-                    // Logic
+                when (term.functor) {
-                    term.functor == "=/2" -> Unify(args[0], args[1])
+                    // Analysis
-                    term.functor == "\\=/2" -> NotUnify(args[0], args[1])
+                    Functor.of("functor/3") -> FunctorOp(args[0], args[1], args[2])
-                    term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    Functor.of("arg/3") -> Arg(args[0], args[1], args[2])
-                    term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body)
-                    term.functor == "\\+/1" -> Not(args[0] as Goal)
-                    term.functor == "\\==/2" -> NotEquivalent(args[0], args[1])
-                    term.functor == "==/2" -> Equivalent(args[0], args[1])
-
-                    term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
-                    term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
-                    term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
 
                     // Arithmetic
+                    Functor.of("inf/0") -> Integer(Int.MAX_VALUE)
+                    Functor.of("=\\=/2") -> if (args.all { it is Expression }) {
+                        EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
+                    } else term
 
-                    term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression)
+                    Functor.of("=:=/2") -> if (args.all { it is Expression }) {
-                    term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
+                        EvaluatesTo(args[0] as Expression, args[1] as Expression)
-                    term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression)
+                    } else term
-                    term.functor == "+/2" && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression)
+
-                    term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
+                    Functor.of("is/2") -> if (args.all { it is Expression }) {
-                    term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
+                        Is(args[0] as Expression, args[1] as Expression)
-                    term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
+                    } else term
-                    term.functor == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
+
+                    Functor.of("-/1") -> if (args.all { it is Expression }) Negate(args[0] as Expression) else term
+                    Functor.of("+/1") -> if (args.all { it is Expression }) Positive(args[0] as Expression) else term
+                    Functor.of("+/2") -> if (args.all { it is Expression }) {
+                        Add(args[0] as Expression, args[1] as Expression)
+                    } else term
+
+                    Functor.of("-/2") -> if (args.all { it is Expression }) {
+                        Subtract(args[0] as Expression, args[1] as Expression)
+                    } else term
+
+                    Functor.of("*/2") -> if (args.all { it is Expression }) {
+                        Multiply(args[0] as Expression, args[1] as Expression)
+                    } else term
+
+                    Functor.of("//2") -> if (args.all { it is Expression }) {
+                        Divide(args[0] as Expression, args[1] as Expression)
+                    } else term
+
+                    Functor.of("between/3") -> if (args.all { it is Expression }) {
+                        Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
+                    } else term
+
+                    Functor.of("succ/2") -> if (args.all { it is Expression }) {
+                        Successor(args[0] as Expression, args[1] as Expression)
+                    } else term
+
+                    // Control
+                    Functor.of("fail/0") -> Fail
+                    Functor.of("false/0") -> False
+                    Functor.of("true/0") -> True
+                    Functor.of("!/0") -> Cut()
+                    Functor.of(",/2") -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    Functor.of(";/2") -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    Functor.of("|/2") -> Bar(args[0] as LogicOperand, args[1] as LogicOperand)
+                    Functor.of("\\+/1") -> Not(args[0] as Goal)
 
                     // Database
-                    term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
+                    Functor.of("dynamic/1") -> Dynamic(Functor.of((args[0] as Atom).name))
-                    term.functor == "retract/1" -> Retract(args[0])
+                    Functor.of("retract/1") -> Retract(args[0])
-                    term.functor == "retractall/1" -> RetractAll(args[0])
+                    Functor.of("retractall/1") -> RetractAll(args[0])
-                    term.functor == "assert/1" -> {
+                    Functor.of("assert/1") -> {
                         if (args[0] is Rule) {
                             Assert(args[0] as Rule)
                         } else {
                             Assert(Fact(args[0] as Head))
                         }
                     }
-                    term.functor == "asserta/1" -> {
+
+                    Functor.of("asserta/1") -> {
                         if (args[0] is Rule) {
                             AssertA(args[0] as Rule)
                         } else {
                             AssertA(Fact(args[0] as Head))
                         }
                     }
-                    term.functor == "assertz/1" -> {
+
+                    Functor.of("assertz/1") -> {
                         if (args[0] is Rule) {
                             AssertZ(args[0] as Rule)
                         } else {
@@ -119,14 +142,25 @@ open class Preprocessor {
                         }
                     }
 
+                    // IO
+                    Functor.of("write/1") -> Write(args[0])
+                    Functor.of("nl/0") -> Nl
+                    Functor.of("read/1") -> Read(args[0])
+
                     // Other
-                    term.functor == "write/1" -> Write(args[0])
+                    Functor.of("initialization/1") -> Initialization(args[0] as Goal)
-                    term.functor == "read/1" -> Read(args[0])
+                    Functor.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal)
-                    term.functor == "initialization/1" -> Initialization(args[0] as Goal)
+
-                    term.functor == "forall/2" -> ForAll(args[0] as LogicOperand, args[1] as Goal)
+                    // Unification
+                    Functor.of("=/2") -> Unify(args[0], args[1])
+                    Functor.of("\\=/2") -> NotUnify(args[0], args[1])
+                    Functor.of("==/2") -> Equivalent(args[0], args[1])
+                    Functor.of("\\==/2") -> NotEquivalent(args[0], args[1])
+
+                    Functor.of(":-/2") -> Rule(args[0] as Head, args[1] as Body)
 
                     else -> {
-                        term.arguments = args
+                        if (term is Structure) term.arguments = args
                         term
                     }
                 }

src/prolog/ast/Database.kt

@@ -23,14 +23,14 @@ open class Database(val sourceFile: String) {
 
         if (sourceFile !== "") {
             Logger.debug("Moving clauses from $sourceFile to main database")
-            predicates.filter { it.key != "/_" }
+            predicates.filter { it.key != Functor.of("/_") }
                 .forEach { (_, predicate) -> db.load(predicate, force = true) }
         }
 
         Logger.info("Initializing database from $sourceFile")
-        if (predicates.contains("/_")) {
+        if (predicates.contains(Functor.of("/_"))) {
             Logger.debug("Loading clauses from /_ predicate")
-            predicates["/_"]?.clauses?.forEach {
+            predicates[Functor.of("/_")]?.clauses?.forEach {
                 Logger.debug("Loading clause $it")
                 val goal = it.body as Goal
                 goal.satisfy(emptyMap()).toList()

src/prolog/ast/logic/Clause.kt

@@ -1,8 +1,8 @@
 package prolog.ast.logic
 
 import prolog.Answers
-import prolog.ast.Database.Program
 import prolog.Substitutions
+import prolog.ast.Database.Program
 import prolog.ast.terms.*
 import prolog.builtins.True
 import prolog.flags.AppliedCut
@@ -45,7 +45,14 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
                         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) } }
+                            val headResult = headToGoalSubs.filterKeys { key ->
+                                goalToHeadSubs.any {
+                                    occurs(
+                                        key as Variable,
+                                        it.value
+                                    )
+                                }
+                            }
                             yield(Result.success(goalToHeadResult + headResult))
                         },
                         onFailure = { error ->

src/prolog/ast/terms/Atom.kt

@@ -4,9 +4,10 @@ import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Resolvent
 import prolog.logic.unifyLazy
+import prolog.ast.arithmetic.Integer
 
 open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
-    override val functor: Functor = "$name/_"
+    override val functor: Functor = Functor(this, Integer(0))
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 

src/prolog/ast/terms/Functor.kt

@@ -0,0 +1,35 @@
+package prolog.ast.terms
+
+import prolog.Substitutions
+import prolog.ast.arithmetic.Integer
+
+data class Functor(val name: Atom, val arity: Integer) : Term {
+    companion object {
+        fun of(functor: String): Functor {
+            // Split the functor string into name and arity, by splitting the last "/"
+            val lastSlash = functor.lastIndexOf('/')
+            val name = Atom(functor.substring(0, lastSlash))
+            val arity = Integer(functor.substring(lastSlash + 1).toIntOrNull() ?: 0)
+            return Functor(name, arity)
+        }
+    }
+
+    override fun toString(): String = "${name.name}/$arity"
+    override fun applySubstitution(subs: Substitutions) : Functor = this
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other == null) return false
+        if (other !is Functor && other !is String) return false
+        if (other is Functor) {
+            return this.name.toString() == other.name.toString() && this.arity == other.arity
+        }
+        return this.toString() == other
+    }
+
+    override fun hashCode(): Int {
+        var result = name.hashCode()
+        result = 31 * result + arity.hashCode()
+        return result
+    }
+}

src/prolog/ast/terms/Goal.kt

@@ -1,8 +1,8 @@
 package prolog.ast.terms
 
 import prolog.Answers
-import prolog.ast.Database.Program
 import prolog.Substitutions
+import prolog.ast.Database.Program
 import prolog.ast.logic.LogicOperand
 
 /**

src/prolog/ast/terms/Head.kt

@@ -6,5 +6,3 @@ package prolog.ast.terms
 interface Head : Term {
     val functor: Functor
 }
-
-typealias Functor = String

src/prolog/ast/terms/Structure.kt

@@ -5,13 +5,14 @@ import prolog.Substitutions
 import prolog.ast.logic.Resolvent
 import prolog.logic.applySubstitution
 import prolog.logic.unifyLazy
+import prolog.ast.arithmetic.Integer
 
 typealias Argument = Term
 
 typealias CompoundTerm = Structure
 
 open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
-    override val functor: Functor = "${name.name}/${arguments.size}"
+    override val functor: Functor = Functor(name, Integer(arguments.size))
 
     override fun solve(goal: Goal, subs: Substitutions): Answers {
         return unifyLazy(goal, this, subs)

src/prolog/builtins/analysisOperators.kt

@@ -0,0 +1,139 @@
+package prolog.builtins
+
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.Database.Program
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.*
+import prolog.ast.logic.Clause
+import prolog.logic.*
+
+/**
+ * [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.
+ * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term.
+ */
+class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) :
+    Structure(Atom("functor"), listOf(term, functorName, functorArity)) {
+    override fun satisfy(subs: Substitutions): Answers {
+        return when {
+            nonvariable(term, subs) -> {
+                val t = applySubstitution(term, subs) as Head
+
+                Conjunction(
+                    Unify(t.functor.arity, functorArity),
+                    Unify(t.functor.name, functorName)
+                ).satisfy(subs)
+            }
+
+            variable(term, subs) -> {
+                require(atomic(functorName, subs) && atomic(functorArity, subs)) {
+                    "Arguments are not sufficiently instantiated"
+                }
+
+                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)))
+            }
+
+            else -> throw IllegalStateException()
+        }
+    }
+
+    override fun applySubstitution(subs: Substitutions): FunctorOp = FunctorOp(
+        term.applySubstitution(subs),
+        functorName.applySubstitution(subs),
+        functorArity.applySubstitution(subs)
+    )
+}
+
+class Arg(private val arg: Term, private val term: Term, private val value: Term) :
+    Structure(Atom("arg"), listOf(arg, term, value)) {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" }
+        require(compound(term, subs)) {
+            val expected = CompoundTerm::class.simpleName?.lowercase()
+            val actual = term::class.simpleName?.lowercase()
+            "Type error: `$expected' expected, found `$term' ($actual)"
+        }
+
+        val t = applySubstitution(term, subs) as Structure
+
+        when {
+            variable(arg, subs) -> {
+                // 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) {
+                    unifyLazy(value, argument, subs).forEach { result ->
+                        result.map {
+                            val sub = arg to Integer(count + 1)
+                            yield(Result.success(it + sub))
+                        }
+                    }
+                    count++
+                }
+
+            }
+
+            else -> {
+                val a = applySubstitution(arg, subs) as Integer
+
+                require(0 <= a.value) { "Domain error: not_less_than_zero" }
+
+                // Fail silently if the argument is out of bounds
+                if (0 == a.value || t.arguments.size < a.value) {
+                    return@sequence
+                }
+
+                val argument = t.arguments[a.value - 1]
+                yieldAll(unifyLazy(argument, value, subs))
+            }
+        }
+    }
+}
+
+/**
+ * [True] if [Head] can be unified with a [Clause] and [Body] with the corresponding Clause Body.
+ *
+ * Gives alternative clauses on backtracking. For facts, Body is unified with the atom [True].
+ *
+ * When accessing builtins (static predicates, private procedures), the program will act as if the builtins do not
+ * exist. Head can only match with dynamic or imported predicates.
+ *
+ * [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)) {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" }
+
+        val predicate = Program.db.predicates[head.functor]
+
+        if (predicate != null) {
+            for (clause in predicate.clauses) {
+                val clauseHead = clause.head
+                val clauseBody = clause.body
+
+                // Unify the head of the clause with the head of the goal
+                unifyLazy(clauseHead, head, subs).forEach { result ->
+                    result.map { headSubs ->
+                        // Unify the body of the clause with the body of the goal
+                        unifyLazy(clauseBody, body, headSubs).forEach { bodyResult ->
+                            bodyResult.map { bodySubs ->
+                                // Combine the substitutions from the head and body
+                                val combinedSubs = headSubs + bodySubs
+                                yield(Result.success(combinedSubs))
+                            }
+                        }
+                    }
+                }
+            }
+        } else {
+            yield(Result.success(emptyMap()))
+        }
+    }
+}

src/prolog/builtins/databaseOperators.kt

@@ -3,26 +3,21 @@ package prolog.builtins
 import io.Logger
 import prolog.Answers
 import prolog.Substitutions
-import prolog.ast.logic.Clause
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.logic.Predicate
-import prolog.ast.Database.Program
-import prolog.ast.terms.Functor
-import prolog.ast.terms.Term
-import prolog.ast.logic.Fact
 import prolog.ast.Database
-import prolog.ast.terms.Body
+import prolog.ast.Database.Program
-import prolog.ast.terms.Goal
+import prolog.ast.arithmetic.Integer
-import prolog.ast.terms.Operator
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Fact
+import prolog.ast.logic.Predicate
+import prolog.ast.terms.*
 import prolog.logic.applySubstitution
 import prolog.logic.unifyLazy
 
 /**
  * (Make) the [Predicate] with the corresponding [Functor] dynamic.
  */
-class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
+class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body {
-    override val functor: Functor = "dynamic/1"
+    override val functor = Functor(Atom("dynamic"), Integer(1))
 
     override fun satisfy(subs: Substitutions): Answers {
         val predicate = Program.db.predicates[dynamicFunctor]
@@ -48,7 +43,7 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
 }
 
 class Assert(clause: Clause) : AssertZ(clause) {
-    override val functor: Functor = "assert/1"
+    override val functor = Functor(Atom("assert"), Integer(1))
 }
 
 /**

tests/interpreter/PreprocessorTests.kt

@@ -6,7 +6,6 @@ import org.junit.jupiter.api.Nested
 import org.junit.jupiter.api.Test
 import parser.grammars.TermsGrammar
 import prolog.ast.arithmetic.Integer
-import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
 import prolog.ast.terms.*
 import prolog.builtins.*
@@ -612,7 +611,7 @@ class PreprocessorTests {
                     Atom("declaration/1")
                 )
             )
-            val expected = Dynamic("declaration/1")
+            val expected = Dynamic(Functor.of("declaration/1"))
 
             val result = preprocessor.preprocess(input)
 

tests/parser/grammars/LogicGrammarTests.kt

@@ -2,7 +2,6 @@ package parser.grammars
 
 import com.github.h0tk3y.betterParse.grammar.Grammar
 import com.github.h0tk3y.betterParse.grammar.parseToEnd
-import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
@@ -14,7 +13,7 @@ import prolog.ast.logic.Rule
 import prolog.ast.terms.CompoundTerm
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
-import prolog.builtins.Conjunction
+import prolog.ast.terms.Functor
 
 class LogicGrammarTests {
     private lateinit var parser: Grammar<List<Clause>>
@@ -94,13 +93,13 @@ class LogicGrammarTests {
 
         assertTrue(rule.head is Structure, "Expected head to be a structure")
         val head = rule.head as Structure
-        assertEquals("parent/2", head.functor, "Expected functor 'parent/2'")
+        assertEquals(Functor.of("parent/2"), head.functor, "Expected functor 'parent/2'")
         assertEquals(Variable("X"), head.arguments[0], "Expected first argument 'X'")
         assertEquals(Variable("Y"), head.arguments[1], "Expected second argument 'Y'")
 
         assertTrue(rule.body is Structure, "Expected body to be a structure")
         val body = rule.body as Structure
-        assertEquals("father/2", body.functor, "Expected functor 'father/2'")
+        assertEquals(Functor.of("father/2"), body.functor, "Expected functor 'father/2'")
         assertEquals(Variable("X"), body.arguments[0], "Expected first argument 'X'")
         assertEquals(Variable("Y"), body.arguments[1], "Expected second argument 'Y'")
     }
@@ -125,12 +124,12 @@ class LogicGrammarTests {
 
         assertEquals(1, result.size, "Expected 1 rule")
         val rule = result[0] as Rule
-        assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'")
+        assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'")
-        assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
+        assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
         val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm
-        assertEquals(",/2", l1.functor, "Expected functor ',/2'")
+        assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'")
         val l2 = l1.arguments[0] as CompoundTerm
-        assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'")
+        assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'")
     }
 
     @Test
@@ -157,6 +156,6 @@ class LogicGrammarTests {
         assertEquals(1, result.size, "Expected 1 rule")
         assertTrue(result[0] is Rule, "Expected a rule")
         val rule = result[0] as Rule
-        assertEquals("/_", rule.head.functor, "Expected a constraint")
+        assertEquals(Functor.of("/0"), rule.head.functor, "Expected a constraint")
     }
 }

tests/prolog/builtins/AnalysisOperatorsTests.kt

@@ -0,0 +1,404 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Nested
+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.logic.Fact
+import prolog.ast.logic.Rule
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.AnonymousVariable
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
+
+class AnalysisOperatorsTests {
+    @Test
+    fun `functor(foo, foo, 0)`() {
+        val functor = FunctorOp(Atom("foo"), Atom("foo"), Integer(0))
+
+        val result = functor.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions")
+    }
+
+    @Test
+    fun `functor(foo(X), foo, Y)`() {
+        val functor = FunctorOp(
+            Structure(Atom("foo"), listOf(Variable("X"))),
+            Atom("foo"),
+            Variable("Y")
+        )
+
+        val result = functor.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(Integer(1), subs[Variable("Y")])
+    }
+
+    @Test
+    fun `functor(foo, X, Y)`() {
+        val atom = Atom("foo")
+        val functor = FunctorOp(atom, Variable("X"), Variable("Y"))
+
+        val result = functor.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(2, subs.size, "Expected 2 substitutions")
+        assertEquals(atom.functor.name, subs[Variable("X")])
+        assertEquals(atom.functor.arity, subs[Variable("Y")])
+    }
+
+    @Test
+    fun `functor(X, foo, 1)`() {
+        val functor = FunctorOp(Variable("X"), Atom("foo"), Integer(1))
+
+        val result = functor.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")
+        assertInstanceOf(Structure::class.java, subs[Variable("X")])
+        val structure = subs[Variable("X")] as Structure
+        assertEquals(Atom("foo"), structure.name)
+        assertEquals(1, structure.arguments.size)
+        assertInstanceOf(AnonymousVariable::class.java, structure.arguments[0])
+    }
+
+    @Test
+    fun `functor(foo(a), foo, 0)`() {
+        val functor = FunctorOp(Structure(Atom("foo"), listOf(Atom("a"))), Atom("foo"), Integer(0))
+
+        val result = functor.satisfy(emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "Expected no results")
+    }
+
+    @Test
+    fun `functor(foo(X), foo, 0)`() {
+        val functor = FunctorOp(Structure(Atom("foo"), listOf(Variable("X"))), Atom("foo"), Integer(0))
+
+        val result = functor.satisfy(emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "Expected no results")
+    }
+
+    @Test
+    fun `functor(X, Y, 1)`() {
+        val functor = FunctorOp(Variable("X"), Variable("Y"), Integer(1))
+
+        val exception = assertThrows<Exception> {
+            functor.satisfy(emptyMap()).toList()
+        }
+        assertEquals("Arguments are not sufficiently instantiated", exception.message)
+    }
+
+    @Test
+    fun `arg without variables`() {
+        val arg = Arg(
+            Integer(1),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Atom("a")
+        )
+
+        val result = arg.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 no substitutions")
+    }
+
+    @Test
+    fun `arg with variable value`() {
+        val arg = Arg(
+            Integer(1),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Variable("Term")
+        )
+
+        val result = arg.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("a"), subs[Variable("Term")])
+    }
+
+    @Test
+    fun `arg with variable arg`() {
+        val arguments = listOf(Atom("a"), Atom("b"), Atom("c"))
+        for (i in arguments.indices) {
+            val arg = Arg(
+                Variable("Arg"),
+                Structure(Atom("f"), arguments),
+                arguments[i]
+            )
+
+            val result = arg.satisfy(emptyMap()).toList()
+
+            assertEquals(1, result.size, "Expected 1 result for arg $i")
+            assertTrue(result[0].isSuccess, "Expected success for arg $i")
+            val subs = result[0].getOrNull()!!
+            assertEquals(1, subs.size, "Expected 1 substitution for arg $i")
+            assertEquals(Integer(i + 1), subs[Variable("Arg")], "Expected arg to be $i + 1")
+        }
+    }
+
+    @Test
+    fun `arg with backtracking`() {
+        val arg = Arg(
+            Variable("Position"),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Variable("Term")
+        )
+
+        val result = arg.satisfy(emptyMap()).toList()
+
+        assertEquals(3, result.size, "Expected 3 results")
+
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs1 = result[0].getOrNull()!!
+        assertEquals(2, subs1.size, "Expected 2 substitutions")
+        assertEquals(Integer(1), subs1[Variable("Position")])
+        assertEquals(Atom("a"), subs1[Variable("Term")])
+
+        assertTrue(result[1].isSuccess, "Expected success")
+        val subs2 = result[1].getOrNull()!!
+        assertEquals(2, subs2.size, "Expected 2 substitutions")
+        assertEquals(Integer(2), subs2[Variable("Position")])
+        assertEquals(Atom("b"), subs2[Variable("Term")])
+
+        assertTrue(result[2].isSuccess, "Expected success")
+        val subs3 = result[2].getOrNull()!!
+        assertEquals(2, subs3.size, "Expected 2 substitutions")
+        assertEquals(Integer(3), subs3[Variable("Position")])
+        assertEquals(Atom("c"), subs3[Variable("Term")])
+    }
+
+    @Test
+    fun `arg raises error if Arg is not compound`() {
+        val arg = Arg(Integer(1), Atom("foo"), Variable("X"))
+
+        val exception = assertThrows<IllegalArgumentException> {
+            arg.satisfy(emptyMap()).toList()
+        }
+        assertEquals("Type error: `structure' expected, found `foo' (atom)", exception.message)
+    }
+
+    @Test
+    fun `arg fails silently if arg = 0`() {
+        val arg = Arg(
+            Integer(0),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Variable("Term")
+        )
+
+        val result = arg.satisfy(emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "Expected no results")
+    }
+
+    @Test
+    fun `arg fails silently if arg gt arity`() {
+        val arg = Arg(
+            Integer(4),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Variable("Term")
+        )
+
+        val result = arg.satisfy(emptyMap()).toList()
+
+        assertTrue(result.isEmpty(), "Expected no results")
+    }
+
+    @Test
+    fun `arg raises error if arg lt 0`() {
+        val arg = Arg(
+            Integer(-1),
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
+            Variable("Term")
+        )
+
+        val exception = assertThrows<IllegalArgumentException> {
+            arg.satisfy(emptyMap()).toList()
+        }
+        assertEquals("Domain error: not_less_than_zero", exception.message)
+    }
+
+    @Nested
+    class `Clause operator` {
+        @BeforeEach
+        fun setup() {
+            Program.reset()
+        }
+
+        @Test
+        fun `clause fact atom without variables`() {
+            Program.load(listOf(Fact(Atom("foo"))))
+
+            val result = ClauseOp(
+                Atom("foo"),
+                True
+            ).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 `clause fact compound without variables`() {
+            Program.load(
+                listOf(
+                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))))
+                )
+            )
+
+            val result = ClauseOp(
+                CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))),
+                True
+            ).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 `clause rule without variables`() {
+            Program.load(listOf(Rule(Atom("foo"), Atom("bar"))))
+
+            val result = ClauseOp(
+                Atom("foo"),
+                Atom("bar")
+            ).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 `clause fact variable body`() {
+            Program.load(listOf(Fact(Atom("foo"))))
+
+            val variable = Variable("Term")
+            val result = ClauseOp(
+                Atom("foo"),
+                variable
+            ).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(True, subs[variable])
+        }
+
+        @Test
+        fun `clause fact with variable head`() {
+            Program.load(
+                listOf(
+                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"))))
+                )
+            )
+
+            val result = ClauseOp(
+                CompoundTerm(Atom("foo"), listOf(Variable("X"))),
+                True
+            ).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("a"), subs[Variable("X")])
+        }
+
+        @Test
+        fun `clause rule with variable body`() {
+            Program.load(listOf(Rule(Atom("foo"), Atom("bar"))))
+
+            val result = ClauseOp(
+                Atom("foo"),
+                Variable("Term")
+            ).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("bar"), subs[Variable("Term")])
+        }
+
+        @Test
+        fun `clause fact variable value with backtracking`() {
+            Program.load(
+                listOf(
+                    Fact(CompoundTerm(Atom("bar"), listOf(Atom("d")))),
+                    Fact(CompoundTerm(Atom("bar"), listOf(Atom("e")))),
+                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))),
+                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))),
+                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("c")))),
+                    Rule(
+                        CompoundTerm(Atom("foo"), listOf(Variable("X"))),
+                        CompoundTerm(Atom("bar"), listOf(Variable("X")))
+                    )
+                )
+            )
+
+            val x = Variable("X")
+            val term = Variable("Term")
+
+            val result = ClauseOp(
+                CompoundTerm(Atom("foo"), listOf(x)),
+                term
+            ).satisfy(emptyMap()).toList()
+
+            assertEquals(4, result.size, "Expected 4 results")
+
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs1 = result[0].getOrNull()!!
+            assertEquals(2, subs1.size, "Expected 2 substitutions")
+            assertEquals(Atom("a"), subs1[x], "Expected a")
+            assertEquals(True, subs1[term], "Expected True")
+
+            assertTrue(result[1].isSuccess, "Expected success")
+            val subs2 = result[1].getOrNull()!!
+            assertEquals(2, subs2.size, "Expected 2 substitutions")
+            assertEquals(Atom("b"), subs2[x], "Expected b")
+            assertEquals(True, subs2[term], "Expected True")
+
+            assertTrue(result[2].isSuccess, "Expected success")
+            val subs3 = result[2].getOrNull()!!
+            assertEquals(2, subs3.size, "Expected 2 substitutions")
+            assertEquals(Atom("c"), subs3[x], "Expected c")
+            assertEquals(True, subs3[term], "Expected True")
+
+            assertTrue(result[3].isSuccess, "Expected success")
+            val subs4 = result[3].getOrNull()!!
+            assertEquals(1, subs4.size, "Expected 2 substitutions")
+            assertEquals(
+                CompoundTerm(Atom("bar"), listOf(Variable("X"))),
+                subs4[term],
+                "Expected bar(X)"
+            )
+        }
+    }
+}

tests/prolog/builtins/DatabaseOperatorsTests.kt

@@ -8,7 +8,6 @@ import org.junit.jupiter.api.Nested
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ValueSource
-import prolog.ast.Database
 import prolog.ast.Database.Program
 import prolog.ast.logic.Clause
 import prolog.ast.logic.Fact
@@ -40,7 +39,7 @@ class DatabaseOperatorsTests {
             createAssert(fact).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0])
+            assertEquals(fact, Program.db.predicates[Functor.of("a/_")]!!.clauses[0])
         }
 
         @Test
@@ -49,7 +48,7 @@ class DatabaseOperatorsTests {
             createAssert(fact).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(fact, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
         }
 
         @Test
@@ -61,7 +60,7 @@ class DatabaseOperatorsTests {
             createAssert(rule).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
         }
     }
 
@@ -92,8 +91,8 @@ class DatabaseOperatorsTests {
             AssertA(rule2).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
-            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1])
+            assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[1])
         }
     }
 
@@ -117,8 +116,8 @@ class DatabaseOperatorsTests {
             AssertZ(rule2).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
-            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1])
+            assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1])
         }
     }
 
@@ -309,20 +308,20 @@ class DatabaseOperatorsTests {
 
         val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
         assertEquals(3, control.size, "Expected 3 results")
-        assertEquals(3, Program.db.predicates["a/1"]!!.clauses.size, "Expected 3 clauses")
+        assertEquals(3, Program.db.predicates[Functor.of("a/1")]!!.clauses.size, "Expected 3 clauses")
 
         val retract = RetractAll(Structure(Atom("a"), listOf(Variable("X"))))
         val result = retract.satisfy(emptyMap()).toList()
 
         assertEquals(1, result.size, "Expected 1 result")
         assertTrue(result[0].isSuccess, "Expected success")
-        assertEquals(0, Program.db.predicates["a/1"]!!.clauses.size, "Expected 0 clauses")
+        assertEquals(0, Program.db.predicates[Functor.of("a/1")]!!.clauses.size, "Expected 0 clauses")
     }
 
     @Test
     fun `If Head refers to a predicate that is not defined, it is implicitly created as a dynamic predicate`() {
         val predicateName = "idonotyetexist"
-        val predicateFunctor = "$predicateName/1"
+        val predicateFunctor = Functor.of("$predicateName/1")
 
         assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")