Update users manual

Remove dev manual, will add comments to source code instead

main/introduction.tex

@@ -98,7 +98,7 @@ \chapter{Introduction}\label{chapter:introduction}
 In Chapter \ref{chapter:transformer}, I show the algorithmic characterization of the correspondence.
 In Chapter \ref{chapter:case-studies}, I showcase the performance of the tool on a selection of case studies.
 In Chapter \ref{chapter:conclusions}, I discuss related work, point at future avenues for improvement and conclude. % TODO rewrite this sentence
-Appendices contain user's and developer's manual for the semantic transformer.
+Appendix \ref{chapter:user-manual} contains user's manual for the semantic transformer.
 
 I assume that the reader is familiar with \LC{} and its semantics (both normal (call-by-name) and applicative (call-by-value) order reduction).
 Familiarity with formal semantics of programming languages (both denotational and operational) is also assumed although not strictly required for understanding of the main subject of this thesis.

main/manual.tex

@@ -25,25 +25,63 @@ \subsection*{Tool usage}
   -h,--help                Show this help text
 \end{lstlisting}
 
+\begin{figure}
+  \lstinputlisting[numbers=left]{interpreters/src/lambda-value.rkt}
+  \caption{An example of a source file}
+  \label{fig:idl-example}
+\end{figure}
+
 \subsection*{Source File Format}
 The tool assumes that the source file with an interpreter is a \textit{Racket} program.
-The interpreter itself (line 6) has to be placed between two comments (lines 4 and 8):
-\begin{lstlisting}[numbers=left]
-#racket
-$\dots$
+An example source listing is shown in Figure \ref{fig:idl-example}.
+The preamble (everything up to the \lstinline!; begin interpreter! marker in line 4) is copied verbatim by the tool and should be used to specify \emph{Racket}'s dialect (line 1) and import syntax definitions (line 2).
+Afterwards an interpreter is specified (lines 4 -- 31) and it ends with another marker \lstinline!; end interpreter! in line 32.
+Everything following the marker is again copied to the output file.
+In the example this space is used to define some tests for the interpreter.
+The syntax of \IDL{} is given in Figure \ref{fig:idl-syntax}.
+
+\subsection*{Top-level definitions}
+The interpreter consists of a sequence of datatype (\textit{data-def}), record (\textit{struct-def}) and function (\textit{fun-def}) definitions.
+One of the functions must be named \lstinline!main! and will serve as an entry point of the interpreter.
+It is required for the \lstinline!main! function to have parameters annotated with types, e.g., \lstinline!(def main ([String foo]$\;$[Any e])$\;$body)!.
+Names (\textit{tp-name}) of datatypes and records must be unique distinct from base types (\textit{base-tp} and \lstinline!Any!).
+All definitions may be mutually recursive.
 
-; begin interpreter
+\subsection*{Terms}
+The term syntax is split into terms and statements where the latter appear as the bodies of function definitions (both top-level and anonymous) and branches.
+Statements are sequences of let-bindings terminated by a regular term (see lines 16--19 of Figure \ref{fig:idl-example}).
 
-;; interpreter goes here
+\subsection*{Execution}
+In order to run the interpreter a library with syntax definitions must be imported.
+Let us assume the following directory structure:
+\begin{lstlisting}
+interpreters/
+  src/
+    lambda-value.rkt
+  lib/
+    idl.rkt
+\end{lstlisting}
+Where \lstinline!idl.rkt! is the library of syntax definitions provided with this thesis and \lstinline!lambda-value.rkt! is the file we want to execute.
+Then it suffices to add \lstinline!(require "../lib/idl.rkt")! (line 2 of the example) at the top of the file.
+
+The run-time behavior of the program follows the call-by-value behavior of \emph{Racket}, e.g.:
+\begin{itemize}
+  \item \lstinline!let! evaluates the bound term to a value before binding.
+  The binding is visible only in following statements.
+  \item Application evaluates terms left-to-right and then applies the value in function position.
+  \item \lstinline!match! evaluates the term under scrutiny and tests patterns against the value in order of their definition continuing with the first match.
+\end{itemize}
+
+\subsection*{Annotations}
+\begin{itemize}
+  \item \lstinline!#:apply! specifies the name for \emph{apply} function generated for the defunctionalized function space whose member is the annotated function.
+  \item \lstinline!#:name! specifies the name for the record which will represent the annotated function after defunctionalization.
+  \item \lstinline!#:no-defun! skips defunctionalization of the annotated function (either all or none of the functions in a space must be annotated).
+  \item \lstinline!#:atomic! means that the annotated function (and calls to it) will be left in direct style during translation to CPS.
+\end{itemize}
 
