src/interpreter/Preprocessor.kt

@@ -48,93 +48,70 @@ 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?
 
-        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()
+                    term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body )
 
-                when (term.functor) {
-                    // Analysis
-                    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)
+                    // Logic
+                    term.functor == "=/2" -> Unify(args[0], args[1])
+                    term.functor == "\\=/2" -> NotUnify(args[0], args[1])
+                    term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    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
 
-                    Functor.of("=:=/2") -> if (args.all { it is Expression }) {
-                        EvaluatesTo(args[0] as Expression, args[1] as Expression)
-                    } else term
-
-                    Functor.of("is/2") -> if (args.all { it is Expression }) {
-                        Is(args[0] as Expression, args[1] as Expression)
-                    } else term
-
-                    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)
+                    term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression)
+                    term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
+                    term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression)
+                    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)
+                    term.functor == "//2" && args.all { it is Expression } -> Divide(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)
+                    term.functor == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
 
                     // Database
-                    Functor.of("dynamic/1") -> Dynamic(Functor.of((args[0] as Atom).name))
-                    Functor.of("retract/1") -> Retract(args[0])
-                    Functor.of("retractall/1") -> RetractAll(args[0])
-                    Functor.of("assert/1") -> {
+                    term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
+                    term.functor == "retract/1" -> Retract(args[0])
+                    term.functor == "retractall/1" -> RetractAll(args[0])
+                    term.functor == "assert/1" -> {
                         if (args[0] is Rule) {
                             Assert(args[0] as Rule)
                         } else {
                             Assert(Fact(args[0] as Head))
                         }
                     }
-
-                    Functor.of("asserta/1") -> {
+                    term.functor == "asserta/1" -> {
                         if (args[0] is Rule) {
                             AssertA(args[0] as Rule)
                         } else {
                             AssertA(Fact(args[0] as Head))
                         }
                     }
-
-                    Functor.of("assertz/1") -> {
+                    term.functor == "assertz/1" -> {
                         if (args[0] is Rule) {
                             AssertZ(args[0] as Rule)
                         } else {
@@ -142,25 +119,14 @@ open class Preprocessor {
                         }
                     }
 
-                    // IO
-                    Functor.of("write/1") -> Write(args[0])
-                    Functor.of("nl/0") -> Nl
-                    Functor.of("read/1") -> Read(args[0])
-
                     // Other
-                    Functor.of("initialization/1") -> Initialization(args[0] as Goal)
-                    Functor.of("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)
+                    term.functor == "write/1" -> Write(args[0])
+                    term.functor == "read/1" -> Read(args[0])
+                    term.functor == "initialization/1" -> Initialization(args[0] as Goal)
+                    term.functor == "forall/2" -> ForAll(args[0] as LogicOperand, args[1] as Goal)
 
                     else -> {
-                        if (term is Structure) term.arguments = args
+                        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 != Functor.of("/_") }
+            predicates.filter { it.key != "/_" }
                 .forEach { (_, predicate) -> db.load(predicate, force = true) }
         }
 
         Logger.info("Initializing database from $sourceFile")
-        if (predicates.contains(Functor.of("/_"))) {
+        if (predicates.contains("/_")) {
             Logger.debug("Loading clauses from /_ predicate")
-            predicates[Functor.of("/_")]?.clauses?.forEach {
+            predicates["/_"]?.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.Substitutions
 import prolog.ast.Database.Program
+import prolog.Substitutions
 import prolog.ast.terms.*
 import prolog.builtins.True
 import prolog.flags.AppliedCut
@@ -45,14 +45,7 @@ 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,10 +4,9 @@ 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 = Functor(this, Integer(0))
+    override val functor: Functor = "$name/_"
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 

src/prolog/ast/terms/Functor.kt

@@ -1,35 +0,0 @@
-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.Substitutions
 import prolog.ast.Database.Program
+import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
 
 /**

src/prolog/ast/terms/Head.kt

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

src/prolog/ast/terms/Structure.kt

@@ -5,14 +5,13 @@ 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 = Functor(name, Integer(arguments.size))
+    override val functor: Functor = "${name.name}/${arguments.size}"
 
     override fun solve(goal: Goal, subs: Substitutions): Answers {
         return unifyLazy(goal, this, subs)

src/prolog/builtins/analysisOperators.kt

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

tests/interpreter/PreprocessorTests.kt

@@ -6,6 +6,7 @@ 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.*
@@ -611,7 +612,7 @@ class PreprocessorTests {
                     Atom("declaration/1")
                 )
             )
-            val expected = Dynamic(Functor.of("declaration/1"))
+            val expected = Dynamic("declaration/1")
 
             val result = preprocessor.preprocess(input)
 

tests/parser/grammars/LogicGrammarTests.kt

@@ -2,6 +2,7 @@ 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
@@ -13,7 +14,7 @@ import prolog.ast.logic.Rule
 import prolog.ast.terms.CompoundTerm
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
-import prolog.ast.terms.Functor
+import prolog.builtins.Conjunction
 
 class LogicGrammarTests {
     private lateinit var parser: Grammar<List<Clause>>
@@ -93,13 +94,13 @@ class LogicGrammarTests {
 
         assertTrue(rule.head is Structure, "Expected head to be a structure")
         val head = rule.head as Structure
-        assertEquals(Functor.of("parent/2"), head.functor, "Expected functor 'parent/2'")
+        assertEquals("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(Functor.of("father/2"), body.functor, "Expected functor 'father/2'")
+        assertEquals("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'")
     }
@@ -124,12 +125,12 @@ class LogicGrammarTests {
 
         assertEquals(1, result.size, "Expected 1 rule")
         val rule = result[0] as Rule
-        assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'")
-        assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
+        assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'")
+        assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
         val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm
-        assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'")
+        assertEquals(",/2", l1.functor, "Expected functor ',/2'")
         val l2 = l1.arguments[0] as CompoundTerm
-        assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'")
+        assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'")
     }
 
     @Test
@@ -156,6 +157,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(Functor.of("/0"), rule.head.functor, "Expected a constraint")
+        assertEquals("/_", rule.head.functor, "Expected a constraint")
     }
 }

tests/prolog/builtins/AnalysisOperatorsTests.kt

@@ -1,404 +0,0 @@
-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,6 +8,7 @@ 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
@@ -39,7 +40,7 @@ class DatabaseOperatorsTests {
             createAssert(fact).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.db.predicates[Functor.of("a/_")]!!.clauses[0])
+            assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0])
         }
 
         @Test
@@ -48,7 +49,7 @@ class DatabaseOperatorsTests {
             createAssert(fact).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
+            assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0])
         }
 
         @Test
@@ -60,7 +61,7 @@ class DatabaseOperatorsTests {
             createAssert(rule).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
+            assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0])
         }
     }
 
@@ -91,8 +92,8 @@ class DatabaseOperatorsTests {
             AssertA(rule2).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
-            assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[1])
+            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1])
         }
     }
 
@@ -116,8 +117,8 @@ class DatabaseOperatorsTests {
             AssertZ(rule2).satisfy(emptyMap())
 
             assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
-            assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0])
-            assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1])
+            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1])
         }
     }
 
@@ -308,20 +309,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[Functor.of("a/1")]!!.clauses.size, "Expected 3 clauses")
+        assertEquals(3, Program.db.predicates["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[Functor.of("a/1")]!!.clauses.size, "Expected 0 clauses")
+        assertEquals(0, Program.db.predicates["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 = Functor.of("$predicateName/1")
+        val predicateFunctor = "$predicateName/1"
 
         assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")