From 68e92ccd2b456b9ce81b0617417bc8abdaff6fa3 Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Wed, 2 Dec 2009 15:50:42 +0100
Subject: [PATCH] Add an intermezzo about substitution.

This is the first attempt at an intermezzo, which is not quite ideal yet,
but it works for now.
---
 Chapters/Normalization.tex | 29 ++++++++++++++++++++++++++---
 Utils/Lambda.tex           | 14 ++++++++++++++
 2 files changed, 40 insertions(+), 3 deletions(-)

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 78b7a1d..03f3792 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -641,8 +641,6 @@
       In the following sections, we will be using a number of functions and
       notations, which we will define here.
 
-      \todo{Define substitution (notation)}
-
       \subsubsection{Concepts}
         A \emph{global variable} is any variable (binder) that is bound at the
         top level of a program, or an external module. A \emph{local variable} is any
@@ -799,8 +797,33 @@
        optimizations, but they are required to get our program into intended
        normal form.
 
+        \placeintermezzo{}{
+          \startframedtext[width=8cm,background=box,frame=no]
+          \startalignment[center]
+            {\tfa Substitution notation}
+          \stopalignment
+          \blank[medium]
+
+          In some of the transformations in this chapter, we need to perform
+          substitution on an expression. Substitution means replacing every
+          occurence of some expression (usually a variable reference) with
+          another expression.
+
+          There have been a lot of different notations used in literature for
+          specifying substitution. The notation that will be used in this report
+          is the following:
+
+          \startlambda
+            E[A=>B]
+          \stoplambda
+
+          This means expression \lam{E} with all occurences of \lam{A} replaced
+          with \lam{B}.
+          \stopframedtext
+        }
+
+      \defref{beta-reduction}
       \subsubsection[sec:normalization:beta]{β-reduction}
-        \defref{beta-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is
         the main reduction step. It reduces applications of lambda abstractions,
         removing both the lambda abstraction and the application.
diff --git a/Utils/Lambda.tex b/Utils/Lambda.tex
index f08d75e..319b424 100644
--- a/Utils/Lambda.tex
+++ b/Utils/Lambda.tex
@@ -124,4 +124,18 @@ draw b;
 \definefloat[example][examples]
 \setupcaption[example][location=top] % Put captions on top
 
+% Margin magic taken from
+% http://www.pragma-ade.com/general/manuals/details.pdf By setting negative
+% margin distances, we put our float inside the outer margin. I think we set
+% both left and right margin distance, because we don't know what will be the
+% outer margin (and it will probably only use the distance of the margin it's
+% actually aligning against).
+% We also set an offset, to prevent protruding text (overfull hboxes) from
+% jamming into the intermezzo. Also, some extra space is easier on the eye
+% (However, the intermezzo is moved to the right by this offset, instead of
+% moving the text to left. We can't increase the offset by much...)
+\setupfloat[intermezzo][offset=.3cm,leftmargindistance=-\leftmarginwidth, rightmargindistance=-\rightmarginwidth, default={outer}]
+\setupcaption[intermezzo][location=top,number=no] % Put captions on top
+
+\setupheads[aligntitle=float]
 % vim: set sw=2 sts=2 expandtab:
-- 
2.30.2