changed an example

book.tex

@@ -99,21 +99,31 @@ Cambridge, Massachusetts\\
 London, England}
 
 \begin{copyrightpage}
-\textcopyright\ [YEAR] Massachusetts Institute of Technology
+  \textcopyright\ [2021] Jeremy G. Siek.  Available for free viewing
+  or personal downloading under the
+  \href{https://creativecommons.org/licenses/by-nc-nd/2.0/uk/}{CC-BY-NC-ND}
+  license.
+  
+  Copyright in this monograph has been licensed exclusively to The MIT
+  Press, \url{http://mitpress.mit.edu}, which will be releasing the final
+  version to the public in 2022. All inquiries regarding rights should
+  be addressed to The MIT Press, Rights and Permissions Department.
+
+%% \textcopyright\ [YEAR] Massachusetts Institute of Technology
 
-All rights reserved. No part of this book may be reproduced in any
-form by any electronic or mechanical means (including photocopying,
-recording, or information storage and retrieval) without permission in
-writing from the publisher.
+%% All rights reserved. No part of this book may be reproduced in any
+%% form by any electronic or mechanical means (including photocopying,
+%% recording, or information storage and retrieval) without permission in
+%% writing from the publisher.
 
-This book was set in LaTeX by Jeremy G. Siek. Printed and bound in the
-United States of America.
+%% This book was set in LaTeX by Jeremy G. Siek. Printed and bound in the
+%% United States of America.
 
-Library of Congress Cataloging-in-Publication Data is available.
+%% Library of Congress Cataloging-in-Publication Data is available.
 
-ISBN:
+%% ISBN:
 
-10\quad9\quad8\quad7\quad6\quad5\quad4\quad3\quad2\quad1
+%% 10\quad9\quad8\quad7\quad6\quad5\quad4\quad3\quad2\quad1
 \end{copyrightpage}
 
 \dedication{This book is dedicated to the programming language wonks
@@ -334,20 +344,22 @@ organization of the course made it difficult for students to
 understand the rationale for the compiler design. Ghuloum proposed the
 incremental approach~\citep{Ghuloum:2006bh}.
 
-We thank the many graduate students who served as teaching assistants
-for the compiler course at IU. In particular, we thank Andre
-Kuhlenschmidt for his work on the garbage collector, Michael Vollmer
-for his work on efficient tail calls, and Michael Vitousek for his
-help running the first offering of the incremental compiler course at
-IU.
+We thank the many students who served as teaching assistants for the
+compiler course at IU and made suggestions for improving the book
+including Carl Factora, Ryan Scott, and Cameron Swords. We especially
+thank Andre Kuhlenschmidt for his work on the garbage collector,
+Michael Vollmer for his work on efficient tail calls, and Michael
+Vitousek for his help running the first offering of the incremental
+compiler course at IU.
 
-We thank Bor-Yuh Chang, John Clements, Jay McCarthy, Joseph Near, Nate
-Nystrom, and Michael Wollowski for teaching courses based on early
-drafts of this book.
+We thank professors Bor-Yuh Chang, John Clements, Jay McCarthy, Joseph
+Near, Ryan Newton, Nate Nystrom, Andrew Tolmach, and Michael Wollowski
+for teaching courses based on early drafts of this book and for their
+invaluable feedback.
 
-We thank Ronald Garcia for being Jeremy's partner when they took the
-compiler course in the early 2000's and especially for finding the bug
-that sent the garbage collector on a wild goose chase!
+We thank Ronald Garcia helping Jeremy survive Dybvig's compiler course
+in the early 2000's and especially for finding the bug that sent the
+garbage collector on a wild goose chase!
 
 \mbox{}\\
 \noindent Jeremy G. Siek \\
@@ -2095,12 +2107,14 @@ in the program below. This is accomplished by introducing a new
 \key{let}-bound variable, binding the complex operand to the new
 variable, and then using the new variable in place of the complex
 operand, as shown in the output of \code{remove-complex-opera*} on the
-right.\\
+right.
+\begin{center}
 \begin{tabular}{lll}
 \begin{minipage}{0.4\textwidth}
 % var_test_19.rkt
 \begin{lstlisting}
-(+ 52 (- 10))
+(let ([x (+ 42 (- 10))])
+  (+ x 10))
 \end{lstlisting}
 \end{minipage}
 &
@@ -2108,12 +2122,13 @@ $\Rightarrow$
 &
 \begin{minipage}{0.4\textwidth}
 \begin{lstlisting}
-(let ([tmp.1 (- 10)])
-  (+ 52 tmp.1))
+(let ([x (let ([tmp.1 (- 10)])
+            (+ 42 tmp.1))])
+   (+ x 10))
 \end{lstlisting}
 \end{minipage}
 \end{tabular}
-
+\end{center}
 
 \begin{figure}[tp]
 \centering
@@ -2139,8 +2154,8 @@ this pass, the language \LangVarANF{}. The only difference is that
 operator arguments are restricted to be atomic expressions that are
 defined by the \Atm{} non-terminal. In particular, integer constants
 and variables are atomic. In the literature, restricting arguments to
-be atomic expressions is called \emph{administrative normal form}, or
-ANF for short~\citep{Danvy:1991fk,Flanagan:1993cg}.
+be atomic expressions is one of the ideas in \emph{administrative
+normal form}, or ANF for short~\citep{Danvy:1991fk,Flanagan:1993cg}.
 \index{subject}{administrative normal form} \index{subject}{ANF}
 
 We recommend implementing this pass with two mutually recursive
@@ -2152,20 +2167,19 @@ returns an expression.  The \code{rco-atom} function returns two
 things: an atomic expression and an alist mapping temporary variables to
 complex subexpressions. You can return multiple things from a function
 using Racket's \key{values} form and you can receive multiple things
-from a function call using the \key{define-values} form. If you are
-not familiar with these features, review the Racket documentation.
+from a function call using the \key{define-values} form.
 Also, the
 \href{https://docs.racket-lang.org/reference/for.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._for%2Flists%29%29}{\code{for/lists}}
   form is useful for applying a function to each element of a list, in
   the case where the function returns multiple values.
   \index{subject}{for/lists}
 
-Returning to the example program \code{(+ 52 (- 10))}, the
-subexpression \code{(- 10)} should be processed using the
+Returning to the example program with the expression \code{(+ 42 (-
+  10))}, the subexpression \code{(- 10)} should be processed using the
 \code{rco-atom} function because it is an argument of the \code{+} and
 therefore needs to become atomic.  The output of \code{rco-atom}
 applied to \code{(- 10)} is as follows.
-
+\begin{center}
 \begin{tabular}{lll}
 \begin{minipage}{0.4\textwidth}
 \begin{lstlisting}
@@ -2182,10 +2196,12 @@ tmp.1
 \end{lstlisting}
 \end{minipage}
 \end{tabular}
+\end{center}
 
-Take special care of programs such as the following one that binds a
+Take special care of programs such as the following that bind a
 variable to an atomic expression. You should leave such variable
-bindings unchanged, as shown in to the program on the right \\
+bindings unchanged, as shown in the program on the right \\
+\begin{center}
 \begin{tabular}{lll}
 \begin{minipage}{0.4\textwidth}
 % var_test_20.rkt
@@ -2205,9 +2221,11 @@ $\Rightarrow$
     b))
 \end{lstlisting}
 \end{minipage}
-\end{tabular} \\
+\end{tabular} 
+\end{center}
 A careless implementation of \key{rco-exp} and \key{rco-atom} might
-produce the following output with unnecessary temporary variables.\\
+produce the following output with unnecessary temporary variables.
+\begin{center}
 \begin{minipage}{0.4\textwidth}
 \begin{lstlisting}
 (let ([tmp.1 42])
@@ -2217,6 +2235,7 @@ produce the following output with unnecessary temporary variables.\\
         b))))
 \end{lstlisting}
 \end{minipage}
