Add note (in plaintext) about the compilation

.chktexrc

@@ -497,7 +497,7 @@ WipeArg
     \Citet:*[][]{} \Citep:*[][]{} \Citealt:*{} \Citealp:*[]{} \Citeauthor:{}
     \citetext:{} \citeyear:*{} \citeyearpar:{}
     # Listings
-    \inlinelst:{}
+    \lstinline:{}
 }
 
 #####################################################################

combined/main.tex

@@ -21,8 +21,7 @@ We also present a compilation from nix to nix-light.
 \input{semantics/semantics}
 
 \subsection{From nix to nix-light}
-
-\todo{Write the semantic of the compilation}
+\input{semantics/compilation.tex}
 
 \section{typing}
 

common/header.tex

@@ -31,15 +31,12 @@
 
 % Fore code blocks
 \usepackage{listings}
-\lstset{%
-  escapeinside={//*}{*//}
-  }
 \lstdefinelanguage{NLight}{%
   morekeywords={%
-    let,in
+    let,in,if,then,else,Cons,Nil
   },%
-  morekeywords={[2]Int,true,false,Bool},   % types go here
-  otherkeywords={:,=}, % operators go here
+  morekeywords={[2]Int,true,false,Bool,T},   % types go here
+  otherkeywords={:,=[]}, % operators go here
   literate={% replace strings with symbols
     {->}{{$\to$}}{2}
     {lambda}{{$\lambda$}}{1}
@@ -51,9 +48,13 @@
   keywordstyle={[2]\itshape}, % style for types
   keepspaces,
   mathescape % optional
-}[keywords,comments,strings]%
-% Mostly because chktex can't expand the behaviour of \verb
-\newcommand{\inlinelst}[1]{\lstinline|#1|}
+}[keywords,comments,strings]
+\lstset{%
+  escapeinside={//*}{*//},
+  breaklines=true,
+  mathescape=true,
+  language=NLight
+}
 
 \usepackage{todo}
 

grammar/grammar.tex

@@ -21,33 +21,10 @@ extended} of a simple lambda calculus with lists (and type annotations).
 The grammar of nix-light is based of the grammar of nix and brings several
 modifications:
 \begin{itemize}
-  \item The main difference concerns records, whose representation is simplified as
-    much as possible:
-
-    \begin{itemize}
-      \item Litteral records are always atomic (\emph{ie} only have one field). An
-        \emph{orthogonal merge} operator ($\orthplus$) allows building complex
-        records~\footnote{We still often write \{ $s_1$ = $y_1$; $\cdots{}$;
-        $s_n$ = $y_n$ \} as a shorthand for \{ $s_1$ = $y_1$; \} $\orthplus
-        \cdots{} \orthplus$ \{ $s_n$ = $y_n$; \}},
-
-      \item The syntax in nix for a recursive definition of records (\texttt{\{ x.y
-        = 1; x.z = 2; \}}) doesn't exist anymore,
-
-      \item The labels can only be nix expressions (so litteral labels must be
-        written as constant strings).
-    \end{itemize}
-
-  \item Another huge change is the removal of the \emph{if} construct which is
+  \item A first huge change is the removal of the \emph{if} construct which is
     replaced by a more general \emph{typecase} which is easier to reason on.
 
-  \item Let bindings are not recursive by default anymore; a special \emph{let
-    rec} construct is introduced equivalent to the recursive \emph{let} of Nix.
-
-  \item Default values in patterns may only be constants. This makes typing of
-    patterns easier, without impact on the expressivity.
-
-  \item The last notable change is that the opaque list construct of nix is
+  \item Another notable change is that the opaque list construct of nix is
     replaced by the classical \texttt{nil} and \texttt{cons}.
     This avoids having over-complicated typing and evaluation rules for lists.
 
@@ -56,7 +33,7 @@ modifications:
 
 The grammar of nix-light is given in the
 figures~\pref{grammar::expressions},~\pref{grammar::values}
-and~\pref{grammar::types}.
+and~\pref{grammar::types} (the types are the same as nix types).
 
 \begin{figure}
   \input{grammar/expressions}

semantics/compilation.tex

@@ -0,0 +1,33 @@
+Both languages are rather similar, so the compilation is mostly
+straightforward: nix lambdas are compiled to nix-light lambdas; nix constants,
+and so on\ldots. The intersesting parts are:
+
+\begin{itemize}
+  \item[If-then-elses] Those are compiled, to typecases, as said in
+    Section~\ref{sec:nix-light-grammar}. However, there are several
+    possibilities for this.
+
+    The obvious one is to translate \lstinline{if $e$ then $e_1$ else $e_2$} into
+    \lstinline{($x$ := ($e$ : Bool) tin true) ? $e_1$ : $e_2$} (where $x$ do not appear
+    free in $e_1$ or $e_2$).
+    However, the interest of the typecase is that it gives us some information
+    on the type of $x$, that we can't use at all here. So this translation
+    isn't very interesting.
+    When possible, we will  to define smarter compilations for some forms of
+    if-then-else.
+
+    The most notable pattern that we want to recognize is
+    \lstinline{if isT $x$ then $e_1$ else $e_2$}
+    (where \lstinline{isT} is a predicate on types such as
+    \lstinline{isInt}, \lstinline{isBool}, \ldots).
+    Such an expression would be compiled to a typecase of the form
+    \lstinline{($x$ := $x$ tin T) ? $e_1$ : $e_2$}, which will later allow us to take
+    advantage of the knowledge of the type of $x$.
+
+  \item[Lists] Nix opaque lists are replaced in nix-light by the more
+    conventional algebraic datatype built using the \lstinline{Cons} and
+    \lstinline{Nil} constructors.
+    This translation is rather easy: the compilation simply considers that
+    \lstinline{[ $e_1$ $\cdots$ $e_n$ ]} is syntactic sugar for
+    \lstinline{Cons($e_1$, Cons($\cdots$, Cons($e_n$, Nil)))} %chktex 36
+\end{itemize}