diff --git a/.idea/.gitignore b/.idea/.gitignore new file mode 100644 index 0000000..13566b8 --- /dev/null +++ b/.idea/.gitignore @@ -0,0 +1,8 @@ +# Default ignored files +/shelf/ +/workspace.xml +# Editor-based HTTP Client requests +/httpRequests/ +# Datasource local storage ignored files +/dataSources/ +/dataSources.local.xml diff --git a/.idea/compiler.xml b/.idea/compiler.xml new file mode 100644 index 0000000..b86273d --- /dev/null +++ b/.idea/compiler.xml @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file diff --git a/.idea/kotlinc.xml b/.idea/kotlinc.xml new file mode 100644 index 0000000..c22b6fa --- /dev/null +++ b/.idea/kotlinc.xml @@ -0,0 +1,6 @@ + + + + + \ No newline at end of file diff --git a/.idea/misc.xml b/.idea/misc.xml new file mode 100644 index 0000000..7c47dd4 --- /dev/null +++ b/.idea/misc.xml @@ -0,0 +1,8 @@ + + + + + + + + \ No newline at end of file diff --git a/.idea/vcs.xml b/.idea/vcs.xml new file mode 100644 index 0000000..35eb1dd --- /dev/null +++ b/.idea/vcs.xml @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file diff --git a/documentatie/verslag.pdf b/documentatie/verslag.pdf new file mode 100644 index 0000000..e69de29 diff --git a/documentatie/verslag.tex b/documentatie/verslag.tex new file mode 100644 index 0000000..49c1846 --- /dev/null +++ b/documentatie/verslag.tex @@ -0,0 +1,17 @@ +%! Author = tdpeuter +%! Date = 27/03/2025 + +% Preamble +\documentclass[11pt]{article} + +% Packages +\usepackage{amsmath} + +% Document +\begin{document} + + % Lexer op basis van https://craftinginterpreters.com/scanning.html + + + +\end{document} \ No newline at end of file diff --git a/pl/scratchpad.pl b/pl/scratchpad.pl new file mode 100644 index 0000000..7234ca2 --- /dev/null +++ b/pl/scratchpad.pl @@ -0,0 +1,4 @@ +likes(mary, john). +likes(john, mary). + +X :- likes(mary, X). diff --git a/src/prolog/Result.kt b/src/prolog/Result.kt deleted file mode 100644 index faf302d..0000000 --- a/src/prolog/Result.kt +++ /dev/null @@ -1,5 +0,0 @@ -package prolog - -import prolog.terms.Variable - -data class Result(val success: Boolean, val substitutions: List) diff --git a/src/prolog/builtins/control.kt b/src/prolog/builtins/control.kt new file mode 100644 index 0000000..0363413 --- /dev/null +++ b/src/prolog/builtins/control.kt @@ -0,0 +1,20 @@ +package prolog.builtins + +import prolog.components.terms.Atom + +/** + * Always fail. + */ +class Fail: Atom("fail") + +/** + * Same as fail, but the name has a more declarative connotation. + */ +typealias False = Fail + +/** + * Always succeed. + */ +class True: Atom("true") + +// TODO Repeat/0 diff --git a/src/prolog/builtins/terms.kt b/src/prolog/builtins/terms.kt new file mode 100644 index 0000000..d7a09c6 --- /dev/null +++ b/src/prolog/builtins/terms.kt @@ -0,0 +1,22 @@ +package prolog.builtins + +import prolog.components.terms.Atom +import prolog.components.terms.Term + +/** + * 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 (such a term is called a skeleton). If Term is atomic, Arity will be unified + * with the integer 0, and Name will be unified with Term. Raises instantiation_error() if Term is unbound and + * Name/Arity is insufficiently instantiated. + * + * SWI-Prolog also supports terms with arity 0, as in a() (see + * [section 5](https://www.swi-prolog.org/pldoc/man?section=extensions)). Such terms must be processed using functor/4 + * or compound_name_arity/3. The predicate functor/3 and =../2 raise a domain_error when faced with these terms. + * Without this precaution a round trip of a term with arity 0 over functor/3 would create an atom. + * + * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3) + */ +fun functor(term: Term, name: Atom, arity: Int): Boolean { + // TODO Implement + return true +} diff --git a/src/prolog/builtins/verification.kt b/src/prolog/builtins/verification.kt new file mode 100644 index 0000000..5b83659 --- /dev/null +++ b/src/prolog/builtins/verification.kt @@ -0,0 +1,41 @@ +package prolog.builtins + +import prolog.components.terms.CompoundTerm +import prolog.components.terms.Term +import prolog.components.terms.Variable + +/** + * True if [Term] is bound (i.e., not a variable) and is not compound. + * Thus, atomic acts as if defined by: + * + * atomic(Term) :- + * nonvar(Term), + * \+ compound(Term). + */ +fun atomic(term: Term): Boolean = nonvariable(term) && !compound(term) + +/** + * True if [Term] is bound to a compound term. + * See also functor/3 =../2, compound_name_arity/3 and compound_name_arguments/3. + */ +fun compound(term: Term): Boolean { + val isCompound = term is CompoundTerm + val isVariableCompound = term is Variable && term.alias().isPresent && compound(term.alias().get()) + return isCompound || isVariableCompound +} + +/** + * True if [Term] currently is not a free variable. + */ +fun nonvariable(term: Term): Boolean = !variable(term) + +/** + * True if [Term] currently is a free variable. + */ +fun variable(term: Term): Boolean { + if (term is Variable) { + return term.alias().isEmpty || term.alias().get() === term || variable(term.alias().get()) + } + + return false; +} diff --git a/src/prolog/builtins2/control/Conjunction.kt b/src/prolog/builtins2/control/Conjunction.kt new file mode 100644 index 0000000..b9cb9b2 --- /dev/null +++ b/src/prolog/builtins2/control/Conjunction.kt @@ -0,0 +1,10 @@ +package prolog.builtins2.control + +import prolog.components.terms.Atom +import prolog.components.Operand +import prolog.components.Operator + +/** + * Conjunction (and). True if both Goal1 and Goal2 are true. + */ +class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) \ No newline at end of file diff --git a/src/prolog/builtins2/control/Disjunction.kt b/src/prolog/builtins2/control/Disjunction.kt new file mode 100644 index 0000000..77f83b7 --- /dev/null +++ b/src/prolog/builtins2/control/Disjunction.kt @@ -0,0 +1,10 @@ +package prolog.builtins2.control + +import prolog.components.terms.Atom +import prolog.components.Operand +import prolog.components.Operator + +/** + * Disjunction (or). True if either Goal1 or Goal2 succeeds. + */ +class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) \ No newline at end of file diff --git a/src/prolog/components/Functor.kt b/src/prolog/components/Functor.kt new file mode 100644 index 0000000..bba168e --- /dev/null +++ b/src/prolog/components/Functor.kt @@ -0,0 +1,9 @@ +package prolog.components + +import prolog.components.terms.Atom + +data class Functor(val name: Atom, val arity: Int) { + override fun toString(): String { + return "${name.name}/${arity}" + } +} diff --git a/src/prolog/components/Goal.kt b/src/prolog/components/Goal.kt new file mode 100644 index 0000000..a7bfb66 --- /dev/null +++ b/src/prolog/components/Goal.kt @@ -0,0 +1,18 @@ +package prolog.components + +import prolog.components.terms.Term + +/** + * Question stated to the Prolog engine. + * + * A goal is either an [atom][prolog.components.terms.Atom] or a [compound term][prolog.components.terms.CompoundTerm]. + * A goal either [succeeds][prolog.builtins.True], in which case the variables in the compound terms have a binding, + * or it fails if Prolog fails to prove it. + */ +interface Goal: Term { + val functor: Functor + + fun prove(): Boolean { + return Program.query(this) + } +} diff --git a/src/prolog/components/Operator.kt b/src/prolog/components/Operator.kt new file mode 100644 index 0000000..e26a49b --- /dev/null +++ b/src/prolog/components/Operator.kt @@ -0,0 +1,19 @@ +package prolog.components + +import prolog.components.terms.Argument +import prolog.components.terms.Atom + +open class Operator( + val symbol: Atom, + val leftOperand: Operand? = null, + val rightOperand: Operand +) { + override fun toString(): String { + return when (leftOperand) { + null -> "${symbol.name} $rightOperand" + else -> "$leftOperand ${symbol.name} $rightOperand" + } + } +} + +typealias Operand = Argument diff --git a/src/prolog/components/Program.kt b/src/prolog/components/Program.kt new file mode 100644 index 0000000..9339436 --- /dev/null +++ b/src/prolog/components/Program.kt @@ -0,0 +1,62 @@ +package prolog.components + +import prolog.builtins.True +import prolog.components.expressions.Clause +import prolog.components.expressions.Fact +import prolog.components.expressions.Predicate + +/** + * Prolog Program or database. + */ +object Program { + private var predicates: Map = emptyMap() + + init { + // Initialize the program with built-in predicates + load(listOf( + Fact(True()) + )) + } + + /** + * Loads a list of clauses into the program. + */ + fun load(clauses: List) { + for (clause in clauses) { + val functor = clause.functor + val predicate = predicates[functor] + + if (predicate != null) { + // If the predicate already exists, add the clause to it + predicate.add(clause) + } else { + // If the predicate does not exist, create a new one + predicates += Pair(functor, Predicate(listOf(clause))) + } + } + } + + fun load(predicate: Predicate) { + val functor = predicate.functor + val existingPredicate = predicates[functor] + + if (existingPredicate != null) { + // If the predicate already exists, add the clauses to it + existingPredicate.addAll(predicate.clauses) + } else { + // If the predicate does not exist, create a new one + predicates += Pair(functor, predicate) + } + } + + fun query(goal: Goal): Boolean { + val functor = goal.functor + val predicate = predicates[functor] + ?: // If the predicate does not exist, return false + return false + // If the predicate exists, evaluate the goal against it + return predicate.evaluate(goal) + } +} + +typealias Database = Program diff --git a/src/prolog/components/expressions/Clause.kt b/src/prolog/components/expressions/Clause.kt new file mode 100644 index 0000000..3362a78 --- /dev/null +++ b/src/prolog/components/expressions/Clause.kt @@ -0,0 +1,35 @@ +package prolog.components.expressions + +import prolog.components.Functor +import prolog.components.Goal +import prolog.components.terms.Head +import prolog.components.terms.Term +import prolog.unify + +// TODO Change this to the right type, supporting operators and normal Clauses +// Probably needs a new interface or abstract class (?) +typealias Body = List + +/** + * ‘Sentence’ of a Prolog program. + * + * A clause consists of a [Head] and body separated by the [neck][prolog.terms.Neck] operator, or it is a [Fact]. + * + * @see [prolog.components.terms.Variable] + * @see [Predicate] + */ +abstract class Clause(val head: Head, val body: Body = emptyList()) : Expression { + val functor: Functor = head.functor + override fun evaluate(goal: Goal): Boolean { + val result = unify(goal, head) + // TODO Evaluate the body + return result.isEmpty + } + + override fun toString(): String { + return when { + body.isEmpty() -> head.toString() + else -> "$head :- ${body.joinToString(", ")}" + } + } +} diff --git a/src/prolog/components/expressions/Expression.kt b/src/prolog/components/expressions/Expression.kt new file mode 100644 index 0000000..34a4ec5 --- /dev/null +++ b/src/prolog/components/expressions/Expression.kt @@ -0,0 +1,7 @@ +package prolog.components.expressions + +import prolog.components.Goal + +interface Expression { + fun evaluate(goal: Goal): Boolean +} diff --git a/src/prolog/components/expressions/Fact.kt b/src/prolog/components/expressions/Fact.kt new file mode 100644 index 0000000..eb8364a --- /dev/null +++ b/src/prolog/components/expressions/Fact.kt @@ -0,0 +1,6 @@ +package prolog.components.expressions + +import prolog.builtins.True +import prolog.components.terms.Head + +class Fact(head: Head) : Clause(head, listOf(True())) diff --git a/src/prolog/components/expressions/Predicate.kt b/src/prolog/components/expressions/Predicate.kt new file mode 100644 index 0000000..b3866a4 --- /dev/null +++ b/src/prolog/components/expressions/Predicate.kt @@ -0,0 +1,54 @@ +package prolog.components.expressions + +import prolog.components.Functor +import prolog.components.Goal + +/** + * 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 : Expression { + val functor: Functor + val clauses: MutableList + + /** + * 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) { + 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" } + clauses.add(clause) + } + + /** + * Adds a list of clauses to the predicate. + */ + fun addAll(clauses: List) { + require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" } + this.clauses.addAll(clauses) + } + + override fun evaluate(goal: Goal): Boolean { + require(goal.functor == functor) { "Goal functor does not match predicate functor" } + return clauses.any { it.evaluate(goal) } + } +} diff --git a/src/prolog/components/expressions/Rule.kt b/src/prolog/components/expressions/Rule.kt new file mode 100644 index 0000000..afad8c7 --- /dev/null +++ b/src/prolog/components/expressions/Rule.kt @@ -0,0 +1,5 @@ +package prolog.components.expressions + +import prolog.components.terms.Head + +class Rule(head: Head, body: Body): Clause(head, body) diff --git a/src/prolog/components/terms/Atom.kt b/src/prolog/components/terms/Atom.kt new file mode 100644 index 0000000..7a08912 --- /dev/null +++ b/src/prolog/components/terms/Atom.kt @@ -0,0 +1,12 @@ +package prolog.components.terms + +import prolog.components.Functor +import prolog.components.Goal + +open class Atom(val name: String): Head(), Term, Goal { + override val functor: Functor = Functor(this, 0) + + override fun toString(): String { + return name + } +} diff --git a/src/prolog/components/terms/Head.kt b/src/prolog/components/terms/Head.kt new file mode 100644 index 0000000..62b26e8 --- /dev/null +++ b/src/prolog/components/terms/Head.kt @@ -0,0 +1,13 @@ +package prolog.components.terms + +import prolog.components.Functor + +/** + * Part of a [Clause][prolog.components.expressions.Clause] before the [neck][prolog.terms.Neck] operator. + * + * @see [Atom] + * @see [CompoundTerm] + */ +abstract class Head: Term { + abstract val functor: Functor +} diff --git a/src/prolog/components/terms/Structure.kt b/src/prolog/components/terms/Structure.kt new file mode 100644 index 0000000..0e11a39 --- /dev/null +++ b/src/prolog/components/terms/Structure.kt @@ -0,0 +1,17 @@ +package prolog.components.terms + +import prolog.components.Functor +import prolog.components.Goal + +open class Structure(val name: Atom, val arguments: List): Head(), Term, Goal { + override val functor: Functor = Functor(name, arguments.size) + + override fun toString(): String { + return when { + arguments.isEmpty() -> name.name + else -> "${name.name}(${arguments.joinToString(", ")})" + } + } +} + +typealias CompoundTerm = Structure diff --git a/src/prolog/components/terms/Term.kt b/src/prolog/components/terms/Term.kt new file mode 100644 index 0000000..a7e6913 --- /dev/null +++ b/src/prolog/components/terms/Term.kt @@ -0,0 +1,32 @@ +package prolog.components.terms + +/** + * Value in Prolog. + * + * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm]. + * In addition, SWI-Prolog also defines the type string. + */ +interface Term + +typealias Argument = Term + +/* + ::= | + ::= | + ::= . | :- . + ::= | , + ::= | ( ) + ::= | , + ::= | | | + ::= ( ) + ::= ?- . + ::= | + ::= | + ::= a | b | c | ... | x | y | z + ::= A | B | C | ... | X | Y | Z | _ + ::= | + ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 + ::= | | | + ::= + | - | * | / | \ | ^ | ~ | : | . | ? | | # | $ | & + ::= | +*/ diff --git a/src/prolog/components/terms/Variable.kt b/src/prolog/components/terms/Variable.kt new file mode 100644 index 0000000..5939a9e --- /dev/null +++ b/src/prolog/components/terms/Variable.kt @@ -0,0 +1,30 @@ +package prolog.components.terms + +import java.util.Optional + +data class Variable(val name: String): Term { + private var alias: Optional = Optional.empty() + + fun alias(): Optional { + return alias + } + + fun bind(term: Term): Optional { + if (alias.isEmpty) { + alias = Optional.of(term) + } + + return alias + } + + fun unbind() { + alias = Optional.empty() + } + + override fun toString(): String { + return when { + alias.isPresent -> "$name = ${alias.get()}" + else -> name + } + } +} diff --git a/src/prolog/terms/Atom.kt b/src/prolog/terms/Atom.kt deleted file mode 100644 index f401895..0000000 --- a/src/prolog/terms/Atom.kt +++ /dev/null @@ -1,3 +0,0 @@ -package prolog.terms - -data class Atom(val name: String): Term() diff --git a/src/prolog/terms/Term.kt b/src/prolog/terms/Term.kt deleted file mode 100644 index 10e1f0a..0000000 --- a/src/prolog/terms/Term.kt +++ /dev/null @@ -1,3 +0,0 @@ -package prolog.terms - -sealed class Term diff --git a/src/prolog/terms/operators.kt b/src/prolog/terms/operators.kt new file mode 100644 index 0000000..2f788ad --- /dev/null +++ b/src/prolog/terms/operators.kt @@ -0,0 +1,9 @@ +package prolog.terms + +import prolog.components.Operand +import prolog.components.Operator +import prolog.components.terms.Atom + +class Neck(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(":-"), leftOperand, rightOperand) + +class Query(rightOperand: Operand): Operator(Atom("?-"), null, rightOperand) diff --git a/src/prolog/unify.kt b/src/prolog/unify.kt index 6387c99..0ad2c5d 100644 --- a/src/prolog/unify.kt +++ b/src/prolog/unify.kt @@ -1,7 +1,83 @@ package prolog -import prolog.terms.Term +import prolog.builtins.atomic +import prolog.builtins.compound +import prolog.builtins.variable +import prolog.components.Goal +import prolog.components.terms.Term +import prolog.components.terms.Variable +import prolog.components.terms.Structure +import java.util.* -fun unify(term1: Term, term2: Term): Result { - return Result(term1 == term2, emptyList()) +typealias Substitution = Map + +// Apply substitutions to a term +fun applySubstitution(term: Term, substitution: Substitution): Term = when { + variable(term) -> (term as Variable).alias().map { applySubstitution(it, substitution) }.orElse(term) + atomic(term) -> term + compound(term) -> { + val structure = term as Structure + Structure(structure.name, structure.arguments.map { applySubstitution(it, substitution) }) + } + else -> term +} + +// Check if a variable occurs in a term +fun occurs(variable: Variable, term: Term): Boolean = when { + variable(term) -> term == variable + atomic(term) -> false + compound(term) -> { + val structure = term as Structure + structure.arguments.any { occurs(variable, it) } + } + else -> false +} + +// Generate possible substitutions +fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence = sequence { + val t1 = applySubstitution(term1, substitution) + val t2 = applySubstitution(term2, substitution) + + when { + t1 == t2 -> yield(substitution) + variable(t1) -> { + val variable = t1 as Variable + if (!occurs(variable, t2)) { + variable.bind(t2) + yield(substitution + (variable to t2)) + } + } + variable(t2) -> { + val variable = t2 as Variable + if (!occurs(variable, t1)) { + variable.bind(t1) + yield(substitution + (variable to t1)) + } + } + compound(t1) && compound(t2) -> { + val structure1 = t1 as Structure + val structure2 = t2 as Structure + if (structure1.functor == structure2.functor) { + val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(substitution) { acc, (arg1, arg2) -> + generateSubstitutions(arg1, arg2, acc).firstOrNull() ?: return@sequence + } + yield(newSubstitution) + } + } + else -> {} + } +} + +// Unify two terms with backtracking and lazy evaluation +fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence { + return generateSubstitutions(term1, term2, substitution) +} + +fun unify(term1: Term, term2: Term): Optional { + val substitutions = unifyLazy(term1, term2).toList() + return if (substitutions.isEmpty()) { + Optional.empty() + } else { + Optional.of(substitutions.first()) + } } diff --git a/tests/lexer/LexerScanPrologTest.kt b/tests/lexer/LexerScanPrologTest.kt index 9e9a054..7d25492 100644 --- a/tests/lexer/LexerScanPrologTest.kt +++ b/tests/lexer/LexerScanPrologTest.kt @@ -1,8 +1,14 @@ package lexer import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertThrows import kotlin.test.assertEquals +/** + * Tests for the Prolog lexer. + * + * These tests are based on the Prolog syntax. + */ class LexerScanPrologTest { @Test fun scan_simple_atom() { @@ -25,4 +31,31 @@ class LexerScanPrologTest { assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}") assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}") } -} \ No newline at end of file + + @Test + fun scan_variable_with_number() { + val tokens = Lexer("X1.").scan() + + assertEquals(3, tokens.size) + + assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}") + assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}") + assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}") + } + + @Test + fun scan_variable_with_underscore() { + val tokens = Lexer("X_1.").scan() + + assertEquals(3, tokens.size) + + assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}") + assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}") + assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}") + } + + @Test + fun scan_variable_that_starts_with_a_number() { + assertThrows { Lexer("1X.").scan() } + } +} diff --git a/tests/lexer/LexerScanTest.kt b/tests/lexer/LexerScanTest.kt index 8d03c61..bd4d515 100644 --- a/tests/lexer/LexerScanTest.kt +++ b/tests/lexer/LexerScanTest.kt @@ -1,8 +1,5 @@ -package be.ugent.logprog.lexer +package lexer -import lexer.Error -import lexer.Lexer -import lexer.TokenType import org.junit.jupiter.api.Test import org.junit.jupiter.api.assertThrows import org.junit.jupiter.api.Assertions.* diff --git a/tests/prolog/EvaluationTest.kt b/tests/prolog/EvaluationTest.kt new file mode 100644 index 0000000..af3a3fc --- /dev/null +++ b/tests/prolog/EvaluationTest.kt @@ -0,0 +1,26 @@ +package prolog + +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import prolog.components.Program +import prolog.components.expressions.Fact +import prolog.components.terms.Atom + +class EvaluationTest { + @Test + fun successful_single_clause_program_query() { + val fact = Fact(Atom("a")) + Program.load(listOf(fact)) + + assertTrue(Program.query(Atom("a"))) + } + + @Test + fun failing_single_clause_program_query() { + val fact = Fact(Atom("a")) + Program.load(listOf(fact)) + + assertFalse(Program.query(Atom("b"))) + } +} \ No newline at end of file diff --git a/tests/prolog/UnifyTest.kt b/tests/prolog/UnifyTest.kt new file mode 100644 index 0000000..7e299ef --- /dev/null +++ b/tests/prolog/UnifyTest.kt @@ -0,0 +1,246 @@ +package prolog + +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Test +import prolog.components.terms.Atom +import prolog.components.terms.Structure +import prolog.components.terms.Variable + +/* + * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms + */ +class UnifyTest { + @Test + fun identical_atoms_unify() { + val atom1 = Atom("a") + val atom2 = Atom("a") + + val result = unify(atom1, atom2) + + assertTrue(result.isPresent, "Identical atoms should unify") + assertEquals(0, result.get().size, "No substitutions should be made") + } + + @Test + fun different_atoms_do_not_unify() { + val atom1 = Atom("a") + val atom2 = Atom("b") + + val result = unify(atom1, atom2) + + assertFalse(result.isPresent, "Different atoms should not unify") + } + + @Test + fun identical_variables_unify() { + val variable1 = Variable("X") + val variable2 = Variable("X") + + val result = unify(variable1, variable2) + + assertTrue(result.isPresent, "Identical variables should unify") + assertEquals(0, result.get().size, "No substitutions should be made") + } + + @Test + fun variable_unifies_with_atom() { + val variable = Variable("X") + val atom = Atom("a") + + val result = unify(atom, variable) + + assertTrue(result.isPresent, "Variable should unify with atom") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(atom, variable.alias().get(), "Variable should be substituted with atom") + } + + @Test + fun variables_alias_when_unified() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val result = unify(variable1, variable2) + + assertTrue(result.isPresent) + assertEquals(1, result.get().size) + assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2") + } + + @Test + fun identical_compound_terms_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + assertTrue(result.isPresent, "Identical compound terms should unify") + assertEquals(0, result.get().size, "No substitutions should be made") + } + + @Test + fun compound_terms_with_different_arguments_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isPresent, "Different compound terms should not unify") + } + + @Test + fun compound_terms_with_different_functors_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isPresent, "Compound terms with different functors should not unify") + } + + @Test + fun variable_unifies_with_compound_term() { + val variable = Variable("X") + val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(variable, structure) + + assertTrue(result.isPresent, "Variable should unify with compound term") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(structure, variable.alias().get(), "Variable should be substituted with compound term") + } + + @Test + fun compound_term_with_variable_unifies_with_part() { + val variable = Variable("X") + val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable)) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + assertTrue(result.isPresent, "Compound term with variable should unify with part") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(Atom("b"), variable.alias().get(), "Variable should be substituted with atom") + } + + @Test + fun compound_terms_with_variable_arguments_lists_alias_variables() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(variable1)) + val structure2 = Structure(Atom("f"), listOf(variable2)) + + val result = unify(structure1, structure2) + + assertTrue(result.isPresent, "Compound terms with variable arguments should unify") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2") + } + + /** + * f(X) = f(Y, Z) + */ + @Test + fun compound_terms_with_different_arity_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Variable("X"))) + val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isPresent, "Compound terms with different arity should not unify") + } + + /** + * f(g(X)) = f(Y) + */ + @Test + fun nested_compound_terms_with_variables_unify() { + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X"))))) + val structure2 = Structure(Atom("f"), listOf(variable2)) + + val result = unify(structure1, structure2) + + assertTrue(result.isPresent, "Nested compound terms with variables should unify") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(Structure(Atom("g"), listOf(Variable("X"))), variable2.alias().get(), "Variable should be substituted with compound term") + } + + /** + * f(g(X), X) = f(Y, a) + */ + @Test + fun compound_terms_with_more_variables() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1)) + val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a"))) + + val result = unify(structure1, structure2) + + assertTrue(result.isPresent, "Compound terms with more variables should unify") + assertEquals(2, result.get().size, "There should be two substitutions") + + assertEquals(Atom("a"), variable1.alias().get(), "Variable 1 should be substituted with atom") + assertEquals(Structure(Atom("g"), listOf(Atom("a"))), variable2.alias().get(), "Variable 2 should be substituted with compound term") + } + + /** + * ?- X = f(X). + * X = f(f(X)). + */ + @Test + fun recursive_unification() { + val variable1 = Variable("X") + val structure2 = Structure(Atom("f"), listOf(Variable("X"))) + + val result = unify(variable1, structure2) + + assertTrue(result.isPresent, "Recursive unification should succeed") + assertEquals(1, result.get().size, "There should be one substitution") + assertEquals(structure2, variable1.alias().get(), "Variable should be substituted with compound term") + } + + /** + * ?- X = bar, Y = bar, X = Y. + */ + @Test + fun multiple_unification() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + val atom = Atom("bar") + + variable1.bind(atom) + variable2.bind(atom) + + val result = unify(variable1, variable2) + + assertTrue(result.isPresent, "Multiple unification should succeed") + assertEquals(0, result.get().size, "No substitutions should be made") + } + + /** + * ?- a = a(). + * false. + */ + @Test + fun atom_with_different_arity() { + val atom1 = Atom("a") + val structure2 = Structure(Atom("a"), emptyList()) + + val result = unify(atom1, structure2) + + assertFalse(result.isPresent, "Atom with different arity should not unify") + } + + @Test + fun temp() { + val atom1 = Atom("a") + val atom2 = Atom("a") + + val result = unify(atom1, atom2) + assertTrue(result.isPresent, "Identical atoms should unify") + } +} \ No newline at end of file diff --git a/tests/prolog/builtins/TermAnalysisConstructionTest.kt b/tests/prolog/builtins/TermAnalysisConstructionTest.kt new file mode 100644 index 0000000..a9c2a5f --- /dev/null +++ b/tests/prolog/builtins/TermAnalysisConstructionTest.kt @@ -0,0 +1,43 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertThrows +import prolog.components.terms.Atom +import prolog.components.terms.Structure + +/** + * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png) + * + * Notes by [David Tonhofer](https://github.com/dtonhofer) + */ +class TermAnalysisConstructionTest { + @Test + fun atomic_term_properties() { + val atom = Atom("foo") + + assertTrue(atomic(atom)) + assertFalse(compound(atom)) + + assertTrue(functor(atom, Atom("foo"), 0)) + } + + @Test + fun compound_arity_0_properties() { + val structure = Structure(Atom("foo"), emptyList()) + + assertFalse(atomic(structure)) + assertTrue(compound(structure)) + } + + @Test + fun compound_arity_1_properties() { + val structure = Structure(Atom("foo"), listOf(Atom("bar"))) + + assertFalse(atomic(structure)) + assertTrue(compound(structure)) + + assertTrue(functor(structure, Atom("foo"), 1)) + } +} \ No newline at end of file diff --git a/tests/prolog/builtins/VerificationBuiltinsTest.kt b/tests/prolog/builtins/VerificationBuiltinsTest.kt new file mode 100644 index 0000000..a6189ca --- /dev/null +++ b/tests/prolog/builtins/VerificationBuiltinsTest.kt @@ -0,0 +1,251 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import prolog.components.terms.Atom +import prolog.components.terms.Structure +import prolog.components.terms.Variable +import kotlin.test.assertEquals + +class BuiltinsTest { + @Test + fun unbound_variable_is_var() { + val variable = Variable("X") + assertTrue(variable(variable)) + assertTrue(variable.alias().isEmpty) + } + + @Test + fun variable_bound_to_atom_is_not_var() { + val variable = Variable("X") + + assertTrue(variable(variable)) + + val atom = Atom("a") + variable.bind(atom) + + assertFalse(variable(variable)) + assertEquals(atom, variable.alias().get()) + } + + @Test + fun variable_bound_to_compound_term_is_not_var() { + val variable = Variable("X") + + assertTrue(variable(variable)) + + val structure = Structure(Atom("a"), listOf(Atom("b"))) + variable.bind(structure) + + assertFalse(variable(variable)) + assertEquals(structure, variable.alias().get()) + } + + /** + * ?- X = X, var(X). + * true. + */ + @Test + fun variable_bound_to_itself_is_var() { + val variable = Variable("X") + variable.bind(variable) + assertTrue(variable(variable)) + } + + /** + * ?- X = Y, var(X). + * X = Y. + */ + @Test + fun variable_bound_to_another_variable_is_var() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + variable1.bind(variable2) + assertTrue(variable(variable1)) + assertEquals(variable2, variable1.alias().get()) + } + + /** + * ?- Y = a, X = Y, var(X). + * false. + */ + @Test + fun variable_bound_to_bound_variable_is_not_var() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + variable2.bind(Atom("a")) + variable1.bind(variable2) + assertFalse(variable(variable1)) + } + + @Test + fun atom_is_not_var() { + val atom = Atom("a") + assertFalse(variable(atom)) + } + + @Test + fun compound_term_is_not_var() { + val structure = Structure(Atom("a"), listOf(Atom("b"))) + assertFalse(variable(structure)) + } + + @Test + fun compound_term_with_var_is_not_var() { + val structure = Structure(Atom("a"), listOf(Variable("X"))) + assertFalse(variable(structure)) + } + + @Test + fun unbound_variable_is_not_nonvar() { + val variable = Variable("X") + assertFalse(nonvariable(variable)) + } + + /** + * ?- A = a, nonvar(A). + * A = a. + */ + @Test + fun variable_bound_to_atom_is_nonvar() { + val variable = Variable("X") + + assertFalse(nonvariable(variable)) + + val atom = Atom("a") + variable.bind(atom) + + assertTrue(nonvariable(variable)) + assertEquals(atom, variable.alias().get()) + } + + /** + * ?- A = f(b), nonvar(A). + * A = f(b). + */ + @Test + fun variable_bound_to_compound_term_is_nonvar() { + val variable = Variable("X") + + assertFalse(nonvariable(variable)) + + val structure = Structure(Atom("a"), listOf(Atom("b"))) + variable.bind(structure) + + assertTrue(nonvariable(variable)) + assertEquals(structure, variable.alias().get()) + } + + /** + * ?- X = X, nonvar(X). + * false. + */ + @Test + fun variable_bound_to_itself_is_not_nonvar() { + val variable = Variable("X") + variable.bind(variable) + assertFalse(nonvariable(variable)) + } + + /** + * ?- X = Y, nonvar(X). + * false. + */ + @Test + fun variable_bound_to_another_variable_is_not_nonvar() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + variable1.bind(variable2) + assertFalse(nonvariable(variable1)) + } + + @Test + fun atom_is_nonvar() { + val atom = Atom("a") + assertTrue(nonvariable(atom)) + } + + @Test + fun compound_term_is_nonvar() { + val structure = Structure(Atom("a"), listOf(Atom("b"))) + assertTrue(nonvariable(structure)) + } + + @Test + fun compound_term_with_var_is_nonvar() { + val structure = Structure(Atom("a"), listOf(Variable("X"))) + assertTrue(nonvariable(structure)) + } + + @Test + fun unbound_variable_is_not_compound() { + val variable = Variable("X") + assertFalse(compound(variable)) + } + + /** + * ?- A = a, compound(A). + * false. + */ + @Test + fun bound_variable_to_atom_is_not_compound() { + val variable = Variable("X") + val atom = Atom("a") + variable.bind(atom) + assertFalse(compound(variable)) + } + + /** + * ?- A = f(b), compound(A). + * A = f(b). + */ + @Test + fun bound_variable_to_compound_term_is_compound() { + val variable = Variable("X") + val structure = Structure(Atom("a"), listOf(Atom("b"))) + variable.bind(structure) + assertTrue(compound(variable)) + } + + /** + * ?- Y = f(b), X = Y, compound(X). + * Y = X, X = f(b). + */ + @Test + fun variable_bound_to_bound_variable_is_compound() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + val structure = Structure(Atom("a"), listOf(Atom("b"))) + + variable2.bind(structure) + variable1.bind(variable2) + + assertTrue(compound(variable1)) + + assertEquals(structure, variable2.alias().get()) + assertEquals(variable2, variable1.alias().get()) + } + + @Test + fun atom_is_not_compound() { + val atom = Atom("a") + assertFalse(compound(atom)) + } + + @Test + fun compound_term_is_compound() { + val structure = Structure(Atom("a"), listOf(Atom("b"))) + assertTrue(compound(structure)) + } + + /** + * ?- compound(a()). + * true. + */ + @Test + fun compound_term_with_no_arguments_is_compound() { + val structure = Structure(Atom("a"), emptyList()) + assertTrue(compound(structure)) + } +} \ No newline at end of file diff --git a/tests/prolog/unifyTest.kt b/tests/prolog/unifyTest.kt deleted file mode 100644 index c93e010..0000000 --- a/tests/prolog/unifyTest.kt +++ /dev/null @@ -1,29 +0,0 @@ -package prolog - -import org.junit.jupiter.api.Assertions.* -import org.junit.jupiter.api.Test -import prolog.terms.Atom - -class unifyTest { - @Test - fun identical_atoms_unify() { - val atom1 = Atom("a") - val atom2 = Atom("a") - - val result = unify(atom1, atom2) - - assertTrue(result.success) - assertEquals(0, result.substitutions.size) - } - - @Test - fun different_atoms_do_not_unify() { - val atom1 = Atom("a") - val atom2 = Atom("b") - - val result = unify(atom1, atom2) - - assertFalse(result.success) - assertEquals(0, result.substitutions.size) - } -} \ No newline at end of file