+\end{center}
 
 \begin{exercise}
 \normalfont
@@ -11841,7 +11860,7 @@ the \code{add1} function.
 \label{fig:gradual-map-vec}
 \end{figure}
 
-\section{Type Checking \LangGrad{}, Casts, and \LangCast{}}
+\section{Type Checking \LangGrad{} and \LangCast{}}
 \label{sec:gradual-type-check}
 
 The type checker for \LangGrad{} uses the \code{Any} type for missing
@@ -13524,7 +13543,11 @@ for the compilation of \LangPoly{}.
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{chapappendix}[Appendix]
+\clearpage
+
+\appendix
+
+\chapter{Appendix}
 
 \section{Interpreters}
 \label{appendix:interp}
@@ -13848,15 +13871,10 @@ and \ref{fig:c3-concrete-syntax}, respectively.
 \label{fig:c3-concrete-syntax}
 \end{figure}
 
-\end{chapappendix}
-
-%\setcounter{chapter}{2}
 
-\clearpage
-
-\appendix
 
 \backmatter
+\addtocontents{toc}{\vspace{11pt}}
 
 %% \addtocontents{toc}{\vspace{11pt}}
 

defs.tex

@@ -3,82 +3,82 @@
 \newcommand{\itm}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\ttm}[1]{\ensuremath{\text{\texttt{#1}}}}
 
-\newcommand{\LangInt}{\ensuremath{R_{\text{\texttt{Int}}}}} % R0
-\newcommand{\LangVar}{$R_{\ttm{Var}}$} % R1
-\newcommand{\LangVarM}{R_{\ttm{Var}}}
-\newcommand{\LangCVar}{$C_{\ttm{Var}}$} % C0
-\newcommand{\LangCVarM}{C_{\ttm{Var}}} % C0
-\newcommand{\LangVarANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Var}}}}
-\newcommand{\LangVarANFM}{R^{\mathsf{ANF}}_{\ttm{Var}}}
-\newcommand{\LangIf}{$R_{\ttm{If}}$} %R2
-\newcommand{\LangIfM}{\ensuremath{R_{\ttm{If}}}} %R2
-\newcommand{\LangCIf}{$C_{\ttm{If}}$} %C1
-\newcommand{\LangCIfM}{\ensuremath{C_{\ttm{If}}}} %C1
-\newcommand{\LangIfANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{if}}}} %R2
-\newcommand{\LangVec}{$R_{\ttm{Vec}}$} %R3
-\newcommand{\LangVecM}{R_{\ttm{Vec}}} %R3
-\newcommand{\LangStruct}{\ensuremath{R^{\ttm{Struct}}_{\ttm{Vec}}}} %R^s3
-\newcommand{\LangCVec}{$C_{\ttm{Vec}}$} %C2
-\newcommand{\LangCVecM}{C_{\ttm{Vec}}} %C2
-\newcommand{\LangVecANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Vec}}}} %R3
-\newcommand{\LangVecANFM}{R^{\mathsf{ANF}}_{\ttm{Vec}}} %R3
-\newcommand{\LangAlloc}{\ensuremath{R_{\ttm{Alloc}}}} %R3'
-\newcommand{\LangFun}{$R_{\ttm{Fun}}$} %R4
-\newcommand{\LangFunM}{R_{\ttm{Fun}}} %R4
-\newcommand{\LangCFun}{$C_{\ttm{Fun}}$} %C3
-\newcommand{\LangCFunM}{C_{\ttm{Fun}}} %C3
-\newcommand{\LangFunANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Fun}}}} %R4
-\newcommand{\LangFunRef}{$R_{\ttm{FunRef}}$} %F1
-\newcommand{\LangFunRefM}{R_{\ttm{FunRef}}} %F1
-\newcommand{\LangFunRefAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{FunRef}}}} %R'4
+\newcommand{\LangInt}{\ensuremath{R_{\mathsf{Int}}}} % R0
+\newcommand{\LangVar}{$R_{\mathsf{Var}}$} % R1
+\newcommand{\LangVarM}{R_{\mathsf{Var}}}
+\newcommand{\LangCVar}{$C_{\mathsf{Var}}$} % C0
+\newcommand{\LangCVarM}{C_{\mathsf{Var}}} % C0
+\newcommand{\LangVarANF}{\ensuremath{R^{\mathsf{ANF}}_{\mathsf{Var}}}}
+\newcommand{\LangVarANFM}{R^{\mathsf{ANF}}_{\mathsf{Var}}}
+\newcommand{\LangIf}{$R_{\mathsf{If}}$} %R2
+\newcommand{\LangIfM}{\ensuremath{R_{\mathsf{If}}}} %R2
+\newcommand{\LangCIf}{$C_{\mathsf{If}}$} %C1
+\newcommand{\LangCIfM}{\ensuremath{C_{\mathsf{If}}}} %C1
+\newcommand{\LangIfANF}{\ensuremath{R^{\mathsf{ANF}}_{\mathsf{if}}}} %R2
+\newcommand{\LangVec}{$R_{\mathsf{Vec}}$} %R3
+\newcommand{\LangVecM}{R_{\mathsf{Vec}}} %R3
+\newcommand{\LangStruct}{\ensuremath{R^{\mathsf{Struct}}_{\mathsf{Vec}}}} %R^s3
+\newcommand{\LangCVec}{$C_{\mathsf{Vec}}$} %C2
+\newcommand{\LangCVecM}{C_{\mathsf{Vec}}} %C2
+\newcommand{\LangVecANF}{\ensuremath{R^{\mathsf{ANF}}_{\mathsf{Vec}}}} %R3
+\newcommand{\LangVecANFM}{R^{\mathsf{ANF}}_{\mathsf{Vec}}} %R3
+\newcommand{\LangAlloc}{\ensuremath{R_{\mathsf{Alloc}}}} %R3'
+\newcommand{\LangFun}{$R_{\mathsf{Fun}}$} %R4
+\newcommand{\LangFunM}{R_{\mathsf{Fun}}} %R4
+\newcommand{\LangCFun}{$C_{\mathsf{Fun}}$} %C3
+\newcommand{\LangCFunM}{C_{\mathsf{Fun}}} %C3
+\newcommand{\LangFunANF}{\ensuremath{R^{\mathsf{ANF}}_{\mathsf{Fun}}}} %R4
+\newcommand{\LangFunRef}{$R_{\mathsf{FunRef}}$} %F1
+\newcommand{\LangFunRefM}{R_{\mathsf{FunRef}}} %F1
+\newcommand{\LangFunRefAlloc}{\ensuremath{R^{\mathsf{Alloc}}_{\mathsf{FunRef}}}} %R'4
 \newcommand{\LangLam}{$R_\lambda$} %R5
 \newcommand{\LangLamM}{\ensuremath{R_\lambda}} %R5
