2p-kt-talk.tex

% !TeX spellcheck = en_GB
%
% \documentclass[handout]{beamer}
\documentclass[presentation]{beamer}
\mode<presentation>{\usetheme{AMSCesenaPurpleAndGold}}
\setbeamertemplate{bibliography item}{\insertbiblabel}
\setbeamersize{description width=0.57cm}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{2p-kt-talk}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title[\twopkt]{
    \twopkt{}: A Kotlin Multi-Platform ecosystem for Symbolic AI
}
%
% \subtitle{Extended Abstract}
%
% same authors order of the presented paper
\author[Ciatto, Rizzato]{
    \emph{Giovanni Ciatto}$^{1}$ % empth the presenting author
    \and
    Lorenzo Rizzato$^{2}$
}
%
\institute[UniBo]{
    $^{1}$ Dipartimento di Informatica -- Scienza e Ingegneria (DISI)
    \\
    \textsc{Alma Mater Studiorum} -- Università di Bologna
    \\
    \texttt{
        giovanni.ciatto@unibo.it % emph the presenting author's email
    }
    \and
    $^{2}$ \texttt{lorenzo.rizzato@studio.unibo.it}
}
%
\date[May 2021]{
    May 2021
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\AtBeginSection[]{
    \begin{frame}<beamer>[shrink,noframenumbering]\frametitle{Next in Line\ldots}
        \mbox{~}
        \tableofcontents[sectionstyle=show/shaded,subsectionstyle=hide,subsubsectionstyle=hide]
        \mbox{~}
    \end{frame}
}
\AtBeginSubsection[]{
    \begin{frame}<beamer>[shrink,noframenumbering]\frametitle{Focus on\ldots}
        \mbox{~}
        \tableofcontents[sectionstyle=show/shaded,subsectionstyle=show/shaded,subsubsectionstyle=hide]%[currentsection,currentsubsection,sectionstyle=shaded,subsectionstyle=shaded,subsubsectionstyle=hide]
        \mbox{~}
    \end{frame}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\\\\\\\\\\\\\\\\\\\\\
\frame{\titlepage}
%\\\\\\\\\\\\\\\\\\\\\

\begin{frame}{\tuprolog{} vs \twopkt{}}
    \begin{block}{\tuprolog{} in the \textbf{past}}
        \begin{itemize}
            \item Malleable Java-based Prolog interpreter

            \item Java library for Prolog-Java interoperability
        \end{itemize}
    \end{block}

    \begin{block}{\tuprolog{} \textbf{nowadays}}
        \begin{itemize}
            \item An open, multi-platform, multi-paradigm ecosystem for LP

            \item \twopkt{} as the main, Kotlin-based implementation
            %
            \begin{itemize}
                \item currently targetting both JVM and JS
                \item involving both GUI and CLI executables
                \item[$\rightarrow$] providing a rich library for LP
            \end{itemize}

            \item Where each LP aspect is made individually available for re-use
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}{Useful Links}
    \begin{block}{\tuprolog{} project homepage}
        \centering
        \url{http://tuprolog.unibo.it}
    \end{block}

    \smallskip

    \begin{alertblock}{\tuprolog{} GitHub repository \hfill \textbf{(please support us with your star =)}}
        \centering
        \url{https://github.com/tuProlog/2p-kt}
    \end{alertblock}
    % %
    % \begin{itemize}
    %     \item star us if you like this project, it's important!
    % \end{itemize}

    \smallskip

    \begin{exampleblock}{Other useful links}
        \begin{itemize}
            \item \url{https://github.com/tuProlog}
            %
            \begin{itemize}
                \item GitHub organization containing all \tuprolog{}-related software projects
            \end{itemize}

            \item \url{https://gitlab.com/pika-lab/tuprolog/2p-in-kotlin}
            %
            \begin{itemize}
                \item GitLab repository where the actual development occurs
            \end{itemize}

            \item \url{https://pika-lab.gitlab.io/tuprolog/2p-in-kotlin}
            %
            \begin{itemize}
                \item documentation of \twopkt{}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
\end{frame}

\begin{frame}<beamer>[shrink,noframenumbering]\frametitle{Outline}
    \mbox{~}
    \tableofcontents
    \mbox{~}
\end{frame}

\section{Historical Perspective}

\subsection{Prolog History}

\begin{frame}{Implementations of Prolog -- Chronological Perspective}
    \input{fig-timeline.tex}
\end{frame}

\begin{frame}{Implementations of Prolog -- Family Tree}
    \input{fig-familytree.tex}
\end{frame}

\begin{frame}[allowframebreaks]{Implementations of Prolog -- Features (from \ccite{Korner2020HistoryFuturePrologTPLP})}
    \input{tab-features.tex}
\end{frame}

\subsection{\tuprolog{} History}

\begin{frame}[allowframebreaks]{\tuprolog{} History}
    \begin{block}{The original idea}
        \begin{itemize}
            \item light-weight Prolog system for \alert{distributed} applications \ccite{tuprolog-padl01}
            \item intentionally designed around a \alert{minimal core}
            \item \emph{configurable} by loading/unloading \alert{libraries} of predicates
            \item native support for \alert{multi-paradigm programming} \ccite{tuprolog-scp57}
            %
            \begin{itemize}
                \item bi-directional integration among OOP and Prolog
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{itemize}
        \item first release lightweight Prolog solver written in Java \ccite{tuprolog-padl01}
        \begin{itemize}
            \item OOP-interoperable
            \item state-machine-based \ccite{weblp-ia5}
        \end{itemize}

        \bigskip

        \item foundation of many research projects
        \begin{description}
            \item[TuCSoN / ReSpecT] coordination model for Internet applications based on network-aware and mobile agents \ccite{tucson-jaamas2} by means of reactions to communication events \ccite{respect-scp41}
            \item[MoK] self-organising knowledge-oriented model based on biochemical tuple space \ccite{mok-idc2012}
            \item[LPaaS] micro-intelligence vision (lightweight logic solvers running on most devices) for IoT and Cloud/Edge computing \ccite{lpaas-tplp18}
            \item[TuSoW] bringing tuple-based coordination at the edge \ccite{tusow-icccn2019}
            \item[Arg2P] defeasible reasoning and argumentation tool \ccite{arg2p-cilc2020}
        \end{description}
    \end{itemize}

    \framebreak

    \begin{block}{Why a complete re-write}
        \begin{itemize}
            \item Need to support LP in general, not only Prolog
            %
            \begin{itemize}
                \item re-design made \twopkt{} an \alert{ecosystem} for LP
                \item widening the scope w.r.t. Prolog
            \end{itemize}

            \item Need to get rid of a lot of legacy-code
            %
            \begin{itemize}
                \item accumulated as the code base stepped through many persons
                \item sub-optimal design choices due to limitations of early Java
                \item lack of fine-grained test units made the codebase hard to maintain
                \item lack of module \& package segregation
                \item lack of automated dependency management
            \end{itemize}
        \end{itemize}
    \end{block}

\end{frame}

\section{Motivation}

\begin{frame}{Why \twopkt{}}
    \begin{itemize}
        \item Building an open an extensible ecosystem\ldots
        \vfill
        \item \ldots supporting \alert{multiple logics} (e.g. FOL, DL, TL, BDI, etc)
        %
        \begin{itemize}
            \item via as many \alert{inference rules} as possible (e.g. deduction, abduction, induction)
            %
            \begin{itemize}
                \item implemented, in turn, via multiple \alert{resolution strategies} (e.g. SLDNF, IFF, Probabilistic, etc.)
            \end{itemize}
        \end{itemize}
        \vfill
        \item Making each aspect of LP individually usable \emph{per se}
        \vfill
        \item Reaching widest possible platform support
        \vfill
        \item Blending LP with OOP and FP
        \vfill
        \item Bridging symbolic and sub-symbolic AI
    \end{itemize}
\end{frame}

\begin{frame}{Which features of LP}
    \begin{enumerate}
        \item Knowledge representation: \alert{terms}, and \alert{clauses}
        \vfill
        \item \alert{Unification}, based on \cite{MartelliMontanari1982} but possibly customisable
        \vfill
        \item Clauses \alert{indexing} and in-memory \alert{storage} facilities for \alert{knowledge bases}
        \vfill
        \item Prolog-like syntax \alert{parsing} \& \alert{formatting}
        \vfill
        \item \alert{Serialization} / \alert{deserialization} of terms, clauses, and knowledge bases
        \vfill
        \item Generic \alert{resolution} API, possibly customisable via \alert{pluggable features}
        \vfill
        \item \alert{SLD NF} (Prolog-like) resolution strategy \cite{Robinson65SLD,Clark77}
        \vfill
        \item Support for other resolution strategies
        \vfill
        \item Common \alert{UI} facilities
        \vfill
        \item[\vdots]
    \end{enumerate}
\end{frame}

\begin{frame}{Why Kotlin}
    \begin{itemize}
        \item Multi-platform support:
        %
        \begin{itemize}
            \item JVM (Win + Linux + Mac)
            \item JS (Web, both browser and server side)
            \item Android
            \item Native?
            \item iOS?
        \end{itemize}

        \vfill

        \item Good platform-specific interoperability
        %
        \begin{itemize}
            \item Kotlin libraries can easily be exploited in bare Java projects
            \item Kotlin libraries can be exploited in bare JavaScript projects
        \end{itemize}

        \vfill

        \item Clean and practical framework and tool-kit available
    \end{itemize}
\end{frame}

\section{Overview of the Project}

\begin{frame}[allowframebreaks]{Project Map}
    \begin{itemize}
        \item \twopkt{} is an ecosystem of \alert{modules}
        %
        \begin{itemize}
            \item denoted by Gradle's notation: \module{moduleName}
        \end{itemize}

        \medskip

        \item Modules are \alert{loosely-coupled}, yet incrementally inter-dependent
        %
        \begin{itemize}
            \item[$\rightarrow$] \alert{onion-like} architectural design
        \end{itemize}

        \medskip

        \item Modules are compilation and \alert{deployment units}
        %
        \begin{itemize}
            \item 1 module $\leftrightarrow$ 1 jar, on the JVM
        \end{itemize}

        \medskip

        \item Using a module as a dependency $\implies$ importing \alert{all} its dependencies
    \end{itemize}

    \framebreak

    \begin{center}
        \includegraphics[width=\linewidth]{img/project-map.pdf}
    \end{center}

    \framebreak

    \begin{description}
        \item[\module{core}] provides \alert{knowledge representations} facilities \& common features
        %
        \begin{itemize}\small
            \item[eg] terms, clauses, substitutions, operators, term formatting, basic exceptions, etc.
        \end{itemize}

        \medskip

        \item[\module{unify}] provides support for \alert{logic unification}
        %
        \begin{itemize}\small
            \item[eg] customisable notion of unificator based on \cite{MartelliMontanari1982}
        \end{itemize}

        \medskip

        \item[\module{theory}] provides support in-memory \alert{storage \& indexing} of clauses
        %
        \begin{itemize}\small
            \item[eg] mutable/immutable and ordered/unordered \alert{collections of clauses} + \alert{logic theories}
        \end{itemize}

        \medskip

        \item[\module{solve}] provides generic support for \alert{resolution-related} stuff
        %
        \begin{itemize}\small
            \item[!] agnostic w.r.t. inference procedures \& resolution strategy
            \item[eg] solvers, solutions, libraries, errors, flags, channels, etc.
        \end{itemize}

        \framebreak

        \item[\module{solve-*}] provide specific implementation for inference procedures \& \alert{resolution} strategy
        %
        \begin{description}\small
            \item[\module{solve-classic}] SLD NF (Prolog-like) resolution \cite{Robinson65SLD,Clark77} based on Piancastelli's state machine \cite{tuprolog-sac08} (\alert{Prolog ISO \cite{prologISO-pt1} Compliant})
            \item[\module{solve-streams}] SLD NF (Prolog-like) resolution \cite{Robinson65SLD,Clark77} based on Enrico Siboni's master thesis and on \cite{Carlsson84}
        \end{description}

        \medskip

        \item[\module{parser-*}] supports \alert{parsing} of terms and clauses in Prolog syntax
        %
        \begin{description}\small
            \item[\module{parser-core}] supports parsing terms
            \item[\module{parser-theory}] supports parsing knowledge bases and streams of clauses
            \item[\module{parser-jvm/js}] platform-specific implementations, based on ANTLR \cite{Parr2013} \hint{(not to be used directly!)}
        \end{description}

        \framebreak

        \item[\module{serialization-*}] support \alert{(de)serialization} of terms, clauses, knowledge bases in \alert{YAML/JSON}
        %
        \begin{description}\small
            \item[\module{serialization-core}] (de)serialization of terms and clauses
            \item[\module{serialization-theory}] (de)serialization of knowledge bases and theories
        \end{description}

        \medskip

        \item[\module{dsl-*}] incrementally support the Kotlin-based DSL for LP described in~\cite{kotlinDSl4PrologWoa2020}, aimed at blending LP, FP, and OOP
        %
        \begin{description}\small
            \item[\module{dsl-core}] basic DSL for building terms/clauses in Kotlin
            \item[\module{dsl-unify}] extension of the DSL including \module{unify} facilities
            \item[\module{dsl-theory}] extension of the DSL including \module{theory} facilities
            \item[\module{dsl-solve}] extension of the DSL including \module{solve} facilities
        \end{description}

        \framebreak

        \item[\module{repl}] command-line interface for Prolog

        \medskip

        \item[\module{ide}] JavaFX-based GUI for Prolog (customisable)

        \medskip

        \item[\module{io-lib}] Prolog ISO compliant Prolog library for I/O

        \medskip

        \item[\module{oop-lib}] Prolog library for OOP interoperability
        %
        \begin{itemize}\small
            \item essentially, lets Kotlin's and Java's OOP facilities be exploited from LP
            \item only JVM is currently supported, due to limitations in Kotlin's reflection API
        \end{itemize}

    \end{description}
\end{frame}

\section{Knowledge Representation: the \module{core} Module}

\begin{frame}[allowframebreaks]{Main Abstractions from the \module{core} Module}
    \begin{block}{Terms and Clauses}\center\itshape\small
        Immutable data structures for terms and clauses in-memory representation \& manipulation
    \end{block}

    \begin{block}{Substitutions}\center\itshape\small
        Immutable data structures representing variables assignments, applicable to terms/clauses
    \end{block}

    \begin{block}{Operators and Operators Sets}\center\itshape\small
        Immutable data structures for representing logic operators and their esembles
    \end{block}

    \framebreak

    \begin{block}{Formatters}\center\itshape\small
        Functional objects aimed at converting terms/clauses into strings of customisable format
    \end{block}

    \begin{block}{Visitors}\center\itshape\small
        Functional objects aimed at easing type-dependent algorithms writing
    \end{block}

    \begin{block}{Exceptions}\center\itshape\small
        Base exception types extensively exploited in all whole \twopkt{} project
    \end{block}
\end{frame}

\subsection{The \kt{Term} Hierarchy}

\subsubsection{Main Sorts of \kt{Term}s and \kt{Clause}s}

\begin{frame}[allowframebreaks]{Term Hierarchy}
    \begin{center}
        \includegraphics[width=.75\linewidth]{img/terms-nofields.pdf}
    \end{center}

    \begin{block}{Common Conventions}
        \begin{itemize}
            \item Only interfaces are publicly available, no classes
            \item Immutable design: all terms are immutable data structures
            \item The hierarchy is a DAG, not a tree
            \item Terms are totally ordered, as the are \kt{Comparable} among each others
            \item We call ``term'' any object which (indirectly) implements \kt{Term}
            %
            \begin{itemize}
                \item[!] there including clauses, i.e. instances of \kt{Clause}
            \end{itemize}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Term} type}

    \begin{block}{The \kt{Term} type}\centering
        Base type for all terms
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.5\linewidth]{img/term.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{is\meta{SubType}: Boolean}] checks whether the current term is an instance of \kt{\meta{SubType}} or not
        \item[\kt{as\meta{SubType}(): \meta{SubType}}] casts the current term to \kt{\meta{SubType}} or returns null if not possible
        \item[\kt{castTo\meta{SubType}(): \meta{SubType}}] casts the current term to \kt{\meta{SubType}} or throws an exception if not possible
        \item[\kt{freshCopy(): Term}] returns a deep copy of the current term where all \kt{Var}iables have been refreshed
        \item[\kt{apply(Substitution): Term}] applies the provided \kt{Substitution} to the current \kt{Term} or throws a \kt{SubstitutionApplicationException} in case a failed \kt{Substitution} has been provided
        \item[\kt{equals(Term, Boolean): Boolean}] checks whether the provided \kt{Term} is deeply equal to the current one, letting the caller choose whether to compare variables by simple or by complete name
        \item[\kt{equals(Any?): Boolean}] checks whether the provides object is a \kt{Term} is deeply equal to the current one, comparing variables by complete names
        \item[\kt{structurallyEquals(Term): Boolean}] checks whether the provided \kt{Term} is deeply equal to the current one, in such a way that all variables are considered equal
        \item[\kt{accept<T>(TermVisitor<T>): T}] returns the object produced by letting the provided \kt{TermVisitor} visit the current \kt{Term}
        \item[\kt{compareTo(Term): Int}] compares the current \kt{Term} with the provided one, according to the total ordering on \kt{Term}s
        \item[\kt{toString(): String}] returns a representation of the current \kt{Term} for debugging purposes
        \item[\kt{variables: Sequence<Var>}] returns the (possibly empty) sequence of variables contained in the current \kt{Term}
        %
        \begin{itemize}\small
            \item[!] duplicates are \emph{not} removed
        \end{itemize}
        \item[\kt{isGround: Boolean}] returns \kt{true} if the current \kt{Term} contains no \kt{Var}iable
    \end{description}

    \framebreak

    \ktSnippet{snippets/TermUsage.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Main Sorts of \kt{Term}s}

    \begin{block}{The \kt{Constant} type is a sub-type of \kt{Term}}\centering
        Base type for all constant terms (namely, strings and numbers)
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.4\linewidth]{img/constant.pdf}
    \end{center}
    %
    \begin{description}
        \item[\kt{value: Any}] returns the value of this \kt{Constant}
    \end{description}

    \begin{alertblock}{About \kt{Constant}s}
        \begin{itemize}
            \item \kt{Constant}s are inherently \alert{ground}
            \item Their \kt{isGround} property always return \kt{true}
            \item Their \kt{variables} property always return an empty sequence
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{block}{The \kt{Numeric} type is a sub-type of \kt{Constant}}\centering
        Base type for all numeric terms (namely, reals and integers)
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.8\linewidth]{img/numeric.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{intValue: BigInteger}] returns the integer value of the current number
        %
        \begin{itemize}
            \item \kt{BigInteger}s can then be converted into \kt{Int}, \kt{Short}, etc.
            \item unlimited amount of digits $\rightarrow$ no overflow, no max value
        \end{itemize}

        \item[\kt{decimalValue: BigDecimal}] returns the decimal value of the current number
        %
        \begin{itemize}
            \item \kt{BigDecimal}s can then be converted into \kt{Double} or \kt{Float}
            \item i.e. a real number with arbitrary precision
        \end{itemize}
    \end{description}

    \framebreak

    \begin{block}{The \kt{Integer} type is a sub-type of \kt{Numeric}}\centering
        Type for all terms representing an integer number
    \end{block}
    %
    \begin{description}
        \item[\kt{value: BigInteger}] returns \kt{this.intValue}
        %
        \begin{itemize}
            \item \kt{BigInteger}s can then be converted into \kt{Int}, \kt{Short}, etc.
            \item unlimited amount of digits $\rightarrow$ no overflow, no max value
        \end{itemize}
    \end{description}

    \ktSnippet{snippets/IntUsage.kt}

    \framebreak

    \begin{block}{The \kt{Real} type is a sub-type of \kt{Numeric}}\centering
        Type for all terms representing a real number
    \end{block}
    %
    \begin{description}
        \item[\kt{value: BigDecimal}] returns \kt{this.decimalValue}
        %
        \begin{itemize}
            \item \kt{BigDecimal}s can then be converted into \kt{Double} or \kt{Float}
            \item i.e. a real number with arbitrary precision
        \end{itemize}
    \end{description}

    \ktSnippet{snippets/RealUsage.kt}

    \framebreak

    \begin{block}{The \kt{Struct} type is a sub-type of \kt{Term}}\centering
        Type for all terms of the form \kt{$f$($t_1$, \ldots, $t_N$)}, i.e. composed by a \alert{funtor} string $f$ and $N$ terms $t_1, \ldots, t_N$ called \alert{arguments}, where $N \geq 0$ is called \alert{arity}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.6\linewidth]{img/struct.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{functor: String}] returns $f$
        \item[\kt{arity: Int}] returns $N$
        \item[\kt{args: Array<Term>}] returns an array containing $t_1, \ldots, t_N$
        \item[\kt{argsList: List<Term>}] returns a list containing $t_1, \ldots, t_N$
        \item[\kt{argsSequence: Sequence<Term>}] returns a sequence containing $t_1, \ldots, t_N$

        \item[\kt{isFunctorWellFormed: Boolean}] returns true if the following condition hold for $f$
        %
        \begin{enumerate}\small
            \item it begins with a lower case letter
            \item it only contains letters (either lower or upper case), digits, or underscores
        \end{enumerate}
        \item[\kt{toString(): String}] returns $f$ iff $N = 0$, otherwise a string of the form
        %
        \begin{center}
            \kt{$f$($t_1$.toString(), \ldots, $t_N$.toString())}
        \end{center}
        %
        \begin{itemize}\small
            \item in both cases, $f$ is wrapped within single quotes iff \kt{isFunctorWellFormed} is false
        \end{itemize}
        \item[\kt{equals(Any?): Boolean}] compares this \kt{Struct}ure with the provided object, returning true if the latter is a \kt{Struct}ure having the same functor, arity, and arguments (which are recursively compared via \kt{equals(Any?)})
        \item[\kt{hashCode(): Int}] computes an hash code value for this \kt{Struct}ure which is coherent w.r.t. \kt{equals(Any?)}
        \item[\kt{equals(Term,Boolean): Boolean}] compares this \kt{Struct}ure with the provided object, returning true if the latter is a \kt{Struct}ure having the same functor, arity, and arguments (which are recursively compared via \kt{equals(Term,Boolean)})
        \item[\kt{structurallyEquals(Term): Boolean}] compares this \kt{Struct}ure with the provided object, returning true if the latter is a \kt{Struct}ure having the same functor, arity, and arguments (which are recursively compared via \kt{structurallyEquals(Term)})
        \item[\kt{indicator: Indicator}] returns the indicator corresponding to the current \kt{Struct}
        %
        \begin{itemize}\small
            \item i.e. the \kt{Struct}ure of the form \pl{'/'($f$, $N$)}
        \end{itemize}
        \item[\kt{get(Int): Term}] returns an argument of the current \kt{Struct} given its index
        \item[\kt{getArgAt(Int): Term}] an alias for \kt{get(Int)}
        \item[\kt{addFirst(Term): Term}] returns a novel \kt{Struct} of the form \pl{$f$($t^*$, $t_1$, \ldots, $t_N$)}, where $t^*$ is the \kt{Term} provided as argument
        \item[\kt{addLast(Term): Term}] returns a novel \kt{Struct} of the form \pl{$f$($t_1$, \ldots, $t_N$, $t^*$)}, where $t^*$ is the \kt{Term} provided as argument
        \item[\kt{append(Term): Term}] an alias for \kt{addLast(Term)}
        \item[\kt{insertAt(Int,Term): Term}] returns a novel \kt{Struct} of the form \pl{$f$($t_1$, \ldots, $t_{i-1}$, $t^*$, $t_{i+1}$, \ldots, $t_N$)}, where $t^*$ is the \kt{Term} provided as argument
        \item[\kt{setFunctor(String): Term}] returns a novel \kt{Struct} of the form \pl{$f^*$($t_1$, \ldots, $t_N$)}, where $f^*$ is the functor \kt{String} provided as argument
    \end{description}

    \framebreak

    \ktSnippet[\tiny]{snippets/StructUsage.kt}

    \framebreak

    \begin{block}{The \kt{Atom} type is a sub-type of both \kt{Struct} and \kt{Constant}}\centering
        Type for all constant 0-ary structures (i.e., with no arguments), representing strings
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.6\linewidth]{img/atom.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{value: String}] returns \kt{this.functor}
        \item[\kt{arity: Int}] must return 0
        \item[\kt{args: Array<Term>}] must return the empty array
        \item[\kt{argsList: List<Term>}] must return the empty list
        \item[\kt{argsSequence: Sequence<Term>}] must return the empty sequence
    \end{description}

    \framebreak

    \ktSnippet{snippets/AtomUsage.kt}

    \framebreak

    \begin{block}{The \kt{Var} type is a sub-type of \kt{Term}}\centering
        Type for all variable terms, representing \alert{named} placeholders for other terms.
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.5\linewidth]{img/var.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{alertblock}{About \kt{Var}iable names}
        \begin{itemize}
            \item Variables are identified by \alert{complete name}
            \item Variables' complete names are \kt{String}s of the form
            %
            \begin{center}
                \pl{$Name$\_$Identifier$}
            \end{center}
            where
            %
            \begin{description}
                \item[$Name$] is the variable's \alert{simple} name
                \item[$Identifier$] is the variable's \alert{identifier}, i.e. an im\-ple\-men\-ta\-tion-spe\-ci\-fic string aimed at distinguishing \kt{Var}iables having the same simple name
            \end{description}
            \item Variables whose simple name is \pl{'\_'} are called \alert{anonymous}
        \end{itemize}
    \end{alertblock}
    %
    \begin{description}
        \item[\kt{name: String}] returns $Name$
        \item[\kt{completeName: String}] returns \pl{$Name$\_$Identifier$}
        \item[\kt{id: String}] returns $Identifier$
        \item[\kt{isAnonymous: Boolean}] returns true iff \pl{$Name$ = '\_'}
        \item[\kt{toString(): Boolean}] returns this \kt{this.completeName}
        \item[\kt{equals(Any?): Boolean}] compares this \kt{Var}iable with the provided object, returning true if the latter is a \kt{Var}iable having the same complete name
        \item[\kt{equals(Term,Boolean): Boolean}] compares this \kt{Var}iable with the provided object, returning true if the latter is a \kt{Var}iable having the same complete (resp. simple) name, assuming that the provided \kt{Boolean} is true (resp. false)
        \item[\kt{structurallyEquals(Term): Boolean}] compares this \kt{Var}iable with the provided object, returning true if the latter is a \kt{Var}iable
    \end{description}

    \ktSnippet{snippets/VarUsage.kt}

    \framebreak

    \begin{block}{The \kt{Indicator} type is a sub-type of \kt{Struct}}
        \begin{center}
            Type for all binary structures of the form
            %
            \begin{center}
                \pl{'/'($f$, $n$)}
            \end{center}
            where $f,n$ are arbitrary terms. If $f$ is an atom and $n$ is a non-negative integer, then the indicator is considered \emph{well formed}
        \end{center}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.7\linewidth]{img/indicator.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{nameTerm: Term}] returns $f$, shortcut for \kt{get(0)}
        \item[\kt{indicatedName: String?}] if $f$ is an atom, returns \kt{$f$.value}, otherwise \kt{null}
        \item[\kt{arityTerm: Term}] returns $n$, shortcut for \kt{get(1)}
        \item[\kt{indicatedArity: Int?}] if $n$ is a non-negative integer, returns \kt{$n$.intValue.toInt()}, otherwise \kt{null}
        \item[\kt{isWellFormed: Boolean}] returns \kt{true} if the indicator is well formed
        \item[\kt{functor: String}] must return \kt{"/"}
        \item[\kt{arity: String}] must return 2
    \end{description}

    \ktSnippet{snippets/IndicatorUsage.kt}

    \framebreak

    \begin{block}{The \kt{Truth} type is a sub-type of \kt{Atom}}
        \begin{center}
            Type for special atoms representing either tautology or contradiction.
            It has only three admissible values: \pl{true} (tautology), \pl{false}, and \pl{fail} (contradictions).
        \end{center}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.9\linewidth]{img/truth.pdf}
    \end{center}
    %
    \begin{description}
        \item[\kt{isTrue: Boolean}] returns \kt{true} if the atom is a tautology
        \item[\kt{isFail: Boolean}] returns \kt{true} if the atom is a contradiction
    \end{description}

    \framebreak

    \ktSnippet[\tiny]{snippets/TruthUsage.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Collections}
    \begin{exampleblock}{How to fold items with structures}
        \begin{itemize}
            \item Suppose you want to collect terms $t_1, \ldots, t_N$\ldots
            \item \ldots using binary structures whose functor is $f$
            \item Two folding strategies: with or without a termination term $T$
            %
            \begin{itemize}
                \item explicit termination: \pl{$f$($t_1$, $f$($t_2$, \ldots $f$($t_N$, $T$) \ldots ))}
                \item implicit termination: \pl{$f$($t_1$, $f$($t_2$, \ldots $f$($t_{N-1}$, $t_N$) \ldots ))}
            \end{itemize}
            \item A particular collection is therefore determined by:
            %
            \begin{itemize}
                \item the particular choice of $f$
                \item the particular folding strategy adopted
                \item the particular termination term $T$, if any
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
    %
    \framebreak
    %
    \begin{block}{The \kt{Collection} type is a sub-type of \kt{Struct}}\centering
        Base type for all right-recursive structures aimed at containing an unlimited amount of terms.
    \end{block}
    %
    \begin{center}
        \includegraphics[width=.8\linewidth]{img/collection.pdf}
    \end{center}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{unfoldedSequence: Sequence<Term>}] in general, returns a sequence containing the terms $t_1, \ldots, t_N$, plus $T$ in case of explicit folding strategy
        \item[\kt{unfoldedList: List<Term>}] in general, returns a list containing the terms $t_1, \ldots, t_N$, plus $T$ in case of explicit folding strategy
        \item[\kt{unfoldedArray: Array<Term>}] in general, returns an array containing the terms $t_1, \ldots, t_N$, plus $T$ in case of explicit folding strategy
        \item[\kt{size: Int}] in general, returns $N$
        \item[\kt{toSequence(): Sequence<Term>}] in general, returns a sequence containing the terms $t_1, \ldots, t_N$
        \item[\kt{toList(): List<Term>}] in general, returns a list containing the terms $t_1, \ldots, t_N$
        \item[\kt{toArray(): Array<Term>}] in general, returns an array containing the terms $t_1, \ldots, t_N$
        \item[\kt{unfold(): Sequence<Term>}] in general, returns a sequence containing the terms \pl{$f$($t1$, $f$($t_2$, \ldots))}, \pl{$f$($t_2$, \ldots)}, \pl{\ldots}, plus $T$ in case of explicit folding strategy, or \pl{$f$($t_{N-1}$, $t_N$)} otherwise
    \end{description}

    \framebreak

    \begin{block}{The \kt{List} type is a sub-type of \kt{Collection}}
        \begin{center}
            Base type for logic lists, i.e. collections using \pl{'.'} as functor and \pl{'[]'} as the termination term.
            %
            So all lists are terms of the form
            \begin{center}
                \pl{'.'($t_1$, '.'($t_2$, \ldots '.'($t_N$, $T$)\ldots))}.
            \end{center}
            %
            A list is considered well formed iff $T \equiv \pl{[]}$.
        \end{center}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.9\linewidth]{img/list.pdf}
    \end{center}
    %
    \begin{alertblock}{About logic lists}
        \begin{itemize}
            \item There are two sub-types of \kt{List}:
            %
            \begin{itemize}
                \item \alert{\kt{Cons}}, capturing all terms of the form \pl{'.'($h$, $t$)} where both $h$ and $t$ are terms of any sort
                \item \alert{\kt{EmptyList}}, which has only one value, namely the atom \pl{'[]'}
            \end{itemize}

            \item Logic lists are represented as strings using the following notation:
            %
            \begin{center}
                \pl{[$t_1$, $t_2$, \ldots $t_n$ | $T$]}
            \end{center}
            %
            \begin{itemize}
                \item where `\pl{| $T$}' may be omitted in case $T \equiv \pl{[]}$
            \end{itemize}
        \end{itemize}
    \end{alertblock}
    %
    \begin{description}
        \item[\kt{isWellFormed: Boolean}] returns \kt{true} if the list is well formed
        \item[\kt{last: Term}] returns $T$
        \item[\kt{isCons: Boolean}] returns \kt{true} if the list is not empty
        \item[\kt{isEmptyList: Boolean}] returns \kt{true} if the list is empty
        \item[\kt{unfoldedSequence: Sequence<Term>}] returns a sequence containing the terms $t_1, \ldots, t_N, \pl{[]}$
        \item[\kt{unfoldedList: List<Term>}] returns a list containing the terms $t_1, \ldots, t_N, \pl{[]}$
        \item[\kt{unfoldedArray: Array<Term>}] returns an array containing the terms $t_1, \ldots, t_N, \pl{[]}$
        \item[\kt{size: Int}] returns $N$ if the list is well formed, or $N+1$ otherwise
        \item[\kt{toSequence(): Sequence<Term>}] returns a sequence containing the terms $t_1, \ldots, t_N$, plus $T$ iff $T \not\equiv \pl{[]}$
        \item[\kt{toList(): List<Term>}] returns a list containing the terms $t_1, \ldots, t_N$, plus $T$ iff $T \not\equiv \pl{[]}$
        \item[\kt{toArray(): Array<Term>}] returns an array containing the terms $t_1, \ldots, t_N$, plus $T$ iff $T \not\equiv \pl{[]}$
        \item[\kt{unfold(): Sequence<Term>}] returns a sequence containing the terms \pl{'.'($t1$, '.'($t_2$, \ldots))}, \pl{'.'($t_2$, \ldots)}, \pl{\ldots}, $T$
    \end{description}

    \ktSnippet[\tiny]{snippets/ListUsage.kt}

    \framebreak

    \begin{block}{The \kt{Tuple} type is a sub-type of \kt{Collection}}
        \begin{center}
            Base type for logic conjunctions, i.e. collections using \pl{','} as functor and an implicit termination strategy.
            %
            So all tuples are terms of the form
            \begin{center}
                \pl{','($t_1$, ','($t_2$, \ldots ','($t_{N-1}$, $t_N$)\ldots))}.
            \end{center}
            %
            Notice that tuples always contain at least 2 terms.
        \end{center}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.9\linewidth]{img/tuple.pdf}
    \end{center}
    %
    \begin{alertblock}{About logic tuples}
        \begin{itemize}
            \item Logic tuples are represented as strings using the following notation:
            %
            \begin{center}
                \pl{($t_1$, $t_2$, \ldots $t_n$)}
            \end{center}
        \end{itemize}
    \end{alertblock}
    %
    \begin{description}
        \item[\kt{unfoldedSequence: Sequence<Term>}] returns a sequence containing the terms $t_1, \ldots, t_N$
        \item[\kt{unfoldedList: List<Term>}] returns a list containing the terms $t_1, \ldots, t_N$
        \item[\kt{unfoldedArray: Array<Term>}] returns an array containing the terms $t_1, \ldots, t_N$
        \item[\kt{size: Int}] returns $N$
        \item[\kt{toSequence(): Sequence<Term>}] returns \kt{this.unfoldedSequence}
        \item[\kt{toList(): List<Term>}] returns \kt{this.unfoldedList}
        \item[\kt{toArray(): Array<Term>}] returns \kt{this.unfoldedArray}
        \item[\kt{unfold(): Sequence<Term>}] returns a sequence containing the terms \pl{','($t1$, ','($t_2$, \ldots))}, \pl{','($t_2$, \ldots)}, \pl{\ldots}, \pl{','($t_{N-1}$, $t_N$)}
    \end{description}

    \framebreak

    \ktSnippet{snippets/TupleUsage.kt}

    \framebreak

    \begin{block}{The \kt{Set} type is a sub-type of \kt{Collection}}
        \begin{center}
            Base type for logic sets, i.e. a particular sort of collection using \pl{\{\}} as functor, which may either be empty or contain a single term---which may possibly be a tuple.
        \end{center}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.9\linewidth]{img/set.pdf}
    \end{center}
    %
    \begin{alertblock}{About logic sets}
        \begin{itemize}
            \item There are two sub-types of \kt{Set}:
            %
            \begin{itemize}
                \item \alert{\kt{Set}}, capturing all terms of the form \pl{'\{\}'($x$)} where $x$ is a term of any sort
                \item \alert{\kt{EmptySet}}, which has only one value, namely the atom \pl{'\{\}'}
            \end{itemize}

            \item Logic sets are represented as strings using the following notations:
            %
            \begin{itemize}
                \item \pl{\{\}} in case of empty set
                \item \pl{\{$t_1$, \ldots $t_N$\}} in case $x$ $\equiv$ \pl{($t_1$, \ldots, $t_N$)}, i.e. if $x$ is a tuple
                \item \pl{\{$x$\}} otherwise
            \end{itemize}
        \end{itemize}
    \end{alertblock}
    %
    \begin{description}
        \item[\kt{unfoldedSequence: Sequence<Term>}] returns a sequence containing the terms $t_1, \ldots, t_N$ if $x$ is a tuple, just $x$ otherwise, or nothing if the set is empty
        \item[\kt{unfoldedList: List<Term>}] returns a list containing the terms $t_1, \ldots, t_N$ if $x$ is a tuple, just $x$ otherwise, or nothing if the set is empty
        \item[\kt{unfoldedArray: Array<Term>}] returns an array containing the terms $t_1, \ldots, t_N$ if $x$ is a tuple, just $x$ otherwise, or nothing if the set is empty
        \item[\kt{size: Int}] returns $N$ if $x$ is a tuple, 1 otherwise, or 0 if the set is empty
        \item[\kt{toSequence(): Sequence<Term>}] returns \kt{this.unfoldedSequence}
        \item[\kt{toList(): List<Term>}] returns \kt{this.unfoldedList}
        \item[\kt{toArray(): Array<Term>}] returns \kt{this.unfoldedArray}
    \end{description}

    \ktSnippet{snippets/SetUsage.kt}

\end{frame}

\begin{frame}[allowframebreaks]{Clauses}

    \begin{block}{The \kt{Clause} type is a sub-type of \kt{Struct}}\centering
        Base type for all structures aimed at representing Horn clauses.
        They all use \pl{':-'} as functor and carry either 1 or 2 arguments, named \emph{head} and \emph{body}.
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.95\linewidth]{img/clause.pdf}
    \end{center}

    \framebreak

    \begin{alertblock}{About clauses}
        \begin{itemize}
            \item There are three sub-types of \kt{Clause}:
            %
            \begin{itemize}
                \item \alert{\kt{Rule}}, capturing all structures of the form \pl{':-'($h$, $b$)} where $h$ is a \kt{Struct}ure and $b$ is a term of any sort
                %
                \begin{itemize}
                    \item \alert{\kt{Fact}}, capturing all rules of the form \pl{':-'($h$, true)}, where $b$ $\equiv$ \pl{true}
                \end{itemize}
                \item \alert{\kt{Directives}}, capturing all structures of the form \pl{':-'($b$)} where $b$ is a term of any sort
            \end{itemize}

            \item Logic clauses are represented as strings using the following notations:
            %
            \begin{itemize}
                \item \pl{$h$ :- $b_1$, \ldots, $b_N$.} in case of rules where $b$ $\equiv$ \pl{($b_1$, \ldots, $b_N$)}
                \item \pl{$h$ :- $b$.} in case of rules
                \item \pl{$h$.} in case of facts
                \item \pl{:- $b_1$, \ldots, $b_N$.} in case of directives where $b$ $\equiv$ \pl{($b_1$, \ldots, $b_N$)}
                \item \pl{:- $b$.} in case of directives
            \end{itemize}
        \end{itemize}
    \end{alertblock}
    %
    \framebreak
    %
    \begin{description}
        \item[\kt{head: Struct?}] returns $h$ for rules, or \kt{null} for directives
        \item[\kt{body: Term}] returns $b$
        \item[\kt{isRule: Boolean}] returns \kt{true} if the clause is not a directive
        \item[\kt{isDirective: Boolean}] returns \kt{true} if the clause is a directive
        \item[\kt{isFact: Boolean}] returns \kt{true} if the clause is a fact
        \item[\kt{isWellFormed: Boolean}] returns \kt{true} iff no sub-term in $b$ which is interpretable as a logic goal is a \kt{Var}iable
    \end{description}

    \framebreak

    \ktSnippet[\tiny]{snippets/ClausesUsage.kt}
\end{frame}

\subsubsection{Creating \kt{Term}s}

\begin{frame}[allowframebreaks]{Creating \kt{Term}s via Static Factories}

    Conventions on terms/clause creation in \twopkt:
    %
    \bigskip
    %
    \begin{itemize}
        \item Terms and clauses can be created via \alert{static factory methods} on interfaces
        %
        \ktSnippet{./snippets/TermsCreation.kt}

        \framebreak

        \item Factory methods always instantiate the most specific type possible:
        %
        \ktSnippet{./snippets/SpecificTermsCreation.kt}
    \end{itemize}

    \framebreak

    \begin{block}{Creating \kt{Integer}s}
        \begin{description}
            \item[\kt{Integer.of(\meta{Kotlin Integer Type})}] creates an \kt{Integer} out of a Kotlin integer
            \item[\kt{Integer.of(BigInteger)}] creates an \kt{Integer} out of a \kt{BigInteger}
            \item[\kt{Integer.of(String,Int)}] parses the string as an \kt{Integer} with the provided base
            \item[\kt{Integer.ZERO}] constant for the \kt{Integer} equal to 0
            \item[\kt{Integer.ONE}] constant for the \kt{Integer} equal to 1
            \item[\kt{Integer.MINUS\_ONE}] constant for the \kt{Integer} equal to -1
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Creating \kt{Real}s}
        \begin{description}
            \item[\kt{Real.of(\meta{Kotlin Floating Type})}] creates a \kt{Real} out of a Kotlin float
            \item[\kt{Real.of(BigInteger)}] creates a \kt{Real} out of a \kt{BigDecimal}
            \item[\kt{Real.of(String)}] parses the string as a \kt{Real}
            \item[\kt{Real.ZERO}] constant for the \kt{Real} equal to 0.0
            \item[\kt{Real.ONE}] constant for the \kt{Real} equal to 1.0
            \item[\kt{Real.MINUS\_ONE}] constant for the \kt{Real} equal to -1.0
            \item[\kt{Real.ONE\_HALF}] constant for the \kt{Real} equal to 0.5
            \item[\kt{Real.ONE\_TENTH}] constant for the \kt{Real} equal to 0.1
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Creating \kt{Atom}s}
        \begin{description}
            \item[\kt{Atom.of(String)}] creates an \kt{Atom} out of a string
            %
            \begin{itemize}\small
                \item returns a \kt{Truth} if \kt{"true"}, \kt{"false"}, or \kt{"fail"} is passed
                \item returns an \kt{EmptyList} if \kt{"[]"} is passed
                \item returns an \kt{EmptySet} if \kt{"\{\}"} is passed
            \end{itemize}
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Creating \kt{Var}iables}
        \begin{description}
            \item[\kt{Var.of(String)}] creates an \kt{Var}iable out of a string
            %
            \begin{itemize}\small
                \item the string is considered as the \kt{Var}iable's \alert{simple} name
                \item[!] there is \alert{no way} to create a \kt{Var}iable with a particular \alert{complete} name
            \end{itemize}

            \item[\kt{Var.anonymous()}] creates an anonymous \kt{Var}iable
        \end{description}
    \end{block}

    \ktSnippet{snippets/VarCreation.kt}

    \framebreak

    \begin{block}{Creating \kt{Struct}ures}
        \begin{description}
            \item[\kt{Struct.of(String,\meta{Container})}] creates an \kt{Struct}ure with the given functor and arguments
            %
            \begin{itemize}\small
                \item where \kt{\meta{Container}} may be an iterable, a sequence, or a varargs of \kt{Term}s
            \end{itemize}

            \item[\kt{Struct.template(String,Int)}] creates an \kt{Struct}ure with the given functor and arity, whose arguments are all anonymous variables

            \item[\kt{Struct.fold(String,\meta{Container},Term?)}] folds the terms in \kt{\meta{Container}} using the provided functor recursively, adopting either an explicit or implicit folding strategy depending on whether the last argument is null or not
        \end{description}
    \end{block}

    \ktSnippet[\tiny]{snippets/StructCreation.kt}

\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{Collection}s via Static Factories}
    \begin{block}{Creating \kt{List}s}
        \begin{description}
            \item[\kt{List.empty()}] creates an \kt{EmptyList}

            \item[\kt{Empty.list()}] creates an \kt{EmptyList}

            \item[\kt{List.of(\meta{Container})}] creates a \kt{[]}-terminated \kt{List} containing all the terms in \kt{\meta{Container}}
            %
            \begin{itemize}\small
                \item where \kt{\meta{Container}} may be an iterable, a sequence, or a varargs of \kt{Term}s
            \end{itemize}

            \item[\kt{List.from(\meta{Container},Term?)}] creates a \kt{List} containing all the terms in \kt{\meta{Container}} and terminated by either the last argument, if it is non-null, or be the last term in \kt{\meta{Container}}, otherwise

            \item[\kt{Cons.singleton(Term)}] creates \kt{List} containing just one item

            \item[\kt{Cons.of(Term,Term)}] creates a term of the form \kt{'.'($t_1$, $t_2$)} where $t_1,t_2$ are the first and second arguments, respectively
        \end{description}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/ListCreation.kt}

    \framebreak

    \begin{block}{Creating \kt{Tuple}s}
        \begin{description}
            \item[\kt{Tuple.of(Term,Term,\meta{Container})}] creates a \kt{Tuple} containing at least 2 terms, other than the ones in \kt{\meta{Container}}
            %
            \begin{itemize}\small
                \item where \kt{\meta{Container}} may be a (possibly empty) iterable, a sequence, or a varargs of \kt{Term}s
            \end{itemize}
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Creating \kt{Set}s}
        \begin{description}
            \item[\kt{Set.empty()}] creates an \kt{EmptySet}

            \item[\kt{Empty.set()}] creates an \kt{EmptySet}

            \item[\kt{Set.of(\meta{Container})}] creates a \kt{Set} containing all the terms in \kt{\meta{Container}}
            %
            \begin{itemize}\small
                \item where \kt{\meta{Container}} may be an iterable, a sequence, or a varargs of \kt{Term}s
            \end{itemize}
        \end{description}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{Clause}s via Static Factories}
    \begin{block}{Creating \kt{Clause}s}
        \begin{description}
            \item[\kt{Clause.of(Struct?,\meta{Container})}] creates either a \kt{Directive} or a \kt{Rule} depending on whether the provide \kt{Struct} is \kt{null} or not. In both cases items in \kt{\meta{Container}} compose the body of the clause, whereas the \kt{Struct} is an optional head
            %
            \begin{itemize}\small
                \item where \kt{\meta{Container}} may be an iterable, a sequence, or a varargs of \kt{Term}s
                \item[!] in any case, if \kt{\meta{Container}} contains at least 2 terms, a \kt{Tuple} is created behind the scenes
            \end{itemize}

            \item[\kt{Rule.of(Struct,\meta{Container})}] creates a \kt{Rule} using provided \kt{Struct} as head and the \emph{conjunction} of terms in \kt{\meta{Container}} as body
            %
            \begin{itemize}\small
                \item[!] returns a \kt{Fact} is \kt{\meta{Container}} is empty
            \end{itemize}

            \item[\kt{Fact.of(Struct)}] creates a \kt{Fact} given the \kt{Struct} acting as head
        \end{description}
    \end{block}
\end{frame}

\subsubsection{About \kt{Term}s' Design}

\begin{frame}[allowframebreaks]{Identity vs. Equalities}
    \begin{block}{Terms Identity}
        Two terms are \alert{identical} iff:
        %
        \begin{itemize}
            \item both are \kt{Integer}s having the same value
            \item both are \kt{Real}s having the same value
            \item both are \kt{Atom}s having the same value
            \item both are \kt{Var}iables having the same \alert{complete} name
            \item both are \kt{Struct}ures having the same
            %
            \begin{itemize}
                \item functor, and arity
                \item their arguments are pair-wise \alert{identical}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{itemize}
        \item Terms' \alert{identity} is tested via \kt{Term.equals(Any?)}
        \item or via \kt{Term.equals(Term, \alert{true})}
        \item or via \kt{$t_1$ == $t_2$} (because of \alert{Kotlin's operator overloading})
        %
        \begin{itemize}
            \item in Kotlin, objects' identity is tested via \kt{$t_1$ === $t_2$})
        \end{itemize}
    \end{itemize}

    \framebreak

    \begin{block}{Terms Equality}
        Two terms are \alert{equal} iff:
        %
        \begin{itemize}
            \item both are \kt{Integer}s having the same value
            \item both are \kt{Real}s having the same value
            \item both are \kt{Atom}s having the same value
            \item both are \kt{Var}iables having the same \alert{simple} name
            \item both are \kt{Struct}ures having the same
            %
            \begin{itemize}
                \item functor, and arity
                \item their arguments are pair-wise \alert{equal}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{itemize}
        \item Terms' \alert{equality} is tested via \kt{Term.equals(Term, \alert{false})}
    \end{itemize}

    \framebreak

    \begin{block}{Terms Structural Equality}
        Two terms are \alert{structurally equal} iff:
        %
        \begin{itemize}
            \item both are \kt{Numbers}s having the same value
            \item both are \kt{Atom}s having the same value
            \item both are \kt{Var}iables
            \item both are \kt{Struct}ures having the same
            %
            \begin{itemize}
                \item functor, and arity
                \item their arguments are pair-wise \alert{structurally equal}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{itemize}
        \item Terms' \alert{structural equality} is tested via \kt{Term.structurallyEquals(Term)}
    \end{itemize}

    \framebreak

    \ktSnippet{snippets/TermEqualities.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Total Ordering of Terms}
    \begin{block}{Overview}
        \begin{itemize}
            \item Terms are totally ordered
            \item Terms are comparable according to the default ordering
            \item Interface \kt{TermComparator} aims to compare terms according to some custom ordering
            \item \kt{TermComparator.DefaultComparator} implements the default ordering of terms
            \item \kt{Term.compareTo} exploits \kt{DefaultComparator} by default
        \end{itemize}
    \end{block}

    \begin{exampleblock}{Default ordering of terms}
        \[ \kt{Var} < \kt{Real} < \kt{Integer} < \kt{Atom} < \kt{Struct} \]
        %
        \begin{itemize}
            \item variables are lexicographically ordered by complete name
            \item numbers are ascendantly ordered by value
            \item atoms are lexicographically ordered by value
            \item structures are ordered by
            %
            \begin{enumerate}
                \item by arity, ascendantly
                \item then by functor, lexicographically
                \item then by $1^{st}$ argument
                \item then by $2^{nd}$ argument
                \item[\vdots]
            \end{enumerate}
        \end{itemize}
    \end{exampleblock}

    \framebreak

    \ktSnippet{snippets/TermOrdering.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Terms' Immutability}

    \begin{alertblock}{Takeaway}\centering
        All terms are \alert{immutable}
    \end{alertblock}

    \begin{block}{Consequences}
        \begin{itemize}
            \item Terms cannot be modified
            %
            \begin{itemize}
                \item[$\rightarrow$] terms are \alert{side-effect free}
                \item[$\rightarrow$] caching \& instance re-use can be exploited pervasively
                \item[$\rightarrow$] no concurrency issue
            \end{itemize}
            \item They must always be re-created from scratch, upon edit
            \item Editing a term implies creating a copy of that term
            \item Thus, many operations imply term copying:
            %
            \begin{itemize}
                \item assigning a value to a variable
                \item applying a substitution to a term
                \item altering some structure's arguments/functor
                \item refreshing some term's variables
                \item[\ldots]
            \end{itemize}

            \smallskip

            \item[!] Cloning a \alert{deep} term may be time consuming
        \end{itemize}
    \end{block}

    \begin{exampleblock}{About Cloning Lists}
        \begin{itemize}
            \item Lists are very likely to become very deep
            \item[$\rightarrow$] List cloning is made lazy to save computational resources
        \end{itemize}
    \end{exampleblock}
\end{frame}

\subsection{\kt{Var}iables and \kt{Scope}s}

\begin{frame}[allowframebreaks]{Conventions for \kt{Var}iables}
    \begin{block}{About Variables Creation}
        \begin{itemize}
            \item Variables are always created \alert{different}
            \item There is no way to create two equals variables
            %
            \begin{itemize}
                \item[!] this is deliberate
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{itemize}
        \item[$\rightarrow$] To create a term where the same variable occurs more than once\ldots
        %
        \begin{itemize}
            \item \ldots a reference to the variable should be locally saved somehow
        \end{itemize}
    \end{itemize}

    \framebreak

    \ktSnippet[\tiny]{snippets/VarReuse.kt}

\end{frame}

\begin{frame}[allowframebreaks]{The need for \kt{Scope}s}

    \begin{center}
        \includegraphics[width=0.35\linewidth]{img/scope.pdf}
    \end{center}

    \framebreak

    \begin{block}{\kt{Scope}s}\centering
        Scopes are \alert{factories} of terms allowing re-use of variables
    \end{block}

    \begin{alertblock}{Why \kt{Scope}s}
        \begin{itemize}
            \item Instances of \kt{Scope} expose methods to create \kt{Terms}
            \item Alternative to create \kt{Term}s via \alert{static factories}
            \item Instances of variables are cached \alert{by simple name}
            \item[$\rightarrow$] Purpose: reusing \kt{Var}iables while creating \kt{Term}s
        \end{itemize}
    \end{alertblock}

    \begin{description}
        \item[\kt{variables: Map<String, Var>}] returns all the \kt{Var}iables created so far in this \kt{Scope}, indexed by \emph{simple} name
        \item[\kt{varOf(String}: Var] returns a \kt{Var} having the provided simple, name possibly re-using some entry of \kt{variables}, if possible, or creating a new one, otherwise
        \item[\kt{anonymous(): Var}] alias for \kt{Var.anonymous}
        \item[\kt{atomOf(String): Atom}] alias for \kt{Atom.of}
        \item[\kt{structOf(String, \meta{Container}): Struct}] alias for \kt{Struct.of}
        %
        \begin{itemize}\small
            \item where \kt{\meta{Container}} may be an iterable, a sequence, or a varargs of \kt{Term}s
        \end{itemize}
        \item[\vdots]
    \end{description}
    %
    \begin{itemize}
        \item (one method exists in \kt{Scope} for each static factory described before)
    \end{itemize}

    \begin{block}{How to create \kt{Scope}s}
        \begin{description}
            \item[\kt{Scope.empty()}] creates a new empty \kt{Scope}

            \item[\kt{Scope.empty(Scope.()->R): R}] creates a new empty \kt{Scope} and accepts a lambda with receiver aimed at creating an object of type \kt{R} using that \kt{Scope}
            %
            \begin{itemize}
                \item can be used via the syntax \kt{Scope.empty \{ \meta{Code} \}} in Kotlin
            \end{itemize}
        \end{description}
    \end{block}

    \framebreak

    \ktSnippet{snippets/ScopeUsage.kt}
\end{frame}

\subsection{\kt{Substitution}s as First Class Entities}

\begin{frame}[allowframebreaks]{The \kt{Substitution} Type Hierarchy}
    \begin{center}
        \includegraphics[width=.8\linewidth]{img/substitutions.pdf}
    \end{center}

    \begin{block}{The \kt{Substitution} type}\centering
        \begin{center}
            Base type for all \alert{substitutions} i.e. assignments of \kt{Var}iables to \kt{Term}s
        \end{center}
        %
        \begin{itemize}
            \item \kt{Substitution} is a sub-type of \kt{Map<Var, Term>}

            \item There are two sub-types of \kt{Substitution}:
            %
            \begin{itemize}
                \item \alert{\kt{Unifier}s}, actually mapping a (possibly empty) set of \kt{Var}s to their corresponding \kt{Term}
                %
                \begin{itemize}
                    \item[ie] an object of the form \kt{\{$v_1$=$t_1$, \ldots, $v_n$=$t_n$\}} where $t \geq 0$, all $v_i$ are \kt{Var}iables, and all $t_i$ are \kt{Term}s
                    \item[!] the empty mapping is an admissible unifier
                \end{itemize}
                \item \alert{\kt{Fail}}, representing the \alert{failed} substitution
            \end{itemize}

            \item Both \kt{Unifier} and \kt{Fail} are nested types of \kt{Substitution}
        \end{itemize}
    \end{block}

    \begin{description}
        \item[\kt{isSuccess: Boolean}] checks whether the current \kt{Substitution} is a \kt{Unifier}
        \item[\kt{isFail: Boolean}] checks whether the current \kt{Substitution} is \kt{Fail}ed
        \item[\kt{getByName(String): Term?}] gets the value of a \kt{Var}iable by its \emph{simple} name
        \item[\kt{plus(Substitution): Substitution}] merges the current \kt{Substitution} with the provided one (a third one is created)
        \item[\kt{minus(\meta{Container}): Substitution}] returns a knew \kt{Substitution} \alert{not} containing any \kt{Var} contained in \kt{\meta{Container}}
        %
        \begin{itemize}\small
            \item where \kt{\meta{Container}} is an iterable, sequence, or varargs of \kt{Var}iables
        \end{itemize}
        \item[\kt{minus(Substitution): Substitution}]  returns a knew \kt{Substitution} \alert{not} containing any \kt{Var} contained in the provided \kt{Substitution}
        \item[\kt{filter(\meta{Container}): Substitution}] returns a knew \kt{Substitution} containing \alert{only} the \kt{Var}iables contained in the provided \kt{\meta{Container}}
        \item[\kt{filter(\meta{Predicate}): Substitution}] returns a knew \kt{Substitution} containing \alert{only} the \kt{Var}iables contained for which \kt{\meta{Predicate}} is \kt{true}
    \end{description}
    %
    \begin{itemize}
        \item[+] methods \& properties of \kt{Map} such as \kt{get}, \kt{size}, etc.
    \end{itemize}

    \framebreak

    \begin{alertblock}{\kt{Substitution}s can be merged}
        Assuming that:
        %
        \begin{itemize}
            \item $U_1 = $ \kt{\{$X_1$=$t_1$, \ldots, $X_n$=$t_n$\}} is a unifier
            \item $U_2 = $ \kt{\{$Y_1$=$t'_1$, \ldots, $Y_m$=$t'_m$\}} is another unifier
            \item $\bot$ denotes the failed substitution
        \end{itemize}
        %
        \[U_1 + U_2 = \begin{cases}
            \text{\kt{\{$X_1$=$t_1$, \ldots, $X_n$=$t_n$, $Y_1$=$t'_1$, \ldots, $Y_m$=$t'_m$\}}} \\
            \qquad\text{ if } \nexists i,j : X_i = Y_j \\
            \text{\kt{\{$X_1$=$t_1$, \ldots, $Y_i$=$t'_j$, \ldots, $Y_m$=$t'_m$\}}} \\
            \qquad\text{ if } \forall i,j : X_i = Y_j \implies t_i = t'_j\\
            \bot \text{ otherwise }
        \end{cases}\]
        %
        \[ U_1 + \bot = \bot + U_2 = \bot \]
    \end{alertblock}

    \ktSnippet[\tiny]{snippets/SubstitutionUsage.kt}

\end{frame}

\begin{frame}{Creating \kt{Substitution}s}
    \begin{block}{Static factories for \kt{Substitution}s}
        \begin{description}
            \item[\kt{Substitution.failed()}] return an instance of \kt{Fail}
            %
            \item[\kt{Substitution.of(\meta{KeyValuePairs})}] creates a new \kt{Substitution} using the provided key-value pairs, where
            %
            \begin{itemize}\small
                \item keys can be either strings or \kt{Var}s
                \item values can be arbitrary \kt{Term}s
                \item multiple pairs can be provided
                \item if the same \kt{Var} is assigned to different \kt{Term}s, an instance of \kt{Fail} is returned
            \end{itemize}

            \item[\kt{Substitution.unifier(\meta{KeyValuePairs})}] creates a new \kt{Unifier} using the provided key-value pairs, where
            %
            \begin{itemize}\small
                \item if the same \kt{Var} is assigned to different \kt{Term}s, a \alert{\kt{SubstitutionException}} is thrown
            \end{itemize}
        \end{description}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{Applying Substitutions to Terms}
    \begin{block}{Definition and Notation}
        Let
        \begin{itemize}
            \item $t$ be a term
            \item $U = $ \kt{\{$X_1$=$t_1$, \ldots, $X_n$=$t_n$\}} be a unifier
        \end{itemize}
        then we denote by
        \[t' = t[U]\]
        the term attained by \alert{applying} $U$ to $t$.
        %
        \begin{itemize}
            \item $t'$ has the same structure of $t$\ldots
            \item \ldots except each occurrence of $X_i$ is replaced by $t_i$
        \end{itemize}
    \end{block}

    \begin{alertblock}{Notable Cases}
        \begin{itemize}
            \item Applying the failed substitution $\bot$ to any term $t$ makes no sense
            \item If $x$ is \alert{ground} then $x[U] = x$, $\forall U$
        \end{itemize}
    \end{alertblock}

    \begin{block}{In practice}
        Let $t$ denote a \kt{Term} and $s$ denote a \kt{Substitution}:
        \begin{description}
            \item[\kt{$t$.apply(Substitution): Term}] returns a new \kt{Term} attained by applying the provided \kt{Substitution} to $t$
            %
            \begin{itemize}\small
                \item may throw a \alert{\kt{SubstitutionApplicationException}} if the \kt{Substitution} is an instance of \kt{Fail} at run time
            \end{itemize}

            \item[\kt{$t$.get(Substitution): Term}] is an alias for \kt{$t$.apply}
            %
            \begin{itemize}
                \item this can be invoked via the syntax \alert{\kt{$t$[$s$]}} in Kotlin
            \end{itemize}

            \item[\kt{$s$.applyTo(Term)}: Term] returns a new \kt{Term} attained by applying $s$ to the provided \kt{Term}
            %
            \begin{itemize}\small
                \item may throw a \alert{\kt{SubstitutionApplicationException}} if the $s$ is an instance of \kt{Fail} at run time
            \end{itemize}
        \end{description}
    \end{block}

    \ktSnippet[\tiny]{snippets/SubstitutionApplication.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Refreshing Terms}
    \begin{block}{Definition and Notation}
        Let $t$ be a \kt{Term} and suppose that $t$:
        %
        \begin{itemize}
            \item is \alert{compound} (i.e. it is a \kt{Struct})
            \item it contains some \kt{Var}iables $X_1$, \ldots, $X_n$
        \end{itemize}
        %
        then \alert{refreshing} $t$ means creating another term $t'$ such that:
        %
        \begin{itemize}
            \item $t'$ has the same structure of $t$
            \item each occurrence of $X_i$ is replaced by $X'_i$, where
            %
            \begin{itemize}
                \item $X'_i$ is a fresh variable s.t. $X'_i \neq X_i$
                \item $X'_i$ has the same name of $X_i$
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{alertblock}{Notable Cases}
        \begin{itemize}
            \item If $t$ is \alert{ground} then refreshing $t$ leaves it unaffected
        \end{itemize}
    \end{alertblock}

    \begin{block}{In practice}
        Let $t$ denote a \kt{Term}:
        %
        \begin{description}
            \item[\kt{$t$.freshCopy(): Term}] returns a new \kt{Term} attained by refreshing $t$
            %
            \begin{itemize}\small
                \item the new \kt{Term} is guaranteed to only contain \kt{Var}iables which have \alert{never} been used before
            \end{itemize}
            \item[\kt{$t$.freshCopy(Scope): Term}] returns a new \kt{Term} attained by refreshing $t$ using the provided \kt{Scope}
            %
            \begin{itemize}\small
                \item if the provided \kt{Scope} already contains some \kt{Var}iable whose simple name is exploited within $t$, then is that \kt{Var}iable is reused
            \end{itemize}
        \end{description}
    \end{block}

    \ktSnippet[\tiny]{snippets/TermRefreshing.kt}
\end{frame}

\subsection{\kt{Operator}s and \kt{OperatorSet}s}

\begin{frame}[allowframebreaks]{Prolog-like Operators}

    \begin{center}
        \includegraphics[width=0.9\linewidth]{img/operators.pdf}
    \end{center}

    \framebreak

    \begin{block}{Definition}
        A Prolog-like \kt{Operator} is an algebraic object composed by 3 fields:
        %
        \begin{description}
            \item[\kt{functor: String}] i.e. the operator's symbol
            \item[\kt{priority: Int}] where lower integers correspond to higher priorities
            %
            \begin{itemize}\small
                \item conventionally, 0 is \alert{max} priority, 1200 is \alert{min} priority
            \end{itemize}
            \item[\kt{specifier: Specifier}] is a descriptor of the operator's
            %
            \begin{description}\small
                \item[arity] i.e. the amount of arguments it takes (either binary or unary)
                \item[position] w.r.t. arguments (prefix, postfix, or infix)
                \item[associativity] e.g. either right- or left-associative, or non-associative
            \end{description}
        \end{description}
    \end{block}

    \begin{block}{About \kt{Specifier}s}
        \begin{itemize}
            \item \kt{Specifier} is an \emph{enum} with 7 constants

            \item Each one is a combination of 3 letters:
            %
            \begin{description}\small
                \item[F] denoting the operator
                \item[X] denoting an expression having \alert{strictly higher} priority
                \item[Y] denoting an expression having \alert{higher or equal} priority
            \end{description}

            \item Each one describes an operator's arity, position, and associativity:
            %
            \medskip
            %
            \input{tab-specifiers.tex}
        \end{itemize}
    \end{block}

    \begin{block}{Creating \kt{Operator}s}
        \begin{description}
            \item[\kt{Operator(String, Specifier, Int)}] creates a new \kt{Operator} having the provided functor, specifier, and priority
            \item[\kt{Operator.fromTerm(Integer, Atom, Atom): Operator?}] creates a new \kt{Operator} having the provided priority, specifier, and functor---provided as \kt{Term}s
            %
            \begin{itemize}\small
                \item the $2^{nd}$ argument must be one \kt{Atom} among \pl{fx}, \pl{fy}, \pl{xf}, \pl{yf}, \pl{xfx}, \pl{yfx}, or \pl{xfy}
                \item returns \kt{null} otherwise
            \end{itemize}
            \item[\kt{Operator.fromTerm(Struct): Operator}] creates a new \kt{Operator} out of a \kt{Struct} of the form \pl{op($p$, $s$, $f$)}
             %
            \begin{itemize}\small
                \item where $p$ must be an \kt{Integer}
                \item and $s$ be one \kt{Atom} among \pl{fx}, \pl{fy}, \pl{xf}, \pl{yf}, \pl{xfx}, \pl{yfx}, or \pl{xfy}
                \item returns \kt{null} otherwise
            \end{itemize}
        \end{description}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{The meaning of \kt{Specifier}s}

    \begin{exampleblock}{How two interpret \textbf{prefix} specifiers \kt{FX} and \kt{FY}}
        \begin{itemize}
            \item If \pl{f} and \pl{g} are operators of type \kt{FY}, and \pl{T} is a term:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{f g T}} only if $priority(\pl{g}) \leq priority(\pl{f})$
                    \item can be written as \alert{\pl{f(g T)}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(T))}} or \alert{\pl{g(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{f f T}} or \alert{\pl{g g T}}
                \end{itemize}
            \end{itemize}

            \item Otherwise, if \pl{f} and \pl{g} are operators of type \kt{FX}:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{f g T}} only if $priority(\pl{g}) < priority(\pl{f})$
                    \item can be written as \alert{\pl{f(g T)}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(T))}}, or \alert{\pl{g(g(T))}}
                %
                \begin{itemize}
                    \item can \alert{never} be written as \alert{\pl{f f T}} or \alert{\pl{g g T}}
                    \item but can be written as \alert{\pl{f(f T)}} or \alert{\pl{g(g T)}}
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}

    \begin{exampleblock}{How two interpret \textbf{postfix} specifiers \kt{XF} and \kt{YF}}
        \begin{itemize}
            \item If \pl{f} and \pl{g} are operators of type \kt{YF}, and \pl{T} is a term:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{T g f}} only if $priority(\pl{g}) \leq priority(\pl{f})$
                    \item can be written as \alert{\pl{(T g) f}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(T))}} or \alert{\pl{g(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{T f f}} or \alert{\pl{T g g}}
                \end{itemize}
            \end{itemize}

            \item Otherwise, if \pl{f} and \pl{g} are operators of type \kt{XF}:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(T))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{T g f}} only if $priority(\pl{g}) < priority(\pl{f})$
                    \item can be written as \alert{\pl{(T g) f}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(T))}}, or \alert{\pl{g(g(T))}}
                %
                \begin{itemize}
                    \item can \alert{never} be written as \alert{\pl{T f f}} or \alert{\pl{T g g}}
                    \item but can be written as \alert{\pl{(T f)f}} or \alert{\pl{(T g)g}}
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}

    \begin{exampleblock}{How two interpret \textbf{infix} specifiers \kt{YFX} and \kt{XFY}}
        \begin{itemize}
            \item If \pl{f} and \pl{g} are operators of type \kt{YFX}, and \pl{A}, \pl{B}, and \pl{C} are terms:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(A, B), C)}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B g C}} only if $priority(\pl{g}) \leq priority(\pl{f})$
                    \item can be written as \alert{\pl{(A f B) g C}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(A, B), C)}} or \alert{\pl{g(g(A, B), C)}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B f C}} or \alert{\pl{A g B g C}}
                \end{itemize}
            \end{itemize}

            \item Conversely, if \pl{f} and \pl{g} are operators of type \kt{XFY}:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(A, g(B, C))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B g C}} only if $priority(\pl{g}) \leq priority(\pl{f})$
                    \item can be written as \alert{\pl{A f (B g C)}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(A, f(B, C))}} or \alert{\pl{g(A, g(B, C))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B f C}} or \alert{\pl{A g B g C}}
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}

    \begin{exampleblock}{How two interpret the \textbf{infix} specifier \kt{XFX}}
        \begin{itemize}
            \item If \pl{f} and \pl{g} are operators of type \kt{XFX}, and \pl{A}, \pl{B}, and \pl{C} are terms:
            %
            \begin{itemize}
                \item expressions of the form \alert{\pl{f(g(A, B), C)}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B g C}} only if $priority(\pl{g}) < priority(\pl{f})$
                    \item can be written as \alert{\pl{(A f B) g C}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(f(A, B), C)}} or \alert{\pl{g(g(A, B), C)}}
                %
                \begin{itemize}
                    \item can \alert{never} be written as \alert{\pl{A f B f C}} or \alert{\pl{A g B g C}}
                    \item but can be written as \alert{\pl{(A f B) f C}} or \alert{\pl{(A g B) g C}}
                \end{itemize}

                \item expressions of the form \alert{\pl{f(A, g(B, C))}}
                %
                \begin{itemize}
                    \item can be written as \alert{\pl{A f B g C}} only if $priority(\pl{g}) < priority(\pl{f})$
                    \item can be written as \alert{\pl{A f (B g C)}} otherwise
                \end{itemize}

                \item expressions of the form \alert{\pl{f(A, f(B, C))}} or \alert{\pl{g(A, g(B, C))}}
                %
                \begin{itemize}
                    \item can \alert{never} be written as \alert{\pl{A f B f C}} or \alert{\pl{A g B g C}}
                    \item but can be written as \alert{\pl{A f (B f C)}} or \alert{\pl{A g (B g C)}}
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
\end{frame}

\begin{frame}[allowframebreaks]{Sets of Operators}
    \begin{block}{The \kt{OperatorSet} typ is a subtype of \kt{Set<Operator>}}
        An \kt{OperatorSet} is simply a set of \kt{Operator}s (no duplicates admitted)
        %
        \begin{itemize}
            \item the \kt{OperatorSet} is \alert{immutable}
            \item operations exist to add/remove/check \kt{Operator}s within \kt{OperatorSet}s
            \item operations exists to \alert{merge} \kt{OperatorSet}s
            \item adding/removing operators implies \alert{creating a copy} of the whole set
        \end{itemize}
    \end{block}

    \framebreak

    Several notable \kt{OperatorSet} exists:
    %
    \begin{itemize}
        \item[eg] one for arithmetic operators:
            \\\medskip\input{tab-operators-arithmetic.tex}

        \framebreak

        \item[eg] one for arithmetic comparison operators:
            \\\medskip\input{tab-operators-arithmetic-comparison.tex}

        \framebreak

        \item[eg] one for term comparison operators:
            \\\medskip\input{tab-operators-term-comparison.tex}

        \framebreak

        \item[eg] one for logic connectors:
            \\\medskip\input{tab-operators-logic.tex}

        \framebreak

        \item[eg] one for clause-related operators:
            \\\medskip\input{tab-operators-clauses.tex}

        \framebreak

        \item[eg] one containing all the aforementioned (ISO Prolog Standard compliant) operators:
            \\\medskip\input{tab-operators-standard.tex}
    \end{itemize}

    \begin{block}{Creating an \kt{OperatorSet}}
        \begin{description}\small
            \item[\kt{OperatorSet(\meta{Container})}] creates a novel set out of some operators
            %
            \begin{itemize}\scriptsize
                \item where \kt{\meta{Container}} may be an iterable, sequence, or varargs of \kt{Operator}s
            \end{itemize}
            \item[\kt{OperatorSet.EMPTY}] references an empty set
            \item[\kt{OperatorSet.ARITHMETIC}] references a set containing arithmetic operators
            \item[\kt{OperatorSet.ARITHMETIC\_COMPARISON}] references a set containing arithmetic comparison operators
            \item[\kt{OperatorSet.TERM\_COMPARISON}] references a set containing term comparison operators
            \item[\kt{OperatorSet.CONTROL\_FLOW}] references a set containing logic connectors
            \item[\kt{OperatorSet.CLAUSES}] references a set containing clause-related operators
            \item[\kt{OperatorSet.STANDARD}] references a set containing all the aforementioned operators
        \end{description}
    \end{block}
\end{frame}

\subsection{Pattern Matching over \kt{Term}s Types}

\begin{frame}[allowframebreaks]{\kt{TermVisitor}s and their Use Cases}

    \begin{block}{About \kt{TermVisitor}s}
        \begin{itemize}
            \item Visitor pattern\footnote{\url{https://en.wikipedia.org/wiki/Visitor_pattern}} applied to \kt{Term}
            \item Supports use cases where a particular operation must be performed depending on the actual type of a \kt{Term}
            \item Essentially, a form of \alert{dynamic dispatch}\footnote{\url{https://en.wikipedia.org/wiki/Dynamic_dispatch}}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{./snippets/TermVisitor.kt}

    \framebreak

    \begin{block}{\kt{TermVisitor}s' contract}
        \begin{itemize}
            \item An instance of \kt{TermVisitor<\textit{T}>} $v$ can be applied to a term $t$ via
            %
            \begin{center}
                \kt{$t$.accept($v$)}
            \end{center}

            \item This returns an object of type \kt{\textit{T}} \ldots

            \item \ldots attained via the most adequate method \kt{visit\meta{Type}} of $v$
            %
            \begin{itemize}
                \item where \kt{\meta{Type}} is the most specific type matching the run-time type of $t$
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{block}{Implementors of \kt{TermVisitor}s}
        \begin{itemize}
            \item May override \kt{defaultValue} to handle the general case
            \item Then override some \kt{visit\meta{Type}} method to handle the particular case of \kt{\meta{Type}}
        \end{itemize}
    \end{block}

    \ktSnippet{./snippets/TermVisitorUsage.kt}
\end{frame}

\subsection{Formatting \kt{Term}s}

\begin{frame}[allowframebreaks]{The \kt{TermFormatter} Type}

    \begin{center}
        \includegraphics[width=0.7\linewidth]{img/term-visitor.pdf}
    \end{center}

    \framebreak

    \begin{block}{About \kt{TermFormatter}s}
        \begin{itemize}
            \item \kt{TermFormatter}s aim at \alert{presenting} terms and clauses as \kt{string}s
            \item Many predefined formatters exist, serving disparate use cases
            %
            \begin{itemize}
                \item configurable via \kt{enums}
            \end{itemize}
        \end{itemize}
    \end{block}

    % \ktSnippet{./snippets/TermFormatter.kt}
\end{frame}

\begin{frame}[allowframebreaks]{\kt{TermFormatter} enums}
    % Three \kt{enum}s exist to support many possible way to present \kt{Term}s:
    % %
    % \ktSnippet{./snippets/TermFormatterEnums.kt}

    \begin{block}{\kt{VarFormat} dictates how \kt{Var}iables are represented}
        \begin{description}
            \item[\kt{COMPLETE\_NAME}] represent variables by \alert{complete} name
            \item[\kt{UNDERSCORE}] represent all variables in the form \kt{\_\meta{Integer}}
            \item[\kt{PRETTY}] represent all variables by \alert{simple} name
            %
            \begin{itemize}\small
                \item progressively renames homonymous variables
                %
                \begin{itemize}\scriptsize
                    \item[eg] \pl{X}, \pl{X1}, \pl{X2}, etc
                \end{itemize}
            \end{itemize}
        \end{description}
    \end{block}

    \begin{block}{\kt{OpFormat} dictates how \kt{Operator}s are treated}
        \begin{description}
            \item[\kt{IGNORE\_OPERATORS}] all \kt{Struct}ures are represented in canonical form:
            \begin{center}
                \pl{\meta{Functor}(\meta{Args})}
            \end{center}
            no matter what, including \kt{Collection}s
            \item[\kt{COLLECTIONS}] like the above, except
            %
            \begin{itemize}
                \item lists are represented in square-brackets form
                \item tuples are represented in round-parentheses form
                \item sets are represented in curly-brackets form
            \end{itemize}
            \item[\kt{EXPRESSIONS}] like the above except that \kt{Struct}ures matching some operator definition are represented in infix, prefix, or infix form, using parentheses only if required
            %
            \begin{itemize}\small
                \item this requires an \kt{OperatorSet} to be specified
            \end{itemize}
        \end{description}
    \end{block}

    \begin{block}{\kt{FuncFormat} dictates how \kt{Struct}ures' functors are represented}
        \begin{description}
            \item[\kt{QUOTED\_IF\_NECESSARY}] enquotes functors if they are not well formed, escaping non-readable characters
            \item[\kt{LITERAL}] represents functors literally, without any enquoting or escaping
        \end{description}
    \end{block}

    \begin{block}{The \kt{numberVars: Boolean} flag}
        Some \kt{TermFormatter} initialisers come with a \kt{numberVars} argument:
        \begin{description}
            \item[when \kt{true}] structures of the form
            %
            \begin{center}
                \pl{'\$VAR'($i$)}
            \end{center}
            where $i$ is a non-negative \kt{Integer} are represented as the \kt{Var}iable named after the $i^{th}$ letter of the alphabet
            %
            \begin{itemize}\small
                \item \pl{'\$VAR'(0)} $\rightarrow$ \pl{A}, \pl{'\$VAR'(1)} $\rightarrow$ \pl{B}, etc.
            \end{itemize}
            \item[when \kt{false}] they are represented as ordinary \kt{Struct}ures
        \end{description}
    \end{block}

    % \ktSnippet{./snippets/TermFormatter.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{TermFormatter}s}
    Static factories for \kt{TermFormatter}s:
    %
    \small
    \begin{description}
        \item[\kt{TermFormatter.of(VarFormat,OpFormat,FuncFormat,Boolean,OperatorSet)}] returns a new formatter using the provided options and operators
        \item[\kt{TermFormatter.default(OperatorSet)}] creates a new formatter using the provided operators and the following settings:
        %
        \begin{itemize}\scriptsize
            \item \kt{VarFormat.UNDERSCORE}, \kt{OpFormat.EXPRESSIONS}, \kt{FuncFormat.LITERAL}
            \item \kt{numberVars = true}
        \end{itemize}
        \item[\kt{TermFormatter.canonical()}] creates a new formatter using the following settings:
        %
        \begin{itemize}\scriptsize
            \item \kt{UNDERSCORE}, \kt{IGNORE\_OPERATORS}, \kt{QUOTED\_IF\_NECESSARY}
            \item \kt{numberVars = false}
        \end{itemize}
        \item[\kt{TermFormatter.readable(OperatorSet)}] creates a new formatter using the provided operators and the following settings:
        %
        \begin{itemize}\scriptsize
            \item \kt{PRETTY}, \kt{EXPRESSIONS}, \kt{QUOTED\_IF\_NECESSARY}
            \item \kt{numberVars = false}
        \end{itemize}
        \item[\kt{TermFormatter.prettyVariables()}] like \kt{canonical}, but with:
        %
        \begin{itemize}\scriptsize
            \item \kt{VarFormat.PRETTY}, \kt{OpFormat.COLLECTIONS}
        \end{itemize}
        \item[\kt{TermFormatter.prettyExpressions(Boolean, OperatorSet)}] creates a new formatter using the provided operators and the following settings:
        %
        \begin{itemize}\scriptsize
            \item \kt{VarFormat.PRETTY} if the $1^{st}$ argument is \kt{true}, \kt{COMPLETE\_NAMES} otherwise
            \item \kt{OpFormat.EXPRESSIONS}, \kt{FuncFormat.QUOTED\_IF\_NECESSARY}
            \item \kt{numberVars = false}
        \end{itemize}
    \end{description}
\end{frame}

\begin{frame}{Formatting \kt{Term}s}
    \ktSnippet[\tiny]{snippets/TermFormatting.kt}
\end{frame}

\subsection{Exceptions}

\begin{frame}[allowframebreaks]{Exceptions in \twopkt{}}

    \begin{center}
        \includegraphics[width=0.7\linewidth]{img/exception.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{TuPrologException} type is a sub-type of \kt{RuntimeException}}\centering
        Base type for all custom exceptions possibly occurring in \twopkt{}
    \end{block}

    \begin{alertblock}{Important convention}\centering
        Custom exceptions possibly defined into any \twopkt{} module must directly or indirectly be sub-types of \kt{TuPrologException}
    \end{alertblock}

    \framebreak

    \begin{block}{Sub-types of \kt{TuPrologException} in \module{core}}
        \begin{description}
            \item[\kt{SubstitutionException}] thrown when attempting to create a \kt{Unifier} out of contradictory assignments
            %
            \begin{itemize}\small
                \item e.g. the same \kt{Var} is assigned to different \kt{Term}s
            \end{itemize}

            \item[\kt{SubstitutionApplicationException}] thrown when attempting to apply a \kt{Fail}ed substitution to a \kt{Term}
        \end{description}
    \end{block}
\end{frame}

\section{Logic Unification: the \module{unify} Module}

\subsection{The \kt{Unificator} type}

\begin{frame}[allowframebreaks]{The \kt{Unificator} type}

    \begin{center}
        \includegraphics[width=0.8\linewidth]{img/unify.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{Unificator} type}\centering
        Matches two terms by finding a suitable substitution to their variables, i.e. the \emph{most general unifier} (MGU)
    \end{block}
    %
    \begin{description}
        \item[\kt{mgu(Term, Term): Substitution}] returns the MGU between two \kt{Terms} if a substitution is found, or a \kt{Fail} object otherwise
        \item[\kt{match(Term, Term): Boolean}] checks if two \kt{Terms} can be unified
        \item[\kt{unify(Term, Term): Term?}] tries to unify two \kt{Terms}, possibly returning the unified Term as a result
        \item[\kt{merge(Substitution, Substitution): Substitution}] merges two \kt{Substitution}s with occurs check enabled
    \end{description}
\end{frame}

\subsection{Default \kt{Unificator}s}

\begin{frame}[allowframebreaks]{Creating \kt{Unificator}s}
    Main \kt{Unificator} static factories:
    \begin{description}
        \item[\kt{naive(): Unificator}] unifies terms based on their \kt{Term.equals} method, while numbers are compared by value
        \item[\kt{strict(): Unificator}] unifies terms based uniquely on their \kt{Term.equals} methods
        \item[\kt{cached(Unificator, Int): Unificator}] makes another \kt{Unificator} cached, memorizing the most recent \kt{Term}s unified through it (according to the given cache size)
        \item[\kt{default: Unificator}] returns a \kt{cached}, \kt{strict} unificator
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks, fragile]{Using \kt{Unificator}s}

    General unification strategy:
    %
    \bigskip
    %
    \input{tab-unification}
    %
    \bigskip
    %
    \begin{itemize}
        \item[!] implementations may alter the way terms are compared
    \end{itemize}

    \framebreak

    Successful unification with \kt{default}:
    %
    \ktSnippet[\tiny]{./snippets/UnificatorDefault.kt}

    \framebreak

    Successful unification with \kt{default} (no bindings):
    %
    \ktSnippet[\tiny]{./snippets/UnificatorDefaultEmpty.kt}

    \framebreak

    Failed unification with \kt{default}:
    %
    \ktSnippet[\tiny]{./snippets/UnificatorFailure.kt}

    \framebreak

    Unification with \kt{cached} unificator:
    %
    \ktSnippet[\tiny]{./snippets/UnificatorCached.kt}

    % examples with default unificators + infix operators
\end{frame}

\subsection{Custom \kt{Unificator}s}

\begin{frame}[allowframebreaks, fragile]{Custom \kt{Unificator}s}
    \begin{block}{Writing custom \kt{Unificator}s}
        \begin{itemize}
            \item create an instance of the \kt{AbstractUnificator} type
            \item override \kt{checkTermsEquality} method
            %
            \begin{itemize}
                \item[!] checking whether the two provided \kt{Term}s are matching
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    E.g. unifying numbers by their absolute value:
    %
    \ktSnippet[\tiny]{./snippets/UnificatorCustom.kt}

\end{frame}

\subsection{Infix operators}

\begin{frame}[allowframebreaks, fragile]{Infix operators}
    \begin{block}{Infix operators: \kt{unifyWith}, \kt{matches}, \kt{mguWith}}
        \begin{itemize}
            \item defined in \kt{Unificator}'s companion object
            \item built as functions with receivers
            \item enable streamlined, DSL-like unification
        \end{itemize}
    \end{block}
    %
    \ktSnippet[\tiny]{./snippets/UnificatorInfix.kt}
\end{frame}

\section{Storing and Indexing Clauses: the \module{theory} Module}

\subsection{Clause Collections}

\begin{frame}[allowframebreaks]{Collections Design}
    \begin{block}{Clause Collections}
        \begin{itemize}
            \item manage the storage of \kt{Clause}s
            \item provide methods for addition and removal of clauses
            \item designed as \kt{Iterable} subtypes
        \end{itemize}
    \end{block}
    %
    \begin{block}{Two dimensions: \textit{mutability} and \textit{ordering}}
        \begin{itemize}
            \item our design tackles both issues
            \item \textit{mutable} collections can be modified in-place
            \item \textit{ordered} collections keep track of the order of insertion
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{ClauseCollection} Type Hierarchy}

    \begin{center}
        \includegraphics[width=\linewidth]{img/clause-collections.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{ClauseCollection} interface}
        \begin{itemize}
            \item defines typical insertion and removal operations
            \item method names similar to Java Collections
            \begin{itemize}
                \item [!] following the \textit{least astonishment principle}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{add(Clause): ClauseCollection}] returns a new collection containing the given clause and the existing ones
        \item[\kt{retrieve(Clause): RetrieveResult<ClauseCollection>}] tries to remove the given clause from the collection
        \item[\kt{contains(Clause): Boolean}] checks if the collection contains the given clause
        \item[\kt{size: Int}] computes the size of the collection
        \item[\kt{isEmpty(): Boolean}] checks if the collection contains any clauses
        \item[\kt{iterator(): Iterator<Clause>}] returns the collection's iterator
    \end{description}

    \framebreak

    \begin{block}{The \kt{RetrieveResult} type}
        \begin{itemize}
            \item represents the output of a \kt{retrieve(Clause)} call
            \item can be a \kt{Success} or \kt{Failure}
        \end{itemize}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.8\linewidth]{img/retrieve-result.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{MutableClauseCollection} interface}
        \begin{itemize}
            \item subtype of \kt{ClauseCollection}
            \item insertions and removals are performed \textbf{in-place}
            \begin{description}
                \item [!] same collection is returned after any operation
            \end{description}
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{add(Clause): MutableClauseCollection}] adds a new clause to this collection
        \item [\kt{retrieve(Clause): RetrieveResult<MutableClauseCollection>}] tries to remove the given clause from this collection
    \end{description}

    \framebreak

    \begin{block}{Clause Queues}
        \begin{itemize}
            \item \textbf{preserve} the \textbf{ordering} of clauses
            \begin{description}
                \item [!] according to their \textit{insertion} order
            \end{description}
            \item store clauses in a \textit{queue}-like structure
            \item defined by the \kt{ClauseQueue} and \kt{MutableClauseQueue} types
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{addFirst(Clause): ClauseQueue}] adds a clause in the \textit{first} position to the collection
        \item[\kt{add/addLast(Clause): ClauseQueue}]  adds a clause in the \textit{last} position to the collection
        \item[\kt{getFifoOrdered(Clause): Sequence<Clause>}] produces a sequence of clauses unifying with the given one, searching \textit{from first to last}
        \item[\kt{getLifoOrdered(Clause): Sequence<Clause>}] produces a sequence of clauses unifying with the given one, searching \textit{from last to first}
    \end{description}

    \framebreak

    \begin{block}{Clause Multisets}
        \begin{itemize}
            \item ignore clause ordering
            \item useful when many clauses may match the goal
            \item defined by the \kt{ClauseMultiSet} and \kt{MutableClauseMultiSet} types
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{count(Clause): Long}] computes the number of clauses unifying with the given one
        \item[\kt{get(Clause): Sequence<Clause>}] produces a sequence of clauses that unify with the given one
        \begin{description}
            \item[!] equivalent to the \kt{[]} operator
        \end{description}
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{ClauseCollection}s}
    Main \kt{ClauseCollection} static factories:
    %
    \begin{description}
        \item[\kt{emptyMultiSet(): ClauseMultiSet}] creates an empty \kt{ClauseMultiset}
        \item[\kt{multiSetOf(Iterable<Clause>): ClauseMultiSet}] creates a \kt{ClauseMultiSet} from the given clauses
        \item[\kt{emptyQueue(): ClauseQueue}] creates an empty \kt{ClauseQueue}
        \item[\kt{queueOf(Iterable<Clause>): ClauseQueue}] creates a \kt{ClauseQueue} from the given clauses
    \end{description}
    %
    These factories return \textit{immutable} collections by default

    \framebreak

    \kt{ClauseQueue} and \kt{ClauseMultiSet} provide three main static factories:
    %
    \begin{description}
        \item[\kt{empty()}: C] creates an empty \kt{C}
        \item[\kt{of(Iterable<Clause>)}: C] creates a \kt{C} from the given clauses
        \item[\kt{of(vararg Clause)}: C] creates a \kt{C} from the given clauses
    \end{description}
    %
    with \kt{C} being either \kt{ClauseQueue} or \kt{ClauseMultiSet}
\end{frame}

\begin{frame}[allowframebreaks]{Using \kt{ClauseCollection}s}
    Ordering a \kt{ClauseQueue}:
    %
    \ktSnippet{./snippets/QueueOrdering.kt}

    \framebreak

    Populating a \kt{ClauseQueue}:
    %
    \ktSnippet{./snippets/QueuePopulate.kt}

    \framebreak

    Retrieving clauses from a \kt{ClauseQueue}:
    %
    \ktSnippet{./snippets/QueueRetrieve.kt}

    \framebreak

    Working with \kt{ClauseMultiSet}s:
    %
    \ktSnippet{./snippets/MultiSet.kt}
\end{frame}

\subsection{Theories}

\begin{frame}[allowframebreaks]{Theories Design and Implementations}

    \begin{block}{The \kt{Theory} type}
        \begin{itemize}
            \item provides high-level management of \kt{Clause}s
            \item meant as a \textit{façade} through which client code can access a knowledge base
            \item design and implementation mirror the ones devised for \kt{Clause} collections
            \item designed as \kt{Iterable} sub-types
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Mutable vs. immutable theories}
        Just like \kt{ClauseCollection}s,
        %
        \begin{itemize}
            \item \textit{mutable} theories can be modified in place
            \item \textit{immutable} theories cannot be changed: their operations build new ones containing the modified clauses
        \end{itemize}
    \end{block}
    %
    \begin{block}{Indexed vs. listed Theories}
        Theories come into two main implementations:
        \begin{itemize}
            \item \textit{indexed} theories are backed by an indexed data structure
            \begin{description}
                \item [!] providing faster look-up, but taking up more space
            \end{description}
            \item \textit{list-based} theories are backed by lists
            \begin{description}
                \item [!] slower but memory-efficient
                \item [!] preserve order of \kt{Clause}s
            \end{description}
        \end{itemize}
    \end{block}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Theory} Type Hierarchy}

    \begin{center}
        \includegraphics[width=0.6\linewidth]{img/theory-base.pdf}
    \end{center}

    \framebreak

    \begin{center}
        \includegraphics[width=0.6\linewidth]{img/theory-immutable.pdf}
    \end{center}

    \framebreak

    \begin{center}
        \includegraphics[width=0.7\linewidth]{img/theory-mutable.pdf}
    \end{center}

    \framebreak

    Main \kt{Theory} methods:
    \begin{description}
        \item[\kt{assertA(Clause): Theory}] adds the given clause \textit{before} all other clauses in this theory
        \item[\kt{assertZ(Clause): Theory}] adds the given clause \textit{after} all other clauses in this theory
        \item[\kt{abolish(Indicator): Theory}] removes all the clauses matching the given \kt{Indicator}
        \item[\kt{retract(Clause): RetractResult<Theory>}] tries to delete a matching clause from this theory
    \end{description}

    \framebreak

    \begin{description}
        \item[\kt{plus(Theory): Theory}] adds the given \kt{Theory} to this
        \item[\kt{contains(Clause): Boolean}] checks if the given \kt{Clause} is contained in this \kt{Theory}
        \item[\kt{get(Clause): Sequence<Clause>}] retrieves all matching clauses from this \kt{Theory}
        \item[\kt{toMutableTheory(): MutableTheory}] converts this \kt{Theory} to a mutable one
        \item[\kt{toImmutableTheory(): Theory}] converts this \kt{Theory} to an immutable one
    \end{description}

    \framebreak

    \begin{block}{The \kt{RetractResult} type}
        \begin{itemize}
            \item represents the output of a \kt{retract(Clause)} call
            \item can be a \kt{Success} or a \kt{Failure}
        \end{itemize}
    \end{block}
    %
    \begin{center}
        \includegraphics[width=0.7\linewidth]{img/retract-result.pdf}
    \end{center}

\end{frame}

\begin{frame}[allowframebreaks]{Creating a \kt{Theory}}
    Static factories for \kt{Theory} (same methods apply for \kt{MutableTheory}):
    %
    \begin{description}
        \item[\kt{empty(): Theory}] creates an empty \kt{Theory} (indexed by default)
        \item[\kt{of(vararg Clause): Theory}] creates a \kt{Theory} containing the given clauses
        \item[\kt{emptyIndexed(): Theory}] creates an empty \kt{Theory} backed by an indexed data structure
        \item[\kt{indexedOf(vararg Clause): Theory}] creates an indexed \kt{Theory} containing the given \kt{Clauses}
        \item[\kt{emptyListed(): Theory}] creates an empty \kt{Theory} backed by a list
        \item[\kt{listedOf(vararg Clause): Theory}] creates a \kt{Theory} backed by a list, containing the given clauses
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks]{Using a \kt{Theory}}
    Asserting clauses into a \kt{Theory}:
    %
    \ktSnippet{./snippets/TheoryAssert.kt}

    \framebreak

    Abolishing \kt{Indicator}s from a \kt{Theory}:
    %
    \ktSnippet{./snippets/TheoryAbolish.kt}

    \framebreak

    Retracting clauses from a \kt{Theory}:
    %
    \ktSnippet{./snippets/TheoryRetract.kt}
\end{frame}

\section{Generic Logic Resolution: the \module{solve} Module}

\begin{frame}[allowframebreaks]{The \module{solve} Module: Overview}

    \begin{block}{Purpose}
        \begin{itemize}
            \item Provide generic support to logic resolution
            \item Re-use as much as possible of Prolog standard
            %
            \begin{itemize}
                \item without committing to any particular resolution strategy
                \item nor to any inference procedure
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    Thus, \module{solve} provides the following abstractions:

    \begin{block}{Solvers and Solutions}\centering
        Solvers are reactive entities capable of answering to users' queries by producing one or more solutions, exploiting logic resolution
    \end{block}

    \begin{block}{Execution Contexts}
        \begin{center}
            An execution context encapsulates some solver's internal state.
            Resolution affects and is affected by the solver's execution context.
        \end{center}

        \small
        Composed by:
        %
        \begin{description}
            \item[libraries] | containers of built-in functionalities exploitable by resolution
            \item[flags] | configurable aspects of a solver
            \item[knowledge bases] (KB) | containers of the logic knowledge used by resolution
            \item[operators] | set of operators used to parse queries and to present solutions
            \item[channels] | I/O facilities to communicate with the external world
        \end{description}
        %
        \begin{itemize}\small
            \item[+] any resolution-specific aspect
            %
            \begin{itemize}\scriptsize
                \item (this may vary depending on how resolution is implemented)
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Libraries}
        \begin{center}
            Containers of built-in functionalities exploitable by resolution
        \end{center}

        Possibly, including:
        %
        \begin{description}
            \item[some \textbf{clauses}] containing logic predicates provided by the library
            \item[some \textbf{primitives}] i.e., logic predicates, implemented in Kotlin, and provided by the library
            \item[some \textbf{functions}] i.e., custom ways to reduce expressions of terms
            \item[some \textbf{operators}] automatically imported into the solver along with the library
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Flags}
        \begin{center}
            Key-value pairs aimed at configuring a solver behaviour
        \end{center}

        Where:
        %
        \begin{itemize}
            \item the key is a string
            \item the value is an arbitrary term
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Knowledge bases (KB)}
        \begin{center}
            Containers of the logic knowledge taken into account by resolution to answer users' queries
        \end{center}

        Following Prolog's conventions, KB are of two sorts:
        %
        \begin{description}
            \item[static KB] | which cannot be altered during resolution
            \item[dynamic KB] | which can be altered during resultion
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Operators}
        \begin{center}
            Each solver may operate upon a dynamic set of operators
        \end{center}

        That:
        %
        \begin{itemize}
            \item may be loaded along with libraries or be dynamically altered during resolution
            \item may affect the way users' queries are parsed
            \item may affect the way solutions are presented to users
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Channels}
        \begin{center}
            Communication facilities among the solver and the external world
        \end{center}

        Channels are of two sorts:
        %
        \begin{description}
            \item[input channels] (a.k.a. \alert{sources}) let a solver receive inputs messages
            \item[output channels] (a.k.a. \alert{sinks}) let a solver provide output messages
        \end{description}
    \end{block}
\end{frame}

\subsection{\kt{Solver}s and the \kt{Solution}s}

\begin{frame}[allowframebreaks]{The \kt{Solver}, \kt{Solution}, and \kt{SolveOptions} Types}
    % Solver

    % MutableSolver

    % Solution.*

    % SolveOpts

    \begin{center}
        \includegraphics[width=\linewidth]{img/solve-io.pdf}
    \end{center}

    \begin{block}{The \kt{Solver} type}
        \kt{Solver}s expose many \kt{solve*} methods, accepting:
        %
        \begin{itemize}
            \item a \alert{goal}, i.e. a \kt{Struct} representing the query to be answered via resolution
            \item an instance of \kt{SolveOptions} describing/constraining the way answers are provided
        \end{itemize}
        %
        and returning one or more \kt{Solution}s
    \end{block}

    \begin{block}{The \kt{Solution} type}
        A \kt{Solution} represents an answer provided by a \kt{Solver} w.r.t. the user's query
        It can be of three actual sorts:
        %
        \begin{description}
            \item[\kt{Solution.Yes}] representing a positive answer
            %
            \begin{itemize}\small
                \item carrying a \kt{Unifier} assigning some variable from the user's query
            \end{itemize}

            \item[\kt{Solution.No}] representing a negative answer

            \item[\kt{Solution.Halt}] representing an exceptional answer
            %
            \begin{itemize}\small
                \item carrying a \kt{TuPrologRuntimeException} locating the error w.r.t. the resolution process
            \end{itemize}
        \end{description}
    \end{block}

    \begin{block}{The \kt{SolveOptions} type}
        Instances of \kt{SolveOptions} are provided along with users' queries and aim at constraining the way solutions are computed by the solver:
        %
        \begin{description}
            \item[\kt{isEager: Boolean}] | if \kt{true} all solutions are computed ASAP
            %
            \begin{itemize}\small
                \item may saturate memory in case of many/infinite solutions!
            \end{itemize}

            \item[\kt{isLazy: Boolean}] | if \kt{true} solutions are \emph{lazily} computed just before being consumed
            %
            \begin{itemize}\small
                \item this is \kt{true} by default
            \end{itemize}

            \item[\kt{timeout: TimeDuration}] | dictates the \alert{maximum} amount of time resolution may use to compute a single solution
            %
            \begin{itemize}\small
                \item defaults to infinite time
            \end{itemize}

            \item[\kt{limit: Int}] | limits the \alert{maximum} amount of computed solutions
            %
            \begin{itemize}\small
                \item defaults to infinite
            \end{itemize}
        \end{description}
    \end{block}

    \begin{block}{The \kt{solve*} methods in \kt{Solver}}
        \begin{description}
            \item[\kt{solve}] | returns a \kt{Sequence} (i.e., a stream) of \kt{Solution}s
            \item[\kt{solveList}] | returns a \kt{List} of \kt{Solution}s
            %
            \begin{itemize}\small
                \item implies \kt{solveOpts.isEager == true}
            \end{itemize}
            \item[\kt{solveOnce}] | returns a single \kt{Solution}
            %
            \begin{itemize}\small
                \item implies \kt{solveOpts.limit == 1}
            \end{itemize}
        \end{description}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{Using a \kt{Solver}}

    \begin{block}{Concept}
        \centering
        \includegraphics[width=.4\linewidth]{img/streamful-solver.pdf}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{./snippets/YesSolutionsList.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/YesSolutions.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/NoSolution.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/TimeoutSolution.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/HaltSolution.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/ManySolutionsLazy.kt}

    \framebreak

    \ktSnippet[\tiny]{./snippets/ManySolutionsEager.kt}
\end{frame}

\begin{frame}[allowframebreaks]{\kt{Solver} vs. \kt{MutableSolver}}
    Notice that there are 2 types for solvers:
    %
    \begin{center}
        \includegraphics[width=.8\linewidth]{img/solve-mutable.pdf}
    \end{center}
    %
    \begin{itemize}\small
        \item \emph{solvers} expose properties supporting \alert{inspection} of their state
        \item \alert{mutable} solvers expose methods to \alert{alter} their state
        %
        \begin{itemize}
            \item[!] the state of \emph{non}-mutable solvers may change too, because of resolution
            %
            \begin{itemize}
                \item[$\rightarrow$] they are \alert{not} immutable
            \end{itemize}
        \end{itemize}
    \end{itemize}

    \framebreak

    \ktSnippet[\tiny]{./snippets/SolverVsMutableSolver.kt}
\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{Solvers} via a \kt{SolverFactory}}
    \begin{block}{About solver factories}\centering
        Objects of type \kt{SolverFactory} aim at instantiating \kt{Solver}s
    \end{block}

    \bigskip

    Main sorts of methods:
    %
    \begin{description}
        \item[\kt{solverOf(\ldots)}] | creates an empty \kt{Solver}
        \item[\kt{solverWithDefaultBuiltins(\ldots)}] | creates a \kt{Solver} and endows it with some default built-in predicates
        \item[\kt{mutableSolverOf(\ldots)}] | creates an empty \kt{MutableSolver}
        \item[\kt{mutableSolverWithDefaultBuiltins(\ldots)}] | creates a \kt{MutableSolver} and endows it with some default built-in predicates
    \end{description}

    \framebreak

    \begin{itemize}
        \item All such methods come with various overloads\ldots
        \item \ldots letting the caller specify the new solver's:
        %
        \begin{enumerate}
            \item libraries to be loaded upon construction
            %
            \begin{itemize}
                \item (possibly, other than the default ones)
            \end{itemize}
            \item initial values of specific flags
            \item content of the static KB
            \item initial content of the dynamic KB
            \item operators to be loaded upon construction
            \item input/output channels to be used for the solver
            \item or some sub-set of the above
        \end{enumerate}
    \end{itemize}

    \framebreak

    \begin{alertblock}{Important convention}\centering
        All implementations of \kt{Solver} should be packed with a corresponding implementation of \kt{SolveFactory}, possibly as a \alert{singleton}
    \end{alertblock}
    %
    \begin{itemize}
        \item[eg] \module{solve-classic} exposes object \kt{ClassicSolverFactory}
        %
        \begin{itemize}
            \item also accessible via \kt{Solver.\alert{classic}}
        \end{itemize}

        \item[eg] \module{solve-streams} exposes object \kt{StreamsSolverFactory}
        %
        \begin{itemize}
            \item also accessible via \kt{Solver.\alert{streams}}
        \end{itemize}
    \end{itemize}

    \framebreak

    \ktSnippet[\tiny]{./snippets/SolverFactories.kt}

    \framebreak

    Solver factories support writing \alert{implementation-agnostic} tests for \kt{Solver}s:
    %
    \ktSnippet[\tiny]{./snippets/TestSolverPrototype.kt}

\end{frame}

\subsection{The \kt{ExecutionContext}}

\begin{frame}[allowframebreaks]{Overview on the general purpose \kt{ExecutionContext}}
    \begin{itemize}
        \item Module \module{solve} exposes a general interface for \kt{ExecutionContext}s
        \item This must be exploited \& customised by implementers of \kt{Solver}s
    \end{itemize}
    %
    \begin{center}
        \includegraphics[width=.6\linewidth]{img/solve-ec.pdf}
    \end{center}

    \framebreak

    \begin{block}{An \kt{ExecutionContext} keeps track of (at least)}
        \begin{itemize}
            \item all inspectable aspects of a \kt{Solver}
            %
            \begin{itemize}
                \item[ie] libraries, flags, KB, operators, and channels
            \end{itemize}
            \item[+] the \alert{\kt{procedure}} resolution is currently focussing upon
            \item[+] the \alert{\kt{substitution}} resolution has constructed so far
            \item[+] other fields possibly specified/customised by implementers
        \end{itemize}
    \end{block}

    \framebreak

    \begin{alertblock}{Conventions}
        \begin{itemize}
            \item \kt{ExecutionContext}s are \alert{immutable}

            \item An \kt{ExecutionContext} can be attained from another one via:
            %
            \begin{description}\small
                \item[\kt{update(\ldots)}] | creating a copy of the current context, only differing for the provided fields
                \item[\kt{apply(\textit{SideEffect})}] | creating a copy of the current context by applying the provide \kt{SideEffect} to it
            \end{description}
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{exampleblock}{Notice that}
        \begin{itemize}
            \item It is always possible to create a novel \kt{(Mutable)Solver} via
             %
             \begin{description}\small
                \item[\kt{createSolver(\ldots)}]
                \item[\kt{createMutableSolver(\ldots)}]
            \end{description}

            \item The new solver is initialised using the current context
            %
            \begin{itemize}
                \item[!] this is fundamental to realise complex functionalities
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
\end{frame}

\begin{frame}{\kt{ExecutionContext} is where everything is linked together}
    \centering
    \includegraphics[width=.75\linewidth]{img/solve.pdf}
\end{frame}

\subsubsection{About \kt{Solver}s' Knowledge Bases}

\begin{frame}[allowframebreaks]{Static vs. Dynamic Knowledge bases}
    \begin{alertblock}{Conventions}
        \begin{itemize}
            \item The \kt{staticKb} is assumed to reference an \alert{immutable} \kt{Theory}
            %
            \begin{itemize}
                \item[ie] read efficient
            \end{itemize}

            \item The \kt{dynamicKb} is assumed to reference a \kt{\alert{Mutable}Theory}
            %
            \begin{itemize}
                \item[ie] write efficient
            \end{itemize}

            \item Resolution is generally only allowed to alter the \alert{dynamic} KB
            %
            \begin{itemize}
                \item[eg] via \pl{assert/1}, or \pl{retract/1}
            \end{itemize}

            \item However, notable exceptions exist
            %
            \begin{itemize}
                \item[eg] via \pl{consult/1}, or \pl{register/2} (from the \module{oop-lib} module)
            \end{itemize}
        \end{itemize}
    \end{alertblock}
\end{frame}

\begin{frame}[allowframebreaks]{Example: Using \kt{Solver}s with custom KB}

    \begin{block}{Endowing \kt{Solver}s with their KB}
        \begin{itemize}
            \item \kt{Solver}s can be provided with their KB upon construction
            %
            \begin{itemize}
                \item cf. \kt{SolverFactory}'s methods
            \end{itemize}

            \item \kt{MutableSolver}s can be provided with their KB dynamically
            %
            \begin{itemize}
                \item[eg] via the many methods of \kt{MutableSolver}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet{./snippets/CustomTheoriesSolver.kt}
    % initialising a solver with custom knowledge bases

    \framebreak

    \ktSnippet{./snippets/CustomTheoriesMutableSolver.kt}
    % loading a custom kb into a mutable solver
\end{frame}

\begin{frame}[allowframebreaks]{Custom KB and \kt{Directive}s}

    \begin{block}{About directives}
        \begin{itemize}
            \item KB may contain some \kt{Directive}s
            \item Implementations of \kt{Solver} should react to particular \kt{Directive}s
            %
            \begin{itemize}
                \item upon KB provisioning (either by construciton or otherwise)
                \item other sorts of directives are ignored
            \end{itemize}
            \item Notice that \kt{Directive}s are just headless \kt{Clauses}
            %
            \begin{itemize}
                \item unless they are provided to a \kt{Solver}
                \item at that point, they acquire procedural meaning
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    Notable directives:
    %
    \begin{description}
        \item[\pl{:- dynamic(\textit{F} / \textit{N}).}] makes any subsequent clause whose head indicator is \pl{\textit{F}/\textit{N}} be loaded into the \alert{dynamic} KB, event if the theory is loaded as static
        \item[\pl{:- static(\textit{F} / \textit{N}).}] dual w.r.t. \pl{dynamic(F/N)}
        \item[\pl{:- op(\textit{P}, \textit{S}, \textit{F}).}] loads a new operator into the \kt{Solver}, having the provided propriety (\pl{\textit{P}}), specifier (\pl{\textit{S}}), and functor (\pl{\textit{F}})
        \item[\pl{:- solve(\textit{G}).}] executes goal \pl{\textit{G}} as soon as the theory has been loaded
        \item[\pl{:- initialization(\textit{G}).}] alias for \pl{solve(\textit{G})}
        \item[\pl{:- set\_prolog\_flag(\textit{N}, \textit{V}).}] (re)sets the flag named \pl{\textit{N}} to the value \pl{\textit{V}}
        \item[\pl{:- include(\textit{P}).}] loads the theory whose path is \pl{\textit{P}} as if it was part of the currently loading one
        %
        \begin{itemize}\small
            \item[!] requires the \module{io-lib} module to be available at run-time
        \end{itemize}
        \item[\pl{:- load(\textit{P}).}] alias for \pl{include(\textit{P})}
    \end{description}

    \framebreak

    \ktSnippet[\tiny]{./snippets/DynamicDirective.kt}
\end{frame}

\subsubsection{Extending \kt{Solver}s via \kt{Libraries}}

\begin{frame}[allowframebreaks]{Overview on \kt{Libraries}}
    \begin{block}{Why \kt{Libraries}}
        \begin{itemize}
            \item Need to extend \kt{Solver}s via built-in functionalities
            \item[eg] operators, rules, (logic) functions, or primitives
        \end{itemize}
    \end{block}

    \framebreak

    \begin{center}
        \includegraphics[height=.75\textheight]{img/libraries.pdf}
    \end{center}

    \framebreak

    \begin{block}{Definition: \kt{Library}}
        A type for \alert{immutable} containers of:
        %
        \begin{description}
            \item[operators] to be loaded along with the \kt{Library}
            \item[theory] in turn containing pre-built rules and facts
            \item[primitives] i.e. logic predicates, written in Kotlin
            \item[functions] i.e. logic functions, written in Kotlin
        \end{description}
    \end{block}

    \begin{block}{Definition: \kt{Signature}}
        Primitives and functions are indexed in \kt{Library}s via \kt{Signature}s,
        %
        \begin{itemize}
            \item[ie] \kt{name}-\kt{arity} pairs
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Definition: \kt{AliasedLibrary}}
        A \kt{Library} with an \alert{alias}
        %
        \begin{itemize}
            \item think about aliases as Java packages names
        \end{itemize}
    \end{block}

    \begin{exampleblock}{Conventions on \textbf{aliases}}
        \begin{itemize}
            \item Same of Java packages names
            \item[ie] camel case, dot separated, space-less
            \item[eg] \texttt{prolog.lang}, \texttt{prolog.io}
        \end{itemize}
    \end{exampleblock}

    \framebreak

    \begin{block}{Definition: \kt{LibraryGroup}}
        A \kt{Library} attained by collecting several \kt{Library}s
    \end{block}

    \framebreak

    \begin{block}{Definition: \kt{Libraries}}
        A group of \kt{AliasedLibrary}, indexed by \alert{alias}
    \end{block}
    %
    \begin{itemize}
        \item this is what \kt{Solver}s' users use, in practice
    \end{itemize}

    \framebreak

    Example 1 -- Using \kt{Libraries}:
    %
    \ktSnippet{snippets/UsingLibraries.kt}

    \framebreak

    Example 2 -- Defining custom \kt{Libraries}:
    %
    \ktSnippet[\tiny]{snippets/DefiningLibraries.kt}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Primitive} Type}

    \begin{alertblock}{Problem}
        \begin{itemize}
            \item Some built-in logic functionalities are easier to write in Kotlin
            \item \ldots as they require \alert{altering} the \kt{Solver}'s \kt{ExecutionContext}
            %
            \begin{itemize}
                \item[eg] \pl{assert/1}, \pl{retract/1}, \pl{write/1}
            \end{itemize}
            \item Some logic functionalities may exploit external computational facilities
        \end{itemize}
    \end{alertblock}

    \begin{block}{Why \kt{Primitive}s}
        \begin{itemize}
            \item A means for calling Kotlin code from LP
            \item A means for writing logic \alert{relations} via OOP+FP+IP
        \end{itemize}
    \end{block}

    \framebreak

    Client-server metaphor:
    %
    \begin{itemize}
        \item users are clients for \kt{Solver}s, which act as servers
        \item \kt{Solver}s are clients for \kt{Primitive}s, which act as servers
    \end{itemize}

    \smallskip

    \begin{center}
        \includegraphics[width=.5\linewidth]{img/primitive-usage.pdf}
    \end{center}

    \framebreak

    When needing to solve a (sub-)goal $G$, a \kt{Solver} may
    %
    \begin{itemize}
        \item look into its KB, or
        \item pick a \kt{Primitive} $P$, compliant with $G$, from a \kt{Library}
        %
        \begin{enumerate}
            \item send a \alert{request}, describing $G$, to $P$
            \item receive several \alert{responses}, describing solutions to $G$, from $P$
            %
            \begin{itemize}
                \item possibly containing some \emph{side effect}, to be \alert{reified}
            \end{itemize}
        \end{enumerate}
    \end{itemize}

    \framebreak

    In code:
    %
    \begin{center}
        \includegraphics[width=.5\linewidth]{img/primitive.pdf}
    \end{center}

    \framebreak

    \ktSnippet[\tiny]{snippets/SumPrimitive.kt}
    % sum (functional)

    \ktSnippet[\tiny]{snippets/NatPrimitive.kt}
    % natural (backtraclabkle)

    \framebreak

    \begin{block}{The many sides of the \kt{Primitive}s}
        \kt{Primitive} are:
        %
        \begin{itemize}
            \item $N$-ary relations, in the eyes of LP
            \item servers \& data producers, in the eyes of \kt{Solver}s
            \item callbacks, in the eyes of libraries implementers
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{Within \kt{Primitive}s, \kt{Request}s are}
        \begin{itemize}
            \item descriptors of the \alert{current} \kt{ExecutionContext}
            \item descriptors of the \alert{actual} arguments of the (sub-)goal
            \item factories of \kt{Response}s
            %
            \begin{itemize}
                \item possibility to specify \alert{success} / \alert{failure} / \alert{exceptions}
                \item possibility to provoke \alert{\kt{SideEffect}}s
            \end{itemize}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{\kt{Primitive}s provoking \kt{SideEffect}s}
    \begin{block}{Definition: \kt{SideEffect}s}
        \begin{itemize}
            \item Instances of \kt{SideEffect} represent an \alert{edit to be perfomed} to some \kt{ExecutionContext}
            \item Only \alert{differences} are represented
            %
            \begin{itemize}
                \item[eg] \alert{clauses} to be \alert{added} / \alert{removed} to the static / dynamic KB
                \item[eg] \alert{flags} to be \alert{set} / \alert{removed} by \alert{name}
                \item[eg] \alert{channels} to be \alert{opened} / \alert{closed} by \alert{name}
            \end{itemize}
            \item \kt{SideEffect}s can be \alert{applied} to \kt{ExecutionContext}
            %
            \begin{itemize}
                \item producing \alert{another} \kt{ExecutionContext}
                \item only differing from the former one for the \alert{edit} represented by the \kt{SideEffect}
            \end{itemize}
            \item \kt{SideEffect} creation \alert{$\neq$} \kt{SideEffect} application
            %
            \begin{itemize}
                \item analogy with lambda expressions
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{center}
        \includegraphics[height=.75\textheight]{img/sideeffects.pdf}
    \end{center}

    \begin{block}{\kt{SideEffect}s creation}
        \begin{itemize}
            \item Side effects are created along with \kt{Responses}
            \item \ldots via \kt{SideEffects\alert{Builder}}\alert{s}
            %
            \begin{itemize}
                \item overloads exist for each \kt{Response.\alert{reply*}} method
                \item supporting the syntax:
                %
                \begin{center}
                    \kt{request.reply*(solution) \alert{\{ \meta{add side effects here} \}}}
                \end{center}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/AssertAllPrimitive.kt}
    % assert

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{PrologFunction} Type}
    \begin{alertblock}{Problem}
        \begin{itemize}
            \item Some predicates may require \alert{logic expressions} to be \alert{evalued} / \alert{reduced}
            %
            \begin{itemize}
                \item[eg] \pl{X is Y + 1} (which is equal to \alert{\pl{is(X, '+'(Y, 1))}})
            \end{itemize}
            \item Evaluation may involve several \alert{functions}
            %
            \begin{itemize}
                \item[ie] objects consuming $N \geq$ terms a producing a \alert{result}
                %
                \begin{itemize}
                    \item which is, in turn, a \kt{Term}
                \end{itemize}
            \end{itemize}
            \item Plugging \alert{custom} functions into a \kt{Solver} should be possible
        \end{itemize}
    \end{alertblock}

    \begin{block}{Why \kt{PrologFunction}s}
        \begin{itemize}
            \item A means for calling Kotlin code from LP
            %
            \begin{itemize}
                \item with the purpose of \alert{evaluating} an expression
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    Design very similar to \kt{Primitives}:
    %
    \begin{center}
        \includegraphics[height=.7\textheight]{img/function.pdf}
    \end{center}
    %
    \begin{itemize}
        \item[!] no support for side effects, nor multiple responses
    \end{itemize}

    \framebreak

    \ktSnippet[\tiny]{snippets/NextFunction.kt}
    % sum (functional)

    \framebreak

    \begin{alertblock}{About \kt{PrologFunction}s usage}
        Expression evaluation:
        %
        \begin{itemize}
            \item is expected to \alert{only} occur as part of some \kt{Primitive} execution
            \item is likely to involve \alert{several} \kt{PrologFunction}s
            \item must be \alert{atomic} in the eyes of the \kt{Solver}
        \end{itemize}
    \end{alertblock}

    \begin{exampleblock}{Example: the \pl{is/2} predicate}
        \begin{itemize}
            \item Prolog's \pl{is/2} is both an operator and a primitive in \twopkt{}
            \item Whenever a goal of the form \pl{is(X, Expr)} is met:
            %
            \begin{itemize}
                \item \pl{Expr} is \alert{evalued}, by applying \alert{all} possible functions
                \item the resulting term is bound to \pl{X}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}

    \framebreak

    \alert{Evaluators} aim to ``apply \alert{all possible} functions'' to an expression:
    %
    \begin{center}
        \includegraphics[width=.5\linewidth]{img/evaluator.pdf}
    \end{center}
    %
    \small
    where
    %
    \begin{itemize}
        \item ``all possible functions'' = \emph{``all functions currently loaded into the \kt{Solver}''}
    \end{itemize}

    \framebreak

    \begin{block}{Sorts of evaluators}
        \begin{description}
            \item[\kt{ExpressionReducer}] reduces all sub-expressions matching some function, leaving others unreduced
            %
            \begin{itemize}\small
                \item sub-expressions are evaluated using a \alert{post-order} visit
                \item[eg] \pl{g(f(1 + 2), 3 + 4)} $\rightarrow$ \pl{g(f(3), 7)}
            \end{itemize}
            \item[\kt{ExpressionEvaluator}] attempts to evaluate all sub-expressions matching some function, throws an error if some does not
            %
            \begin{itemize}\small
                \item sub-expressions are evaluated using a \alert{post-order} visit
                \item[eg] \pl{(1 + 2) - (3 + f(x))} $\rightarrow$ error as there is no function for \pl{f/1}
            \end{itemize}
            \item[\kt{ArithmeticEvaluator}] like \kt{ExpressionEvaluator}, but only leverages on arithmetic functions
            %
            \begin{itemize}\small
                \item[ie] functions accepting and returning \kt{Numeric} arguments
            \end{itemize}
        \end{description}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/ReducePrimitive.kt}
    %
    \begin{itemize}\small
        \item implementation of \pl{is/2} is analogous, except \kt{ExpressionEvaluator} is used
    \end{itemize}
\end{frame}

\subsubsection{Communicating with the external world via \kt{Channel}s}

\begin{frame}[allowframebreaks]{Overview on \kt{Channel}s}
    \begin{block}{Why \kt{Channel}s}
        \begin{itemize}
            \item \kt{Solver}s are \alert{prosumers} of data \alert{streams}
            \item Data represented in the form of \alert{characters} / \alert{strings}
            \item I/O facilities similar to Java's \kt{Reader}s and \kt{Writer}s are needed
            %
            \begin{itemize}
                \item[!] unfortunately, Kotlin MP does not support I/O
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{block}{Design choices}
        \begin{itemize}
            \item \kt{Channel}s are of 2 sorts: either \kt{InputChannel}s or \kt{OutputChannel}s
            %
            \begin{itemize}
                \item \kt{InputChannel}s (aka \alert{sources}) let \kt{Solver}s read data of type \kt{T}
                \item \kt{OutputChannel}s (aka \alert{sinks}) let \kt{Solver}s write data of type \kt{T}
            \end{itemize}
            \item \kt{Channel}s are identified by unique terms, in the eyes of \kt{Solver}s
            %
            \begin{itemize}
                \item or by some \alert{alias}, i.e. an \alert{atom}
            \end{itemize}
            \item \kt{Channel}s provide basic support to the features of \module{io-lib}
            \item Each \kt{Solver} contains an \kt{InputStore} and an \kt{OutputStore}
            %
            \begin{itemize}
                \item keeping track of currently available \kt{Channel}s
                \item and their aliases
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{block}{Default \kt{Channel}s}
        Each \kt{Solver} is initialised with 4 default \kt{Channel}s:
        %
        \begin{description}
            \item[\kt{stdIn: InputChannel<\textit{String}>}] main input channel
            \item[\kt{stdOut: OutputChannel<\textit{String}>}] main output channel
            \item[\kt{stdErr: OutputChannel<\textit{String}>}] error channel
            \item[\kt{warnings: OutputChannel<\textit{PrologWarning}>}] warning channel
            %
            \begin{itemize}
                \item does not output strings, but instances of \kt{PrologWarning}
            \end{itemize}
        \end{description}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Channel} Type Hierarchy}
    \begin{center}
        \includegraphics[width=.6\linewidth]{img/channels.pdf}
    \end{center}

    \begin{block}{The \kt{Channel<\texttt{T}>} type}\centering
        Base type for both input/output channels.
        All channels are \alert{observable} entities supporting the (un)registration of \alert{listeners}.
    \end{block}
    %
    \begin{description}
        \item[\kt{addListener(Listener<T>)}] registers a new listener
        \item[\kt{removeListener(Listener<T>)}] unregisters a listener
        \item[\kt{clearListeners(Listener<T>)}] unregisters all listeners
        \item[\kt{close()}] closes the channel (no more write/read allowed)
        \item[\kt{isClosed: Boolean}] returns \kt{true} iff the channel has been closed
        \item[\kt{streamTerm: Struct}] returns the \kt{Struct} identifying this channel
        %
        \begin{itemize}\small
            \item is always a structure of the form:
            %
            \begin{center}
                \pl{'\$stream'(InOut, Id)}
            \end{center}
            where
            %
            \begin{itemize}\scriptsize
                \item \pl{InOut} is either \pl{`in'} or \pl{`out'}, depending on the sort of channel
                \item \pl{Id} is a number uniquely identifying the channel instance
            \end{itemize}
        \end{itemize}
    \end{description}

    \framebreak

    \begin{block}{The \kt{InputChannel<\texttt{T}>} type is a sub-type of \kt{Channel<\texttt{T}>}}\centering
        Base type for \alert{input} channels.
        Support reading an instance of \kt{\texttt{T}} at a time, from some data source.
    \end{block}
    %
    \begin{description}
        \item[\kt{read(): T?}] consumes and returns the next instance of \kt{\texttt{T}} in the channel
        %
        \begin{itemize}\small
            \item returns \kt{null} if the channel is \alert{over}
            \item throws \kt{IllegalStateException} if the channel is \alert{closed}
        \end{itemize}
        \item[\kt{peek(): T?}] like \kt{read}, but does not consume
        \item[\kt{available: Boolean}] returns \kt{true} iff  the next instance of \kt{\texttt{T}} can be read/peeked without blocking
        \item[\kt{isOver: Boolean}] returns \kt{tree} iff the next call to \kt{read}/\kt{peek} would return \kt{null}
    \end{description}

    \framebreak

    \begin{block}{The \kt{OutputChannel<\texttt{T}>} type is a sub-type of \kt{Channel<\texttt{T}>}}\centering
        Base type for \alert{output} channels.
        Support writing an instance of \kt{\texttt{T}} at a time, onto some data sink.
    \end{block}
    %
    \begin{description}
        \item[\kt{write(T)}] writes an instance of \kt{\texttt{T}}
        %
        \begin{itemize}\small
            \item throws \kt{IllegalStateException} if the channel is \alert{closed}
        \end{itemize}
        \item[\kt{flush()}] ensures data is actually written to the channel
        %
        \begin{itemize}\small
            \item (useful in case of buffering / caching)
        \end{itemize}
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{Creating \kt{Channel}s}

    \begin{block}{Design choices -- \kt{InputChannel}s}
        \kt{InputChannel}s may be created out of:
        %
        \begin{itemize}
            \item a \alert{generator} function (of type \alert{\kt{() -> T}})
            \item a \kt{String}---supporting its consumption \alert{character-wise}
            \item an \kt{InputStream} or \kt{Reader} (JVM only)
            %
            \begin{itemize}
                \item[eg] \kt{System.in}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{stdIn(): InputChannel<String>}] returns a wrapper of the actual standard input of the current program
        %
        \begin{itemize}\small
            \item[eg] \kt{System.in} on the JVM
            \item[!] makes no sense on \alert{JS Browser-side}
        \end{itemize}
        \item[\kt{of(() -> \textit{T}): InputChannel<\textit{T}>}] creates an input channel out of a generator function
        \item[\kt{of(String): InputChannel<String>}] creates an input channel consuming a string \alert{character-wise}
    \end{description}

    \ktSnippet{snippets/InputFromStdin.kt}
    \ktSnippet{snippets/InputFromString.kt}
    \ktSnippet{snippets/InputFromFunction.kt}

    \framebreak

    \begin{block}{Design choices -- \kt{InputChannel}s}
        \kt{OutputChannel}s may be created out of:
        %
        \begin{itemize}
            \item a \alert{consumer} function (of type \alert{\kt{(T) -> Unit}})
            \item an \kt{OutputStream} or \kt{Writer} (JVM only)
            %
            \begin{itemize}
                \item[eg] \kt{System.out} or \kt{System.err}
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{stdOut(): OutputChannel<String>}] returns a wrapper of the actual standard output of the program
        %
        \begin{itemize}\small
            \item[eg] \kt{System.out} on the JVM
            \item[eg] \kt{Console.log} on JS
        \end{itemize}
        \item[\kt{stdErr(): OutputChannel<String>}] returns a wrapper of the actual standard error of the program
        %
        \begin{itemize}\small
            \item[eg] \kt{System.err} on the JVM
            \item[eg] \kt{Console.error} on JS
        \end{itemize}
        \item[\kt{warn(): OutputChannel<PrologWarning>}] returns a channel outputting warnings to the actual standard error of the program
        \item[\kt{of((\textit{T}) -> Unit): OutputChannel<\textit{T}>}] creates an output channel out of a consumer function (i.e. a \emph{callback})
    \end{description}

    \ktSnippet{snippets/OutputToStd.kt}
    \ktSnippet{snippets/OutputToCallback.kt}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{ChannelStore} Type Hierarchy}

    \begin{center}
        \includegraphics[width=.8\linewidth]{img/channels+stores.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{InputStore} type}
        Immutable map keeping track of currently open \kt{InputChannel}s for a \kt{Solver}, and their aliases
        %
        \begin{itemize}
            \item References the \alert{standard} input channel
            \item Keeps track of the \alert{current} input channel
            %
            \begin{itemize}
                \item[ie] the one the \kt{Solver} reads from, by default
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{The \kt{OutputStore} type}
        Map keeping track of currently open \kt{OutputChannel}s for a \kt{Solver}, and their aliases
        %
        \begin{itemize}
            \item References the \alert{standard} input and error channels
            \item References the \alert{warnings} channel
            \item Keeps track of the \alert{current} output channel
            %
            \begin{itemize}
                \item[ie] the one the \kt{Solver} writes onto, by default
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    Common methods:
    %
    \begin{description}
        \item[\kt{current: Channel<String>}] returns the current channel
        \item[\kt{setCurrent(Channel<String>)}] returns a new store having a different current channel
        \item[\kt{setCurrent(String)}] returns a new store having a different current channel (selected by \alert{alias})
        \item[\kt{findByTerm(Term)}] returns a channel by its identifier term
        \item[\kt{aliasesOf(Channel<String>)}] returns all the aliases of a given channel
    \end{description}
    %
    \begin{itemize}
        \item[+] all methods of \kt{Map<String, Channel<String>>}
    \end{itemize}
