diff --git a/documentatie/9781292153971.bib b/documentatie/9781292153971.bib deleted file mode 100644 index fa401bc..0000000 --- a/documentatie/9781292153971.bib +++ /dev/null @@ -1,11 +0,0 @@ -@book{russell2016, - author = {Russell, Stuart and Norvig, Peter}, - title = {{Artificial Intelligence A Modern Approach, Global Edition}}, - abstract = {{For one or two-semester, undergraduate or graduate-level courses in Artificial Intelligence. The long-anticipated revision of this best-selling text offers the most comprehensive, up-to-date introduction to the theory and practice of artificial intelligence. }}, - pages = {1152}, - publisher = {Pearson Deutschland}, - year = {2016}, - isbn = {9781292153964}, - doi = {}, - url = {https://elibrary.pearson.de/book/99.150005/9781292153971} -} diff --git a/documentatie/verslag.tex b/documentatie/verslag.tex index 346708d..49c1846 100644 --- a/documentatie/verslag.tex +++ b/documentatie/verslag.tex @@ -1,230 +1,17 @@ %! Author = tdpeuter %! Date = 27/03/2025 -\documentclass[11pt,a4paper]{article} +% Preamble +\documentclass[11pt]{article} +% Packages \usepackage{amsmath} -\usepackage[dutch]{babel} % Nederlands taal -\usepackage{enumitem} % Aanpasbare lijsten -\usepackage[margin=1in]{geometry} % Sane marges -\usepackage{hyperref} % Hyperlinks -\usepackage{multicol} % Meerdere kolommen - -\title{Ghent Prolog} -\author{Tibo De Peuter} -\date{\today} % Document \begin{document} - \maketitle - \section{Inleiding}\label{sec:inleiding} + % Lexer op basis van https://craftinginterpreters.com/scanning.html - % Uitvoeren van testen ref appendix - \section{Architectuur}\label{sec:architectuur} - % Overzicht van programma-loop - - \begin{enumerate} - \item Lexing and parsing - \item Preprocessor - \item Programma en Repl - \end{enumerate} - - % Parser maakt gebruik van welk Grammar??? - - % Preprocessor om parser eenvoudig te houden (eventueel later eigen implementatie - - % Interfaces: satisfiable, resolvent - - \subsection{Unificatie}\label{subsec:unificatie} - - Zoals beschreven in Artificial Intelligence a Modern Approach. Algoritme is geïnspireerd door - - \section{Implementatie}\label{sec:implementatie} - - % Kotlin, libraries - Ghent Prolog werd geschreven in Kotlin, en gebruikt verder twee bibliotheken: \href{https://github.com/h0tk3y/better-parse}{\texttt{better-parse}}, een parser combinator library voor het parsen van een gedefinieerde grammatica, en \href{}{}, voor het gebruik van command-line argumenten. - % TODO Add link - - % Data representatie: klassen, satisfiable, resolvent - - %% Evaluatie strategie - - % Overzicht van geïmplementeerde predicaten in appendix. - - % Belangrijkste delen zijn Clause.satisfy - - \section{Resultaat}\label{sec:resultaat} - - % Code wordt lelijk en overzichtelijk. Door de geneste datatypes veel boilerplate. - - \subsection{Afwijkingen van SWI-Prolog}\label{subsec:afwijkingen} - - % Occurs check - - % SLD Resolutie - In tegenstelling tot ISO Prolog en SWI-Prolog, maak ik geen gebruik van SLD-resolutie. - % TODO Bronnen voor SLD-resolutie - % TODO Bronnen voor ISO-Prolog maakt gebruik van SLD resolutie - % TODO Bronnen voor SWIPL maakt gebruik van SLD resolutie - - \section{Toekomstig werk}\label{sec:toekomstig-werk} - - % Stack gebruiken - - \section{Conclusie}\label{sec:conclusie} - - \appendix - \newpage - - \section{Aanvullende opmerkingen}\label{sec:aanvullende-opmerkingen} - - \subsection{Operator precedentie en associativiteit}\label{subsec:operator-precedence} - - Mijn implementatie ondersteunt operator precedentie en associativiteit. - Deze functionaliteit bevindt zich in de parser, omdat de argumenten van een operator steeds rechtstreeks als parameters in de constructor van de klasse worden meegegeven. - - Operator precedentie en associativiteit werd geïmplementeerd volgens de \href{https://www.swi-prolog.org/pldoc/man?section=operators}{SWI-Prolog documentatie}. - - \subsection{Test driven development}\label{subsec:ttd} - - Doorheen de ontwikkeling van grote delen van mijn implementatie heb ik gebruik gemaakt van Test Driven Development, onder andere met behulp van \href{https://kotlinlang.org/api/core/kotlin-stdlib/kotlin/-t-o-d-o.html}{Kotlin \texttt{TODO}}. - - \subsection{Onafgewerkte Lexer en Parser implementatie}\label{subsec:lexer-parser} - - Bij de start van het project was ik begonnen met het schrijven van mijn eigen lexer en parser. Uit gebruik omdat het eenvoudiger was om de parser library - % TODO reference sectie over de parser - te gebruiken. - - De implementatie was gebaseerd op \href{https://craftinginterpreters.com/contents.html}{Crafting Interpreters, Robert Nystrom} en \href{https://www.youtube.com/playlist?list=PLGNbPb3dQJ_5FTPfFIg28UxuMpu7k0eT4}{Building a Parser from scratch, Dmitry Soshnikov}. - - De voorlopige implementatie van de lexer en parser kunnen hier teruggevonden worden. - % TODO Link naar commit met voorlopige implementatie - - \section{Uitvoeren en testen}\label{sec:uitvoeren-en-testen} - - Om Ghent Prolog op een Windows, Linux of MacOS uit te voeren is het voldoende om Java te installeren en Ghent Prolog op te roepen met `./src/gpl`. De nodige stappen, waaronder het bouwen van een JAR, worden dan automatisch uitgevoerd. - - De ingediende JAR kan ook handmatig opgeroepen worden met \texttt{java -jar ./build/gpl.jar}. - - Er word ook een Docker omgeving voorzien waarin Ghent Prolog opgeroepen kan worden met \texttt{gpl}. - - Het programma ondersteunt de volgende vlaggen: - - % TODO gpl --help - - \subsection{Testen}\label{subsection:testen} - - De testen kunnen uitgevoerd worden door de meeste IDE's. - - Alternatief kunnen de testen uitgevoerd worden met \texttt{./gradlew test}. Resultaten worden naar \texttt{stdout} geschreven of kunnen bekeken worden met - % TODO HTML rapporten. - - \section{Overzicht van geïmplementeerde predicaten}\label{sec:predicaten} - - \begin{multicols}{2} - \begin{itemize}[label={}] - \item \textbf{Analysing and Constructing Terms} - \begin{itemize} - \item \texttt{functor/3} - \item \texttt{arg/3} - \item \texttt{=..} - \item \texttt{numbervars/1} - \item \texttt{numbervars/3} - \end{itemize} - \item \textbf{Arithmetic} - \begin{itemize} - \item \texttt{between/3} - \item \texttt{succ/2} - \item \texttt{plus/3} - \item \texttt{=\textbackslash=/2} - \item \texttt{=:=/2} - \item \texttt{is/2} - \item \texttt{-/1} - \item \texttt{+/1} - \item \texttt{+/2} - \item \texttt{*/2} - \item \texttt{//2} - \item \texttt{inf/0} - \end{itemize} - \item \textbf{Comparison and Unification of Terms} - \begin{itemize} - \item \texttt{=/2} - \item \texttt{\textbackslash=/2} - \item \texttt{==/2} - \item \texttt{\textbackslash==/2} - \end{itemize} - \item \textbf{Control Predicates} - \begin{itemize} - \item \texttt{fail/0} - \item \texttt{false/0} - \item \texttt{true/0} - \item \texttt{!/0} - \item \texttt{,/2} - \item \texttt{;/2} - \item \texttt{|/2} - \item \texttt{\textbackslash+/1} - \end{itemize} - \item \textbf{Database} - \begin{itemize} - \item \texttt{retract/1} - \item \texttt{retractall/1} - \item \texttt{asserta/1} - \item \texttt{assertz/1} - \item \texttt{assert/1} - \end{itemize} - \item \textbf{Declaring predicate properties} - \begin{itemize} - \item \texttt{dynamic/1} - \end{itemize} - \item \textbf{Delimited continuations} - \begin{itemize} - \item \texttt{reset/3} - \item \texttt{shift/1} - \end{itemize} - \item \textbf{Examining the program} - \begin{itemize} - \item \texttt{clause/2} - \end{itemize} - \item \textbf{Forall} - \begin{itemize} - \item \texttt{forall/2} - \end{itemize} - \item \textbf{Loading Prolog source files} - \begin{itemize} - \item \texttt{consult/1} - \item \texttt{initialization/1} - \end{itemize} - \item \textbf{Meta-Call Predicates} - \begin{itemize} - \item \texttt{call/1} - \item \texttt{once/1} - \item \texttt{ignore/1} - \end{itemize} - \item \textbf{Primitive character I/O} - \begin{itemize} - \item \texttt{nl/0} - \end{itemize} - \item \textbf{Term reading and writing} - \begin{itemize} - \item \texttt{write/1} - \item \texttt{writeln/1} - \item \texttt{read/1} - \end{itemize} - \item \textbf{Verify Type of a Term} - \begin{itemize} - \item \texttt{var/1} - \item \texttt{nonvar/1} - \item \texttt{atom/1} - \item \texttt{compound/1} - \end{itemize} - \end{itemize} - \end{multicols} - - \section{Dankwoord}\label{sec:dankwoord} - - Bedankt aan LogicalCaptain om steeds nuttige informatie en voorbeelden te geven bij SWI-Prolog documentatie die iets minder duidelijk is. Uw nota's waren verhelderend en zorgden voor een beter begrip van en voor de nuances van SWI-Prolog. - -\end{document} +\end{document} \ No newline at end of file diff --git a/examples/basics/backtracking.pl b/examples/basics/backtracking.pl index 820bd4f..167f037 100644 --- a/examples/basics/backtracking.pl +++ b/examples/basics/backtracking.pl @@ -4,6 +4,6 @@ leq(s(X), s(Y)) :- leq(X, Y). :- initialization(main). main :- - leq(A, s(s(s(0)))), - write(A), nl, + leq(X, s(s(s(0)))), + write(X), nl, fail. diff --git a/examples/meta/continuations.pl b/examples/meta/continuations.pl deleted file mode 100644 index 8661361..0000000 --- a/examples/meta/continuations.pl +++ /dev/null @@ -1,22 +0,0 @@ -% Based on -% https://occasionallycogent.com/continuations_in_prolog/ - -test(Cont, Term) :- - writeln("Inside test"), - reset(test_, Term, Cont), - writeln("After reset"). - -test_ :- - writeln("Entering reset"), - shift(Y), - X is 1 + (2 * Y), - write("In test X = "), write(X), writeln("; done"). - -main :- - test(Cont, Term), - \+ \+ ( writeln("Calling Cont(2)"), - Term = 2, call(Cont)), - \+ \+ ( writeln("Calling Cont(4)"), - Term = 4, call(Cont)). - -:- initialization(main). diff --git a/examples/meta/mib_voorbeelden.pl b/examples/meta/mib_voorbeelden.pl deleted file mode 100644 index 47003d5..0000000 --- a/examples/meta/mib_voorbeelden.pl +++ /dev/null @@ -1,48 +0,0 @@ -% Old mag steeds door New vervangen worden -mib(Old, New, Old, New). - -% Een term blijft enkel behouden als het een attoom is -% (dat is, niet compound), en als het niet Old is -mib(Old, _, Term, Term) :- - atomic(Term), - Term \= Old. - -% Voor een samengestelde Term -mib(Old, New, Pre, Post) :- - compound(Pre), - functor(Pre, F, N), % Pre heeft naam F en arriteit N - functor(Post, F, N), % Post is term met zelfde naam (F) en arriteit (N) - mib(N, Old, New, Pre, Post). - -% Extra predicaat om de argumenten te vervangen van een samengestelde term -% -% N = het nr van het argument (strikt positief) -mib(0, _, _, _, _) :- !. % Argument 0 bestaat niet, als we hier komen zijn we klaar. - -mib(N, Old, New, Pre, Post) :- - arg(N, Pre, ArgPre), % neem het N-de argument - mib(Old, New, ArgPre, ArgPost), % vertaal het - arg(N, Post, ArgPost), % unificeer het met het N-de argument van output - N1 is N-1, - mib(N1, Old, New, Pre, Post). % Herhaal voor argument N-1 - -example1 :- - mib(a, b, a, Result), - write(Result), nl. -example2 :- - mib(a, b, f(a), Result), - write(Result), nl. -example3 :- - mib(b, a, f(g(a, b), h(c, d), i(e, f)), Result), - write(Result), nl, - mib(d, c, Result, Result2), - write(Result2), nl, - mib(f, e, Result2, Result3), - write(Result3), nl. - -main :- - example1, - example2, - example3. - -:- initialization(main). diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index fb72dcf..6c17705 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -48,99 +48,67 @@ open class Preprocessor { } protected open fun preprocess(term: Term, nested: Boolean = false): Term { - // TODO Remove hardcoding by storing the functors as constants in operators? - 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 Atom, is Structure -> { + is Structure -> { // Preprocess the arguments first to recognize builtins - val args = if (term is Structure) { - term.arguments.map { preprocess(it, nested = true) } - } else emptyList() + val args = term.arguments.map { preprocess(it, nested = true) } - when (term.functor) { - // Analysis - Functor.of("functor/3") -> FunctorOp(args[0], args[1], args[2]) - Functor.of("arg/3") -> Arg(args[0], args[1], args[2]) - Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body) - Functor.of("=../2") -> Univ(args[0], args[1]) - Functor.of("numbervars/1") -> NumberVars(args[0]) - Functor.of("numbervars/3") -> NumberVars(args[0], args[1] as Integer, args[2]) + 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 - Functor.of("inf/0") -> Integer(Int.MAX_VALUE) - Functor.of("=\\=/2") -> if (args.all { it is Expression }) { - EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) - } else term - Functor.of("=:=/2") -> if (args.all { it is Expression }) { - EvaluatesTo(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("is/2") -> if (args.all { it is Expression }) { - Is(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("-/1") -> if (args.all { it is Expression }) Negate(args[0] as Expression) else term - Functor.of("+/1") -> if (args.all { it is Expression }) Positive(args[0] as Expression) else term - Functor.of("+/2") -> if (args.all { it is Expression }) { - Add(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("-/2") -> if (args.all { it is Expression }) { - Subtract(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("*/2") -> if (args.all { it is Expression }) { - Multiply(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("//2") -> if (args.all { it is Expression }) { - Divide(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("between/3") -> if (args.all { it is Expression }) { - Between(args[0] as Expression, args[1] as Expression, args[2] as Expression) - } else term - - Functor.of("succ/2") -> if (args.all { it is Expression }) { - Successor(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("plus/3") -> if (args.all { it is Expression }) { - Plus(args[0] as Expression, args[1] as Expression, args[2] as Expression) - } else term - - // Control - Functor.of("fail/0") -> Fail - Functor.of("false/0") -> False - Functor.of("true/0") -> True - Functor.of("!/0") -> Cut() - Functor.of(",/2") -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand) - Functor.of(";/2") -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand) - Functor.of("\\+/1") -> Not(args[0] as Goal) + 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 - Functor.of("dynamic/1") -> Dynamic(Functor.of((args[0] as Atom).name)) - Functor.of("retract/1") -> Retract(args[0]) - Functor.of("retractall/1") -> RetractAll(args[0]) - Functor.of("assert/1") -> { + 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)) } } - - Functor.of("asserta/1") -> { + term.functor == "asserta/1" -> { if (args[0] is Rule) { AssertA(args[0] as Rule) } else { AssertA(Fact(args[0] as Head)) } } - - Functor.of("assertz/1") -> { + term.functor == "assertz/1" -> { if (args[0] is Rule) { AssertZ(args[0] as Rule) } else { @@ -148,48 +116,13 @@ open class Preprocessor { } } - // Delimited Continuations - Functor.of("reset/3") -> Reset(args[0] as Goal, args[1], args[2]) - Functor.of("shift/1") -> Shift(args[0]) - - // IO - Functor.of("write/1") -> Write(args[0]) - Functor.of("nl/0") -> Nl - Functor.of("writeln/1") -> WriteLn(args[0]) - Functor.of("read/1") -> Read(args[0]) - - // Lists - Functor.of("member/2") -> Member(args[0], args[1]) - Functor.of("append/3") -> Append(args[0], args[1], args[2]) - - // Loading - Functor.of("consult/1") -> Consult(args[0]) - Functor.of("initialization/1") -> Initialization(args[0] as Goal) - - // Meta - Functor.of("call/1") -> Call(args[0]) - Functor.of("once/1") -> Once(args[0] as Goal) - Functor.of("ignore/1") -> Ignore(args[0] as Goal) - // Other - Functor.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal) - - // Unification - Functor.of("=/2") -> Unify(args[0], args[1]) - Functor.of("\\=/2") -> NotUnify(args[0], args[1]) - Functor.of("==/2") -> Equivalent(args[0], args[1]) - Functor.of("\\==/2") -> NotEquivalent(args[0], args[1]) - - // Verification - Functor.of("atomic/1") -> Atomic(args[0]) - Functor.of("compound/1") -> Compound(args[0]) - Functor.of("nonvar/1") -> NonVar(args[0]) - Functor.of("var/1") -> Var(args[0]) - - Functor.of(":-/2") -> Rule(args[0] as Head, args[1] as Body) + term.functor == "write/1" -> Write(args[0]) + term.functor == "read/1" -> Read(args[0]) + term.functor == "initialization/1" -> Initialization(args[0] as Goal) else -> { - if (term is Structure) term.arguments = args + term.arguments = args term } } @@ -205,4 +138,4 @@ open class Preprocessor { return prepped } -} +} \ No newline at end of file diff --git a/src/io/IoHandler.kt b/src/io/IoHandler.kt index f12deb7..c5706a1 100644 --- a/src/io/IoHandler.kt +++ b/src/io/IoHandler.kt @@ -3,8 +3,7 @@ package io interface IoHandler { fun prompt( message: String, - hint: () -> String = { "Please enter a valid input." }, - check: (String) -> Boolean = { true } + hint: () -> String = { "Please enter a valid input." } ): String fun say(message: String) diff --git a/src/io/Terminal.kt b/src/io/Terminal.kt index d20c8e8..1b9df94 100644 --- a/src/io/Terminal.kt +++ b/src/io/Terminal.kt @@ -20,16 +20,15 @@ class Terminal( override fun prompt( message: String, - hint: () -> String, - check: (String) -> Boolean, + hint: () -> String ): String { say("$message ") - var input: String = readLine().trim() - while (!check(input)) { + var input: String = readLine() + while (input.isBlank()) { say(hint(), error) - input += readLine().trim() + input = readLine() } - return input.trim() + return input } override fun say(message: String) { diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 9051484..3fb9e48 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -3,14 +3,10 @@ package parser.grammars import com.github.h0tk3y.betterParse.combinators.* import com.github.h0tk3y.betterParse.grammar.parser import com.github.h0tk3y.betterParse.parser.Parser -import com.github.h0tk3y.betterParse.utils.Tuple2 import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List as PList import prolog.ast.terms.* import prolog.builtins.Dynamic -import prolog.ast.lists.List.Empty -import prolog.ast.lists.List.Cons /** * Precedence is based on the following table: @@ -69,7 +65,6 @@ open class TermsGrammar : Tokens() { // Base terms (atoms, compounds, variables, numbers) protected val baseTerm: Parser by (dummy or (-leftParenthesis * parser(::term) * -rightParenthesis) - or parser(::list) or compound or atom or variable @@ -92,24 +87,19 @@ open class TermsGrammar : Tokens() { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } - protected val op700: Parser by (univOp or equivalent or notEquivalent or equals or notEquals or isOp) use { text } + protected val op700: Parser by (equivalent or equals or notEquals or isOp) use { text } protected val term700: Parser by (term500 * optional(op700 * term500)) use { if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2)) } - protected val not: Parser by (notOp * parser(::term900)) use { - CompoundTerm(Atom(t1.text), listOf(t2)) - } - protected val term900: Parser by (not or term700) - protected val op1000: Parser by (comma) use { text } - protected val term1000: Parser by (term900 * zeroOrMore(op1000 * term900)) use { - constructRightAssociative(t1, t2) + protected val term1000: Parser by (term700 * zeroOrMore(op1000 * term700)) use { + t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } protected val op1100: Parser by (semicolon) use { text } protected val term1100: Parser by (term1000 * zeroOrMore(op1100 * term1000)) use { - constructRightAssociative(t1, t2) + t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } protected val dynamic: Parser by (dynamicOp * functor) use { @@ -122,20 +112,6 @@ open class TermsGrammar : Tokens() { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } - // Lists - protected val list: Parser by (-leftBracket * separated( - parser(::termNoConjunction), - comma, - acceptZero = true - ) * -rightBracket) use { - var list: PList = Empty - // Construct the list in reverse order - for (term in this.terms.reversed()) { - list = Cons(term, list) - } - list - } - // Term - highest level expression protected val term: Parser by term1200 protected val termNoConjunction: Parser by term700 @@ -145,12 +121,4 @@ open class TermsGrammar : Tokens() { protected val body: Parser by term use { this as Body } override val rootParser: Parser by term - - fun constructRightAssociative(left: Term, pairs: List>): Term { - if (pairs.isEmpty()) return left - - val (name, next) = pairs.first() - val remainingPairs = pairs.drop(1) - return CompoundTerm(Atom(name), listOf(left, constructRightAssociative(next, remainingPairs))) - } } diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index ccdbae9..ac8c36f 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -10,8 +10,6 @@ import com.github.h0tk3y.betterParse.lexer.token abstract class Tokens : Grammar() { protected val leftParenthesis: Token by literalToken("(") protected val rightParenthesis: Token by literalToken(")") - protected val leftBracket: Token by literalToken("[") - protected val rightBracket: Token by literalToken("]") protected val exclamation: Token by literalToken("!") // 1200 protected val neck by literalToken(":-") @@ -21,11 +19,7 @@ abstract class Tokens : Grammar() { protected val semicolon: Token by literalToken(";") // 1000 protected val comma: Token by literalToken(",") - // 900 - protected val notOp: Token by literalToken("\\+") // 700 - protected val univOp: Token by literalToken("=..") - protected val notEquivalent: Token by literalToken("\\==") protected val equivalent: Token by literalToken("==") protected val equals: Token by literalToken("=") protected val isOp: Token by literalToken("is") diff --git a/src/prolog/ast/Database.kt b/src/prolog/ast/Database.kt index b309883..be2da7a 100644 --- a/src/prolog/ast/Database.kt +++ b/src/prolog/ast/Database.kt @@ -23,14 +23,14 @@ open class Database(val sourceFile: String) { if (sourceFile !== "") { Logger.debug("Moving clauses from $sourceFile to main database") - predicates.filter { it.key != Functor.of("/_") } + predicates.filter { it.key != "/_" } .forEach { (_, predicate) -> db.load(predicate, force = true) } } Logger.info("Initializing database from $sourceFile") - if (predicates.contains(Functor.of("/_"))) { + if (predicates.contains("/_")) { Logger.debug("Loading clauses from /_ predicate") - predicates[Functor.of("/_")]?.clauses?.forEach { + predicates["/_"]?.clauses?.forEach { Logger.debug("Loading clause $it") val goal = it.body as Goal goal.satisfy(emptyMap()).toList() diff --git a/src/prolog/ast/arithmetic/ArithmeticOperator.kt b/src/prolog/ast/arithmetic/ArithmeticOperator.kt index d87c6e8..61550a9 100644 --- a/src/prolog/ast/arithmetic/ArithmeticOperator.kt +++ b/src/prolog/ast/arithmetic/ArithmeticOperator.kt @@ -4,7 +4,4 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Operator abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) : - Operator(symbol, leftOperand, rightOperand), Expression { - constructor(symbol: String, leftOperand: Expression, rightOperand: Expression) : - this(Atom(symbol), leftOperand, rightOperand) -} + Operator(symbol, leftOperand, rightOperand), Expression diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt index a787cb2..80d0bde 100644 --- a/src/prolog/ast/arithmetic/Float.kt +++ b/src/prolog/ast/arithmetic/Float.kt @@ -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 @@ -32,8 +33,6 @@ class Float(override val value: kotlin.Float): Number { else -> throw IllegalArgumentException("Cannot multiply $this and $other") } - override fun applySubstitution(subs: Substitutions): Float = this - override fun equals(other: Any?): Boolean { if (this === other) return true if (other !is Float) return false @@ -44,4 +43,7 @@ class Float(override val value: kotlin.Float): Number { override fun hashCode(): Int { return super.hashCode() } + + override fun clone(): Float = Float(value) + override fun applySubstitution(subs: Substitutions): Float = this } \ No newline at end of file diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt index c12cfcd..d0a48cb 100644 --- a/src/prolog/ast/arithmetic/Integer.kt +++ b/src/prolog/ast/arithmetic/Integer.kt @@ -3,6 +3,7 @@ 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, LogicOperand() { // Integers are already evaluated @@ -33,7 +34,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() { Float(value / other.value.toFloat()) } } - else -> throw IllegalArgumentException("Cannot divide $this and $other") } @@ -43,5 +43,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() { else -> throw IllegalArgumentException("Cannot multiply $this and $other") } + override fun clone(): Integer = Integer(value) override fun applySubstitution(subs: Substitutions): Integer = this } diff --git a/src/prolog/ast/lists/List.kt b/src/prolog/ast/lists/List.kt deleted file mode 100644 index cd5ee80..0000000 --- a/src/prolog/ast/lists/List.kt +++ /dev/null @@ -1,65 +0,0 @@ -package prolog.ast.lists - -import prolog.Substitutions -import prolog.ast.terms.Term -import prolog.ast.arithmetic.Integer - -sealed class List : Term { - abstract val head: Term - open val tail: Term? = null - - operator fun component1(): Term = head - operator fun component2(): Term? = tail - - val size: Integer - get() = when (this) { - is Empty -> Integer(0) - is Cons -> { - val tailSize = if (tail is List) { (tail as List).size.value } else 0 - Integer(1 + tailSize) - } - } - - fun isEmpty(): Boolean = this is Empty - - /** - * The empty list [] - */ - object Empty : List() { - override val head = this - override fun applySubstitution(subs: Substitutions): Empty = this - override fun toString(): String = "[]" - } - - class Cons(override val head: Term, override var tail: Term) : List() { - override fun applySubstitution(subs: Substitutions): List { - val newHead = head.applySubstitution(subs) - val newTail = tail.applySubstitution(subs) as List - return Cons(newHead, newTail) - } - - override fun toString(): String { - val values = mutableListOf() - var current: Term? = this - while (current != null && current is Cons) { - values.add(current.head) - current = current.tail - } - if (current != null && current !is Empty) values.add(current) - return "[${values.joinToString(", ")}]" - } - } - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (other == null) return false - if (other !is List) return false - if (this is Empty && other is Empty) return true - if (this is Cons && other is Cons) { - return this.head == other.head && this.tail == other.tail - } - return false - } - - override fun hashCode(): Int = super.hashCode() -} diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index dc1c0c4..d511641 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -1,8 +1,8 @@ package prolog.ast.logic import prolog.Answers -import prolog.Substitutions import prolog.ast.Database.Program +import prolog.Substitutions import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut @@ -27,38 +27,28 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { // Only if the body can be proven, the substitutions should be returned. // Do this in a lazy way. - // Since we are only interested in substitutions in the goal (as opposed to the head of this clause), - // we can use variable renaming and filter out the substitutions that are not in the goal. - val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, emptyMap()) + val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs) Program.variableRenamingStart = headEnd val renamedHead = applySubstitution(head, headRenaming) - val simplifiedGoal = applySubstitution(goal, subs) - unifyLazy(simplifiedGoal, renamedHead, emptyMap()).forEach { headAnswer -> - headAnswer.map { headAndGoalSubs -> - // Filter the substitutions to only include those that map from head to goal - val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values } - val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) } - val headResult = headToGoalSubs.filterKeys { key -> - goalToHeadSubs.any { occurs(key as Variable, it.value) } - } - val newSubs = headRenaming + headToGoalSubs - body.satisfy(newSubs).forEach { bodyAnswer -> + unifyLazy(goal, renamedHead, subs).forEach { headAnswer -> + headAnswer.map { headSubs -> + // If the body can be proven, yield the (combined) substitutions + val preBody = applySubstitution(body, headRenaming + headSubs) as Body + preBody.satisfy(subs).forEach { bodyAnswer -> bodyAnswer.fold( onSuccess = { bodySubs -> - // If the body can be proven, yield the (combined) substitutions - val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } - val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) } - yield(Result.success(goalResult + headResult + bodyResult)) + val newSubs = headSubs + bodySubs + val result = newSubs + .mapValues { applySubstitution(it.value, newSubs) } + .filter { it.key !is AnonymousVariable && 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) { - val bodySubs = error.subs - val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } - val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) } - yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult))) + yield(Result.failure(AppliedCut(headSubs + error.subs))) } else { yield(Result.failure(AppliedCut())) } @@ -85,5 +75,7 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { return true } - override fun hashCode(): Int = super.hashCode() + override fun hashCode(): Int { + return super.hashCode() + } } diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt index b6cc83d..f0cae19 100644 --- a/src/prolog/ast/logic/Fact.kt +++ b/src/prolog/ast/logic/Fact.kt @@ -2,9 +2,11 @@ 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) { - override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head) -} + override fun clone(): Fact = Fact(head) + override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head as Term, subs) as Head) +} \ No newline at end of file diff --git a/src/prolog/ast/logic/LogicOperator.kt b/src/prolog/ast/logic/LogicOperator.kt index 8fb488f..5353f0d 100644 --- a/src/prolog/ast/logic/LogicOperator.kt +++ b/src/prolog/ast/logic/LogicOperator.kt @@ -10,8 +10,5 @@ abstract class LogicOperator( leftOperand: LogicOperand? = null, rightOperand: LogicOperand ) : Operator(symbol, leftOperand, rightOperand), Satisfiable { - constructor(symbol: String, leftOperand: LogicOperand? = null, rightOperand: LogicOperand) : - this(Atom(symbol), leftOperand, rightOperand) - abstract override fun satisfy(subs: Substitutions): Answers } diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt index 26148a3..add106d 100644 --- a/src/prolog/ast/logic/Rule.kt +++ b/src/prolog/ast/logic/Rule.kt @@ -3,11 +3,13 @@ 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) { + override fun clone(): Rule = Rule(head, body) override fun applySubstitution(subs: Substitutions): Rule = Rule( - head = applySubstitution(head, subs) as Head, + head = applySubstitution(head as Term, subs) as Head, body = applySubstitution(body, subs) as Body ) } diff --git a/src/prolog/ast/terms/AnonymousVariable.kt b/src/prolog/ast/terms/AnonymousVariable.kt index abb751c..8211292 100644 --- a/src/prolog/ast/terms/AnonymousVariable.kt +++ b/src/prolog/ast/terms/AnonymousVariable.kt @@ -14,7 +14,8 @@ class AnonymousVariable(private val id: Int) : Variable("_$id") { } } - override fun applySubstitution(subs: Substitutions): AnonymousVariable = this - override fun toString(): String = "_" + + override fun clone(): AnonymousVariable = AnonymousVariable(id) + override fun applySubstitution(subs: Substitutions): AnonymousVariable = this } \ No newline at end of file diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index 42c12c5..dcd0a7d 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -4,15 +4,12 @@ import prolog.Answers import prolog.Substitutions import prolog.ast.logic.Resolvent import prolog.logic.unifyLazy -import prolog.ast.arithmetic.Integer open class Atom(val name: String) : Goal(), Head, Body, Resolvent { - override val functor: Functor = Functor(this, Integer(0)) + override val functor: Functor = "$name/_" override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs) - override fun applySubstitution(subs: Substitutions): Atom = this - override fun toString(): String { return name } @@ -24,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) } \ No newline at end of file diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index 989c4d9..4918d1e 100644 --- a/src/prolog/ast/terms/Body.kt +++ b/src/prolog/ast/terms/Body.kt @@ -2,4 +2,4 @@ package prolog.ast.terms import prolog.ast.logic.Satisfiable -interface Body : Term, Satisfiable +interface Body : Term, Satisfiable \ No newline at end of file diff --git a/src/prolog/ast/terms/Functor.kt b/src/prolog/ast/terms/Functor.kt deleted file mode 100644 index b7a4cc3..0000000 --- a/src/prolog/ast/terms/Functor.kt +++ /dev/null @@ -1,37 +0,0 @@ -package prolog.ast.terms - -import prolog.Substitutions -import prolog.ast.arithmetic.Integer - -data class Functor(val name: Atom, val arity: Integer) : Term { - constructor(name: String, arity: Int) : this(Atom(name), Integer(arity)) - - companion object { - fun of(functor: String): Functor { - // Split the functor string into name and arity, by splitting the last "/" - val lastSlash = functor.lastIndexOf('/') - val name = Atom(functor.substring(0, lastSlash)) - val arity = Integer(functor.substring(lastSlash + 1).toIntOrNull() ?: 0) - return Functor(name, arity) - } - } - - override fun toString(): String = "${name.name}/$arity" - override fun applySubstitution(subs: Substitutions) : Functor = this - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (other == null) return false - if (other !is Functor && other !is String) return false - if (other is Functor) { - return this.name.toString() == other.name.toString() && this.arity == other.arity - } - return this.toString() == other - } - - override fun hashCode(): Int { - var result = name.hashCode() - result = 31 * result + arity.hashCode() - return result - } -} diff --git a/src/prolog/ast/terms/Goal.kt b/src/prolog/ast/terms/Goal.kt index 4f98585..95f9016 100644 --- a/src/prolog/ast/terms/Goal.kt +++ b/src/prolog/ast/terms/Goal.kt @@ -1,8 +1,8 @@ package prolog.ast.terms import prolog.Answers -import prolog.Substitutions import prolog.ast.Database.Program +import prolog.Substitutions import prolog.ast.logic.LogicOperand /** diff --git a/src/prolog/ast/terms/Head.kt b/src/prolog/ast/terms/Head.kt index fe5048d..71b4e8a 100644 --- a/src/prolog/ast/terms/Head.kt +++ b/src/prolog/ast/terms/Head.kt @@ -6,3 +6,5 @@ package prolog.ast.terms interface Head : Term { val functor: Functor } + +typealias Functor = String diff --git a/src/prolog/ast/terms/Operator.kt b/src/prolog/ast/terms/Operator.kt index 136c423..cf43b24 100644 --- a/src/prolog/ast/terms/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -7,9 +7,6 @@ abstract class Operator( private val leftOperand: Operand? = null, private val rightOperand: Operand ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Term { - constructor(symbol: String, leftOperand: Operand? = null, rightOperand: Operand) : - this(Atom(symbol), leftOperand, rightOperand) - override fun toString(): String { return when (leftOperand) { null -> "${symbol.name} $rightOperand" diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index 162dc61..bcd5e71 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -5,16 +5,13 @@ import prolog.Substitutions import prolog.ast.logic.Resolvent import prolog.logic.applySubstitution import prolog.logic.unifyLazy -import prolog.ast.arithmetic.Integer typealias Argument = Term typealias CompoundTerm = Structure open class Structure(val name: Atom, var arguments: List) : Goal(), Head, Body, Resolvent { - constructor(name: String, vararg arguments: Argument) : this(Atom(name), arguments.asList()) - - override val functor: Functor = Functor(name, Integer(arguments.size)) + override val functor: Functor = "${name.name}/${arguments.size}" override fun solve(goal: Goal, subs: Substitutions): Answers { return unifyLazy(goal, this, subs) @@ -23,15 +20,10 @@ open class Structure(val name: Atom, var arguments: List) : Goal(), He override fun toString(): String { return when { arguments.isEmpty() -> name.name - else -> "${name.name}(${arguments.joinToString(",")})" + else -> "${name.name}(${arguments.joinToString(", ")})" } } - override fun applySubstitution(subs: Substitutions): Structure = Structure( - name, - arguments.map { applySubstitution(it, subs) } - ) - override fun equals(other: Any?): Boolean { if (this === other) return true if (other !is Structure) return false @@ -42,4 +34,10 @@ open class Structure(val name: Atom, var arguments: List) : Goal(), He 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) } + ) } diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 8e46626..7720457 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -1,9 +1,9 @@ package prolog.ast.terms import prolog.Substitutions -import prolog.ast.arithmetic.Float -import prolog.ast.arithmetic.Integer import prolog.logic.compare +import prolog.ast.arithmetic.Integer +import prolog.ast.arithmetic.Float /** * Value in Prolog. @@ -12,7 +12,7 @@ import prolog.logic.compare * [Float] or [CompoundTerm]. * In addition, SWI-Prolog also defines the type TODO string. */ -interface Term : Comparable { +interface Term : Comparable, Cloneable { override fun compareTo(other: Term): Int = compare(this, other, emptyMap()) fun applySubstitution(subs: Substitutions): Term } diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index bcfee5c..8068864 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -34,11 +34,12 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() { return name == other.name } - override fun applySubstitution(subs: Substitutions): Variable = this - 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 } \ No newline at end of file diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt deleted file mode 100644 index 7f83ab0..0000000 --- a/src/prolog/builtins/analysisOperators.kt +++ /dev/null @@ -1,250 +0,0 @@ -package prolog.builtins - -import com.sun.tools.javac.resources.CompilerProperties.Fragments.Anonymous -import prolog.Answers -import prolog.Substitutions -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.terms.* -import prolog.ast.logic.Clause -import prolog.logic.* -import prolog.ast.lists.List -import prolog.ast.lists.List.Empty -import prolog.ast.lists.List.Cons - -/** - * [True] when [Term] is a term with [Functor] Name/Arity. - * - * If Term is a [Variable] it is unified with a new term whose arguments are all different variables. - * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term. - * - * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3) - */ -class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) : - Structure("functor", term, functorName, functorArity) { - override fun satisfy(subs: Substitutions): Answers { - return when { - nonvariable(term, subs) -> { - val t = applySubstitution(term, subs) as Head - - Conjunction( - Unify(t.functor.arity, functorArity), - Unify(t.functor.name, functorName) - ).satisfy(subs) - } - - variable(term, subs) -> { - require(atomic(functorName, subs) && atomic(functorArity, subs)) { - "Arguments are not sufficiently instantiated" - } - - val t = applySubstitution(term, subs) - val name = applySubstitution(functorName, subs) as Atom - val arity = applySubstitution(functorArity, subs) as Integer - val result = Structure(name, List(arity.value) { AnonymousVariable.create() }) - sequenceOf(Result.success(mapOf(t to result))) - } - - else -> throw IllegalStateException() - } - } - - override fun applySubstitution(subs: Substitutions): FunctorOp = FunctorOp( - term.applySubstitution(subs), - functorName.applySubstitution(subs), - functorArity.applySubstitution(subs) - ) -} - -class Arg(private val arg: Term, private val term: Term, private val value: Term) : - Structure("arg", arg, term, value) { - override fun satisfy(subs: Substitutions): Answers = sequence { - require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" } - require(compound(term, subs)) { - val expected = CompoundTerm::class.simpleName?.lowercase() - val actual = term::class.simpleName?.lowercase() - "Type error: `$expected' expected, found `$term' ($actual)" - } - - val t = applySubstitution(term, subs) as Structure - - when { - variable(arg, subs) -> { - // Value will be unified with the successive arguments of term. - // On successful unification, arg is unified with the argument number. - // Backtracking yields alternative solutions. - for ((count, argument) in t.arguments.withIndex()) { - unifyLazy(value, argument, subs).forEach { result -> - result.map { - val sub = arg to Integer(count + 1) - yield(Result.success(it + sub)) - } - } - } - - } - - else -> { - val a = applySubstitution(arg, subs) as Integer - - require(0 <= a.value) { "Domain error: not_less_than_zero" } - - // Fail silently if the argument is out of bounds - if (0 == a.value || t.arguments.size < a.value) { - return@sequence - } - - val argument = t.arguments[a.value - 1] - yieldAll(unifyLazy(argument, value, subs)) - } - } - } - - override fun applySubstitution(subs: Substitutions): Arg = Arg( - arg.applySubstitution(subs), - term.applySubstitution(subs), - value.applySubstitution(subs) - ) -} - -/** - * [True] if [Head] can be unified with a [Clause] and [Body] with the corresponding Clause Body. - * - * Gives alternative clauses on backtracking. For facts, Body is unified with the atom [True]. - * - * When accessing builtins (static predicates, private procedures), the program will act as if the builtins do not - * exist. Head can only match with dynamic or imported predicates. - * - * [SWI-Prolog Operator clause/2](https://www.swi-prolog.org/pldoc/doc_for?object=clause/2) - */ -class ClauseOp(private val head: Head, private val body: Body) : - Structure("clause", head, body) { - override fun satisfy(subs: Substitutions): Answers = sequence { - require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" } - - val predicate = Program.db.predicates[head.functor] - - if (predicate != null) { - for (clause in predicate.clauses) { - val clauseHead = clause.head - val clauseBody = clause.body - - val appliedHead = applySubstitution(head, subs) - val appliedBody = applySubstitution(body, subs) - - // Unify the head of the clause with the head of the goal - unifyLazy(clauseHead, appliedHead, subs).forEach { result -> - result.map { headSubs -> - // Unify the body of the clause with the body of the goal - unifyLazy(clauseBody, appliedBody, headSubs).forEach { bodyResult -> - bodyResult.map { bodySubs -> - // Combine the substitutions from the head and body - val combinedSubs = headSubs + bodySubs - yield(Result.success(combinedSubs)) - } - } - } - } - } - } else { - yield(Result.success(emptyMap())) - } - } - - override fun applySubstitution(subs: Substitutions): ClauseOp = ClauseOp( - head.applySubstitution(subs) as Head, - body.applySubstitution(subs) as Body - ) -} - -open class Univ(private val term: Term, private val list: Term) : Operator("=..", term, list) { - override fun satisfy(subs: Substitutions): Answers { - return when { - nonvariable(term, subs) && nonvariable(list, subs) -> { - val t = applySubstitution(term, subs) - val l = applySubstitution(list, subs) as List - unifyLazy(t, listToTerm(l), subs) - } - - variable(term, subs) && nonvariable(list, subs) -> { - val l = applySubstitution(list, subs) as List - val t = listToTerm(l) - unifyLazy(term, t, subs) - } - - nonvariable(term, subs) && variable(list, subs) -> { - val t = applySubstitution(term, subs) - val l = termToList(t) - unifyLazy(l, list, subs) - } - - else -> throw Exception("Arguments are not sufficiently instantiated") - } - } - - protected open fun listToTerm(list: List): Term { - return when { - list.size.value == 1 -> list.head - - list.size.value > 1 -> { - val head = list.head - val arguments = mutableListOf() - var tail: Term? = list.tail - while (tail != null && tail is Cons) { - arguments.add(tail.head) - tail = tail.tail - } - if (tail != null && tail !is Empty) { - arguments.add(tail) - } - Structure(head as Atom, arguments) - } - - else -> throw IllegalStateException("List is empty") - } - } - - protected open fun termToList(term: Term): List { - return when (term) { - is Atom -> Cons(term, Empty) - - is Structure -> { - val head = term.functor.name - val arguments = term.arguments - // Construct the list by iterating over the arguments in reverse - var tail: List = Empty - for (i in arguments.size - 1 downTo 0) { - tail = Cons(arguments[i], tail) - } - return Cons(head, tail) - } - - else -> throw IllegalStateException("Term is not a valid structure") - } - } - - override fun applySubstitution(subs: Substitutions): Univ = Univ( - term.applySubstitution(subs), - list.applySubstitution(subs) - ) -} - -class NumberVars(private val term: Term, private val start: Integer, private val end: Term) : - Structure("numbervars", term, start, end) { - private var yieldEnd: Boolean = true - - constructor(term: Term) : this(term, Integer(0), AnonymousVariable.create()) { - yieldEnd = false - } - - override fun satisfy(subs: Substitutions): Answers = sequence { - val (newEnd, newSubs) = numbervars(term, start.value, subs) - unifyLazy(end, Integer(newEnd), subs).forEach { endResult -> - endResult.map { endSubs -> - val result = if (yieldEnd) (newSubs + endSubs) else newSubs - yield(Result.success(result)) - } - - } - } -} diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt index dbdccf4..5ce34b3 100644 --- a/src/prolog/builtins/arithmeticOperators.kt +++ b/src/prolog/builtins/arithmeticOperators.kt @@ -22,7 +22,7 @@ import prolog.logic.* * True if expression Expr1 evaluates to a number non-equal to Expr2. */ class EvaluatesToDifferent(private val left: Expression, private val right: Expression) : - Operator("=\\=", left, right), Satisfiable { + Operator(Atom("=\\="), left, right), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -49,7 +49,7 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr * True if Expr1 evaluates to a number equal to Expr2. */ class EvaluatesTo(private val left: Expression, private val right: Expression) : - Operator("=:=", left, right) { + Operator(Atom("=:="), left, right) { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -72,7 +72,7 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) : * True when Number is the value to which Expr evaluates. */ class Is(val number: Expression, val expr: Expression) : - Operator("is", number, expr), Satisfiable { + Operator(Atom("is"), number, expr), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = number.simplify(subs) val t2 = expr.simplify(subs) @@ -108,7 +108,7 @@ class Positive(operand: Expression) : Add(Integer(0), operand) * Result = Expr1 + Expr2 */ open class Add(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("+", expr1, expr2) { + ArithmeticOperator(Atom("+"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr1, expr2, result, subs) @@ -122,16 +122,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) : ) } -class Plus(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) : - CompoundTerm("plus", expr1, expr2, expr3) { - override fun satisfy(subs: Substitutions): Answers = plus(expr1, expr2, expr3, subs) -} - /** * Result = Expr1 - Expr2 */ open class Subtract(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("-", expr1, expr2) { + ArithmeticOperator(Atom("-"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr2, result, expr1, subs) @@ -149,7 +144,7 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression * Result = Expr1 * Expr2 */ class Multiply(val expr1: Expression, val expr2: Expression) : - ArithmeticOperator("*", expr1, expr2) { + ArithmeticOperator(Atom("*"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = mul(expr1, expr2, result, subs) @@ -164,7 +159,7 @@ class Multiply(val expr1: Expression, val expr2: Expression) : } class Divide(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("/", expr1, expr2) { + ArithmeticOperator(Atom("/"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = div(expr1, expr2, result, subs) @@ -183,7 +178,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) : - CompoundTerm("between", expr1, expr2, expr3), Satisfiable { + CompoundTerm(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val e1 = expr1.simplify(subs) val e2 = expr2.simplify(subs) @@ -213,8 +208,3 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv override fun toString(): String = "$expr1..$expr3..$expr2" } - -class Successor(private val expr1: Expression, private val expr2: Expression) : - CompoundTerm("succ", expr1, expr2), Satisfiable { - override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs) -} diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 3d81786..41c8b6d 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -2,23 +2,21 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions -import prolog.ast.Database.Program import prolog.ast.logic.LogicOperand import prolog.ast.logic.LogicOperator import prolog.ast.terms.Atom import prolog.ast.terms.Body import prolog.ast.terms.Goal +import prolog.ast.terms.Structure import prolog.flags.AppliedCut -import prolog.flags.AppliedShift import prolog.logic.applySubstitution -import prolog.logic.numbervars /** * Always fail. */ object Fail : Atom("fail"), Body { override fun satisfy(subs: Substitutions): Answers = emptySequence() - override fun applySubstitution(subs: Substitutions): Fail = this + override fun applySubstitution(subs: Substitutions): Fail = Fail } /** @@ -31,7 +29,7 @@ typealias False = Fail */ object True : Atom("true"), Body { override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap())) - override fun applySubstitution(subs: Substitutions): True = this + override fun applySubstitution(subs: Substitutions): True = True } // TODO Repeat/0 @@ -41,72 +39,62 @@ class Cut() : Atom("!") { return sequenceOf(Result.failure(AppliedCut(emptyMap()))) } - override fun applySubstitution(subs: Substitutions): Cut = this + override fun applySubstitution(subs: Substitutions): Cut = Cut() } /** * Conjunction (and). True if both Goal1 and Goal2 are true. */ -open class Conjunction(val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(",", left, right) { +class Conjunction(val left: LogicOperand, private val right: LogicOperand) : + LogicOperator(Atom(","), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { - fun satisfyRight(leftSubs: Substitutions): Answers = sequence { - right.satisfy(subs + leftSubs).forEach { right -> - right.fold( - // If the right part succeeds, yield the result with the left substitutions - onSuccess = { rightSubs -> - yield(Result.success(leftSubs + rightSubs)) - }, - onFailure = { exception -> - // If the right part fails, check if it's a cut - if (exception is AppliedCut) { - // If it's a cut, yield the result with the left substitutions - val newSubs = if (exception.subs != null) leftSubs + exception.subs else null - yield(Result.failure(AppliedCut(newSubs))) - return@sequence - } - - // If it's not a cut, yield the failure - yield(Result.failure(exception)) - } - ) - } - } - - fun findNextCutSolution(appliedCut: AppliedCut): Answers = sequence { - val leftSubs = appliedCut.subs - right.satisfy(subs + (appliedCut.subs!!)).firstOrNull()?.map { rightSubs -> - // If the right part succeeds, yield the result with the left substitutions - yield(Result.success(leftSubs + rightSubs)) - return@sequence - } ?: yield(Result.failure(AppliedCut())) - } - // Satisfy the left part first, which either succeeds or fails left.satisfy(subs).forEach { left -> left.fold( // If it succeeds, satisfy the right part with the updated substitutions and return all results - onSuccess = { leftSubs -> yieldAll(satisfyRight(leftSubs)) }, + onSuccess = { leftSubs -> + right.satisfy(subs + leftSubs).forEach { + it.fold( + // If the right part succeeds, yield the result with the left substitutions + onSuccess = { rightSubs -> + yield(Result.success(leftSubs + rightSubs)) + }, + // If the right part fails, check if it's a cut + onFailure = { exception -> + if (exception is AppliedCut) { + if (exception.subs != null) { + // If it's a cut, yield the result with the left substitutions + yield(Result.failure(AppliedCut(leftSubs + exception.subs))) + } else { + yield(Result.failure(AppliedCut())) + } + return@sequence + } + + // If it's not a cut, yield the failure + yield(Result.failure(exception)) + } + ) + } + }, // If it fails, check these conditions: onFailure = { exception -> - when (exception) { - // 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions - is AppliedCut -> yieldAll(findNextCutSolution(exception)) - - // 2. If the left part is a shift, we need to check if the right part can be satisfied - is AppliedShift -> { - if (exception.cont == null) { - // Pass the right of our disjunction as the continuation - val newShift = AppliedShift(exception.subs, exception.ball, right as Goal) - yield(Result.failure(newShift)) - } else { - // Satisfy the right part with the updated substitutions - yieldAll(satisfyRight(exception.subs)) + // 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions + if (exception is AppliedCut) { + right.satisfy(subs + (exception.subs!!)).firstOrNull()?.fold( + onSuccess = { + // If the right part succeeds, yield the result with the left substitutions + yield(Result.success(exception.subs + it)) + return@sequence + }, + onFailure = { + // If the right part fails, yield the failure + yield(Result.failure(it)) } - } - - // 3. Any other failure should be returned as is - else -> yield(Result.failure(exception)) + ) ?: yield(Result.failure(AppliedCut())) + } else { + // 2. Any other failure should be returned as is + yield(Result.failure(exception)) } } ) @@ -123,22 +111,9 @@ open class Conjunction(val left: LogicOperand, private val right: LogicOperand) * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(";", left, right) { + LogicOperator(Atom(";"), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { - left.satisfy(subs).forEach { left -> - left.fold( - onSuccess = { leftSubs -> - yield(Result.success(leftSubs)) - }, - onFailure = { failure -> - if (failure is AppliedCut) { - val leftSubs = failure.subs - yield(Result.failure(AppliedCut(leftSubs))) - return@sequence - } - } - ) - } + yieldAll(left.satisfy(subs)) yieldAll(right.satisfy(subs)) } @@ -158,7 +133,7 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l /** * True if 'Goal' cannot be proven. */ -open class Not(private val goal: Goal) : LogicOperator("\\+", rightOperand = goal) { +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 val goalResults = goal.satisfy(subs).iterator() diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index 922201f..c8f3b29 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -1,23 +1,27 @@ package prolog.builtins -import io.Logger import prolog.Answers import prolog.Substitutions -import prolog.ast.Database -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer import prolog.ast.logic.Clause -import prolog.ast.logic.Fact +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure import prolog.ast.logic.Predicate -import prolog.ast.terms.* +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(Atom("dynamic"), Integer(1)) +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] @@ -39,17 +43,18 @@ class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body { 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(Atom("assert"), Integer(1)) + 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("asserta", rightOperand = clause) { +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 @@ -64,7 +69,7 @@ class AssertA(val clause: Clause) : Operator("asserta", rightOperand = clause) { /** * Assert a [Clause] as a last clause of the [Predicate] into the [Program]. */ -open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clause) { +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 @@ -82,7 +87,7 @@ open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clau * * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1) */ -open class Retract(val term: Term) : Operator("retract", rightOperand = term) { +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) { @@ -97,12 +102,6 @@ open class Retract(val term: Term) : Operator("retract", rightOperand = term) { return@sequence } - // Check if the predicate is dynamic - if (!predicate.dynamic) { - yield(Result.failure(Exception("No permission to modify static procedure '$functorName'"))) - return@sequence - } - predicate.clauses.toList().forEach { clause -> unifyLazy(term, clause.head, subs).forEach { unifyResult -> unifyResult.fold( @@ -121,29 +120,3 @@ open class Retract(val term: Term) : Operator("retract", rightOperand = term) { override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs)) } - -class RetractAll(term: Term) : Retract(term) { - override fun satisfy(subs: Substitutions): Answers { - // Check that term is a structure or atom - if (term !is Structure && term !is Atom) { - return sequenceOf(Result.failure(Exception("Cannot retract a non-structure or non-atom"))) - } - - // If the predicate does not exist, implicitly create it - val functor = term.functor - val predicate = Program.db.predicates[functor] - if (predicate == null) { - Logger.debug("Predicate $functor not found, creating it") - Program.db.predicates += functor to Predicate(functor, dynamic = true) - } - - // Propagate errors from the super class - super.satisfy(subs).forEach { - if (it.isFailure) { - return sequenceOf(it) - } - } - - return sequenceOf(Result.success(emptyMap())) - } -} diff --git a/src/prolog/builtins/delimitedContinuationsOperators.kt b/src/prolog/builtins/delimitedContinuationsOperators.kt deleted file mode 100644 index 43f6e22..0000000 --- a/src/prolog/builtins/delimitedContinuationsOperators.kt +++ /dev/null @@ -1,74 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.arithmetic.Integer -import prolog.ast.terms.Goal -import prolog.ast.terms.Structure -import prolog.ast.terms.Term -import prolog.flags.AppliedShift -import prolog.logic.applySubstitution -import prolog.logic.unifyLazy - -/** - * These classes provide support for delimited continuations in Prolog. - * More specifically, they implement the reset/3 and shift/1 operators. - * - * See also [SWI-Prolog 4.9 Delimited Continuations](https://www.swi-prolog.org/pldoc/man?section=delcont) - */ - -/** - * Call [Goal]. If Goal calls [Shift], and the arguments of Shift can be unified with Ball, Shift causes Reset to - * return, unifying Cont with a Goal that represents the continuation after shift. - */ -class Reset(private val goal: Goal, private val ball: Term, private val cont: Term) : - Structure("reset", goal, ball, cont) { - override fun satisfy(subs: Substitutions): Answers = sequence { - goal.satisfy(subs).forEach { goalResult -> - goalResult.fold( - // If Goal succeeds, then reset/3 also succeeds and binds Cont and Term1 to 0. - onSuccess = { goalSubs -> - unifyLazy(cont, Integer(0), goalSubs).forEach { contResult -> - contResult.map { contSubs -> - yield(Result.success(goalSubs + contSubs)) - } - } - }, - onFailure = { failure -> - // If at some point Goal calls shift(Term2), then its further execution is suspended. - if (failure is AppliedShift) { - require(failure.cont != null) { "Shift must have a continuation" } - // Reset/3 succeeds immediately, binding Term1 to Term2 and Cont to the remainder of Goal. - val shiftSubs = failure.subs - val appliedBall = applySubstitution(failure.ball, shiftSubs) - val appliedCont = applySubstitution(failure.cont, shiftSubs) - Conjunction(Unify(ball, appliedBall), Unify(appliedCont, cont)) - .satisfy(shiftSubs) - .forEach { conResult -> - conResult.map { conSubs -> - yield(Result.success(shiftSubs + conSubs)) - } - } - } else { - // If Goal fails, then reset also fails. - yield(Result.failure(failure)) - } - } - ) - } - } -} - -/** - * Variables that have been bound during the procedure called by reset/3 stay bound after a shift/1: - */ -class Shift(private val ball: Term) : Structure("shift", ball) { - override fun satisfy(subs: Substitutions): Answers = sequence { - val shift = AppliedShift( - subs = subs, - ball = ball, - cont = null - ) - yield(Result.failure(shift)) - } -} diff --git a/src/prolog/builtins/ioOperators.kt b/src/prolog/builtins/ioOperators.kt index e841679..4c80d61 100644 --- a/src/prolog/builtins/ioOperators.kt +++ b/src/prolog/builtins/ioOperators.kt @@ -16,9 +16,7 @@ import prolog.logic.unifyLazy /** * Write [Term] to the current output, using brackets and operators where appropriate. */ -class Write(private val term: Term) : Operator("write", rightOperand = term), Satisfiable { - constructor(message: String) : this(Atom(message)) - +class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t = applySubstitution(term, subs) @@ -47,12 +45,6 @@ object Nl : Atom("nl"), Satisfiable { override fun applySubstitution(subs: Substitutions): Nl = this } -class WriteLn(private val term: Term) : Conjunction(Write(term), Nl) { - constructor(message: String) : this(Atom(message)) - override fun applySubstitution(subs: Substitutions): WriteLn = WriteLn(applySubstitution(term, subs)) - override fun toString(): String = "writeln($term)" -} - /** * Read the next Prolog term from the current input stream and unify it with [Term]. * diff --git a/src/prolog/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt deleted file mode 100644 index 9835c44..0000000 --- a/src/prolog/builtins/listOperators.kt +++ /dev/null @@ -1,78 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.lists.List -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty -import prolog.ast.terms.Body -import prolog.ast.terms.Operator -import prolog.ast.terms.Structure -import prolog.ast.terms.Term -import prolog.ast.terms.Variable -import prolog.logic.applySubstitution -import prolog.logic.unifyLazy - -class Member(private val element: Term, private val list: Term) : Operator("member", element, list) { - private var solution: Body = when (list) { - is Empty -> Fail - is Cons -> Disjunction( - Unify(element, list.head), - Member(element, list.tail) - ) - - else -> { - // Generate a sequence of lists that have anonymous variables in them. - // Place element at each index - // TODO Fix this - Unify(element, list) - } - } - - override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs) - - override fun applySubstitution(subs: Substitutions): Member = Member( - applySubstitution(element, subs), - applySubstitution(list, subs) as List - ) - - override fun toString(): String = "$element ∈ $list" -} - -class Append(private val list1: Term, private val list2: Term, private val list3: Term) : - Structure("append", list1, list2, list3) { - override fun satisfy(subs: Substitutions): Answers = sequence { - val l1 = applySubstitution(list1, subs) - val l2 = applySubstitution(list2, subs) - val l3 = applySubstitution(list3, subs) - - if (l1 is Empty) { - yieldAll(unifyLazy(l2, l3, subs)) - } - - val head1 = if (l1 is Cons) l1.head else Variable("Head1") - val tail1 = if (l1 is Cons) l1.tail else Variable("Tail1") - val head3 = if (l3 is Cons) l3.head else Variable("Head3") - val tail3 = if (l3 is Cons) l3.tail else Variable("Tail3") - - unifyLazy(head1, head3, subs).forEach { headResult -> - headResult.map { headSubs -> - val newSubs = subs + headSubs - Append(tail1, list2, tail3).satisfy(newSubs).forEach { tailResult -> - tailResult.map { tailSubs -> - val result = headSubs + tailSubs - yield(Result.success(result)) - } - } - } - } - - TODO("This does not return the expected results, especially when using variables for the lists.") - } - - override fun applySubstitution(subs: Substitutions): Append = Append( - applySubstitution(list1, subs), - applySubstitution(list2, subs), - applySubstitution(list3, subs) - ) -} diff --git a/src/prolog/builtins/loadingSourceOperators.kt b/src/prolog/builtins/loadingSourceOperators.kt deleted file mode 100644 index 0f002f3..0000000 --- a/src/prolog/builtins/loadingSourceOperators.kt +++ /dev/null @@ -1,39 +0,0 @@ -package prolog.builtins - -import interpreter.FileLoader -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.Operator -import prolog.ast.terms.Term -import prolog.logic.applySubstitution - -class Consult(val file: Term) : Operator("consult", rightOperand = file) { - private val fileLoader = FileLoader() - - override fun satisfy(subs: Substitutions): Answers { - val fileAtom = applySubstitution(file, subs) - require(fileAtom is Atom) { "File name must be an atom" } - - var filePath = fileAtom.name - if (!filePath.endsWith(".pl")) { - filePath += ".pl" - } - - try { - fileLoader.load(filePath) - return sequenceOf(Result.success(emptyMap())) - } catch (e: Exception) { - return sequenceOf(Result.failure(e)) - } - } - - override fun toString(): String = "consult($file)" -} - -class Initialization(val goal: LogicOperand) : LogicOperator(":-", rightOperand = goal) { - override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1) - override fun toString(): String = goal.toString() -} diff --git a/src/prolog/builtins/metaOperators.kt b/src/prolog/builtins/metaOperators.kt deleted file mode 100644 index 3abbabb..0000000 --- a/src/prolog/builtins/metaOperators.kt +++ /dev/null @@ -1,51 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.terms.Goal -import prolog.ast.terms.Operator -import prolog.ast.terms.Term -import prolog.flags.AppliedCut -import prolog.logic.applySubstitution - -class Call(private val goal: Term) : Operator("call", rightOperand = goal) { - override fun satisfy(subs: Substitutions): Answers { - val appliedGoal = applySubstitution(goal, subs) as Goal - return appliedGoal.satisfy(subs) - } -} - -/** - * Make a possibly nondeterministic [Goal] semideterministic, i.e. succeed at most once. - */ -class Once(private val goal: Term) : Operator("once", rightOperand = goal) { - private val conjunction = Conjunction(Call(goal), Cut()) - override fun satisfy(subs: Substitutions): Answers = conjunction.satisfy(subs).take(1) -} - -/** - * Calls [Goal] once, but succeeds, regardless of whether Goal succeeded or not. - */ -class Ignore(goal: Term) : Operator("ignore", rightOperand = goal) { - private val disjunction = Disjunction( - Conjunction(Call(goal), Cut()), - True - ) - - override fun satisfy(subs: Substitutions): Answers = sequence { - disjunction.satisfy(subs).forEach { result -> - result.fold( - onSuccess = { newSubs -> - yield(Result.success(newSubs)) - }, - onFailure = { failure -> - if (failure is AppliedCut && failure.subs != null) { - yield(Result.success(failure.subs)) - } else { - yield(Result.failure(failure)) - } - } - ) - } - } -} diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 88170fb..4cc582f 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -3,21 +3,14 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions import prolog.ast.logic.LogicOperand +import prolog.ast.terms.Atom import prolog.ast.logic.LogicOperator -import prolog.ast.terms.Goal -class Query(val query: LogicOperand) : LogicOperator("?-", rightOperand = 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) } - -/** - * For all alternative bindings of Cond, Action can be proven. - * It does not say which is wrong if one proves wrong. - * - * @see [SWI-Prolog Predicate forall/2](https://www.swi-prolog.org/pldoc/doc_for?object=forall/2) - */ -class ForAll(private val condition: LogicOperand, private val action: Goal) : - Not(Conjunction(condition, Not(action))) { - override fun toString() = "forall($condition, $action)" -} - diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index c00175d..6019b18 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -7,6 +7,7 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions +import prolog.ast.terms.Atom import prolog.ast.terms.Operator import prolog.ast.terms.Term import prolog.logic.applySubstitution @@ -16,12 +17,12 @@ import prolog.logic.unifyLazy /** * Unify Term1 with Term2. True if the unification succeeds. */ -class Unify(private val term1: Term, private val term2: Term): Operator("=", term1, term2) { +class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="), term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - yieldAll(unifyLazy(t1, t2, emptyMap())) + yieldAll(unifyLazy(t1, t2, subs)) } override fun applySubstitution(subs: Substitutions): Unify = Unify( @@ -30,16 +31,21 @@ class Unify(private val term1: Term, private val term2: Term): Operator("=", ter ) } -class NotUnify(private val term1: Term, private val term2: Term) : Not(Unify(term1, term2)) { - override fun toString(): String = "($term1 \\= $term2)" +class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) { + private val not = Not(Unify(term1, term2)) + override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs) + override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify( + applySubstitution(term1, subs), + applySubstitution(term2, subs) + ) } -class Equivalent(private val term1: Term, private val term2: Term) : Operator("==", term1, term2) { +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) val t2 = applySubstitution(term2, subs) - if (equivalent(t1, t2, emptyMap())) { + if (equivalent(t1, t2, subs)) { yield(Result.success(emptyMap())) } } @@ -49,7 +55,3 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator("= applySubstitution(term2, subs) ) } - -class NotEquivalent(private val term1: Term, private val term2: Term) : Not(Equivalent(term1, term2)) { - override fun toString(): String = "($term1 \\== $term2)" -} diff --git a/src/prolog/builtins/verificationOperators.kt b/src/prolog/builtins/verificationOperators.kt deleted file mode 100644 index fc87091..0000000 --- a/src/prolog/builtins/verificationOperators.kt +++ /dev/null @@ -1,52 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.terms.Operator -import prolog.ast.terms.Term -import prolog.logic.* - -class Atomic(private val term: Term) : Operator("atomic", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (atomic(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Atomic = Atomic(applySubstitution(term, subs)) -} - -class Compound(private val term: Term) : Operator("compound", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (compound(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Compound = Compound(applySubstitution(term, subs)) -} - -class NonVar(private val term: Term) : Operator("nonvar", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (nonvariable(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): NonVar = NonVar(applySubstitution(term, subs)) -} - -class Var(private val term: Term) : Operator("var", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (variable(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Var = Var(applySubstitution(term, subs)) -} diff --git a/src/prolog/flags/AppliedShift.kt b/src/prolog/flags/AppliedShift.kt deleted file mode 100644 index a96b55d..0000000 --- a/src/prolog/flags/AppliedShift.kt +++ /dev/null @@ -1,14 +0,0 @@ -package prolog.flags - -import prolog.Substitutions -import prolog.ast.terms.Goal -import prolog.ast.terms.Term - -/** - * An exception that indicates that a shift has been applied in the Prolog engine. - */ -data class AppliedShift( - val subs: Substitutions, - val ball: Term, - val cont: Term? = null, -) : Throwable() \ No newline at end of file diff --git a/src/prolog/logic/terms.kt b/src/prolog/logic/terms.kt index 459d58d..8c2b26f 100644 --- a/src/prolog/logic/terms.kt +++ b/src/prolog/logic/terms.kt @@ -1,10 +1,29 @@ 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 + * arguments are all different variables (such a term is called a skeleton). If Term is atomic, Arity will be unified + * with the integer 0, and Name will be unified with Term. Raises instantiation_error() if Term is unbound and + * Name/Arity is insufficiently instantiated. + * + * SWI-Prolog also supports terms with arity 0, as in a() (see + * [section 5](https://www.swi-prolog.org/pldoc/man?section=extensions)). Such terms must be processed using functor/4 + * or compound_name_arity/3. The predicate functor/3 and =../2 raise a domain_error when faced with these terms. + * Without this precaution a round trip of a term with arity 0 over functor/3 would create an atom. + * + * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3) + */ +fun functor(term: Term, name: Atom, arity: Int): Boolean { + // TODO Implement + return true +} + /** * Unify the free variables in Term with a term $VAR(N), where N is the number of the variable. * Counting starts at Start. diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 1ac842b..5b5d21e 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -7,11 +7,11 @@ import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer import prolog.ast.arithmetic.Number -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty +import prolog.ast.logic.Clause import prolog.ast.logic.Fact +import prolog.ast.logic.LogicOperator +import prolog.ast.logic.Rule import prolog.ast.terms.* -import prolog.ast.lists.List as PList // Apply substitutions to a term fun applySubstitution(term: Term, subs: Substitutions): Term = when { @@ -21,19 +21,28 @@ fun applySubstitution(term: Term, subs: Substitutions): Term = when { val variable = term as Variable subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term } - atomic(term, subs) -> term - compound(term, subs) -> term.applySubstitution(subs) + compound(term, subs) -> { + term.applySubstitution(subs) + } else -> term } -fun applySubstitution(expr: Expression, subs: Substitutions): Expression { - return applySubstitution(expr as Term, subs) as Expression +//TODO Combine with the other applySubstitution function +fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when { + 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 -fun occurs(variable: Variable, term: Term, subs: Substitutions = emptyMap()): Boolean = when { +fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when { variable(term, subs) -> term == variable atomic(term, subs) -> false compound(term, subs) -> { @@ -50,10 +59,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val t2 = applySubstitution(term2, subs) when { - equivalent(t1, t2, subs) -> { - yield(Result.success(emptyMap())) - } - + equivalent(t1, t2, subs) -> yield(Result.success(emptyMap())) variable(t1, subs) -> { val variable = t1 as Variable if (!occurs(variable, t2, subs)) { @@ -76,32 +82,18 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val args1 = structure1.arguments val args2 = structure2.arguments if (args1.size == args2.size) { - yieldAll(unifyArgs(args1, args2, subs)) - } - } - } - - t1 is PList && t2 is PList -> { - if (equivalent(t1, t2, subs)) { - yield(Result.success(emptyMap())) - } else if (t1.size == t2.size) { - val head1 = t1.head - val head2 = t2.head - - unifyLazy(head1, head2, subs).forEach { headSubs -> - headSubs.map { headResult -> - if (t1 is Empty && t2 is Empty) { - yield(Result.success(headResult)) - } else if (t1 is Cons && t2 is Cons) { - val tail1 = t1.tail - val tail2 = t2.tail - unifyLazy(tail1, tail2, headResult).forEach { tailSubs -> - tailSubs.map { tailResult -> - yield(Result.success(headResult + tailResult)) - } - } - } + val results = args1.zip(args2).map { (arg1, arg2) -> + unifyLazy(arg1, arg2, subs) } + // Combine the results of all unifications + val combinedResults = results.reduce { acc, result -> + acc.flatMap { a -> + result.map { b -> + if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap() + } + }.map { Result.success(it) } + } + yieldAll(combinedResults) } } } @@ -110,32 +102,6 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence } } -private fun unifyArgs( - args1: List, - args2: List, - subs: Substitutions -): Answers = sequence { - // Using the current subs, unify the first argument of each list - val arg1 = applySubstitution(args1[0], subs) - val arg2 = applySubstitution(args2[0], subs) - unifyLazy(arg1, arg2, subs).forEach { headResult -> - // Use the resulting substitutions to unify the rest of the arguments - headResult.map { headSubs -> - val rest1 = args1.drop(1).map { applySubstitution(it, headSubs) } - val rest2 = args2.drop(1).map { applySubstitution(it, headSubs) } - if (rest1.isEmpty() && rest2.isEmpty()) { - yield(Result.success(headSubs)) - } else if (rest1.isNotEmpty() && rest2.isNotEmpty()) { - unifyArgs(rest1, rest2, subs).forEach { tailResult -> - tailResult.map { tailSubs -> - yield(Result.success(headSubs + tailSubs)) - } - } - } - } - } -} - fun unify(term1: Term, term2: Term): Answer { val substitutions = unifyLazy(term1, term2, emptyMap()).iterator() return if (substitutions.hasNext()) { @@ -151,32 +117,12 @@ fun unify(term1: Term, term2: Term): Answer { fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean { return when { term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0 - term1 is Structure && term2 is Structure -> { - term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) -> - equivalent(arg1, arg2, subs) - } - } - + term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0 term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0 term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0 term1 is Variable && term2 is Variable -> term1 == term2 term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs) term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs) - term1 is PList && term2 is PList -> { - if (term1.isEmpty() && term2.isEmpty()) { - true - } else if (term1.isEmpty() || term2.isEmpty()) { - false - } else { - require(term1 is Cons && term2 is Cons) - val head1 = term1.head - val tail1 = term1.tail - val head2 = term2.head - val tail2 = term2.tail - equivalent(head1, head2, subs) && equivalent(tail1, tail2, subs) - } - } - else -> false } } diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt index 688cea4..5e8b0d4 100644 --- a/src/repl/Repl.kt +++ b/src/repl/Repl.kt @@ -6,7 +6,6 @@ import io.Terminal import parser.ReplParser import prolog.Answer import prolog.Answers -import prolog.flags.AppliedCut class Repl { private val io = Terminal() @@ -30,52 +29,40 @@ class Repl { } private fun query(): Answers { - val queryString = io.prompt("?-", { "| " }, { it.endsWith(".") }) + 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") - return - } + } else { + io.say(prettyPrint(iterator.next())) - io.say(prettyPrint(iterator.next())) + while (iterator.hasNext()) { + var command = io.prompt("") - while (true) { - when (io.prompt("")) { - ";" -> { - try { + while (command !in knownCommands) { + io.say("Unknown action: $command (h for help)\n") + command = io.prompt("Action?") + } + + when (command) { + ";" -> { io.say(prettyPrint(iterator.next())) - } catch (_: NoSuchElementException) { - break } - } - - "" -> { - io.checkNewLine() - return - } - "a" -> { - io.checkNewLine() - return - } - "." -> { - io.checkNewLine() - return - } - "h" -> { - help() - io.say("Action?") - } - - else -> { - io.say("Unknown action: (h for help)\n") - io.say("Action?") + "a" -> return + "." -> return + "h" -> { + help() + io.say("Action?") + } } } } @@ -102,15 +89,10 @@ class Repl { } return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" } }, - onFailure = { failure -> - if (failure is AppliedCut) { - if (failure.subs != null) { - return prettyPrint(Result.success(failure.subs)) - } - return "false." - } - - return "ERROR: ${failure.message}" + onFailure = { + val text = "Failure: ${it.message}" + Logger.warn(text) + return text } ) } diff --git a/src/tool/mapEach.kt b/src/tool/mapEach.kt deleted file mode 100644 index 1786867..0000000 --- a/src/tool/mapEach.kt +++ /dev/null @@ -1,3 +0,0 @@ -package tool - -fun Sequence.mapEach(transform: (T) -> R): Sequence = map(transform) diff --git a/tests/e2e/Examples.kt b/tests/e2e/Examples.kt index 250f804..f93fc35 100644 --- a/tests/e2e/Examples.kt +++ b/tests/e2e/Examples.kt @@ -27,7 +27,7 @@ class Examples { @Test fun debugHelper() { - loader.load("examples/meta/continuations.pl") + loader.load("examples/basics/backtracking.pl") } @ParameterizedTest @@ -37,13 +37,6 @@ class Examples { assertEquals(expected, outStream.toString()) } - @ParameterizedTest - @MethodSource("meta") - fun `Identical output for meta`(inputFile: String, expected: String) { - loader.load("examples/meta/$inputFile") - assertEquals(expected, outStream.toString()) - } - @ParameterizedTest @MethodSource("other") fun `Identical output for other`(inputFile: String, expected: String) { @@ -52,7 +45,7 @@ class Examples { } 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.\n"), + 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"), @@ -64,11 +57,6 @@ class Examples { Arguments.of("write.pl", "gpl zegt: dag(wereld)\n"), ) - fun meta() = listOf( - Arguments.of("continuations.pl", "Inside test\nEntering reset\nAfter reset\nCalling Cont(2)\nIn test X = 5; done\nCalling Cont(4)\nIn test X = 9; done\n"), - Arguments.of("mib_voorbeelden.pl", "b\nf(b)\nf(g(a,a),h(c,d),i(e,f))\nf(g(a,a),h(c,c),i(e,f))\nf(g(a,a),h(c,c),i(e,e))\n") - ) - fun other() = listOf( Arguments.of("program.pl", "10\nhello(world)") ) diff --git a/tests/interpreter/ParserPreprocessorIntegrationTests.kt b/tests/interpreter/ParserPreprocessorIntegrationTests.kt index cf1cd94..05df756 100644 --- a/tests/interpreter/ParserPreprocessorIntegrationTests.kt +++ b/tests/interpreter/ParserPreprocessorIntegrationTests.kt @@ -41,7 +41,10 @@ class ParserPreprocessorIntegrationTests { val parsed = parser.parseToEnd("X is $input") as Term assertEquals( - Structure("is", Variable("X"), Structure("-",number)), + Structure(Atom("is"), listOf( + Variable("X"), + Structure(Atom("-"), listOf(number)), + )), parsed ) @@ -71,7 +74,7 @@ class ParserPreprocessorIntegrationTests { val result = parser.parseToEnd(input) as Term assertEquals( - Structure("is", Variable("X"), Structure("-", Integer(1), Integer(2))), + Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))), result ) diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index 60bcbf9..bf54869 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -6,6 +6,7 @@ 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.* @@ -37,7 +38,7 @@ class PreprocessorTests { @Test fun `multiple anonymous variables should be unique`() { - val input = CompoundTerm("foo", Variable("_"), Variable("_")) + val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_"))) val result = preprocessor.preprocess(input) @@ -68,7 +69,7 @@ class PreprocessorTests { for (argument in inner.arguments) { if ((argument as Variable).name != "Name") { assertTrue( - argument.name.matches("_\\d+".toRegex()), + (argument as Variable).name.matches("_\\d+".toRegex()), "Expected anonymous variable name, but got ${argument.name}" ) } @@ -83,13 +84,27 @@ class PreprocessorTests { test( mapOf( Atom("=\\=") to Atom("=\\="), - CompoundTerm("=\\=") to CompoundTerm("=\\="), + CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()), Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"), - CompoundTerm("EvaluatesToDifferent") to CompoundTerm("EvaluatesToDifferent"), - CompoundTerm("=\\=", Atom("a")) to CompoundTerm("=\\=", Atom("a")), - CompoundTerm("=\\=", Integer(1)) to CompoundTerm("=\\=", Integer(1)), - CompoundTerm("=\\=", Atom("=\\=")) to CompoundTerm("=\\=", Atom("=\\=")), - CompoundTerm("=\\=", Integer(1), Integer(2)) to EvaluatesToDifferent(Integer(1), Integer(2)) + 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) + ) ) ) } @@ -99,7 +114,7 @@ class PreprocessorTests { test( mapOf( Atom("=:=") to Atom("=:="), - CompoundTerm("=:=") to CompoundTerm("=:="), + CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()), Atom("EvaluatesTo") to Atom("EvaluatesTo"), CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm( Atom("EvaluatesTo"), @@ -597,7 +612,7 @@ class PreprocessorTests { Atom("declaration/1") ) ) - val expected = Dynamic(Functor.of("declaration/1")) + val expected = Dynamic("declaration/1") val result = preprocessor.preprocess(input) diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index 5ca662a..57a1f99 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -2,6 +2,7 @@ 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 @@ -13,7 +14,7 @@ import prolog.ast.logic.Rule import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Structure import prolog.ast.terms.Variable -import prolog.ast.terms.Functor +import prolog.builtins.Conjunction class LogicGrammarTests { private lateinit var parser: Grammar> @@ -32,7 +33,7 @@ class LogicGrammarTests { "male(jimmy).", "female(mary).", "not(not(true)).", - "not(a,not(b,c),d,not(not(a)))." + "not(a, not(b, c), d, not(not(a)))." ]) fun `parse simple fact`(input: String) { val result = parser.parseToEnd(input) @@ -93,13 +94,13 @@ class LogicGrammarTests { assertTrue(rule.head is Structure, "Expected head to be a structure") val head = rule.head as Structure - assertEquals(Functor.of("parent/2"), head.functor, "Expected functor 'parent/2'") + assertEquals("parent/2", head.functor, "Expected functor 'parent/2'") assertEquals(Variable("X"), head.arguments[0], "Expected first argument 'X'") assertEquals(Variable("Y"), head.arguments[1], "Expected second argument 'Y'") assertTrue(rule.body is Structure, "Expected body to be a structure") val body = rule.body as Structure - assertEquals(Functor.of("father/2"), body.functor, "Expected functor 'father/2'") + assertEquals("father/2", body.functor, "Expected functor 'father/2'") assertEquals(Variable("X"), body.arguments[0], "Expected first argument 'X'") assertEquals(Variable("Y"), body.arguments[1], "Expected second argument 'Y'") } @@ -124,13 +125,12 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") val rule = result[0] as Rule - assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'") - assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'") - val l0 = (rule.body as CompoundTerm) - val l1 = l0.arguments[0] as CompoundTerm - assertEquals(Functor.of("invited/2"), l1.functor, "Expected functor 'invited/2'") - val l2 = l0.arguments[1] as CompoundTerm - assertEquals(Functor.of(",/2"), l2.functor, "Expected functor ',/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 @@ -157,6 +157,6 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") assertTrue(result[0] is Rule, "Expected a rule") val rule = result[0] as Rule - assertEquals(Functor.of("/0"), rule.head.functor, "Expected a constraint") + assertEquals("/_", rule.head.functor, "Expected a constraint") } } \ No newline at end of file diff --git a/tests/parser/grammars/TermsGrammarTests.kt b/tests/parser/grammars/TermsGrammarTests.kt index b39a0d8..d3b45e2 100644 --- a/tests/parser/grammars/TermsGrammarTests.kt +++ b/tests/parser/grammars/TermsGrammarTests.kt @@ -19,8 +19,6 @@ import prolog.ast.terms.Term import prolog.ast.terms.Variable import prolog.builtins.Is import prolog.logic.equivalent -import prolog.ast.lists.List.Empty -import prolog.ast.lists.List.Cons class TermsGrammarTests { private lateinit var parser: Grammar @@ -354,49 +352,4 @@ class TermsGrammarTests { ) } } - - @Nested - class Lists { - private lateinit var parser: Grammar - - @BeforeEach - fun setup() { - parser = TermsGrammar() as Grammar - } - - @Test - fun `parse empty list`() { - val input = "[]" - - val result = parser.parseToEnd(input) - - assertEquals(Empty, result, "Expected empty list") - } - - @Test - fun `parse non-empty list`() { - val input = "[a, b, c]" - - val result = parser.parseToEnd(input) - - assertEquals( - Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Empty))), - result, - "Expected non-empty list" - ) - } - - @Test - fun `parse nested lists`() { - val input = "[a, [b, c], d]" - - val result = parser.parseToEnd(input) - - assertEquals( - Cons(Atom("a"), Cons(Cons(Atom("b"), Cons(Atom("c"), Empty)), Cons(Atom("d"), Empty))), - result, - "Expected nested lists" - ) - } - } } \ No newline at end of file diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index 8392eae..d8310dd 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/tests/prolog/EvaluationTests.kt @@ -15,10 +15,7 @@ import prolog.ast.terms.Structure import prolog.ast.terms.Variable import prolog.ast.Database.Program import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List.Empty -import prolog.ast.lists.List.Cons import prolog.ast.terms.AnonymousVariable -import prolog.builtins.Unify class EvaluationTests { @BeforeEach @@ -428,10 +425,7 @@ class EvaluationTests { fun `leq Peano`() { val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create()))) val rule = Rule( - Structure( - Atom("leq"), - listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y")))) - ), + Structure(Atom("leq"), listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))), Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))), ) @@ -445,9 +439,7 @@ class EvaluationTests { assertEquals(1, subs.size, "Expected 1 substitution") assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0") - val result2 = - Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0)))))) - .toList() + val result2 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0)))))).toList() assertEquals(2, result2.size, "Expected 2 results") @@ -460,42 +452,5 @@ class EvaluationTests { val subs2b = result2[1].getOrNull()!! assertEquals(1, subs2b.size, "Expected 1 substitution") assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)") - - val result3 = Program.query( - Structure( - Atom("leq"), - listOf(Variable("X"), Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0)))))) - ) - ).toList() - - assertEquals(3, result3.size, "Expected 3 results") - assertTrue(result3[0].isSuccess, "Expected success") - val subs3a = result3[0].getOrNull()!! - assertEquals(1, subs3a.size, "Expected 1 substitution") - assertEquals(Integer(0), subs3a[Variable("X")], "Expected X to be 0") - assertTrue(result3[1].isSuccess, "Expected success") - val subs3b = result3[1].getOrNull()!! - assertEquals(1, subs3b.size, "Expected 1 substitution") - assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs3b[Variable("X")], "Expected X to be s(0)") - assertTrue(result3[2].isSuccess, "Expected success") - val subs3c = result3[2].getOrNull()!! - assertEquals(1, subs3c.size, "Expected 1 substitution") - assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))") - } - - @Test - fun `foo(emptyList) = foo(X)`() { - val list = Empty - val left = Structure(Atom("foo"), listOf(list)) - val right = Structure(Atom("foo"), listOf(Variable("X"))) - - val unific = Unify(left, right) - val result = unific.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(list, subs[Variable("X")], "Expected X to be list(1, 2)") } } diff --git a/tests/prolog/builtins/AnalysisOperatorsTests.kt b/tests/prolog/builtins/AnalysisOperatorsTests.kt deleted file mode 100644 index a6866c3..0000000 --- a/tests/prolog/builtins/AnalysisOperatorsTests.kt +++ /dev/null @@ -1,646 +0,0 @@ -package prolog.builtins - -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 org.junit.jupiter.api.assertThrows -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty -import prolog.ast.logic.Fact -import prolog.ast.logic.Rule -import prolog.ast.terms.* -import prolog.logic.equivalent - -class AnalysisOperatorsTests { - @Test - fun `functor(foo, foo, 0)`() { - val functor = FunctorOp(Atom("foo"), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `functor(foo(X), foo, Y)`() { - val functor = FunctorOp( - Structure(Atom("foo"), listOf(Variable("X"))), - Atom("foo"), - Variable("Y") - ) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Integer(1), subs[Variable("Y")]) - } - - @Test - fun `functor(foo, X, Y)`() { - val atom = Atom("foo") - val functor = FunctorOp(atom, Variable("X"), Variable("Y")) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(2, subs.size, "Expected 2 substitutions") - assertEquals(atom.functor.name, subs[Variable("X")]) - assertEquals(atom.functor.arity, subs[Variable("Y")]) - } - - @Test - fun `functor(X, foo, 1)`() { - val functor = FunctorOp(Variable("X"), Atom("foo"), Integer(1)) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertInstanceOf(Structure::class.java, subs[Variable("X")]) - val structure = subs[Variable("X")] as Structure - assertEquals(Atom("foo"), structure.name) - assertEquals(1, structure.arguments.size) - assertInstanceOf(AnonymousVariable::class.java, structure.arguments[0]) - } - - @Test - fun `functor(foo(a), foo, 0)`() { - val functor = FunctorOp(Structure(Atom("foo"), listOf(Atom("a"))), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `functor(foo(X), foo, 0)`() { - val functor = FunctorOp(Structure(Atom("foo"), listOf(Variable("X"))), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `functor(X, Y, 1)`() { - val functor = FunctorOp(Variable("X"), Variable("Y"), Integer(1)) - - val exception = assertThrows { - functor.satisfy(emptyMap()).toList() - } - assertEquals("Arguments are not sufficiently instantiated", exception.message) - } - - @Test - fun `arg without variables`() { - val arg = Arg( - Integer(1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Atom("a") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected no substitutions") - } - - @Test - fun `arg with variable value`() { - val arg = Arg( - Integer(1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("a"), subs[Variable("Term")]) - } - - @Test - fun `arg with variable arg`() { - val arguments = listOf(Atom("a"), Atom("b"), Atom("c")) - for (i in arguments.indices) { - val arg = Arg( - Variable("Arg"), - Structure(Atom("f"), arguments), - arguments[i] - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result for arg $i") - assertTrue(result[0].isSuccess, "Expected success for arg $i") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution for arg $i") - assertEquals(Integer(i + 1), subs[Variable("Arg")], "Expected arg to be $i + 1") - } - } - - @Test - fun `arg with backtracking`() { - val arg = Arg( - Variable("Position"), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(3, result.size, "Expected 3 results") - - assertTrue(result[0].isSuccess, "Expected success") - val subs1 = result[0].getOrNull()!! - assertEquals(2, subs1.size, "Expected 2 substitutions") - assertEquals(Integer(1), subs1[Variable("Position")]) - assertEquals(Atom("a"), subs1[Variable("Term")]) - - assertTrue(result[1].isSuccess, "Expected success") - val subs2 = result[1].getOrNull()!! - assertEquals(2, subs2.size, "Expected 2 substitutions") - assertEquals(Integer(2), subs2[Variable("Position")]) - assertEquals(Atom("b"), subs2[Variable("Term")]) - - assertTrue(result[2].isSuccess, "Expected success") - val subs3 = result[2].getOrNull()!! - assertEquals(2, subs3.size, "Expected 2 substitutions") - assertEquals(Integer(3), subs3[Variable("Position")]) - assertEquals(Atom("c"), subs3[Variable("Term")]) - } - - @Test - fun `arg raises error if Arg is not compound`() { - val arg = Arg(Integer(1), Atom("foo"), Variable("X")) - - val exception = assertThrows { - arg.satisfy(emptyMap()).toList() - } - assertEquals("Type error: `structure' expected, found `foo' (atom)", exception.message) - } - - @Test - fun `arg fails silently if arg = 0`() { - val arg = Arg( - Integer(0), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `arg fails silently if arg gt arity`() { - val arg = Arg( - Integer(4), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `arg raises error if arg lt 0`() { - val arg = Arg( - Integer(-1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val exception = assertThrows { - arg.satisfy(emptyMap()).toList() - } - assertEquals("Domain error: not_less_than_zero", exception.message) - } - - @Nested - class `Clause operator` { - @BeforeEach - fun setup() { - Program.reset() - } - - @Test - fun `clause fact atom without variables`() { - Program.load(listOf(Fact(Atom("foo")))) - - val result = ClauseOp( - Atom("foo"), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause fact compound without variables`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b")))) - ) - ) - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause rule without variables`() { - Program.load(listOf(Rule(Atom("foo"), Atom("bar")))) - - val result = ClauseOp( - Atom("foo"), - Atom("bar") - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause fact variable body`() { - Program.load(listOf(Fact(Atom("foo")))) - - val variable = Variable("Term") - val result = ClauseOp( - Atom("foo"), - variable - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(True, subs[variable]) - } - - @Test - fun `clause fact with variable head`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))) - ) - ) - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(Variable("X"))), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("a"), subs[Variable("X")]) - } - - @Test - fun `clause rule with variable body`() { - Program.load(listOf(Rule(Atom("foo"), Atom("bar")))) - - val result = ClauseOp( - Atom("foo"), - Variable("Term") - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("bar"), subs[Variable("Term")]) - } - - @Test - fun `clause fact variable value with backtracking`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("bar"), listOf(Atom("d")))), - Fact(CompoundTerm(Atom("bar"), listOf(Atom("e")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("c")))), - Rule( - CompoundTerm(Atom("foo"), listOf(Variable("X"))), - CompoundTerm(Atom("bar"), listOf(Variable("X"))) - ) - ) - ) - - val x = Variable("X") - val term = Variable("Term") - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(x)), - term - ).satisfy(emptyMap()).toList() - - assertEquals(4, result.size, "Expected 4 results") - - assertTrue(result[0].isSuccess, "Expected success") - val subs1 = result[0].getOrNull()!! - assertEquals(2, subs1.size, "Expected 2 substitutions") - assertEquals(Atom("a"), subs1[x], "Expected a") - assertEquals(True, subs1[term], "Expected True") - - assertTrue(result[1].isSuccess, "Expected success") - val subs2 = result[1].getOrNull()!! - assertEquals(2, subs2.size, "Expected 2 substitutions") - assertEquals(Atom("b"), subs2[x], "Expected b") - assertEquals(True, subs2[term], "Expected True") - - assertTrue(result[2].isSuccess, "Expected success") - val subs3 = result[2].getOrNull()!! - assertEquals(2, subs3.size, "Expected 2 substitutions") - assertEquals(Atom("c"), subs3[x], "Expected c") - assertEquals(True, subs3[term], "Expected True") - - assertTrue(result[3].isSuccess, "Expected success") - val subs4 = result[3].getOrNull()!! - assertEquals(1, subs4.size, "Expected 2 substitutions") - assertEquals( - CompoundTerm(Atom("bar"), listOf(Variable("X"))), - subs4[term], - "Expected bar(X)" - ) - } - } - - @Nested - class `Univ operator` { - @Test - fun `univ without variables`() { - val univ = Univ(Atom("foo"), Cons(Atom("foo"), Empty)) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `univ with variable list`() { - val list = Variable("List") - val univ = Univ( - CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))), - list - ) - val expected = Cons(Atom("foo"), Cons(Atom("a"), Cons(Atom("b"), Empty))) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(expected, subs[list], "Expected List to be $expected") - } - - @Test - fun `univ with variable in compound`() { - val list = Variable("List") - val univ = Univ( - CompoundTerm(Atom("foo"), listOf(Variable("X"))), - list - ) - val expected = Cons(Atom("foo"), Cons(Variable("X"), Empty)) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(expected, subs[list], "Expected List to be $expected") - } - - @Test - fun `univ with var foo`() { - val univ = Univ( - Variable("Term"), - Cons(Atom("foo"), Empty) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("foo"), subs[Variable("Term")], "Expected Term to be foo") - } - - @Test - fun `univ with var foo(a)`() { - val univ = Univ( - Variable("Term"), - Cons(Atom("foo"), Cons(Atom("a"), Empty)) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals( - Structure(Atom("foo"), listOf(Atom("a"))), - subs[Variable("Term")], - "Expected Term to be foo(a)" - ) - } - - @Test - fun `univ with var foo(X)`() { - val univ = Univ( - Variable("Term"), - Cons(Atom("foo"), Cons(Variable("X"), Empty)) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals( - Structure(Atom("foo"), listOf(Variable("X"))), - subs[Variable("Term")], - "Expected Term to be foo(X)" - ) - } - - @Test - fun `univ with var foo(a, b(X), c)`() { - val univ = Univ( - Variable("Term"), - Cons( - Atom("foo"), - Cons(Atom("a"), Cons(CompoundTerm(Atom("b"), listOf(Variable("X"))), Cons(Atom("c"), Empty))) - ) - ) - val expected = CompoundTerm( - Atom("foo"), - listOf(Atom("a"), CompoundTerm(Atom("b"), listOf(Variable("X"))), Atom("c")) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(expected, subs[Variable("Term")], "Expected Term to be $expected") - } - - @Test - fun `univ with unified var should return substitution`() { - val univ = Univ( - CompoundTerm( - Atom("foo"), listOf( - Atom("a"), - CompoundTerm(Atom("bar"), listOf(Variable("X"))), - Atom("c") - ) - ), - Cons( - Atom("foo"), - Cons(Atom("a"), Cons(CompoundTerm(Atom("bar"), listOf(Atom("b"))), Cons(Atom("c"), Empty))) - ) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("b"), subs[Variable("X")], "Expected X to be b") - } - - @Test - fun `univ of incompatible structures should fail`() { - val univ = Univ( - CompoundTerm(Atom("foo"), listOf(Atom("a"))), - Cons(Atom("bar"), Empty) - ) - - val result = univ.satisfy(emptyMap()).toList() - - assertEquals(0, result.size, "Expected 0 results") - } - - @Test - fun `univ with two vars should throw`() { - val univ = Univ(Variable("X"), Variable("Y")) - - val exception = assertThrows { - univ.satisfy(emptyMap()).toList() - } - assertEquals("Arguments are not sufficiently instantiated", exception.message) - } - - class OpenUniv(term: Term, list: Term) : Univ(term, list) { - public override fun listToTerm(list: List): Term = super.listToTerm(list) - public override fun termToList(term: Term): List = super.termToList(term) - } - - @Test - fun `a to term`() { - val univ = OpenUniv(Atom(""), Empty) - - val originalList = Cons(Atom("a"), Empty) - val originalTerm = Atom("a") - - val term = univ.listToTerm(originalList) - assertEquals(originalTerm, term, "Expected term to be a") - - val list = univ.termToList(term) - assertEquals(originalList, list, "Expected list to be [a]") - } - - @Test - fun `foo, bar to compound`() { - val univ = OpenUniv(Atom(""), Empty) - - val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Empty)) - val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar"))) - - val term = univ.listToTerm(originalList) - assertEquals(originalTerm, term) - - val list = univ.termToList(term) - assertEquals(originalList, list) - } - - @Test - fun `foo, bar, baz to compound`() { - val univ = OpenUniv(Atom(""), Empty) - - val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Atom("baz"), Empty))) - val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar"), Atom("baz"))) - - val term = univ.listToTerm(originalList) - assertEquals(originalTerm, term) - - val list = univ.termToList(term) - assertEquals(originalList, list) - } - - @Test - fun `foo, bar, (baz, bar) to compound with list`() { - val univ = OpenUniv(Atom(""), Empty) - - val originalList = - Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty))) - val originalTerm = CompoundTerm( - Atom("foo"), - listOf(Atom("bar"), Cons(Atom("baz"), Cons(Atom("bar"), Empty))) - ) - - val term = univ.listToTerm(originalList) - assertTrue(equivalent(originalTerm, term, emptyMap()), "Expected term to be foo(bar, [baz, bar]))") - - val list = univ.termToList(term) - assertTrue(equivalent(originalList, list, emptyMap()), "Expected list to be [foo, bar, [baz, bar]]") - } - } -} diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt index 51a27c3..8e96085 100644 --- a/tests/prolog/builtins/DatabaseOperatorsTests.kt +++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt @@ -8,13 +8,13 @@ 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.Functor import prolog.ast.terms.Structure import prolog.ast.terms.Variable @@ -39,7 +39,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates[Functor.of("a/_")]!!.clauses[0]) + assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0]) } @Test @@ -48,7 +48,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0]) } @Test @@ -60,7 +60,7 @@ class DatabaseOperatorsTests { createAssert(rule).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0]) } } @@ -91,8 +91,8 @@ class DatabaseOperatorsTests { AssertA(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) - assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) + assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1]) } } @@ -116,8 +116,8 @@ class DatabaseOperatorsTests { AssertZ(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) - assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) + assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1]) } } @@ -131,7 +131,7 @@ class DatabaseOperatorsTests { @Test fun `simple retract`() { - val predicate = Predicate(listOf(Fact(Atom("a"))), dynamic = true) + val predicate = Predicate(listOf(Fact(Atom("a")))) Program.db.load(predicate) assertEquals(1, Program.query(Atom("a")).count()) @@ -146,13 +146,11 @@ class DatabaseOperatorsTests { @Test fun `retract atom`() { - val predicate = Predicate( - listOf( - Fact(Atom("a")), - Fact(Atom("a")), - Fact(Atom("a")) - ), dynamic = true - ) + val predicate = Predicate(listOf( + Fact(Atom("a")), + Fact(Atom("a")), + Fact(Atom("a")) + )) Program.db.load(predicate) val control = Program.query(Atom("a")).toList() @@ -172,9 +170,11 @@ class DatabaseOperatorsTests { 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") @@ -183,13 +183,11 @@ class DatabaseOperatorsTests { @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")))) - ), dynamic = true - ) + 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() @@ -210,6 +208,7 @@ class DatabaseOperatorsTests { 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() @@ -219,6 +218,7 @@ class DatabaseOperatorsTests { 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() @@ -228,9 +228,8 @@ class DatabaseOperatorsTests { assertTrue(subs.isNotEmpty(), "Expected substitutions") assertTrue(Variable("X") in subs, "Expected variable X") assertEquals(Atom("d"), subs[Variable("X")], "Expected d") - assertEquals(0, predicate.clauses.size, "Expected no clauses") - assertFalse(result.hasNext(), "Expected no more results") + assertEquals(0, predicate.clauses.size, "Expected no clauses") } @Test @@ -293,45 +292,4 @@ class DatabaseOperatorsTests { assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob") assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi") } - - @Test - fun `retract all`() { - 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")))) - ), dynamic = true - ) - - Program.db.load(predicate) - - val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList() - assertEquals(3, control.size, "Expected 3 results") - assertEquals(3, Program.db.predicates[Functor.of("a/1")]!!.clauses.size, "Expected 3 clauses") - - val retract = RetractAll(Structure(Atom("a"), listOf(Variable("X")))) - val result = retract.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - assertEquals(0, Program.db.predicates[Functor.of("a/1")]!!.clauses.size, "Expected 0 clauses") - } - - @Test - fun `If Head refers to a predicate that is not defined, it is implicitly created as a dynamic predicate`() { - val predicateName = "idonotyetexist" - val predicateFunctor = Functor.of("$predicateName/1") - - assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before") - - val retractAll = RetractAll(Structure(Atom(predicateName), listOf(Variable("X")))) - val result = retractAll.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - - assertTrue(predicateFunctor in Program.db.predicates, "Expected predicate to exist after") - assertTrue(Program.db.predicates[predicateFunctor]!!.dynamic, "Expected predicate to be dynamic") - } } \ No newline at end of file diff --git a/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt deleted file mode 100644 index 7d461d0..0000000 --- a/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt +++ /dev/null @@ -1,73 +0,0 @@ -package prolog.builtins - -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue -import org.junit.jupiter.api.BeforeEach -import org.junit.jupiter.api.Test -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty -import prolog.ast.logic.Rule -import prolog.ast.terms.Atom -import prolog.ast.terms.Structure -import prolog.ast.terms.Variable - -class DelimitedContinuationsOperatorsTests { - @BeforeEach - fun setup() { - Program.reset() - } - - @Test - fun `example member`() { - val member = Member(Variable("X"), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty)))) - val reset = Reset(member, Variable("Ball"), Variable("Cont")) - - val result = reset.satisfy(emptyMap()).toList() - - assertEquals(3, result.size, "Expected 3 results") - - assertTrue(result[0].isSuccess, "Expected success for first result") - val subs0 = result[0].getOrNull()!! - assertEquals(2, subs0.size, "Expected 2 substitutions for first result") - assertEquals(Integer(1), subs0[Variable("X")]) - assertEquals(Integer(0), subs0[Variable("Cont")]) - - assertTrue(result[1].isSuccess, "Expected success for second result") - val subs1 = result[1].getOrNull()!! - assertEquals(2, subs1.size, "Expected 2 substitutions for second result") - assertEquals(Integer(2), subs1[Variable("X")]) - assertEquals(Integer(0), subs1[Variable("Cont")]) - - assertTrue(result[2].isSuccess, "Expected success for third result") - val subs2 = result[2].getOrNull()!! - assertEquals(2, subs2.size, "Expected 2 substitutions for third result") - assertEquals(Integer(3), subs2[Variable("X")]) - assertEquals(Integer(0), subs2[Variable("Cont")]) - } - - @Test - fun `example with output`() { - val reset = Reset(Atom("test_"), Variable("Term"), Variable("Cont")) - val isOp = Is(Variable("X"), Add(Integer(1), Multiply(Integer(2), Variable("Y")))) - Program.load( - listOf( - Rule( - Structure(Atom("test"), listOf(Variable("Cont"), Variable("Term"))), - Conjunction(WriteLn("Inside test"), Conjunction(reset, WriteLn("After reset"))) - ), - Rule( - Atom("test_"), - Conjunction(WriteLn("Entering reset"), Conjunction(Shift(Variable("Y")), Conjunction(isOp, Conjunction(Write("In test X = "), Conjunction(Write(Variable("X")), WriteLn("; done")))))) - ) - ) - ) - - val notNot2 = Not(Not(Conjunction(WriteLn("calling Cont(2)"), Conjunction(Unify(Variable("Term"), Integer(2)), Call(Variable("Cont")))))) - val notNot4 = Not(Not(Conjunction(WriteLn("calling Cont(4)"), Conjunction(Unify(Variable("Term"), Integer(4)), Call(Variable("Cont")))))) - val query = Conjunction(Structure(Atom("test"), listOf(Variable("Cont"), Variable("Term"))), Conjunction(notNot2, notNot4)) - - val result = query.satisfy(emptyMap()).toList() - } -} diff --git a/tests/prolog/builtins/IoOperatorsTests.kt b/tests/prolog/builtins/IoOperatorsTests.kt index 6bf8ee0..05607ec 100644 --- a/tests/prolog/builtins/IoOperatorsTests.kt +++ b/tests/prolog/builtins/IoOperatorsTests.kt @@ -55,7 +55,7 @@ class IoOperatorsTests { 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") + assertEquals("person(john, doe)", outStream.toString().trim(), "Output should match the structure") } @Test diff --git a/tests/prolog/builtins/ListOperatorsTests.kt b/tests/prolog/builtins/ListOperatorsTests.kt deleted file mode 100644 index f6d0b71..0000000 --- a/tests/prolog/builtins/ListOperatorsTests.kt +++ /dev/null @@ -1,232 +0,0 @@ -package prolog.builtins - -import com.sun.source.tree.EmptyStatementTree -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue -import org.junit.jupiter.api.Disabled -import org.junit.jupiter.api.Test -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty -import prolog.ast.terms.Atom -import prolog.ast.terms.Term -import prolog.ast.terms.Variable - -class ListOperatorsTests { - @Test - fun `size empty list is 0`() { - assertEquals(0, Empty.size.value, "Expected size of empty list to be 0") - } - - @Test - fun `size of singleton is 1`() { - val list = Cons(Atom("a"), Empty) - - assertEquals(1, list.size.value, "Expected size of singleton list to be 1") - } - - @Test - fun `size of list with five elements is 5`() { - val list = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("e"), Empty))))) - - assertEquals(5, list.size.value, "Expected size of list with five elements to be 5") - } - - @Test - fun `member(a, list of a)`() { - val atom = Atom("a") - val list = Cons(atom, Empty) - - val member = Member(atom, list) - - val result = member.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - } - - @Test - fun `member should only check shallow`() { - val list = Cons(Atom("a"), Cons(Cons(Atom("b"), Empty), Empty)) - - var result = Member(Atom("a"), list).satisfy(emptyMap()).toList() - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - result = Member(Atom("b"), list).satisfy(emptyMap()).toList() - assertEquals(0, result.size, "Expected no solution") - } - - @Test - fun `member with variable in list`() { - val atom = Atom("a") - val variable = Variable("X") - val list = Cons(variable, Empty) - - val member = Member(atom, list) - - val result = member.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom") - } - - @Disabled("Not implemented yet") - @Test - fun `appended empty lists is an empty list`() { - val append = Append(Empty, Empty, Empty) - - val result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - } - - @Disabled("Not implemented yet") - @Test - fun `appending two empty lists gives an empty list`() { - val list1 = Empty - val list2 = Empty - val list12 = Variable("Result") - - val append = Append(list1, list2, list12) - - val result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list12], "Expected result to be empty list") - } - - @Disabled("Not implemented yet") - @Test - fun `appending an empty list to another list gives that list`() { - val nonempty = Cons(Atom("a"), Empty) - - var append = Append(nonempty, Empty, Empty) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - append = Append(Empty, nonempty, Empty) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - val variable = Variable("List1AndList2") - - append = Append(Empty, nonempty, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(nonempty, subs[variable], "Expected result to be nonempty list") - - append = Append(nonempty, Empty, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - } - - @Disabled("Not implemented yet") - @Test - fun `appending two lists gives combined list`() { - val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty)) - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - val list4 = Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("a"), Cons(Atom("b"), Empty)))) - - var append = Append(list1, list2, list3) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - val variable = Variable("List1AndList2") - - append = Append(list1, list2, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(list3, subs[variable], "Expected result to be combined list") - - append = Append(list2, list1, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(list4, subs[variable], "Expected result to be combined list") - } - - @Disabled("Not implemented yet") - @Test - fun `you can find the appended list`() { - val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - val list2: Term = Variable("List2") - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - - var append = Append(list1, list2, list1) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list2], "Expected result to be empty list") - - append = Append(list1, list2, list3) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Cons(Atom("c"), Cons(Atom("d"), Empty)), subs[list2], "Expected result to be list with c and d") - } - - @Disabled("Not implemented yet") - @Test - fun `you can find the prepended list`() { - val list1 = Variable("List1") - val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty)) - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - - var append = Append(list1, list2, list2) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list1], "Expected result to be empty list") - - append = Append(list1, list2, list3) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Cons(Atom("a"), Cons(Atom("b"), Empty)), subs[list1], "Expected result to be list with a and b") - } -} \ No newline at end of file diff --git a/tests/prolog/builtins/MetaOperatorsTests.kt b/tests/prolog/builtins/MetaOperatorsTests.kt deleted file mode 100644 index aeb642c..0000000 --- a/tests/prolog/builtins/MetaOperatorsTests.kt +++ /dev/null @@ -1,34 +0,0 @@ -package prolog.builtins - -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue -import org.junit.jupiter.api.Test -import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List.Cons -import prolog.ast.lists.List.Empty -import prolog.ast.terms.Variable - -class MetaOperatorsTests { - @Test - fun `ignore of failing goal succeeds`() { - val goal = Member(Integer(4), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty)))) - - val result = Ignore(goal).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Should return one result") - assertTrue(result[0].isSuccess, "Result should be successful") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `ignore of succeeding goal returns first solution`() { - val goal = Member(Variable("X"), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty)))) - - val result = Ignore(goal).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Should return one result") - assertTrue(result[0].isSuccess, "Result should be successful") - val subs = result[0].getOrNull()!! - assertEquals(Integer(1), subs[Variable("X")], "Expected first solution to be 1") - } -} \ No newline at end of file diff --git a/tests/prolog/builtins/OtherOperatorsTests.kt b/tests/prolog/builtins/OtherOperatorsTests.kt deleted file mode 100644 index e9341d6..0000000 --- a/tests/prolog/builtins/OtherOperatorsTests.kt +++ /dev/null @@ -1,54 +0,0 @@ -package prolog.builtins - -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue -import org.junit.jupiter.api.Test -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.logic.Rule -import prolog.ast.terms.Atom -import prolog.ast.terms.CompoundTerm -import prolog.ast.terms.Variable -import java.io.ByteArrayOutputStream -import java.io.PrintStream - -class OtherOperatorsTests { - @Test - fun `forall(X is 1, X == 1)`() { - val forall = ForAll(Is(Variable("X"), Integer(1)), EvaluatesTo(Variable("X"), Integer(1))) - - val result = forall.satisfy(emptyMap()).toList() - - assertEquals(1, result.size) - } - - /** - * @see [Forall instead of failure-driven loops](https://riptutorial.com/prolog/example/19554/forall-instead-of-failure-driven-loops#example) - */ - @Test - fun `forall printer`() { - val printer = Rule( - CompoundTerm(Atom("print"), listOf(Variable("X"))), - ForAll( - Between(Integer(1), Variable("X"), Variable("Y")), - Write(Variable("Y")) - ) - ) - Program.load(listOf(printer)) - - // Set output - val outStream = ByteArrayOutputStream() - System.setOut(PrintStream(outStream)) - - var expected = "" - for (i in 1..5) { - val result = CompoundTerm(Atom("print"), listOf(Integer(i))).satisfy(emptyMap()).toList() - assertEquals(1, result.size) - assertTrue(result[0].isSuccess) - - expected += "$i" - assertEquals(expected, outStream.toString()) - outStream.reset() - } - } -} diff --git a/tests/prolog/logic/TermAnalysisConstructionTest.kt b/tests/prolog/builtins/TermAnalysisConstructionTest.kt similarity index 65% rename from tests/prolog/logic/TermAnalysisConstructionTest.kt rename to tests/prolog/builtins/TermAnalysisConstructionTest.kt index 7000a49..a137fca 100644 --- a/tests/prolog/logic/TermAnalysisConstructionTest.kt +++ b/tests/prolog/builtins/TermAnalysisConstructionTest.kt @@ -1,10 +1,13 @@ -package prolog.logic +package prolog.builtins -import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test import prolog.ast.terms.Atom -import prolog.ast.terms.Functor import prolog.ast.terms.Structure +import prolog.logic.atomic +import prolog.logic.compound +import prolog.logic.functor /** * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png) @@ -19,12 +22,12 @@ class TermAnalysisConstructionTest { assertTrue(atomic(atom)) assertFalse(compound(atom)) - assertEquals(Functor("foo", 0), atom.functor) + assertTrue(functor(atom, Atom("foo"), 0)) } @Test fun compound_arity_0_properties() { - val structure = Structure("foo") + val structure = Structure(Atom("foo"), emptyList()) assertFalse(atomic(structure)) assertTrue(compound(structure)) @@ -32,11 +35,11 @@ class TermAnalysisConstructionTest { @Test fun compound_arity_1_properties() { - val structure = Structure("foo", Atom("bar")) + val structure = Structure(Atom("foo"), listOf(Atom("bar"))) assertFalse(atomic(structure)) assertTrue(compound(structure)) - assertEquals(Functor("foo", 1), structure.functor) + assertTrue(functor(structure, Atom("foo"), 1)) } } \ No newline at end of file diff --git a/tests/prolog/logic/UnificationTests.kt b/tests/prolog/logic/UnificationTests.kt index 1324a12..10a37e7 100644 --- a/tests/prolog/logic/UnificationTests.kt +++ b/tests/prolog/logic/UnificationTests.kt @@ -10,16 +10,13 @@ import prolog.ast.terms.Variable import prolog.builtins.Add import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Nested -import prolog.ast.lists.List -import prolog.ast.lists.List.Empty -import prolog.ast.lists.List.Cons /* * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms */ class UnificationTests { @Nested - class `unify logic` { + class `unify` { @Test fun identical_atoms_unify() { val atom1 = Atom("a") @@ -333,7 +330,7 @@ class UnificationTests { } @Nested - class `applySubstitution logic` { + class `applySubstitution` { @Test fun `apply substitution without sub`() { val term = Variable("X") @@ -370,120 +367,4 @@ class UnificationTests { assertEquals(Integer(35), result) } } - - @Nested - class `equivalent logic` { - @Test - fun `empty lists are equivalent`() { - var eq = equivalent(Empty, Empty, emptyMap()) - assertTrue(eq, "Empty lists should be equivalent") - - val variable = Variable("X") - - eq = equivalent(Empty, variable, mapOf(variable to Empty)) - assertTrue(eq, "Empty list and variable should be equivalent") - - eq = equivalent(variable, Empty, mapOf(variable to Empty)) - assertTrue(eq, "Variable and empty list should be equivalent") - } - - @Test - fun `singletons are equivalent`() { - val atom = Atom("a") - val list1 = Cons(atom, Empty) - val list2 = Cons(atom, Empty) - - var eq = equivalent(list1, list2, emptyMap()) - assertTrue(eq, "Singleton lists should be equivalent") - - val variable = Variable("X") - - eq = equivalent(list1, variable, mapOf(variable to list2)) - assertTrue(eq, "Singleton list and variable should be equivalent") - - eq = equivalent(variable, list1, mapOf(variable to list2)) - assertTrue(eq, "Variable and singleton list should be equivalent") - } - - @Test - fun `singleton and empty list are not equivalent`() { - val atom = Atom("a") - val list1 = Cons(atom, Empty) - val list2 = Empty - - var eq = equivalent(list1, list2, emptyMap()) - assertFalse(eq, "Singleton and empty lists should not be equivalent") - - eq = equivalent(list2, list1, emptyMap()) - assertFalse(eq, "Empty and singleton lists should not be equivalent") - - val variable = Variable("X") - - eq = equivalent(list1, variable, mapOf(variable to list2)) - assertFalse(eq, "Singleton list and variable should not be equivalent") - - eq = equivalent(variable, list1, mapOf(variable to list2)) - assertFalse(eq, "Variable and singleton list should not be equivalent") - } - - @Test - fun `identical lists are equivalent`() { - val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - val list2 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - - var eq = equivalent(list1, list2, emptyMap()) - assertTrue(eq, "Identical lists should be equivalent") - - eq = equivalent(list2, list1, emptyMap()) - assertTrue(eq, "Identical lists should be equivalent") - - val variable = Variable("X") - - eq = equivalent(list1, variable, mapOf(variable to list2)) - assertTrue(eq, "Identical lists should be equivalent") - - eq = equivalent(variable, list2, mapOf(variable to list1)) - assertTrue(eq, "Identical lists should be equivalent") - } - - @Test - fun `identical nested lists are equivalent`() { - val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty))) - val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty))) - - var eq = equivalent(list1, list2, emptyMap()) - assertTrue(eq, "Identical nested lists should be equivalent") - - eq = equivalent(list2, list1, emptyMap()) - assertTrue(eq, "Identical nested lists should be equivalent") - - val variable = Variable("X") - - eq = equivalent(list1, variable, mapOf(variable to list2)) - assertTrue(eq, "Identical nested lists should be equivalent") - - eq = equivalent(variable, list2, mapOf(variable to list1)) - assertTrue(eq, "Identical nested lists should be equivalent") - } - - @Test - fun `lists with different nests are not equivalent`() { - val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("bar"), Cons(Atom("baz"), Empty)), Empty))) - val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty))) - - var eq = equivalent(list1, list2, emptyMap()) - assertFalse(eq, "Lists with different nests should not be equivalent") - - eq = equivalent(list2, list1, emptyMap()) - assertFalse(eq, "Lists with different nests should not be equivalent") - - val variable = Variable("X") - - eq = equivalent(list1, variable, mapOf(variable to list2)) - assertFalse(eq, "Lists with different nests should not be equivalent") - - eq = equivalent(variable, list2, mapOf(variable to list1)) - assertFalse(eq, "Lists with different nests should not be equivalent") - } - } } \ No newline at end of file