-\newcommand{\LangCLam}{$C_{\ttm{Clos}}$} %C4
-\newcommand{\LangCLamM}{C_{\ttm{Clos}}} %C4
-\newcommand{\LangAny}{$R_{\ttm{Any}}$} %R6
-\newcommand{\LangAnyM}{R_{\ttm{Any}}} %R6
-\newcommand{\LangAnyFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{Any}}}} %R'6
-\newcommand{\LangAnyAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{Any}}}} %R'6
-\newcommand{\LangCAny}{$C_{\ttm{Any}}$} %C5
-\newcommand{\LangCAnyM}{C_{\ttm{Any}}} %C5
-\newcommand{\LangDyn}{$R_{\ttm{Dyn}}$} %R7
-\newcommand{\LangDynM}{R_{\ttm{Dyn}}} %R7
-\newcommand{\LangDynFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{Dyn}}}} %R'7
-\newcommand{\LangLoop}{$R_{\ttm{While}}$} %R8
-\newcommand{\LangLoopM}{R_{\ttm{While}}} %R8
-\newcommand{\LangLoopFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{While}}}} %R'8
-\newcommand{\LangLoopAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{While}}}} %R'8
+\newcommand{\LangCLam}{$C_{\mathsf{Clos}}$} %C4
+\newcommand{\LangCLamM}{C_{\mathsf{Clos}}} %C4
+\newcommand{\LangAny}{$R_{\mathsf{Any}}$} %R6
+\newcommand{\LangAnyM}{R_{\mathsf{Any}}} %R6
+\newcommand{\LangAnyFunRef}{\ensuremath{R^{\mathsf{FunRef}}_{\mathsf{Any}}}} %R'6
+\newcommand{\LangAnyAlloc}{\ensuremath{R^{\mathsf{Alloc}}_{\mathsf{Any}}}} %R'6
+\newcommand{\LangCAny}{$C_{\mathsf{Any}}$} %C5
+\newcommand{\LangCAnyM}{C_{\mathsf{Any}}} %C5
+\newcommand{\LangDyn}{$R_{\mathsf{Dyn}}$} %R7
+\newcommand{\LangDynM}{R_{\mathsf{Dyn}}} %R7
+\newcommand{\LangDynFunRef}{\ensuremath{R^{\mathsf{FunRef}}_{\mathsf{Dyn}}}} %R'7
+\newcommand{\LangLoop}{$R_{\mathsf{While}}$} %R8
+\newcommand{\LangLoopM}{R_{\mathsf{While}}} %R8
+\newcommand{\LangLoopFunRef}{\ensuremath{R^{\mathsf{FunRef}}_{\mathsf{While}}}} %R'8
+\newcommand{\LangLoopAlloc}{\ensuremath{R^{\mathsf{Alloc}}_{\mathsf{While}}}} %R'8
 \newcommand{\LangCLoop}{$C_{\circlearrowleft}$} %C7
 \newcommand{\LangCLoopM}{C_{\circlearrowleft}} %C7