\end{frame}

\begin{frame}{Using \kt{Channel}s}
    \ktSnippet[\tiny]{snippets/CustomChannels.kt}
\end{frame}

\subsubsection{Configuring \kt{Solver}s via \kt{Flag}s}

\begin{frame}{Overview on flags}
    \begin{block}{About flags}
        \begin{itemize}
            \item Flags are key-value pairs carrying configurable aspects of \kt{Solver}s
            %
            \begin{itemize}
                \item \alert{keys} are \kt{String}s, whereas
                \item \alert{values} are \kt{Term}s
            \end{itemize}
            \item Some flags are editable, while others are \kt{read-only}
            %
            \begin{itemize}
                \item All flags can be inspected during resolution
                \item Editable flags' values can be altered during resolution
            \end{itemize}
            \item Custom flags may be defined/inspected during resolution
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{FlagStore} and \kt{NotableFlag} Types}
    \begin{center}
        \includegraphics[width=.8\linewidth]{img/flags.pdf}
    \end{center}

    \begin{alertblock}{No type for flags}
        \begin{itemize}
            \item Kotlin's \kt{Pair}s are used instead
            \item Flag $\equiv$ \kt{Pair<String, Term>}, in the general case
            \item \kt{NotableFlag} as the convenience type for \alert{built-in} flags
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{block}{The \kt{NotableFlag} type}\centering
        Ad-hoc type representing \alert{built-in} flags and their admissible values
    \end{block}
    %
    \begin{description}
        \item[\kt{name: String}] returns the name (i.e. the key) of the flag
        \item[\kt{admissibleValues: Sequence<Term>}] returns the set of admissible values of the flag
        \item[\kt{defaultValue: Term}] returns some item of \kt{admissibleValues}
        \item[\kt{isEditable: Boolean}] returns \kt{true} iff the flag's value can be altered during resolution
        \item[\kt{isAdmissibleValue(Term): Boolean}] checks whether the provided \kt{Term} is an admissible value for the flag
        \item[\kt{toPair(): Pair<String, Term>}] converts the notable flag into a key-value pair
    \end{description}

    \framebreak

    \begin{block}{The \kt{FlagStore} type}
        Immutable map keeping track of currently defined \alert{flags}' keys and their \alert{values}
        %
        \begin{itemize}
            \item[+] some methods for getting/setting \kt{NotableFlag}s
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item[\kt{get(NotableFlag): Term?}] returns the \emph{actual} value of some \alert{notable} flag
        \item[\kt{get(String): Term?}] returns the \emph{actual} value of some flag
        \item[\kt{set(NotableFlag): FlagStore}] returns a novel store where the provided \alert{notable} flag is set to its \emph{default} value
        \item[\kt{set(NotableFlag, Term): FlagStore}] returns a novel store where the provided \alert{notable} flag is set to the \emph{provided} value
        \item[\kt{set(String, Term): FlagStore}] returns a novel store where the provided flag is set to the provided value
        \item[\kt{plus(\meta{OtherFlags}): FlagStore}] returns a novel store containing the provided flags as well
        \item[\kt{minus(\meta{FlagNames}): FlagStore}] returns a novel store not containing the provided flags names
    \end{description}
    %
    \begin{itemize}
        \item[+] methods of \kt{Map}
    \end{itemize}
