tdpeuter/2025LogProg-project-GhentProlog
tdpeuter/2025LogProg-project-GhentProlog
Archived
1
Fork 0
Code Issues Releases Activity Actions

Compare commits

base: tdpeuter:1feb3893c53ad8015ec99988529f145c8afd1e29
Branches Tags
tdpeuter:main
tdpeuter:sync
..
compare: tdpeuter:973365e2ec75f3915bc2bb9ae14fd98801552b0b
Branches Tags
tdpeuter:main
tdpeuter:sync

No commits in common. "1feb3893c53ad8015ec99988529f145c8afd1e29" and "973365e2ec75f3915bc2bb9ae14fd98801552b0b" have entirely different histories.
1feb3893c5 ... 973365e2ec

16 changed files with 47 additions and 805 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/interpreter/Preprocessor.kt
View file

@ -65,7 +65,6 @@ open class Preprocessor {
Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body)
Functor.of("atomic/1") -> AtomicOp(args[0])
Functor.of("compound/1") -> CompoundOp(args[0])
Functor.of("=../2") -> Univ(args[0], args[1])
// Arithmetic
Functor.of("inf/0") -> Integer(Int.MAX_VALUE)

20
src/parser/grammars/TermsGrammar.kt
View file

@ -5,11 +5,8 @@ import com.github.h0tk3y.betterParse.grammar.parser
import com.github.h0tk3y.betterParse.parser.Parser
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.lists.List
import prolog.ast.terms.*
import prolog.builtins.Dynamic
import prolog.ast.lists.List.Empty
import prolog.ast.lists.List.Cons
/**
* Precedence is based on the following table:
@ -68,7 +65,6 @@ open class TermsGrammar : Tokens() {
// Base terms (atoms, compounds, variables, numbers)
protected val baseTerm: Parser<Term> by (dummy
or (-leftParenthesis * parser(::term) * -rightParenthesis)
or parser(::list)
or compound
or atom
or variable
@ -91,7 +87,7 @@ open class TermsGrammar : Tokens() {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val op700: Parser<String> by (univOp or equivalent or notEquivalent or equals or notEquals or isOp) use { text }
protected val op700: Parser<String> by (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
}
@ -116,20 +112,6 @@ open class TermsGrammar : Tokens() {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
// Lists
protected val list: Parser<List> by (-leftBracket * separated(
parser(::termNoConjunction),
comma,
acceptZero = true
) * -rightBracket) use {
var list: List = Empty
// Construct the list in reverse order
for (term in this.terms.reversed()) {
list = Cons(term, list)
}
list
}
// Term - highest level expression
protected val term: Parser<Term> by term1200
protected val termNoConjunction: Parser<Term> by term700

3
src/parser/grammars/Tokens.kt
View file

@ -10,8 +10,6 @@ import com.github.h0tk3y.betterParse.lexer.token
abstract class Tokens : Grammar<Any>() {
protected val leftParenthesis: Token by literalToken("(")
protected val rightParenthesis: Token by literalToken(")")
protected val leftBracket: Token by literalToken("[")
protected val rightBracket: Token by literalToken("]")
protected val exclamation: Token by literalToken("!")
// 1200
protected val neck by literalToken(":-")
@ -22,7 +20,6 @@ abstract class Tokens : Grammar<Any>() {
// 1000
protected val comma: Token by literalToken(",")
// 700
protected val univOp: Token by literalToken("=..")
protected val notEquivalent: Token by literalToken("\\==")
protected val equivalent: Token by literalToken("==")
protected val equals: Token by literalToken("=")

57
src/prolog/ast/lists/List.kt
View file

@ -1,57 +0,0 @@
package prolog.ast.lists
import prolog.Substitutions
import prolog.ast.terms.Term
import prolog.ast.arithmetic.Integer
sealed class List : Term {
abstract val head: Term
open val tail: List? = null
val size: Integer
get() = when (this) {
is Empty -> Integer(0)
is Cons -> Integer(1 + tail.size.value)
}
fun isEmpty(): Boolean = this is Empty
/**
* The empty list []
*/
object Empty : List() {
override val head = this
override fun applySubstitution(subs: Substitutions): Empty = this
override fun toString(): String = "[]"
}
class Cons(override val head: Term, override var tail: List) : List() {
override fun applySubstitution(subs: Substitutions): List {
val newHead = head.applySubstitution(subs)
val newTail = tail.applySubstitution(subs) as List
return Cons(newHead, newTail)
}
override fun toString(): String {
val values = mutableListOf<Term>()
var current: List? = this
while (current != null && current !is Empty) {
values.add(current.head)
current = current.tail
}
return "[${values.joinToString(", ")}]"
}
}
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other == null) return false
if (other !is List) return false
if (this is Empty && other is Empty) return true
if (this is Cons && other is Cons) {
return this.head == other.head && this.tail == other.tail
}
return false
}
override fun hashCode(): Int = super.hashCode()
}

