\documentclass[pagesize=a5,fontsize=10pt,DIV=calc,bibliography=totoc, index=totoc]{scrbook}

\iffalse
TODOs:
 * Session graph? LoC-Tabelle?

Guides:
 * Sentence case in section titles
 * I have proved foo, but foo is a proven fact.
 * Capitalization after : if it is a sentence
 * runtime = system, run time = time
 * fixed point, but fixed-point induction

Things to capitalize:
 * Haskell
 * Core
 * Call Arity
 * Isabelle
 * Church

Things not to capitalize
 * Nominal logic
 * Trace tree
 * Co-call graph
 * List fusion

Symbol index keys:
 * A  arrows
 * Cn n-ary constructors
 * O0 constants
 * On n-ary operations
 * Rn n-ary relations
 * S  semantics functions

Final Layout checks:
 * Section Headers not before Section starts (e.g. 2.3)
 * Missing references (search for ??)
 * Missing diamonds in definitions (\index!)
 * Get rid of Draft!, check for TODOs

BE hints:
 * formalize
 * analise

XKCD quotes:
Functional programming combines the flexibility and power of abstract mathematics with the intuitive clarity of abstract mathematics. #1270
Honestly, we hacked most of it together with Perl. #224
The problem with Haskell is that it's a language built on lazy evaluation and nobody's actually called for it. #1312
I started with $P\wedge \neg P$ and derived your Mom’s phone number. #704
Excuse me, but _real_ programmer use butterflies. #378

Oh, hey, I didn’t see you guys all the way over there. #435
The first rule of tautology club is the first rule of tautology club. #703
White to continue insisting this is a chessboard. #1287
Do you know how much scripture we’ll have to revise. #459
Come explore the future with me! #209
Hey, in the future, if you’re on any tech support call, you can say the code word “Shibboleet” at any point and you’ll be automatically transferred to someone who konws a minimum of two programming languages. #806
Honk iff you love formal logic. #1033

\fi

\newif\ifdraft
\draftfalse

\usepackage[ngerman,english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}

\usepackage{lettrine}

\DeclareUnicodeCharacter{3BB}{\textlambda}
\DeclareUnicodeCharacter{2192}{\ensuremath{\rightarrow}}
\DeclareUnicodeCharacter{B2}{\ensuremath{^2}}

\newcommand{\thesimons}{%
  \footnote{famously known as “The Simons”\label{simons}}%
  \global\def\thesimons{\footref{simons}}%
}
\newif\ifbiblatex
\biblatextrue

