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

Compare commits

base: tdpeuter:095659cf30945701312249c8af661b818b984a8a
Branches Tags
tdpeuter:main
tdpeuter:sync
..
compare: tdpeuter:a937b1bc4479b3c793bacf1b924dcad58b280ef1
Branches Tags
tdpeuter:main
tdpeuter:sync

19 commits
095659cf30 ... a937b1bc44

Author SHA1 Message Date
Tibo De Peuter
a937b1bc44
Sync 2025-05-05 00:18:38 +02:00
Tibo De Peuter
a85169dced
Checkpoint 2025-05-04 21:50:58 +02:00
Tibo De Peuter
5bfa1691dd
Retract 2025-05-02 23:50:29 +02:00
Tibo De Peuter
80fb3d1e60
Assert{a,z,} 2025-05-02 21:51:34 +02:00
Tibo De Peuter
f9017da734
Checkpoint 2025-05-02 13:28:00 +02:00
Tibo De Peuter
23b2ce9362
test: Fix failing 2025-05-02 09:09:23 +02:00
Tibo De Peuter
724e911a6f
Checkpoint 2025-05-01 21:16:48 +02:00
Tibo De Peuter
9db1c66781
Checkpoint 2025-05-01 17:13:35 +02:00
Tibo De Peuter
43b364044e
Quoted atoms 2025-04-30 12:08:36 +02:00
Tibo De Peuter
1e087c8339
Fix double printing 2025-04-30 10:52:58 +02:00
Tibo De Peuter
bfb509f41f
Arithmetic ops parsing 2025-04-30 09:18:46 +02:00
Tibo De Peuter
0a32797df1
test: Rule met cut 2025-04-29 15:47:00 +02:00
Tibo De Peuter
8e6a34a231
Argument parsing 2025-04-28 13:36:24 +02:00
Tibo De Peuter
32165a90f5
Arithmetic preprocessing 2025-04-28 12:20:03 +02:00
Tibo De Peuter
174855d7a3
Preprocessing 2025-04-27 22:02:50 +02:00
Tibo De Peuter
82a8fccf87
IO Operators 2025-04-27 20:11:15 +02:00
Tibo De Peuter
b9f419a59d
Rework parsing structure 2025-04-27 19:31:29 +02:00
Tibo De Peuter
a4ec29f084
Remove old lexer+parser implementation 2025-04-27 18:22:03 +02:00
Tibo De Peuter
d5632e9217
feat: Write 2025-04-27 14:47:56 +02:00
89 changed files with 3979 additions and 1802 deletions
Download patch file Download diff file Expand all files Collapse all files

8
.idea/2025LogProg-PrologInterpreter.iml generated Normal file
View file

@ -0,0 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
<module version="4">
<component name="AdditionalModuleElements">
<content url="file://$MODULE_DIR$" dumb="true">
<sourceFolder url="file://$MODULE_DIR$/examples" type="java-resource" />
</content>
</component>
</module>

8
.idea/modules.xml generated Normal file
View file

@ -0,0 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="ProjectModuleManager">
<modules>
<module fileurl="file://$PROJECT_DIR$/.idea/2025LogProg-PrologInterpreter.iml" filepath="$PROJECT_DIR$/.idea/2025LogProg-PrologInterpreter.iml" />
</modules>
</component>
</project>

38
build.gradle.kts
View file

@ -10,6 +10,8 @@ repositories {
}
dependencies {
// CLI argument parsing
implementation("com.xenomachina:kotlin-argparser:2.0.7")
// Parser combinator library
implementation("com.github.h0tk3y.betterParse:better-parse:0.4.4")
@ -26,20 +28,26 @@ sourceSets {
}
}
tasks {
withType<Jar> {
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>("test") {
useJUnitPlatform()
testLogging {
events("passed", "skipped", "failed")
}
}
tasks.register<Jar>("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")
}
}

33
examples/scratchpad.pl
View file

@ -1 +1,32 @@
choice(X) :- X = 1, !; X = 2.
% choice(X) :- X = 1, !; X = 2.
:- dynamic declaration/1.
add_declaration_first(NewDecl) :-
asserta(declaration(NewDecl)).
add_declaration_last(NewDecl) :-
assertz(declaration(NewDecl)).
database :-
add_declaration_first('Man is born free, and everywhere he is in chains.'),
retract(declaration(_)),
add_declaration_last('The revolution devours its own children.'),
add_declaration_first('I disapprove of what you say, but I will defend to the death your right to say it.'),
add_declaration_first('Give me Liberty, or give me Death!'),
add_declaration_last('So this is how liberty dies, with thunderous applause.').
show_declarations :-
declaration(Decl),
write(Decl), nl,
fail.
show_declarations.
:- initialization(main).
main :-
database,
show_declarations,
retractall(declaration(_)),
show_declarations.

3
src/Debug.kt
View file

@ -1,3 +0,0 @@
data object Debug {
val on: Boolean = true
}

118
src/Main.kt
View file

@ -1,107 +1,29 @@
import better_parser.SimpleReplParser
import interpreter.SourceFileReader
import prolog.Answer
import kotlin.system.exitProcess
import com.xenomachina.argparser.ArgParser
import interpreter.FileLoader
import io.GhentPrologArgParser
import io.Logger
import repl.Repl
fun help(): String {
println("Unknown command. Type 'h' for help.")
println("Commands:")
println(" ; - find next solution")
println(" a - abort")
println(" . - end query")
println(" h - help")
println(" exit - exit Prolog REPL")
return ""
}
fun main(args: Array<String>) {
// Parse command line arguments
val parsedArgs = ArgParser(args).parseInto(::GhentPrologArgParser)
fun say(message: String) {
println(message)
}
parsedArgs.run {
val loader = FileLoader()
fun prompt(message: String): String {
print("$message ")
var input = readlnOrNull()
// Set the verbosity level
Logger.level = verbosity
while (input.isNullOrBlank()) {
if (input == null) {
println("Exiting Prolog REPL.")
exitProcess(0)
// Check if script was provided
for (file in script) {
loader.load(file)
}
if (input.isBlank()) {
print("$message ")
}
input = readlnOrNull()
}
if (input == "exit") {
println("Exiting Prolog REPL.")
exitProcess(0)
}
return input
}
fun prettyResult(result: Answer): String {
result.fold(
onSuccess = {
val subs = result.getOrNull()!!
if (subs.isEmpty()) {
return "true."
}
return subs.entries.joinToString(", ") { "${it.key} = ${it.value}" }
},
onFailure = {
return "Failure: ${result.exceptionOrNull()!!}"
}
)
}
val knownCommands = setOf(";", "a", ".")
fun main() {
SourceFileReader().readFile("tests/better_parser/resources/parent.pl")
val parser = SimpleReplParser(debug = false)
say("Prolog REPL. Type 'exit' to quit.")
while (true) {
val queryString = prompt("?-")
try {
val query = parser.parse(queryString)
val answers = query.satisfy(emptyMap())
if (answers.none()) {
say("false.")
} else {
val iterator = answers.iterator()
var previous = iterator.next()
while (iterator.hasNext()) {
var command = prompt(prettyResult(previous))
while (command !in knownCommands) {
say("Unknown action: $command (h for help)")
command = prompt("Action?")
}
when (command) {
";" -> previous = iterator.next()
"a" -> break
"." -> break
}
}
say(prettyResult(previous))
}
} catch (e: Exception) {
println("Error: ${e.message}")
// Check if REPL was requested
if (repl) {
Repl()
} else {
Logger.warn("REPL not started. Use -r or --repl to start the REPL.")
}
}
}

17
src/better_parser/PrologParser.kt
View file

@ -1,17 +0,0 @@
package better_parser
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import prolog.Program
import prolog.ast.logic.Clause
import prolog.ast.terms.Atom
class PrologParser {
private val parser: Grammar<List<Clause>> = SimpleSourceParser() as Grammar<List<Clause>>
public fun parse(input: String) {
val clauses: List<Clause> = parser.parseToEnd(input)
Program.load(clauses)
}
}

70
src/better_parser/PrologSourceParser.kt
View file

@ -1,70 +0,0 @@
package better_parser
import com.github.h0tk3y.betterParse.combinators.*
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.lexer.literalToken
import com.github.h0tk3y.betterParse.lexer.regexToken
import com.github.h0tk3y.betterParse.parser.Parser
import prolog.ast.logic.Fact
import prolog.ast.arithmetic.Integer
import prolog.ast.arithmetic.Float
import prolog.ast.logic.Clause
import prolog.ast.logic.LogicOperand
import prolog.ast.logic.Rule
import prolog.ast.terms.*
import prolog.builtins.Conjunction
import prolog.builtins.Disjunction
class PrologSourceParser : Grammar<List<Clause>>() {
// Define the tokens
private val atom by regexToken("[a-z][a-zA-Z0-9_]*")
private val variable by regexToken("[A-Z][a-zA-Z0-9_]*")
private val number by regexToken("-?[0-9]+(\\.[0-9]+)?")
private val whitespace by regexToken("\\s+", ignore = true)
private val comma by literalToken(",")
private val semicolon by literalToken(";")
private val neck by literalToken(":-")
private val lparen by literalToken("(")
private val rparen by literalToken(")")
private val dot by literalToken(".")
private val atomParser by atom use { Atom(text) }
private val variableParser by variable use { Variable(text) }
private val intParser by number use { Integer(text.toInt()) }
private val floatParser by number use { Float(text.toFloat()) }
private val numberParser by (intParser or floatParser)
private val compoundTermParser by (atomParser and skip(lparen) and separated(
atomParser or variableParser,
comma
) and skip(rparen)) use {
CompoundTerm(t1, t2.terms)
}
private val termParser: Parser<Term> by (numberParser or variableParser or compoundTermParser or atomParser)
private val logicOperandParser: Parser<LogicOperand> by (termParser or compoundTermParser or atomParser) map {
it as LogicOperand
}
private val conjunctionParser: Parser<Conjunction> by (logicOperandParser and comma and logicOperandParser) use {
Conjunction(t1, t3)
}
private val disjunctionParser: Parser<Disjunction> by (logicOperandParser and semicolon and logicOperandParser) use {
Disjunction(t1, t3)
}
private val operatorParser: Parser<Operator> by (conjunctionParser or disjunctionParser)
private val headParser by (compoundTermParser or atomParser)
private val bodyParser by (operatorParser or compoundTermParser or atomParser)
private val factParser by (headParser and dot) use { Fact(t1 as Head) }
private val ruleParser by (headParser and neck and bodyParser and dot) use {
Rule(t1 as Head, t3 as Body)
}
private val clauseParser: Parser<Clause> by (factParser or ruleParser)
override val rootParser: Parser<List<Clause>> by zeroOrMore(clauseParser)
}

67
src/better_parser/SimplePrologParser.kt
View file

@ -1,67 +0,0 @@
package better_parser
import com.github.h0tk3y.betterParse.combinators.*
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parser
import com.github.h0tk3y.betterParse.lexer.Token
import com.github.h0tk3y.betterParse.lexer.literalToken
import com.github.h0tk3y.betterParse.lexer.regexToken
import com.github.h0tk3y.betterParse.lexer.token
import com.github.h0tk3y.betterParse.parser.Parser
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
open class SimplePrologParser : Grammar<Any>() {
// Prolog tokens
protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*")
protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*")
// Arithmetic tokens
private val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+")
private val integerToken: Token by regexToken("-?([1-9][0-9]*|0)")
// Special tokens
protected val neck by literalToken(":-")
protected val comma: Token by literalToken(",")
protected val leftParenthesis: Token by literalToken("(")
protected val rightParenthesis: Token by literalToken(")")
protected val dot by literalToken(".")
// Ignored tokens
protected val whitespace: Token by regexToken("\\s+", ignore = true)
protected val singleLineComment: Token by regexToken("%[^\\n]*", ignore = true)
protected val multiLineComment: Token by regexToken("/\\*.*?\\*/", ignore = true)
protected val dummy by token { _, _ -> -1 } use { throw IllegalStateException("This parser should not be used") }
// Prolog parsers
protected val variable: Parser<Variable> by variableToken use { Variable(text) }
protected val atom: Parser<Atom> by nameToken use { Atom(text) }
protected val compound: Parser<Structure> by (atom and skip(leftParenthesis) and separated(
parser(::term),
comma,
acceptZero = true
) and skip(rightParenthesis)) use {
Structure(t1, t2.terms)
}
// Arithmetic parsers
private val int: Parser<Integer> by integerToken use { Integer(text.toInt()) }
private val float: Parser<Float> by floatToken use {
Float(text.toFloat())
}
protected val term: Parser<Term> by (dummy
or float
or int
or variable
or compound
or atom
) map { it }
override val rootParser: Parser<Any> = term
}

27
src/better_parser/SimpleReplParser.kt
View file

@ -1,27 +0,0 @@
package better_parser
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.grammar.parseToEnd
import com.github.h0tk3y.betterParse.parser.Parser
import prolog.ast.logic.LogicOperand
import prolog.builtins.Query
class SimpleReplParser(val debug: Boolean = false) : SimpleSourceParser() {
override val rootParser: Parser<Query> by (body * -dot) use { Query(this as LogicOperand) }
fun parse(input: String): Query {
if (debug) {
println("Parsing input: $input")
}
val query = parseToEnd(input) as Query
if (debug) {
println("Parsed query: $query")
}
return query
}
}

48
src/better_parser/SimpleSourceParser.kt
View file

@ -1,48 +0,0 @@
package better_parser
import com.github.h0tk3y.betterParse.combinators.*
import com.github.h0tk3y.betterParse.grammar.parser
import com.github.h0tk3y.betterParse.lexer.literalToken
import com.github.h0tk3y.betterParse.parser.Parser
import prolog.ast.arithmetic.ArithmeticOperator
import prolog.ast.logic.*
import prolog.ast.terms.*
import prolog.builtins.Conjunction
import prolog.builtins.Disjunction
open class SimpleSourceParser : SimplePrologParser() {
protected val simpleLogicOperand: Parser<LogicOperand> by (dummy
or compound
or atom
)
protected val logicOperand: Parser<LogicOperand> by (dummy
or parser(::operator)
or simpleLogicOperand
)
protected val arithmeticOperator: Parser<ArithmeticOperator> by dummy
protected val logicOperator: Parser<LogicOperator> by (simpleLogicOperand * comma * logicOperand) use {
Conjunction(t1, t3)
}
protected val operator: Parser<Operator> by (arithmeticOperator or logicOperator) use { this as Operator }
protected val head: Parser<Head> by (dummy
or compound
or atom
)
protected val body: Parser<Body> by (dummy
or operator
or head
) use { this as Body }
// ----
private val rule: Parser<Rule> by (head * -neck * body) use { Rule(t1, t2) }
private val fact: Parser<Fact> by head use { Fact(this) }
private val clause: Parser<Clause> by ((rule or fact) * -dot)
private val clauses: Parser<List<Clause>> by zeroOrMore(clause)
override val rootParser: Parser<Any> by clauses
}

2
src/gpl
View file

@ -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

55
src/interpreter/FileLoader.kt Normal file
View file

@ -0,0 +1,55 @@
package interpreter
import io.Logger
import parser.ScriptParser
import prolog.ast.Database
import prolog.ast.Database.Program
import prolog.ast.logic.Clause
import prolog.ast.logic.Predicate
class FileLoader {
private val parser = ScriptParser()
fun load(filePath: String) {
Logger.info("Loading file: $filePath")
val input = readFile(filePath)
Logger.debug("Parsing content of $filePath")
val clauses: List<Clause> = parser.parse(input)
Logger.debug("Adding clauses to program")
addToProgram(clauses, filePath)
Logger.debug("Finished loading file: $filePath")
}
fun readFile(filePath: String): String {
try {
Logger.debug("Reading $filePath")
val file = java.io.File(filePath)
if (!file.exists()) {
Logger.error("File $filePath does not exist")
throw IllegalArgumentException("File not found: $filePath")
}
return file.readText()
} catch (e: Exception) {
Logger.error("Error reading file: $filePath")
throw RuntimeException("Error reading file: $filePath", e)
}
}
fun addToProgram(clauses: List<Clause>, filePath: String) {
Logger.debug("Grouping clauses by functor")
val groupedClauses = clauses.groupBy { it.functor }
val predicates: List<Predicate> = groupedClauses.map { (_, clauses) ->
Predicate(clauses)
}
val database = Database(filePath)
predicates.forEach { database.load(it) }
Program.consult(database)
}
}

141
src/interpreter/Preprocessor.kt Normal file
View file

@ -0,0 +1,141 @@
package interpreter
import io.Logger
import prolog.ast.arithmetic.Expression
import prolog.ast.arithmetic.Integer
import prolog.ast.logic.Clause
import prolog.ast.logic.Fact
import prolog.ast.logic.LogicOperand
import prolog.ast.logic.Rule
import prolog.ast.terms.*
import prolog.builtins.*
/**
* Preprocessor for Prolog
*
* This class preprocesses Prolog code and applies various transformations such as recognizing builtins.
*/
open class Preprocessor {
/**
* Preprocesses the input Prolog code.
*
* @param input The already parsed Prolog code as a list of clauses.
* @return The preprocessed Prolog code as a list of clauses.
*/
fun preprocess(input: List<Clause>): List<Clause> {
return input.map { preprocess(it) }
}
fun preprocess(input: Query): Query {
return Query(preprocess(input.query) as Goal)
}
private fun preprocess(clause: Clause): Clause {
return when (clause) {
is Fact -> {
Fact(preprocess(clause.head) as Head)
}
is Rule -> {
Rule(
preprocess(clause.head) as Head,
preprocess(clause.body as Term) as Body
)
}
else -> clause
}
}
protected open fun preprocess(term: Term, nested: Boolean = false): Term {
val prepped = when (term) {
Atom("true") -> True
Structure(Atom("true"), emptyList()) -> True
Atom("false") -> False
Structure(Atom("false"), emptyList()) -> False
Atom("fail") -> Fail
Structure(Atom("fail"), emptyList()) -> Fail
Atom("!") -> Cut()
Structure(Atom("!"), emptyList()) -> Cut()
Atom("inf") -> Integer(Int.MAX_VALUE)
Atom("nl") -> Nl
Variable("_") -> AnonymousVariable.create()
is Structure -> {
// Preprocess the arguments first to recognize builtins
val args = term.arguments.map { preprocess(it, nested = true) }
when {
// TODO Remove hardcoding by storing the functors as constants in operators?
term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body )
// Logic
term.functor == "=/2" -> Unify(args[0], args[1])
term.functor == "\\=/2" -> NotUnify(args[0], args[1])
term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == "\\+/1" -> Not(args[0] as Goal)
term.functor == "==/2" -> Equivalent(args[0], args[1])
term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
// Arithmetic
term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression)
term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression)
term.functor == "+/2" && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression)
term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
// Database
term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
term.functor == "retract/1" -> Retract(args[0])
term.functor == "assert/1" -> {
if (args[0] is Rule) {
Assert(args[0] as Rule)
} else {
Assert(Fact(args[0] as Head))
}
}
term.functor == "asserta/1" -> {
if (args[0] is Rule) {
AssertA(args[0] as Rule)
} else {
AssertA(Fact(args[0] as Head))
}
}
term.functor == "assertz/1" -> {
if (args[0] is Rule) {
AssertZ(args[0] as Rule)
} else {
AssertZ(Fact(args[0] as Head))
}
}
// 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.arguments = args
term
}
}
}
else -> term
}
Logger.debug(
"Preprocessed term $term into $prepped (kind ${prepped::class.simpleName})",
!nested && (prepped != term || prepped::class != term::class)
)
return prepped
}
}