-\newcommand{\LangLoopANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{While}}}} %R8
-\newcommand{\LangArray}{\ensuremath{R^{\ttm{Vecof}}_{\ttm{While}}}} %R^s3
-\newcommand{\LangGrad}{$R_{\ttm{?}}$} %R9
-\newcommand{\LangGradM}{R_{\ttm{?}}} %R9
-\newcommand{\LangCast}{$R_{\ttm{cast}}$} %R9'
-\newcommand{\LangCastM}{R_{\ttm{cast}}} %R9'
-\newcommand{\LangProxy}{\ensuremath{R_{\ttm{proxy}}}} %R8''
-\newcommand{\LangPVec}{\ensuremath{R_{\ttm{PVec}}}} %R8''
-\newcommand{\LangPVecFunRef}{\ensuremath{R^{\ttm{FunRef}}_{\ttm{PVec}}}} %R8''
-\newcommand{\LangPVecAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{PVec}}}} %R8''
-\newcommand{\LangPoly}{\ensuremath{R_{\ttm{Poly}}}} %R10
-\newcommand{\LangInst}{\ensuremath{R_{\ttm{Inst}}}} %R'10
-\newcommand{\LangCLoopPVec}{\ensuremath{C^{\ttm{PVec}}_{\circlearrowleft}}} %Cp7
+\newcommand{\LangLoopANF}{\ensuremath{R^{\mathsf{ANF}}_{\mathsf{While}}}} %R8
+\newcommand{\LangArray}{\ensuremath{R^{\mathsf{Vecof}}_{\mathsf{While}}}} %R^s3
+\newcommand{\LangGrad}{$R_{\mathsf{?}}$} %R9
+\newcommand{\LangGradM}{R_{\mathsf{?}}} %R9
+\newcommand{\LangCast}{$R_{\mathsf{cast}}$} %R9'
+\newcommand{\LangCastM}{R_{\mathsf{cast}}} %R9'
+\newcommand{\LangProxy}{\ensuremath{R_{\mathsf{proxy}}}} %R8''
+\newcommand{\LangPVec}{\ensuremath{R_{\mathsf{PVec}}}} %R8''
+\newcommand{\LangPVecFunRef}{\ensuremath{R^{\mathsf{FunRef}}_{\mathsf{PVec}}}} %R8''
+\newcommand{\LangPVecAlloc}{\ensuremath{R^{\mathsf{Alloc}}_{\mathsf{PVec}}}} %R8''
+\newcommand{\LangPoly}{\ensuremath{R_{\mathsf{Poly}}}} %R10
+\newcommand{\LangInst}{\ensuremath{R_{\mathsf{Inst}}}} %R'10
+\newcommand{\LangCLoopPVec}{\ensuremath{C^{\mathsf{PVec}}_{\circlearrowleft}}} %Cp7
 