\end{frame}

\begin{frame}[allowframebreaks]{Example: Default \kt{NotableFlag}s and their Purpose}

    \begin{block}{\pl{unknown}}
        Defines what to do when no rule/primitive is found for solving a (sub-)goal:
        %
        \begin{itemize}
            \item Class: \kt{it.unibo.tuprolog.solve.flags.\alert{Unknown}}
            \item Admissible values:
            %
            \begin{description}
                \item[\pl{fail}] the goal is silently considered \pl{false}
                \item[\pl{warning}] \emph{(default)}  the goal is considered \pl{false} \& a warning is raised
                \item[\pl{error}] an error is raised and resolution is interrupted
            \end{description}
        \end{itemize}
    \end{block}

    \begin{block}{\pl{max\_arity}}
        Read-only flag dictating the maximum admissible value for a \kt{Struct}
        %
        \begin{itemize}
            \item Class: \kt{it.unibo.tuprolog.solve.flags.\alert{MaxArity}}
            \item Admissible values: \kt{Int.MAX\_VALUE} (i.e. $2^{31} - 1$)
        \end{itemize}
    \end{block}

    \begin{block}{\pl{last\_call\_optimization}}
        Dictates whether Prolog \kt{Solver}s should optimise \alert{tail-recursive} rules
        %
        \begin{itemize}
            \item Class: \kt{it.unibo.tuprolog.solve.flags.\alert{LastCallOptimization}}
            \item Admissible values:
            %
            \begin{description}
                \item[\pl{on}] \emph{(default)} optimization is performed whenever possible
                \item[\pl{off}] optimization is never performed
            \end{description}
        \end{itemize}
    \end{block}

    \begin{block}{\pl{double\_quotes}}
        Read-only flag dictating how double-quoted literals should be interpreted
        %
        \begin{itemize}
            \item Class: \kt{it.unibo.tuprolog.solve.flags.\alert{DoubleQuotes}}
            \item Admissible values: \pl{atom}
            %
            \begin{itemize}
                \item[ie] double-quoted literals are always considered as \kt{Atom}
            \end{itemize}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}{Using \kt{Flag}s}
    \ktSnippet{snippets/Flags.kt}