23
src/interpreter/SourceFileReader.kt
View file

@ -1,23 +0,0 @@
package interpreter
import better_parser.PrologParser
class SourceFileReader {
private val parser = PrologParser()
fun readFile(filePath: String) {
return try {
val file = java.io.File(filePath)
if (!file.exists()) {
throw IllegalArgumentException("File not found: $filePath")
}
val content = file.readText()
// Parse the content using SimpleSourceParser
parser.parse(content)
} catch (e: Exception) {
throw RuntimeException("Error reading file: $filePath", e)
}
}
}

21
src/io/GhentPrologArgParser.kt Normal file
View file

@ -0,0 +1,21 @@
package io
import com.xenomachina.argparser.ArgParser
import com.xenomachina.argparser.default
class GhentPrologArgParser(parser: ArgParser) {
val script by parser.adding("-s", "--script", help = "Script to run")
val repl by parser.flagging("-r", "--repl", help = "Start the REPL")
val verbosity by parser.mapping(
"--vvv" to Logger.Level.DEBUG,
"--debug" to Logger.Level.DEBUG,
"--vv" to Logger.Level.INFO,
"--verbose" to Logger.Level.INFO,
"--info" to Logger.Level.INFO,
"-v" to Logger.Level.WARN,
"--warn" to Logger.Level.WARN,
"--error" to Logger.Level.ERROR,
help = "Set the verbosity level (default: WARN)",
).default(Logger.defaultLevel)
}

10
src/io/IoHandler.kt Normal file
View file

@ -0,0 +1,10 @@
package io
interface IoHandler {
fun prompt(
message: String,
hint: () -> String = { "Please enter a valid input." }
): String
fun say(message: String)
}

25
src/io/Logger.kt Normal file
View file

@ -0,0 +1,25 @@
package io
object Logger {
enum class Level {
DEBUG, INFO, WARN, ERROR
}
val defaultLevel: Level = Level.WARN
var level: Level = defaultLevel
private val io = Terminal()
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, 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)
}

71
src/io/Terminal.kt Normal file
View file

@ -0,0 +1,71 @@
package io
import prolog.ast.Database.Program
import java.io.BufferedReader
import java.io.BufferedWriter
import java.io.InputStream
import java.io.OutputStream
/**
* Handles input and output from a terminal.
*/
class Terminal(
inputStream: InputStream = System.`in`,
outputStream: OutputStream = System.`out`,
errorStream: OutputStream = System.err
) : IoHandler {
val input: BufferedReader = inputStream.bufferedReader()
val output: BufferedWriter = outputStream.bufferedWriter()
val error: BufferedWriter = errorStream.bufferedWriter()
override fun prompt(
message: String,
hint: () -> String
): String {
say("$message ")
var input: String = readLine()
while (input.isBlank()) {
say(hint(), error)
input = readLine()
}
return input
}
override fun say(message: String) {
output.write(message)
output.flush()
}
fun say(message: String, writer: BufferedWriter = output) {
writer.write(message)
writer.flush()
}
/**
* Reads a line from the input stream.
*/
fun readLine(reader: BufferedReader = input): String {
val line = reader.readLine()
if (line == null) {
Logger.info("End of stream reached")
cleanup()
}
return line
}
fun cleanup() {
Logger.info("Closing terminal streams")
input.close()
output.close()
error.close()
System.exit(0)
}
fun checkNewLine() {
if (Program.storeNewLine) {
say("\n")
Program.storeNewLine = false
}
}
}

127
src/lexer/Lexer.kt
View file

@ -1,127 +0,0 @@
package lexer
import lexer.errors.LexingError
import lexer.errors.LexingErrorType
import lexer.state.LexerPosition
import lexer.state.TokenPosition
class Lexer(private val source: String) {
private var tokens: List<Token> = emptyList()
private val position = LexerPosition(0, 0, -1)
/**
* Scans the source code and returns a list of tokens.
* @return List of [Token]s
*/
fun scan(): List<Token> {
while (hasNext()) {
val char: Char = peek()
tokens += when {
char == '(' -> scanSymbol(TokenType.PARENTHESIS_LEFT)
char == ')' -> scanSymbol(TokenType.PARENTHESIS_RIGHT)
char == '.' -> scanSymbol(TokenType.DOT)
char == '"' -> scanQuotedString()
char == '%' -> { scanComment(); continue }
char.isLetterOrDigit() -> scanAlphanumeric()
char.isWhitespace() -> { scanWhitespace(); continue }
else -> throw LexingError(LexingErrorType.UNKNOWN_TOKEN, "Did not recognize $char", position)
}
}
tokens += Token(TokenType.EOF, "EOF", getPosition(0))
return tokens
}
private fun hasNext(): Boolean {
// Check if the position is within the source length
return position.offset < source.length
}
private fun peek(): Char {
// Peek should only be called if there is a next character
require(hasNext()) {
LexingError(LexingErrorType.UNEXPECTED_END_OF_INPUT, "Expected additional character", position)
}
return source[position.offset]
}
private fun next(): Char {
// Advance the position and return the character
val char = peek()
position.offset++
position.column++
return char
}
private fun getPosition(length: Int = 1): TokenPosition {
// Return a new TokenPosition based on the current LexerPosition
return TokenPosition(position.line, position.column, length)
}
/* * * * * * *
* Scanners *
* * * * * * */
/**
* Scans a symbol token, given the expected [TokenType].
* @param tokenType The expected [TokenType]
* @return The scanned [Token]
*/
private fun scanSymbol(tokenType: TokenType): Token {
return Token(tokenType, next().toString(), getPosition(1))
}
private fun scanAlphanumeric(): Token {
// Scan all alphanumeric characters
var length = 0
while (hasNext() && peek().isLetterOrDigit()) {
next()
length++
}
val value = source.substring(position.offset - length, position.offset)
return Token(TokenType.ALPHANUMERIC, value, getPosition(length))
}
private fun scanQuotedString(): Token {
// "Assert" that the next character is the start of a quoted string
require(next() == '"') {
LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected opening quote '('", position)
}
var length = 0
while (hasNext() && peek() != '"') {
next()
length++
}
// "Assert" that the next character is the end of the quoted string
require(next() == '"') {
LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected closing quote ')'", position)
}
val value = source.substring(position.offset - length - 1, position.offset - 1)
return Token(TokenType.ALPHANUMERIC, value, getPosition(length))
}
private fun scanComment() {
// "Assert" that the next character is the start of a comment
require(next() == '%') {
LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected opening comment '%'", position)
}
// Skip all characters until the end of the line
while (hasNext() && peek() != '\n') {
next()
}
}
private fun scanWhitespace() {
// Skip all whitespace characters
while (hasNext() && peek().isWhitespace()) {
if (next() == '\n') {
position.line++
position.column = 0
}
}
}
}

9
src/lexer/Token.kt
View file

@ -1,9 +0,0 @@
package lexer
import lexer.state.TokenPosition
data class Token(
val type: TokenType,
val value: String,
val position: TokenPosition
)

15
src/lexer/TokenType.kt
View file

@ -1,15 +0,0 @@
package lexer
enum class TokenType {
ALPHANUMERIC,
// TODO Replace with SMALL_LETTER, CAPITAL_LETTER, DIGIT, HEX_DIGIT, ... ?
// Structure
COMMA,
DOT,
PARENTHESIS_LEFT, PARENTHESIS_RIGHT,
// Special
EOF
}

13
src/lexer/errors/LexingError.kt
View file

@ -1,13 +0,0 @@
package lexer.errors
import lexer.state.LexerPosition
data class LexingError(
val type: LexingErrorType,
override val message: String,
val position: LexerPosition
) : Throwable(
"""
${position.line}:${position.column + 1} ${type}: $message
""".trimIndent()
)

7
src/lexer/errors/LexingErrorType.kt
View file

@ -1,7 +0,0 @@
package lexer.errors
enum class LexingErrorType {
UNKNOWN_TOKEN,
UNEXPECTED_TOKEN,
UNEXPECTED_END_OF_INPUT,
}

3
src/lexer/state/LexerPosition.kt
View file

@ -1,3 +0,0 @@
package lexer.state
data class LexerPosition(var offset: Int, var line: Int, var column: Int)

3
src/lexer/state/TokenPosition.kt
View file

@ -1,3 +0,0 @@
package lexer.state
data class TokenPosition(val line: Int, val column: Int, val length: Int)

136
src/parser/Parser.kt
View file

@ -1,137 +1,11 @@
package parser
import lexer.Token
import lexer.TokenType
import parser.errors.ParsingError
import parser.errors.ParsingErrorType
import parser.state.ParserPosition
import prolog.ast.logic.Clause
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
class Parser(private val tokens: List<Token>) {
private val position: ParserPosition = ParserPosition(0)
fun parse(): List<Term> {
val terms = mutableListOf<Term>()
while (hasNext()) {
position.save()
var term: Term? = null
while (term == null) {
// Try each parser rule in order
}
require(term != null) {
ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected a term", position)
}
terms.add(term)
}
return terms
}
interface Parser {
/**
* Matches the current token with any of the expected types.
* If it matches, it consumes the token and returns true.
* Parses the input string and returns the parsed result.
*
* @param types The list of expected token types.
* @return True if the current token matches any of the expected types, false otherwise.
* @param input The input string to parse.
* @return The parsed result, which is the AST of the input.
*/
private fun match(types: List<TokenType>): Boolean {
for (type in types) {
if (check(type)) {
next()
return true
}
}
return false
}
/**
* Checks if the current token matches the expected type.
*/
private fun check(type: TokenType): Boolean {
return hasNext() && peek().type == type
}
private fun hasNext(): Boolean {
// Check if the position is within the tokens list
// TODO Check for EOF instead?
return position.offset < tokens.size
}
private fun peek(): Token {
require(hasNext()) { "Unexpected end of input" }
return tokens[position.offset]
}
private fun next(): Token {
val token = peek()
position.offset++
return token
}
private fun previous(): Token {
require(0 < position.offset) { "No previous token" }
return tokens[position.offset - 1]
}
/* * * * * *
* Parsers *
* * * * * */
private fun parseWithTry(parseRule: () -> Term): Term {
try {
return parseRule()
} catch (e: Exception) {
throw ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Unexpected token", position)
}
}
private fun parseClause(): Clause {
return try {
Fact(parseStructure())
} catch (e: Exception) {
Fact(parseAtom())
}
}
private fun parseStructure(): Structure {
val name = parseAtom()
val args = mutableListOf<Term>()
require(match(listOf(TokenType.PARENTHESIS_LEFT))) {
ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected '(' after structure name", position)
}
// TODO Handle arguments
require(match(listOf(TokenType.PARENTHESIS_RIGHT))) {
ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected ')' after structure arguments", position)
}
return Structure(name, args)
}
private fun parseAtom(): Atom {
return Atom(parseLetterDigit())
}
private fun parseLetterDigit(): String {
require(match(listOf(TokenType.ALPHANUMERIC)) && previous().value[0].isLowerCase()) {
ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected lowercase letter", position)
}
return previous().value
}
fun parse(input: String): Any
}

12
src/parser/ReplParser.kt Normal file
View file

@ -0,0 +1,12 @@
package parser
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import parser.grammars.QueryGrammar
import prolog.builtins.Query
class ReplParser : Parser {
private val grammar: Grammar<Query> = QueryGrammar() as Grammar<Query>
override fun parse(input: String): Query = grammar.parseToEnd(input)
}

18
src/parser/ScriptParser.kt Normal file
View file

@ -0,0 +1,18 @@
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<List<Clause>> = LogicGrammar() as Grammar<List<Clause>>
private val preprocessor = Preprocessor()
override fun parse(input: String): List<Clause> {
val raw = grammar.parseToEnd(input)
return preprocessor.preprocess(raw)
}
}

12
src/parser/errors/ParsingError.kt
View file

@ -1,12 +0,0 @@
package parser.errors
import parser.state.ParserPosition
class ParsingError(private val type: ParsingErrorType, override val message: String, private val position: ParserPosition) :
Throwable() {
override fun toString(): String {
return """
($position) ${type}: $message
""".trimIndent()
}
}

7
src/parser/errors/ParsingErrorType.kt
View file

@ -1,7 +0,0 @@
package parser.errors
enum class ParsingErrorType {
UNEXPECTED_TOKEN,
INTERNAL_ERROR,
}

21
src/parser/grammars/LogicGrammar.kt Normal file
View file

@ -0,0 +1,21 @@
package parser.grammars
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<Rule> by (-neck * body) use {
Rule(Atom(""), this)
}
protected val rule: Parser<Rule> by (head * -neck * body) use { Rule(t1, t2) }
protected val fact: Parser<Fact> by head use { Fact(this) }
protected val clause: Parser<Clause> by ((rule or constraint or fact) * -dot)
protected val clauses: Parser<List<Clause>> by oneOrMore(clause)
override val rootParser: Parser<Any> by clauses
}

16
src/parser/grammars/QueryGrammar.kt Normal file
View file

@ -0,0 +1,16 @@
package parser.grammars
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.parser.Parser
import prolog.ast.logic.LogicOperand
import prolog.builtins.Query
class QueryGrammar : TermsGrammar() {
protected val query: Parser<Query> by (body * -dot) use {
Query(this as LogicOperand)
}
override val rootParser: Parser<Any> by query
}

124
src/parser/grammars/TermsGrammar.kt Normal file
View file

