Reorganize physical hierarchy

Thi makes it closer to the structure of the document and much easier to
work with

Makefile

@@ -5,13 +5,13 @@ VIEWER=evince
 
 .PHONY: all clean
 
-all: combined/main.pdf
+all: main.pdf
 
 view: combined/main.pdf
 	$(VIEWER) out/main.pdf
 
 check: FORCE
-	chktex -g0 -l .chktexrc combined/main.tex
+	chktex -g0 -l .chktexrc main.tex
 
 %.pdf: %.tex common/header.tex FORCE
 	latexmk -output-directory=out -pdf -xelatex -use-make $<

main.tex

@@ -19,39 +19,39 @@ We also present a compilation from nix to nix-light.
 
 \subsection{Grammar}
 \label{sec:nix-grammar}
-\input{grammar/nix}
+\input{nix/grammar}
 
 \subsection{Typing}
 \todo{Write}
 
 \subsection{Preprocessing}
 \todo{Reformulate to fit the position in the document}
-\input{semantics/preprocessing.tex}
+\input{nix/preprocessing}
 
 \section{Nix-light}
 
 \subsection{Grammar}
 \label{sec:nix-light-grammar}
-\input{grammar/nix-light}
+\input{nix-light/grammar}
 
 \subsection{Semantics}
-\input{semantics/semantics}
+\input{nix-light/semantics}
 
 \section{Nix-light typing}
 
 \subsection{The $\λ\&-calculus$}
-\input{typing/lambdaCalculus}
+\input{nix-light/typing/lambdaCalculus}
 
 \subsection{Bidirectional typing}
-\input{typing/bidir.tex}
+\input{nix-light/typing/bidir.tex}
 
 \subsection{Soundness}
-\input{typing/soundness}
+\input{nix-light/typing/soundness}
 
 \section{Compilation}
 
 \subsection{Compilation rules}
-\input{semantics/compilation.tex}
+\input{compilation/main}
 
 \subsection{Preservation of typing}
 

nix-light/grammar.tex

@@ -16,11 +16,11 @@ figures~\pref{grammar::expressions},~\pref{grammar::values}
 and~\pref{grammar::types} (the types are the same as nix types).
 
 \begin{figure}
-  \input{grammar/expressions}
+  \input{nix-light/grammar/expressions}
   \caption{\label{grammar::expressions}The nix-light grammar for expressions}
 \end{figure}
 
 \begin{figure}
-  \input{grammar/values}
+  \input{nix-light/grammar/values}
   \caption{\label{grammar::values}The nix-light grammar for values}
 \end{figure}

nix-light/typing/lambdaCalculus.tex

@@ -29,7 +29,7 @@ Maybe~\todo{Find out wether this is true} this enjoys principal typing.
 \todo{Define the projections $\pi_1$ and $\pi_2$}.
 
 \begin{figure}
-  \input{typing/inferenceRules/lambdaCalculus}
+  \input{nix-light/typing/inferenceRules/lambdaCalculus}
   \caption{Typing rules for the $\λ\&-calculus$\label{typing::lambda-calculus}\\
   \small{The ``$\delta$'' symbol means either ``$\Uparrow$'' either ``$\Downarrow$''
   (but always the same within a given inferrence rule)}}

nix/grammar.tex

@@ -24,6 +24,6 @@ extended} of a simple lambda calculus with lists (and type annotations).
 \end{figure}
 
 \begin{figure}
-  \input{grammar/types}
+  \input{nix/types}
   \caption{\label{grammar::types}The nix and nix-light grammar for types}
 \end{figure}