diff --git a/src/prolog/builtins/analysingAndConstructionOperators.kt b/src/prolog/builtins/analysingAndConstructionOperators.kt index ba589ef..f2a9079 100644 --- a/src/prolog/builtins/analysingAndConstructionOperators.kt +++ b/src/prolog/builtins/analysingAndConstructionOperators.kt @@ -3,56 +3,43 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions import prolog.ast.arithmetic.Integer -import prolog.ast.terms.AnonymousVariable -import prolog.ast.terms.Atom -import prolog.ast.terms.Head -import prolog.ast.terms.Structure -import prolog.ast.terms.Term -import prolog.ast.terms.Variable -import prolog.logic.applySubstitution -import prolog.logic.atomic -import prolog.logic.nonvariable -import prolog.logic.unifyLazy -import prolog.logic.variable +import prolog.ast.terms.* +import prolog.logic.* +import java.util.Locale +import java.util.Locale.getDefault +/** + * [True] when [Term] is a term with [FunctorInfo] 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 Functor(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 { - if (nonvariable(term, subs)) { - val t = applySubstitution(term, subs) as Head + return when { + nonvariable(term, subs) -> { + val t = applySubstitution(term, subs) as Head - return Conjunction( - Unify(t.functor.arity, functorArity), - Unify(t.functor.name, functorName) - ).satisfy(subs) - } - - if (variable(term, subs)) { - require(atomic(functorName, subs) && atomic(functorArity, subs)) { - "Arguments are not sufficiently instantiated" + Conjunction( + Unify(t.functor.arity, functorArity), + Unify(t.functor.name, functorName) + ).satisfy(subs) } - val name = applySubstitution(functorName, subs) as Atom - val arity = applySubstitution(functorArity, subs) as Integer - - val result = if (arity.value == 0) { - functorName - } else { - val argList = mutableListOf() - for (i in 1..arity.value) { - argList.add(AnonymousVariable.create()) + variable(term, subs) -> { + require(atomic(functorName, subs) && atomic(functorArity, subs)) { + "Arguments are not sufficiently instantiated" } - Structure(name, argList) + + 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))) } - if (nonvariable(term, subs)) { - return unifyLazy(term, result, subs) - } - - return sequenceOf(Result.success(mapOf(term to result))) + else -> throw IllegalStateException() } - - throw IllegalStateException() } override fun applySubstitution(subs: Substitutions): Functor = Functor( @@ -60,6 +47,51 @@ class Functor(private val term: Term, private val functorName: Term, private val functorName.applySubstitution(subs), functorArity.applySubstitution(subs) ) - - override fun toString(): String = "functor($term, $functorName, $functorArity)" +} + +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)) + } + } + } } diff --git a/tests/prolog/builtins/AnalysingAndConstructionOperatorsTests.kt b/tests/prolog/builtins/AnalysingAndConstructionOperatorsTests.kt index 6e91bfc..8c2e28d 100644 --- a/tests/prolog/builtins/AnalysingAndConstructionOperatorsTests.kt +++ b/tests/prolog/builtins/AnalysingAndConstructionOperatorsTests.kt @@ -4,6 +4,7 @@ import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertInstanceOf import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertThrows import prolog.ast.arithmetic.Integer import prolog.ast.terms.AnonymousVariable import prolog.ast.terms.Atom @@ -88,4 +89,148 @@ class AnalysingAndConstructionOperatorsTests { assertTrue(result.isEmpty(), "Expected no results") } + + @Test + fun `functor(X, Y, 1)`() { + val functor = Functor(Variable("X"), Variable("Y"), Integer(1)) + + val exception = assertThrows { + 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 { + 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 { + arg.satisfy(emptyMap()).toList() + } + assertEquals("Domain error: not_less_than_zero", exception.message) + } } \ No newline at end of file