@ -0,0 +1,124 @@
package parser.grammars
import com.github.h0tk3y.betterParse.combinators.*
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.terms.*
import prolog.builtins.Dynamic
/**
* Precedence is based on the following table:
*
* | Precedence | Type | Operators |
* |------------|------|-----------------------------------------------------------------------------------------------|
* | 1200 | xfx | --\>, :-, =\>, ==\> |
* | 1200 | fx | :-, ?- |
* | 1150 | fx | dynamic |
* | 1105 | xfy | | |
* | 1100 | xfy | ; |
* | 1050 | xfy | ->, *-> |
* | 1000 | xfy | , |
* | 990 | xfx | := |
* | 900 | fy | \+ |
* | 700 | xfx | <, =, =.., =:=, =<, ==, =\=, >, >=, \=, \==, as, is, >:<, :< |
* | 600 | xfy | : |
* | 500 | yfx | +, -, /\, \/, xor |
* | 500 | fx | ? |
* | 400 | yfx | *, /, //, div, rdiv, <<, >>, mod, rem |
* | 200 | xfx | ** |
* | 200 | xfy | ^ |
* | 200 | fy | +, -, \ |
* | 100 | yfx | . |
* | 1 | fx | $ |
*
* It is very easy to extend this grammar to support more operators. Just add them at the appropriate rule or create a
* new rule and chain it to the existing ones.
*
* @see [SWI-Prolog Predicate op/3](https://www.swi-prolog.org/pldoc/man?predicate=op/3)
*/
open class TermsGrammar : Tokens() {
// Basic named terms
protected val variable: Parser<Variable> by (variableToken or anonymousVariableToken) use { Variable(text) }
protected val simpleAtom: Parser<Atom> by (nameToken or exclamation) use { Atom(text) }
protected val quotedAtom: Parser<Atom> by (dummy
or ticked
or doubleTicked
or backTicked
) use { Atom(text.substring(1, text.length - 1)) }
protected val atom: Parser<Atom> by (quotedAtom or simpleAtom)
protected val compound: Parser<Structure> by (atom * -leftParenthesis * separated(
parser(::termNoConjunction),
comma,
acceptZero = true
) * -rightParenthesis) use {
Structure(t1, t2.terms)
}
// Basic arithmetic
protected val int: Parser<Integer> by integerToken use { Integer(text.toInt()) }
protected val float: Parser<Float> by floatToken use { Float(text.toFloat()) }
protected val functor: Parser<String> by (nameToken * divide * int) use { "${t1.text}${t2.text}$t3" }
// Base terms (atoms, compounds, variables, numbers)
protected val baseTerm: Parser<Term> by (dummy
or (-leftParenthesis * parser(::term) * -rightParenthesis)
or compound
or atom
or variable
or float
or int
)
protected val op200: Parser<CompoundTerm> by ((plus or minus) * parser(::term200)) use {
CompoundTerm(Atom(t1.text), listOf(t2))
}
protected val term200: Parser<Term> by (op200 or baseTerm)
protected val op400: Parser<String> by (multiply or divide) use { text }
protected val term400: Parser<Term> by (term200 * zeroOrMore(op400 * term200)) use {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val op500: Parser<String> by (plus or minus) use { text }
protected val term500: Parser<Term> by (term400 * zeroOrMore(op500 * term400)) use {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val op700: Parser<String> by (equivalent 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))
}
protected val op1000: Parser<String> by (comma) use { text }
protected val term1000: Parser<Term> by (term700 * zeroOrMore(op1000 * term700)) use {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val op1100: Parser<String> by (semicolon) use { text }
protected val term1100: Parser<Term> by (term1000 * zeroOrMore(op1100 * term1000)) use {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val dynamic: Parser<Term> by (dynamicOp * functor) use {
CompoundTerm( Atom(t1.text), listOf(Atom(t2)) )
}
protected val term1150: Parser<Term> by (dynamic or term1100) use { this }
protected val op1200: Parser<String> by (neck) use { text }
protected val term1200: Parser<Term> by (term1150 * zeroOrMore(op1200 * term1100)) use {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
// Term - highest level expression
protected val term: Parser<Term> by term1200
protected val termNoConjunction: Parser<Term> by term700
// Parts for clauses
protected val head: Parser<Head> by (compound or atom)
protected val body: Parser<Body> by term use { this as Body }
override val rootParser: Parser<Any> by term
}

56
src/parser/grammars/Tokens.kt Normal file
View file

@ -0,0 +1,56 @@
package parser.grammars
import com.github.h0tk3y.betterParse.combinators.use
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.lexer.Token
import com.github.h0tk3y.betterParse.lexer.literalToken
import com.github.h0tk3y.betterParse.lexer.regexToken
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 exclamation: Token by literalToken("!")
// 1200
protected val neck by literalToken(":-")
// 1150
protected val dynamicOp by literalToken("dynamic")
// 1100
protected val semicolon: Token by literalToken(";")
// 1000
protected val comma: Token by literalToken(",")
// 700
protected val equivalent: Token by literalToken("==")
protected val equals: Token by literalToken("=")
protected val isOp: Token by literalToken("is")
// 500
protected val plus: Token by literalToken("+")
protected val minus: Token by literalToken("-")
protected val notEquals: Token by literalToken("\\=")
// 400
protected val multiply: Token by literalToken("*")
protected val divide: Token by literalToken("/")
// 100
protected val dot by literalToken(".")
// Prolog tokens
protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*")
protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*")
protected val anonymousVariableToken: Token by literalToken("_")
// Arithmetic tokens
protected val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+")
protected val integerToken: Token by regexToken("-?([1-9][0-9]*|0)")
// Ignored tokens
protected val whitespace: Token by regexToken("\\s+", ignore = true)
protected val singleLineComment: Token by regexToken("%[^\\n]*", ignore = true)
protected val multiLineComment: Token by regexToken("/\\*.*?\\*/", ignore = true)
protected val ticked: Token by regexToken("'[^']*'")
protected val doubleTicked: Token by regexToken("\"[^\"]*\"")
protected val backTicked: Token by regexToken("`[^`]*`")
// Helper
protected val dummy by token { _, _ -> -1 } use { throw IllegalStateException("This parser should not be used") }
}

25
src/parser/state/ParserPosition.kt
View file

@ -1,25 +0,0 @@
package parser.state
import parser.errors.ParsingError
import parser.errors.ParsingErrorType
data class ParserPosition(var offset: Int) {
private val checkpoints: ArrayDeque<ParserPosition> = ArrayDeque()
fun save() {
checkpoints.addLast(this.copy())
}
fun reload() {
require(checkpoints.isNotEmpty()) {
ParsingError(ParsingErrorType.INTERNAL_ERROR, "No checkpoint to reload from", this)
}
val checkpoint = checkpoints.removeLast()
offset = checkpoint.offset
}
override fun toString(): String {
return "at $offset"
}
}

80
src/prolog/Program.kt
View file

@ -1,80 +0,0 @@
package prolog
import Debug
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 Program: Resolvent {
var predicates: Map<Functor, Predicate> = emptyMap()
init {
setup()
}
private fun setup() {
if (Debug.on) {
println("Setting up Prolog program...")
}
// Initialize the program with built-in predicates
load(listOf(
))
}
/**
* Queries the program with a goal.
* @return true if the goal can be proven, false otherwise.
*/
fun query(goal: Goal): Answers = solve(goal, emptyMap())
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<Clause>) {
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 clear() {
predicates = emptyMap()
setup()
}
}

2
src/prolog/Substitution.kt
View file

@ -4,7 +4,7 @@ import prolog.ast.terms.Term
abstract class Substitution(val from: Term, val to: Term) {
val mapped: Pair<Term, Term>? = if (from != to) from to to else null
override fun toString(): String = "$from -> $to"
override fun toString(): String = "$from |-> $to"
}
typealias Substitutions = Map<Term, Term>
typealias Answer = Result<Substitutions>

130
src/prolog/ast/Database.kt Normal file
View file

@ -0,0 +1,130 @@
package prolog.ast
import io.Logger
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
*/
open class Database(val sourceFile: String) {
var predicates: Map<Functor, Predicate> = emptyMap()
/**
* Initializes the database by running the initialization clauses of that database.
*/
fun initialize() {
databases.add(this)
if (sourceFile !== "") {
Logger.debug("Moving clauses from $sourceFile to main database")
predicates.filter { it.key != "/_" }
.forEach { (_, predicate) -> db.load(predicate, force = true) }
}
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()
}
}
}
/**
* Loads a list of clauses into the program.
*
* @param clauses The list of clauses to load.
* @param index The index at which to insert the clause. If null, the clause is added to the end of the list.
* @param force If true, the clause is added even if the predicate is static.
*/
fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) {
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, index, force)
} else {
// If the predicate does not exist, create a new one, usually during Program execution, so dynamic.
predicates += Pair(functor, Predicate(listOf(clause), dynamic = true))
}
Logger.debug("Loaded clause $clause into predicate $functor")
}
}
fun load(predicate: Predicate, force: Boolean = false) {
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() {
if (sourceFile == "") {
Logger.debug("Clearing main database")
predicates = emptyMap()
return
}
Logger.debug("Clearing database $sourceFile")
// Remove our clauses from the database
predicates.forEach { (_, predicate) ->
val dbPredicate = db.predicates[predicate.functor]
predicate.clauses.forEach { clause -> dbPredicate?.clauses?.remove(clause) }
}
databases.remove(this)
}
/**
* Object to handle execution
*
* This object is a singleton that manages a list of databases.
*/
companion object Program : Resolvent {
var db = Database("")
var databases: MutableList<Database> = mutableListOf(db)
var storeNewLine: Boolean = false
var variableRenamingStart: Int = 0
/**
* Queries the program with a goal.
* @return true if the goal can be proven, false otherwise.
*/
fun query(goal: Goal): Answers = solve(goal, emptyMap())
override fun solve(goal: Goal, subs: Substitutions): Answers {
val functor = goal.functor
// If the predicate does not exist, return false
val predicate = db.predicates[functor] ?: return emptySequence()
// If the predicate exists, evaluate the goal against it
return predicate.solve(goal, subs)
}
fun consult(database: Database) = database.initialize()
fun disregard(database: Database) = database.clear()
fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) = db.load(clauses, index, force)
fun reset() {
databases.toList().map { it.clear() }
variableRenamingStart = 0
storeNewLine = false
}
}
}

15
src/prolog/ast/arithmetic/Float.kt
View file

@ -1,6 +1,7 @@
package prolog.ast.arithmetic
import prolog.Substitutions
import prolog.ast.terms.Term
class Float(override val value: kotlin.Float): Number {
// Floats are already evaluated
@ -31,4 +32,18 @@ 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()
}
override fun clone(): Float = Float(value)
override fun applySubstitution(subs: Substitutions): Float = this
}

10
src/prolog/ast/arithmetic/Integer.kt
View file

@ -1,11 +1,16 @@
package prolog.ast.arithmetic
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.LogicOperand
import prolog.ast.terms.Term
data class Integer(override val value: Int) : Number {
data class Integer(override val value: Int) : Number, LogicOperand() {
// Integers are already evaluated
override fun simplify(subs: Substitutions): Simplification = Simplification(this, this)
override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
override fun toString(): String = value.toString()
override operator fun plus(other: Number): Number = when (other) {
@ -37,4 +42,7 @@ data class Integer(override val value: Int) : Number {
is Integer -> Integer(value * other.value)
else -> throw IllegalArgumentException("Cannot multiply $this and $other")
}
override fun clone(): Integer = Integer(value)
override fun applySubstitution(subs: Substitutions): Integer = this
}

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

@ -1,13 +1,14 @@
package prolog.ast.logic
import prolog.Answers
import prolog.ast.Database.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.occurs
import prolog.logic.unifyLazy
/**
@ -15,29 +16,45 @@ import prolog.logic.unifyLazy
*
* A clause consists of a [Head] and body separated by the neck operator, or it is a [Fact].
*
* @see [prolog.ast.terms.Variable]
* @see [Variable]
* @see [Predicate]
*/
abstract class Clause(val head: Head, val body: Body) : Resolvent {
abstract class Clause(var head: Head, var body: Body) : Term, 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 ->
val preHead = applySubstitution(head, subs)
val preGoal = applySubstitution(goal, subs)
val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs)
val headReverse = headRenaming.entries.associate { (a, b) -> b to a }
Program.variableRenamingStart = headEnd
val renamedHead = applySubstitution(head, headRenaming)
unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer ->
headAnswer.map { headSubs ->
// If the body can be proven, yield the (combined) substitutions
body.satisfy(subs + newHeadSubs).forEach { bodyAnswer ->
val preBody = applySubstitution(body, headRenaming + headSubs) as Body
preBody.satisfy(subs).forEach { bodyAnswer ->
bodyAnswer.fold(
onSuccess = { newBodySubs ->
yield(Result.success(newHeadSubs + newBodySubs))
onSuccess = { bodySubs ->
var result = (headSubs + bodySubs)
.mapKeys { applySubstitution(it.key, headReverse) }
.mapValues { applySubstitution(it.value, headReverse) }
result = result.map { it.key to applySubstitution(it.value, result) }
.toMap()
.filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())}
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 +69,19 @@ abstract class Clause(val head: Head, val body: Body) : Resolvent {
}
}
override fun toString(): String {
return when {
body is True -> head.toString()
else -> "$head :- $body"
}
override fun toString(): String = if (body is True) head.toString() else "$head :- $body"
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is Clause) return false
if (head != other.head) return false
if (body != other.body) return false
return true
}
override fun hashCode(): Int {
return super.hashCode()
}
}

8
src/prolog/ast/logic/Fact.kt
View file

@ -1,6 +1,12 @@
package prolog.ast.logic
import prolog.Substitutions
import prolog.ast.terms.Head
import prolog.ast.terms.Term
import prolog.builtins.True
import prolog.logic.applySubstitution
class Fact(head: Head) : Clause(head, True)
class Fact(head: Head) : Clause(head, True) {
override fun clone(): Fact = Fact(head)
override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head as Term, subs) as Head)
}

26
src/prolog/ast/logic/Predicate.kt
View file

@ -15,48 +15,54 @@ import prolog.flags.AppliedCut
class Predicate : Resolvent {
val functor: Functor
val clauses: MutableList<Clause>
var dynamic = false
/**
* Creates a predicate with the given functor and an empty list of clauses.
*/
constructor(functor: Functor) {
constructor(functor: Functor, dynamic: Boolean = false) {
this.functor = functor
this.clauses = mutableListOf()
this.dynamic = dynamic
}
/**
* Creates a predicate with the given clauses.
*/
constructor(clauses: List<Clause>) {
constructor(clauses: List<Clause>, dynamic: Boolean = false) {
this.functor = clauses.first().functor
require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
this.clauses = clauses.toMutableList()
this.dynamic = dynamic
}
/**
* Adds a clause to the predicate.
*
* @param clause The clause to add.
* @param index The index at which to insert the clause. If null, the clause is added to the end of the list.
* @param force If true, the clause is added even if the predicate is static.
*/
fun add(clause: Clause) {
fun add(clause: Clause, index: Int? = null, force: Boolean = false) {
require(clause.functor == functor) { "Clause functor does not match predicate functor" }
require(dynamic || force) { "No permission to modify static procedure '$functor'" }
if (Debug.on) {
println("Adding clause $clause to predicate $functor")
}
clauses.add(clause)
if (index != null) clauses.add(index, clause) else clauses.add(clause)
}
/**
* Adds a list of clauses to the predicate.
*/
fun addAll(clauses: List<Clause>) {
fun addAll(clauses: List<Clause>, force: Boolean = false) {
require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
require(dynamic || force) { "No permission to modify static procedure '$functor'" }
this.clauses.addAll(clauses)
}
override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
require(goal.functor == functor) { "Goal functor does not match predicate functor" }
// Try to unify the goal with the clause
// If the unification is successful, yield the substitutions
clauses.forEach { clause ->

11
src/prolog/ast/logic/Rule.kt
View file

@ -1,6 +1,15 @@
package prolog.ast.logic
import prolog.Substitutions
import prolog.ast.terms.Body
import prolog.ast.terms.Head
import prolog.ast.terms.Term
import prolog.logic.applySubstitution
class Rule(head: Head, body: Body) : Clause(head, body)
class Rule(head: Head, body: Body) : Clause(head, body) {
override fun clone(): Rule = Rule(head, body)
override fun applySubstitution(subs: Substitutions): Rule = Rule(
head = applySubstitution(head as Term, subs) as Head,
body = applySubstitution(body, subs) as Body
)
}

21
src/prolog/ast/terms/AnonymousVariable.kt Normal file
View file

@ -0,0 +1,21 @@
package prolog.ast.terms
import io.Logger
import prolog.Substitutions
class AnonymousVariable(private val id: Int) : Variable("_$id") {
companion object {
private var counter = 0
fun create(): AnonymousVariable {
val id = counter
counter++
Logger.debug("Creating anonymous variable: _${id}")
return AnonymousVariable(id)
}
}
override fun toString(): String = "_"
override fun clone(): AnonymousVariable = AnonymousVariable(id)
override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
}

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

@ -21,4 +21,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
override fun hashCode(): Int {
return javaClass.hashCode()
}
override fun clone(): Atom = Atom(name)
override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
}

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

@ -2,4 +2,4 @@ package prolog.ast.terms
import prolog.ast.logic.Satisfiable
interface Body : Satisfiable
interface Body : Term, Satisfiable

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

@ -1,7 +1,7 @@
package prolog.ast.terms
import prolog.Answers
import prolog.Program
import prolog.ast.Database.Program
import prolog.Substitutions
import prolog.ast.logic.LogicOperand

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

@ -6,7 +6,7 @@ abstract class Operator(
private val symbol: Atom,
private val leftOperand: Operand? = null,
private val rightOperand: Operand
) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)) {
) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Term {
override fun toString(): String {
return when (leftOperand) {
null -> "${symbol.name} $rightOperand"

18
src/prolog/ast/terms/Structure.kt
View file

@ -3,6 +3,7 @@ package prolog.ast.terms
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Resolvent
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
typealias Argument = Term
@ -22,4 +23,21 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
else -> "${name.name}(${arguments.joinToString(", ")})"
}
}
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is Structure) return false
if (functor != other.functor) return false
return arguments.zip(other.arguments).all { (a, b) -> a == b }
}
override fun hashCode(): Int {
return javaClass.hashCode()
}
override fun clone(): Structure = Structure(name, arguments)
override fun applySubstitution(subs: Substitutions): Structure = Structure(
name,
arguments.map { applySubstitution(it, subs) }
)
}

11
src/prolog/ast/terms/Term.kt
View file

@ -1,14 +1,19 @@
package prolog.ast.terms
import prolog.Substitutions
import prolog.logic.compare
import prolog.ast.arithmetic.Integer
import prolog.ast.arithmetic.Float
/**
* Value in Prolog.
*
* A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
* [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
* A [Term] is either a [Variable], [Atom], [Integer],
* [Float] or [CompoundTerm].
* In addition, SWI-Prolog also defines the type TODO string.
*/
interface Term : Comparable<Term> {
interface Term : Comparable<Term>, Cloneable {
override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
fun applySubstitution(subs: Substitutions): Term
public override fun clone(): Term
}

27
src/prolog/ast/terms/Variable.kt
View file

@ -1,10 +1,12 @@
package prolog.ast.terms
import prolog.Answers
import prolog.Substitutions
import prolog.ast.arithmetic.Expression
import prolog.ast.arithmetic.Simplification
import prolog.ast.logic.LogicOperand
data class Variable(val name: String) : Term, Expression {
open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
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 +18,28 @@ 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 equals(other: Any?): Boolean {
if (this === other) return true
if (other == null || other !is Variable) return false
return name == other.name
}
override fun hashCode(): Int {
return name.hashCode()
}
override fun toString(): String = name
override fun clone(): Variable = Variable(name)
override fun applySubstitution(subs: Substitutions): Variable = this
}

35
src/prolog/builtins/arithmeticOperators.kt
View file

@ -11,23 +11,6 @@ import prolog.ast.terms.*
import prolog.logic.*
// TODO >
class GreaterThan(private val left: Expression, private val right: Expression) :
Operator(Atom(">"), left, right), Satisfiable {
override fun satisfy(subs: Substitutions): Answers {
val t1 = left.simplify(subs)
val t2 = right.simplify(subs)
if (!atomic(t1.to, subs) || !atomic(t2.to, subs)) {
return sequenceOf(Result.failure(IllegalArgumentException("Both operands must be instantiated")))
}
return if (0 < compare(t1.to, t2.to, subs)) {
sequenceOf(Result.success(emptyMap()))
} else {
emptySequence()
}
}
}
// TODO <
@ -79,11 +62,11 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
/**
* True when Number is the value to which Expr evaluates.
*/
class Is(private val left: Expression, private val right: Expression) :
Operator(Atom("is"), left, right), Satisfiable {
class Is(val number: Expression, val expr: Expression) :
Operator(Atom("is"), number, expr), Satisfiable {
override fun satisfy(subs: Substitutions): Answers {
val t1 = left.simplify(subs)
val t2 = right.simplify(subs)
val t1 = number.simplify(subs)
val t2 = expr.simplify(subs)
if (!atomic(t2.to, subs)) {
return sequenceOf(Result.failure(IllegalArgumentException("Right operand must be instantiated")))
@ -136,7 +119,7 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
/**
* Result = Expr1 * Expr2
*/
class Multiply(private val expr1: Expression, private val expr2: Expression) :
class Multiply(val expr1: Expression, val expr2: Expression) :
ArithmeticOperator(Atom("*"), expr1, expr2) {
override fun simplify(subs: Substitutions): Simplification {
val result = Variable("Result")
@ -161,7 +144,7 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
// TODO Expr rem Expr
class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) :
Operator(Atom("between"), expr1, expr2) {
CompoundTerm(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable {
override fun satisfy(subs: Substitutions): Answers {
val e1 = expr1.simplify(subs)
val e2 = expr2.simplify(subs)
@ -169,8 +152,8 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
require(e1.to is Integer && e2.to is Integer) { "Arguments must be integers" }
val v1 = e1.to as Integer
val v2 = e2.to as Integer
val v1 = e1.to
val v2 = e2.to
return if (variable(e3.to, subs)) {
between(v1, v2, e3.to as Variable).map { answer ->
@ -182,4 +165,6 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
}
}
}
override fun toString(): String = "$expr1..$expr3..$expr2"
}

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

@ -3,10 +3,11 @@ package prolog.builtins
import prolog.Answers
import prolog.Substitutions
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.logic.LogicOperator
import prolog.ast.terms.Structure
import prolog.flags.AppliedCut
/**
@ -34,6 +35,8 @@ class Cut() : Atom("!") {
override fun satisfy(subs: Substitutions): Answers {
return sequenceOf(Result.failure(AppliedCut(emptyMap())))
}
override fun applySubstitution(subs: Substitutions): Cut = Cut()
}
/**
@ -94,6 +97,11 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
)
}
}
override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
left.applySubstitution(subs) as LogicOperand,
right.applySubstitution(subs) as LogicOperand
)
}
/**
@ -105,6 +113,12 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
yieldAll(left.satisfy(subs))
yieldAll(right.satisfy(subs))
}
override fun clone(): Disjunction = Disjunction(left.clone() as LogicOperand, right.clone() as LogicOperand)
override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
left.applySubstitution(subs) as LogicOperand,
right.applySubstitution(subs) as LogicOperand
)
}
@Deprecated("Use Disjunction instead")
@ -120,7 +134,8 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l
class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) {
override fun satisfy(subs: Substitutions): Answers {
// If the goal can be proven, return an empty sequence
if (goal.satisfy(subs).toList().isNotEmpty()) {
val goalResults = goal.satisfy(subs).iterator()
if (goalResults.hasNext()) {
return emptySequence()
}
// If the goal cannot be proven, return a sequence with an empty map

116
src/prolog/builtins/databaseOperators.kt Normal file
View file

@ -0,0 +1,116 @@
package prolog.builtins
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Clause
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.logic.Predicate
import prolog.ast.Database.Program
import prolog.ast.terms.Functor
import prolog.ast.terms.Term
import prolog.ast.logic.Fact
import prolog.ast.Database
import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Operator
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
/**
* (Make) the [Predicate] with the corresponding [Functor] dynamic.
*/
class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
override val functor: Functor = "dynamic/1"
override fun satisfy(subs: Substitutions): Answers {
val predicate = Program.db.predicates[dynamicFunctor]
if (predicate == null) {
return sequenceOf(Result.failure(Exception("Predicate $dynamicFunctor not found")))
}
predicate.dynamic = true
return sequenceOf(Result.success(emptyMap()))
}
override fun toString(): String = "dynamic $dynamicFunctor"
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is Dynamic) return false
return dynamicFunctor == other.dynamicFunctor
}
override fun hashCode(): Int = super.hashCode()
override fun clone(): Dynamic = Dynamic(dynamicFunctor)
override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
}
class Assert(clause: Clause) : AssertZ(clause) {
override val functor: Functor = "assert/1"
}
/**
* Assert a [Clause] as a first clause of the [Predicate] into the [Program].
*/
class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
override fun satisfy(subs: Substitutions): Answers {
// Add clause to the program
val evaluatedClause = applySubstitution(clause, subs) as Clause
Program.load(listOf(evaluatedClause), 0)
return sequenceOf(Result.success(emptyMap()))
}
}
/**
* Assert a [Clause] as a last clause of the [Predicate] into the [Program].
*/
open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) {
override fun satisfy(subs: Substitutions): Answers {
// Add clause to the program
val evaluatedClause = applySubstitution(clause, subs) as Clause
Program.load(listOf(evaluatedClause))
return sequenceOf(Result.success(emptyMap()))
}
}
/**
* When [Term] is an [Atom] or a term, it is unified with the first unifying [Clause] in the [Database].
* The [Fact] or Clause is removed from the Database. It respects the logical update view.
*
* @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1)
*/
class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
override fun satisfy(subs: Substitutions): Answers = sequence {
// Check that term is a structure or atom
if (term !is Structure && term !is Atom) {
yield(Result.failure(Exception("Cannot retract a non-structure or non-atom")))
return@sequence
}
val functorName = term.functor
val predicate = Program.db.predicates[functorName]
if (predicate == null) {
return@sequence
}
predicate.clauses.toList().forEach { clause ->
unifyLazy(term, clause.head, subs).forEach { unifyResult ->
unifyResult.fold(
onSuccess = { substitutions ->
// If unification is successful, remove the clause
predicate.clauses.remove(clause)
yield(Result.success(substitutions))
},
onFailure = {
// If unification fails, do nothing
}
)
}
}
}
}

75
src/prolog/builtins/ioOperators.kt Normal file
View file

@ -0,0 +1,75 @@
package prolog.builtins
import io.Logger
import io.Terminal
import parser.ReplParser
import prolog.Answers
import prolog.ast.Database.Program
import prolog.Substitutions
import prolog.ast.logic.Satisfiable
import prolog.ast.terms.Atom
import prolog.ast.terms.Operator
import prolog.ast.terms.Term
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
/**
* Write [Term] to the current output, using brackets and operators where appropriate.
*/
class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
override fun satisfy(subs: Substitutions): Answers {
val t = applySubstitution(term, subs)
Terminal().say(t.toString())
Program.storeNewLine = true
return sequenceOf(Result.success(emptyMap()))
}
override fun toString(): String = "write($term)"
}
/**
* Write a newline character to the current output stream.
*/
object Nl : Atom("nl"), Satisfiable {
override fun satisfy(subs: Substitutions): Answers {
Terminal().say("\n")
Program.storeNewLine = false
return sequenceOf(Result.success(emptyMap()))
}
}
/**
* Read the next Prolog term from the current input stream and unify it with [Term].
*
* On reaching end-of-file, [Term] is unified with the [Atom] `end_of_file`.
*/
class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfiable {
private val io = Terminal()
private val parser = ReplParser()
private fun readTerm(): Term {
val input = io.readLine()
Logger.debug("Read input: $input")
return when (input) {
"end_of_file" -> Atom("end_of_file")
else -> {
val out = parser.parse(input).query
Logger.debug("Parsed input: $out")
out as? Term ?: throw IllegalArgumentException("Expected a term, but got: $out")
}
}
}
override fun satisfy(subs: Substitutions): Answers = sequence {
val t1 = applySubstitution(term, subs)
val t2 = readTerm()
Logger.debug("Read term: $t2")
yieldAll(unifyLazy(t1, t2, subs))
}
}

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

@ -6,6 +6,11 @@ import prolog.ast.logic.LogicOperand
import prolog.ast.terms.Atom
import prolog.ast.logic.LogicOperator
class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) {
override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1)
override fun toString(): String = goal.toString()
}
class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs)
}

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