\end{frame}

\subsubsection{Other sorts of custom fields}

\begin{frame}[allowframebreaks]{Overview on \kt{CustomData}}

    \begin{center}
        \includegraphics[width=.8\linewidth]{img/customdata.pdf}
    \end{center}

    \begin{block}{About \kt{CustomDataStore}s}
        \begin{itemize}
            \item To ease extensibility, \kt{ExecutionContext}s main contain \kt{CustomData} too
            \item This is achieved via one more property, of type \kt{CustomDataStore}
            \item \kt{CustomDataStore}s have 3 fields of type \kt{CustomData}
            \item \kt{CustomData} are key-value store which may keep \alert{any sort} of data
            \item This may exploited by \kt{Primitive}s/\kt{Solver}s implementers
            %
            \begin{itemize}
                \item to accumulate/inspect data to affect resolution
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{block}{Sorts of \kt{CustomData}}
        Custom data are of 3 sorts:
        %
        \begin{description}
            \item[ephemeral] | automatically erased after a choice point is selected
            %
            \begin{itemize}\small
                \item[eg] in Prolog, once every time \alert{backtracking} is performed
            \end{itemize}
            \item[durable] | automatically erased after a solution is reached
            \item[persistent] | never erased automatically
        \end{description}
    \end{block}
\end{frame}