22
src/prolog/ast/logic/Clause.kt
View file

@ -39,26 +39,28 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
// Filter the substitutions to only include those that map from head to goal
val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values }
val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
val headResult = headToGoalSubs.filterKeys { key ->
goalToHeadSubs.any { occurs(key as Variable, it.value) }
}
val newSubs = headRenaming + headToGoalSubs
body.satisfy(newSubs).forEach { bodyAnswer ->
bodyAnswer.fold(
onSuccess = { bodySubs ->
// If the body can be proven, yield the (combined) substitutions
val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
yield(Result.success(goalResult + headResult + bodyResult))
val goalToHeadResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
val headResult = headToGoalSubs.filterKeys { key ->
goalToHeadSubs.any {
occurs(
key as Variable,
it.value
)
}
}
yield(Result.success(goalToHeadResult + headResult))
},
onFailure = { error ->
if (error is AppliedCut) {
// Find single solution and return immediately
if (error.subs != null) {
val bodySubs = error.subs
val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult)))
var result = goalToHeadSubs.mapValues { applySubstitution(it.value, error.subs) }
yield(Result.failure(AppliedCut(result)))
} else {
yield(Result.failure(AppliedCut()))
}

2
src/prolog/ast/terms/Atom.kt
View file

@ -11,7 +11,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
override fun applySubstitution(subs: Substitutions): Atom = this
override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
override fun toString(): String {
return name

101
src/prolog/builtins/analysisOperators.kt
View file

@ -7,9 +7,6 @@ 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.
@ -35,11 +32,10 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v
"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)))
sequenceOf(Result.success(mapOf(term to result)))
}
else -> throw IllegalStateException()
@ -70,13 +66,15 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
// 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()) {
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++
}
}
@ -96,12 +94,6 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
}
}
}
override fun applySubstitution(subs: Substitutions): Arg = Arg(
arg.applySubstitution(subs),
term.applySubstitution(subs),
value.applySubstitution(subs)
)
}
/**
@ -126,14 +118,11 @@ class ClauseOp(private val head: Head, private val body: Body) :
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 ->
unifyLazy(clauseHead, head, subs).forEach { result ->
result.map { headSubs ->
// Unify the body of the clause with the body of the goal
unifyLazy(clauseBody, appliedBody, headSubs).forEach { bodyResult ->
unifyLazy(clauseBody, body, headSubs).forEach { bodyResult ->
bodyResult.map { bodySubs ->
// Combine the substitutions from the head and body
val combinedSubs = headSubs + bodySubs
@ -147,11 +136,6 @@ class ClauseOp(private val head: Head, private val body: Body) :
yield(Result.success(emptyMap()))
}
}
override fun applySubstitution(subs: Substitutions): ClauseOp = ClauseOp(
head.applySubstitution(subs) as Head,
body.applySubstitution(subs) as Body
)
}
class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
@ -162,8 +146,6 @@ class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
emptySequence()
}
}
override fun applySubstitution(subs: Substitutions): AtomicOp = AtomicOp(term.applySubstitution(subs))
}
class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term) {
@ -174,75 +156,4 @@ class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term
emptySequence()
}
}
override fun applySubstitution(subs: Substitutions): CompoundOp = CompoundOp(term.applySubstitution(subs))
}
open class Univ(private val term: Term, private val list: Term) : Operator(Atom("=.."), 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: List? = list.tail
while (tail != null && tail !is Empty) {
arguments.add(tail.head)
tail = tail.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)
)
}

7
src/prolog/builtins/controlOperators.kt
View file

@ -2,15 +2,14 @@ package prolog.builtins
import prolog.Answers
import prolog.Substitutions
import prolog.ast.Database.Program
import prolog.ast.logic.LogicOperand
import prolog.ast.logic.LogicOperator
import prolog.ast.terms.Atom
import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Structure
import prolog.flags.AppliedCut
import prolog.logic.applySubstitution
import prolog.logic.numbervars
/**
* Always fail.
@ -54,8 +53,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
left.fold(
// If it succeeds, satisfy the right part with the updated substitutions and return all results
onSuccess = { leftSubs ->
right.satisfy(subs + leftSubs).forEach { right ->
right.fold(
right.satisfy(subs + leftSubs).forEach {
it.fold(
// If the right part succeeds, yield the result with the left substitutions
onSuccess = { rightSubs ->
yield(Result.success(leftSubs + rightSubs))

27
src/prolog/builtins/listOperators.kt
View file

@ -1,27 +0,0 @@
package prolog.builtins
import prolog.Answers
import prolog.Substitutions
import prolog.ast.lists.List
import prolog.ast.lists.List.Cons
import prolog.ast.lists.List.Empty
import prolog.ast.terms.Atom
import prolog.ast.terms.Operator
import prolog.ast.terms.Term
class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
private var solution: Operator = if (list is Empty) {
Unify(element, list)
} else if (list is Cons) {
Disjunction(
Unify(element, list.head),
Member(element, list.tail)
)
} else {
throw IllegalArgumentException("Invalid list type: ${list::class.simpleName}")
}
override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs)
override fun toString(): String = "$element ∈ $list"
}

4
src/prolog/builtins/unificationOperators.kt
View file

@ -22,7 +22,7 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
val t1 = applySubstitution(term1, subs)
val t2 = applySubstitution(term2, subs)
yieldAll(unifyLazy(t1, t2, emptyMap()))
yieldAll(unifyLazy(t1, t2, subs))
}
override fun applySubstitution(subs: Substitutions): Unify = Unify(
@ -45,7 +45,7 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
val t1 = applySubstitution(term1, subs)
val t2 = applySubstitution(term2, subs)
if (equivalent(t1, t2, emptyMap())) {
if (equivalent(t1, t2, subs)) {
yield(Result.success(emptyMap()))
}
}

90
src/prolog/logic/unification.kt
View file

@ -7,11 +7,10 @@ import prolog.ast.arithmetic.Expression
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.arithmetic.Number
import prolog.ast.lists.List
import prolog.ast.lists.List.Cons
import prolog.ast.lists.List.Empty
import prolog.ast.logic.Clause
import prolog.ast.logic.Fact
import prolog.ast.logic.LogicOperator
import prolog.ast.logic.Rule
import prolog.ast.terms.*
// Apply substitutions to a term
@ -59,10 +58,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
val t2 = applySubstitution(term2, subs)
when {
equivalent(t1, t2, subs) -> {
yield(Result.success(emptyMap()))
}
equivalent(t1, t2, subs) -> yield(Result.success(emptyMap()))
variable(t1, subs) -> {
val variable = t1 as Variable
if (!occurs(variable, t2, subs)) {
@ -85,32 +81,18 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
val args1 = structure1.arguments
val args2 = structure2.arguments
if (args1.size == args2.size) {
yieldAll(unifyArgs(args1, args2, subs))
}
}
}
t1 is List && t2 is List -> {
if (equivalent(t1, t2, subs)) {
yield(Result.success(emptyMap()))
} else if (t1.size == t2.size) {
val head1 = t1.head
val head2 = t2.head
unifyLazy(head1, head2, subs).forEach { headSubs ->
headSubs.map { headResult ->
if (t1 is Empty && t2 is Empty) {
yield(Result.success(headResult))
} else if (t1 is Cons && t2 is Cons) {
val tail1 = t1.tail
val tail2 = t2.tail
unifyLazy(tail1, tail2, headResult).forEach { tailSubs ->
tailSubs.map { tailResult ->
yield(Result.success(headResult + tailResult))
}
val results = args1.zip(args2).map { (arg1, arg2) ->
unifyLazy(arg1, arg2, subs)
}
// Combine the results of all unifications
val combinedResults = results.reduce { acc, result ->
acc.flatMap { a ->
result.map { b ->
if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
}
}.map { Result.success(it) }
}
yieldAll(combinedResults)
}
}
}
@ -119,32 +101,6 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
}
}
private fun unifyArgs(
args1: kotlin.collections.List<Argument>,
args2: kotlin.collections.List<Argument>,
subs: Substitutions
): Answers = sequence {
// Using the current subs, unify the first argument of each list
val arg1 = applySubstitution(args1[0], subs)
val arg2 = applySubstitution(args2[0], subs)
unifyLazy(arg1, arg2, subs).forEach { headResult ->
// Use the resulting substitutions to unify the rest of the arguments
headResult.map { headSubs ->
val rest1 = args1.drop(1).map { applySubstitution(it, headSubs) }
val rest2 = args2.drop(1).map { applySubstitution(it, headSubs) }
if (rest1.isEmpty() && rest2.isEmpty()) {
yield(Result.success(headSubs))
} else if (rest1.isNotEmpty() && rest2.isNotEmpty()) {
unifyArgs(rest1, rest2, subs).forEach { tailResult ->
tailResult.map { tailSubs ->
yield(Result.success(headSubs + tailSubs))
}
}
}
}
}
}
fun unify(term1: Term, term2: Term): Answer {
val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
return if (substitutions.hasNext()) {
@ -160,32 +116,12 @@ fun unify(term1: Term, term2: Term): Answer {
fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
return when {
term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0
term1 is Structure && term2 is Structure -> {
term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) ->
equivalent(arg1, arg2, subs)
}
}
term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0
term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0
term1 is Variable && term2 is Variable -> term1 == term2
term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
term1 is List && term2 is List -> {
if (term1.isEmpty() && term2.isEmpty()) {
true
} else if (term1.isEmpty() || term2.isEmpty()) {
false
} else {
require(term1 is Cons && term2 is Cons)
val head1 = term1.head
val tail1 = term1.tail
val head2 = term2.head
val tail2 = term2.tail
equivalent(head1, head2, subs) && equivalent(tail1, tail2, subs)
}
}
else -> false
}
}

47
tests/parser/grammars/TermsGrammarTests.kt
View file

@ -19,8 +19,6 @@ import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.builtins.Is
import prolog.logic.equivalent
import prolog.ast.lists.List.Empty
import prolog.ast.lists.List.Cons
class TermsGrammarTests {
private lateinit var parser: Grammar<Term>
@ -354,49 +352,4 @@ class TermsGrammarTests {
)
}
}
@Nested
class Lists {
private lateinit var parser: Grammar<Term>
@BeforeEach
fun setup() {
parser = TermsGrammar() as Grammar<Term>
}
@Test
fun `parse empty list`() {
val input = "[]"
val result = parser.parseToEnd(input)
assertEquals(Empty, result, "Expected empty list")
}
@Test
fun `parse non-empty list`() {
val input = "[a, b, c]"
val result = parser.parseToEnd(input)
assertEquals(
Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Empty))),
result,
"Expected non-empty list"
)
}
@Test
fun `parse nested lists`() {
val input = "[a, [b, c], d]"
val result = parser.parseToEnd(input)
assertEquals(
Cons(Atom("a"), Cons(Cons(Atom("b"), Cons(Atom("c"), Empty)), Cons(Atom("d"), Empty))),
result,
"Expected nested lists"
)
}
}
}

19
tests/prolog/EvaluationTests.kt
View file

@ -15,10 +15,7 @@ import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.lists.List.Empty
import prolog.ast.lists.List.Cons
import prolog.ast.terms.AnonymousVariable
import prolog.builtins.Unify
class EvaluationTests {
@BeforeEach
@ -482,20 +479,4 @@ class EvaluationTests {
assertEquals(1, subs3c.size, "Expected 1 substitution")
assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
}
@Test
fun `foo(emptyList) = foo(X)`() {
val list = Empty
val left = Structure(Atom("foo"), listOf(list))
val right = Structure(Atom("foo"), listOf(Variable("X")))
val unific = Unify(left, right)
val result = unific.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(list, subs[Variable("X")], "Expected X to be list(1, 2)")
}
}

252
tests/prolog/builtins/AnalysisOperatorsTests.kt
View file

@ -7,13 +7,13 @@ 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.lists.List
import prolog.ast.lists.List.Cons
import prolog.ast.lists.List.Empty
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.ast.terms.*
import prolog.logic.equivalent
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
@ -401,246 +401,4 @@ class AnalysisOperatorsTests {
)
}
}
@Nested
class `Univ operator` {
@Test
fun `univ without variables`() {
val univ = Univ(Atom("foo"), Cons(Atom("foo"), Empty))
val result = univ.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 `univ with variable list`() {
val list = Variable("List")
val univ = Univ(
CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))),
list
)
val expected = Cons(Atom("foo"), Cons(Atom("a"), Cons(Atom("b"), Empty)))
val result = univ.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(expected, subs[list], "Expected List to be $expected")
}
@Test
fun `univ with variable in compound`() {
val list = Variable("List")
val univ = Univ(
CompoundTerm(Atom("foo"), listOf(Variable("X"))),
list
)
val expected = Cons(Atom("foo"), Cons(Variable("X"), Empty))
val result = univ.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(expected, subs[list], "Expected List to be $expected")
}
@Test
fun `univ with var foo`() {
val univ = Univ(
Variable("Term"),
Cons(Atom("foo"), Empty)
)
val result = univ.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("foo"), subs[Variable("Term")], "Expected Term to be foo")
}
@Test
fun `univ with var foo(a)`() {
val univ = Univ(
Variable("Term"),
Cons(Atom("foo"), Cons(Atom("a"), Empty))
)
val result = univ.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(
Structure(Atom("foo"), listOf(Atom("a"))),
subs[Variable("Term")],
"Expected Term to be foo(a)"
)
}
@Test
fun `univ with var foo(X)`() {
val univ = Univ(
Variable("Term"),
Cons(Atom("foo"), Cons(Variable("X"), Empty))
)
val result = univ.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(
Structure(Atom("foo"), listOf(Variable("X"))),
subs[Variable("Term")],
"Expected Term to be foo(X)"
)
}
@Test
fun `univ with var foo(a, b(X), c)`() {
val univ = Univ(
Variable("Term"),
Cons(
Atom("foo"),
Cons(Atom("a"), Cons(CompoundTerm(Atom("b"), listOf(Variable("X"))), Cons(Atom("c"), Empty)))
)
)
val expected = CompoundTerm(
Atom("foo"),
listOf(Atom("a"), CompoundTerm(Atom("b"), listOf(Variable("X"))), Atom("c"))
)
val result = univ.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(expected, subs[Variable("Term")], "Expected Term to be $expected")
}
@Test
fun `univ with unified var should return substitution`() {
val univ = Univ(
CompoundTerm(
Atom("foo"), listOf(
Atom("a"),
CompoundTerm(Atom("bar"), listOf(Variable("X"))),
Atom("c")
)
),
Cons(
Atom("foo"),
Cons(Atom("a"), Cons(CompoundTerm(Atom("bar"), listOf(Atom("b"))), Cons(Atom("c"), Empty)))
)
)
val result = univ.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("b"), subs[Variable("X")], "Expected X to be b")
}
@Test
fun `univ of incompatible structures should fail`() {
val univ = Univ(
CompoundTerm(Atom("foo"), listOf(Atom("a"))),
Cons(Atom("bar"), Empty)
)
val result = univ.satisfy(emptyMap()).toList()
assertEquals(0, result.size, "Expected 0 results")
}
@Test
fun `univ with two vars should throw`() {
val univ = Univ(Variable("X"), Variable("Y"))
val exception = assertThrows<Exception> {
univ.satisfy(emptyMap()).toList()
}
assertEquals("Arguments are not sufficiently instantiated", exception.message)
}
class OpenUniv(term: Term, list: Term) : Univ(term, list) {
public override fun listToTerm(list: List): Term = super.listToTerm(list)
public override fun termToList(term: Term): List = super.termToList(term)
}
@Test
fun `a to term`() {
val univ = OpenUniv(Atom(""), Empty)
val originalList = Cons(Atom("a"), Empty)
val originalTerm = Atom("a")
val term = univ.listToTerm(originalList)
assertEquals(originalTerm, term, "Expected term to be a")
val list = univ.termToList(term)
assertEquals(originalList, list, "Expected list to be [a]")
}
@Test
fun `foo, bar to compound`() {
val univ = OpenUniv(Atom(""), Empty)
val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Empty))
val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar")))
val term = univ.listToTerm(originalList)
assertEquals(originalTerm, term)
val list = univ.termToList(term)
assertEquals(originalList, list)
}
@Test
fun `foo, bar, baz to compound`() {
val univ = OpenUniv(Atom(""), Empty)
val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Atom("baz"), Empty)))
val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar"), Atom("baz")))
val term = univ.listToTerm(originalList)
assertEquals(originalTerm, term)
val list = univ.termToList(term)
assertEquals(originalList, list)
}
@Test
fun `foo, bar, (baz, bar) to compound with list`() {
val univ = OpenUniv(Atom(""), Empty)
val originalList =
Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
val originalTerm = CompoundTerm(
Atom("foo"),
listOf(Atom("bar"), Cons(Atom("baz"), Cons(Atom("bar"), Empty)))
)
val term = univ.listToTerm(originalList)
assertTrue(equivalent(originalTerm, term, emptyMap()), "Expected term to be foo(bar, [baz, bar]))")
val list = univ.termToList(term)
assertTrue(equivalent(originalList, list, emptyMap()), "Expected list to be [foo, bar, [baz, bar]]")
}
}
}

73
tests/prolog/builtins/ListOperatorsTests.kt
View file

@ -1,73 +0,0 @@
package prolog.builtins
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Test
import prolog.ast.lists.List.Cons
import prolog.ast.lists.List.Empty
import prolog.ast.terms.Atom
import prolog.ast.terms.Variable
class ListOperatorsTests {
@Test
fun `size empty list is 0`() {
assertEquals(0, Empty.size.value, "Expected size of empty list to be 0")
}
@Test
fun `size of singleton is 1`() {
val list = Cons(Atom("a"), Empty)
assertEquals(1, list.size.value, "Expected size of singleton list to be 1")
}
@Test
fun `size of list with five elements is 5`() {
val list = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("e"), Empty)))))
assertEquals(5, list.size.value, "Expected size of list with five elements to be 5")
}
@Test
fun `member(a, list of a)`() {
val atom = Atom("a")
val list = Cons(atom, Empty)
val member = Member(atom, list)
val result = member.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Expected one solution")
assertTrue(result[0].isSuccess, "Expected success")
assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
}
@Test
fun `member should only check shallow`() {
val list = Cons(Atom("a"), Cons(Cons(Atom("b"), Empty), Empty))
var result = Member(Atom("a"), list).satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Expected one solution")
assertTrue(result[0].isSuccess, "Expected success")
assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
result = Member(Atom("b"), list).satisfy(emptyMap()).toList()
assertEquals(0, result.size, "Expected no solution")
}
@Test
fun `member with variable in list`() {
val atom = Atom("a")
val variable = Variable("X")
val list = Cons(variable, Empty)
val member = Member(atom, list)
val result = member.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Expected one solution")
assertTrue(result[0].isSuccess, "Expected success")
assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom")
}
}

123
tests/prolog/logic/UnificationTests.kt
View file

@ -10,16 +10,13 @@ import prolog.ast.terms.Variable
import prolog.builtins.Add
import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Nested
import prolog.ast.lists.List
import prolog.ast.lists.List.Empty
import prolog.ast.lists.List.Cons
/*
* Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
*/
class UnificationTests {
@Nested
class `unify logic` {
class `unify` {
@Test
fun identical_atoms_unify() {
val atom1 = Atom("a")
@ -333,7 +330,7 @@ class UnificationTests {
}
@Nested
class `applySubstitution logic` {
class `applySubstitution` {
@Test
fun `apply substitution without sub`() {
val term = Variable("X")
@ -370,120 +367,4 @@ class UnificationTests {
assertEquals(Integer(35), result)
}
}
@Nested
class `equivalent logic` {
@Test
fun `empty lists are equivalent`() {
var eq = equivalent(Empty, Empty, emptyMap())
assertTrue(eq, "Empty lists should be equivalent")
val variable = Variable("X")
eq = equivalent(Empty, variable, mapOf(variable to Empty))
assertTrue(eq, "Empty list and variable should be equivalent")
eq = equivalent(variable, Empty, mapOf(variable to Empty))
assertTrue(eq, "Variable and empty list should be equivalent")
}
@Test
fun `singletons are equivalent`() {
val atom = Atom("a")
val list1 = Cons(atom, Empty)
val list2 = Cons(atom, Empty)
var eq = equivalent(list1, list2, emptyMap())
assertTrue(eq, "Singleton lists should be equivalent")
val variable = Variable("X")
eq = equivalent(list1, variable, mapOf(variable to list2))
assertTrue(eq, "Singleton list and variable should be equivalent")
eq = equivalent(variable, list1, mapOf(variable to list2))
assertTrue(eq, "Variable and singleton list should be equivalent")
}
@Test
fun `singleton and empty list are not equivalent`() {
val atom = Atom("a")
val list1 = Cons(atom, Empty)
val list2 = Empty
var eq = equivalent(list1, list2, emptyMap())
assertFalse(eq, "Singleton and empty lists should not be equivalent")
eq = equivalent(list2, list1, emptyMap())
assertFalse(eq, "Empty and singleton lists should not be equivalent")
val variable = Variable("X")
eq = equivalent(list1, variable, mapOf(variable to list2))
assertFalse(eq, "Singleton list and variable should not be equivalent")
eq = equivalent(variable, list1, mapOf(variable to list2))
assertFalse(eq, "Variable and singleton list should not be equivalent")
}
@Test
fun `identical lists are equivalent`() {
val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty))
val list2 = Cons(Atom("a"), Cons(Atom("b"), Empty))
var eq = equivalent(list1, list2, emptyMap())
assertTrue(eq, "Identical lists should be equivalent")
eq = equivalent(list2, list1, emptyMap())
assertTrue(eq, "Identical lists should be equivalent")
val variable = Variable("X")
eq = equivalent(list1, variable, mapOf(variable to list2))
assertTrue(eq, "Identical lists should be equivalent")
eq = equivalent(variable, list2, mapOf(variable to list1))
assertTrue(eq, "Identical lists should be equivalent")
}
@Test
fun `identical nested lists are equivalent`() {
val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
var eq = equivalent(list1, list2, emptyMap())
assertTrue(eq, "Identical nested lists should be equivalent")
eq = equivalent(list2, list1, emptyMap())
assertTrue(eq, "Identical nested lists should be equivalent")
val variable = Variable("X")
eq = equivalent(list1, variable, mapOf(variable to list2))
assertTrue(eq, "Identical nested lists should be equivalent")
eq = equivalent(variable, list2, mapOf(variable to list1))
assertTrue(eq, "Identical nested lists should be equivalent")
}
@Test
fun `lists with different nests are not equivalent`() {
val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("bar"), Cons(Atom("baz"), Empty)), Empty)))
val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
var eq = equivalent(list1, list2, emptyMap())
assertFalse(eq, "Lists with different nests should not be equivalent")
eq = equivalent(list2, list1, emptyMap())
assertFalse(eq, "Lists with different nests should not be equivalent")
val variable = Variable("X")
eq = equivalent(list1, variable, mapOf(variable to list2))
assertFalse(eq, "Lists with different nests should not be equivalent")
eq = equivalent(variable, list2, mapOf(variable to list1))
assertFalse(eq, "Lists with different nests should not be equivalent")
}
}
}