\documentclass{article}

\usepackage{hyperref}
\usepackage{fodot}

\newcommand{\pkg}[1]{\texttt{#1}}

\begin{document}

\title{The package \pkg{fodot}\thanks{This document corresponds to the
version 0.0.1 of \pkg{fodot}, at the date of 2025/08/29.}} 
\author{Christian Fleiner \\ \texttt{christian.fleiner@kuleuven.be}}

\maketitle

\begin{abstract}
The package \pkg{fodot} provides helpful commands to work with the \fodot language in \LaTeX including syntax highlighting in listings.
\end{abstract}


\section{Contributing}
Contributions are always welcome. The project is hosted at \url{https://gitlab.com/EAVISE/CFL/fodot-latex}.

\section{Description}
In the following, the capabilities of the package are described and illustrated. The \fodot language itself is not introduced. \fodot\footnote{\url{https://docs.idp-z3.be/en/stable/introduction.html}} is the technical implementation of \fodott\footnote{\url{https://fo-dot.readthedocs.io/en/latest/FO-dot.html}} used in the reasoning engine IDP-Z3\footnote{\url{https://idp-z3.be/}}. Please refer to the official documentation to learn more.

\subsection{Commands}
The following commands are currently supported:
\begin{enumerate}
    \item Type \verb|\fodot| for: \fodot. \textit{(partial implementation of \fodott)}
    \item Type \verb|\fodott| for: \fodott. \textit{(formal knowledge representation language)}
\end{enumerate}


\subsection{FODOT Syntax Highlighting}

There are two styles to highlight \fodot code in listings.
\fodot code must be always copied in ASCII format.  
\texttt{fodot} replaces operators with their UTF-8 symbol.
\texttt{fodotASCII} keeps the ASCII representations.

There are a few bugs that require workarounds:
\begin{itemize}
    \item \verb|*| is somehow not recognized. Replace \verb|*| with \texttt{TIMES} in listing.
    \item \verb|=<| is highlighted but not replaced (while \verb|<=| would work). Instead, replace \verb|=<| with \verb|=&lt;| in listing (not relevant for \texttt{fodotASCII})
\end{itemize}

The syntax highlighter does not support patterns to highlight URLs. 

See the following templates for each style:
\begin{quote}
    \verb|\begin{lstlisting}[style=fodot]| \\
    \ldots \\
    \verb|\end{lstlisting}|
\end{quote}

\begin{quote}
    \verb|\begin{lstlisting}[style=fodotASCII]| \\
    \ldots \\
    \verb|\end{lstlisting}|
\end{quote}

\subsubsection{Examples: Fodot Style}
\textbf{Code snippet A}
\begin{lstlisting}[style=fodot]
vocabulary { 
    // this is a single-line comment
    type Method := {Nail, Glue, Screw}
    type Wall := {Brick, Wood, Tile}
    [this is an annotation]
    type Difficulty := {1..3}
    
    /*
    this is a block comment
    */
    wall  : () -> Wall
    method: () -> Method
    hole : () -> Bool
    weight: () -> Int
    difficulty : () -> Difficulty
}
theory {
    weight() > 0.
    method() = Nail  => weight() =&lt; 25.
    method() = Screw => weight() =&lt; 40.
    method() = Glue  => weight() =&lt; 15.

    hole() <=> method() = Nail | method() = Screw.
    wall() = Tile => ~hole().

    { difficulty() = 1 <- method() = Glue.
    difficulty() = 2 <- method() = Nail.
    difficulty() = 3 <- method() = Screw.}
}
display {
    view() = expanded.
}

\end{lstlisting}
\newpage
\textbf{Code Snippet B}
\begin{lstlisting}[style=fodot]
@prefix we: <http://www.example.org/whatever#>.
 vocabulary V {
     @prefix se: <http://www.example.org/somethingelse#_url>.
     type T
     type T := {c1, c2, c3}                  
     type T := constructed from {c1, c2(T1, f:T2)}
     type T := {1,2,3} <: Int                   
     type T := {1..3} <: Int                     
     type we::T
     type <http://www.example.org/foo#Type>

     p : () -> Bool                            
     p1, p2 : T1 TIMES T2 -> Bool                      
     f: total T -> T                          
     f: T * T -> T  (domain: p, codomain: q)     
     f: partial TTIMEST -> T                      
     f1, f2: Concept[T1->T2] -> T              

     [this is the intended meaning of p]
     p : () -> Bool

     var x in T                                
     import W
 }

 theory T:V {
     (~p1()&p2() | p3() => p4() <=> p5()) <= p6(). 
     p(f1(f2())).
     f1() < f2() =&lt; f3() = f4() >= f5() > f6().  
     f() ~= c.                                 
     !x,y in T: p(x,y).                         
     !x in p, (y,z) in q: q(x,x) | p(y) | p(z).  
     ?x in Concept[()->Bool]: $(x)().              
     ?x: p(x).  # if var x declared in voc    
     ?>1 x in T: p(x).                         

     f() in {1,2,3}.
     f() = #{xinT: p(x)}.                       
     f() = min{  f(x) | x in T: p(x) }.
     f() = sum{{ f(x) | x in T: p(x) }}.
     if p1() then p2() else p3().
     f1() = if p() then f2() else f3().

     p := {1,2,3}.                             
     p(#2020-01-01) is enumerated.
     p(#TODAY) is not enumerated.

     { p(1). }
     { (co-induction)
       !xinT: p1(x) <- p2(x).                    
       f(1)=1.
       !x: f(x)=1 <- p(x).                     
       !x: f(x):=1 <- p(x).                      
     }

     [this is the intended meaning of the rule]
     p().
 }

 structure S:V {
     p := false.                             
     p := {1,2,3}.                            
     p := {0..9, 100}.                       
     p := {#2021-01-01}.                     
     p := {(1,2), (3,4)}.                      
     p := {                                    
     1 2                                      
     3 4                                      
     }.                                        

     f := 1.                                  
     f := {->1} .                           
     f := {1->1, 2->2}.                         
     f := {(1,2)->3} else 2.                   
     f :> {(1,2)->3}.                         
 }

 display {
     goal_symbol := {`p1, `p2}.                
     hide(`p).
     expand := {`p}.                         
     view() = expanded.
     optionalPropagation().
 }

 procedure main() {
     pretty_print(model_check    (T,S))
     pretty_print(model_expand   (T,S))
     pretty_print(model_propagate(T,S))
     pretty_print(minimize(T,S, term="cost()"))
 }
\end{lstlisting}
\newpage
\subsubsection{Examples: FodotASCII Style}
\textbf{Code Snippet A}
\begin{lstlisting}[style=fodotASCII]
vocabulary { 
    // this is a single-line comment
    type Method := {Nail, Glue, Screw}
    type Wall := {Brick, Wood, Tile}
    [this is an annotation]
    type Difficulty := {1..3}
    
    /*
    this is a block comment
    */
    wall  : () -> Wall
    method: () -> Method
    hole : () -> Bool
    weight: () -> Int
    difficulty : () -> Difficulty
}
theory {
    weight() > 0.
    method() = Nail  => weight() =&lt; 25.
    method() = Screw => weight() =< 40.
    method() = Glue  => weight() =< 15.

    hole() <=> method() = Nail | method() = Screw.
    wall() = Tile => ~hole().

    { difficulty() = 1 <- method() = Glue.
    difficulty() = 2 <- method() = Nail.
    difficulty() = 3 <- method() = Screw.}
}
display {
    view() = expanded.
}

\end{lstlisting}
\newpage
\textbf{Code Snippet B}
\begin{lstlisting}[style=fodotASCII]

@prefix we: <http://www.example.org/whatever#>.
 vocabulary V {
     @prefix se: <http://www.example.org/somethingelse#_url>.
     type T
     type T := {c1, c2, c3}                  
     type T := constructed from {c1, c2(T1, f:T2)}
     type T := {1,2,3} <: Int                   
     type T := {1..3} <: Int                     
     type we::T
     type <http://www.example.org/foo#Type>

     p : () -> Bool                            
     p1, p2 : T1 TIMES T2 -> Bool                      
     f: total T -> T                          
     f: T * T -> T  (domain: p, codomain: q)     
     f: partial TTIMEST -> T                      
     f1, f2: Concept[T1->T2] -> T              

     [this is the intended meaning of p]
     p : () -> Bool

     var x in T                                
     import W
 }

 theory T:V {
     (~p1()&p2() | p3() => p4() <=> p5()) <= p6(). 
     p(f1(f2())).
     f1() < f2() =< f3() = f4() >= f5() > f6().  
     f() ~= c.                                 
     !x,y in T: p(x,y).                         
     !x in p, (y,z) in q: q(x,x) | p(y) | p(z).  
     ?x in Concept[()->Bool]: $(x)().              
     ?x: p(x).  # if var x declared in voc    
     ?>1 x in T: p(x).                         

     f() in {1,2,3}.
     f() = #{xinT: p(x)}.                       
     f() = min{  f(x) | x in T: p(x) }.
     f() = sum{{ f(x) | x in T: p(x) }}.
     if p1() then p2() else p3().
     f1() = if p() then f2() else f3().

     p := {1,2,3}.                             
     p(#2020-01-01) is enumerated.
     p(#TODAY) is not enumerated.

     { p(1). }
     { (co-induction)
       !xinT: p1(x) <- p2(x).                    
       f(1)=1.
       !x: f(x)=1 <- p(x).                     
       !x: f(x):=1 <- p(x).                      
     }

     [this is the intended meaning of the rule]
     p().
 }

 structure S:V {
     p := false.                             
     p := {1,2,3}.                            
     p := {0..9, 100}.                       
     p := {#2021-01-01}.                     
     p := {(1,2), (3,4)}.                      
     p := {                                    
     1 2                                      
     3 4                                      
     }.                                        

     f := 1.                                  
     f := {->1} .                           
     f := {1->1, 2->2}.                         
     f := {(1,2)->3} else 2.                   
     f :> {(1,2)->3}.                         
 }

 display {
     goal_symbol := {`p1, `p2}.                
     hide(`p).
     expand := {`p}.                         
     view() = expanded.
     optionalPropagation().
 }

 procedure main() {
     pretty_print(model_check    (T,S))
     pretty_print(model_expand   (T,S))
     pretty_print(model_propagate(T,S))
     pretty_print(minimize(T,S, term="cost()"))
 }
\end{lstlisting}

\end{document}