\subsection{Errors and Warnings}

\begin{frame}[allowframebreaks]{The \kt{TuPrologRuntimeException} Type Hierarchy}

    \begin{center}
        \includegraphics[width=\linewidth]{img/errors.pdf}
    \end{center}

    \framebreak

    \begin{description}
        \item[\kt{TuProlog\textit{Runtime}Exception}] base type for all issues which may occur during resolution
        %
        \begin{itemize}\small
            \item when thrown \alert{within \kt{Primitive}s}, they affect the ongoing resolution
            \item resolution is interrupted, and a \kt{Solution.\alert{Halt}} is produced
            %
            \begin{itemize}\scriptsize
                \item the solution keeps track of the exception
                \item the exception keeps track of the execution context where the issue occurred
            \end{itemize}
        \end{itemize}

        \item[\kt{HaltException}] provokes the immediate interruption of the resolution process
        %
        \begin{itemize}\small
            \item may carry an \alert{exit code} (integer)
            \item analogous to \kt{System.exit(\meta{Int})} one the JVM
            \item produces a \kt{Solution.Halt}
        \end{itemize}

        \item[\kt{TimeOutException}] provokes the immediate interruption of the resolution process
        %
        \begin{itemize}\small
            \item automatically thrown by \kt{Solver}s upon \alert{timeouts}
        \end{itemize}

        \framebreak

        \item[\kt{PrologError}] base types for LP-related errors
        %
        \begin{itemize}\small
            \item[ie] errors which can be caught in LP
            \item[eg] via \kt{catch/3}, in Prolog
        \end{itemize}

        \item[\kt{PrologWarning}] base types for LP-related warnings
        %
        \begin{itemize}\small
            \item these are not meant to be thrown
            \item instances of \kt{PrologWarning} must be considered ordinary data structures to be outputted on the \kt{warnings} \kt{OutputChannel}
        \end{itemize}
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{PrologError} Type Hierarchy}

    \begin{block}{About \kt{PrologError}s}
        \begin{itemize}
            \item Each instance of \kt{PrologError} corresponds to a \kt{Term}
            \item The term can be thrown with predicate \alert{\kt{throw/1}}\ldots
            \item \ldots and caught via \alert{\kt{catch/3}}
        \end{itemize}
    \end{block}

    \begin{block}{Prolog ISO Standard Errors}
        Following the Standard:
        %
        \begin{itemize}
            \item each subtype of \kt{PrologError} has a corresponding \alert{error \kt{Struct}}
            \item the general pattern is as follows:
            %
            \begin{center}
                \pl{error(\textit{Description}, \textit{Custom})}
            \end{center}
            %
            where:
            %
            \begin{description}\small
                \item[\pl{\textit{Description}}] is a \kt{Term} whose structure depends on the particular sub-type of \kt{PrologError}
                %
                \begin{itemize}\scriptsize
                    \item it aims at describing the error, logically
                \end{itemize}
                \item[\pl{\textit{Custom}}] is a custom, implementation-specific \kt{Term}
                %
                \begin{itemize}\scriptsize
                    \item \twopkt{}'s convention: it carries the message to be shown to the user
                    \item so, it is commonly an \kt{Atom}
                \end{itemize}
            \end{description}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{description}
        \item[\kt{InstantiationError}] to be thrown when a sub-goal/argument is being evaluated but it is not sufficiently instantiated
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is always the atom \alert{\pl{instantiation\_error}}
            \item[\pl{\textit{Custom}}] describes what argument/sub-term provoked the error
        \end{description}

        \framebreak

        \item[\kt{TypeError}] to be thrown when a sub-goal/argument is being evaluated but has not the right logic type
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{type\_error(\textit{Expected}, \textit{Culprit})}
            \item[\pl{\textit{Expected}}] is an \kt{Atom} describing the expected type
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{TypeError.\alert{Expected}}
                \item[eg] \pl{atom}, \pl{atomic}, \pl{callable}, \pl{character}, \pl{compound}, etc.
            \end{itemize}
            \item[\pl{\textit{Culprit}}] is the \kt{Term} having the wrong type
        \end{description}

        \framebreak

        \item[\kt{DomainError}] to be thrown when a sub-goal/argument is being evaluated and it has the right type, but its value is not admissible
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{domain\_error(\textit{Expected}, \textit{Culprit})}
            \item[\pl{\textit{Expected}}] is an \kt{Atom} describing the expected value
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{DomainError.\alert{Expected}}
                \item[eg] \pl{not\_less\_than\_zero}, \pl{non\_empty\_list}, \pl{operator\_specifier}, etc.
            \end{itemize}
            \item[\pl{\textit{Culprit}}] is the \kt{Term} having the wrong value
        \end{description}

        \framebreak

        \item[\kt{RepresentationError}] to be thrown when a value cannot be represented as a \kt{Term}
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{representation\_error(\textit{Limit})}
            \item[\pl{\textit{Limit}}] describes the representation limit which has been hit
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{RepresentationError.\alert{Limit}}
                \item[eg] \pl{character}, \pl{character\_code}, \pl{max\_arity}, etc.
            \end{itemize}
        \end{description}

        \framebreak

        \item[\kt{SyntaxError}] to be thrown when parsing some badly formed string during resolution
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is always the atom \alert{\pl{syntax\_error}}
            \item[\pl{\textit{Custom}}] describes why the string could not be parsed, and localizes the issue into the string
        \end{description}

        \framebreak

        \item[\kt{EvaluationError}] to be thrown when some expression evaluation meets an arithmetic issue
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{evaluation\_error(\textit{Type})}
            \item[\pl{\textit{Type}}] describes the evaluation issue which has been met
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{EvaluationError.\alert{Type}}
                \item[eg] \pl{zero\_divisor}, \pl{int\_overflow}, \pl{float\_overflow}, etc.
            \end{itemize}
        \end{description}

        \framebreak

        \item[\kt{ExistenceError}] to be thrown accessing some resource by name/reference fails because the resource does not exist
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{existence\_error(\textit{ObjectType}, \textit{Culprit})}
            \item[\pl{\textit{ObjectType}}] describes the sort of resource which does not exist
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{ExistenceError.\alert{ObjectType}}
                \item[eg] \pl{procedure}, \pl{source\_sink}, \pl{stream}, etc.
            \end{itemize}
        \end{description}

        \framebreak

        \item[\kt{PermissionError}] to be thrown when performing an operation which is not permitted
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is a \kt{Struct} of the form \pl{permission\_error(\textit{Operation}, \textit{Permission}, \textit{Culprit})}
            \item[\pl{\textit{Operation}}] describes the sort of operation which failed
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{PermissionError.\alert{Operation}}
                \item[eg] \pl{access}, \pl{invoke}, \pl{modify}, \pl{open}, etc.
            \end{itemize}
            \item[\pl{\textit{Permission}}] describes the sort of resource for which the operation is not permitted
            %
            \begin{itemize}\scriptsize
                \item admissible values are contained into the class \kt{PermissionError.\alert{Permission}}
                \item[eg] \pl{flag}, \pl{operator}, \pl{source\_sink}, \pl{static\_procedure}, etc.
            \end{itemize}
            \item[\pl{\textit{Culprit}}] is the (sub-)goal which provoked the error
        \end{description}

        \framebreak

        \item[\kt{SystemError}] to be thrown for any other circumstance
        %
        \begin{description}\small
            \item[\pl{\textit{Description}}] is always the atom \alert{\pl{system\_error}}
            \item[\pl{\textit{Custom}}] provides the actual description of the problem
        \end{description}
        %
        \begin{itemize}
            \item[!] this may be used to wrap Kotlin exceptions occurring during resolution
        \end{itemize}
    \end{description}