-; end interpreter
 
-$\ldots$
-\end{lstlisting}
 
-The interpreter consists of a sequence of datatype, record and function definitions.
-One of the functions must be named \lstinline!main! and will serve as an entry point of the interpreter.
-The syntax of top-level definitions is given in Figure ???
 
 \begin{figure}
 \centering
@@ -72,21 +110,38 @@ \subsection*{Source File Format}
 & ::= \lstinline!Any! | $\mathit{base\mh tp}$ | $\mathit{tp\mh name}$\\
 
 $\mathit{fun\mh def}$
-& ::= \lstinline!(def $\mathit{var}$ $\mathit{annot}\ldots$ ($\mathit{arg}\ldots$) $\mathit{term}$)!\\
+& ::= \lstinline!(def $\mathit{var}$ $\mathit{annot}\ldots$ ($\mathit{arg}\ldots$) $\mathit{statements}$)!\\
 
 $\mathit{annot}$
 & ::= \lstinline!#:no-defun!
     | \lstinline!#:atomic!
-    | \lstinline!#:name $\mathit{tp\mh name}$!
-    | \lstinline!#:apply $\mathit{var}$!\\
+    | \lstinline!#:name !$\mathit{tp\mh name}$
+    | \lstinline!#:apply !$\mathit{var}$\\
 
 $\mathit{arg}$
 & ::= $\mathit{var}$ | \lstinline![$\mathit{tp}$ $\mathit{var}$]!\\
 
+$\mathit{const}$
+& ::= $\mathit{integer}$ | $\mathit{string}$ | \lstinline!#t! | \lstinline!#f!\\
+
+$\mathit{statements}$
+& ::= \lstinline!(let $\mathit{var}$ $\mathit{term}$)! $\mathit{statements}$
+    | $\mathit{term}$\\
+
 $\mathit{term}$
 & ::= $\mathit{var}$ 
-    | \lstinline!(fun $\mathit{annot}\ldots$ ($\mathit{arg}\ldots$) $\mathit{term}$)!
+    | \lstinline!(fun $\mathit{annot}\ldots$ ($\mathit{arg}\ldots$) $\mathit{statements}$)!
     | \lstinline!($\mathit{term}$ $\mathit{term}\ldots$)!\\
 &   | \lstinline!{$\mathit{tp\mh name}$ $\mathit{term}\ldots$}!
+    | \lstinline!(match $\mathit{term}$ $\mathit{branch}\ldots$)!
+    | \lstinline!(error $\mathit{string}$)!\\
+
+$\mathit{branch}$
+& ::= \lstinline!($\mathit{pattern}$ $\mathit{statements}$)!\\
+
+$\mathit{pattern}$
+& ::= $\mathit{var}$ | $\mathit{const}$ | \lstinline!_! | \lstinline![$\mathit{base\mh tp}$ $\mathit{var}$]! | \lstinline!{$\mathit{tp\mh name}$ $\mathit{pattern}\ldots$}!\\
 \end{tabular}
+\caption{Syntax of \IDL{}}
+\label{fig:idl-syntax}
 \end{figure}

thesis.tex

@@ -12,12 +12,12 @@
 \usepackage[scale=0.8]{FiraMono}
 
 \lstdefinelanguage{idl}{%
-  alsoletter={-,?,\#,:},
+  alsoletter={-?\#:},
   otherkeywords={(,),\{,\},[,]},
   morekeywords={def,fun,def-data,def-struct,match,let,error},
   morekeywords=[2]{String,Integer,Any,Boolean},
   morekeywords=[3]{(,),\{,\},[,]},
-  morekeywords=[4]{\#:apply, \#:atomic, \#:no-defun}
+  morekeywords=[4]{\#:bar,\#:apply,\#:atomic,\#:no-defun,\#:name,\#t, \#f, \#:foo},
   sensitive=false,
   morestring=[b]",
   morecomment=[l]{;;}
@@ -101,7 +101,6 @@
 
   \appendix
   \input{main/manual.tex}
-  \input{main/dev-manual.tex}
 
   \printbibliography[heading=bibintoc]
 \end{document}