@ -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)

2
src/prolog/logic/arithmetic.kt
View file

@ -58,7 +58,7 @@ fun succ(term1: Expression, term2: Expression, subs: Substitutions): Answers {
it.fold(
onSuccess = { result ->
val t1 = applySubstitution(term1, result)
if (t1 in result) {
if (t1 in result || t1 in result.values) {
val e1 = t1.simplify(result)
if (e1.to is Integer && e1.to.value < 0) {
return@sequence

53
src/prolog/logic/terms.kt
View file

@ -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<Int, Substitutions> {
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).any { (it.key as Variable).name == suggestedName }) {
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 = applySubstitution(term, subs) as Structure
var n = start
val s: MutableMap<Term, Term> = 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())
}
}
}

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

@ -4,42 +4,52 @@ import prolog.Answer
import prolog.Answers
import prolog.Substitutions
import prolog.ast.arithmetic.Expression
import prolog.ast.logic.LogicOperator
import prolog.ast.terms.*
import kotlin.NoSuchElementException
import prolog.ast.arithmetic.Number
import prolog.ast.arithmetic.Integer
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.arithmetic.Number
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
fun applySubstitution(term: Term, subs: Substitutions): Term = when {
variable(term, emptyMap()) -> subs[(term as Variable)] ?: term
atomic(term, subs) -> term
compound(term, subs) -> {
val structure = term as Structure
Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
term is Fact -> term.applySubstitution(subs)
variable(term, emptyMap()) -> {
val variable = term as Variable
subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
}
atomic(term, subs) -> term
compound(term, subs) -> {
term.applySubstitution(subs)
}
else -> term
}
//TODO Combine with the other applySubstitution function
fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when {
variable(expr, subs) -> applySubstitution(expr as Term, subs) as Expression
atomic(expr, subs) -> expr
variable(expr, emptyMap()) -> applySubstitution(expr as Term, subs) as Expression
atomic(expr, subs) -> expr
expr is LogicOperator -> {
expr.arguments = expr.arguments.map { applySubstitution(it, subs) }
expr
}
else -> expr
}
// 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) -> {
val structure = term as Structure
structure.arguments.any { occurs(variable, it, subs) }
}
else -> false
}
@ -49,19 +59,21 @@ 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)))
}
}
compound(t1, subs) && compound(t2, subs) -> {
val structure1 = t1 as Structure
val structure2 = t2 as Structure
@ -75,22 +87,25 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
}
// 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) }
acc.flatMap { a ->
result.map { b ->
if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
}
}.map { Result.success(it) }
}
yieldAll(combinedResults)
}
}
}
else -> {}
}
}
fun unify(term1: Term, term2: Term): Answer {
val substitutions = unifyLazy(term1, term2, emptyMap()).toList()
return if (substitutions.isNotEmpty()) {
substitutions.first()
val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
return if (substitutions.hasNext()) {
substitutions.next()
} else {
Result.failure(NoSuchElementException())
}
@ -122,37 +137,40 @@ fun compare(term1: Term, term2: Term, subs: Substitutions): Int {
return when (t1) {
is Variable -> {
when (t2) {
is Variable -> t1.name.compareTo(t2.name)
is Variable -> t1.name.compareTo(t2.name)
is Number -> -1
is Atom -> -1
is Atom -> -1
is Structure -> -1
else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
}
}
is Number -> {
when (t2) {
is Variable -> 1
is Integer -> (t1.value as Int).compareTo(t2.value)
is Float -> (t1.value as kotlin.Float).compareTo(t2.value)
is Atom -> -1
is Variable -> 1
is Integer -> (t1.value as Int).compareTo(t2.value)
is Float -> (t1.value as kotlin.Float).compareTo(t2.value)
is Atom -> -1
is Structure -> -1
else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
}
}
is Atom -> {
when (t2) {
is Variable -> 1
is Variable -> 1
is Number -> 1
is Atom -> t1.name.compareTo(t2.name)
is Atom -> t1.name.compareTo(t2.name)
is Structure -> -1
else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
}
}
is Structure -> {
when (t2) {
is Variable -> 1
is Number -> 1
is Atom -> 1
is Atom -> 1
is Structure -> {
val arityComparison = t1.arguments.size.compareTo(t2.arguments.size)
if (arityComparison != 0) return arityComparison
@ -164,9 +182,11 @@ fun compare(term1: Term, term2: Term, subs: Substitutions): Int {
}
return 0
}
else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
}
}
else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
}
}

95
src/repl/Repl.kt
View file

@ -1,4 +1,99 @@
package repl
import interpreter.Preprocessor
import io.Logger
import io.Terminal
import parser.ReplParser
import prolog.Answer
import prolog.Answers
class Repl {
private val io = Terminal()
private val parser = ReplParser()
private val preprocessor = Preprocessor()
init {
welcome()
while (true) {
try {
printAnswers(query())
} catch (e: Exception) {
Logger.error("Error parsing REPL: ${e.message}")
}
}
}
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)
return query.satisfy(emptyMap())
}
private fun printAnswers(answers: Answers) {
val knownCommands = setOf(";", "a", ".", "h")
val iterator = answers.iterator()
if (!iterator.hasNext()) {
io.say("false.\n")
} else {
io.say(prettyPrint(iterator.next()))
while (iterator.hasNext()) {
var command = io.prompt("")
while (command !in knownCommands) {
io.say("Unknown action: $command (h for help)\n")
command = io.prompt("Action?")
}
when (command) {
";" -> {
io.say(prettyPrint(iterator.next()))
}
"a" -> return
"." -> return
"h" -> {
help()
io.say("Action?")
}
}
}
}
io.say("\n")
}
private fun help(): String {
io.say("Commands:\n")
io.say(" ; find next solution\n")
io.say(" a abort\n")
io.say(" . end query\n")
io.say(" h help\n")
return ""
}
private fun prettyPrint(result: Answer): String {
result.fold(
onSuccess = {
val subs = result.getOrNull()!!
if (subs.isEmpty()) {
io.checkNewLine()
return "true."
}
return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
},
onFailure = {
val text = "Failure: ${it.message}"
Logger.warn(text)
return text
}
)
}
}

156
tests/better_parser/SimplePrologPrologParserTests.kt
View file

@ -1,156 +0,0 @@
package better_parser
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.ValueSource
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.logic.equivalent
class SimplePrologPrologParserTests {
private lateinit var parser: Grammar<Term>
@BeforeEach
fun setup() {
parser = SimplePrologParser() as Grammar<Term>
}
@ParameterizedTest
@ValueSource(strings = ["a", "foo", "foo1", "fooBar", "foo_bar"])
fun `parse atom`(name: String) {
val result = parser.parseToEnd(name)
assertEquals(Atom(name), result, "Expected atom '$name'")
}
@ParameterizedTest
@ValueSource(strings = ["X", "X1", "X_1"])
fun `parse variable`(name: String) {
val result = parser.parseToEnd(name)
assertEquals(Variable(name), result, "Expected atom '$name'")
}
@Test
fun `empty compound term`() {
val input = "f()"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Structure(Atom("f"), emptyList()), result, emptyMap()),
"Expected atom 'f'"
)
}
@Test
fun `parse compound term f(a)`() {
val input = "f(a)"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Structure(Atom("f"), listOf(Atom("a"))), result, emptyMap()),
"Expected atom 'f(a)'"
)
}
@Test
fun `parse compound term f(a, b)`() {
val input = "f(a, b)"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), result, emptyMap()),
"Expected atom 'f(a, b)'"
)
}
@Test
fun `parse compound term with variable f(a, X)`() {
val input = "f(a, X)"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Structure(Atom("f"), listOf(Atom("a"), Variable("X"))), result, emptyMap()),
"Expected atom 'f(a, X)'"
)
}
@Test
fun `parse nested compound term f(a, g(b))`() {
val input = "f(a, g(b))"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(
Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))),
result,
emptyMap()
),
"Expected atom 'f(a, g(b))'"
)
}
@Test
fun `parse compound term with variable f(a, g(X))`() {
val input = "f(a, g(X))"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(
Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))),
result,
emptyMap()
),
"Expected atom 'f(a, g(X))'"
)
}
@ParameterizedTest
@ValueSource(ints = [-987654321, -543, -21, -1, 0, 1, 5, 12, 345, 123456789])
fun `parse integer`(number: Int) {
val input = number.toString()
val result = parser.parseToEnd(input)
assertEquals(Integer(number), result, "Expected integer '$number'")
}
@Test
fun `parse float`() {
val input = "42.0"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Float(42.0f), result, emptyMap()),
"Expected float '42.0'"
)
}
@Test
fun `parse negative float`() {
val input = "-42.0"
val result = parser.parseToEnd(input)
assertTrue(
equivalent(Float(-42.0f), result, emptyMap()),
"Expected float '-42.0'"
)
}
}

75
tests/compare.sh Normal file
View file

@ -0,0 +1,75 @@
#!/usr/bin/env bash
# This script is expected to be run from the root of the project.
WATCH_ALONG=0
# Paths to the two implementations
GPL="src/gpl"
SPL="swipl"
GPL_FLAGS=("--error")
SPL_FLAGS=("--quiet" "-t" "'true'")
# Directory containing test files
TEST_DIR="examples"
# Temporary files for storing outputs
GPL_OUT=$(mktemp)
GPL_ERR=$(mktemp)
SPL_OUT=$(mktemp)
SPL_ERR=$(mktemp)
touch "$GPL_OUT" "$GPL_ERR" "$SPL_OUT" "$SPL_ERR"
# 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"
"examples/basics/unification.pl"
"examples/basics/write.pl"
)
for TESTFILE in "${files[@]}"; do
# Run both programs with the test file
"${SPL}" "${SPL_FLAGS[@]}" "$TESTFILE" > "${SPL_OUT}" 2> "${SPL_ERR}"
"${GPL}" "${GPL_FLAGS[@]}" -s "$TESTFILE" > "${GPL_OUT}" 2> "${GPL_ERR}"
# Compare the outputs
was_different="$(
diff -q "$SPL_OUT" "$GPL_OUT" > /dev/null
echo $?
)"
if [[ "${was_different}" -ne 0 || "${WATCH_ALONG}" -eq 1 ]]; then
if [ "${was_different}" -ne 0 ]; then
message="TEST FAILED"
fi
printf "%s for %s\n" "${message:="Result"}" "${TESTFILE}"
printf "\nTest:\n%s\n" "$(cat "${TESTFILE}")"
printf "\nExpected:\n%s\n" "$(cat "${SPL_OUT}" && cat "${SPL_ERR}")"
printf "\nGot:\n%s\n" "$(cat "${GPL_OUT}" && cat "${GPL_ERR}")"
echo "-----------------------------------------"
fi
if [ "${was_different}" -ne 0 ]; then
FAILED=$((FAILED + 1))
else
PASSED=$((PASSED + 1))
fi
done
# Clean up temporary files
rm "$SPL_OUT" "$GPL_OUT" "$SPL_ERR" "$GPL_ERR"
# 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