-\newcommand{\LangXVar}{\ensuremath{\mathrm{x86}_{\ttm{Var}}}} % pseudo x86_0
-\newcommand{\LangXASTInt}{\ensuremath{\mathrm{x86}_{\ttm{Int}}}} % x86_0
-\newcommand{\LangXInt}{$\mathrm{x86}_{\ttm{Int}}$} %x86^{\dagger}_0
-\newcommand{\LangXIntM}{\mathrm{x86}_{\ttm{Int}}} %x86^{\dagger}_0
-\newcommand{\LangXASTIf}{\ensuremath{\mathrm{x86}_{\ttm{If}}}} %x86_1
-\newcommand{\LangXIf}{$\mathrm{x86}_{\ttm{If}}$} %x86^{\dagger}_1
-\newcommand{\LangXIfM}{\mathrm{x86}_{\ttm{If}}} %x86^{\dagger}_1
-\newcommand{\LangXIfVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{If}}}} %x86^{*}_1
-\newcommand{\LangXASTGlobal}{\ensuremath{\mathrm{x86}_{\ttm{Global}}}} %x86_2
-\newcommand{\LangXGlobal}{$\mathrm{x86}_{\ttm{Global}}$} %x86^{\dagger}_2
-\newcommand{\LangXGlobalM}{\mathrm{x86}_{\ttm{Global}}} %x86^{\dagger}_2
-\newcommand{\LangXGlobalVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{Global}}}} %x86^{*}_2
-\newcommand{\LangXIndCall}{$\mathrm{x86}_{\ttm{callq*}}$} %x86_3
-\newcommand{\LangXIndCallM}{\mathrm{x86}_{\ttm{callq*}}} %x86_3
-\newcommand{\LangXIndCallVar}{\ensuremath{\mathrm{x86}^{\ttm{Var}}_{\ttm{callq*}}}} %x86^*_3
+\newcommand{\LangXVar}{\ensuremath{\mathrm{x86}_{\mathsf{Var}}}} % pseudo x86_0
+\newcommand{\LangXASTInt}{\ensuremath{\mathrm{x86}_{\mathsf{Int}}}} % x86_0
+\newcommand{\LangXInt}{$\mathrm{x86}_{\mathsf{Int}}$} %x86^{\dagger}_0
+\newcommand{\LangXIntM}{\mathrm{x86}_{\mathsf{Int}}} %x86^{\dagger}_0
+\newcommand{\LangXASTIf}{\ensuremath{\mathrm{x86}_{\mathsf{If}}}} %x86_1
+\newcommand{\LangXIf}{$\mathrm{x86}_{\mathsf{If}}$} %x86^{\dagger}_1
+\newcommand{\LangXIfM}{\mathrm{x86}_{\mathsf{If}}} %x86^{\dagger}_1
+\newcommand{\LangXIfVar}{\ensuremath{\mathrm{x86}^{\mathsf{Var}}_{\mathsf{If}}}} %x86^{*}_1
+\newcommand{\LangXASTGlobal}{\ensuremath{\mathrm{x86}_{\mathsf{Global}}}} %x86_2
+\newcommand{\LangXGlobal}{$\mathrm{x86}_{\mathsf{Global}}$} %x86^{\dagger}_2
+\newcommand{\LangXGlobalM}{\mathrm{x86}_{\mathsf{Global}}} %x86^{\dagger}_2
+\newcommand{\LangXGlobalVar}{\ensuremath{\mathrm{x86}^{\mathsf{Var}}_{\mathsf{Global}}}} %x86^{*}_2
+\newcommand{\LangXIndCall}{$\mathrm{x86}_{\mathsf{callq*}}$} %x86_3
+\newcommand{\LangXIndCallM}{\mathrm{x86}_{\mathsf{callq*}}} %x86_3
+\newcommand{\LangXIndCallVar}{\ensuremath{\mathrm{x86}^{\mathsf{Var}}_{\mathsf{callq*}}}} %x86^*_3
 
 \newcommand{\Stmt}{\itm{stmt}}
 \newcommand{\Exp}{\itm{exp}}
