250 lines
9.2 KiB
Kotlin
250 lines
9.2 KiB
Kotlin
package prolog.builtins
|
|
|
|
import com.sun.tools.javac.resources.CompilerProperties.Fragments.Anonymous
|
|
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.*
|
|
import prolog.ast.lists.List
|
|
import prolog.ast.lists.List.Empty
|
|
import prolog.ast.lists.List.Cons
|
|
|
|
/**
|
|
* [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.
|
|
*
|
|
* Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3)
|
|
*/
|
|
class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) :
|
|
Structure("functor", 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 t = applySubstitution(term, subs)
|
|
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(t 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("arg", 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.
|
|
for ((count, argument) in t.arguments.withIndex()) {
|
|
unifyLazy(value, argument, subs).forEach { result ->
|
|
result.map {
|
|
val sub = arg to Integer(count + 1)
|
|
yield(Result.success(it + sub))
|
|
}
|
|
}
|
|
}
|
|
|
|
}
|
|
|
|
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))
|
|
}
|
|
}
|
|
}
|
|
|
|
override fun applySubstitution(subs: Substitutions): Arg = Arg(
|
|
arg.applySubstitution(subs),
|
|
term.applySubstitution(subs),
|
|
value.applySubstitution(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("clause", 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
|
|
|
|
val appliedHead = applySubstitution(head, subs)
|
|
val appliedBody = applySubstitution(body, subs)
|
|
|
|
// Unify the head of the clause with the head of the goal
|
|
unifyLazy(clauseHead, appliedHead, subs).forEach { result ->
|
|
result.map { headSubs ->
|
|
// Unify the body of the clause with the body of the goal
|
|
unifyLazy(clauseBody, appliedBody, 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()))
|
|
}
|
|
}
|
|
|
|
override fun applySubstitution(subs: Substitutions): ClauseOp = ClauseOp(
|
|
head.applySubstitution(subs) as Head,
|
|
body.applySubstitution(subs) as Body
|
|
)
|
|
}
|
|
|
|
open class Univ(private val term: Term, private val list: Term) : Operator("=..", term, list) {
|
|
override fun satisfy(subs: Substitutions): Answers {
|
|
return when {
|
|
nonvariable(term, subs) && nonvariable(list, subs) -> {
|
|
val t = applySubstitution(term, subs)
|
|
val l = applySubstitution(list, subs) as List
|
|
unifyLazy(t, listToTerm(l), subs)
|
|
}
|
|
|
|
variable(term, subs) && nonvariable(list, subs) -> {
|
|
val l = applySubstitution(list, subs) as List
|
|
val t = listToTerm(l)
|
|
unifyLazy(term, t, subs)
|
|
}
|
|
|
|
nonvariable(term, subs) && variable(list, subs) -> {
|
|
val t = applySubstitution(term, subs)
|
|
val l = termToList(t)
|
|
unifyLazy(l, list, subs)
|
|
}
|
|
|
|
else -> throw Exception("Arguments are not sufficiently instantiated")
|
|
}
|
|
}
|
|
|
|
protected open fun listToTerm(list: List): Term {
|
|
return when {
|
|
list.size.value == 1 -> list.head
|
|
|
|
list.size.value > 1 -> {
|
|
val head = list.head
|
|
val arguments = mutableListOf<Term>()
|
|
var tail: Term? = list.tail
|
|
while (tail != null && tail is Cons) {
|
|
arguments.add(tail.head)
|
|
tail = tail.tail
|
|
}
|
|
if (tail != null && tail !is Empty) {
|
|
arguments.add(tail)
|
|
}
|
|
Structure(head as Atom, arguments)
|
|
}
|
|
|
|
else -> throw IllegalStateException("List is empty")
|
|
}
|
|
}
|
|
|
|
protected open fun termToList(term: Term): List {
|
|
return when (term) {
|
|
is Atom -> Cons(term, Empty)
|
|
|
|
is Structure -> {
|
|
val head = term.functor.name
|
|
val arguments = term.arguments
|
|
// Construct the list by iterating over the arguments in reverse
|
|
var tail: List = Empty
|
|
for (i in arguments.size - 1 downTo 0) {
|
|
tail = Cons(arguments[i], tail)
|
|
}
|
|
return Cons(head, tail)
|
|
}
|
|
|
|
else -> throw IllegalStateException("Term is not a valid structure")
|
|
}
|
|
}
|
|
|
|
override fun applySubstitution(subs: Substitutions): Univ = Univ(
|
|
term.applySubstitution(subs),
|
|
list.applySubstitution(subs)
|
|
)
|
|
}
|
|
|
|
class NumberVars(private val term: Term, private val start: Integer, private val end: Term) :
|
|
Structure("numbervars", term, start, end) {
|
|
private var yieldEnd: Boolean = true
|
|
|
|
constructor(term: Term) : this(term, Integer(0), AnonymousVariable.create()) {
|
|
yieldEnd = false
|
|
}
|
|
|
|
override fun satisfy(subs: Substitutions): Answers = sequence {
|
|
val (newEnd, newSubs) = numbervars(term, start.value, subs)
|
|
unifyLazy(end, Integer(newEnd), subs).forEach { endResult ->
|
|
endResult.map { endSubs ->
|
|
val result = if (yieldEnd) (newSubs + endSubs) else newSubs
|
|
yield(Result.success(result))
|
|
}
|
|
|
|
}
|
|
}
|
|
}
|