63
tests/e2e/Examples.kt Normal file
View file

@ -0,0 +1,63 @@
package e2e
import interpreter.FileLoader
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import org.junit.jupiter.api.TestInstance
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.Arguments
import org.junit.jupiter.params.provider.MethodSource
import prolog.ast.Database.Program
import java.io.ByteArrayOutputStream
import java.io.PrintStream
@TestInstance(TestInstance.Lifecycle.PER_CLASS)
class Examples {
private val loader = FileLoader()
private lateinit var outStream: ByteArrayOutputStream
@BeforeEach
fun setup() {
Program.reset()
outStream = ByteArrayOutputStream()
System.setOut(PrintStream(outStream))
}
@Test
fun debugHelper() {
loader.load("examples/basics/backtracking.pl")
}
@ParameterizedTest
@MethodSource("basics")
fun `Identical output for basics`(inputFile: String, expected: String) {
loader.load("examples/basics/$inputFile")
assertEquals(expected, outStream.toString())
}
@ParameterizedTest
@MethodSource("other")
fun `Identical output for other`(inputFile: String, expected: String) {
loader.load("examples/$inputFile")
assertEquals(expected, outStream.toString())
}
fun basics() = listOf(
Arguments.of("arithmetics.pl", "gimli is a level 4 fighter with 35 hitpoints.\nlegolas is a level 5 ranger with 30 hitpoints.\ngandalf is a level 10 wizard with 25 hitpoints.\nfrodo is a level 2 rogue with 20 hitpoints.\nlegolas threw gimli, and gimli took 5 damage.\ngimli is a level 4 fighter with 30 hitpoints.\ngandalf casts aid.\ngimli is a level 4 fighter with 35 hitpoints.\nlegolas leveled up.\nlegolas is a level 6 ranger with 30 hitpoints"),
Arguments.of("backtracking.pl", "0\ns(0)\ns(s(0))\ns(s(s(0)))\n"),
Arguments.of("cut.pl", "0\n"),
Arguments.of("disjunction.pl", "Alice likes Italian food.\nBob likes Italian food.\n"),
Arguments.of("equality.pl", "X == Y failed\nX = Y succeeded\nX == Y succeeded\nX = Y succeeded\nX == Y succeeded\n"),
Arguments.of("forall.pl", "Only alice likes pizza.\n"),
Arguments.of("fraternity.pl", "Citizen robespierre is eligible for the event.\nCitizen danton is eligible for the event.\nCitizen camus is eligible for the event.\n"),
Arguments.of("liberty.pl", "Give me Liberty, or give me Death!\nI disapprove of what you say, but I will defend to the death your right to say it.\nThe revolution devours its own children.\nSo this is how liberty dies, with thunderous applause.\n"),
Arguments.of("unification.pl", "While alice got an A, carol got an A, but bob did not get an A, dave did not get an A, unfortunately.\n"),
Arguments.of("write.pl", "gpl zegt: dag(wereld)\n"),
)
fun other() = listOf(
Arguments.of("program.pl", "10\nhello(world)")
)
}

9
tests/interpreter/OpenPreprocessor.kt Normal file
View file

@ -0,0 +1,9 @@
package interpreter
import prolog.ast.terms.Term
class OpenPreprocessor : Preprocessor() {
public override fun preprocess(term: Term, nested: Boolean): Term {
return super.preprocess(term, nested)
}
}

92
tests/interpreter/ParserPreprocessorIntegrationTests.kt Normal file
View file

@ -0,0 +1,92 @@
package interpreter
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Nested
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.ValueSource
import parser.grammars.TermsGrammar
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Goal
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.builtins.Is
import prolog.builtins.Subtract
class ParserPreprocessorIntegrationTests {
@Nested
class `Arithmetic`() {
val parser = TermsGrammar()
val preprocessor = OpenPreprocessor()
@ParameterizedTest
@ValueSource(strings = ["-1", "-1.0", "-1.5"])
fun `can parse negative numbers`(input: String) {
val number = if (input.contains('.')) {
Float(input.substring(1).toFloat())
} else {
Integer(input.substring(1).toInt())
}
val negativeNumber = if (input.contains('.')) {
Float(input.toFloat())
} else {
Integer(input.toInt())
}
// Check if parser returns the same result
val parsed = parser.parseToEnd("X is $input") as Term
assertEquals(
Structure(Atom("is"), listOf(
Variable("X"),
Structure(Atom("-"), listOf(number)),
)),
parsed
)
// Check if preprocessor returns the same result
val prepped = preprocessor.preprocess(parsed)
val expected = Is(
Variable("X"),
Subtract(Integer(0), number)
)
assertEquals(expected, prepped)
assertEquals(expected.toString(), prepped.toString())
// Check if evaluation is correct
val solutions = (prepped as Is).satisfy(emptyMap()).toList()
assertEquals(1, solutions.size)
assertEquals(negativeNumber, solutions[0].getOrNull()!![Variable("X")])
}
@ParameterizedTest
@ValueSource(strings = ["X is 1 - 2", "X is 1-2"])
fun `can add negative numbers`(input: String) {
val result = parser.parseToEnd(input) as Term
assertEquals(
Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))),
result
)
val prepped = preprocessor.preprocess(result)
val expected = Is(
Variable("X"),
Subtract(Integer(1), Integer(2))
)
assertEquals(expected, prepped)
assertEquals(expected.toString(), prepped.toString())
}
}
}

622
tests/interpreter/PreprocessorTests.kt Normal file
View file

