From 9db1c66781147869229aa39ee8fa2fa3c99895b9 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Thu, 1 May 2025 17:13:35 +0200 Subject: [PATCH] Checkpoint --- build.gradle.kts | 36 ++-- examples/scratchpad.pl | 24 ++- src/Main.kt | 16 +- src/gpl | 2 +- src/interpreter/FileLoader.kt | 13 +- src/interpreter/Preprocessor.kt | 24 ++- src/io/Logger.kt | 15 +- src/io/Terminal.kt | 8 + src/parser/ScriptParser.kt | 8 +- src/parser/grammars/LogicGrammar.kt | 15 +- src/parser/grammars/TermsGrammar.kt | 49 ++---- src/parser/grammars/Tokens.kt | 2 + src/prolog/Program.kt | 82 +++------ src/prolog/Substitution.kt | 2 +- src/prolog/ast/Database.kt | 76 ++++++++ src/prolog/ast/arithmetic/Float.kt | 11 ++ src/prolog/ast/logic/Clause.kt | 47 +++-- src/prolog/ast/logic/Predicate.kt | 1 + src/prolog/ast/terms/Variable.kt | 13 +- src/prolog/builtins/io.kt | 4 + src/prolog/builtins/other.kt | 4 + src/prolog/builtins/unificationOperators.kt | 5 + src/prolog/logic/terms.kt | 53 ++++++ src/prolog/logic/unification.kt | 8 +- src/repl/Repl.kt | 22 ++- tests/compare.sh | 53 ++++++ tests/e2e/myClass.kt | 4 + tests/interpreter/PreprocessorTests.kt | 4 +- tests/interpreter/SourceFileReaderTests.kt | 4 - tests/parser/OperatorParserTests.kt | 13 ++ tests/parser/grammars/LogicGrammarTests.kt | 12 ++ tests/parser/grammars/TermsGrammarTests.kt | 15 +- tests/prolog/EvaluationTests.kt | 186 +++++++++++++++++++- tests/prolog/logic/TermsTests.kt | 109 ++++++++++++ 34 files changed, 746 insertions(+), 194 deletions(-) create mode 100644 src/prolog/ast/Database.kt create mode 100644 tests/compare.sh create mode 100644 tests/e2e/myClass.kt create mode 100644 tests/prolog/logic/TermsTests.kt diff --git a/build.gradle.kts b/build.gradle.kts index ea7f816..cd901a3 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,20 +28,26 @@ sourceSets { } } -tasks { - withType { - manifest { - attributes["Main-Class"] = "MainKt" - } - from(configurations.runtimeClasspath.get().map { - if (it.isDirectory) it else zipTree(it) - }) - } - - test { - useJUnitPlatform() - testLogging { - events("passed", "skipped", "failed") - } +tasks.named("test") { + useJUnitPlatform() + testLogging { + events("passed", "skipped", "failed") + } +} + +tasks.register("fatJar") { + manifest { + attributes["Main-Class"] = "MainKt" + } + duplicatesStrategy = DuplicatesStrategy.EXCLUDE + from(configurations.runtimeClasspath.get().map { + if (it.isDirectory) it else zipTree(it) + }) + with(tasks.jar.get() as CopySpec) +} + +tasks { + build { + dependsOn("fatJar") } } diff --git a/examples/scratchpad.pl b/examples/scratchpad.pl index 357e09b..b122c4f 100644 --- a/examples/scratchpad.pl +++ b/examples/scratchpad.pl @@ -1 +1,23 @@ -choice(X) :- X = 1, !; X = 2. +% choice(X) :- X = 1, !; X = 2. +grade(alice, a). +grade(bob, b). +grade(carol, a). +grade(dave, c). + +got_an_a(Student) :- + grade(Student, Grade), + Grade = a. + +did_not_get_an_a(Student) :- + grade(Student, Grade), + Grade \= a. + +:- initialization(main). + +main :- + write("While "), + got_an_a(X), + write(X), write(" got an A, "), fail; + write("but "), + did_not_get_an_a(Y), + write(Y), write(" did not get an A, "), fail; write("unfortunately."), nl. diff --git a/src/Main.kt b/src/Main.kt index cb40600..55a12bf 100644 --- a/src/Main.kt +++ b/src/Main.kt @@ -5,7 +5,7 @@ import io.GhentPrologArgParser import io.Logger import repl.Repl -fun main(args: Array) = mainBody { +fun main(args: Array) { // Parse command line arguments val parsedArgs = ArgParser(args).parseInto(::GhentPrologArgParser) @@ -22,21 +22,9 @@ fun main(args: Array) = mainBody { // Check if REPL was requested if (repl) { - Repl().start() + Repl() } else { Logger.warn("REPL not started. Use -r or --repl to start the REPL.") } } } - -fun help() { - println(""" - Ghent Prolog: A Prolog interpreter in Kotlin - - Options: - -s, --source Specify the source file to load - -r, --repl Start the REPL (default) - -v, --verb - -h, --help Show this help message - """.trimIndent()) -} diff --git a/src/gpl b/src/gpl index c1eecb1..714a5a2 100755 --- a/src/gpl +++ b/src/gpl @@ -20,7 +20,7 @@ fi if [ ! -f "${JAR_PATH}" ]; then printf 'Info: JAR file not found at "%s"\n' "${JAR_PATH}" printf 'Info: Building the project...\n' - ./gradlew build + ./gradlew fatJar if [ "${?}" -ne 0 ]; then printf 'Error: Build failed\n' exit 1 diff --git a/src/interpreter/FileLoader.kt b/src/interpreter/FileLoader.kt index 2cd7022..2121fd7 100644 --- a/src/interpreter/FileLoader.kt +++ b/src/interpreter/FileLoader.kt @@ -2,22 +2,27 @@ package interpreter import io.Logger import parser.ScriptParser +import prolog.ast.Database import prolog.Program import prolog.ast.logic.Clause class FileLoader { private val parser = ScriptParser() - fun load(filePath: String): () -> Unit { + fun load(filePath: String) { + Logger.info("Loading file: $filePath") + val input = readFile(filePath) Logger.debug("Parsing content of $filePath") val clauses: List = parser.parse(input) - Program.load(clauses) + val db = Database(filePath) + db.load(clauses) + Program.add(db) + db.initialize() - // TODO Pass next commands to execute - return {} + Logger.debug("Finished loading file: $filePath") } fun readFile(filePath: String): String { diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 7ee95d0..031cab9 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -47,7 +47,7 @@ open class Preprocessor { } } - protected open fun preprocess(term: Term): Term { + protected open fun preprocess(term: Term, nested: Boolean = false): Term { val prepped = when (term) { Atom("true") -> True Structure(Atom("true"), emptyList()) -> True @@ -61,7 +61,7 @@ open class Preprocessor { Atom("nl") -> Nl is Structure -> { // Preprocess the arguments first to recognize builtins - val args = term.arguments.map { preprocess(it) } + val args = term.arguments.map { preprocess(it, nested = true) } when { // TODO Remove hardcoding by storing the functors as constants in operators? @@ -77,7 +77,7 @@ open class Preprocessor { term.functor == "\\+/1" -> { Not(args[0] as Goal) } - // Arithmetic + term.functor == "=\\=/2" && args.all { it is Expression } -> { EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) } @@ -90,6 +90,16 @@ open class Preprocessor { Is(args[0] as Expression, args[1] as Expression) } + // Arithmetic + + term.functor == "=/2" && args.all { it is Expression } -> { + Unify(args[0] as Expression, args[1] as Expression) + } + + term.functor == "\\=/2" && args.all { it is Expression } -> { + NotUnify(args[0] as Expression, args[1] as Expression) + } + term.functor == "-/1" && args.all { it is Expression } -> { Negate(args[0] as Expression) } @@ -121,6 +131,7 @@ open class Preprocessor { // Other term.functor == "write/1" -> Write(args[0]) term.functor == "read/1" -> Read(args[0]) + term.functor == "initialization/1" -> Initialization(args[0] as Goal) else -> term } @@ -129,9 +140,10 @@ open class Preprocessor { else -> term } - if (prepped != term || prepped::class != term::class) { - Logger.debug("Preprocessed term: $term -> $prepped (is ${prepped::class.simpleName})") - } + Logger.debug( + "Preprocessed term $term into $prepped (kind ${prepped::class.simpleName})", + !nested && (prepped != term || prepped::class != term::class) + ) return prepped } diff --git a/src/io/Logger.kt b/src/io/Logger.kt index a0db3cc..ac9de5a 100644 --- a/src/io/Logger.kt +++ b/src/io/Logger.kt @@ -8,17 +8,18 @@ object Logger { val defaultLevel: Level = Level.WARN var level: Level = defaultLevel - private val io: IoHandler = Terminal() + private val io = Terminal() - fun log(message: String, messageLevel: Level = defaultLevel) { - if (level <= messageLevel) { + fun log(message: String, messageLevel: Level = defaultLevel, onlyIf: Boolean) { + if (level <= messageLevel && onlyIf) { + io.checkNewLine() val text = "$messageLevel: $message\n" io.say(text) } } - fun debug(message: String) = log(message, Level.DEBUG) - fun info(message: String) = log(message, Level.INFO) - fun warn(message: String) = log(message, Level.WARN) - fun error(message: String) = log(message, Level.ERROR) + fun debug(message: String, onlyIf: Boolean = true) = log(message, Level.DEBUG, onlyIf) + fun info(message: String, onlyIf: Boolean = true) = log(message, Level.INFO, onlyIf) + fun warn(message: String, onlyIf: Boolean = true) = log(message, Level.WARN, onlyIf) + fun error(message: String, onlyIf: Boolean = true) = log(message, Level.ERROR, onlyIf) } diff --git a/src/io/Terminal.kt b/src/io/Terminal.kt index ba12468..c75a3eb 100644 --- a/src/io/Terminal.kt +++ b/src/io/Terminal.kt @@ -1,5 +1,6 @@ package io +import prolog.Program import java.io.BufferedReader import java.io.BufferedWriter import java.io.InputStream @@ -60,4 +61,11 @@ class Terminal( error.close() System.exit(0) } + + fun checkNewLine() { + if (Program.storeNewLine) { + say("\n") + Program.storeNewLine = false + } + } } diff --git a/src/parser/ScriptParser.kt b/src/parser/ScriptParser.kt index a61a28c..f95731c 100644 --- a/src/parser/ScriptParser.kt +++ b/src/parser/ScriptParser.kt @@ -2,11 +2,17 @@ package parser import com.github.h0tk3y.betterParse.grammar.Grammar import com.github.h0tk3y.betterParse.grammar.parseToEnd +import interpreter.Preprocessor +import io.Logger import parser.grammars.LogicGrammar import prolog.ast.logic.Clause class ScriptParser: Parser { private val grammar: Grammar> = LogicGrammar() as Grammar> + private val preprocessor = Preprocessor() - override fun parse(input: String): List = grammar.parseToEnd(input) + override fun parse(input: String): List { + val raw = grammar.parseToEnd(input) + return preprocessor.preprocess(raw) + } } \ No newline at end of file diff --git a/src/parser/grammars/LogicGrammar.kt b/src/parser/grammars/LogicGrammar.kt index 10c3b82..396aa50 100644 --- a/src/parser/grammars/LogicGrammar.kt +++ b/src/parser/grammars/LogicGrammar.kt @@ -1,22 +1,21 @@ package parser.grammars -import com.github.h0tk3y.betterParse.combinators.oneOrMore -import com.github.h0tk3y.betterParse.combinators.or -import com.github.h0tk3y.betterParse.combinators.separated -import com.github.h0tk3y.betterParse.combinators.times -import com.github.h0tk3y.betterParse.combinators.unaryMinus -import com.github.h0tk3y.betterParse.combinators.use +import com.github.h0tk3y.betterParse.combinators.* import com.github.h0tk3y.betterParse.parser.Parser import prolog.ast.logic.Clause import prolog.ast.logic.Fact import prolog.ast.logic.Rule +import prolog.ast.terms.Atom class LogicGrammar : TermsGrammar() { + protected val constraint: Parser by (-neck * body) use { + Rule(Atom(""), this) + } protected val rule: Parser by (head * -neck * body) use { Rule(t1, t2) } protected val fact: Parser by head use { Fact(this) } - protected val clause: Parser by ((rule or fact) * -dot) + protected val clause: Parser by ((rule or constraint or fact) * -dot) protected val clauses: Parser> by oneOrMore(clause) override val rootParser: Parser by clauses -} \ No newline at end of file +} diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 9bac47c..52d4ef0 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -1,16 +1,10 @@ package parser.grammars -import com.github.h0tk3y.betterParse.combinators.or -import com.github.h0tk3y.betterParse.combinators.separated -import com.github.h0tk3y.betterParse.combinators.times -import com.github.h0tk3y.betterParse.combinators.unaryMinus -import com.github.h0tk3y.betterParse.combinators.use +import com.github.h0tk3y.betterParse.combinators.* import com.github.h0tk3y.betterParse.grammar.parser import com.github.h0tk3y.betterParse.parser.Parser -import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer -import prolog.ast.logic.LogicOperand import prolog.ast.terms.* open class TermsGrammar : Tokens() { @@ -37,42 +31,32 @@ open class TermsGrammar : Tokens() { protected val float: Parser by floatToken use { Float(text.toFloat()) } // Operators - protected val logOps: Parser by (dummy + protected val ops: Parser by (dummy + // Logic or comma or semicolon + // Arithmetic + or plus + or equals + or notEquals ) use { this.text } - protected val simpleLogicOperand: Parser by (dummy + protected val simpleOperand: Parser by (dummy + // Logic or compound or atom - ) - protected val logicOperand: Parser by (dummy - or parser(::logicOperator) - or simpleLogicOperand - ) - protected val logicOperator: Parser by (simpleLogicOperand * logOps * logicOperand) use { - CompoundTerm(Atom(t2), listOf(t1, t3)) - } - - protected val arithmeticOps: Parser by (dummy - or plus - ) use { this.text } - protected val simpleArithmeticOperand: Parser by (dummy + or variable + // Arithmetic or int or float ) - protected val arithmeticOperand: Parser by (dummy - or parser(::arithmeticOperator) - or simpleArithmeticOperand - ) use { this as Expression } - protected val arithmeticOperator: Parser by (simpleArithmeticOperand * arithmeticOps * arithmeticOperand) use { + protected val operand: Parser by (dummy + or parser(::operator) + or simpleOperand + ) + protected val operator: Parser by (simpleOperand * ops * operand) use { CompoundTerm(Atom(t2), listOf(t1, t3)) } - protected val operator: Parser by (dummy - or logicOperator - or arithmeticOperator - ) - // Parts protected val head: Parser by (dummy or compound @@ -81,6 +65,7 @@ open class TermsGrammar : Tokens() { protected val body: Parser by (dummy or operator or head + or variable ) use { this as Body } protected val term: Parser by (dummy diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index 14c5be9..cf55e09 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -22,6 +22,8 @@ abstract class Tokens : Grammar() { protected val rightParenthesis: Token by literalToken(")") protected val comma: Token by literalToken(",") protected val semicolon: Token by literalToken(";") + protected val equals: Token by literalToken("=") + protected val notEquals: Token by literalToken("\\=") protected val plus: Token by literalToken("+") protected val dot by literalToken(".") diff --git a/src/prolog/Program.kt b/src/prolog/Program.kt index 7bf9492..87e787e 100644 --- a/src/prolog/Program.kt +++ b/src/prolog/Program.kt @@ -1,32 +1,25 @@ package prolog import io.Logger +import prolog.ast.Database import prolog.ast.logic.Clause -import prolog.ast.logic.Predicate import prolog.ast.logic.Resolvent -import prolog.ast.terms.Functor import prolog.ast.terms.Goal -typealias Database = Program - /** - * Prolog Program or database. + * Object to handle execution + * + * This object is a singleton that manages a list of databases. */ -object Program: Resolvent { - var predicates: Map = emptyMap() +object Program : Resolvent { + private val internalDb = Database("") + private val databases: MutableList = mutableListOf(internalDb) - init { - Logger.debug("Initializing ${this::class.java.simpleName}") - setup() - Logger.debug("Initialization of ${this::class.java.simpleName} complete") - } + var storeNewLine: Boolean = false + var variableRenamingStart: Int = 0 - private fun setup() { - Logger.debug("Setting up ${this::class.java.simpleName}") - - // Initialize the program with built-in predicates - load(listOf( - )) + fun add(database: Database) { + databases.add(database) } /** @@ -35,51 +28,24 @@ object Program: Resolvent { */ fun query(goal: Goal): Answers = solve(goal, emptyMap()) - override fun solve(goal: Goal, subs: Substitutions): Answers { + override fun solve(goal: Goal, subs: Substitutions): Answers = sequence { Logger.debug("Solving goal $goal") - val functor = goal.functor - // If the predicate does not exist, return false - val predicate = predicates[functor] ?: return emptySequence() - // If the predicate exists, evaluate the goal against it - return predicate.solve(goal, subs) - } - - /** - * 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))) - } - - Logger.debug("Loaded clause $clause into predicate $functor") + for (database in databases) { + yieldAll(database.solve(goal, subs)) } } - 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 load(clauses: List) = internalDb.load(clauses) fun clear() { - Logger.debug("Clearing ${this::class.java.simpleName}") - predicates = emptyMap() - setup() + databases.forEach { it.clear() } + } + + fun clear(filePath: String) { + val correspondingDBs = databases.filter { it.sourceFile == filePath } + + require(correspondingDBs.isNotEmpty()) { "No database found for file: $filePath" } + + correspondingDBs.forEach { it.clear() } } } \ No newline at end of file diff --git a/src/prolog/Substitution.kt b/src/prolog/Substitution.kt index e9fb28b..062d63e 100644 --- a/src/prolog/Substitution.kt +++ b/src/prolog/Substitution.kt @@ -4,7 +4,7 @@ import prolog.ast.terms.Term abstract class Substitution(val from: Term, val to: Term) { val mapped: Pair? = if (from != to) from to to else null - override fun toString(): String = "$from -> $to" + override fun toString(): String = "$from |-> $to" } typealias Substitutions = Map typealias Answer = Result diff --git a/src/prolog/ast/Database.kt b/src/prolog/ast/Database.kt new file mode 100644 index 0000000..e295e39 --- /dev/null +++ b/src/prolog/ast/Database.kt @@ -0,0 +1,76 @@ +package prolog.ast + +import io.Logger +import prolog.Program +import prolog.Answers +import prolog.Substitutions +import prolog.ast.logic.Clause +import prolog.ast.logic.Predicate +import prolog.ast.logic.Resolvent +import prolog.ast.terms.Functor +import prolog.ast.terms.Goal + +/** + * Prolog Program or Database + */ +class Database(val sourceFile: String): Resolvent { + private var predicates: Map = emptyMap() + + fun initialize() { + Logger.info("Initializing database from $sourceFile") + if (predicates.contains("/_")) { + Logger.debug("Loading clauses from /_ predicate") + predicates["/_"]?.clauses?.forEach { + Logger.debug("Loading clause $it") + val goal = it.body as Goal + goal.satisfy(emptyMap()).toList() + } + } + } + + override fun solve(goal: Goal, subs: Substitutions): Answers { + val functor = goal.functor + // If the predicate does not exist, return false + val predicate = predicates[functor] ?: return emptySequence() + // If the predicate exists, evaluate the goal against it + return predicate.solve(goal, subs) + } + + /** + * 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))) + } + + Logger.debug("Loaded clause $clause into predicate $functor") + } + } + + 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 clear() { + Logger.debug("Clearing ${this::class.java.simpleName}") + predicates = emptyMap() + } +} \ No newline at end of file diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt index 3bbf694..da49530 100644 --- a/src/prolog/ast/arithmetic/Float.kt +++ b/src/prolog/ast/arithmetic/Float.kt @@ -31,4 +31,15 @@ class Float(override val value: kotlin.Float): Number { is Integer -> Float(value * other.value.toFloat()) else -> throw IllegalArgumentException("Cannot multiply $this and $other") } + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other !is Float) return false + if (value != other.value) return false + return true + } + + override fun hashCode(): Int { + return super.hashCode() + } } \ No newline at end of file diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index 58b2eb4..3bf4138 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -1,13 +1,13 @@ package prolog.ast.logic import prolog.Answers +import prolog.Program import prolog.Substitutions -import prolog.ast.terms.Body -import prolog.ast.terms.Functor -import prolog.ast.terms.Goal -import prolog.ast.terms.Head +import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut +import prolog.logic.applySubstitution +import prolog.logic.numbervars import prolog.logic.unifyLazy /** @@ -21,23 +21,39 @@ import prolog.logic.unifyLazy abstract class Clause(val head: Head, val body: Body) : Resolvent { val functor: Functor = head.functor - override fun solve (goal: Goal, subs: Substitutions): Answers = sequence { + override fun solve(goal: Goal, subs: Substitutions): Answers = sequence { // If the clause is a rule, unify the goal with the head and then try to prove the body. // Only if the body can be proven, the substitutions should be returned. // Do this in a lazy way. - unifyLazy(goal, head, subs).forEach { headAnswer -> - headAnswer.map { newHeadSubs -> + + // Since we are only interested in substitutions in the goal (as opposed to the head of this clause), + // we can use variable renaming and filter out the substitutions that are not in the goal. + val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs) + + val reverse = renamed.entries.associate { (a, b) -> b to a } + Program.variableRenamingStart = end + + var newSubs: Substitutions = subs + renamed + unifyLazy(goal, head, newSubs).forEach { headAnswer -> + headAnswer.map { headSubs -> // If the body can be proven, yield the (combined) substitutions - body.satisfy(subs + newHeadSubs).forEach { bodyAnswer -> + newSubs = subs + renamed + headSubs + body.satisfy(newSubs).forEach { bodyAnswer -> bodyAnswer.fold( - onSuccess = { newBodySubs -> - yield(Result.success(newHeadSubs + newBodySubs)) + onSuccess = { bodySubs -> + var result = (headSubs + bodySubs) + .mapKeys { reverse[it.key] ?: it.key } + .mapValues { reverse[it.value] ?: it.value } + result = result.map { it.key to applySubstitution(it.value, result) } + .toMap() + .filterNot { it.key in renamed.keys } + yield(Result.success(result)) }, onFailure = { error -> if (error is AppliedCut) { // Find single solution and return immediately if (error.subs != null) { - yield(Result.failure(AppliedCut(newHeadSubs + error.subs))) + yield(Result.failure(AppliedCut(headSubs + error.subs))) } else { yield(Result.failure(AppliedCut())) } @@ -52,10 +68,5 @@ abstract class Clause(val head: Head, val body: Body) : Resolvent { } } - override fun toString(): String { - return when { - body is True -> head.toString() - else -> "$head :- $body" - } - } -} \ No newline at end of file + override fun toString(): String = if (body is True) head.toString() else "$head :- $body" +} diff --git a/src/prolog/ast/logic/Predicate.kt b/src/prolog/ast/logic/Predicate.kt index 5bd9c17..236f286 100644 --- a/src/prolog/ast/logic/Predicate.kt +++ b/src/prolog/ast/logic/Predicate.kt @@ -51,6 +51,7 @@ class Predicate : Resolvent { 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 -> diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index 713c44d..0ef7ee6 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -1,10 +1,11 @@ package prolog.ast.terms +import prolog.Answers import prolog.Substitutions import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Simplification -data class Variable(val name: String) : Term, Expression { +data class Variable(val name: String) : Term, Body, Expression { override fun simplify(subs: Substitutions): Simplification { // If the variable is bound, return the value of the binding // If the variable is not bound, return the variable itself @@ -16,5 +17,15 @@ data class Variable(val name: String) : Term, Expression { return Simplification(this, result) } + override fun satisfy(subs: Substitutions): Answers { + // If the variable is bound, satisfy the bound term + if (this in subs) { + val boundTerm = subs[this]!! as Body + return boundTerm.satisfy(subs) + } + + return sequenceOf(Result.failure(IllegalArgumentException("Unbound variable: $this"))) + } + override fun toString(): String = name } \ No newline at end of file diff --git a/src/prolog/builtins/io.kt b/src/prolog/builtins/io.kt index d04f74d..3f9aaae 100644 --- a/src/prolog/builtins/io.kt +++ b/src/prolog/builtins/io.kt @@ -4,6 +4,7 @@ import io.Logger import io.Terminal import parser.ReplParser import prolog.Answers +import prolog.Program import prolog.Substitutions import prolog.ast.logic.Satisfiable import prolog.ast.terms.Atom @@ -21,6 +22,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis Terminal().say(t.toString()) + Program.storeNewLine = true + return sequenceOf(Result.success(emptyMap())) } } @@ -31,6 +34,7 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis object Nl : Atom("nl"), Satisfiable { override fun satisfy(subs: Substitutions): Answers { Terminal().say("\n") + Program.storeNewLine = false return sequenceOf(Result.success(emptyMap())) } } diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 9321880..8609473 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -6,6 +6,10 @@ import prolog.ast.logic.LogicOperand import prolog.ast.terms.Atom import prolog.ast.logic.LogicOperator +class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) { + override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1) +} + class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) { override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs) } diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index fc40df7..892c616 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -26,6 +26,11 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("=" } } +class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) { + private val not = Not(Unify(term1, term2)) + override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs) +} + class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) diff --git a/src/prolog/logic/terms.kt b/src/prolog/logic/terms.kt index 6bf2665..8d1eeb0 100644 --- a/src/prolog/logic/terms.kt +++ b/src/prolog/logic/terms.kt @@ -1,7 +1,10 @@ package prolog.logic +import prolog.Substitutions import prolog.ast.terms.Atom +import prolog.ast.terms.Structure import prolog.ast.terms.Term +import prolog.ast.terms.Variable /** * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose @@ -20,3 +23,53 @@ fun functor(term: Term, name: Atom, arity: Int): Boolean { // TODO Implement return true } + +/** + * Unify the free variables in Term with a term $VAR(N), where N is the number of the variable. + * Counting starts at Start. + * End is unified with the number that should be given to the next variable. + * + * Source: [SWI-Prolog Predicate numbervars/3](https://www.swi-prolog.org/pldoc/man?predicate=numbervars/3) + * + * @return Pair of the next number and only the new substitutions of variables to $VAR(N) + */ +fun numbervars( + term: Term, + start: Int = 0, + subs: Substitutions = emptyMap(), + sessionSubs: Substitutions = emptyMap() +): Pair { + when { + variable(term, subs) -> { + // All instances of the same variable are unified with the same term + if (term in sessionSubs) { + return Pair(start, emptyMap()) + } + + val from = term as Variable + var suggestedName = "${from.name}($start)" + // If the suggested name is already in use, find a new one + while ((subs + sessionSubs).filter { (it.key as Variable).name == suggestedName }.isNotEmpty()) { + val randomInfix = ((0..9) + ('a'..'z') + ('A'..'Z')).random() + suggestedName = "${from.name}_${randomInfix}_($start)" + } + return Pair(start + 1, mapOf(from to Variable(suggestedName))) + } + + compound(term, subs) -> { + val from = term as Structure + var n = start + val s: MutableMap = sessionSubs.toMutableMap() + from.arguments.forEach { arg -> + val (newN, newSubs) = numbervars(arg, n, subs, s) + n = newN + s += newSubs + } + return Pair(n, s) + } + + else -> { + return Pair(start, emptyMap()) + } + } +} diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 08b4d1c..68242b1 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -36,7 +36,7 @@ fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when } // Check if a variable occurs in a term -private fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when { +fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when { variable(term, subs) -> term == variable atomic(term, subs) -> false compound(term, subs) -> { @@ -53,18 +53,18 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val t2 = applySubstitution(term2, subs) when { - equivalent(t1, t2, subs) -> yield(Result.success(subs)) + equivalent(t1, t2, subs) -> yield(Result.success(emptyMap())) variable(t1, subs) -> { val variable = t1 as Variable if (!occurs(variable, t2, subs)) { - yield(Result.success(subs + (variable to t2))) + yield(Result.success(mapOf(term1 to t2))) } } variable(t2, subs) -> { val variable = t2 as Variable if (!occurs(variable, t1, subs)) { - yield(Result.success(subs + (variable to t1))) + yield(Result.success(mapOf(term2 to t1))) } } diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt index 5704cdc..a7c684a 100644 --- a/src/repl/Repl.kt +++ b/src/repl/Repl.kt @@ -6,14 +6,15 @@ import io.Terminal import parser.ReplParser import prolog.Answer import prolog.Answers +import prolog.Program class Repl { private val io = Terminal() private val parser = ReplParser() private val preprocessor = Preprocessor() - fun start() { - io.say("Prolog REPL. Type '^D' to quit.\n") + init { + welcome() while (true) { try { printAnswers(query()) @@ -23,15 +24,19 @@ class Repl { } } - fun query(): Answers { + private fun welcome() { + io.checkNewLine() + io.say("Prolog REPL. Type '^D' to quit.\n") + } + + private fun query(): Answers { val queryString = io.prompt("?-", { "| " }) val simpleQuery = parser.parse(queryString) val query = preprocessor.preprocess(simpleQuery) - Logger.debug("Satisfying query: $query") return query.satisfy(emptyMap()) } - fun printAnswers(answers: Answers) { + private fun printAnswers(answers: Answers) { val knownCommands = setOf(";", "a", ".", "h") val iterator = answers.iterator() @@ -68,7 +73,7 @@ class Repl { io.say("\n") } - fun help(): String { + private fun help(): String { io.say("Commands:\n") io.say(" ; find next solution\n") io.say(" a abort\n") @@ -77,12 +82,13 @@ class Repl { return "" } - fun prettyPrint(result: Answer): String { + private fun prettyPrint(result: Answer): String { result.fold( onSuccess = { val subs = result.getOrNull()!! if (subs.isEmpty()) { - return "true." + io.checkNewLine() + return "true.\n" } return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" } }, diff --git a/tests/compare.sh b/tests/compare.sh new file mode 100644 index 0000000..9bdadab --- /dev/null +++ b/tests/compare.sh @@ -0,0 +1,53 @@ +#!/usr/bin/env bash + +# This script is expected to be run from the root of the project. + +# Paths to the two implementations +GPL="src/gpl" +SPL="swipl" + +GPL_FLAGS=("--debug") +SPL_FLAGS=("--quiet" "-t" "'true'") + +# Directory containing test files +TEST_DIR="examples" + +# Temporary files for storing outputs +GPL_OUT=$(mktemp) +SPL_OUT=$(mktemp) + +# Flag to track if all tests pass +PASSED=0 +FAILED=0 + +# Iterate over all test files in the test directory +#for TESTFILE in $(find ${TEST_DIR} -type f); do +files=("examples/program.pl" "examples/basics/disjunction.pl" "examples/basics/fraternity.pl") +for TESTFILE in "${files[@]}"; do + # Run both programs with the test file + "${SPL}" "${SPL_FLAGS[@]}" "$TESTFILE" > "${SPL_OUT}" 2>&1 + "${GPL}" "${GPL_FLAGS[@]}" -s "$TESTFILE" > "${GPL_OUT}" 2>&1 + + # Compare the outputs + if diff -q "$SPL_OUT" "$GPL_OUT" > /dev/null; then + PASSED=$((PASSED + 1)) + else + echo "Test failed! Outputs differ for $TESTFILE" + printf "\nTest:\n%s\n" "$(cat "$TESTFILE")" + printf "\nExpected:\n%s\n" "$(cat "$SPL_OUT")" + printf "\nGot:\n%s\n" "$(cat "$GPL_OUT")" + echo "-----------------------------------------" + FAILED=$((FAILED + 1)) + fi +done + +# Clean up temporary files +rm "$SPL_OUT" "$GPL_OUT" + +# Final result, summary +if [ $FAILED -eq 0 ]; then + echo "All tests passed!" +else + printf "Tests passed: %d\nTests failed: %d\n" "$PASSED" "$FAILED" + exit 1 +fi diff --git a/tests/e2e/myClass.kt b/tests/e2e/myClass.kt new file mode 100644 index 0000000..f5ff7c3 --- /dev/null +++ b/tests/e2e/myClass.kt @@ -0,0 +1,4 @@ +package e2e + +class myClass { +} \ No newline at end of file diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index ed2862b..3f3ad3f 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -12,8 +12,8 @@ import prolog.builtins.* class PreprocessorTests { class OpenPreprocessor : Preprocessor() { - public override fun preprocess(input: Term): Term { - return super.preprocess(input) + public override fun preprocess(term: Term, nested: Boolean): Term { + return super.preprocess(term, nested) } } diff --git a/tests/interpreter/SourceFileReaderTests.kt b/tests/interpreter/SourceFileReaderTests.kt index 55fc73a..55cdbcc 100644 --- a/tests/interpreter/SourceFileReaderTests.kt +++ b/tests/interpreter/SourceFileReaderTests.kt @@ -16,8 +16,6 @@ class SourceFileReaderTests { val reader = FileLoader() reader.readFile(inputFile) - - println(Program.predicates) } @Test @@ -26,7 +24,5 @@ class SourceFileReaderTests { val reader = FileLoader() reader.readFile(inputFile) - - println(Program.predicates) } } \ No newline at end of file diff --git a/tests/parser/OperatorParserTests.kt b/tests/parser/OperatorParserTests.kt index 8cfdb95..a8bedb0 100644 --- a/tests/parser/OperatorParserTests.kt +++ b/tests/parser/OperatorParserTests.kt @@ -26,4 +26,17 @@ class OperatorParserTests { assertEquals(Structure(Atom(","), listOf(Atom("a"), Atom("b"))), result, "Expected atom 'a, b'") } + + class BodyParser : TermsGrammar() { + override val rootParser: Parser by body + } + + @Test + fun `parse equality`() { + val input = "a = b" + + val result = BodyParser().parseToEnd(input) + + assertEquals(Structure(Atom("="), listOf(Atom("a"), Atom("b"))), result, "Expected atom 'a = b'") + } } \ No newline at end of file diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index 9afb439..d7e054e 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -129,4 +129,16 @@ class LogicGrammarTests { val conjunction = rule.body as CompoundTerm assertEquals("invited/2", (conjunction.arguments[0] as CompoundTerm).functor, "Expected functor 'invited/2'") } + + @Test + fun `parse constraints`() { + val input = ":- a." + + val result = parser.parseToEnd(input) + + assertEquals(1, result.size, "Expected 1 rule") + assertTrue(result[0] is Rule, "Expected a rule") + val rule = result[0] as Rule + assertEquals("/_", rule.head.functor, "Expected a constraint") + } } \ No newline at end of file diff --git a/tests/parser/grammars/TermsGrammarTests.kt b/tests/parser/grammars/TermsGrammarTests.kt index 203eac2..9acbdfd 100644 --- a/tests/parser/grammars/TermsGrammarTests.kt +++ b/tests/parser/grammars/TermsGrammarTests.kt @@ -2,9 +2,12 @@ package parser.grammars import com.github.h0tk3y.betterParse.grammar.Grammar import com.github.h0tk3y.betterParse.grammar.parseToEnd +import com.github.h0tk3y.betterParse.parser.Parser import org.junit.jupiter.api.Assertions +import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertDoesNotThrow import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.ValueSource import prolog.ast.arithmetic.Float @@ -14,6 +17,7 @@ import prolog.ast.terms.Structure import prolog.ast.terms.Term import prolog.ast.terms.Variable import prolog.logic.equivalent +import kotlin.test.assertEquals class TermsGrammarTests { private lateinit var parser: Grammar @@ -167,9 +171,12 @@ class TermsGrammarTests { val result = parser.parseToEnd(input) - Assertions.assertTrue( - equivalent(Float(-42.0f), result, emptyMap()), - "Expected float '-42.0'" - ) + assertEquals(Float(-42.0f), result, "Expected float '-42.0'") + } + + @ParameterizedTest + @ValueSource(strings = ["got_an_a(Student)", "grade(Student, Grade)"]) + fun `parse unification`(input: String) { + assertDoesNotThrow { parser.parseToEnd(input) } } } \ No newline at end of file diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index 6fd5fe5..cab3d0a 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/tests/prolog/EvaluationTests.kt @@ -2,6 +2,7 @@ package prolog import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Nested import org.junit.jupiter.api.Test import prolog.ast.logic.Fact import prolog.ast.logic.Rule @@ -108,9 +109,9 @@ class EvaluationTests { val parent = Rule( Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */ Disjunction( - Structure(Atom("father"), listOf(variable1, variable2)), - /* ; */ - Structure(Atom("mother"), listOf(variable1, variable2)) + Structure(Atom("father"), listOf(variable1, variable2)), + /* ; */ + Structure(Atom("mother"), listOf(variable1, variable2)) ) ) @@ -212,7 +213,182 @@ class EvaluationTests { assertEquals(expectedResults.size, actualResults.size, "Number of results should match") for (i in expectedResults.indices) { assertEquals(expectedResults[i].size, actualResults[i].getOrNull()!!.size, "Substitution size should match") - assertTrue(expectedResults[i].all { actualResults[i].getOrNull()!![it.key]?.let { it1 -> equivalent(it.value, it1, emptyMap()) } ?: false }, "Substitution values should match") + assertTrue(expectedResults[i].all { + actualResults[i].getOrNull()!![it.key]?.let { it1 -> + equivalent( + it.value, + it1, + emptyMap() + ) + } ?: false + }, "Substitution values should match") } } -} \ No newline at end of file + + @Test + fun `likes(alice, pizza)`() { + val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))) + val goal = Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))) + + Program.load(listOf(fact)) + + val result = Program.query(goal).toList() + + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + val subs = result[0].getOrNull()!! + assertEquals(0, subs.size, "Expected no substitutions") + } + + @Test + fun `likes(Person, pizza)`() { + val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))) + val goal = Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza"))) + + Program.load(listOf(fact)) + + val result = Program.query(goal).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("alice"), subs[Variable("Person")], "Expected Person to be alice") + } + + @Test + fun `likes_food(alice)`() { + val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))) + val rule = Rule( + Structure(Atom("likes_food"), listOf(Variable("Person"))), + Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza"))) + ) + + val goal = Structure(Atom("likes_food"), listOf(Atom("alice"))) + + Program.load(listOf(fact, rule)) + + val result = Program.query(goal).toList() + + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + val subs = result[0].getOrNull()!! + assertEquals(0, subs.size, "Expected no substitutions") + } + + @Test + fun `likes_food(Person)`() { + val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))) + val rule = Rule( + Structure(Atom("likes_food"), listOf(Variable("Person"))), + Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza"))) + ) + + val goal = Structure(Atom("likes"), listOf(Variable("X"), Atom("pizza"))) + + Program.load(listOf(fact, rule)) + + val result = Program.query(goal).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("alice"), subs[Variable("X")], "Expected Person to be alice") + } + + @Test + fun `requires querying exact`() { + val fact1 = Fact(Atom("a")) + val fact2 = Fact(Atom("b")) + val rule1 = Rule( + Atom("c"), + Conjunction( + Atom("a"), + Atom("b") + ) + ) + + Program.load(listOf(fact1, fact2, rule1)) + + val result = Program.query(Atom("c")).toList() + + assertEquals(1, result.size, "Expected 1 result") + } + + @Test + fun `requires querying with variable`() { + val fact1 = Fact(Atom("a")) + val fact2 = Fact(Atom("b")) + val rule1 = Rule( + Structure(Atom("has fact"), listOf(Variable("X"))), + Variable("X") + ) + + Program.load(listOf(fact1, fact2, rule1)) + + val result = Program.query(Structure(Atom("has fact"), listOf(Atom("a")))).toList() + + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + val subs = result[0].getOrNull()!! + assertEquals(0, subs.size, "Expected no substitutions") + } + + @Nested + class `requires querying with filled variable` { + @BeforeEach + fun setup() { + val fact1 = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))) + val fact2 = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pasta")))) + val fact3 = Fact(Structure(Atom("likes"), listOf(Atom("bob"), Atom("pasta")))) + val rule1 = Rule( + Structure(Atom("likes_italian_food"), listOf(Variable("Person"))), + Disjunction( + Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza"))), + Structure(Atom("likes"), listOf(Variable("Person"), Atom("pasta"))) + ) + ) + + Program.clear() + Program.load(listOf(fact1, fact2, fact3, rule1)) + } + + @Test + fun `likes_italian_food(alice)`() { + val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Atom("alice")))).toList() + + assertEquals(2, result.size, "Expected 2 results") + + assertTrue(result[0].isSuccess, "Expected success") + val subs1 = result[0].getOrNull()!! + assertEquals(0, subs1.size, "Expected no substitutions") + + assertTrue(result[1].isSuccess, "Expected success") + val subs2 = result[1].getOrNull()!! + assertEquals(0, subs2.size, "Expected no substitutions") + } + + @Test + fun `likes_italian_food(X)`() { + val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Variable("X")))).toList() + + assertEquals(3, result.size, "Expected 3 results") + + assertTrue(result[0].isSuccess, "Expected success") + val subs3 = result[0].getOrNull()!! + assertEquals(1, subs3.size, "Expected 1 substitution, especially without 'Person'") + assertEquals(Atom("alice"), subs3[Variable("X")], "Expected alice") + + assertTrue(result[1].isSuccess, "Expected success") + val subs4 = result[1].getOrNull()!! + assertEquals(1, subs4.size, "Expected 1 substitution, especially without 'Person'") + assertEquals(Atom("alice"), subs4[Variable("X")], "Expected alice") + + assertTrue(result[2].isSuccess, "Expected success") + val subs5 = result[2].getOrNull()!! + assertEquals(1, subs5.size, "Expected 1 substitution, especially without 'Person'") + assertEquals(Atom("bob"), subs5[Variable("X")], "Expected bob") + } + } +} diff --git a/tests/prolog/logic/TermsTests.kt b/tests/prolog/logic/TermsTests.kt new file mode 100644 index 0000000..f67f46a --- /dev/null +++ b/tests/prolog/logic/TermsTests.kt @@ -0,0 +1,109 @@ +package prolog.logic + +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable + +class TermsTests { + @Test + fun `rename vars in atom`() { + val term = Atom("a") + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start, end, "Expected end to still be at start") + assertTrue(subs.isEmpty(), "Expected no substitutions") + } + + @Test + fun `rename vars in var`() { + val term = Variable("X") + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start + 1, end, "Expected end to be incremented by 1") + assertEquals(1, subs.size, "Expected one substitution") + assertTrue(subs.containsKey(term), "Expected subs to contain the original term") + assertEquals(Variable("X($start)"), subs[term], "Expected subs to contain the new term") + } + + @Test + fun `rename vars in compound term without vars`() { + val term = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start, end, "Expected end to still be at start") + assertTrue(subs.isEmpty(), "Expected no substitutions") + } + + @Test + fun `rename vars in compound term`() { + val term = Structure(Atom("f"), listOf(Variable("X"), Variable("Y"))) + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start + 2, end, "Expected end to be incremented by 2") + assertEquals(2, subs.size, "Expected two substitutions") + assertTrue(subs.containsKey(term.arguments[0]), "Expected subs to contain the first original term") + assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term") + assertTrue(subs.containsKey(term.arguments[1]), "Expected subs to contain the second original term") + assertEquals(Variable("Y(${start + 1})"), subs[term.arguments[1]], "Expected subs to contain the new term") + } + + @Test + fun `renaming identical vars should keep the same name`() { + val term = Structure(Atom("f"), listOf(Variable("X"), Variable("X"))) + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start + 1, end, "Expected end to be incremented by 1") + assertEquals(1, subs.size, "Expected one substitution") + assertTrue(subs.containsKey(term.arguments[0]), "Expected subs to contain the first original term") + assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term") + assertTrue(subs.containsKey(term.arguments[1]), "Expected subs to contain the second original term") + assertEquals(Variable("X($start)"), subs[term.arguments[1]], "Expected subs to contain the new term") + } + + @Test + fun `renaming identical vars should keep the same name in nested terms`() { + val term = Structure(Atom("f"), listOf(Variable("X"), Structure(Atom("g"), listOf(Variable("X"))))) + val start = 0 + + val (end, subs) = numbervars(term, start) + + assertEquals(start + 1, end, "Expected end to be incremented by 1") + assertEquals(1, subs.size, "Expected one substitution") + assertTrue(subs.containsKey(Variable("X")), "Expected subs to contain the variable") + assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term") + } + + @Test + fun `renaming multiple times`() { + val variable = Variable("X") + val term = Structure(Atom("f"), listOf(variable)) + val start = 0 + + val (end1, subs1) = numbervars(term, start, emptyMap()) + + assertEquals(start + 1, end1, "Expected end to be incremented by 1") + assertEquals(1, subs1.size, "Expected one substitution") + assertTrue(subs1.containsKey(variable), "Expected subs to contain the variable") + assertEquals(Variable("X($start)"), subs1[variable], "Expected subs to contain the new term") + + val (end2, subs2) = numbervars(term, end1, subs1) + + assertEquals(start + 2, end2, "Expected end to be incremented by 2") + assertEquals(1, subs2.size, "Expected one substitution") + assertTrue(subs2.containsKey(variable), "Expected subs to contain the variable") + assertEquals(Variable("X($end1)"), subs2[variable], "Expected subs to contain the new term") + } +} \ No newline at end of file