@@ -102,22 +102,22 @@
 \newcommand{\RP}[0]{\key{)}}
 \newcommand{\LS}[0]{\key{[}}
 \newcommand{\RS}[0]{\key{]}}
-\newcommand{\INT}[1]{\key{(Int}\;#1\key{)}}
-\newcommand{\BOOL}[1]{\key{(Bool}\;#1\key{)}}
+\newcommand{\INT}[1]{\key{(Int}~#1\key{)}}
+\newcommand{\BOOL}[1]{\key{(Bool}~#1\key{)}}
 \newcommand{\PRIM}[2]{\LP\key{Prim}~#1~\LP #2\RP\RP}
-\newcommand{\READ}{\key{(Prim}\;\code{read}\;\key{())}}
+\newcommand{\READ}{\key{(Prim}~\code{read}~\key{())}}
 \newcommand{\CREAD}{\key{(read)}}
-\newcommand{\NEG}[1]{\key{(Prim}\;\code{-}\;\code{(}#1\code{))}}
+\newcommand{\NEG}[1]{\key{(Prim}~\code{-}~\code{(}#1\code{))}}
 \newcommand{\CNEG}[1]{\LP\key{-}~#1\RP}
-\newcommand{\PROGRAM}[2]{\LP\code{Program}\;#1\;#2\RP}
-\newcommand{\CPROGRAM}[2]{\LP\code{CProgram}\;#1\;#2\RP}
-\newcommand{\XPROGRAM}[2]{\LP\code{X86Program}\;#1\;#2\RP}
+\newcommand{\PROGRAM}[2]{\LP\code{Program}~#1~#2\RP}
+\newcommand{\CPROGRAM}[2]{\LP\code{CProgram}~#1~#2\RP}
+\newcommand{\XPROGRAM}[2]{\LP\code{X86Program}~#1~#2\RP}
 \newcommand{\PROGRAMDEFSEXP}[3]{\code{(ProgramDefsExp}~#1~#2~#3\code{)}}
 \newcommand{\PROGRAMDEFS}[2]{\code{(ProgramDefs}~#1~#2\code{)}}
-\newcommand{\ADD}[2]{\key{(Prim}\;\code{+}\;\code{(}#1\;#2\code{))}}
+\newcommand{\ADD}[2]{\key{(Prim}~\code{+}~\code{(}#1~#2\code{))}}
 \newcommand{\CADD}[2]{\LP\key{+}~#1~#2\RP}
 \newcommand{\CMUL}[2]{\LP\key{*}~#1~#2\RP}
-\newcommand{\SUB}[2]{\key{(Prim}\;\code{-}\;\code{(}#1\;#2\code{))}}
+\newcommand{\SUB}[2]{\key{(Prim}~\code{-}~\code{(}#1~#2\code{))}}
 \newcommand{\CSUB}[2]{\LP\key{-}~#1~#2\RP}
 \newcommand{\CWHILE}[2]{\LP\key{while}~#1~#2\RP}
 \newcommand{\WHILE}[2]{\LP\key{WhileLoop}~#1~#2\RP}
@@ -126,68 +126,68 @@
 \newcommand{\BEGIN}[2]{\LP\key{Begin}~#1~#2\RP}
 \newcommand{\CSETBANG}[2]{\LP\key{set!}~#1~#2\RP}
 \newcommand{\SETBANG}[2]{\LP\key{SetBang}~#1~#2\RP}
-\newcommand{\AND}[2]{\key{(Prim}\;\code{and}\;\code{(}#1\;#2\code{))}}
-\newcommand{\OR}[2]{\key{(Prim}\;\code{or}\;\code{(}#1\;#2\code{))}}
-\newcommand{\NOT}[1]{\key{(Prim}\;\code{not}\;\code{(}#1\;\code{))}}
-\newcommand{\UNIOP}[2]{\key{(Prim}\;#1\;\code{(}#2\code{))}}
-\newcommand{\CUNIOP}[2]{\LP #1\;#2 \RP}
-\newcommand{\BINOP}[3]{\key{(Prim}\;#1\;\code{(}#2\;#3\code{))}}
-\newcommand{\CBINOP}[3]{\LP #1\;#2\;#3\RP}
+\newcommand{\AND}[2]{\key{(Prim}~\code{and}~\code{(}#1~#2\code{))}}
+\newcommand{\OR}[2]{\key{(Prim}~\code{or}~\code{(}#1~#2\code{))}}
+\newcommand{\NOT}[1]{\key{(Prim}~\code{not}~\code{(}#1~\code{))}}
+\newcommand{\UNIOP}[2]{\key{(Prim}~#1~\code{(}#2\code{))}}
+\newcommand{\CUNIOP}[2]{\LP #1~#2 \RP}
+\newcommand{\BINOP}[3]{\key{(Prim}~#1~\code{(}#2~#3\code{))}}
+\newcommand{\CBINOP}[3]{\LP #1~#2~#3\RP}
 \newcommand{\CLET}[3]{\LP\key{let}~\LP\LS#1~#2\RS\RP~#3\RP}
 \newcommand{\CIF}[3]{\LP\key{if}~#1~#2~#3\RP}
-\newcommand{\VAR}[1]{\key{(Var}\;#1\key{)}}
+\newcommand{\VAR}[1]{\key{(Var}~#1\key{)}}
 \newcommand{\LET}[3]{\key{(Let}~#1~#2~#3\key{)}}
-\newcommand{\IF}[3]{\key{(If}\,#1\;#2\;#3\key{)}}
+\newcommand{\IF}[3]{\key{(If}\,#1~#2~#3\key{)}}
 \newcommand{\CAST}[3]{\LP\key{Cast}~#1~#2~#3\RP}
-\newcommand{\VECTOR}[1]{\LP\key{Prim}\;\code{vector}\;\LP\;#1\RP\RP}
-\newcommand{\VECREF}[2]{\LP\key{Prim}\;\code{vector-ref}\;\LP\;#1\;#2\RP\RP}
-\newcommand{\VECSET}[3]{\LP\key{Prim}\;\code{vector-set!}\;\LP\;#1\;#2\;#3\RP\RP}
-\newcommand{\VECLEN}[1]{\LP\key{Prim}\;\code{vector-length}\;\LP\;#1\RP\RP}
-\newcommand{\ANYVECREF}[2]{\LP\key{Prim}\;\code{any-vector-ref}\;\LP\;#1\;#2\RP\RP}
-\newcommand{\ANYVECSET}[3]{\LP\key{Prim}\;\code{any-vector-set!}\;\LP\;#1\;#2\;#3\RP\RP}
-\newcommand{\ANYVECLEN}[1]{\LP\key{Prim}\;\code{any-vector-length}\;\LP\;#1\RP\RP}
+\newcommand{\VECTOR}[1]{\LP\key{Prim}~\code{vector}~\LP~#1\RP\RP}
+\newcommand{\VECREF}[2]{\LP\key{Prim}~\code{vector-ref}~\LP~#1~#2\RP\RP}
+\newcommand{\VECSET}[3]{\LP\key{Prim}~\code{vector-set!}~\LP~#1~#2~#3\RP\RP}
+\newcommand{\VECLEN}[1]{\LP\key{Prim}~\code{vector-length}~\LP~#1\RP\RP}
+\newcommand{\ANYVECREF}[2]{\LP\key{Prim}~\code{any-vector-ref}~\LP~#1~#2\RP\RP}
+\newcommand{\ANYVECSET}[3]{\LP\key{Prim}~\code{any-vector-set!}~\LP~#1~#2~#3\RP\RP}
+\newcommand{\ANYVECLEN}[1]{\LP\key{Prim}~\code{any-vector-length}~\LP~#1\RP\RP}
 \newcommand{\CLOSURE}[2]{\LP\key{Closure}~#1~#2\RP}
 \newcommand{\ALLOC}[2]{\LP\key{Allocate}~#1~#2\RP}
 \newcommand{\ALLOCCLOS}[3]{\LP\key{AllocateClosure}~#1~#2~#3\RP}
 
 \newcommand{\VOID}[1]{\key{(Void)}}
-\newcommand{\APPLY}[2]{\key{(Apply}\;#1\;#2\code{)}}
-\newcommand{\CALL}[2]{\key{(Call}\;#1\;#2\code{)}}
-\newcommand{\TAILCALL}[2]{\key{(TailCall}\;#1\;#2\code{)}}
+\newcommand{\APPLY}[2]{\key{(Apply}~#1~#2\code{)}}
+\newcommand{\CALL}[2]{\key{(Call}~#1~#2\code{)}}
+\newcommand{\TAILCALL}[2]{\key{(TailCall}~#1~#2\code{)}}
 \newcommand{\FUNDEF}[5]{\key{(Def}~#1~#2~#3~#4~#5\code{)}}
-\newcommand{\FUNREF}[1]{\key{(FunRef}\;#1\code{)}}
-\newcommand{\CFUNREF}[1]{\key{(fun-ref}\;#1\code{)}}
+\newcommand{\FUNREF}[1]{\key{(FunRef}~#1\code{)}}
+\newcommand{\CFUNREF}[1]{\key{(fun-ref}~#1\code{)}}
 \newcommand{\FUNREFARITY}[2]{\key{(FunRefArity}~#1~#2\code{)}}
 \newcommand{\CFUNREFARITY}[2]{\key{(fun-ref-arity}~#1~#2\code{)}}
 \newcommand{\LAMBDA}[3]{\key{(Lambda}~#1~#2~#3\code{)}}
-\newcommand{\CLAMBDA}[3]{\LP\key{lambda:}\,#1\,\key{:}\,#2\;\Exp\RP}
-\newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2\;\Exp\RP}
+\newcommand{\CLAMBDA}[3]{\LP\key{lambda:}\,#1\,\key{:}\,#2~\Exp\RP}
+\newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2~\Exp\RP}
 \newcommand{\INJECT}[2]{\LP\key{Inject}~#1~#2\RP}
 \newcommand{\PROJECT}[2]{\LP\key{Project}~#1~#2\RP}
 \newcommand{\CINJECT}[2]{\LP\key{inject}~#1~#2\RP}
 \newcommand{\CPROJECT}[2]{\LP\key{project}~#1~#2\RP}
 \newcommand{\VALUEOF}[2]{\LP\key{ValueOf}~#1~#2\RP}
 
-\newcommand{\ASSIGN}[2]{\key{(Assign}~#1\;#2\key{)}}
+\newcommand{\ASSIGN}[2]{\key{(Assign}~#1~#2\key{)}}
 \newcommand{\RETURN}[1]{\key{(Return}~#1\key{)}}
 \newcommand{\SEQ}[2]{\key{(Seq}~#1~#2\key{)}}
 \newcommand{\GOTO}[1]{\key{(Goto}~#1\key{)}}
-\newcommand{\IFSTMT}[3]{\key{(IfStmt}\,#1\;#2\;#3\key{)}}
+\newcommand{\IFSTMT}[3]{\key{(IfStmt}\,#1~#2~#3\key{)}}
 
-\newcommand{\IMM}[1]{\key{(Imm}\;#1\key{)}}
-\newcommand{\REG}[1]{\key{(Reg}\;#1\key{)}}
-\newcommand{\BYTEREG}[1]{\key{(ByteReg}\;#1\key{)}}
+\newcommand{\IMM}[1]{\key{(Imm}~#1\key{)}}
+\newcommand{\REG}[1]{\key{(Reg}~#1\key{)}}
+\newcommand{\BYTEREG}[1]{\key{(ByteReg}~#1\key{)}}
 \newcommand{\DEREF}[2]{\key{(Deref}~#1~#2\key{)}}
 \newcommand{\DEF}[5]{\LP\key{Def}~#1~#2~#3~#4~#5\RP}
 \newcommand{\CDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,\key{:}\,#3~#4\RP}
 \newcommand{\CGDEF}[4]{\LP\key{define}~\LP#1~#2\RP\,#3~#4\RP}
 \newcommand{\DECL}[2]{\LP\key{Decl}~#1~#2\RP}
 \newcommand{\INST}[3]{\LP\key{Inst}~#1~#2~#3\RP}
-\newcommand{\CFG}[1]{\key{(CFG}\;#1\key{)}}
-\newcommand{\BLOCK}[2]{\key{(Block}\;#1\;#2\key{)}}
-\newcommand{\STACKLOC}[1]{(\key{stack}\;#1)}
-\newcommand{\BININSTR}[3]{\key{(Instr}\;#1\;\key{(}\;#2\;#3\key{))}}
-\newcommand{\UNIINSTR}[2]{\key{(Instr}\;#1\;\key{(}\;#2\key{))}}
+\newcommand{\CFG}[1]{\key{(CFG}~#1\key{)}}
+\newcommand{\BLOCK}[2]{\key{(Block}~#1~#2\key{)}}
+\newcommand{\STACKLOC}[1]{(\key{stack}~#1)}
+\newcommand{\BININSTR}[3]{\key{(Instr}~#1~\key{(}~#2~#3\key{))}}
+\newcommand{\UNIINSTR}[2]{\key{(Instr}~#1~\key{(}~#2\key{))}}
 \newcommand{\CALLQ}[2]{\key{(Callq}~#1~#2\key{)}}
 \newcommand{\INDCALLQ}[2]{\key{(IndirectCallq}~#1~#2\key{)}}
 \newcommand{\RETQ}{\key{(Retq)}}