Writing

src/ActorMonad.lagda.tex

@@ -38,7 +38,7 @@
 The \AgdaFunction{InboxShape} is a variant type that details
 all the messages that can be received from an inbox.
 Every message sent to an actor will have exactly one of the types that is listed,
-which we communicate as a tag attached to the message (see section \ref{sec:messages}).
+which we communicate as a tag attached to the message (see section~\ref{sec:messages}).
 We can think of the \AgdaFunction{InboxShape} as a set of types,
 and every message coming paired with a proof that the message is a type from that set.
 To know what type a message has you have to inspect the proof,
@@ -183,25 +183,18 @@
 A de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term,
 and denotes the number of binders that are in scope between that occurrence
 and its corresponding binder.
-Following are some examples comparing a λ-calculus with names
-and a λ-calculus using de Bruijn indices.
-
-\begin{table}[htbp]
-\centering
-\begin{tabular}{ll}
-Named                                 & de Bruijn                 \\
-$ λ\ x → x $                          & $ λ\ 1 $                  \\
-$ λ\ x → λ\ y → x $                   & $ λ\ λ\ 2 $               \\
-$ λ\ x → λ\ y → λ\ z → x\ z\ (y\ z) $ & $ λ\ λ\ λ\ 3\ 1\ (2\ 1) $ \\
-\end{tabular}
-\end{table}
+Figure~\ref{fig:debruijn} shows some examples comparing a λ-calculus with names
+to a λ-calculus using de Bruijn indices.
+
+\input{include/figures/debruijn}
 
 What makes de Bruijn indices easy to work with in Agda is that it lets us manage
 the variable typing context as a list of types, with variables as
 (de Bruijn) indices into that list.
 We choose to represent the indices as the membership proposition
 in order to make the de Bruijn indices correct by construction.
 This lets us define the type judgement $Γ ⊢ T$ as:
+
 \begin{minipage}{\textwidth}
 \begin{code}
 ReferenceTypes = List InboxShape
@@ -241,7 +234,7 @@
 since different actors receiving the reply will have a different \AgdaFunction{InboxShape}.
 This pattern, together with a selective receive construct,
 can be used to implement synchronous calls,
-which we explore in chapter \ref{chap:selective_receive}.
+which we explore in chapter~\ref{chap:selective_receive}.
 %</ReferenceSubtype>
 
 %<*Messages>
@@ -269,7 +262,11 @@
 send-field-content : TypingContext → MessageField → Set₁
 send-field-content Γ (ValueType A) = Lift A
 send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 record SendMessage (To : InboxShape)
                    (Γ : TypingContext) : Set₁ where
   constructor SendM
@@ -287,7 +284,7 @@
 Instead we find the unit type \AgdaDatatype{⊤}, which has no computational content at all.
 The answer to this puzzle lies in that receiving a message will have the side-effect of
 adding the references from every reference field to the variable context.
-We saw in figure \ref{fig:actorm} that the shape of the variable typing context is maintained
+We saw in figure~\ref{fig:actorm} that the shape of the variable typing context is maintained
 in the type of the monad,
 making it easy to create indices into the variable context
 without making them a part of the message.
@@ -299,19 +296,31 @@
 receive-field-content : MessageField → Set
 receive-field-content (ValueType A) = A
 receive-field-content (ReferenceType Fw) = ⊤
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 record Message (To : InboxShape) : Set₁ where
   constructor Msg
   field
     {MT} : MessageType
     received-message-type : MT ∈ To
     received-fields : All receive-field-content MT
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 extract-references : MessageType → ReferenceTypes
 extract-references [] = []
 extract-references (ValueType x ∷ mt) = extract-references mt
 extract-references (ReferenceType T ∷ mt) = T ∷ extract-references mt
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 add-references : ∀ {To} → TypingContext → Message To → TypingContext
 add-references Γ (Msg {MT} x x₁) = extract-references MT ++ Γ
 \end{code}

src/Examples/MonadParameterized.lagda.tex

@@ -33,12 +33,17 @@
 %</Monad>
 
 %<*MonadFile>
+\begin{minipage}{\textwidth}
 \begin{code}
 
 data FileState : Set where
   Open : String → FileState
   Closed : FileState
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 data FileMonad : (A : Set) → FileState → (A → FileState) → Set₁ where
   return : ∀ {A post} → (val : A) → FileMonad A (post val) post
   _>>=_ : ∀ {A B pre mid post} →
@@ -48,12 +53,17 @@
   OpenFile : String → FileMonad FileState Closed (λ x → x)
   CloseFile : ∀ { s } → FileMonad ⊤ (Open s) (λ _ → Closed)
   WriteFile : ∀ { s } → String → FileMonad ⊤ (Open s) (λ _ → Open s)
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 writeHello : FileMonad ⊤ Closed (λ _ → Closed)
 writeHello = OpenFile "world.txt" >>= λ {
   Closed → return _ ;
   (Open _) → WriteFile "hello" >>= λ _ → CloseFile
   }
 \end{code}
+\end{minipage}
 %</MonadFile>
 

src/Examples/SizedStream.lagda.tex

@@ -22,15 +22,21 @@
 \end{code}
 %</SkipTwice>
 %<*Fib>
+\begin{minipage}{\textwidth}
 \begin{code}
 zipWith : (i : Size) {A B C : Set} → (A → B → C) →
           Stream i A → Stream i B → Stream i C
 (zipWith i f xs ys) .head = f (xs .head) (ys .head)
 (zipWith i f xs ys) .tail j = zipWith j f (xs .tail j) (ys .tail j)
+\end{code}
+\end{minipage}
 
+\begin{minipage}{\textwidth}
+\begin{code}
 fib : (i : Size) → Stream i ℕ
 fib i .head = 0
 fib i .tail j .head = 1
 fib i .tail j .tail k = zipWith k _+_ (fib k) (fib j .tail k)
 \end{code}
+\end{minipage}
 %</Fib>

src/Selective/SimulationEnvironment.lagda.tex

@@ -453,14 +453,20 @@
     is-ls : (heads) ++ (el ∷ tails) ≡ ls
 \end{code}
 %</SplitList>
-%<*FoundInList>
+%<*matches-filter>
 \begin{code}
 matches-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set
 matches-filter f v = f v ≡ true
-
+\end{code}
+%</matches-filter>
+%<*misses-filter>
+\begin{code}
 misses-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set
 misses-filter f v = f v ≡ false
-
+\end{code}
+%</misses-filter>
+%<*FoundInList>
+\begin{code}
 data FoundInList {a : Level} {A : Set a}
                  (ls : List A)
                  (f : A → Bool) :