Arg
This commit is contained in:
parent
65c4d925d3
commit
752c278cb0
GPG key ID:
38297DE43F75FFE2
2 changed files with 218 additions and 41 deletions
|
|
@ -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)) {
|
||||
return when {
|
||||
nonvariable(term, subs) -> {
|
||||
val t = applySubstitution(term, subs) as Head
|
||||
|
||||
return Conjunction(
|
||||
Conjunction(
|
||||
Unify(t.functor.arity, functorArity),
|
||||
Unify(t.functor.name, functorName)
|
||||
).satisfy(subs)
|
||||
}
|
||||
|
||||
if (variable(term, 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 = if (arity.value == 0) {
|
||||
functorName
|
||||
} else {
|
||||
val argList = mutableListOf<Term>()
|
||||
for (i in 1..arity.value) {
|
||||
argList.add(AnonymousVariable.create())
|
||||
}
|
||||
Structure(name, argList)
|
||||
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)
|
||||
else -> throw IllegalStateException()
|
||||
}
|
||||
|
||||
return sequenceOf(Result.success(mapOf(term to result)))
|
||||
}
|
||||
|
||||
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))
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<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)
|
||||
}
|
||||
}
|
||||
Reference in a new issue