\ifbiblatex
\usepackage[backend=biber,style=alphabetic,sorting=nyt,maxalphanames=5,minalphanames=3,maxbibnames=10]{biblatex}
\DefineBibliographyStrings{english}{phdthesis = {Ph.D.\@ thesis}}
\DeclareFieldFormat[article,inbook,incollection,inproceedings,patent,thesis,unpublished]{title}{\mkbibemph{#1}}
\DeclareFieldFormat{journaltitle}{#1}
\DeclareFieldFormat{issuetitle}{#1}
\DeclareFieldFormat{maintitle}{#1}
\DeclareFieldFormat{booktitle}{#1}

\DefineBibliographyExtras{english}{\renewcommand{\finalandcomma}{}}
\newbibmacro*{in:}{}

% http://tex.stackexchange.com/q/218706/15107
\setcounter{biburlnumpenalty}{400}  % allow breaks at numbers
\setcounter{biburlucpenalty}{400}   % allow breaks at uppercase letters
\setcounter{biburllcpenalty}{400}   % allow breaks at lowercase letters

\bibliography{bib}
\else
\usepackage[numbers,square]{natbib}
\bibliographystyle{amsalpha}
\fi

\usepackage{paralist}


\usepackage{xcolor}
\usepackage{hyperref}
\hypersetup{%
  colorlinks=false,% hyperlinks will be black
  linkbordercolor=blue,% hyperlink borders will be red
  hyperfootnotes=false,
  pdfborderstyle={/S/U/W 0.5}% border style will be underline of width 1pt
}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{mathtools}
\usepackage[safe]{tipa} % for \textlambda
\usepackage{mathpartir}
\usepackage{stmaryrd}
\usepackage{conteq}
\usepackage{xparse}
\usepackage[amsmath,thmmarks]{ntheorem}
\usepackage{afterpage}
\usepackage{adjustbox}
\usepackage{needspace}

\usepackage{array}
\usepackage{bigstrut}
\usepackage{multirow}
\usepackage{polytable}
\usepackage{booktabs}
\usepackage{pdflscape}
\usepackage{rotating}

\usepackage{caption}
\captionsetup{labelsep = colon}
\KOMAoptions{numbers=noenddot}

\usepackage{tikz}
\usetikzlibrary{decorations.pathreplacing}

\input{isainput}

% KOMA vs. lhs2tex und isabelle
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}


% Figures unabhängig vom Kapitel zählen
\usepackage{chngcntr}
\counterwithout{figure}{chapter}
\counterwithout{table}{chapter}
\counterwithout{footnote}{chapter}



% Index
%\usepackage{makeidx}
\usepackage{index}
\usepackage{ragged2e}
\usepackage{scrindex}
%\usepackage[hangindent=0pt,columns=2,justific=RaggedRight]{idxlayout}
\usepackage[itemlayout=relhang,subindent=1em,subsubindent=2em,hangindent=1em]{idxlayout}
\makeindex
\newcommand{\idxdummy}{\text{\textcolor{lightgray}{\rule{1ex}{1ex}}}}
\newcommand{\thisidexpl}{}
\newcommand{\idxexpl}[1]{%
  \renewcommand{\thisidexpl}{#1}%
}
\newcommand{\outputidxexpl}{%
  \ifthenelse{\equal{\thisidexpl}{}}{}{%
    \nopagebreak% does not work reliable
    \\%
    %\needspace{\baselineskip}%
    {\raggedright%
    \thisidexpl\par%
    }%
  }%
  \renewcommand{\thisidexpl}{}%
}

\newif\iflineno
\linenofalse
\ifdraft
%\overfullrule=1mm
%\proofmodetrue
\indexproofstyle{\footnotesize\it}

\iflineno
\usepackage[switch,pagewise]{lineno}
\linenumbers

\newcommand*\patchAmsMathEnvironmentForLineno[1]{%
  \expandafter\let\csname old#1\expandafter\endcsname\csname #1\endcsname
  \expandafter\let\csname oldend#1\expandafter\endcsname\csname end#1\endcsname
  \renewenvironment{#1}%
     {\linenomath\csname old#1\endcsname}%
     {\csname oldend#1\endcsname\endlinenomath}}% 
\newcommand*\patchBothAmsMathEnvironmentsForLineno[1]{%
  \patchAmsMathEnvironmentForLineno{#1}%
  \patchAmsMathEnvironmentForLineno{#1*}}%
\AtBeginDocument{%
\patchBothAmsMathEnvironmentsForLineno{equation}%
\patchBothAmsMathEnvironmentsForLineno{align}%
\patchBothAmsMathEnvironmentsForLineno{flalign}%
\patchBothAmsMathEnvironmentsForLineno{alignat}%
\patchBothAmsMathEnvironmentsForLineno{gather}%
\patchBothAmsMathEnvironmentsForLineno{multline}%
}
\fi % \iflineno
\fi % \ifdraft

\mathtoolsset{
  above-shortintertext-sep=-0em,
  below-shortintertext-sep=-0em,
}

\ConteqDefineLayout
	{onecolumnr}
	{\begin{align*}}
	{ &\mathrel{\phantom{=}} #1 \\ }
	{ & #1 }
	{ & #1 \tag*{#2} }
	{ \\ }
	{\end{align*}}


\ifdraft
\usepackage{todonotes}
%\usepackage{showframe}
\else
\usepackage[disable]{todonotes}
\fi

\usepackage{microtype}


\KOMAoptions{chapterprefix=true}
\renewcommand*{\chapterformat}{%
\LARGE\MakeUppercase{\chapapp} \thechapter%
}
\addtokomafont{chapter}{\Huge}
\newcommand{\prechapterskip}{3cm}
\renewcommand*{\chapterheadstartvskip}{\vspace{\prechapterskip}\vspace{0.25cm}}
\renewcommand*{\chapterheadmidvskip}{}
\renewcommand{\chapterlineswithprefixformat}[3]{
     \centering
     \ifthenelse{\equal{#2}{}}{
       % manually adjusted :-(
       \vspace*{-2.1pt}%
     }{%
       \hrule%
       \vspace*{1pt}%
       \hrule%
       \vspace*{7pt}%
     }%
     {%
     \LARGE
     \ifthenelse{\equal{#2}{}}%
         {\phantom{\MakeUppercase{\chapapp}}}%
	 {\MakeUppercase{\chapapp} \thechapter}%
     }%
     \vspace*{7pt}%
     \hrule%
     \vspace*{9pt}%
     #3%
}

\newcommand{\xkcd}[2]{
{
\small
\strut\hfill\parbox[t][\prechapterskip][t]{\linewidth}{
\raggedright
#1
\par
\vspace{4pt}
\hrule
\vspace{4pt}
\raggedleft
\textit{Randall Munroe, \href{http://xkcd.com/#2}{xkcd \##2}}
\par
}
}
}
\newcommand{\xkcdquote}[2]{
\setchapterpreamble[or][.45\textwidth]{
\xkcd{#1}{#2}
}
}

%\usepackage{titlesec}
%\titleformat{\chapter}[display]
%        {\sectfont\Large\filcenter}
%        {\titlerule%[1pt]%
%         \vspace{1pt}%
%         \titlerule%
%         %\vspace{.4pc}%
%         \LARGE\MakeUppercase{\chaptertitlename} \thechapter}
%        {1pc}
%        {\titlerule
%         \vspace{1pc}%
%         \Huge}


% get rid of fourier fontenc warnings
% from http://newsgroups.derkeiler.com/Archive/Comp/comp.text.tex/2006-01/msg00679.html
\makeatletter
\let\my@@font@warning\@font@warning
\let\@font@warning\@font@info
\makeatother
%
\usepackage{mathpazo}
%
\makeatletter
\let\@font@warning\my@@font@warning
\makeatother

% Palatino: 5% mehr Zeilendurchschuss (laut KOMA-skript)
\linespread{1.05}

% URL formatting
\urlstyle{sf}
\makeatletter
% Inspired by http://anti.teamidiot.de/nei/2009/09/latex_url_slash_spacingkerning/
% but slightly less kern and shorter underscore
\let\UrlSpecialsOld\UrlSpecials
\def\UrlSpecials{\UrlSpecialsOld\do\/{\Url@slash}\do\_{\Url@underscore}}%
\def\Url@slash{\@ifnextchar/{\kern-.11em\mathchar47\kern-.2em}%
   {\kern-.0em\mathchar47\kern-.08em\penalty\UrlBreakPenalty}}
\def\Url@underscore{\nfss@text{\leavevmode \kern.06em\vbox{\hrule\@width.3em}}}
\makeatother


% References

\usepackage[capitalise,nameinlink,nosort]{cleveref}
% captialize everything bug “page”
\crefname{page}{page}{pages}
% Historic
\newcommand{\myref}[2]{\cref{#2}}


% stuff from KSP Formatvorlage
%%%
% head, foot
\RequirePackage[%
  headsepline,      % Linie unter der Kopfzeile
  automark,         % automatische Aktualisierung der Kolumnentitel
  nouppercase,      % Grossbuchstaben verhindern
  %markuppercase    % Grossbuchstaben erzwingen
  %markusedcase     % vordefinierten Stil beibehalten
  komastyle,        % Stil von Koma Script
  %standardstyle,   % Stil der Standardklassen
]{scrpage2}
\pagestyle{scrheadings}
\ohead[\pagemark]{\pagemark}
\ihead[]{\headmark}
\chead[]{}
\ofoot[]{}
\ifoot[]{}
\cfoot[]{}
\renewcommand*{\chaptermarkformat}{}

\setkomafont{pageheadfoot}{\small\usekomafont{pagenumber}}

%Set part and chpater pagestyle to empty: without head
\renewcommand*{\titlepagestyle}{empty}
\renewcommand*{\partpagestyle}{empty}
\renewcommand*{\chapterpagestyle}{empty}
\renewcommand*{\indexpagestyle}{empty}

\KOMAoptions{paper=A5, pagesize, headlines=1.1, headsepline}
\typearea[8mm]{15} %8mm BCOR, DIV14
\KOMAoptions{DIV=last}
% end stuff from KSP Formatvorlage


%% LaTeX-Dissertationsheader nach KIT-Vorlage
%% Verwendung:
%% 1. Parameter: Diss-Titel
%% 2. Parameter: Diss-Untertitel (wenn nicht vorhanden, weglassen)
%% 3. Parameter: Vor- und Zuname
%% 4. Parameter: Geburtsort
%% 5. Parameter: Pr\"ufungstermin
%% 6. Parameter: Name erster Gutachter (voller Titel)
%% 7. Parameter: Name zweiter Gutachter (voller Titel)
% Von Andreas Lochbihler übernommen
\newcommand{\thesistitle}[7]%
{
  {%
    \begin{otherlanguage}{ngerman}
    \setlength{\parindent}{0pt}
    \setlength{\parskip}{3pt}
    \thispagestyle{empty}
    \begin{center}
      \sffamily
      \LARGE \textbf{#1}

      \Large \textbf{#2}
      \vspace*{25pt}

      \normalsize
      zur Erlangung des akademischen Grades eines
      \vspace{10pt}

      \Large
      Doktors der Naturwissenschaften

      \vspace{15pt}
      \normalsize
      der Fakultät für Informatik\\
      des Karlsruher Instituts für Technologie (KIT)

      \vspace{15pt}
      \Large \textbf{genehmigte} \\
      \LARGE \textbf{Dissertation}
      \vspace{10pt}

      \normalsize
      von
      
      \vspace{10pt}
      \Large \textbf{#3}
      \vspace{10pt}
        
      \normalsize
      aus #4
    \end{center}
    \vfill
    \begin{tabular}{l@{\qquad}l}
      Tag der mündlichen Prüfung: & 25. April 2016\\
      ~\\
      Erster Gutachter: & #6\\
      ~\\
      Zweiter Gutachter: & #7\\
      ~
    \end{tabular}

\hrule
\enlargethispage{1cm}
\begin{center}
{
Das vorliegende Dokument, erstellt am \today,\\ unterscheidet sich von der genehmigten
Version duch die auf\\\url{http://www.joachim-breitner.de/thesis/\#errata}\\
aufgeführten Korrekturen.

\nopagebreak
}
\end{center}

    \eject
    \pagebreak
    \end{otherlanguage}
  }
}


\allowdisplaybreaks[3]

\input{thmdefs}
\input{syntax}
\input{haskell}

\newcommand{\lydiaetal}{S{\'a}nchez-Gil {\em et~al.\@}}

\input{listings/preamble.tex}
\renewcommand{\hsindent}[1]{~~~~}
\setlength{\blanklineskip}{\baselineskip}
\usepackage{sansmath}

\hyphenation{Chak-ra-var-ty}


\begin{document}
\frontmatter

%\setcounter{page}{7}

\thesistitle
 {Lazy Evaluation:}
 {From natural semantics\\ to a machine-checked compiler transformation}
 {Joachim Breitner}
 {Herrenberg}
 {St. Nimmerleinstag}
 {Prof. Dr.-Ing. Gregor Snelting}
 {Prof. Tobias Nipkow, Ph.D.}

\clearpage
\strut
\vfill
\noindent
\includegraphics[scale=.6]{CC-By}\\
This document is licensed under the Creative Commons Attribution 3.0 DE License (CC BY 3.0 DE):\\
\url{http://creativecommons.org/licenses/by/3.0/de/}

\tableofcontents


\chapter*{Abstract}
\markboth{Abstract}{Abstract}
\input{abstract}

\selectlanguage{ngerman}
\chapter*{Zusammenfassung}
\markboth{Zusammenfassung}{Zusammenfassung}
\input{zusammenfassung}
\selectlanguage{english}

\chapter*{Acknowledgements}
\markboth{Acknowledgements}{Acknowledgements}
\input{acks}

\mainmatter


\xkcdquote{Functional programming combines the flexibility and power of abstract mathematics with the intuitive clarity of abstract mathematics.}{1270}
\chapter{Introduction}
\label{ch:introduction}
\input{intro}

\xkcdquote{I mean, ostensibly, yes. Honestly, we hacked most of it together with Perl}{224}
\chapter{Formalizing Launchbury's natural semantics}
\label{ch:launchbury}
\input{launchbury}

\xkcdquote{The problem with Haskell is that it's a language built on lazy evaluation and nobody's actually called for it.}{1312}
\chapter{Call Arity}
\label{ch:call-arity}
\input{call-arity}

\xkcdquote{I started with $P\wedge \neg P$ and derived your Mom’s phone number.}{704}
\chapter{The safety of Call Arity}
\label{ch:provingcallarity}
\input{call-arity-safe}

\xkcdquote{Excuse me, but \underline{real} programmer use butterflies.}{378}
\chapter{Conclusion}
\label{ch:conclusion}
\input{conclusion}

\appendix
\xkcdquote{Honk iff you love formal logic.}{1033}
\chapter{Formal definitions and main theorems}
\label{ch:formal-stuff}
\input{formal-stuff}

\xkcdquote{It's like someone took a transcript of a couple arguing at IKEA and made random edits until it compiled without errors.}{1513}
%\xkcdquote{The \#1 programmer excuse for legitimately slacking off:\par\centering “My code's compiling.”}{303}
\chapter{Call Arity code}
\label{ch:listings}
\input{listings.tex}

\ifbiblatex
\begingroup
\setlength{\emergencystretch}{.5em}
\printbibliography
\endgroup
\else
\bibliography{bib}
\fi

\printindex

\selectlanguage{ngerman}

%\chapter*{Lebenslauf}
%\markboth{Lebenslauf}{Lebenslauf}
%\input{lebenslauf}
%\selectlanguage{english}

\end{document}