diff --git a/documentatie/9781292153971.bib b/documentatie/9781292153971.bib new file mode 100644 index 0000000..fa401bc --- /dev/null +++ b/documentatie/9781292153971.bib @@ -0,0 +1,11 @@ +@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 49c1846..346708d 100644 --- a/documentatie/verslag.tex +++ b/documentatie/verslag.tex @@ -1,17 +1,230 @@ %! Author = tdpeuter %! Date = 27/03/2025 -% Preamble -\documentclass[11pt]{article} +\documentclass[11pt,a4paper]{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 - % Lexer op basis van https://craftinginterpreters.com/scanning.html + \section{Inleiding}\label{sec:inleiding} + % Uitvoeren van testen ref appendix + \section{Architectuur}\label{sec:architectuur} -\end{document} \ No newline at end of file + % 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} diff --git a/examples/basics/backtracking.pl b/examples/basics/backtracking.pl index 167f037..820bd4f 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(X, s(s(s(0)))), - write(X), nl, + leq(A, s(s(s(0)))), + write(A), nl, fail. diff --git a/examples/meta/continuations.pl b/examples/meta/continuations.pl new file mode 100644 index 0000000..8661361 --- /dev/null +++ b/examples/meta/continuations.pl @@ -0,0 +1,22 @@ +% 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 new file mode 100644 index 0000000..47003d5 --- /dev/null +++ b/examples/meta/mib_voorbeelden.pl @@ -0,0 +1,48 @@ +% 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 6c17705..fb72dcf 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -48,67 +48,99 @@ 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 Structure -> { + is Atom, is Structure -> { // Preprocess the arguments first to recognize builtins - val args = term.arguments.map { preprocess(it, nested = true) } + val args = if (term is Structure) { + term.arguments.map { preprocess(it, nested = true) } + } else emptyList() - 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) + 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]) // 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 - 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) + 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) // Database - term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name) - term.functor == "retract/1" -> Retract(args[0]) - term.functor == "assert/1" -> { + 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") -> { if (args[0] is Rule) { Assert(args[0] as Rule) } else { Assert(Fact(args[0] as Head)) } } - term.functor == "asserta/1" -> { + + Functor.of("asserta/1") -> { if (args[0] is Rule) { AssertA(args[0] as Rule) } else { AssertA(Fact(args[0] as Head)) } } - term.functor == "assertz/1" -> { + + Functor.of("assertz/1") -> { if (args[0] is Rule) { AssertZ(args[0] as Rule) } else { @@ -116,13 +148,48 @@ 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 - term.functor == "write/1" -> Write(args[0]) - term.functor == "read/1" -> Read(args[0]) - term.functor == "initialization/1" -> Initialization(args[0] as Goal) + 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) else -> { - term.arguments = args + if (term is Structure) term.arguments = args term } } @@ -138,4 +205,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 c5706a1..f12deb7 100644 --- a/src/io/IoHandler.kt +++ b/src/io/IoHandler.kt @@ -3,7 +3,8 @@ package io interface IoHandler { fun prompt( message: String, - hint: () -> String = { "Please enter a valid input." } + hint: () -> String = { "Please enter a valid input." }, + check: (String) -> Boolean = { true } ): String fun say(message: String) diff --git a/src/io/Terminal.kt b/src/io/Terminal.kt index 1b9df94..d20c8e8 100644 --- a/src/io/Terminal.kt +++ b/src/io/Terminal.kt @@ -20,15 +20,16 @@ class Terminal( override fun prompt( message: String, - hint: () -> String + hint: () -> String, + check: (String) -> Boolean, ): String { say("$message ") - var input: String = readLine() - while (input.isBlank()) { + var input: String = readLine().trim() + while (!check(input)) { say(hint(), error) - input = readLine() + input += readLine().trim() } - return input + return input.trim() } override fun say(message: String) { diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 3fb9e48..9051484 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -3,10 +3,14 @@ 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: @@ -65,6 +69,7 @@ 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 @@ -87,19 +92,24 @@ open class TermsGrammar : Tokens() { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } - protected val op700: Parser by (equivalent or equals or notEquals or isOp) use { text } + protected val op700: Parser by (univOp or equivalent or notEquivalent 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 (term700 * zeroOrMore(op1000 * term700)) use { - t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } + protected val term1000: Parser by (term900 * zeroOrMore(op1000 * term900)) use { + constructRightAssociative(t1, t2) } protected val op1100: Parser by (semicolon) use { text } protected val term1100: Parser by (term1000 * zeroOrMore(op1100 * term1000)) use { - t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } + constructRightAssociative(t1, t2) } protected val dynamic: Parser by (dynamicOp * functor) use { @@ -112,6 +122,20 @@ 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 @@ -121,4 +145,12 @@ 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 ac8c36f..ccdbae9 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -10,6 +10,8 @@ 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(":-") @@ -19,7 +21,11 @@ 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 be2da7a..b309883 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 != "/_" } + predicates.filter { it.key != Functor.of("/_") } .forEach { (_, predicate) -> db.load(predicate, force = true) } } Logger.info("Initializing database from $sourceFile") - if (predicates.contains("/_")) { + if (predicates.contains(Functor.of("/_"))) { Logger.debug("Loading clauses from /_ predicate") - predicates["/_"]?.clauses?.forEach { + predicates[Functor.of("/_")]?.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 61550a9..d87c6e8 100644 --- a/src/prolog/ast/arithmetic/ArithmeticOperator.kt +++ b/src/prolog/ast/arithmetic/ArithmeticOperator.kt @@ -4,4 +4,7 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Operator abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) : - Operator(symbol, leftOperand, rightOperand), Expression + Operator(symbol, leftOperand, rightOperand), Expression { + constructor(symbol: String, leftOperand: Expression, rightOperand: Expression) : + this(Atom(symbol), leftOperand, rightOperand) +} diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt index da49530..a787cb2 100644 --- a/src/prolog/ast/arithmetic/Float.kt +++ b/src/prolog/ast/arithmetic/Float.kt @@ -32,6 +32,8 @@ 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 diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt index dbf9c39..c12cfcd 100644 --- a/src/prolog/ast/arithmetic/Integer.kt +++ b/src/prolog/ast/arithmetic/Integer.kt @@ -33,6 +33,7 @@ data class Integer(override val value: Int) : Number, LogicOperand() { Float(value / other.value.toFloat()) } } + else -> throw IllegalArgumentException("Cannot divide $this and $other") } @@ -41,4 +42,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() { is Integer -> Integer(value * other.value) else -> throw IllegalArgumentException("Cannot multiply $this and $other") } + + override fun applySubstitution(subs: Substitutions): Integer = this } diff --git a/src/prolog/ast/lists/List.kt b/src/prolog/ast/lists/List.kt new file mode 100644 index 0000000..cd5ee80 --- /dev/null +++ b/src/prolog/ast/lists/List.kt @@ -0,0 +1,65 @@ +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 2abfa77..dc1c0c4 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.ast.Database.Program import prolog.Substitutions +import prolog.ast.Database.Program import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut @@ -29,32 +29,36 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { // Since we are only interested in substitutions in the goal (as opposed to the head of this clause), // we can use variable renaming and filter out the substitutions that are not in the goal. - val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs) + val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, emptyMap()) + Program.variableRenamingStart = headEnd - val reverse = renamed.entries.associate { (a, b) -> b to a } - Program.variableRenamingStart = end - - var newSubs: Substitutions = subs + renamed - unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer -> - headAnswer.map { headSubs -> - // If the body can be proven, yield the (combined) substitutions - newSubs = subs + renamed + headSubs + 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 -> bodyAnswer.fold( onSuccess = { bodySubs -> - var result = (headSubs + bodySubs) - .mapKeys { applySubstitution(it.key, reverse)} - .mapValues { applySubstitution(it.value, reverse) } - result = result.map { it.key to applySubstitution(it.value, result) } - .toMap() - .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())} - yield(Result.success(result)) + // 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)) }, onFailure = { error -> if (error is AppliedCut) { // Find single solution and return immediately if (error.subs != null) { - yield(Result.failure(AppliedCut(headSubs + error.subs))) + 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))) } else { yield(Result.failure(AppliedCut())) } @@ -81,7 +85,5 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { return true } - override fun hashCode(): Int { - return super.hashCode() - } + override fun hashCode(): Int = super.hashCode() } diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt index a52990e..b6cc83d 100644 --- a/src/prolog/ast/logic/Fact.kt +++ b/src/prolog/ast/logic/Fact.kt @@ -1,6 +1,10 @@ package prolog.ast.logic +import prolog.Substitutions import prolog.ast.terms.Head import prolog.builtins.True +import prolog.logic.applySubstitution -class Fact(head: Head) : Clause(head, True) \ No newline at end of file +class Fact(head: Head) : Clause(head, True) { + override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head) +} diff --git a/src/prolog/ast/logic/LogicOperator.kt b/src/prolog/ast/logic/LogicOperator.kt index 5353f0d..8fb488f 100644 --- a/src/prolog/ast/logic/LogicOperator.kt +++ b/src/prolog/ast/logic/LogicOperator.kt @@ -10,5 +10,8 @@ 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 9eba36e..26148a3 100644 --- a/src/prolog/ast/logic/Rule.kt +++ b/src/prolog/ast/logic/Rule.kt @@ -1,6 +1,13 @@ package prolog.ast.logic +import prolog.Substitutions import prolog.ast.terms.Body import prolog.ast.terms.Head +import prolog.logic.applySubstitution -class Rule(head: Head, body: Body) : Clause(head, body) \ No newline at end of file +class Rule(head: Head, body: Body) : Clause(head, body) { + override fun applySubstitution(subs: Substitutions): Rule = Rule( + head = applySubstitution(head, 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 1bc0633..abb751c 100644 --- a/src/prolog/ast/terms/AnonymousVariable.kt +++ b/src/prolog/ast/terms/AnonymousVariable.kt @@ -1,8 +1,9 @@ package prolog.ast.terms import io.Logger +import prolog.Substitutions -class AnonymousVariable(id: Int) : Variable("_$id") { +class AnonymousVariable(private val id: Int) : Variable("_$id") { companion object { private var counter = 0 fun create(): AnonymousVariable { @@ -13,5 +14,7 @@ class AnonymousVariable(id: Int) : Variable("_$id") { } } + override fun applySubstitution(subs: Substitutions): AnonymousVariable = this + override fun toString(): String = "_" } \ No newline at end of file diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index 3a6afad..42c12c5 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -4,12 +4,15 @@ 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 = "$name/_" + override val functor: Functor = Functor(this, Integer(0)) 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 } diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index dc61c7d..989c4d9 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 : Satisfiable \ No newline at end of file +interface Body : Term, Satisfiable diff --git a/src/prolog/ast/terms/Functor.kt b/src/prolog/ast/terms/Functor.kt new file mode 100644 index 0000000..b7a4cc3 --- /dev/null +++ b/src/prolog/ast/terms/Functor.kt @@ -0,0 +1,37 @@ +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 95f9016..4f98585 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.ast.Database.Program import prolog.Substitutions +import prolog.ast.Database.Program import prolog.ast.logic.LogicOperand /** diff --git a/src/prolog/ast/terms/Head.kt b/src/prolog/ast/terms/Head.kt index 71b4e8a..fe5048d 100644 --- a/src/prolog/ast/terms/Head.kt +++ b/src/prolog/ast/terms/Head.kt @@ -6,5 +6,3 @@ 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 cf43b24..136c423 100644 --- a/src/prolog/ast/terms/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -7,6 +7,9 @@ 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 385da2c..162dc61 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -3,14 +3,18 @@ package prolog.ast.terms import prolog.Answers 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 { - override val functor: Functor = "${name.name}/${arguments.size}" + constructor(name: String, vararg arguments: Argument) : this(Atom(name), arguments.asList()) + + override val functor: Functor = Functor(name, Integer(arguments.size)) override fun solve(goal: Goal, subs: Substitutions): Answers { return unifyLazy(goal, this, subs) @@ -19,10 +23,15 @@ 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 diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 0fdad49..8e46626 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -1,14 +1,18 @@ package prolog.ast.terms +import prolog.Substitutions +import prolog.ast.arithmetic.Float +import prolog.ast.arithmetic.Integer import prolog.logic.compare /** * Value in Prolog. * - * A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer], - * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm]. + * A [Term] is either a [Variable], [Atom], [Integer], + * [Float] or [CompoundTerm]. * In addition, SWI-Prolog also defines the type TODO string. */ interface Term : Comparable { 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 2d23170..bcfee5c 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -34,6 +34,8 @@ 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() } diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt new file mode 100644 index 0000000..7f83ab0 --- /dev/null +++ b/src/prolog/builtins/analysisOperators.kt @@ -0,0 +1,250 @@ +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 306337e..dbdccf4 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(Atom("=\\="), left, right), Satisfiable { + Operator("=\\=", left, right), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -39,13 +39,17 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr } } + override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent( + left.applySubstitution(subs) as Expression, + right.applySubstitution(subs) as Expression + ) } /** * True if Expr1 evaluates to a number equal to Expr2. */ class EvaluatesTo(private val left: Expression, private val right: Expression) : - Operator(Atom("=:="), left, right) { + Operator("=:=", left, right) { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -57,13 +61,18 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) : return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence() } + + override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo( + left.applySubstitution(subs) as Expression, + right.applySubstitution(subs) as Expression + ) } /** * True when Number is the value to which Expr evaluates. */ class Is(val number: Expression, val expr: Expression) : - Operator(Atom("is"), number, expr), Satisfiable { + Operator("is", number, expr), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = number.simplify(subs) val t2 = expr.simplify(subs) @@ -78,6 +87,11 @@ class Is(val number: Expression, val expr: Expression) : return unifyLazy(t1.to, t2.to, subs) } + + override fun applySubstitution(subs: Substitutions): Is = Is( + number.applySubstitution(subs) as Expression, + expr.applySubstitution(subs) as Expression + ) } /** @@ -94,49 +108,74 @@ class Positive(operand: Expression) : Add(Integer(0), operand) * Result = Expr1 + Expr2 */ open class Add(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator(Atom("+"), expr1, expr2) { + ArithmeticOperator("+", expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr1, expr2, result, subs) val simplification = result.simplify(map.first().getOrThrow()) return Simplification(this, simplification.to) } + + override fun applySubstitution(subs: Substitutions): Add = Add( + expr1.applySubstitution(subs) as Expression, + expr2.applySubstitution(subs) as 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(Atom("-"), expr1, expr2) { + ArithmeticOperator("-", expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr2, result, expr1, subs) val simplification = result.simplify(map.first().getOrThrow()) return Simplification(this, simplification.to) } + + override fun applySubstitution(subs: Substitutions): Subtract = Subtract( + expr1.applySubstitution(subs) as Expression, + expr2.applySubstitution(subs) as Expression + ) } /** * Result = Expr1 * Expr2 */ class Multiply(val expr1: Expression, val expr2: Expression) : - ArithmeticOperator(Atom("*"), expr1, expr2) { + ArithmeticOperator("*", expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = mul(expr1, expr2, result, subs) val simplification = result.simplify(map.first().getOrThrow()) return Simplification(this, simplification.to) } + + override fun applySubstitution(subs: Substitutions): Multiply = Multiply( + expr1.applySubstitution(subs) as Expression, + expr2.applySubstitution(subs) as Expression + ) } class Divide(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator(Atom("/"), expr1, expr2) { + ArithmeticOperator("/", expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = div(expr1, expr2, result, subs) val simplification = result.simplify(map.first().getOrThrow()) return Simplification(this, simplification.to) } + + override fun applySubstitution(subs: Substitutions): Divide = Divide( + expr1.applySubstitution(subs) as Expression, + expr2.applySubstitution(subs) as Expression + ) } // TODO Expr mod Expr @@ -144,7 +183,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(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable { + CompoundTerm("between", expr1, expr2, expr3), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val e1 = expr1.simplify(subs) val e2 = expr2.simplify(subs) @@ -166,5 +205,16 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv } } + override fun applySubstitution(subs: Substitutions): Between = Between( + expr1.applySubstitution(subs) as Expression, + expr2.applySubstitution(subs) as Expression, + expr3.applySubstitution(subs) as Expression + ) + 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 613c915..3d81786 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -2,18 +2,23 @@ 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.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 } /** @@ -26,6 +31,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 } // TODO Repeat/0 @@ -34,77 +40,112 @@ class Cut() : Atom("!") { override fun satisfy(subs: Substitutions): Answers { return sequenceOf(Result.failure(AppliedCut(emptyMap()))) } + + override fun applySubstitution(subs: Substitutions): Cut = this } /** * Conjunction (and). True if both Goal1 and Goal2 are true. */ -class Conjunction(val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(Atom(","), left, right) { +open class Conjunction(val left: LogicOperand, private val right: LogicOperand) : + LogicOperator(",", 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 -> - 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)) - } - ) - } - }, + onSuccess = { leftSubs -> yieldAll(satisfyRight(leftSubs)) }, // If it fails, check these conditions: onFailure = { exception -> - // 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)) + 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)) } - ) ?: yield(Result.failure(AppliedCut())) - } else { - // 2. Any other failure should be returned as is - yield(Result.failure(exception)) + } + + // 3. Any other failure should be returned as is + else -> yield(Result.failure(exception)) } } ) } } + + override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction( + applySubstitution(left, subs) as LogicOperand, + applySubstitution(right, subs) as LogicOperand + ) } /** * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(Atom(";"), left, right) { + LogicOperator(";", left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { - yieldAll(left.satisfy(subs)) + 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(right.satisfy(subs)) } + + override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction( + applySubstitution(left, subs) as LogicOperand, + applySubstitution(right, subs) as LogicOperand + ) } @Deprecated("Use Disjunction instead") @@ -117,7 +158,7 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l /** * True if 'Goal' cannot be proven. */ -class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) { +open class Not(private val goal: Goal) : LogicOperator("\\+", rightOperand = goal) { override fun satisfy(subs: Substitutions): Answers { // If the goal can be proven, return an empty sequence val goalResults = goal.satisfy(subs).iterator() @@ -127,4 +168,6 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go // If the goal cannot be proven, return a sequence with an empty map return sequenceOf(Result.success(emptyMap())) } + + override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal) } diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index eaf67b8..922201f 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -1,27 +1,23 @@ package prolog.builtins +import io.Logger import prolog.Answers import prolog.Substitutions -import prolog.ast.logic.Clause -import prolog.ast.terms.Atom -import prolog.ast.terms.Structure -import prolog.ast.logic.Predicate -import prolog.ast.Database.Program -import prolog.ast.terms.Functor -import prolog.ast.terms.Term -import prolog.ast.logic.Fact import prolog.ast.Database -import prolog.ast.terms.Body -import prolog.ast.terms.Goal -import prolog.ast.terms.Operator +import prolog.ast.Database.Program +import prolog.ast.arithmetic.Integer +import prolog.ast.logic.Clause +import prolog.ast.logic.Fact +import prolog.ast.logic.Predicate +import prolog.ast.terms.* import prolog.logic.applySubstitution import prolog.logic.unifyLazy /** * (Make) the [Predicate] with the corresponding [Functor] dynamic. */ -class Dynamic(private val dynamicFunctor: Functor): Goal(), Body { - override val functor: Functor = "dynamic/1" +class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body { + override val functor = Functor(Atom("dynamic"), Integer(1)) override fun satisfy(subs: Substitutions): Answers { val predicate = Program.db.predicates[dynamicFunctor] @@ -42,16 +38,18 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body { } override fun hashCode(): Int = super.hashCode() + + override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor) } class Assert(clause: Clause) : AssertZ(clause) { - override val functor: Functor = "assert/1" + override val functor = Functor(Atom("assert"), Integer(1)) } /** * Assert a [Clause] as a first clause of the [Predicate] into the [Program]. */ -class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) { +class AssertA(val clause: Clause) : Operator("asserta", rightOperand = clause) { override fun satisfy(subs: Substitutions): Answers { // Add clause to the program val evaluatedClause = applySubstitution(clause, subs) as Clause @@ -59,12 +57,14 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) { return sequenceOf(Result.success(emptyMap())) } + + override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause) } /** * Assert a [Clause] as a last clause of the [Predicate] into the [Program]. */ -open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) { +open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clause) { override fun satisfy(subs: Substitutions): Answers { // Add clause to the program val evaluatedClause = applySubstitution(clause, subs) as Clause @@ -72,6 +72,8 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) return sequenceOf(Result.success(emptyMap())) } + + override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause) } /** @@ -80,7 +82,7 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) * * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1) */ -class Retract(val term: Term) : Operator(Atom("retract"), null, term) { +open class Retract(val term: Term) : Operator("retract", rightOperand = term) { override fun satisfy(subs: Substitutions): Answers = sequence { // Check that term is a structure or atom if (term !is Structure && term !is Atom) { @@ -95,6 +97,12 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, 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( @@ -110,4 +118,32 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, 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 new file mode 100644 index 0000000..43f6e22 --- /dev/null +++ b/src/prolog/builtins/delimitedContinuationsOperators.kt @@ -0,0 +1,74 @@ +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 1271296..e841679 100644 --- a/src/prolog/builtins/ioOperators.kt +++ b/src/prolog/builtins/ioOperators.kt @@ -16,7 +16,9 @@ import prolog.logic.unifyLazy /** * Write [Term] to the current output, using brackets and operators where appropriate. */ -class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable { +class Write(private val term: Term) : Operator("write", rightOperand = term), Satisfiable { + constructor(message: String) : this(Atom(message)) + override fun satisfy(subs: Substitutions): Answers { val t = applySubstitution(term, subs) @@ -27,6 +29,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis return sequenceOf(Result.success(emptyMap())) } + override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs)) + override fun toString(): String = "write($term)" } @@ -39,6 +43,14 @@ object Nl : Atom("nl"), Satisfiable { Program.storeNewLine = false return sequenceOf(Result.success(emptyMap())) } + + 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)" } /** @@ -72,4 +84,6 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi yieldAll(unifyLazy(t1, t2, subs)) } + + override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs)) } diff --git a/src/prolog/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt new file mode 100644 index 0000000..9835c44 --- /dev/null +++ b/src/prolog/builtins/listOperators.kt @@ -0,0 +1,78 @@ +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 new file mode 100644 index 0000000..0f002f3 --- /dev/null +++ b/src/prolog/builtins/loadingSourceOperators.kt @@ -0,0 +1,39 @@ +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 new file mode 100644 index 0000000..3abbabb --- /dev/null +++ b/src/prolog/builtins/metaOperators.kt @@ -0,0 +1,51 @@ +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 4cc582f..88170fb 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -3,14 +3,21 @@ 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 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) { +class Query(val query: LogicOperand) : LogicOperator("?-", rightOperand = 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 892c616..c00175d 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -7,7 +7,6 @@ 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 @@ -17,27 +16,40 @@ import prolog.logic.unifyLazy /** * Unify Term1 with Term2. True if the unification succeeds. */ -class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="), term1, term2) { +class Unify(private val term1: Term, private val term2: Term): Operator("=", term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - yieldAll(unifyLazy(t1, t2, subs)) + yieldAll(unifyLazy(t1, t2, emptyMap())) } + + override fun applySubstitution(subs: Substitutions): Unify = Unify( + applySubstitution(term1, subs), + applySubstitution(term2, subs) + ) } -class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) { - private val not = Not(Unify(term1, term2)) - override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs) +class NotUnify(private val term1: Term, private val term2: Term) : Not(Unify(term1, term2)) { + override fun toString(): String = "($term1 \\= $term2)" } -class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) { +class Equivalent(private val term1: Term, private val term2: Term) : Operator("==", term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - if (equivalent(t1, t2, subs)) { + if (equivalent(t1, t2, emptyMap())) { yield(Result.success(emptyMap())) } } + + override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent( + applySubstitution(term1, subs), + 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 new file mode 100644 index 0000000..fc87091 --- /dev/null +++ b/src/prolog/builtins/verificationOperators.kt @@ -0,0 +1,52 @@ +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 new file mode 100644 index 0000000..a96b55d --- /dev/null +++ b/src/prolog/flags/AppliedShift.kt @@ -0,0 +1,14 @@ +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 8c2b26f..459d58d 100644 --- a/src/prolog/logic/terms.kt +++ b/src/prolog/logic/terms.kt @@ -1,29 +1,10 @@ package prolog.logic import prolog.Substitutions -import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Term import prolog.ast.terms.Variable -/** - * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose - * 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 1e7b57f..1ac842b 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -7,45 +7,33 @@ import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer import prolog.ast.arithmetic.Number -import prolog.ast.logic.Clause +import prolog.ast.lists.List.Cons +import prolog.ast.lists.List.Empty 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 { - term is Fact -> { - Fact(applySubstitution(term.head, subs) as Head) - } + term is Fact -> term.applySubstitution(subs) variable(term, emptyMap()) -> { val variable = term as Variable subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term } + atomic(term, subs) -> term - compound(term, subs) -> { - val structure = term as Structure - Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) }) - } + compound(term, subs) -> term.applySubstitution(subs) else -> term } -//TODO Combine with the other applySubstitution function -fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when { - variable(expr, 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 +fun applySubstitution(expr: Expression, subs: Substitutions): Expression { + return applySubstitution(expr as Term, subs) as Expression } // Check if a variable occurs in a term -fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when { +fun occurs(variable: Variable, term: Term, subs: Substitutions = emptyMap()): Boolean = when { variable(term, subs) -> term == variable atomic(term, subs) -> false compound(term, subs) -> { @@ -62,7 +50,10 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val t2 = applySubstitution(term2, subs) when { - equivalent(t1, t2, subs) -> yield(Result.success(emptyMap())) + equivalent(t1, t2, subs) -> { + yield(Result.success(emptyMap())) + } + variable(t1, subs) -> { val variable = t1 as Variable if (!occurs(variable, t2, subs)) { @@ -85,18 +76,32 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val args1 = structure1.arguments val args2 = structure2.arguments if (args1.size == args2.size) { - 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() + 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)) + } } - }.map { Result.success(it) } + } } - yieldAll(combinedResults) } } } @@ -105,6 +110,32 @@ 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()) { @@ -120,12 +151,32 @@ 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 -> 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 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 5e8b0d4..688cea4 100644 --- a/src/repl/Repl.kt +++ b/src/repl/Repl.kt @@ -6,6 +6,7 @@ import io.Terminal import parser.ReplParser import prolog.Answer import prolog.Answers +import prolog.flags.AppliedCut class Repl { private val io = Terminal() @@ -29,40 +30,52 @@ class Repl { } private fun query(): Answers { - val queryString = io.prompt("?-", { "| " }) + val queryString = io.prompt("?-", { "| " }, { it.endsWith(".") }) val simpleQuery = parser.parse(queryString) val query = preprocessor.preprocess(simpleQuery) return query.satisfy(emptyMap()) } private fun printAnswers(answers: Answers) { - val knownCommands = setOf(";", "a", ".", "h") - val iterator = answers.iterator() if (!iterator.hasNext()) { io.say("false.\n") - } else { - io.say(prettyPrint(iterator.next())) + return + } - while (iterator.hasNext()) { - var command = io.prompt("") + io.say(prettyPrint(iterator.next())) - while (command !in knownCommands) { - io.say("Unknown action: $command (h for help)\n") - command = io.prompt("Action?") + while (true) { + when (io.prompt("")) { + ";" -> { + try { + io.say(prettyPrint(iterator.next())) + } catch (_: NoSuchElementException) { + break + } } - when (command) { - ";" -> { - io.say(prettyPrint(iterator.next())) - } - "a" -> return - "." -> return - "h" -> { - help() - io.say("Action?") - } + "" -> { + 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?") } } } @@ -89,10 +102,15 @@ class Repl { } return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" } }, - onFailure = { - val text = "Failure: ${it.message}" - Logger.warn(text) - return text + onFailure = { failure -> + if (failure is AppliedCut) { + if (failure.subs != null) { + return prettyPrint(Result.success(failure.subs)) + } + return "false." + } + + return "ERROR: ${failure.message}" } ) } diff --git a/src/tool/mapEach.kt b/src/tool/mapEach.kt new file mode 100644 index 0000000..1786867 --- /dev/null +++ b/src/tool/mapEach.kt @@ -0,0 +1,3 @@ +package tool + +fun Sequence.mapEach(transform: (T) -> R): Sequence = map(transform) diff --git a/tests/e2e/Examples.kt b/tests/e2e/Examples.kt index f93fc35..250f804 100644 --- a/tests/e2e/Examples.kt +++ b/tests/e2e/Examples.kt @@ -27,7 +27,7 @@ class Examples { @Test fun debugHelper() { - loader.load("examples/basics/backtracking.pl") + loader.load("examples/meta/continuations.pl") } @ParameterizedTest @@ -37,6 +37,13 @@ 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) { @@ -45,7 +52,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"), + 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("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"), @@ -57,6 +64,11 @@ 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 05df756..cf1cd94 100644 --- a/tests/interpreter/ParserPreprocessorIntegrationTests.kt +++ b/tests/interpreter/ParserPreprocessorIntegrationTests.kt @@ -41,10 +41,7 @@ class ParserPreprocessorIntegrationTests { val parsed = parser.parseToEnd("X is $input") as Term assertEquals( - Structure(Atom("is"), listOf( - Variable("X"), - Structure(Atom("-"), listOf(number)), - )), + Structure("is", Variable("X"), Structure("-",number)), parsed ) @@ -74,7 +71,7 @@ class ParserPreprocessorIntegrationTests { val result = parser.parseToEnd(input) as Term assertEquals( - Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))), + Structure("is", Variable("X"), Structure("-", Integer(1), Integer(2))), result ) diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index bf54869..60bcbf9 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -6,7 +6,6 @@ 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.* @@ -38,7 +37,7 @@ class PreprocessorTests { @Test fun `multiple anonymous variables should be unique`() { - val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_"))) + val input = CompoundTerm("foo", Variable("_"), Variable("_")) val result = preprocessor.preprocess(input) @@ -69,7 +68,7 @@ class PreprocessorTests { for (argument in inner.arguments) { if ((argument as Variable).name != "Name") { assertTrue( - (argument as Variable).name.matches("_\\d+".toRegex()), + argument.name.matches("_\\d+".toRegex()), "Expected anonymous variable name, but got ${argument.name}" ) } @@ -84,27 +83,13 @@ class PreprocessorTests { test( mapOf( Atom("=\\=") to Atom("=\\="), - CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()), + CompoundTerm("=\\=") to CompoundTerm("=\\="), Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"), - CompoundTerm(Atom("EvaluatesToDifferent"), emptyList()) to CompoundTerm( - Atom("EvaluatesToDifferent"), - emptyList() - ), - CompoundTerm(Atom("=\\="), listOf(Atom("a"))) to CompoundTerm( - Atom("=\\="), - listOf(Atom("a")) - ), - CompoundTerm(Atom("=\\="), listOf(Integer(1))) to CompoundTerm( - Atom("=\\="), - listOf(Integer(1)) - ), - CompoundTerm(Atom("=\\="), listOf(Atom("=\\="))) to CompoundTerm( - Atom("=\\="), - listOf(Atom("=\\=")) - ), - CompoundTerm(Atom("=\\="), listOf(Integer(1), Integer(2))) to EvaluatesToDifferent( - Integer(1), Integer(2) - ) + 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)) ) ) } @@ -114,7 +99,7 @@ class PreprocessorTests { test( mapOf( Atom("=:=") to Atom("=:="), - CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()), + CompoundTerm("=:=") to CompoundTerm("=:="), Atom("EvaluatesTo") to Atom("EvaluatesTo"), CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm( Atom("EvaluatesTo"), @@ -612,7 +597,7 @@ class PreprocessorTests { Atom("declaration/1") ) ) - val expected = Dynamic("declaration/1") + val expected = Dynamic(Functor.of("declaration/1")) val result = preprocessor.preprocess(input) diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index 57a1f99..5ca662a 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -2,7 +2,6 @@ package parser.grammars import com.github.h0tk3y.betterParse.grammar.Grammar import com.github.h0tk3y.betterParse.grammar.parseToEnd -import org.junit.jupiter.api.Assertions import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test @@ -14,7 +13,7 @@ import prolog.ast.logic.Rule import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Structure import prolog.ast.terms.Variable -import prolog.builtins.Conjunction +import prolog.ast.terms.Functor class LogicGrammarTests { private lateinit var parser: Grammar> @@ -33,7 +32,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) @@ -94,13 +93,13 @@ class LogicGrammarTests { assertTrue(rule.head is Structure, "Expected head to be a structure") val head = rule.head as Structure - assertEquals("parent/2", head.functor, "Expected functor 'parent/2'") + assertEquals(Functor.of("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("father/2", body.functor, "Expected functor 'father/2'") + assertEquals(Functor.of("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'") } @@ -125,12 +124,13 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") val rule = result[0] as Rule - 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'") + 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'") } @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("/_", rule.head.functor, "Expected a constraint") + assertEquals(Functor.of("/0"), 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 d3b45e2..b39a0d8 100644 --- a/tests/parser/grammars/TermsGrammarTests.kt +++ b/tests/parser/grammars/TermsGrammarTests.kt @@ -19,6 +19,8 @@ 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 @@ -352,4 +354,49 @@ 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 ac3df3f..8392eae 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/tests/prolog/EvaluationTests.kt @@ -14,6 +14,11 @@ import prolog.ast.terms.Atom 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 @@ -108,8 +113,8 @@ class EvaluationTests { val variable2 = Variable("Y") val parent = Rule( - Structure(Atom("parent"), listOf(variable1, variable2)), - /* :- */ Disjunction( + Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */ + Disjunction( Structure(Atom("father"), listOf(variable1, variable2)), /* ; */ Structure(Atom("mother"), listOf(variable1, variable2)) @@ -118,10 +123,14 @@ class EvaluationTests { Program.load(listOf(father, mother, parent)) - val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))) - assertTrue(result1.toList().isNotEmpty()) - val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))) - assertTrue(result2.toList().isNotEmpty()) + val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList() + assertEquals(1, result1.size, "Expected 1 result") + assertTrue(result1[0].isSuccess, "Expected success") + assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions") + val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList() + assertEquals(1, result2.size, "Expected 1 result") + assertTrue(result2[0].isSuccess, "Expected success") + assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions") val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane")))) assertFalse(result3.any()) @@ -414,4 +423,79 @@ class EvaluationTests { assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob") } } + + @Test + 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(Variable("X"), Variable("Y"))), + ) + + Program.db.load(listOf(fact, rule)) + + val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList() + + assertEquals(1, result1.size, "Expected 1 result") + assertTrue(result1[0].isSuccess, "Expected success") + val subs = result1[0].getOrNull()!! + 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() + + assertEquals(2, result2.size, "Expected 2 results") + + assertTrue(result2[0].isSuccess, "Expected success") + val subs2a = result2[0].getOrNull()!! + assertEquals(1, subs2a.size, "Expected 1 substitution") + assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0") + + assertTrue(result2[1].isSuccess, "Expected success") + 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 new file mode 100644 index 0000000..a6866c3 --- /dev/null +++ b/tests/prolog/builtins/AnalysisOperatorsTests.kt @@ -0,0 +1,646 @@ +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 8e96085..51a27c3 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["a/_"]!!.clauses[0]) + assertEquals(fact, Program.db.predicates[Functor.of("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["a/1"]!!.clauses[0]) + assertEquals(fact, Program.db.predicates[Functor.of("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["a/1"]!!.clauses[0]) + assertEquals(rule, Program.db.predicates[Functor.of("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["a/1"]!!.clauses[0]) - assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1]) + assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule1, Program.db.predicates[Functor.of("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["a/1"]!!.clauses[0]) - assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1]) + assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) } } @@ -131,7 +131,7 @@ class DatabaseOperatorsTests { @Test fun `simple retract`() { - val predicate = Predicate(listOf(Fact(Atom("a")))) + val predicate = Predicate(listOf(Fact(Atom("a"))), dynamic = true) Program.db.load(predicate) assertEquals(1, Program.query(Atom("a")).count()) @@ -146,11 +146,13 @@ class DatabaseOperatorsTests { @Test fun `retract atom`() { - val predicate = Predicate(listOf( - Fact(Atom("a")), - Fact(Atom("a")), - Fact(Atom("a")) - )) + val predicate = Predicate( + listOf( + Fact(Atom("a")), + Fact(Atom("a")), + Fact(Atom("a")) + ), dynamic = true + ) Program.db.load(predicate) val control = Program.query(Atom("a")).toList() @@ -170,11 +172,9 @@ 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,11 +183,13 @@ 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")))) - )) + 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() @@ -208,7 +210,6 @@ 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() @@ -218,7 +219,6 @@ 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,8 +228,9 @@ class DatabaseOperatorsTests { assertTrue(subs.isNotEmpty(), "Expected substitutions") assertTrue(Variable("X") in subs, "Expected variable X") assertEquals(Atom("d"), subs[Variable("X")], "Expected d") - assertFalse(result.hasNext(), "Expected no more results") assertEquals(0, predicate.clauses.size, "Expected no clauses") + + assertFalse(result.hasNext(), "Expected no more results") } @Test @@ -292,4 +293,45 @@ 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 new file mode 100644 index 0000000..7d461d0 --- /dev/null +++ b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt @@ -0,0 +1,73 @@ +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 05607ec..6bf8ee0 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 new file mode 100644 index 0000000..f6d0b71 --- /dev/null +++ b/tests/prolog/builtins/ListOperatorsTests.kt @@ -0,0 +1,232 @@ +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 new file mode 100644 index 0000000..aeb642c --- /dev/null +++ b/tests/prolog/builtins/MetaOperatorsTests.kt @@ -0,0 +1,34 @@ +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 new file mode 100644 index 0000000..e9341d6 --- /dev/null +++ b/tests/prolog/builtins/OtherOperatorsTests.kt @@ -0,0 +1,54 @@ +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/builtins/TermAnalysisConstructionTest.kt b/tests/prolog/logic/TermAnalysisConstructionTest.kt similarity index 65% rename from tests/prolog/builtins/TermAnalysisConstructionTest.kt rename to tests/prolog/logic/TermAnalysisConstructionTest.kt index a137fca..7000a49 100644 --- a/tests/prolog/builtins/TermAnalysisConstructionTest.kt +++ b/tests/prolog/logic/TermAnalysisConstructionTest.kt @@ -1,13 +1,10 @@ -package prolog.builtins +package prolog.logic -import org.junit.jupiter.api.Assertions.assertFalse -import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Assertions.* 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) @@ -22,12 +19,12 @@ class TermAnalysisConstructionTest { assertTrue(atomic(atom)) assertFalse(compound(atom)) - assertTrue(functor(atom, Atom("foo"), 0)) + assertEquals(Functor("foo", 0), atom.functor) } @Test fun compound_arity_0_properties() { - val structure = Structure(Atom("foo"), emptyList()) + val structure = Structure("foo") assertFalse(atomic(structure)) assertTrue(compound(structure)) @@ -35,11 +32,11 @@ class TermAnalysisConstructionTest { @Test fun compound_arity_1_properties() { - val structure = Structure(Atom("foo"), listOf(Atom("bar"))) + val structure = Structure("foo", Atom("bar")) assertFalse(atomic(structure)) assertTrue(compound(structure)) - assertTrue(functor(structure, Atom("foo"), 1)) + assertEquals(Functor("foo", 1), structure.functor) } } \ No newline at end of file diff --git a/tests/prolog/logic/UnificationTests.kt b/tests/prolog/logic/UnificationTests.kt index 10a37e7..1324a12 100644 --- a/tests/prolog/logic/UnificationTests.kt +++ b/tests/prolog/logic/UnificationTests.kt @@ -10,13 +10,16 @@ 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` { + class `unify logic` { @Test fun identical_atoms_unify() { val atom1 = Atom("a") @@ -330,7 +333,7 @@ class UnificationTests { } @Nested - class `applySubstitution` { + class `applySubstitution logic` { @Test fun `apply substitution without sub`() { val term = Variable("X") @@ -367,4 +370,120 @@ 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