@ -0,0 +1,622 @@
package interpreter
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.Nested
import org.junit.jupiter.api.Test
import parser.grammars.TermsGrammar
import prolog.ast.arithmetic.Integer
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.ast.terms.*
import prolog.builtins.*
class PreprocessorTests {
val preprocessor = OpenPreprocessor()
companion object {
val preprocessor = OpenPreprocessor()
fun test(tests: Map<Term, Term>) {
for ((input, expected) in tests) {
val result = preprocessor.preprocess(input)
assertEquals(expected, result, "Expected preprocessed")
assertEquals(expected::class, result::class, "Expected same class")
}
}
}
@Test
fun `can preprocess anonymous variable`() {
val input = Variable("_")
val result = preprocessor.preprocess(input)
assertInstanceOf(AnonymousVariable::class.java, result, "Expected anonymous variable")
assertTrue((result as Variable).name.matches("_\\d+".toRegex()), "Expected anonymous variable name")
}
@Test
fun `multiple anonymous variables should be unique`() {
val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_")))
val result = preprocessor.preprocess(input)
assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term")
assertEquals(2, (result as CompoundTerm).arguments.size, "Expected two terms")
for (argument in result.arguments) {
assertTrue(
(argument as Variable).name.matches("_\\d+".toRegex()),
"Expected anonymous variable name, but got ${argument.name}"
)
}
val first = result.arguments[0] as Variable
val second = result.arguments[1] as Variable
assertNotEquals(first.name, second.name, "Expected different anonymous variable names")
}
@Test
fun `can preprocess nested anonymous variables`() {
val input = TermsGrammar().parseToEnd("name(character(Name, _, _, _))") as Term
val result = preprocessor.preprocess(input)
assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term")
assertEquals(1, (result as CompoundTerm).arguments.size, "Expected one term")
assertInstanceOf(CompoundTerm::class.java, result.arguments[0], "Expected compound term")
val inner = result.arguments[0] as CompoundTerm
assertEquals(4, inner.arguments.size, "Expected four terms")
for (argument in inner.arguments) {
if ((argument as Variable).name != "Name") {
assertTrue(
(argument as Variable).name.matches("_\\d+".toRegex()),
"Expected anonymous variable name, but got ${argument.name}"
)
}
}
}
@Nested
class `Arithmetic operators` {
@Test
fun `evaluates to different`() {
test(
mapOf(
Atom("=\\=") to Atom("=\\="),
CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()),
Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"),
CompoundTerm(Atom("EvaluatesToDifferent"), emptyList()) to CompoundTerm(
Atom("EvaluatesToDifferent"),
emptyList()
),
CompoundTerm(Atom("=\\="), listOf(Atom("a"))) to CompoundTerm(
Atom("=\\="),
listOf(Atom("a"))
),
CompoundTerm(Atom("=\\="), listOf(Integer(1))) to CompoundTerm(
Atom("=\\="),
listOf(Integer(1))
),
CompoundTerm(Atom("=\\="), listOf(Atom("=\\="))) to CompoundTerm(
Atom("=\\="),
listOf(Atom("=\\="))
),
CompoundTerm(Atom("=\\="), listOf(Integer(1), Integer(2))) to EvaluatesToDifferent(
Integer(1), Integer(2)
)
)
)
}
@Test
fun `evaluates to`() {
test(
mapOf(
Atom("=:=") to Atom("=:="),
CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()),
Atom("EvaluatesTo") to Atom("EvaluatesTo"),
CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm(
Atom("EvaluatesTo"),
emptyList()
),
CompoundTerm(Atom("=:="), listOf(Atom("a"))) to CompoundTerm(
Atom("=:="),
listOf(Atom("a"))
),
CompoundTerm(Atom("=:="), listOf(Atom("=:="))) to CompoundTerm(
Atom("=:="),
listOf(Atom("=:="))
),
CompoundTerm(Atom("=:="), listOf(Integer(1), Integer(2))) to EvaluatesTo(
Integer(1), Integer(2)
)
)
)
}
@Test
fun `is`() {
test(
mapOf(
Atom("is") to Atom("is"),
CompoundTerm(Atom("is"), emptyList()) to CompoundTerm(Atom("is"), emptyList()),
Atom("Is") to Atom("Is"),
CompoundTerm(Atom("Is"), emptyList()) to CompoundTerm(Atom("Is"), emptyList()),
CompoundTerm(Atom("is"), listOf(Atom("a"))) to CompoundTerm(
Atom("is"),
listOf(Atom("a"))
),
CompoundTerm(Atom("is"), listOf(Integer(1))) to CompoundTerm(
Atom("is"),
listOf(Integer(1))
),
CompoundTerm(Atom("is"), listOf(Atom("is"))) to CompoundTerm(
Atom("is"),
listOf(Atom("is"))
),
CompoundTerm(Atom("is"), listOf(Integer(1), Integer(2))) to Is(
Integer(1), Integer(2)
)
)
)
}
@Test
fun `negate and subtract`() {
test(
mapOf(
Atom("-") to Atom("-"),
CompoundTerm(Atom("-"), emptyList()) to CompoundTerm(Atom("-"), emptyList()),
Atom("Negate") to Atom("Negate"),
CompoundTerm(Atom("Negate"), emptyList()) to CompoundTerm(
Atom("Negate"),
emptyList()
),
CompoundTerm(Atom("-"), listOf(Atom("a"))) to CompoundTerm(
Atom("-"),
listOf(Atom("a"))
),
CompoundTerm(Atom("-"), listOf(Integer(1))) to Negate(Integer(1)),
CompoundTerm(Atom("-"), listOf(Atom("-"))) to CompoundTerm(
Atom("-"),
listOf(Atom("-"))
),
CompoundTerm(Atom("-"), listOf(Integer(1), Integer(2))) to Subtract(
Integer(1), Integer(2)
),
CompoundTerm(Atom("-"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
Atom("-"),
listOf(Atom("1"), Atom("2"))
),
CompoundTerm(Atom("-"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
Atom("-"),
listOf(Integer(1), Integer(2), Integer(3))
)
)
)
}
@Test
fun `positive and add`() {
test(
mapOf(
Atom("+") to Atom("+"),
CompoundTerm(Atom("+"), emptyList()) to CompoundTerm(Atom("+"), emptyList()),
Atom("Positive") to Atom("Positive"),
CompoundTerm(Atom("Positive"), emptyList()) to CompoundTerm(
Atom("Positive"),
emptyList()
),
CompoundTerm(Atom("+"), listOf(Atom("a"))) to CompoundTerm(
Atom("+"),
listOf(Atom("a"))
),
CompoundTerm(Atom("+"), listOf(Integer(1))) to Positive(Integer(1)),
CompoundTerm(Atom("+"), listOf(Atom("+"))) to CompoundTerm(
Atom("+"),
listOf(Atom("+"))
),
CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2))) to Add(
Integer(1), Integer(2)
),
CompoundTerm(Atom("+"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
Atom("+"),
listOf(Atom("1"), Atom("2"))
),
CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
Atom("+"),
listOf(Integer(1), Integer(2), Integer(3))
)
)
)
}
@Test
fun multiply() {
test(
mapOf(
Atom("*") to Atom("*"),
CompoundTerm(Atom("*"), emptyList()) to CompoundTerm(Atom("*"), emptyList()),
Atom("Multiply") to Atom("Multiply"),
CompoundTerm(Atom("Multiply"), emptyList()) to CompoundTerm(
Atom("Multiply"),
emptyList()
),
CompoundTerm(Atom("*"), listOf(Atom("a"))) to CompoundTerm(
Atom("*"),
listOf(Atom("a"))
),
CompoundTerm(Atom("*"), listOf(Integer(1))) to CompoundTerm(Atom("*"), listOf(Integer(1))),
CompoundTerm(Atom("*"), listOf(Atom("*"))) to CompoundTerm(
Atom("*"),
listOf(Atom("*"))
),
CompoundTerm(Atom("*"), listOf(Integer(1), Integer(2))) to Multiply(
Integer(1), Integer(2)
),
CompoundTerm(Atom("*"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
Atom("*"),
listOf(Atom("1"), Atom("2"))
),
CompoundTerm(Atom("*"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
Atom("*"),
listOf(Integer(1), Integer(2), Integer(3))
)
)
)
}
@Test
fun divide() {
test(
mapOf(
Atom("/") to Atom("/"),
CompoundTerm(Atom("/"), emptyList()) to CompoundTerm(Atom("/"), emptyList()),
Atom("Divide") to Atom("Divide"),
CompoundTerm(Atom("Divide"), emptyList()) to CompoundTerm(
Atom("Divide"),
emptyList()
),
CompoundTerm(Atom("/"), listOf(Atom("a"))) to CompoundTerm(
Atom("/"),
listOf(Atom("a"))
),
CompoundTerm(Atom("/"), listOf(Integer(1))) to CompoundTerm(Atom("/"), listOf(Integer(1))),
CompoundTerm(Atom("/"), listOf(Atom("/"))) to CompoundTerm(
Atom("/"),
listOf(Atom("/"))
),
CompoundTerm(Atom("/"), listOf(Integer(1), Integer(2))) to Divide(
Integer(1), Integer(2)
),
CompoundTerm(Atom("/"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
Atom("/"),
listOf(Atom("1"), Atom("2"))
),
CompoundTerm(Atom("/"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
Atom("/"),
listOf(Integer(1), Integer(2), Integer(3))
)
)
)
}
@Test
fun between() {
test(
mapOf(
Atom("between") to Atom("between"),
CompoundTerm(Atom("between"), emptyList()) to CompoundTerm(
Atom("between"),
emptyList()
),
Atom("Between") to Atom("Between"),
CompoundTerm(Atom("Between"), emptyList()) to CompoundTerm(
Atom("Between"),
emptyList()
),
CompoundTerm(Atom("between"), listOf(Atom("a"))) to CompoundTerm(
Atom("between"),
listOf(Atom("a"))
),
CompoundTerm(Atom("between"), listOf(Integer(1))) to CompoundTerm(
Atom("between"),
listOf(Integer(1))
),
CompoundTerm(Atom("between"), listOf(Atom("between"))) to CompoundTerm(
Atom("between"),
listOf(Atom("between"))
),
CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2))) to CompoundTerm(
Atom("between"),
listOf(Integer(1), Integer(2))
),
CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2), Integer(3))) to Between(
Integer(1), Integer(2), Integer(3)
),
)
)
}
@Test
fun `fun combinations`() {
/*
* [X - 1] is [(1 + 2) * ((12 / 3) - 0)]
* should return
* X = 13
*/
val sum_ = CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2)))
val sum = Add(Integer(1), Integer(2))
val div_ = CompoundTerm(Atom("/"), listOf(Integer(12), Integer(3)))
val div = Divide(Integer(12), Integer(3))
val sub_ = CompoundTerm(Atom("-"), listOf(div_, Integer(0)))
val sub = Subtract(div, Integer(0))
val right_ = CompoundTerm(Atom("*"), listOf(sum_, sub_))
val right = Multiply(sum, sub)
val left_ = CompoundTerm(Atom("-"), listOf(Variable("X"), Integer(1)))
val left = Subtract(Variable("X"), Integer(1))
val expr_ = CompoundTerm(Atom("is"), listOf(left_, right_))
val expr = Is(left, right)
val result = OpenPreprocessor().preprocess(expr_)
assertEquals(expr, result)
assertEquals(Is::class, result::class)
val `is` = result as Is
assertEquals(left, `is`.number)
assertEquals(Subtract::class, `is`.number::class)
assertEquals(right, `is`.expr)
assertEquals(Multiply::class, `is`.expr::class)
val multiply = `is`.expr as Multiply
assertEquals(sum, multiply.expr1)
assertEquals(Add::class, multiply.expr1::class)
}
}
@Nested
class `Control operators` {
private var preprocessor = OpenPreprocessor()
@Test
fun fail() {
test(
mapOf(
Atom("fail") to Fail,
CompoundTerm(Atom("fail"), emptyList()) to Fail,
Atom("Fail") to Atom("Fail"),
CompoundTerm(Atom("Fail"), emptyList()) to CompoundTerm(Atom("Fail"), emptyList()),
CompoundTerm(Atom("fail"), listOf(Atom("a"))) to CompoundTerm(Atom("fail"), listOf(Atom("a"))),
CompoundTerm(Atom("fail"), listOf(Atom("fail"))) to CompoundTerm(Atom("fail"), listOf(Fail))
)
)
}
@Test
fun `true`() {
test(
mapOf(
Atom("true") to True,
CompoundTerm(Atom("true"), emptyList()) to True,
Atom("True") to Atom("True"),
CompoundTerm(Atom("True"), emptyList()) to CompoundTerm(Atom("True"), emptyList()),
CompoundTerm(Atom("true"), listOf(Atom("a"))) to CompoundTerm(Atom("true"), listOf(Atom("a"))),
CompoundTerm(Atom("true"), listOf(Atom("true"))) to CompoundTerm(Atom("true"), listOf(True))
)
)
}
@Test
fun cut() {
test(
mapOf(
Atom("!") to Cut(),
CompoundTerm(Atom("!"), emptyList()) to Cut(),
CompoundTerm(Atom("!"), listOf(Atom("a"))) to CompoundTerm(Atom("!"), listOf(Atom("a"))),
CompoundTerm(Atom("!"), listOf(Atom("!"))) to CompoundTerm(Atom("!"), listOf(Cut()))
)
)
}
@Test
fun conjunction() {
test(
mapOf(
CompoundTerm(Atom(","), listOf(Atom("a"), Atom("b"))) to Conjunction(Atom("a"), Atom("b")),
CompoundTerm(Atom(","), listOf(Atom("a"), Atom("b"), Atom("c"))) to CompoundTerm(
Atom(","),
listOf(Atom("a"), Atom("b"), Atom("c"))
),
// Nested conjunctions
CompoundTerm(
Atom(","),
listOf(Atom("a"), CompoundTerm(Atom(","), listOf(Atom("b"), Atom("c"))))
) to Conjunction(Atom("a"), Conjunction(Atom("b"), Atom("c"))),
)
)
}
@Test
fun disjunction() {
test(
mapOf(
CompoundTerm(Atom(";"), listOf(Atom("a"), Atom("b"))) to Disjunction(Atom("a"), Atom("b")),
CompoundTerm(Atom(";"), listOf(Atom("a"), Atom("b"), Atom("c"))) to CompoundTerm(
Atom(";"),
listOf(Atom("a"), Atom("b"), Atom("c"))
),
// Nested disjunctions
CompoundTerm(
Atom(";"),
listOf(Atom("a"), CompoundTerm(Atom(";"), listOf(Atom("b"), Atom("c"))))
) to Disjunction(Atom("a"), Disjunction(Atom("b"), Atom("c"))),
)
)
}
@Test
fun not() {
test(
mapOf(
CompoundTerm(Atom("\\+"), listOf(Atom("a"))) to Not(Atom("a")),
CompoundTerm(Atom("\\+"), listOf(Atom("a"), Atom("b"))) to CompoundTerm(
Atom("\\+"),
listOf(Atom("a"), Atom("b"))
),
// Nested not
CompoundTerm(
Atom("foo"),
listOf(
Atom("bar"),
CompoundTerm(Atom("\\+"), listOf(CompoundTerm(Atom("\\+"), listOf(Atom("baz")))))
)
) to CompoundTerm(Atom("foo"), listOf(Atom("bar"), Not(Not(Atom("baz"))))),
)
)
}
@Test
fun `is`() {
test(
mapOf(
CompoundTerm(Atom("is"), listOf(Variable("T"), Integer(1))) to Is(Variable("T"), Integer(1)),
CompoundTerm(Atom("is"), listOf(Variable("T"), Add(Variable("HP"), Integer(5)))) to Is(
Variable("T"),
Add(Variable("HP"), Integer(5))
),
CompoundTerm(Atom("is"), listOf(Variable("T"), Subtract(Variable("HP"), Integer(5)))) to Is(
Variable("T"),
Subtract(Variable("HP"), Integer(5))
),
)
)
}
}
@Nested
class `Database operators` {
private val preprocessor = OpenPreprocessor()
@Test
fun `assert(fact)`() {
val input = Structure(
Atom("assert"), listOf(
Structure(
Atom(":-"), listOf(
Atom("a"),
Atom("b")
)
)
)
)
val expected = Assert(
Rule(
Atom("a"),
Atom("b")
)
)
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
@Test
fun `asserta(fact)`() {
val input = Structure(
Atom("asserta"), listOf(
Structure(
Atom(":-"), listOf(
Atom("a"),
Atom("b")
)
)
)
)
val expected = AssertA(
Rule(
Atom("a"),
Atom("b")
)
)
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
@Test
fun `assertz(fact)`() {
val input = Structure(
Atom("assertz"), listOf(
Structure(
Atom(":-"), listOf(
Atom("a"),
Atom("b")
)
)
)
)
val expected = AssertZ(
Rule(
Atom("a"),
Atom("b")
)
)
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
@Test
fun `retract(atom)`() {
val input = Structure(
Atom("retract"), listOf(
Atom("a")
)
)
val expected = Retract(Atom("a"))
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
@Test
fun `retract(compund with variable)`() {
val input = Structure(
Atom("retract"), listOf(
CompoundTerm(Atom("a"), listOf(Variable("X")))
)
)
val expected = Retract(CompoundTerm(Atom("a"), listOf(Variable("X"))))
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
@Test
fun `dynamic declaration`() {
val input = Structure(
Atom("dynamic"), listOf(
Atom("declaration/1")
)
)
val expected = Dynamic("declaration/1")
val result = preprocessor.preprocess(input)
assertEquals(expected, result)
}
}
}

16
tests/interpreter/SourceFileReaderTests.kt
View file

@ -2,31 +2,27 @@ package interpreter
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import prolog.Program
import prolog.ast.Database.Program
class SourceFileReaderTests {
@BeforeEach
fun setup() {
Program.clear()
Program.reset()
}
@Test
fun a() {
val inputFile = "tests/better_parser/resources/a.pl"
val reader = SourceFileReader()
val inputFile = "tests/parser/resources/a.pl"
val reader = FileLoader()
reader.readFile(inputFile)
println(Program.predicates)
}
@Test
fun foo() {
val inputFile = "tests/better_parser/resources/foo.pl"
val reader = SourceFileReader()
val inputFile = "tests/parser/resources/foo.pl"
val reader = FileLoader()
reader.readFile(inputFile)
println(Program.predicates)
}
}

62
tests/lexer/ScanPrologParserTests.kt
View file

@ -1,62 +0,0 @@
package lexer
import lexer.errors.LexingError
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 ScanPrologParserTests {
@Test
fun scan_simple_atom() {
val tokens = Lexer("atom.").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() {
val tokens = Lexer("X.").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_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<LexingError> { Lexer("1X.").scan() }
}
}

191
tests/lexer/ScanTests.kt
View file

@ -1,191 +0,0 @@
package lexer
import lexer.errors.LexingError
import org.junit.jupiter.api.Test
import org.junit.jupiter.api.assertThrows
import org.junit.jupiter.api.Assertions.*
class ScanTests {
@Test
fun scan_emptyString_returns_EOF() {
val tokens = Lexer("").scan()
assertEquals(1, tokens.size, "Expected 1 token, got ${tokens.size}")
assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
}
@Test
fun scan_unknownSymbol_returns_Error() {
assertThrows<LexingError> { Lexer("€").scan() }
}
@Test
fun scan_dot_returns_Dot() {
val tokens = Lexer(".").scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.DOT, tokens[0].type, "Expected DOT token, got ${tokens[0].type}")
assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
}
@Test
fun scan_two_dots_returns_two_dots() {
val tokens = Lexer("..").scan()
assertEquals(3, tokens.size)
assertEquals(TokenType.DOT, tokens[0].type, "Expected DOT 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_letter_returns_letter() {
val tokens = Lexer("a").scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
assertEquals(0, tokens[0].position.line, "Expected line 0, got ${tokens[0].position.line}")
assertEquals(0, tokens[0].position.column, "Expected column 0, got ${tokens[0].position.column}")
assertEquals(1, tokens[0].position.length, "Expected length 1, got ${tokens[0].position.length}")
}
@Test
fun scan_word_returns_alphanumerics() {
val lexer = Lexer("word")
val tokens = lexer.scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
assertEquals(4, tokens[0].position.length, "Expected length 4, got ${tokens[0].position.length}")
assertEquals("word", tokens[0].value, "Expected 'word', got ${tokens[0].value}")
}
@Test
fun scan_space_returns_nothing() {
val lexer = Lexer(" ")
val tokens = lexer.scan()
assertEquals(1, tokens.size)
assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
}
@Test
fun scan_whitespace_various_returns_nothing() {
val lexer = Lexer(" \t\n\r")
val tokens = lexer.scan()
assertEquals(1, tokens.size)
assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
}
@Test
fun scan_separated_words() {
val tokens = Lexer("word1 word2").scan()
assertEquals(3, tokens.size, "Expected 3 tokens, got ${tokens.size}")
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals("word1", tokens[0].value, "Expected 'word1', got ${tokens[0].value}")
assertEquals(5, tokens[0].position.length, "Expected length 5, got ${tokens[0].position.length}")
assertEquals(TokenType.ALPHANUMERIC, tokens[1].type, "Expected ALPHANUMERIC token, got ${tokens[1].type}")
assertEquals("word2", tokens[1].value, "Expected 'word2', got ${tokens[1].value}")
assertEquals(5, tokens[1].position.length, "Expected length 5, got ${tokens[1].position.length}")
}
@Test
fun scan_multiline() {
val tokens = Lexer(
"""
word1
word2
""".trimIndent()
).scan()
assertEquals(3, tokens.size, "Expected 3 tokens, got ${tokens.size}")
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals("word1", tokens[0].value, "Expected 'word1', got ${tokens[0].value}")
assertEquals(5, tokens[0].position.length, "Expected length 5, got ${tokens[0].position.length}")
assertEquals(TokenType.ALPHANUMERIC, tokens[1].type, "Expected ALPHANUMERIC token, got ${tokens[1].type}")
assertEquals("word2", tokens[1].value, "Expected 'word2', got ${tokens[1].value}")
assertEquals(5, tokens[1].position.length, "Expected length 5, got ${tokens[1].position.length}")
}
@Test
fun scan_parenthesis_returns_parenthesis() {
val lexer = Lexer("()")
val tokens = lexer.scan()
assertEquals(3, tokens.size)
assertEquals(
TokenType.PARENTHESIS_LEFT,
tokens[0].type,
"Expected LEFT_PARENTHESES token, got ${tokens[0].type}"
)
assertEquals(
TokenType.PARENTHESIS_RIGHT,
tokens[1].type,
"Expected RIGHT_PARENTHESES token, got ${tokens[1].type}"
)
assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
}
@Test
fun scan_simple_quoted_string_returns_string() {
val lexer = Lexer("\"string\"")
val tokens = lexer.scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
assertEquals("string", tokens[0].value, "Expected 'string', got ${tokens[0].value}")
}
@Test
fun scan_quoted_string_with_space_returns_string() {
val lexer = Lexer("\"string with space\"")
val tokens = lexer.scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
assertEquals("string with space", tokens[0].value, "Expected 'string with space', got ${tokens[0].value}")
}
@Test
fun scan_comments_returns_nothing() {
val lexer = Lexer("% comment")
val tokens = lexer.scan()
assertEquals(1, tokens.size)
assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
}
@Test
fun scan_comment_and_sentence_returns_sentence() {
val tokens = Lexer("""
% comment
sentence
""".trimIndent()).scan()
assertEquals(2, tokens.size)
assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
assertEquals("sentence", tokens[0].value, "Expected 'sentence', got ${tokens[0].value}")
}
}

43
tests/parser/OperatorParserTests.kt Normal file
View file

@ -0,0 +1,43 @@
package parser
import com.github.h0tk3y.betterParse.combinators.use
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.assertEquals
import org.junit.jupiter.api.Test
import parser.grammars.TermsGrammar
import prolog.ast.terms.Atom
import prolog.ast.terms.CompoundTerm
import prolog.ast.terms.Operator
import prolog.ast.terms.Structure
class OperatorParserTests {
class OperatorParser: TermsGrammar() {
override val rootParser: Parser<CompoundTerm> by body use { this as CompoundTerm }
}
private var parser = OperatorParser() as Grammar<CompoundTerm>
@Test
fun `parse conjunction`() {
val input = "a, b"
val result = parser.parseToEnd(input)
assertEquals(Structure(Atom(","), listOf(Atom("a"), Atom("b"))), result, "Expected atom 'a, b'")
}
class BodyParser : TermsGrammar() {
override val rootParser: Parser<Any> 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'")
}
}

4
tests/parser/ParseFromTextTests.kt
View file

@ -1,4 +0,0 @@
package parser
class ParseFromTextTests {
}

91
tests/parser/ParseTests.kt
View file

@ -1,91 +0,0 @@
package parser
import lexer.Token
import lexer.state.TokenPosition
import lexer.TokenType
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.Test
import prolog.ast.terms.Atom
import prolog.ast.terms.CompoundTerm
class ParseTests {
@Test
fun `parse atom a`() {
val input = Token(TokenType.ALPHANUMERIC, "a", TokenPosition(0, 0, 1))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom("a"), result[0], "Expected atom 'a'")
}
@Test
fun `parse atom foo`() {
val input = Token(TokenType.ALPHANUMERIC, "foo", TokenPosition(0, 0, 3))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom("foo"), result[0], "Expected atom 'foo'")
}
@Test
fun `parse atom foo1`() {
val input = Token(TokenType.ALPHANUMERIC, "foo1", TokenPosition(0, 0, 4))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom("foo1"), result[0], "Expected atom 'foo1'")
}
@Test
fun `parse atom fooBar`() {
val name = "fooBar"
val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 6))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom(name), result[0], "Expected atom 'fooBar'")
}
@Test
fun `parse atom foo_bar`() {
val name = "foo_bar"
val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 7))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom(name), result[0], "Expected atom 'foo_bar'")
}
@Test
fun `parse atom my_FooBar1`() {
val name = "my_FooBar1"
val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 11))
val result = Parser(listOf(input)).parse()
assertEquals(1, result.size, "Expected 1 term")
assertEquals(Atom(name), result[0], "Expected atom 'my_FooBar1'")
}
@Test
fun `parse compound term f()`() {
val input = listOf(
Token(TokenType.ALPHANUMERIC, "f", TokenPosition(0, 0, 1)),
Token(TokenType.PARENTHESIS_LEFT, "(", TokenPosition(0, 1, 2)),
Token(TokenType.PARENTHESIS_RIGHT, ")", TokenPosition(0, 3, 4))
)
val result = Parser(input).parse()
assertEquals(1, result.size, "Expected 1 term")
assertTrue(result[0] is CompoundTerm)
assertEquals("f", (result[0] as CompoundTerm).name)
assertEquals(0, (result[0] as CompoundTerm).arguments.size)
}
}

75
tests/parser/builtins/DatabaseOperatorsParserTests.kt Normal file
View file

@ -0,0 +1,75 @@
package parser.builtins
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import parser.grammars.TermsGrammar
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
class DatabaseOperatorsParserTests {
private lateinit var parser: Grammar<Term>
@BeforeEach
fun setup() {
parser = TermsGrammar() as Grammar<Term>
}
@Test
fun `parse assert(rule)`() {
val input = "assert((a :- b))"
val expected = Structure(Atom("assert"), listOf(
Structure(Atom(":-"), listOf(
Atom("a"),
Atom("b")
))
))
val result = parser.parseToEnd(input)
assertEquals(expected, result)
}
@Test
fun `parse assertA(rule)`() {
val input = "assertA((a :- b))"
val expected = Structure(Atom("assertA"), listOf(
Structure(Atom(":-"), listOf(
Atom("a"),
Atom("b")
))
))
val result = parser.parseToEnd(input)
assertEquals(expected, result)
}
@Test
fun `parse assertZ(rule)`() {
val input = "assertZ((a :- b))"
val expected = Structure(Atom("assertZ"), listOf(
Structure(Atom(":-"), listOf(
Atom("a"),
Atom("b")
))
))
val result = parser.parseToEnd(input)
assertEquals(expected, result)
}
@Test
fun `parse dynamic declaration`() {
val input = "dynamic declaration/1"
val expected = Structure(Atom("dynamic"), listOf(Atom("declaration/1")))
val result = parser.parseToEnd(input)
assertEquals(expected, result)
}
}

48
tests/better_parser/SimpleSourcePrologParserTests.kt → tests/parser/grammars/LogicGrammarTests.kt
View file