\end{frame}

\begin{frame}{The \kt{PrologWarning} Type Hierarchy}

    Main sub-types:
    %
    \bigskip
    %
    \begin{description}
        \item[\kt{MissingPredicate}] used to signal that a \kt{Solver} knows no predicate to solve a (sub-)goal

        \bigskip

        \item[\kt{InitializationIssue}] used to signal a failure/error while executing some \alert{directive}
    \end{description}
\end{frame}

\subsection{Custom \kt{Primitive}s, \kt{Function}s, and \kt{Libraries}s}

\begin{frame}[allowframebreaks]{Overview on Custom Libraries}
    \begin{itemize}
        \item Libraries are the basic means to provide built-in functionalities to solvers

        \bigskip

        \item Default built-in functionalities are provided via libraries as well

        \bigskip

        \item Creating a library essentially means:
        %
        \begin{enumerate}
            \item defining a number of \alert{primitives}
            \item defining a number of \alert{functions}
            \item defining a number of \alert{rules} and \alert{facts}
            \item deciding which of these should be usable as operators
            \item defining \alert{operators} accordingly
        \end{enumerate}

        \bigskip

        \item[!] Primitives, in particular, are the most common object libraries implementers will manipulate
    \end{itemize}

    \framebreak

    \begin{block}{Writing \textbf{primitives} involves many common aspects}
        \begin{itemize}
            \item[eg] input validation
            \item[eg] permission checking
            \item[eg] arguments/results packing \& unpacking
            \item[\vdots]
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{Overview on \kt{PrimitiveWrappers}}
    \begin{block}{The \kt{PrimitiveWrapper} type hierarchy}
        A pool of abstract classes factorising common aspects of primitives' implementation
        %
        \begin{itemize}
            \item primitive wrapper $\approx$ signature + primitive + utility methods
        \end{itemize}
    \end{block}

    \framebreak

    \begin{center}
        \includegraphics[width=\linewidth]{img/wrappers.pdf}
    \end{center}

    \framebreak

    Main wrapper classes:
    %
    \begin{description}
        \item[\kt{PredicateWithoutArguments}] base class for 0-ary predicates
        \item[\kt{UnaryPredicate}] base class for 1-ary predicates
        \item[\kt{BinaryRelation}] base class for 2-ary predicates
        \item[\kt{TernaryRelation}] base class for 3-ary predicates
        \item[\kt{QuaternaryRelation}] base class for 4-ary predicates
        \item[\kt{QuinaryRelation}] base class for 5-ary predicates
    \end{description}

    \framebreak

    Each wrapper class, comes with 4 more abstract sub-classes:
    %
    \begin{description}
        \item[\kt{WithoutSideEffects}] to be preferred if the predicate does not provoke side-effects
        \item[\kt{NonBacktrackable}] to be preferred if the predicate is not backtrackable, yet it may provoke side-effects
        \item[\kt{Functional}] to be preferred if the predicate is not backtrackable and does not provoke side-effects
        \item[\kt{Predicative}] to be preferred if the predicate has a boolean semantics, i.e. it is not backtrackable, it does not provoke side-effects, and it does not assign any variable
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks]{\kt{PrimitiveWrapper}s' Utility Methods}\small

    Each sub-class of \kt{PrimitiveWrapper} inherits a number of protected utility methods:
    %
    \begin{description}
        \item[\kt{ensuringAllArgumentsAreInstantiated()}] throws an \kt{InstantiationError} if some argument is a \kt{Var}
        % \framebreak
        \item[\kt{ensuringArgumentIsWellFormedIndicator(Int)}] checks whether the argument at the provided index is a well formed indicator (i.e. \pl{\meta{Atom}/\meta{Integer}}), throwing the most adequate error in case it is not
        % \framebreak
        \item[\kt{ensuringArgumentIsWellFormedClause(Int)}] checks whether the argument at the provided index is a well formed clause (i.e. no sub-goal in the body is a \kt{Var}), throwing the most adequate error in case it is not
        % \framebreak
        \item[\kt{ensuringArgumentIsInstantiated(Int)}] throws an \kt{InstantiationError} if the argument at the provided index is a \kt{Var}
        % \framebreak
        \item[\kt{ensuringArgumentIsNumeric(Int)}] throws a \kt{TypeError} if the argument at the provided index is not \kt{Numeric}
        % \framebreak
        \item[\kt{ensuringArgumentIsStruct(Int)}] throws a \kt{TypeError} if the argument at the provided index is not a \kt{Struct}
        % \framebreak
        \item[\kt{ensuringArgumentIsCallable(Int)}] alias for \kt{ensuringArgumentIsStruct}
        % \framebreak
        \item[\kt{ensuringArgumentIsVariable(Int)}] throws a \kt{TypeError} if the argument at the provided index is not a \kt{Var}
        % \framebreak
        \item[\kt{ensuringArgumentIsCompound(Int)}] throws a \kt{TypeError} if the argument at the provided index is not a \kt{Struct} s.t. $\kt{arity} > 0$
        % \framebreak
        \item[\kt{ensuringArgumentIsAtom(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{Atom}
        % \framebreak
        \item[\kt{ensuringArgumentIsConstant(Int)}] throws a \kt{TypeError} if the argument at the provided index is not a \kt{Constant}
        % \framebreak
        \item[\kt{ensuringArgumentIsGround(Int)}] throws an \kt{InstantiationError} if the argument at the provided index is not \emph{ground}
        % \framebreak
        \item[\kt{ensuringArgumentIsChar(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{Atom} s.t. $\kt{value.length} == 1$
        % \framebreak
        \item[\kt{ensuringArgumentIsSpecifier(Int)}] throws a \kt{DomainError} if the argument at the provided index is not an \kt{Atom} from the set \pl{\{fx, fy, xf, yf, xfx, yfx, xfy\}}
        % \framebreak
        \item[\kt{ensuringArgumentIsList(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{List}
        % \framebreak
        \item[\kt{ensuringArgumentIsInteger(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{Integer}
        % \framebreak
        \item[\kt{ensuringArgumentIsNonNegativeInteger(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{Integer}, or a \kt{DomainError} if it is a negative integer
        % \framebreak
        \item[\kt{ensuringArgumentIsArity(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{Integer}, a \kt{DomainError} if it is a negative integer, or a \kt{RepresentationError} is it is an integer greater than \kt{MaxArity.defaultValue}
        % \framebreak
        \item[\kt{ensuringArgumentIsWellFormedList(Int)}] throws a \kt{TypeError} if the argument at the provided index is not an \kt{List}, or a \kt{DomainError} if it is a \kt{List} whose termination item is not \pl{[]}
        % \framebreak
        \item[\kt{ensuringArgumentIsCharCode(Int)}] throws a \kt{RepresentationError} if the argument at the provided index does not correspond to a character according to the UTF-16 encoding
        % \framebreak
        \item[\kt{checkTermIsRecursivelyCallable(Term)}] checks whether the provided \kt{Term} is a well formed clause (i.e. no sub-goal in the body is a \kt{Var}), throwing the most adequate error in case it is not
        % \framebreak
        \item[\kt{ensuringTermIsCharCode(Term)}] throws a \kt{RepresentationError} if the provided \kt{Term} does not correspond to a character according to the UTF-16 encoding
        % \framebreak
        \item[\kt{ensuringTermIsWellFormedList(Term)}] throws a \kt{TypeError} if the provided \kt{Term} is not an \kt{List}, or a \kt{DomainError} if it is a \kt{List} whose termination item is not \pl{[]}
        % \framebreak
        \item[\kt{ensuringProcedureHasPermission(Signature, PermissionError.Operation)}] throws a \kt{PermissionError} is the provided \kt{Signature} matches some entry among the \kt{Solver}'s libraries, or static KB
        % \framebreak
        \item[\kt{ensuringClauseProcedureHasPermission(Clause, PermissionError.Operation)}] same as above, except that the \kt{Signature} of the \kt{Clause}'s \kt{head} is considerer
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks]{Example of \kt{PrimitiveWrappers} of all sorts}

    \begin{block}{Example 1: \pl{atom\_length(\textit{+Atom}, \textit{-Length})}}
        \begin{itemize}
            \item Purpose: computes the length of an atom
            \item Sort of primitive: binary relation, non-backtrackable, no side effect
            \item May throw:
            %
            \begin{description}\small
                \item[\kt{InstantiationError}] if the $1^{st}$ argument is a \kt{Var}
                \item[\kt{TypeError}] if the $1^{st}$ argument is not an \kt{Atom}, or the $2^{nd}$ is not an \kt{Integer}
                \item[\kt{DomainError}] if the $2^{nd}$ argument is a \emph{negative} \kt{Integer}
            \end{description}
            \item Usage example, in Prolog:
            %
            \begin{itemize}
                \item[?-] \pl{atom\_length(abc, X)} $\rightarrow$ \pl{X=3}
                \item[?-] \pl{atom\_length(abc, 3)} $\rightarrow$ \pl{true}
                \item[?-] \pl{atom\_length(abc, 4)} $\rightarrow$ \pl{false}
                \item[?-] \pl{atom\_length(X, 4)} $\rightarrow$ \pl{instantiation\_error}
                \item[?-] \pl{atom\_length(a, b)} $\rightarrow$ \pl{type\_error}
                \item[?-] \pl{atom\_length(a, -1)} $\rightarrow$ \pl{domain\_error}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/AtomLength.kt}

    \framebreak

    \begin{block}{Example 2: \pl{assert(\textit{+Clause})}}
        \begin{itemize}
            \item Purpose: adds a clause to the dynamic KB
            \item Sort of primitive: unary predicate, non-backtrackable, side effects
            \item May throw:
            %
            \begin{description}\small
                \item[\kt{InstantiationError}] if the $1^{st}$ argument is a \kt{Var}
                \item[\kt{TypeError}] if the $1^{st}$ argument is not a \kt{Struct}
                \item[\kt{DomainError}] if the $1^{st}$ argument is a bad-formed \kt{Clause}
                \item[\kt{PermissionError}] if the signature of \pl{\textit{Clause}} clashes with some other procedure from the \kt{Solver}'s library or static KB
            \end{description}
            \item Usage example, in Prolog:
            %
            \begin{itemize}
                \item[?-] \pl{assert(fact)} $\rightarrow$ \pl{true}
                \item[?-] \pl{assert(goal :- subgoal)} $\rightarrow$ \pl{true}
                \item[?-] \pl{assert(goal :- (subgoal, G))} $\rightarrow$ \pl{domain\_error}
                \item[?-] \pl{assert(1)} $\rightarrow$ \pl{type\_error}
                \item[?-] \pl{assert(X)} $\rightarrow$ \pl{instantiation\_error}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/Assert.kt}

    \framebreak

    \begin{block}{Example 3: \pl{retract(\textit{?Pattern})}}
        \begin{itemize}
            \item Purpose: removes each clause matching \pl{\textit{Pattern}} in the dynamic KB
            %
            \begin{itemize}
                \item removes clauses one by one, via backtracking
            \end{itemize}
            \item Sort of primitive: unary predicate, backtrackable, side effects
            \item May throw:
            %
            \begin{description}\small
                \item[\kt{InstantiationError}] if the $1^{st}$ argument is a \kt{Var}
                \item[\kt{TypeError}] if the $1^{st}$ argument is not a \kt{Struct}
                \item[\kt{DomainError}] if the $1^{st}$ argument is a bad-formed \kt{Clause}
                \item[\kt{PermissionError}] if the signature of \pl{\textit{Clause}} matches some other procedure from the \kt{Solver}'s library or static KB
            \end{description}
            \item Usage example, in Prolog (assume KB contains \alert{\pl{f(1). f(2).}})
            %
            \begin{itemize}
                \item[?-] \pl{retract(f(X))} $\rightarrow$ \pl{X=1}, \pl{X=2}
                \item[?-] \pl{retract(f(1))} $\rightarrow$ \pl{true}
                \item[?-] \pl{retract(f(3))} $\rightarrow$ \pl{false}
                % \item[?-] \pl{retract(X)} $\rightarrow$ \pl{instantiation\_error}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/Retract.kt}

    \framebreak

    \begin{block}{Example 4: \pl{findall(\textit{+Template}, \textit{:Goal}, \textit{-Solutions})} \hfill (pt. 1)}
        \begin{itemize}
            \item Assumptions: \pl{\textit{Template}} is a pattern reusing variables from \pl{\textit{Goal}}
            \item Purpose: computes all solutions to \pl{\textit{Goal}}, each solution is mapped into \pl{\textit{Template}}, all templates are aggregates into a list and the list is bound to \pl{\textit{Solutions}}
            \item Sort of primitive: ternary relation, non-backtrackable, no side-effects
            \item[!] Peculiarities: involves an \alert{inner} resolution process
        \end{itemize}
    \end{block}

    \begin{block}{Example 4: \pl{findall(\textit{+Template}, \textit{:Goal}, \textit{-Solutions})} \hfill (pt. 2)}
        \begin{itemize}
            \item May throw:
            %
            \begin{description}\small
                \item[\kt{InstantiationError}] if the $2^{nd}$ argument is a \kt{Var}
                \item[\kt{TypeError}] if the $2^{nd}$ argument is not a \kt{Struct}
                \item[any other error] possibly thrown by \pl{\textit{Goal}}
            \end{description}
            \item Usage example, in Prolog:
            %
            \begin{itemize}
                \item[?-] \pl{findall(X+1, member(X, [a,b]), L)} $\rightarrow$ \pl{L=[a+1, b+1]}
                \item[?-] \pl{findall(\_, false, [])} $\rightarrow$ \pl{true}
                \item[?-] \pl{findall(Z, (Z is X + 1), L)} $\rightarrow$ \pl{instantiation\_error}
                \item[?-] \pl{findall(\_, 4, \_)} $\rightarrow$ \pl{type\_error}
                \item[?-] \pl{findall(\_, G, \_)} $\rightarrow$ \pl{instantiation\_error}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \ktSnippet[\tiny]{snippets/FindAll.kt}
\end{frame}

\subsubsection{Default libraries}

\begin{frame}[allowframebreaks]{About \kt{DefaultBuiltins} and \kt{CommonBuiltins}}
    \begin{alertblock}{Convention}
        Each implementer of \kt{Solver} should provide a library object named \alert{\kt{DefaultBuiltins}}
        %
        \begin{itemize}
            \item containing all default built-in functionalities for that sort of \kt{Solver}
            \item to be used by the specific \kt{SolveFactory} implementation
            \item modules \module{solve-classic} and \module{solve-streams} are no exception
            %
            \begin{itemize}
                \item[eg] \kt{it.unibo.tuprolog.solve.\alert{classic}.stdlib.DefaultBuiltins}
                \item[eg] \kt{it.unibo.tuprolog.solve.\alert{streams}.stdlib.DefaultBuiltins}
            \end{itemize}
        \end{itemize}
    \end{alertblock}

    \begin{block}{The \kt{CommonBuiltins} library}
        \begin{itemize}
            \item Most functionalities are \alert{agnostic} w.r.t. how \kt{Solver}s are implemented
            \item[$\rightarrow$] Module \module{solve} provides an implementation for most of them
            %
            \begin{itemize}
                \item in \kt{it.unibo.tuprolog.solve.stdlib.\alert{CommonBuiltins}}
            \end{itemize}
            \item These functionalities are taken from the Prolog ISO Standard \cite{prologISO-pt1}
            %
            \begin{itemize}
                \item yet, they are \alert{resolution-agnostic}
            \end{itemize}
            \item Implementers may choose to reuse some or all functionalities from \kt{CommonBuiltins}
        \end{itemize}
    \end{block}

    \framebreak

    Module \kt{solve}'s \kt{CommonBuiltins} content:
    %
    \begin{description}
        \item[operators:] all Prolog standard operators

        \item[primitives:] \pl{abolish/1}, \pl{arg/3}, \pl{'=:='/2}, \pl{'>'/2}, \pl{'>='/2}, \pl{'<'/2}, \pl{'=<'/2}, \pl{'=$\backslash$='/2}, \pl{assert/1}, \pl{asserta/1}, \pl{assertz/1}, \pl{atom/1}, \pl{atom\_chars/2}, \pl{atom\_codes/2}, \pl{atom\_concat/3}, \pl{atomic/1}, \pl{atom\_length/2}, \pl{between/3}, \pl{bagof/3}, \pl{callable/1}, \pl{char\_code/2}, \pl{clause/2}, \pl{compound/1}, \pl{copy\_term/2}, \pl{current\_op/2}, \pl{current\_prolog\_flag/2}, \pl{ensure\_executable/1}, \pl{findall/3}, \pl{float/1}, \pl{functor/3}, \pl{get\_durable/2}, \pl{get\_ephemeral/2}, \pl{get\_persistent/2}, \pl{ground/1}, \pl{halt/0}, \pl{halt/1}, \pl{integer/1}, \pl{is/2}, \pl{natural/1}, \pl{nl/0}, \pl{nonvar/1}, \pl{'$\backslash$='/2}, \pl{number/1}, \pl{number\_chars/2}, \pl{number\_codes/2}, \pl{op/3}, \pl{repeat/0}, \pl{retract/1}, \pl{retractall/1}, \pl{reverse/2}, \pl{set\_durable/2}, \pl{set\_ephemeral/2}, \pl{setof/2}, \pl{set\_persistent/2}, \pl{set\_prolog\_plag/2}, \pl{sleep/1}, \pl{sub\_atom/5}, \pl{'@>'/2}, \pl{'@>='/2}, \pl{'=='/2}, \pl{'@<'/2}, \pl{'@=<'/2}, \pl{'$\backslash$=='/2}, \pl{'$\backslash$=@='/2}, \pl{'=@='/2}, \pl{'='/2}, \pl{'=..'/2}, \pl{var/1}, \pl{write/1}

        \item[functions:] \pl{abs/1}, \pl{'+'/2}, \pl{atan/1}, \pl{'/$\backslash$'/2}, \pl{'$\backslash$'/1}, \pl{'<<'/2}, \pl{'$\backslash$/'/2}, \pl{'>>'/2}, \pl{ceiling/1}, \pl{cos/1}, \pl{exp/1}, \pl{'**'/2}, \pl{float/1}, \pl{float\_fractional\_part/1}, \pl{float\_integer\_part/1}, \pl{'/'/2floor/1}, \pl{'//'/2}, \pl{mod/2}, \pl{'*'/2}, \pl{log/1}, \pl{rem/2}, \pl{round/1}, \pl{sign/1}, \pl{'-'/1}, \pl{sin/1}, \pl{sqrt/1}, \pl{'-'/2}, \pl{truncate/1}

        \item[theory:] \pl{not/1}, \pl{'->/2}, \pl{';'/2}, \pl{member/2}, \pl{append/3}
    \end{description}

    \framebreak

    Module \alert{\kt{solve-classic}}'s \kt{DefaultBuiltins} content:
    %
    \begin{description}
        \item[operators:] all operators in \kt{CommonBuiltins.operators}
        \item[functions:] all functions in \kt{CommonBuiltins.functions}
        \item[theory:] all clauses in \kt{CommonBuiltins.theory}
        %
        \begin{itemize}
            \item[+] \pl{call/1}, \pl{catch/3}, \pl{','/2}, \pl{'!'/0}, \pl{'$\backslash$+'/1}
        \end{itemize}
        \item[primitives:] all primitives in \kt{CommonBuiltins.primitives}
        %
        \begin{itemize}
            \item[+] \pl{throw/1}
        \end{itemize}
    \end{description}

    \framebreak

    Module \alert{\kt{solve-classic}}'s \kt{DefaultBuiltins} content:
    %
    \begin{description}
        \item[operators:] all operators in \kt{CommonBuiltins.operators}
        \item[functions:] all functions in \kt{CommonBuiltins.functions}
        \item[theory:] all clauses in \kt{CommonBuiltins.theory}
        \item[primitives:] all primitives in \kt{CommonBuiltins.primitives}
        %
        \begin{itemize}
            \item[+] \pl{call/1}, \pl{catch/3}, \pl{','/2}, \pl{'!'/0}, \pl{throw/1}, \pl{'$\backslash$+'/1}
        \end{itemize}
    \end{description}
\end{frame}

\section{Prolog as a State Machine: the \module{solve-classic} Module}

\begin{frame}[allowframebreaks]{Overview on the \module{solve-classic} Module}

    \begin{block}{Module \module{solve-classic} in a nutshell}
        \begin{itemize}
            \item Main implementation of \kt{Solver}

            \item Provides Prolog ISO Standard resolution

            \item State-Machine-based de#spired by \cite{tuprolog-sac08}
        \end{itemize}
    \end{block}

    \framebreak

    Main abstractions from this module (\alert{client-code}):
    %
    \begin{center}
        \includegraphics[width=.6\linewidth]{img/classic.pdf}
    \end{center}

    \begin{block}{The \kt{ClassicSolver}}
        \begin{itemize}
            \item State-Machine-based implementation of \kt{Solver}
            %
            \begin{itemize}
                \item whose instances are created via the \kt{ClassicSolverFactory}
                %
                \begin{itemize}
                    \item also accessible via \kt{Solver.classic}
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    Main abstractions from this module (details):
    %
    \begin{center}
        \includegraphics[width=.6\linewidth]{img/classic-details.pdf}
    \end{center}

    \begin{description}
        \item[\kt{State}] base type for states of the Prolog State Machine (PSM)

        \medskip

        \item[\kt{ClassicExecutionContext}] data structure containing the \kt{ExecutionContext} of (each state of) the PSM

        \medskip

        \item[\kt{SolutionIterator}] where the PSM is executed
        %
        \begin{itemize}
            \item[ie] an object iterating over states and outputting \kt{Solution}s
        \end{itemize}

        \medskip

        \item[\kt{MutableSolutionIterator}] a particular sort of solution iterator supporting \alert{hijack of state transitions}
        %
        \begin{itemize}
            \item[eg] to alter the execution context or the destination state
        \end{itemize}

        \medskip

        \item[\kt{AbstractClassicSolver}] abstract class for classic-like solvers
        %
        \begin{itemize}
            \item supporting the creation of custom solvers reusing (part of) the PSM
        \end{itemize}
    \end{description}
\end{frame}

\begin{frame}[allowframebreaks]{Prolog State Machine in a Nutshell}
    \begin{center}
        \includegraphics[width=.9\linewidth]{img/classic-sm.pdf}
    \end{center}

    \begin{block}{Main Features}
        \begin{itemize}
            \item 9 locations (1 initial, 2 ending)
            \item 2 ancillary data structures
            \item infinite possible states
        \end{itemize}
    \end{block}

    \begin{block}{Ancillary data structures}
        \begin{description}
            \item[Execution Context \textbf{Stack} ($\mathbf{E}$)] tracking currently exploring items of the proof-tree
            \item[Choice Point \textbf{Queue} ($\mathbf{C}$)] tracking unexplored items of the proof-tree
        \end{description}
    \end{block}

    \begin{block}{Locations}
        \begin{description}\small
            \item[Goal Selection] selects the next (sub-)goal to be proved, possibly popping from $\mathbf{E}$

            \item[Primitive Selection] looks for a primitive to solve the selected (sub-)goal;

            \item[Primitive Execution] if some is found, the $1^{st}$ response is consumed, while a choice points are appended to $\mathbf{C}$ for the others

            \item[Rule Selection] if no primitive is selected, some rule is looked for instead, for the same sub-goal;

            \item[Rule Execution] if a rule is found, resolution proceeds by pushing a new execution context to $\mathbf{E}$, to tackle the body;

            \item[Backtracking] if no rule is found, the sub-goal is considered failed and resolution continues taking the next choice point in $\mathbf{C}$.

            \item[End] reached when there are no more goals or no more choice points.

            \item[Execption] reached some primitive responses carries an exception. This is where catching occurs.

            \item[Halt] reached when an exception is not caught.
        \end{description}
    \end{block}
\end{frame}

\begin{frame}{Prolog State Machine, Formally}
    \begin{alertblock}{Formal specification here:}\small
        \begin{center}
            \url{https://github.com/tuProlog/2pkt-state-machine/releases/latest}
        \end{center}
        %
        \begin{itemize}
            \item[$\rightarrow$] download the \texttt{2pkt-state-machine-X.Y.Z-DATE.pdf} file
        \end{itemize}
    \end{alertblock}
\end{frame}

\section{Reading and Writing Data: the \module{io-lib} Module}

\begin{frame}[allowframebreaks]{Overview on IO in LP}

    \begin{block}{Purpose / Requirements}
        Provide \kt{Solver}s with I/O facilities:
        %
        \begin{enumerate}
            \item\label{iolib:platform-independence} in a \alert{platform-independent} way
            %
            \begin{itemize}
                \item[ie] supporting both JVM and JS
            \end{itemize}

            \item\label{iolib:solver-agnosticism} in a \alert{solver-implentation-agnostic} way
            %
            \begin{itemize}
                \item[ie] supporting both \emph{classic}, and \emph{streams} solvers
                \item[+] supporting future sorts of solvers too
            \end{itemize}

            \item\label{iolib:location-transparency} in a \alert{location-transparent} way
            %
            \begin{itemize}
                \item[ie] supporting transparent access to both \emph{local} and \emph{remote} resources
            \end{itemize}
        \end{enumerate}
    \end{block}

    \framebreak

    \begin{alertblock}{Main challenges}
        \begin{itemize}
            \item Kotlin MP does not provide platform independent I/O API
            \item JVM supports accessing both local and remote resources via \alert{streams}
            %
            \begin{itemize}
                \item blocking, synchronous API
                \item async API available too
            \end{itemize}
            \item JS server-side (i.e. NodeJS) supports accessing both local and remote resource via \alert{callbacks}
            %
            \begin{itemize}
                \item non-blocking, asynchronous API
                \item sync API available too
            \end{itemize}
            \item JS browser-side supports accessing remote resources via \alert{callbacks}
            %
            \begin{itemize}
                \item non-blocking, asynchronous API
                \item NO sync API
            \end{itemize}
            \item[$\rightarrow$] requirements \ref{iolib:platform-independence} and \ref{iolib:location-transparency} are hard to attain
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{exampleblock}{Strategy}
        \begin{enumerate}
            \item Define minimal multi-platform API for I/O
            \item Provide platform-specific implementations for that API
            \item Provide implementation of \kt{Channel}s exploiting such API
            \item Provide logic predicated to manipulate \kt{Channel}s from LP
        \end{enumerate}
    \end{exampleblock}

    \framebreak

    \begin{block}{Goal}
        \centering
        Support access to local/remote resources to any solver on all platforms
    \end{block}

    \medskip

    Cf. the \pl{consult/1} predicate/directive, supporting loading of external theories into the current solver's static KB:
    %
    \plSnippet{snippets/consult.pl}

\end{frame}

\begin{frame}[allowframebreaks]{The multi-platform notion of \kt{Url}}
    \begin{center}
        \includegraphics[width=.5\linewidth]{img/url.pdf}
    \end{center}

    \begin{block}{Purpose}
        \begin{itemize}
            \item Mimicking Java's URL type
            \item Providing unified multi-platform API for I/O
            \item Supporting requirements \ref{iolib:platform-independence} and \ref{iolib:location-transparency}
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}[allowframebreaks]{Content of the \kt{IOLib}}
    \kt{it.unibo.tuprolog.solve.libs.io.\alert{IOLib}}
    %
    \medskip
    %
    \begin{description}

        \item[primitives:] \pl{at\_end\_of\_stream/0}, \pl{at\_end\_of\_stream/1}, \pl{char\_conversion/2}, \pl{close/1}, \pl{close/2}, \pl{consult/1}, \pl{current\_char\_conversion/2}, \pl{current\_input/1}, \pl{current\_output/1}, \pl{flush\_output/1}, \pl{get\_byte/1}, \pl{get\_byte/2}, \pl{get\_char/1}, \pl{get\_char/2}, \pl{get\_code/1}, \pl{get\_code/2}, \pl{nl/1}, \pl{open/3}, \pl{open/4}, \pl{peek\_byte/1}, \pl{peek\_byte/2}, \pl{peek\_char/1}, \pl{peek\_char/2}, \pl{peek\_code/1}, \pl{peek\_code/2}, \pl{put\_byte/1}, \pl{put\_byte/2}, \pl{put\_char/1}, \pl{put\_char/2}, \pl{put\_code/1}, \pl{put\_code/2}, \pl{read/1}, \pl{read/2}, \pl{read\_term/2}, \pl{read\_term/3}, \pl{set\_input/1}, \pl{set\_output/1}, \pl{set\_theory/1}, \pl{stream\_property/2}, \pl{write/2}, \pl{write\_canonical/1}, \pl{write\_canonical/2}, \pl{write\_eq/1}, \pl{write\_eq/2}, \pl{write\_term/2}, \pl{write\_term/3}

        \framebreak

        \item[operators:] none

        \item[theory:] none

        \item[functions:] none
    \end{description}

    \bigskip

    \begin{block}{Takeaway}\centering
        \kt{IOLib} = I/O predicates from the Prolog ISO Standard \ccite{prologISO-pt1}, realised as \kt{Solver}-independent primitives
    \end{block}
\end{frame}

% \begin{frame}[allowframebreaks]{Platform-specific Issues}

% \end{frame}

\section{OOP and Prolog: the \module{oop-lib} Module}

\begin{frame}[allowframebreaks]{Overview on the OOP Lib Design}

    \begin{block}{Perspective}
        \begin{description}
            \item[\kt{Solver}s] $\rightarrow$ let OOP exploit LP
            \item[\kt{Primitive}s] $\rightarrow$ let LP wrap/call OOP
            \item[\module{oop-lib}] $\rightarrow$ \alert{lets LP exploit OOP}
        \end{description}
    \end{block}

    \framebreak

    Concept:
    %
    \bigskip
    %
    \begin{enumerate}
        \item Two more sub-sorts of \kt{Atom}, generically called \alert{\kt{Ref}erences}
        %
        \begin{description}
            \item[\kt{ObjectRef}erences] | representing references to \alert{objects}
            \item[\kt{TypeRef}erences] | representing references to \alert{type}s
            %
            \begin{itemize}
                \item[eg] interfaces, classes, etc.
            \end{itemize}
        \end{description}
        %
        \begin{center}
            \includegraphics[width=\linewidth]{img/refs.pdf}
        \end{center}

        \framebreak

        \item \kt{TypeRef}erenes can be attained from type names via \pl{type/2}:
        %
        \plSnippet{snippets/type2.pl}

        \bigskip

        \item \kt{ObjectRef}erenes can be attained from \kt{TypeRef}erenes via \pl{new\_object/2}:
        %
        \plSnippet[\tiny]{snippets/new_object2.pl}

        \framebreak

        \item \kt{Ref}erences' methods can be invoked via the following syntax:
        %
        \begin{center}
            \pl{Ref\alert{.}methodName(Arg$_1$, \ldots, Arg$_n$)}
        \end{center}

        \smallskip

        \item \kt{Ref}erences' properties, fields, 0-ary methods can be similarly accessed:
        %
        \begin{center}
            \pl{Ref\alert{.}propertyName} \quad or \quad \pl{Ref.'PropertyName'}
        \end{center}

        \smallskip

        \item Results of properties / fields / methods can be bound to variables via \kt{':='/2}:
        %
        \plSnippet[\tiny]{snippets/System_out_println.pl}

        \framebreak

        \item Terms are automatically converted into object of the \alert{most adequate} type, upon method invocation, and result are converted back into terms
        %
        \begin{itemize}
            \item we call this \alert{smart cast}
            \item smart \alert{overload selection} is performed in case of ambiguity
        \end{itemize}
        %
        \plSnippet[\tiny]{snippets/StringBuilder_append_toString.pl}
        %
        \begin{itemize}\small
            \item recall that Java's \kt{StringBuilder.\textit{append}} has several overloads
        \end{itemize}

        \framebreak

        \item \alert{Aliases} are available to quick-access common types or objects
        %
        \plSnippet[\tiny]{snippets/aliases.pl}

        \framebreak

        \item \alert{Aliases} can be
        %
        \begin{itemize}
            \item inspected via \pl{alias/2}
            \item added (resp. removed) via \pl{register/2} (resp. \pl{unregister/1})
            \item used in place of actual \kt{Ref}erences via the \alert{de-aliasing operator} \pl{\$/1}
        \end{itemize}
        %
        \plSnippet[\tiny]{snippets/aliases_usage.pl}

        \framebreak

        \item \alert{Specific casts} can be performed via the \alert{cast operator} \pl{as/2}
        %
        \begin{itemize}
            \item which enables \emph{explicit} overload selection
        \end{itemize}
        %
        \plSnippet[\tiny]{snippets/overload_selection.pl}
    \end{enumerate}

    \framebreak

    \begin{alertblock}{Notable remarks about \module{oop-lib}}
        \begin{itemize}
            \item API is currently considered unstable
            \item Design is tailored on Kotlin's OOP model:
            %
            \begin{itemize}
                \item fields $\rightarrow$ properties
                \item static members $\rightarrow$ companion objects
                \item strong reliance on Kotlin's reflection
                \item pervasive exploitation of \kt{KClass}es
            \end{itemize}
            \item Design is multi-platform, yet only JVM implementation works
            %
            \begin{itemize}
                \item Kotlin's JS reflection is poorly supported ATM
                \item Kotlin's JVM reflection is quite buggy ATM
                \item Kotlin's reflection has a very clean design
            \end{itemize}
            \item On JVM, fields and static are supported too!
        \end{itemize}
    \end{alertblock}

    % references to types and objects

    % term to object conversions
    %     + smart cast and overloading selection

    % object to term conversions

    % ad-hoc predicates

    % ad-hoc operators

    % aliases
\end{frame}

\subsection{\kt{Ref}erences: \kt{TypeRef}erences and \kt{ObjectRef}}

\begin{frame}[allowframebreaks]{The \kt{Ref} Type Hierarchy}

    \begin{center}
        \includegraphics[width=.8\linewidth]{./img/full-refs.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{Ref} type is a sub-type of \kt{Atom}}
        \centering
        Base type for all sorts of references
    \end{block}
    %
    \begin{description}
        \item[\kt{invoke(TermToObjectConverter, String, \meta{Terms}): Result}] invokes a \alert{method} on the current \kt{Ref}erence by name, passing the provided \kt{Term}s as arguments, which are converted into objects using the provided \kt{TermToObjectConverter}

        \item[\kt{invoke(String, \meta{Terms}): Result}] invokes a \alert{method} on the current \kt{Ref}erence by name, passing the provided \kt{Term}s as arguments, which are converted into objects using the \emph{default} \kt{TermToObjectConverter}

        \item[\kt{assign(TermToObjectConverter, String, Term): Boolean}] assign the provided \kt{Term} as the new value of some \alert{property}/\alert{field} of the current \kt{Ref}erence, selected by name. The term is converted into an object using the provided \kt{TermToObjectConverter}

        \item[\kt{assign(String, Term): Boolean}] assign the provided \kt{Term} as the new value of some \alert{property}/\alert{field} of the current \kt{Ref}erence, selected by name. The term is converted into an object using the \emph{default} \kt{TermToObjectConverter}
    \end{description}

    \framebreak

    \begin{block}{The \kt{TypeRef} type is a sub-type of \kt{Ref}}
        \centering
        Base type for all sorts of references to \alert{types}---there including interfaces, classes, Kotlin objects, etc.
    \end{block}
    %
    \begin{description}
        \item[\kt{type: KClass<*>}] the type being referenced

        \item[\kt{invoke(\ldots)}] methods inherited from \kt{Ref} can be used to call both \alert{static} methods and \kt{companion objects'} methods

        \item[\kt{assign(\ldots)}] methods inherited from \kt{Ref} can be used to set both static properties/methods or companion objects' ones

        \item[\kt{create(TermToObjectConverter, \meta{Terms}): Result}] calls the constructor of the referenced type to create a new instance. The provided terms are passed to the constructor after being converted into objects using the provided \kt{TermToObjectConverter}

        \item[\kt{create(\meta{Terms}): Result}] calls the constructor of the referenced type to create a new instance. The provided terms are passed to the constructor after being converted into objects using the \emph{default} \kt{TermToObjectConverter}
    \end{description}

    \framebreak

    \begin{block}{The \kt{ObjectRef} type is a sub-type of \kt{Ref}}
        \centering
        Base type for all sorts of references to \alert{objects}---i.e. instances of types
    \end{block}
    %
    \begin{description}
        \item[\kt{object: Any}] the object being referenced

        \item[\kt{invoke(\ldots)}] methods inherited from \kt{Ref} can be used to call both \alert{instance} methods on the referenced objects

        \item[\kt{assign(\ldots)}] methods inherited from \kt{Ref} can be used to set \alert{instance} properties/fields on the referenced objects
    \end{description}

    \framebreak

    \begin{block}{The \kt{Result} type}
        Instances of \kt{Result} aim to wrap objects:
        %
        \begin{itemize}
            \item returned by invoking methods on \kt{Ref}erences
            \item created from \kt{TypeRef}erences
        \end{itemize}

        Two sub-types:
        %
        \begin{description}
            \item[\kt{None}] representing the lack of result
            \item[\kt{Value}] representing the return of an object
        \end{description}
    \end{block}
    %
    \begin{description}
        \item[\kt{value: Any?}] is the returned object

        \item[\kt{toTerm(): Term?}] converts the returned value (if any) into a \kt{Term}, using the default \kt{ObjectToTermConverter}

        \item[\kt{asObjectRef(): ObjectRef?}] converts the returned value (if any) into an \kt{ObjectRef}erence
    \end{description}

\end{frame}

\begin{frame}{Creation of \kt{Ref}erences}
    \begin{description}
        \item[\kt{ObjectRef.of(Any?)}] creates a new \kt{ObjectRef} to the provided object. May return a \kt{NullRef} is the provided object is \kt{null}

        \bigskip

        \item[\kt{ObjectRef.NULL}] returns the singleton instance of \kt{NullRef}

        \bigskip

        \item[\kt{TypeRef.of(KClass<*>)}] creates a new \kt{TypeRef} to the provided type
    \end{description}
\end{frame}

\subsection{OOP to/from LP Conversions}

\begin{frame}[allowframebreaks]{The \kt{TypeFactory} Type}
    \begin{block}{Purpose}
        \begin{itemize}
            \item Loading OOP types from names
            \item Instantiating \kt{TypeRef}erences from type names
        \end{itemize}
    \end{block}

    \begin{alertblock}{Concept}
        \begin{itemize}
            \item Type discovery/loading is platform specific\ldots
            \item \ldots a platform-agnostic type is necessary in a multi-platform module
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{center}
        \includegraphics[width=.5\linewidth]{img/TypeFactory.pdf}
    \end{center}

    \framebreak

    \begin{alertblock}{Platform-specific names for types}
        \begin{description}
            \item[JVM:] \kt{name.of.package.\alert{TypeName}}
            \item[JS:] \kt{\alert{module-name}:name.of.package.\alert{TypeName}}
        \end{description}
    \end{alertblock}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TermToObjectConverter} Type}
    \begin{block}{Purpose}
        \begin{itemize}
            \item Converting \alert{arguments} of methods into objects upon \alert{invocation}
            \item Converting \alert{arguments} of constructors into objects upon \alert{creation}
            \item Converting \alert{values} of properties into objects upon \alert{assignment}
        \end{itemize}
    \end{block}

    \begin{alertblock}{Concept}
        \begin{itemize}
            \item Each LP type may correspond to several OOP types
            \item Preferences may exists among target OOP types
            \item Each LP type has 1 preferred corresponding OOP type
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{center}
        \includegraphics[width=.6\linewidth]{img/TermToObjectConverter.pdf}
    \end{center}

    \framebreak

    \input{tab-terms-to-objects.tex}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{ObjectToTermConverter} Type}
    \begin{block}{Purpose}
        \begin{itemize}
            \item Converting \alert{results} of methods invocations into \alert{\kt{Term}s}
            \item Converting \alert{results} of constructors into \alert{\kt{ObjectRef}erences}
        \end{itemize}
    \end{block}

    \begin{alertblock}{Concept}
        \begin{itemize}
            \item Conversion of OOP types into LP ones is \alert{straightforward}
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{center}
        \includegraphics[width=.5\linewidth]{img/ObjectToTermConverter.pdf}
    \end{center}

    \framebreak

    \begin{center}
        \input{tab-objects-to-terms.tex}
    \end{center}
\end{frame}

\subsection{Overload Selection}

\begin{frame}[allowframebreaks]{The \kt{OverloadSelector} Type}
    \begin{block}{Purpose}
        Selecting the \alert{most adequate overload}
        \begin{itemize}
            \item of a method / property / constructor
            \item w.r.t. the admissible LP$\rightarrow$OOP conversions for \alert{actual} arguments
            \item when invoking / assigning / creating
        \end{itemize}
    \end{block}

    \begin{alertblock}{Concept}
        \begin{itemize}
            \item Many \alert{strategies} may be exploited to select an overload
            \item \kt{OverloadSelector} is the general API to do so
            \item They essentially select \alert{target OOP types} for actual arguments
        \end{itemize}
    \end{alertblock}

    \framebreak

    \begin{center}
        \includegraphics[width=.5\linewidth]{img/OverloadSelector.pdf}
    \end{center}

    \framebreak

    \begin{exampleblock}{Current strategy (JVM)}
        An attempt is performed to select the available overload which
        %
        \begin{itemize}
            \item maximizes the sum of the proprities of all target OOP types
            \item using explicit casts (i.e. \pl{as/2}) as \alert{strong} constraints
            \item taking the most specific formal type into account
            %
            \begin{itemize}
                \item[eg] among \kt{Any} and \kt{String}, the latter should be preferred for \kt{Atom}s
            \end{itemize}
            \item taking actual values into account
            %
            \begin{itemize}
                \item[eg] 129 cannot be converted into \kt{Byte}
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
\end{frame}

\subsection{Logic Predicates and Operators for OOP}

\begin{frame}{Content of the \kt{OOPLib}}

    \kt{it.unibo.tuprolog.solve.libs.oop.\alert{OOPLib}}
    %
    \vfill
    %
    \begin{description}

        \item[operators:] \pl{'.'/2}, \pl{':='/2}, \pl{'as/2'}, \pl{'\$'/1}

        \vfill

        \item[theory:] \pl{':='/2}, \pl{'.'/2}, \pl{fluent\_reduce/2}, \pl{new\_object/2}, \pl{property\_reduce/2}

        \vfill

        \item[primitives:] \pl{assign/3}, \pl{cast/3}, \pl{type/2}, \pl{invoke\_method/3}, \pl{invoke\_strict/3}, \pl{new\_object/3}, \pl{null\_ref/1}, \pl{object\_ref/1}, \pl{ref/1}, \pl{register/2}, \pl{type\_ref/1}, \pl{unregister/1}

        \vfill

        \item[functions:] none
    \end{description}
\end{frame}

% \begin{frame}{Main predicates of the \kt{OOPLib}}
%     \ttfamily
%     invoke\_method/3
%     invoke\_strict/3
%     assign/3
%     cast/3
%     new\_object/3
%     new\_object/2 (rule)
%     register/2
%     unregister/1
%     alias/2 (rule)
%     :=/2 (rule)
%     ./2 (rule)
%     fluent\_reduce/3
%     property\_reduce/3
% \end{frame}

\section{LP + OOP + FP in Kotlin: the \module{dsl-*} Modules}

\begin{frame}[allowframebreaks]{Overview on the DSL}

    \begin{block}{Perspective}
        \begin{description}
            \item[\kt{Solver}s] $\rightarrow$ let OOP exploit LP
            \item[\kt{Primitive}s] $\rightarrow$ let LP wrap/call OOP
            \item[\module{oop-lib}] $\rightarrow$ lets LP exploit OOP
            \item[\module{dsl-*}] $\rightarrow$ \alert{let Kotlin expoit LP with Prolog-like syntax}
        \end{description}
    \end{block}

    \framebreak

    \begin{block}{Purpose}
        \begin{itemize}
            \item integrating OOP, FP and LP
            \item bringing OOP software engineering techniques to LP and FP
            \item bringing declarativity from FP and LP to OOP
            \item enriching the Kotlin language in a fruitful and natural way
        \end{itemize}
    \end{block}

    \framebreak

    \begin{exampleblock}{DSL in practice}
        \begin{itemize}
            \item writing tests using LP-like syntax
            \item[!] \alert{without} relying a parser
            %
            \begin{itemize}
                \item to keep the dependency graph small/sparse
                \item to prevent developers from using the parser unless strictly needed
            \end{itemize}
        \end{itemize}
    \end{exampleblock}

    \framebreak

    \begin{columns}
        \centering
        \begin{column}{.48\linewidth}
            \ktSnippet[\tiny]{snippets/Relatives.kt}
        \end{column}
        \hfill
        \begin{column}{.48\linewidth}
            \plSnippet[\tiny]{snippets/relatives.pl}
        \end{column}
    \end{columns}

\end{frame}

\begin{frame}[allowframebreaks]{Design Principles of the DSL (cf. \ccite{kotlinDSl4PrologWoa2020})}
    \begin{enumerate}
        \item the DSL has to be a \textit{strict} extension of Kotlin
        \begin{description}
            \item [$\rightarrow$] no Kotlin feature is hindered by using the DSL
        \end{description}
        \vfill
        \item the DSL has to be fully \textit{interoperable} with the hosting language
        \begin{description}
            \item [$\rightarrow$] all Kotlin features may be exploited by the DSL
        \end{description}
        \vfill
        \item the DSL has to be fully \textit{encapsulated} and \textit{identifiable}
        \begin{description}
            \item [$\rightarrow$] preventing unintended usage
        \end{description}
        \vfill
        \item the DSL should be as close as possible to LP, syntactically and semantically
        \begin{description}
            \item [$\rightarrow$] easing its exploitation by logic programmers
        \end{description}
    \end{enumerate}
\end{frame}

\begin{frame}[allowframebreaks]{Architecture}

    \begin{center}
        \includegraphics[width=0.3\linewidth]{img/dsl-layers.pdf}
    \end{center}

    \framebreak

    \begin{center}
        \includegraphics[width=0.50\linewidth]{img/dsl-core.pdf}
    \end{center}

    \framebreak

    \begin{block}{The \kt{PrologAwareScope} interface}
        \begin{itemize}
            \item Enables the conversion of Kotlin objects to Prolog \kt{Term}s via the \kt{Any.toTerm()} extension method
            \item using the following type mapping:
            \begin{itemize}
                \item a Kotlin number is converted either to a Prolog real or integer number
                \item a Kotlin string is converted either to a Prolog variable or atom
                \item a Kotlin boolean is always converted to an atom
                \item a Kotlin iterable is always converted into a Prolog list
                \begin{description}
                    \item [!] each item has to be convertible to a \kt{Term}
                \end{description}
                \item Kotlin objects that are sub-types of \kt{Term} remain unaffected
                \item if the object cannot be converted to a \kt{Term}, an error is raised
            \end{itemize}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{The \kt{VariablesAwareScope} interface}
        \begin{itemize}
            \item provides \kt{A-Z} shortcuts to instantiate Prolog variables
        \end{itemize}
    \end{block}
    %
    \begin{block}{The \kt{PrologStdLibScope} interface}
        \begin{itemize}
            \item provides a number of methods that allow the invocation of standard library predicates
            \begin{description}
                \item [e.g.] \kt{assert}, \kt{retract}, \kt{bagof}, \kt{consult}, etc\ldots
            \end{description}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{The \kt{PrologScope} interface}
        \begin{itemize}
            \item enables the construction of compound terms
            \begin{description}
                \item [$\rightarrow$] via the \kt{String.invoke()} extension method
                \item [e.g.] \kt{"human"("socrates")}
            \end{description}
            \item allows to retrieve variable substitutions in a leaner fashion, without having to create explicit variables through \kt{varOf()}
            \begin{description}
                \item [$\rightarrow$] via the \kt{Substitution.get(Any)} extension method
                \item [e.g.] \kt{substitution.get("X")}
            \end{description}
            \item adds the capability of converting Kotlin objects into logic clauses
            \begin{description}
                \item [$\rightarrow$] via the \kt{rule} and \kt{fact} factory methods
                \item [$\rightarrow$] via the \kt{Any.and(Any)} and \kt{Any.or(Any)} extension methods
            \end{description}
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{The \kt{PrologScopeWithUnification interface}}
        \begin{itemize}
            \item exposes a number of extension methods providing unification-related support to Kotlin objects
            \begin{description}
                \item [!] provided that they can be converted into \kt{Term}s
            \end{description}
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{Any.mguWith(Any): Substitution}] computes the MGU between two Kotlin objects
        \item [\kt{Any.matches(Any): Boolean}] checks whether two Kotlin objects match or not, according to logic unification
        \item [\kt{Any.unifyWith(Any): Term?}] unifies two Kotlin objects, according to logic unification
    \end{description}

    \framebreak

    \begin{block}{The \kt{PrologScopeWithTheories} interface}
        \begin{itemize}
            \item allows the combination of clauses into logic theories
            \begin{description}
                \item [$\rightarrow$] via the \kt{theoryOf} factory method
            \end{description}
        \end{itemize}
    \end{block}
    %
    \begin{block}{The \kt{PrologScopeWithResolution} interface}
        \begin{itemize}
            \item adds the capability of performing logic queries and consuming their solutions
            \item provides methods that allow
            \begin{itemize}
                \item instancing Prolog solvers
                \begin{description}
                    \item [$\rightarrow$] via \kt{solverOf(...)}
                \end{description}
                \item loading static and dynamic Prolog theories
                \begin{description}
                    \item [$\rightarrow$] via \kt{staticKb(...)}, \kt{dynamicKb(...)}
                \end{description}
                \item invoking Prolog queries on the loaded theories
                \begin{description}
                    \item [$\rightarrow$] via \kt{solve(...)}
                \end{description}
            \end{itemize}
        \end{itemize}
    \end{block}

\end{frame}

\begin{frame}{Usage Example}
    \ktSnippet[\tiny]{./snippets/DslNQueens.kt}
\end{frame}

\section{Parsing Logic Knowledge: the \module{parser-*} Modules}

\begin{frame}[allowframebreaks]{The \kt{TermParser} Type}

    \begin{block}{The \kt{TermParser} interface}
        \begin{itemize}
            \item provides methods to parse \kt{Term}s from strings
            \begin{description}
                \item[!] throwing a \kt{ParseException} upon failure
            \end{description}
            \item allows to select the operators used for parsing
        \end{itemize}
    \end{block}
    %
    All methods come in two forms:
    %
    \begin{description}
        \item[\kt{parse\meta{T}(String): \meta{T}}] parses a \kt{\meta{T}} from a given string, using default operators
        \item[\kt{parse\meta{T}(String, OperatorSet): \meta{T}}] parses a \kt{\meta{T}} from a given string, using the given operators
    \end{description}
    %
    with \kt{\meta{T}} a sub-type of \kt{Term} %, \kt{Struct}, \kt{Constant}, \kt{Var}, \kt{Atom}, \kt{Numeric}, \kt{Integer}, \kt{Real} or \kt{Clause}

    \framebreak

    Static factories for \kt{TermParser}:
    %
    \begin{description}
        \item [\kt{withNoOperator: TermParser}] creates a parser with no operators loaded
        \item [\kt{withStandardOperators: TermParser}] creates a parser with standard operators loaded
        \item [\kt{withDefaultOperators: TermParser}] creates a parser with default operators loaded (\kt{standard} operators)
        \item [\kt{withOperators(OperatorsSet): TermParser}] creates a parser with the given \kt{OperatorSet} loaded
        \item [\kt{withOperators(vararg Operator): TermParser}] creates a parser with the given operators loaded
    \end{description}

    \framebreak

    Successful \kt{Term} parsing:
    %
    \ktSnippet{./snippets/TermParserUsage.kt}

    \framebreak

    \kt{Term} parsing failure:
    %
    \ktSnippet{./snippets/TermParserFailure.kt}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TermReader} Type (JVM-only)}
    \begin{block}{The \kt{TermReader} interface}
        \begin{itemize}
            \item provides methods to parse \kt{Term}s
            \item input is loaded \textbf{lazily} from an \kt{InputStream}/\kt{Reader}/\kt{String}
            \item only available on the JVM as part of the \kt{jvm} implementations of the \kt{parser-core} module
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{readTerm(Reader): Term?}] tries to read a term from the given \kt{Reader}, with default operators
        \item [\kt{readTerm(Reader, OperatorSet): Term?}] tries to read a term from the given \kt{Reader}, with the given operator set
        \item [\kt{readTerm(InputStream): Term?}] tries to read a term from the given \kt{InputStream}, with default operators
        \item [\kt{readTerm(InputStream, OperatorSet): Term?}] tries to read a term from the given \kt{InputStream}, with the given operator set
    \end{description}

    \framebreak

    Multiple-\kt{Term} reading methods:
    %
    \begin{description}
        \item [\kt{readTerms(Reader): Sequence<Term>}] reads a sequence of terms from the given \kt{Reader}, with default operators
        \item [\kt{readTerms(Reader, OperatorSet): Sequence<Term>}] reads a sequence of terms from the given \kt{Reader}, with the given operator set
        \item [\kt{readTerms(InputStream): Sequence<Term>}] reads a sequence of terms from the given \kt{InputStream}, with default operators
        \item [\kt{readTerms(InputStream, OperatorSet): Sequence<Term>}] reads a sequence of terms from the given \kt{InputStream}, with the given operator set
        \item [\kt{readTerms(String): Sequence<Term>}] reads a sequence of terms from the given \kt{String}, with default operators
        \item [\kt{readTerms(String, OperatorSet): Sequence<Term>}] reads a sequence of terms from the given \kt{String}, with the given operator set
    \end{description}

    \framebreak

    Static factories for \kt{TermReader}:
    %
    \begin{description}
        \item [\kt{withNoOperator: TermReader}] creates a \kt{TermReader} with no operators loaded
        \item [\kt{withStandardOperators: TermReader}] creates a \kt{TermReader} with standard operators loaded
        \item [\kt{withDefaultOperators: TermReader}] creates a \kt{TermReader} with default operators loaded (\kt{standard} operators)
        \item [\kt{withOperators(OperatorsSet): TermReader}] creates a \kt{TermReader} with the given \kt{OperatorSet} loaded
        \item [\kt{withOperators(vararg Operator): TermReader}] creates a \kt{TermReader} with the given operators loaded
    \end{description}

    \framebreak

    Reading \kt{Term}s from a \kt{String}:
    %
    \ktSnippet{./snippets/TermReaderString.kt}
    %
    Reading \kt{Term}s from a \kt{File}:
    %
    \ktSnippet{./snippets/TermReaderFile.kt}

    \framebreak

    Reading failure:
    %
    \ktSnippet{./snippets/TermReaderFailure.kt}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{ClausesParser} Type}
    \begin{block}{The \kt{ClausesParser} interface}
        \begin{itemize}
            \item provides methods to parse multiple \kt{Clause}s from strings
            \begin{description}
                \item[!] throwing a \kt{ParseException} upon failure
            \end{description}
            \item allows to select the operators used for parsing
            \item very similar to \kt{TermParser}, but is capable of parsing entire theories instead of single \kt{Term}s
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{parseTheory(String, OperatorSet): Theory}] parses a \kt{Theory} from the given string, using the given operator set
        \item [\kt{parseTheory(String): Theory}] parses a \kt{Theory} from the given string, using default operators
        \item [\kt{parseClausesLazily(String, OperatorSet): Sequence<Clause>}] parses a \textit{lazily evaluated} sequence of \kt{Clause}s from the given string, with the given operator set
        \item [\kt{parseClausesLazily(String): Sequence<Clause>}] parses a \textit{lazily evaluated} sequence of \kt{Clause}s from the given string, with default operators
        \item [\kt{parseClauses(String, OperatorSet): List<Clause>}] parses a sequence of \kt{Clause}s from the given string, with the given operator set
        \item [\kt{parseClauses(String): List<Clause>}] parses a sequence of \kt{Clause}s from the given string, with default operators
    \end{description}

    \framebreak

    Static factories for \kt{ClausesParser}:
    %
    \begin{description}
        \item [\kt{withNoOperator: ClausesParser}] creates a parser with no operators loaded
        \item [\kt{withStandardOperators: ClausesParser}] creates a parser with standard operators loaded
        \item [\kt{withDefaultOperators: ClausesParser}] creates a parser with default operators loaded (\kt{standard} operators)
        \item [\kt{withOperators(OperatorSet): ClausesParser}] creates a parser with the given \kt{OperatorSet} loaded
        \item [\kt{withOperators(vararg Operator): ClausesParser}] creates a parser with the given operators loaded
    \end{description}

    \framebreak

    Successful clauses parsing (as \kt{Theory}, \kt{Sequence} and \kt{List} of \kt{Clause}s):
    %
    \ktSnippet{./snippets/ClausesParserUsage.kt}

    \framebreak

    \kt{Clause}s parsing failure:
    %
    \ktSnippet{./snippets/ClausesParserFailure.kt}

\end{frame}

\section{(De)Serialising Logic Knowledge: the \module{serialize-*} Modules}

\begin{frame}[allowframebreaks]{(De)Serialisation Overview}
    % onion design: (de)objectifiers <-> (de)serializers

    \begin{block}{Serialisation}
        \begin{itemize}
            \item performed via \kt{Serializer}s and \kt{Objectifier}s
            \item \kt{Serializer}s convert \kt{Term}s/\kt{Theory}s into strings
            \begin{description}
                \item[!] formatted according to some \kt{MIME} type
            \end{description}
            \item \kt{Objectifier}s are used by \kt{Serializer}s to convert \kt{Term}s/\kt{Theory}s into translatable objects first
            \begin{description}
                \item[!] acting as a middleware layer
            \end{description}
        \end{itemize}
    \end{block}
    %
    \begin{block}{De-serialisation}
        \begin{itemize}
            \item serialisation's dual process
            \item converting strings into \kt{Term}s and \kt{Theory}s
            \item employing \kt{Deserializer}s and \kt{Deobjectifier}s
        \end{itemize}
    \end{block}

    \framebreak

    \begin{block}{\kt{Term} vs \kt{Theory} (de)serialisation}
        \begin{itemize}
            \item \twopkt's design tackles both single and multiple serialisation strategies
            \begin{itemize}
                \item \kt{:serialize-core} concerns single-\kt{Term} (de)serialisation
                \item \kt{:serialize-theory} concerns \kt{Theory} (de)serialisation
            \end{itemize}
        \end{itemize}
    \end{block}
    %
    \begin{block}{Supported MIME types}
        \begin{itemize}
            \item currently, (de)serialisation supports \kt{JSON} and \kt{YAML}
        \end{itemize}
    \end{block}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Serializer}/\kt{Objectifier} hierarchy}
    \begin{center}
        \includegraphics[width=\linewidth]{img/serialization.pdf}
    \end{center}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{Deserializer}/\kt{Deobjectifier} hierarchy}
    \begin{center}
        \includegraphics[width=\linewidth]{img/deserialization.pdf}
    \end{center}
\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TermSerializer} Type}

    \begin{block}{The \kt{TermSerializer} type}
        \begin{itemize}
            \item exposes methods that perform \kt{Term} serialisation
            \item targeting a specific MIME type
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{mimeType: MimeType}] the format to which input \kt{Term}s are serialized
        \item [\kt{serialize(Term): String}] serialises a given \kt{Term} to a string formatted according to the selected \kt{mimeType}
        \item [\kt{serializeMany(vararg Term): String}] serialises the given \kt{Term}s to a string formatted according to the selected \kt{mimeType}
        \item [\kt{serializeMany(Iterable<Term>): String}] analogous to \kt{serializeMany(varargs Term): String}
        \item [\kt{serializeMany(Sequence<Term>): String}] analogous to \kt{serializeMany(varargs Term): String}
    \end{description}

    \framebreak

    Static factories for \kt{TermSerializer}:
    %
    \begin{description}
        \item [\kt{of(MimeType): TermSerializer}] creates a new \kt{TermSerializer} employing the given format
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TermDeserializer} Type}

    \begin{block}{The \kt{TermDeserializer} Type}
        \begin{itemize}
            \item provides methods that convert strings back to \kt{Term}s
            \item according to a specific MIME type
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{mimeType: MimeType}] the format from which the input string is de-serialised
        \item [\kt{deserialize(String): Term}] de-serialises the given string according to the selected \kt{mimeType}, yielding a single \kt{Term}
        \item [\kt{deserializeMany(String): Iterable<Term>}]  de-serialises the given string according to the selected \kt{mimeType}, yielding multiple \kt{Term}s
    \end{description}

    \framebreak

    Static factories for \kt{TermDeserializer}:
    %
    \begin{description}
        \item [\kt{of(MimeType): TermDeserializer}] creates a new \kt{TermDeserializer} according to the given format
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TheorySerializer} Type}

    \begin{block}{The \kt{TheorySerializer} Type}
        \begin{itemize}
            \item exposes methods that perform \kt{Theory} serialisation
            \item targeting a specific MIME type
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{mimeType: MimeType}] the format to which input \kt{Theory}s are serialized
        \item [\kt{serialize(Theory): String}] serialises a given \kt{Theory} to a string formatted according to the selected \kt{mimeType}
        \item [\kt{serializeMany(vararg Theory): String}] serialises the given \kt{Theory}s to a string formatted according to the selected \kt{mimeType}
        \item [\kt{serializeMany(Iterable<Theory>): String}] analogous to \kt{serializeMany(varargs Theory): String}
        \item [\kt{serializeMany(Sequence<Theory>): String}] analogous to \kt{serializeMany(varargs Theory): String}
    \end{description}

    \framebreak

    Static factories for \kt{TheorySerializer}:
    %
    \begin{description}
        \item [\kt{of(MimeType): TheorySerializer}] creates a new \kt{TheorySerializer} employing the given format
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{The \kt{TheoryDeserializer} Type}

    \begin{block}{The \kt{TheoryDeserializer} Type}
        \begin{itemize}
            \item provides methods that convert strings back to \kt{Theory}s
            \item according to a specific MIME type
        \end{itemize}
    \end{block}
    %
    \begin{description}
        \item [\kt{mimeType: MimeType}] the format from which the input string is de-serialised
        \item [\kt{deserialize(String): Theory}] de-serialises the given string according to the selected \kt{mimeType}, yielding a single \kt{Theory}
        \item [\kt{deserializeMany(String): Iterable<Theory>}]  de-serialises the given string according to the selected \kt{mimeType}, yielding multiple \kt{Theory}s
    \end{description}

    \framebreak

    Static factories for \kt{TheoryDeserializer}:
    %
    \begin{description}
        \item [\kt{of(MimeType): TheoryDeserializer}] creates a new \kt{TheoryDeserializer} according to the given format
    \end{description}

