83 lines
2.6 KiB
Kotlin
83 lines
2.6 KiB
Kotlin
package prolog.ast.logic
|
|
|
|
import prolog.Answers
|
|
import prolog.Substitutions
|
|
import prolog.ast.terms.Functor
|
|
import prolog.ast.terms.Goal
|
|
import prolog.flags.AppliedCut
|
|
|
|
/**
|
|
* Collection of [Clause]s with the same [Functor].
|
|
*
|
|
* If a goal is proved, the system looks for a predicate with the same functor, then uses indexing
|
|
* to select candidate clauses and then tries these clauses one-by-one.
|
|
*/
|
|
class Predicate : Resolvent {
|
|
val functor: Functor
|
|
val clauses: MutableList<Clause>
|
|
|
|
/**
|
|
* Creates a predicate with the given functor and an empty list of clauses.
|
|
*/
|
|
constructor(functor: Functor) {
|
|
this.functor = functor
|
|
this.clauses = mutableListOf()
|
|
}
|
|
|
|
/**
|
|
* Creates a predicate with the given clauses.
|
|
*/
|
|
constructor(clauses: List<Clause>) {
|
|
this.functor = clauses.first().functor
|
|
|
|
require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
|
|
this.clauses = clauses.toMutableList()
|
|
}
|
|
|
|
/**
|
|
* Adds a clause to the predicate.
|
|
*/
|
|
fun add(clause: Clause) {
|
|
require(clause.functor == functor) { "Clause functor does not match predicate functor" }
|
|
|
|
if (Debug.on) {
|
|
println("Adding clause $clause to predicate $functor")
|
|
}
|
|
|
|
clauses.add(clause)
|
|
}
|
|
|
|
/**
|
|
* Adds a list of clauses to the predicate.
|
|
*/
|
|
fun addAll(clauses: List<Clause>) {
|
|
require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
|
|
this.clauses.addAll(clauses)
|
|
}
|
|
|
|
override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
|
|
require(goal.functor == functor) { "Goal functor does not match predicate functor" }
|
|
// Try to unify the goal with the clause
|
|
// If the unification is successful, yield the substitutions
|
|
clauses.forEach { clause ->
|
|
clause.solve(goal, subs).forEach { clauseResult ->
|
|
clauseResult.fold(
|
|
onSuccess = {
|
|
yield(Result.success(it))
|
|
},
|
|
onFailure = {
|
|
if (it is AppliedCut) {
|
|
if (it.subs != null) {
|
|
// If it's a cut, yield the result with the left substitutions
|
|
yield(Result.success(it.subs))
|
|
}
|
|
return@sequence
|
|
} else {
|
|
yield(Result.failure(it))
|
|
}
|
|
}
|
|
)
|
|
}
|
|
}
|
|
}
|
|
}
|