@ -1,7 +1,8 @@
package better_parser
package parser.grammars
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
@ -14,14 +15,13 @@ import prolog.ast.terms.CompoundTerm
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.builtins.Conjunction
import prolog.builtins.Disjunction
class SimpleSourcePrologParserTests {
class LogicGrammarTests {
private lateinit var parser: Grammar<List<Clause>>
@BeforeEach
fun setup() {
parser = SimpleSourceParser() as Grammar<List<Clause>>
parser = LogicGrammar() as Grammar<List<Clause>>
}
@ParameterizedTest
@ -40,7 +40,7 @@ class SimpleSourcePrologParserTests {
assertEquals(1, result.size, "Expected 1 fact")
assertTrue(result[0] is Fact, "Expected a fact")
assertEquals(input, "${result[0].toString()}.", "Expected fact to be '$input'")
assertEquals(input, "${result[0]}.", "Expected fact to be '$input'")
}
@ParameterizedTest
@ -114,7 +114,7 @@ class SimpleSourcePrologParserTests {
assertEquals(1, result.size, "Expected 1 rule")
assertInstanceOf(Rule::class.java, result[0], "Expected a rule")
val rule = result[0] as Rule
assertInstanceOf(Conjunction::class.java, rule.body, "Expected body to be a conjunction")
assertInstanceOf(CompoundTerm::class.java, rule.body, "Expected body to be a compound term")
}
@Test
@ -125,8 +125,38 @@ class SimpleSourcePrologParserTests {
assertEquals(1, result.size, "Expected 1 rule")
val rule = result[0] as Rule
assertTrue(rule.body is Conjunction, "Expected body to be a conjunction")
val conjunction = rule.body as Conjunction
assertEquals("invited/2", (conjunction.left as CompoundTerm).functor, "Expected functor 'invited/2'")
assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'")
assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm
assertEquals(",/2", l1.functor, "Expected functor ',/2'")
val l2 = l1.arguments[0] as CompoundTerm
assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'")
}
@Test
fun `parse check_identical(X, Y)`() {
var input = "check_identical(X, Y) :- X == Y."
assertDoesNotThrow {
val result = parser.parseToEnd(input)
}
input = "check_identical(X, Y) :- X = Y, !, write('X == Y succeeded'), nl."
assertDoesNotThrow {
val result = parser.parseToEnd(input)
}
}
@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")
}
}

355
tests/parser/grammars/TermsGrammarTests.kt Normal file
View file

@ -0,0 +1,355 @@
package parser.grammars
import com.github.h0tk3y.betterParse.grammar.Grammar
import com.github.h0tk3y.betterParse.grammar.parseToEnd
import org.junit.jupiter.api.Assertions
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Nested
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
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.builtins.Is
import prolog.logic.equivalent
class TermsGrammarTests {
private lateinit var parser: Grammar<Term>
@BeforeEach
fun setup() {
parser = TermsGrammar() as Grammar<Term>
}
@ParameterizedTest
@ValueSource(strings = ["a", "foo", "foo1", "fooBar", "foo_bar"])
fun `parse atom`(name: String) {
val result = parser.parseToEnd(name)
assertEquals(Atom(name), result, "Expected atom '$name'")
}
@ParameterizedTest
@ValueSource(
strings = [
"'tick'",
"\"doubleTick\"",
"`backTick`",
"'i have spaces'",
"`i have a 'quote' inside`",
"'I have Cases'",
"'I, h@v3 many (!!!) special characters?! {}'"
]
)
fun `Parse a quoted atom`(input: String) {
val result = parser.parseToEnd(input)
val expected = input.substring(1, input.length - 1)
assertEquals(Atom(expected), result, "Expected atom")
}
@ParameterizedTest
@ValueSource(strings = ["X", "X1", "X_1"])
fun `parse variable`(name: String) {
val result = parser.parseToEnd(name)
assertEquals(Variable(name), result)
}
@Test
fun `parse anonymous variable`() {
val input = "_"
val result = parser.parseToEnd(input)
assertEquals(Variable("_"), result, "Expected anonymous variable")
}
@Test
fun `empty compound term`() {
val input = "f()"
val result = parser.parseToEnd(input)
assertEquals(Structure(Atom("f"), emptyList()), result, "Expected atom 'f'")
}
@Test
fun `parse compound term f(a)`() {
val input = "f(a)"
val result = parser.parseToEnd(input)
assertEquals(Structure(Atom("f"), listOf(Atom("a"))), result, "Expected atom 'f(a)'")
}
@Test
fun `parse compound term f(a, b)`() {
val input = "f(a, b)"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("f"), listOf(Atom("a"), Atom("b"))),
result,
"Expected atom 'f(a, b)'"
)
}
@Test
fun `parse compound term with variable f(a, X)`() {
val input = "f(a, X)"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("f"), listOf(Atom("a"), Variable("X"))),
result,
"Expected atom 'f(a, X)'"
)
}
@Test
fun `parse compound term with var and int`() {
val input = "check_identical(A, 13)"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("check_identical"), listOf(Variable("A"), Integer(13))),
result,
"Expected atom 'check_identical(A, 13)'"
)
}
@Test
fun `parse nested compound term f(a, g(b))`() {
val input = "f(a, g(b))"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))),
result,
"Expected atom 'f(a, g(b))'"
)
}
@Test
fun `parse compound term with variable f(a, g(X))`() {
val input = "f(a, g(X))"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))),
result,
"Expected atom 'f(a, g(X))'"
)
}
@Test
fun `parse nested compound term with variables`() {
val input = "hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))"
val result = parser.parseToEnd(input)
assertEquals(
Structure(
Atom("hit"),
listOf(
Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("HP"))),
Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("T")))
)
),
result,
"Expected atom 'hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))'"
)
}
@Test
fun `parse compound term with anonymous variables`() {
val input = "f(a, _, g(X))"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("f"), listOf(Atom("a"), Variable("_"), Structure(Atom("g"), listOf(Variable("X"))))),
result,
"Expected atom 'f(a, _, g(X))'"
)
}
@ParameterizedTest
@ValueSource(ints = [0, 1, 5, 12, 345, 123456789])
fun `parse positive integer`(number: Int) {
val input = number.toString()
val result = parser.parseToEnd(input)
assertEquals(Integer(number), result, "Expected integer '$number'")
}
@ParameterizedTest
@ValueSource(ints = [-987654321, -543, -21, -1])
fun `parse negative integer`(number: Int) {
val input = number.toString()
val result = parser.parseToEnd(input)
assertEquals(Structure(Atom("-"), listOf(Integer(0 - number))), result, "Expected integer '$number'")
}
@Test
fun `parse float`() {
val input = "42.0"
val result = parser.parseToEnd(input)
assertEquals(Float(42.0f), result, "Expected float '42.0'")
}
@Test
fun `parse negative float`() {
val input = "-42.0"
val result = parser.parseToEnd(input)
assertEquals(Structure(Atom("-"), listOf(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) }
}
@Nested
class `Operators and precedence` {
private lateinit var parser: Grammar<Term>
@BeforeEach
fun setup() {
parser = TermsGrammar() as Grammar<Term>
}
@Test
fun `can parse equivalent`() {
val input = "X == Y"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("=="), listOf(Variable("X"), Variable("Y"))),
result,
"Expected equivalent operator"
)
}
@Test
fun `can parse cut`() {
val input = "!"
val result = parser.parseToEnd(input)
assertEquals(Atom("!"), result, "Expected cut operator")
}
@Test
fun `can parse 'is'`() {
val input = "T is 1"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("is"), listOf(Variable("T"), Integer(1))),
result
)
}
@Test
fun `can parse 'is' with addition`() {
val input = "T is 1 + 2"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("is"), listOf(Variable("T"), Structure(Atom("+"), listOf(Integer(1), Integer(2))))),
result
)
}
@ParameterizedTest
@ValueSource(strings = ["+", "-", "*", "/"])
fun `can parse with spaces`(operator: String) {
val input = "1 $operator 2"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom(operator), listOf(Integer(1), Integer(2))),
result,
"Expected operator '$operator'"
)
}
@ParameterizedTest
@ValueSource(strings = ["+", "-", "*", "/"])
fun `can parse without spaces`(operator: String) {
val input = "1${operator}2"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom(operator), listOf(Integer(1), Integer(2))),
result,
"Expected operator '$operator' without spaces"
)
}
@Test
fun `parse addition and multiplication`() {
val input = "1 + 2 * 3"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("+"), listOf(Integer(1), Structure(Atom("*"), listOf(Integer(2), Integer(3))))),
result,
"Expected addition and multiplication"
)
}
@Test
fun `parse multiplication and addition`() {
val input = "1 * 2 + 3"
val result = parser.parseToEnd(input)
assertEquals(
Structure(Atom("+"), listOf(Structure(Atom("*"), listOf(Integer(1), Integer(2))), Integer(3))),
result,
"Expected multiplication and addition"
)
}
@Test
fun `complex expression`() {
val input = "1 + 2 * 3 - 4 / 5"
val result = parser.parseToEnd(input)
assertEquals(
Structure(
Atom("-"),
listOf(
Structure(Atom("+"), listOf(Integer(1), Structure(Atom("*"), listOf(Integer(2), Integer(3))))),
Structure(Atom("/"), listOf(Integer(4), Integer(5)))
)
),
result,
"Expected complex expression"
)
}
}
}

0
tests/better_parser/resources/a.pl → tests/parser/resources/a.pl
View file

0
tests/better_parser/resources/foo.pl → tests/parser/resources/foo.pl
View file

3
tests/better_parser/resources/parent.pl → tests/parser/resources/parent.pl
View file

@ -5,6 +5,3 @@ parent(john, jimmy).
parent(mary, jimmy).
father(X, Y) :- parent(X, Y), male(X).
mother(X, Y) :- parent(X, Y), female(X).
foo(0).
foo(X) :- X > 0, Y is X - 1, foo(Y).

239
tests/prolog/EvaluationTests.kt
View file

@ -2,20 +2,23 @@ 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.arithmetic.Integer
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.builtins.Conjunction
import prolog.builtins.Disjunction
import prolog.builtins.Query
import prolog.logic.equivalent
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.builtins.*
import prolog.ast.Database.Program
class EvaluationTests {
@BeforeEach
fun setUp() {
Program.clear()
Program.reset()
}
@Test
@ -105,20 +108,24 @@ class EvaluationTests {
val variable2 = Variable("Y")
val parent = Rule(
Structure(Atom("parent"), listOf(variable1, variable2)),
/* :- */ Disjunction(
Structure(Atom("father"), listOf(variable1, variable2)),
/* ; */
Structure(Atom("mother"), listOf(variable1, variable2))
Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */
Disjunction(
Structure(Atom("father"), listOf(variable1, variable2)),
/* ; */
Structure(Atom("mother"), listOf(variable1, variable2))
)
)
Program.load(listOf(father, mother, parent))
val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
assertTrue(result1.toList().isNotEmpty())
val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
assertTrue(result2.toList().isNotEmpty())
val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList()
assertEquals(1, result1.size, "Expected 1 result")
assertTrue(result1[0].isSuccess, "Expected success")
assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList()
assertEquals(1, result2.size, "Expected 1 result")
assertTrue(result2[0].isSuccess, "Expected success")
assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
assertFalse(result3.any())
@ -211,36 +218,204 @@ 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")
}
}
/**
foo(0).
foo(X) :- X > 0, Y is X - 1, foo(Y).
*/
@Test
fun recursive_query() {
val fact = Fact(Structure(Atom("foo"), listOf(Integer(0))))
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("foo"), listOf(Variable("X"))),
Conjunction(
GreaterThan(Variable("X"), Integer(0)),
Conjunction(
Is(Variable("Y"), Subtract(Variable("X"), Integer(1))),
Structure(Atom("foo"), listOf(Variable("Y")))
)
)
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(Structure(Atom("foo"), listOf(Integer(0)))).toList()
val result = Program.query(goal).toList()
val result5 = Program.query(Structure(Atom("foo"), listOf(Integer(5)))).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")
}
assertTrue(Program.query(Structure(Atom("foo"), listOf(Atom("1")))).any())
assertTrue(Program.query(Structure(Atom("foo"), listOf(Atom("2")))).any())
assertFalse(Program.query(Structure(Atom("foo"), listOf(Atom("-1")))).any())
@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.reset()
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")
}
@Test
fun `likes_italian_food(Person)`() {
val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Variable("Person")))).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")
assertEquals(Atom("alice"), subs3[Variable("Person")], "Expected alice")
assertTrue(result[1].isSuccess, "Expected success")
val subs4 = result[1].getOrNull()!!
assertEquals(1, subs4.size, "Expected 1 substitution")
assertEquals(Atom("alice"), subs4[Variable("Person")], "Expected alice")
assertTrue(result[2].isSuccess, "Expected success")
val subs5 = result[2].getOrNull()!!
assertEquals(1, subs5.size, "Expected 1 substitution")
assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
}
}
}

28
tests/prolog/builtins/ControlOperatorsTests.kt
View file

@ -3,7 +3,7 @@ package prolog.builtins
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import prolog.Program
import prolog.ast.Database.Program
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.ast.terms.Atom
@ -14,7 +14,25 @@ import prolog.ast.terms.Variable
class ControlOperatorsTests {
@BeforeEach
fun setUp() {
Program.clear()
Program.reset()
}
@Test
fun `rule with cut as body`() {
Program.load(
listOf(
Rule(Atom("foo"), Cut()),
Fact(Atom("foo"))
)
)
val goal = Atom("foo")
val result = Program.query(goal).toList()
assertEquals(1, result.size, "Expected 1 result")
assertTrue(result[0].isSuccess, "Expected success")
assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions")
}
// See also: https://stackoverflow.com/a/23292126
@ -37,7 +55,7 @@ class ControlOperatorsTests {
// Now with cut
Program.clear()
Program.reset()
Program.load(
listOf(
@ -86,7 +104,7 @@ class ControlOperatorsTests {
// Now with cut in the middle
Program.clear()
Program.reset()
Program.load(
listOf(
@ -120,7 +138,7 @@ class ControlOperatorsTests {
// Now with cut at the end
Program.clear()
Program.reset()
Program.load(
listOf(

295
tests/prolog/builtins/DatabaseOperatorsTests.kt Normal file
View file

@ -0,0 +1,295 @@
package prolog.builtins
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Assertions.assertFalse
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Nested
import org.junit.jupiter.api.Test
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.ValueSource
import prolog.ast.Database
import prolog.ast.Database.Program
import prolog.ast.logic.Clause
import prolog.ast.logic.Fact
import prolog.ast.logic.Predicate
import prolog.ast.logic.Rule
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
class DatabaseOperatorsTests {
@BeforeEach
fun setup() {
Program.reset()
}
abstract class AssertTestsBase<T : Structure> {
protected abstract fun createAssert(clause: Clause): Structure
@BeforeEach
fun setup() {
Program.reset()
}
@ParameterizedTest
@ValueSource(classes = [AssertA::class, AssertZ::class, Assert::class])
fun `assert(fact atom)`(assertKind: Class<*>) {
val fact = Fact(Atom("a"))
createAssert(fact).satisfy(emptyMap())
assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0])
}
@Test
fun `assert(fact structure)`() {
val fact = Fact(Structure(Atom("a"), listOf(Atom("b"))))
createAssert(fact).satisfy(emptyMap())
assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0])
}
@Test
fun `assert(rule)`() {
val rule = Rule(
Structure(Atom("a"), listOf(Atom("b"))),
Atom("c")
)
createAssert(rule).satisfy(emptyMap())
assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0])
}
}
@Nested
class AssertTests : AssertTestsBase<Assert>() {
override fun createAssert(clause: Clause): Structure {
return Assert(clause)
}
}
@Nested
class AssertATests : AssertTestsBase<AssertA>() {
override fun createAssert(clause: Clause): Structure {
return AssertA(clause)
}
@Test
fun `asserta adds to the beginning`() {
val rule1 = Rule(
Structure(Atom("a"), listOf(Atom("b"))),
Atom("c")
)
val rule2 = Rule(
Structure(Atom("a"), listOf(Atom("d"))),
Atom("e")
)
AssertA(rule1).satisfy(emptyMap())
AssertA(rule2).satisfy(emptyMap())
assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0])
assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1])
}
}
@Nested
class AssertZTests : AssertTestsBase<AssertZ>() {
override fun createAssert(clause: Clause): Structure {
return AssertZ(clause)
}
@Test
fun `assertz adds to the end`() {
val rule1 = Rule(
Structure(Atom("a"), listOf(Atom("b"))),
Atom("c")
)
val rule2 = Rule(
Structure(Atom("a"), listOf(Atom("d"))),
Atom("e")
)
AssertZ(rule1).satisfy(emptyMap())
AssertZ(rule2).satisfy(emptyMap())
assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0])
assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1])
}
}
@Test
fun `retract fails silently for unknown predicates`() {
val retract = Retract(Atom("unknown"))
val result = retract.satisfy(emptyMap())
assertTrue(result.none(), "Expected no results")
}
@Test
fun `simple retract`() {
val predicate = Predicate(listOf(Fact(Atom("a"))))
Program.db.load(predicate)
assertEquals(1, Program.query(Atom("a")).count())
val retract = Retract(Atom("a"))
assertEquals(1, retract.satisfy(emptyMap()).toList().size, "Expected 1 result")
assertEquals(0, predicate.clauses.size, "Expected 0 clauses")
assertTrue(retract.satisfy(emptyMap()).none())
}
@Test
fun `retract atom`() {
val predicate = Predicate(listOf(
Fact(Atom("a")),
Fact(Atom("a")),
Fact(Atom("a"))
))
Program.db.load(predicate)
val control = Program.query(Atom("a")).toList()
assertEquals(3, control.size, "Expected 3 results")
val retract = Retract(Atom("a"))
val result = retract.satisfy(emptyMap()).iterator()
assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
assertTrue(result.hasNext(), "Expected more results")
val answer = result.next()
assertTrue(answer.isSuccess, "Expected success")
assertTrue(answer.getOrNull()!!.isEmpty(), "Expected no substitutions")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
assertTrue(result.next().isSuccess)
assertTrue(result.hasNext(), "Expected more results")
assertTrue(result.next().isSuccess)
assertFalse(result.hasNext(), "Expected more results")
assertEquals(0, predicate.clauses.size, "Expected no remaining clauses")
}
@Test
fun `retract compound with variable`() {
val predicate = Predicate(listOf(
Fact(Structure(Atom("a"), listOf(Atom("b")))),
Fact(Structure(Atom("a"), listOf(Atom("c")))),
Fact(Structure(Atom("a"), listOf(Atom("d"))))
))
Program.db.load(predicate)
val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
assertEquals(3, control.size, "Expected 3 results")
val retract = Retract(Structure(Atom("a"), listOf(Variable("X"))))
val result = retract.satisfy(emptyMap()).iterator()
assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
assertTrue(result.hasNext(), "Expected more results")
var answer = result.next()
assertTrue(answer.isSuccess, "Expected success")
var subs = answer.getOrNull()!!
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("b"), subs[Variable("X")], "Expected b")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
answer = result.next()
assertTrue(answer.isSuccess, "Expected success")
subs = answer.getOrNull()!!
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("c"), subs[Variable("X")], "Expected c")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(1, predicate.clauses.size, "Expected 1 clause")
answer = result.next()
assertTrue(answer.isSuccess, "Expected success")
subs = answer.getOrNull()!!
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("d"), subs[Variable("X")], "Expected d")
assertFalse(result.hasNext(), "Expected no more results")
assertEquals(0, predicate.clauses.size, "Expected no clauses")
}
@Test
fun `custom assert example`() {
var query = Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))
var result = Program.query(query).toList()
assertEquals(0, result.size, "Expected 0 results")
var assert: Structure = Assert(Fact(query))
assert.satisfy(emptyMap())
result = Program.query(query).toList()
assertEquals(1, result.size, "Expected 1 result")
assertTrue(result[0].getOrNull()!!.isEmpty())
assert = AssertZ(Fact(Structure(Atom("likes"), listOf(Atom("bob"), Atom("sushi")))))
assert.satisfy(emptyMap())
query = Structure(Atom("likes"), listOf(Atom("bob"), Variable("X")))
result = Program.query(query).toList()
assertEquals(1, result.size, "Expected 1 result")
assertTrue(result[0].isSuccess, "Expected success")
assertEquals(Atom("sushi"), result[0].getOrNull()!![Variable("X")], "Expected sushi")
query = Structure(Atom("likes"), listOf(Variable("X"), Variable("Y")))
result = Program.query(query).toList()
assertEquals(2, result.size, "Expected 2 results")
assertTrue(result[0].isSuccess, "Expected success")
var result0 = result[0].getOrNull()!!
assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice")
assertEquals(Atom("pizza"), result0[Variable("Y")], "Expected pizza")
assertTrue(result[1].isSuccess, "Expected success")
var result1 = result[1].getOrNull()!!
assertEquals(Atom("bob"), result1[Variable("X")], "Expected bob")
assertEquals(Atom("sushi"), result1[Variable("Y")], "Expected sushi")
assert = AssertA(
Rule(
Structure(Atom("likes"), listOf(Variable("X"), Atom("italian"))),
Structure(Atom("likes"), listOf(Variable("X"), Atom("pizza")))
)
)
assert.satisfy(emptyMap())
result = Program.query(query).toList()
assertEquals(3, result.size, "Expected 3 results")
assertTrue(result[0].isSuccess, "Expected success")
result0 = result[0].getOrNull()!!
assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice")
assertEquals(Atom("italian"), result0[Variable("Y")], "Expected italian")
assertTrue(result[1].isSuccess, "Expected success")
result1 = result[1].getOrNull()!!
assertEquals(Atom("alice"), result1[Variable("X")], "Expected alice")
assertEquals(Atom("pizza"), result1[Variable("Y")], "Expected pizza")
assertTrue(result[2].isSuccess, "Expected success")
val result2 = result[2].getOrNull()!!
assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob")
assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi")
}
}