\end{frame}

\begin{frame}[allowframebreaks]{Terms/Theory to JSON Mapping}
    \input{tab-serialization-mapping.tex}
\end{frame}

\begin{frame}[allowframebreaks]{Complete Usage Example}
    \ktSnippet{./snippets/SerializeDeserialize.kt}
\end{frame}

\section{Using \twopkt}

\begin{frame}{Intended Usages of \twopkt{}}
    \begin{block}{Usage as a JVM or JS \textbf{library}}
        \centering
        For \alert{developers} willing to re-use one or more functionalities
    \end{block}

    \vfill

    \begin{block}{Usage as a JVM or Web \textbf{application}}
        \centering
        For \alert{users} willing to use logic solvers interactively, \emph{à la Prolog}
    \end{block}

\end{frame}

\subsection{As a library, for developers}

\begin{frame}{Using \twopkt{} as a library -- Overview}

    \begin{itemize}
        \item \twopkt{} modules are compiled, packed, and deployed on both:
        %
        \begin{description}
            \item[Maven Central Repository] | Multiplatform + JVM packages only
            \item[GitHub Packages] | Multiplatform + JVM packages only
            \item[GitHub Releases] |JVM executables only + Dokka documentation
            \item[NPM] | JS packages only
        \end{description}

        \vfill

        \item Developers willing to use \twopkt{} facilities can
        %
        \begin{itemize}
            \item declare a Maven dependency (in JVM or MPP projects)
            \item declare a NPM dependency (in JS projects)
        \end{itemize}

        \vfill

        \item JS and JVM artefacts are versioned using \alert{\kt{SemVer}} and versions are kept aligned

        \vfill

        \item Documentation is produced for the Kotlin API alone
        %
        \begin{itemize}
            \item the Java or JS API are very close to the Kotlin one
            \item yet, knowing how Kotlin code is compiled is very useful
        \end{itemize}

    \end{itemize}

