Sync

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}
+}

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}
+
+    % 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}

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.

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

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

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

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)

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

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<Term> 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<String> by (equivalent or equals or notEquals or isOp) use { text }
+    protected val op700: Parser<String> by (univOp or equivalent or notEquivalent or equals or notEquals or isOp) use { text }
     protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
         if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
     }
 
+    protected val not: Parser<Term> by (notOp * parser(::term900)) use {
+        CompoundTerm(Atom(t1.text), listOf(t2))
+    }
+    protected val term900: Parser<Term> by (not or term700)
+
     protected val op1000: Parser<String> by (comma) use { text }
-    protected val term1000: Parser<Term> by (term700 * zeroOrMore(op1000 * term700)) use {
-        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    protected val term1000: Parser<Term> by (term900 * zeroOrMore(op1000 * term900)) use {
+        constructRightAssociative(t1, t2)
     }
 
     protected val op1100: Parser<String> by (semicolon) use { text }
     protected val term1100: Parser<Term> by (term1000 * zeroOrMore(op1100 * term1000)) use {
-        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+        constructRightAssociative(t1, t2)
     }
 
     protected val dynamic: Parser<Term> 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<PList> 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<Term> by term1200
     protected val termNoConjunction: Parser<Term> by term700
@@ -121,4 +145,12 @@ open class TermsGrammar : Tokens() {
     protected val body: Parser<Body> by term use { this as Body }
 
     override val rootParser: Parser<Any> by term
+
+    fun constructRightAssociative(left: Term, pairs: List<Tuple2<String, Term>>): 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)))
+    }
 }

src/parser/grammars/Tokens.kt

@@ -10,6 +10,8 @@ import com.github.h0tk3y.betterParse.lexer.token
 abstract class Tokens : Grammar<Any>() {
     protected val leftParenthesis: Token by literalToken("(")
     protected val rightParenthesis: Token by literalToken(")")
+    protected val 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<Any>() {
     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")

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

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)
+}

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

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
 }

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<Term>()
+            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()
+}

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()
 }

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)
+class Fact(head: Head) : Clause(head, True) {
+    override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head)
+}

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
 }

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)
+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
+    )
+}

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 = "_"
 }

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
     }

src/prolog/ast/terms/Body.kt

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

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
+    }
+}

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
 
 /**

src/prolog/ast/terms/Head.kt

@@ -6,5 +6,3 @@ package prolog.ast.terms
 interface Head : Term {
     val functor: Functor
 }
-
-typealias Functor = String

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"

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<Argument>) : 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<Argument>) : 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

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<Term> {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
+    fun applySubstitution(subs: Substitutions): Term
 }

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()
     }

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<Term>()
+                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))
+            }
+
+        }
+    }
+}

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)
+}

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

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()))
+    }
 }

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))
+    }
+}

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

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)
+    )
+}

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()
+}

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))
+                    }
+                }
+            )
+        }
+    }
+}

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)"
+}
+

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)"
 }

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))
+}

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

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.

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<Argument>,
+    args2: List<Argument>,
+    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
     }
 }

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}"
             }
         )
     }

src/tool/mapEach.kt

@@ -0,0 +1,3 @@
+package tool
+
+fun <T, R> Sequence<T>.mapEach(transform: (T) -> R): Sequence<R> = map(transform)

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

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
             )
 

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)
 

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<List<Clause>>
@@ -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")
     }
 }

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<Term>
@@ -352,4 +354,49 @@ class TermsGrammarTests {
             )
         }
     }
+
+    @Nested
+    class Lists {
+        private lateinit var parser: Grammar<Term>
+
+        @BeforeEach
+        fun setup() {
+            parser = TermsGrammar() as Grammar<Term>
+        }
+
+        @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"
+            )
+        }
+    }
 }

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)")
+    }
 }

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<Exception> {
+            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<IllegalArgumentException> {
+            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<IllegalArgumentException> {
+            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<Exception> {
+                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]]")
+        }
+    }
+}

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")
+    }
 }

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()
+    }
+}

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

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")
+    }
+}

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")
+    }
+}

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()
+        }
+    }
+}

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

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")
+        }
+    }
 }