164
tests/prolog/builtins/IoOperatorsTests.kt Normal file
View file

@ -0,0 +1,164 @@
package prolog.builtins
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Test
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.ValueSource
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.CompoundTerm
import prolog.ast.terms.Variable
import java.io.ByteArrayInputStream
import java.io.ByteArrayOutputStream
import java.io.PrintStream
class IoOperatorsTests {
private var outStream = ByteArrayOutputStream()
@BeforeEach
fun setup() {
outStream = ByteArrayOutputStream()
System.setOut(PrintStream(outStream))
}
@Test
fun dummyTest() {
val message = "Hello, World!"
print(message)
assertEquals(message, outStream.toString(), "Output should match the message")
}
@ParameterizedTest
@ValueSource(strings = [
"a",
"hello",
"a very special christmas",
"1 2 3 piano"
])
fun `write atoms`(name: String) {
val write = Write(Atom(name))
val result = write.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
assertEquals(name, outStream.toString(), "Output should match the atom")
}
@Test
fun `write structure`() {
val write = Write(CompoundTerm(Atom("person"), listOf(Atom("john"), Atom("doe"))))
val result = write.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
assertEquals("person(john, doe)", outStream.toString().trim(), "Output should match the structure")
}
@Test
fun `write arithmetic`() {
val a = Integer(1)
val b = Variable("B")
val c = Float(2.0f)
val d = Variable("D")
val mul = Multiply(c, d)
val sub = Subtract(b, mul)
val expr = EvaluatesTo(a, sub)
val expected1 = "(1 =:= (B - (2.0 * D)))"
val expected2 = "=:=(1, -(B, *(2.0, D)))"
val write = Write(expr)
val result = write.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
val output = outStream.toString()
assertTrue(output == expected1 || output == expected2, "Output should match the arithmetic expression")
}
@Test
fun `write nl`() {
val nl = Nl
val result = nl.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
assertTrue(outStream.toString().contains("\n"), "Output should contain a newline")
}
@Test
fun `read term`() {
val inputStream = ByteArrayInputStream("hello.".toByteArray())
System.setIn(inputStream)
val read = Read(Variable("X"))
val result = read.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
val answer = result[0].getOrNull()!!
assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
assertInstanceOf(Atom::class.java, answer[Variable("X")], "Output should be an atom")
assertEquals(Atom("hello"), answer[Variable("X")], "Output should match the read term")
}
@Test
fun `read between(1, 2, 3)`() {
val inputStream = ByteArrayInputStream("between(1, 2, 3).".toByteArray())
System.setIn(inputStream)
val read = Read(Variable("X"))
val result = read.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
val answer = result[0].getOrNull()!!
assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
assertInstanceOf(CompoundTerm::class.java, answer[Variable("X")], "Output should be a compound term")
assertEquals(
CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2), Integer(3))),
answer[Variable("X")],
"Output should match the read term"
)
}
@Test
fun `read foo(a, X, b, Y, c, Z)`() {
val inputStream = ByteArrayInputStream("foo(A, x, B, y, C, z).".toByteArray())
System.setIn(inputStream)
val read = Read(CompoundTerm(Atom("foo"), listOf(
Atom("a"),
Variable("X"),
Atom("b"),
Variable("Y"),
Atom("c"),
Variable("Z")
)))
val result = read.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Should return one result")
assertTrue(result[0].isSuccess, "Result should be successful")
val answer = result[0].getOrNull()!!
assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
assertTrue(answer.containsKey(Variable("Y")), "Result should be successful")
assertTrue(answer.containsKey(Variable("Z")), "Result should be successful")
assertEquals(Atom("x"), answer[Variable("X")], "Output should match the read term")
assertEquals(Atom("y"), answer[Variable("Y")], "Output should match the read term")
assertEquals(Atom("z"), answer[Variable("Z")], "Output should match the read term")
}
}

17
tests/prolog/logic/ArithmeticTests.kt
View file

@ -583,10 +583,23 @@ class ArithmeticTests {
assertTrue(equivalent(result[0].getOrThrow()[t3]!!, Float(6.0f), result[0].getOrNull()!!), "X should be equal to 6.0")
}
@Test
fun `addition with negative`() {
val t1 = Integer(1)
val t2 = Integer(-1)
val t3 = Integer(0)
val result = plus(t1, t2, t3, emptyMap()).toList()
assertEquals(1, result.size, "There should be one solution")
assertTrue(result[0].isSuccess, "Expected success")
assertTrue(result[0].getOrNull()!!.isEmpty(), "1 + -1 should already be equal to 0")
}
@RepeatedTest(100)
fun `random test for mul`() {
val t1 = Integer((0..1000).random())
val t2 = Integer((0..1000).random())
val t1 = Integer((-1000..1000).random())
val t2 = Integer((-1000..1000).random())
val t3 = Variable("X")
val result = mul(t1, t2, t3, emptyMap()).toList()

110
tests/prolog/logic/TermsTests.kt Normal file
View file

@ -0,0 +1,110 @@
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 variable1 = subs1[variable] as Variable
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(variable1), "Expected subs to contain the variable")
assertEquals(Variable("X@$start@$end1"), subs2[variable1], "Expected subs to contain the new term")
}
}

370
tests/prolog/logic/UnificationTests.kt Normal file
View file

@ -0,0 +1,370 @@
package prolog.logic
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.Test
import prolog.Substitutions
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.builtins.Add
import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Nested
/*
* Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
*/
class UnificationTests {
@Nested
class `unify` {
@Test
fun identical_atoms_unify() {
val atom1 = Atom("a")
val atom2 = Atom("a")
val result = unify(atom1, atom2)
assertTrue(result.isSuccess, "Identical atoms should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "Different atoms should not unify")
}
/**
* ?- X = X.
* true.
*/
@Test
fun identical_variables_unify() {
val variable1 = Variable("X")
val variable2 = Variable("X")
val result = unify(variable1, variable2)
assertTrue(result.isSuccess, "Identical variables should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "Variable should unify with atom")
assertEquals(1, result.getOrNull()!!.size, "There should be one substitution")
assertEquals(atom, result.getOrNull()!![variable], "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.isSuccess)
assertEquals(1, result.getOrNull()!!.size)
assertEquals(variable2, result.getOrNull()!![variable1], "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.isSuccess, "Identical compound terms should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "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.isSuccess, "Compound terms with different functors should not unify")
}
/**
* ?- X = f(a, b).
* X = f(a, b).
*/
@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.isSuccess, "Variable should unify with compound term")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), subs[variable]!!, subs),
"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.isSuccess, "Compound term with variable should unify with part")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
val equivalence = equivalent(Atom("b"), subs[variable]!!, subs)
assertTrue(equivalence, "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.isSuccess, "Compound terms with variable arguments should unify")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
assertEquals(variable2, subs[variable1], "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.isSuccess, "Compound terms with different arity should not unify")
}
/**
* ?- f(g(X)) = f(Y).
* Y = g(X).
*/
@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.isSuccess, "Nested compound terms with variables should unify")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("g"), listOf(Variable("X"))), subs[variable2]!!, subs),
"Variable should be substituted with compound term"
)
}
/**
* ?- f(g(X), X) = f(Y, a).
* X = a,
* Y = g(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.isSuccess, "Compound terms with more variables should unify")
val subs = result.getOrNull()!!
assertEquals(2, subs.size, "There should be two substitutions")
assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
assertTrue(
equivalent(Atom("a"), subs[variable1]!!, subs),
"Variable 1 should be substituted with atom"
)
assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("g"), listOf(Atom("a"))), subs[variable2]!!, subs),
"Variable 2 should be substituted with compound term"
)
}
/**
* ?- X = f(X).
* X = f(f(X)).
*/
@Test
@Disabled("If the occurs check is applied, this should fail")
fun recursive_unification() {
val variable1 = Variable("X")
val structure2 = Structure(Atom("f"), listOf(Variable("X")))
val result = unifyLazy(variable1, structure2, emptyMap()).toList()
assertEquals(1, result.size, "There should be one result")
assertTrue(result[0].isSuccess, "Recursive unification should succeed")
val subs = result[0].getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable1), "Variable should be in the substitution map")
assertEquals(structure2, subs[variable1], "Variable should be substituted with compound term")
}
/**
* ?- X = bar, Y = bar, X = Y.
* X = Y, Y = bar.
*/
@Test
fun multiple_unification() {
val variable1 = Variable("X")
val variable2 = Variable("Y")
val atom = Atom("bar")
val map: Substitutions = mapOf(
variable1 to atom,
variable2 to atom
)
val result = unifyLazy(variable1, variable2, map).toList()
assertEquals(1, result.size, "There should be one substitution")
assertTrue(result[0].isSuccess, "Multiple unification should succeed")
assertEquals(0, result[0].getOrNull()!!.size, "No (additional) 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.isSuccess, "Atom with different arity should not unify")
}
@Test
fun identical_integers_unify() {
val int1 = Integer(1)
val int2 = Integer(1)
val result = unify(int1, int2)
assertTrue(result.isSuccess, "Identical integers should unify")
assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
}
@Test
fun different_integers_do_not_unify() {
val int1 = Integer(1)
val int2 = Integer(2)
val result = unify(int1, int2)
assertFalse(result.isSuccess, "Different integers should not unify")
}
@Test
fun `1 + 2 does not unify with 3`() {
val expr1 = Add(Integer(1), Integer(2))
val expr2 = Integer(3)
val result = unify(expr1, expr2)
assertFalse(result.isSuccess, "1 + 2 should not unify with 3")
}
}
@Nested
class `applySubstitution` {
@Test
fun `apply substitution without sub`() {
val term = Variable("X")
val subs: Substitutions = emptyMap()
val result = applySubstitution(term, subs)
assertEquals(term, result)
}
@Test
fun `apply single substitution`() {
val sub = Variable("X") to Integer(5)
val subs: Substitutions = mapOf(sub)
val term = Variable("X")
val result = applySubstitution(term, subs)
assertEquals(Integer(5), result)
}
@Test
fun `apply chained substitution`() {
val sub1 = Variable("HP") to Variable("HP(19)")
val sub2 = Variable("HP(19)") to Integer(35)
val subs: Substitutions = mapOf(sub1, sub2)
val term = Variable("HP")
val result = applySubstitution(term, subs)
assertEquals(Integer(35), result)
}
}
}

327
tests/prolog/logic/UnifyTests.kt
View file

@ -1,327 +0,0 @@
package prolog.logic
import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Test
import prolog.Substitutions
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.builtins.Add
/*
* Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
*/
class UnifyTests {
@Test
fun identical_atoms_unify() {
val atom1 = Atom("a")
val atom2 = Atom("a")
val result = unify(atom1, atom2)
assertTrue(result.isSuccess, "Identical atoms should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "Different atoms should not unify")
}
/**
* ?- X = X.
* true.
*/
@Test
fun identical_variables_unify() {
val variable1 = Variable("X")
val variable2 = Variable("X")
val result = unify(variable1, variable2)
assertTrue(result.isSuccess, "Identical variables should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "Variable should unify with atom")
assertEquals(1, result.getOrNull()!!.size, "There should be one substitution")
assertEquals(atom, result.getOrNull()!![variable], "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.isSuccess)
assertEquals(1, result.getOrNull()!!.size)
assertEquals(variable2, result.getOrNull()!![variable1], "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.isSuccess, "Identical compound terms should unify")
assertEquals(0, result.getOrNull()!!.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.isSuccess, "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.isSuccess, "Compound terms with different functors should not unify")
}
/**
* ?- X = f(a, b).
* X = f(a, b).
*/
@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.isSuccess, "Variable should unify with compound term")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), subs[variable]!!, subs),
"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.isSuccess, "Compound term with variable should unify with part")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
val equivalence = equivalent(Atom("b"), subs[variable]!!, subs)
assertTrue(equivalence, "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.isSuccess, "Compound terms with variable arguments should unify")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
assertEquals(variable2, subs[variable1], "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.isSuccess, "Compound terms with different arity should not unify")
}
/**
* ?- f(g(X)) = f(Y).
* Y = g(X).
*/
@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.isSuccess, "Nested compound terms with variables should unify")
val subs = result.getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("g"), listOf(Variable("X"))), subs[variable2]!!, subs),
"Variable should be substituted with compound term"
)
}
/**
* ?- f(g(X), X) = f(Y, a).
* X = a,
* Y = g(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.isSuccess, "Compound terms with more variables should unify")
val subs = result.getOrNull()!!
assertEquals(2, subs.size, "There should be two substitutions")
assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
assertTrue(
equivalent(Atom("a"), subs[variable1]!!, subs),
"Variable 1 should be substituted with atom"
)
assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
assertTrue(
equivalent(Structure(Atom("g"), listOf(Atom("a"))), subs[variable2]!!, subs),
"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 = unifyLazy(variable1, structure2, emptyMap()).toList()
assertEquals(1, result.size, "There should be one result")
assertTrue(result[0].isSuccess, "Recursive unification should succeed")
val subs = result[0].getOrNull()!!
assertEquals(1, subs.size, "There should be one substitution")
assertTrue(subs.containsKey(variable1), "Variable should be in the substitution map")
assertEquals(structure2, subs[variable1], "Variable should be substituted with compound term")
}
/**
* ?- X = bar, Y = bar, X = Y.
* X = Y, Y = bar.
*/
@Disabled
@Test
fun multiple_unification() {
val variable1 = Variable("X")
val variable2 = Variable("Y")
val atom = Atom("bar")
val map: Substitutions = mapOf(
variable1 to atom,
variable2 to atom
)
val result = unifyLazy(variable1, variable2, map).toList()
assertEquals(1, result.size, "There should be one substitution")
assertTrue(result[0].isSuccess, "Multiple unification should succeed")
assertEquals(0, result[0].getOrNull()!!.size, "No (additional) 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.isSuccess, "Atom with different arity should not unify")
}
@Test
fun identical_integers_unify() {
val int1 = Integer(1)
val int2 = Integer(1)
val result = unify(int1, int2)
assertTrue(result.isSuccess, "Identical integers should unify")
assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
}
@Test
fun different_integers_do_not_unify() {
val int1 = Integer(1)
val int2 = Integer(2)
val result = unify(int1, int2)
assertFalse(result.isSuccess, "Different integers should not unify")
}
@Test
fun `1 + 2 does not unify with 3`() {
val expr1 = Add(Integer(1), Integer(2))
val expr2 = Integer(3)
val result = unify(expr1, expr2)
assertFalse(result.isSuccess, "1 + 2 should not unify with 3")
}
}