\end{frame}

\subsubsection{For JVM Developers}

\begin{frame}{Using \twopkt{} as a JVM library -- Overview}
    \begin{itemize}
        \item \twopkt{} modules are compiled into ordinary JVM bytecode

        \vfill

        \item They can be exploited as dependencies in most JVM-targetting languages
        %
        \begin{itemize}
            \item[eg] Java, Scala, Groovy, etc.
        \end{itemize}

        \vfill

        \item They can be imported using the Maven naming convention:
        %
        \begin{description}\small
            \item[\kt{groupId}:] \kt{it.unibo.tuprolog}
            \item[\kt{artifactId}:] \kt{\textit{MODULE\_NAME}-jvm}
            \item[\kt{version}:] a \kt{SemVer}-compliant string
        \end{description}
        %
        which are kept coherent on all Maven Repositories\footnote{\url{https://search.maven.org/search?q=g:it.unibo.tuprolog}}
        %
        \begin{itemize}
            \item provided that some dependency management system is in place
            %
            \begin{itemize}
                \item[eg] Gradle, Maven, etc.
            \end{itemize}
        \end{itemize}
    \end{itemize}
\end{frame}

\begin{frame}[allowframebreaks]{Kotlin--Java interoperability}
    \begin{alertblock}{Required readings}
        \begin{itemize}
            \item \url{https://kotlinlang.org/docs/java-to-kotlin-interop.html}
            \item \url{https://kotlinlang.org/docs/java-interop.html}
        \end{itemize}
    \end{alertblock}

    \begin{block}{Kotlin to Java in a nutshell}
        \begin{itemize}\small
            \item \kt{Unit} $\rightarrow$ \kt{void}
            \begin{itemize}
                \item the remainder of the type system is almost identical
            \end{itemize}
            \item \kt{varargs} $\rightarrow$ \kt{\ldots} (Java's varargs)
            \item public instance properties $\rightarrow$ getters (+ setters, if \kt{var})
            \item private/protected instance properties $\rightarrow$ fields
            \item objects $\rightarrow$ singleton classes with \kt{INSTANCE} constant
            \item optional parameters $\rightarrow$ method overloads
            %
            \begin{itemize}
                \item if \kt{@JvmOverloads} are provided
            \end{itemize}
            \item companion objects $\rightarrow$ \kt{Companion} constants
            \item companion objects members $\rightarrow$ accessible via \kt{Companion} constants
            %
            \begin{itemize}
                \item unless \kt{@JvmStatic} annotations are provided
            \end{itemize}
        \end{itemize}
    \end{block}

    \begin{exampleblock}{\twopkt{} Conventions}
        \begin{itemize}
            \item \kt{@JvmStatic} annotation on all public members of companion objects
            \item overload provided where possible in presence of optional parameters
        \end{itemize}
    \end{exampleblock}
\end{frame}

\subsubsection{For JavaScript Developers}

\begin{frame}{Using \twopkt{} as a JS library -- Overview}
    \begin{itemize}
        \item \twopkt{} modules are transpiled into ordinary JS code
        %
        \begin{itemize}
            \item targetting \alert{NodeJS}
            %
            \begin{itemize}
                \item transpiled NodeJS code can then be packed via \alert{WebPack}
            \end{itemize}
        \end{itemize}

        \vfill

        \item They can be exploited as dependencies in most JS-targetting languages
        %
        \begin{itemize}
            \item there including TypeScript, etc
        \end{itemize}

        \vfill

        \item They can be imported as NPM dependencies\footnote{\url{https://www.npmjs.com/org/tuprolog}}
        %
        \begin{description}\small
            \item[\kt{organization}:] \kt{@tuprolog}
            \item[\kt{name}:] \kt{2p-\textit{MODULE\_NAME}}
            \item[\kt{version}:] a \kt{SemVer}-compliant string
        \end{description}
    \end{itemize}
\end{frame}

\begin{frame}[allowframebreaks]{Kotlin--JavaScript interoperability}
    \begin{alertblock}{Required readings}
        \begin{itemize}
            \item \url{https://kotlinlang.org/docs/js-to-kotlin-interop.html}
            \item \url{https://kotlinlang.org/docs/js-interop.html}
        \end{itemize}
    \end{alertblock}

    \begin{block}{Kotlin to JavaScript in a nutshell}
        \begin{itemize}\small
            \item no overloading $\rightarrow$ members name are mangled\footnotemark{} by default
            %
            \begin{itemize}
                \item unless \kt{@JsName} annotation is used
            \end{itemize}
            \item type-system \& Kotlin's common library are re-implemented in JS
            \item primitive types are cumbersome
            %
            \begin{itemize}
                \item integer \& float types are collapsed
                \item longs are re-implemented
                \item Kotlin's array $\rightarrow$ JS arrays
                \item Kotlin's function $\rightarrow$ JS functions (there including lambdas)
            \end{itemize}
            \item packages, interfaces, and classes are \alert{emulated} via JS objects
            %
            \begin{itemize}
                \item but they correctly reflect the Kotlin codebase
            \end{itemize}
            \item companion objects $\rightarrow$ \kt{Companion} constants
            \item \kt{varargs} $\rightarrow$ JS arrays
        \end{itemize}
    \end{block}

    \footnotetext{\url{https://en.wikipedia.org/wiki/Name_mangling}}

    \begin{exampleblock}{\twopkt{} Conventions}
        \begin{itemize}
            \item \kt{@JsName} annotation on all public methods/properties
            %
            \begin{itemize}
                \item[$\rightarrow$] the JavaScript API is slightly different
            \end{itemize}
        \end{itemize}
    \end{exampleblock}
\end{frame}

\subsection{As an application, for end users}

\begin{frame}{Using \twopkt{} as an application -- Overview}
    \begin{block}{\textbf{Graphical} User Interface (GUI)}
        \begin{description}
            \item[\module{ide}] JavaFX-based, JVM-specific GUI for Prolog
            %
            \begin{itemize}
                \item pluggable \kt{Solver}s
            \end{itemize}
            \item[Playground] Web-based, JS-specific GUI for Prolog
        \end{description}
    \end{block}

    \begin{block}{\textbf{Command-Line} Interface (CLI)}
        \begin{description}
            \item[\module{cli}] Kotlin-based, multi-platform CLI for Prolog
            \item[Playground] Web-based, JS-specific GUI
        \end{description}
    \end{block}
\end{frame}

\subsubsection{Graphical User Interfaces}

\begin{frame}[allowframebreaks]{The \module{ide}}
    \begin{block}{How to obtain \& run the \module{ide}}
        \begin{enumerate}
            \item From \url{https://github.com/tuProlog/2p-kt/releases/latest}
            %
            \begin{itemize}
                \item download the \alert{\kt{2p-ide-X.Y.Z-redist.jar}} file
            \end{itemize}

            \item Start the \kt{.jar} by either
            %
            \begin{itemize}
                \item double click on the file (depends on your system configuration)
                \item run \kt{java -jar /path/to/2p-ide-X.Y.Z-redist.jar} on your shell
            \end{itemize}

            \item[!] Requires Java 11+ to be properly installed and configured
            %
            \begin{itemize}
                \item should work on Win, Linux, and MacOS
            \end{itemize}
        \end{enumerate}
    \end{block}

    \framebreak

    How to use the IDE:
    %
    \begin{center}
        \includegraphics[width=\linewidth]{img/ide-tutorial.pdf}
    \end{center}
\end{frame}

\begin{frame}[allowframebreaks]{The Playground}
    \begin{block}{How to obtain \& run the Playground}
        \begin{enumerate}
            \item Browse to \url{https://pika-lab.gitlab.io/tuprolog/2p-kt-web/}
            %
            \begin{itemize}
                \item that's it
            \end{itemize}

            \item[!] \textbf{The Playground is currently unstable}
            %
            \begin{itemize}
                \item it is just a proof of concept
            \end{itemize}
        \end{enumerate}
    \end{block}

    \begin{alertblock}{Potential}
        Even if it is currently unstable, our Playground:
        %
        \begin{itemize}
            \item aims at demonstrating the feasibility of using \twopkt{} \alert{in-browser}
            \item aims to become a valuable alternative to \href{https://swish.swi-prolog.org}{SWISH Prolog}
            %
            \begin{itemize}
                \item where logic computation occurs on the \alert{browser-side}
                %
                \begin{itemize}
                    \item no sandbox required
                    \item no Internet connection required (after page load)
                \end{itemize}
            \end{itemize}
        \end{itemize}
    \end{alertblock}

    \framebreak

    Preview:
    %
    \begin{center}
        \includegraphics[width=.9\linewidth]{img/playground.png}
    \end{center}
\end{frame}


\subsubsection{Command Line Interfaces}

\begin{frame}[allowframebreaks]{Usage of the CLI}
    \begin{block}{How to obtain \& run the \module{repl}}
        \begin{enumerate}
            \item From \url{https://github.com/tuProlog/2p-kt/releases/latest}
            %
            \begin{itemize}
                \item download the \alert{\kt{2p-repl-X.Y.Z-redist.jar}} file
            \end{itemize}

            \item Start the \kt{.jar} by either
            %
            \begin{itemize}
                \item double click on the file (depends on your system configuration)
                \item run \kt{java -jar /path/to/2p-repl-X.Y.Z-redist.jar} on your shell
            \end{itemize}

            \item[!] Requires Java 11+ to be properly installed and configured
            %
            \begin{itemize}
                \item should work on Win, Linux, and MacOS
            \end{itemize}
        \end{enumerate}
    \end{block}

    \framebreak

    Run \kt{java -jar 2p-repl-X.Y.Z-redist.jar \alert{--help}} to get:
    %
    \txtSnippet[\tiny]{snippets/repl-doc.txt}

    \framebreak

    Run \kt{java -jar 2p-repl-X.Y.Z-redist.jar \alert{solve} --help} to get:
    %
    \txtSnippet[\tiny]{snippets/repl-solve-doc.txt}

    \framebreak

    Usage example:
    %
    \begin{center}
        \includegraphics[width=.7\linewidth]{img/repl.png}
    \end{center}

\end{frame}

\section*{}
\frame{\titlepage}

\section*{\bibname}

\setbeamertemplate{page number in head/foot}{}

\begin{frame}[t,allowframebreaks,noframenumbering]\frametitle{\refname}
% \begin{frame}[c]\frametitle{\refname}
    \footnotesize
%    \scriptsize
    \bibliographystyle{plain}
    \bibliography{2p-kt-talk}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%