finished array challenge

book.tex

@@ -7173,7 +7173,7 @@ for the compilation of \LangVec{}.
 \index{structure}
 
 Figure~\ref{fig:r3s-concrete-syntax} defines the concrete syntax for
-$R^s_3$, which extends $R^3$ with support for simple structures.
+\LangStruct{}, which extends \LangVec{} with support for simple structures.
 Recall that a \code{struct} in Typed Racket is a user-defined data
 type that contains named fields and that is heap allocated, similar to
 a vector. The following is an example of a structure definition, in
@@ -7204,12 +7204,12 @@ this case the definition of a \code{point} type.
   &\mid& \gray{ (\key{vector-set!}\;\Exp\;\Int\;\Exp) }\\
   &\mid& \gray{ (\key{void}) } \mid (\Var\;\Exp \ldots)\\
   \Def &::=& (\key{struct}\; \Var \; ([\Var \,\key{:}\, \Type] \ldots)\; \code{\#:mutable})\\
-  R^s_3 &::=& \Def \ldots \; \Exp
+  \LangStruct{} &::=& \Def \ldots \; \Exp
 \end{array}
 \]
 \end{minipage}
 }
-\caption{The concrete syntax of $R^s_3$, extending \LangVec{}
+\caption{The concrete syntax of \LangStruct{}, extending \LangVec{}
   (Figure~\ref{fig:Rvec-concrete-syntax}).}
 \label{fig:r3s-concrete-syntax}
 \end{figure}
@@ -7247,7 +7247,7 @@ mark. The following example uses \code{set-point-x!} to change the
 
 \begin{exercise}\normalfont
   Extend your compiler with support for simple structures, compiling
-  $R^s_3$ to x86 assembly code. Create five new test cases that use
+  \LangStruct{} to x86 assembly code. Create five new test cases that use
   structures and test your compiler.
 \end{exercise}
 
@@ -9498,7 +9498,7 @@ Section~\ref{sec:compile-r7} but first we describe the \LangAny{} language
 in greater detail.
 
 \section{The \LangAny{} Language}
-\label{sec:r6-lang}
+\label{sec:Rany-lang}
 
 \begin{figure}[tp]
 \centering
@@ -9522,13 +9522,13 @@ in greater detail.
 \end{minipage}
 }
 \caption{The abstract syntax of \LangAny{}, extending \LangLam{} (Figure~\ref{fig:Rlam-syntax}).}
-\label{fig:r6-syntax}
+\label{fig:Rany-syntax}
 \end{figure}
 
 
-The abstract syntax of \LangAny{} is defined in Figure~\ref{fig:r6-syntax}.
+The abstract syntax of \LangAny{} is defined in Figure~\ref{fig:Rany-syntax}.
 (The concrete syntax of \LangAny{} is in the Appendix,
-Figure~\ref{fig:r6-concrete-syntax}.)  The $\INJECT{e}{T}$ form
+Figure~\ref{fig:Rany-concrete-syntax}.)  The $\INJECT{e}{T}$ form
 converts the value produced by expression $e$ of type $T$ into a
 tagged value.  The $\PROJECT{e}{T}$ form converts the tagged value
 produced by expression $e$ into a value of type $T$ or else halts the
@@ -9768,21 +9768,21 @@ in Figure~\ref{fig:apply-project}.
 \label{sec:compile-r7}
 
 The \code{cast-insert} pass compiles from \LangDyn{} to \LangAny{}.
-Figure~\ref{fig:compile-r7-r6} shows the compilation of many of the
+Figure~\ref{fig:compile-r7-Rany} shows the compilation of many of the
 \LangDyn{} forms into \LangAny{}. An important invariant of this pass is that
 given a subexpression $e$ in the \LangDyn{} program, the pass will produce
 an expression $e'$ in \LangAny{} that has type \key{Any}. For example, the
-first row in Figure~\ref{fig:compile-r7-r6} shows the compilation of
+first row in Figure~\ref{fig:compile-r7-Rany} shows the compilation of
 the Boolean \code{\#t}, which must be injected to produce an
 expression of type \key{Any}.
 %
-The second row of Figure~\ref{fig:compile-r7-r6}, the compilation of
+The second row of Figure~\ref{fig:compile-r7-Rany}, the compilation of
 addition, is representative of compilation for many primitive
 operations: the arguments have type \key{Any} and must be projected to
 \key{Integer} before the addition can be performed.
 
 The compilation of \key{lambda} (third row of
-Figure~\ref{fig:compile-r7-r6}) shows what happens when we need to
+Figure~\ref{fig:compile-r7-Rany}) shows what happens when we need to
 produce type annotations: we simply use \key{Any}.
 %
 The compilation of \code{if} and \code{eq?}  demonstrate how this pass
@@ -9917,13 +9917,13 @@ $\Rightarrow$
 \end{tabular} 
 
 \caption{Cast Insertion}
-\label{fig:compile-r7-r6}
+\label{fig:compile-r7-Rany}
 \end{figure}
 
 
 
 \section{Reveal Casts}
-\label{sec:reveal-casts-r6}
+\label{sec:reveal-casts-Rany}
 
 % TODO: define R'_6
 
@@ -10001,13 +10001,13 @@ translated in a similar way.
 \end{lstlisting}
 
 \section{Remove Complex Operands}
-\label{sec:rco-r6}
+\label{sec:rco-Rany}
 
 The \code{ValueOf} and \code{Exit} forms are both complex expressions.
 The subexpression of \code{ValueOf} must be atomic.
 
 \section{Explicate Control and \LangCAny{}}
-\label{sec:explicate-r6}
+\label{sec:explicate-Rany}
 
 The output of \code{explicate-control} is the \LangCAny{} language whose
 syntax is defined in Figure~\ref{fig:c5-syntax}. The \code{ValueOf}
@@ -10046,7 +10046,7 @@ of an integer, as in \LangCVec{} (Figure~\ref{fig:c2-syntax}).
 
 
 \section{Select Instructions}
-\label{sec:select-r6}
+\label{sec:select-Rany}
 
 In the \code{select-instructions} pass we translate the primitive
 operations on the \code{Any} type to x86 instructions that involve
@@ -10164,7 +10164,7 @@ The code generation for \code{any-vector-set!} is similar to the other
 \code{any-vector} operations.
 
 \section{Register Allocation for \LangAny{}}
-\label{sec:register-allocation-r6}
+\label{sec:register-allocation-Rany}
 \index{register allocation}
 
 There is an interesting interaction between tagged values and garbage
@@ -10348,8 +10348,8 @@ evaluated left-to-right.
 \]
 \end{minipage}
 }
-\caption{The concrete syntax of \LangLoop{}, extending \LangAny{} (Figure~\ref{fig:r6-concrete-syntax}).}
-\label{fig:r8-concrete-syntax}
+\caption{The concrete syntax of \LangLoop{}, extending \LangAny{} (Figure~\ref{fig:Rany-concrete-syntax}).}
+\label{fig:Rwhile-concrete-syntax}
 \end{figure}
 
 \begin{figure}[tp]
@@ -10374,13 +10374,13 @@ evaluated left-to-right.
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangLoop{}, extending \LangAny{} (Figure~\ref{fig:r6-syntax}).}
-\label{fig:r8-syntax}
+\caption{The abstract syntax of \LangLoop{}, extending \LangAny{} (Figure~\ref{fig:Rany-syntax}).}
+\label{fig:Rwhile-syntax}
 \end{figure}
 
 The concrete syntax of \LangLoop{} is defined in
-Figure~\ref{fig:r8-concrete-syntax} and its abstract syntax is defined
-in Figure~\ref{fig:r8-syntax}.
+Figure~\ref{fig:Rwhile-concrete-syntax} and its abstract syntax is defined
+in Figure~\ref{fig:Rwhile-syntax}.
 %
 The definitional interpreter for \LangLoop{} is shown in
 Figure~\ref{fig:interp-Rwhile}. We add three new cases for \code{SetBang},
@@ -11001,7 +11001,7 @@ R^{\dagger}_8  &::=& \gray{ \PROGRAMDEFS{\code{'()}}{\Def} }
 \end{minipage}
 }
 \caption{\LangLoopANF{} is \LangLoop{} in administrative normal form (ANF).}
-\label{fig:r8-anf-syntax}
+\label{fig:Rwhile-anf-syntax}
 \end{figure}
 
 As usual, when a complex expression appears in a grammar position that
@@ -11207,7 +11207,334 @@ The \code{analyze-dataflow} function has four parameters.
 Figure~\ref{fig:Rwhile-passes} provides an overview of all the passes needed
 for the compilation of \LangLoop{}.
 
-% TODO: challenge assignment
+
+\section{Challenge: Arrays}
+\label{sec:arrays}
+
+In Chapter~\ref{ch:tuples} we studied tuples, that is, sequences of
+elements whose length is determined at compile-time and where each
+element of a tuple may have a different type (they are
+heterogeous). This challenge is also about sequences, but this time
+the length is determined at run-time and all the elements have the same
+type (they are homogeneous). We use the term ``array'' for this later
+kind of sequence.
+
+The Racket language does not distinguish between tuples and arrays,
+they are both represented by vectors. However, Typed Racket
+distinguishes between tuples and arrays: the \code{Vector} type is for
+tuples and the \code{Vectorof} type is for arrays.
+%
+Figure~\ref{fig:Rvecof-concrete-syntax} defines the concrete syntax
+for \LangArray{}, extending \LangLoop{} with the \code{Vectorof} type
+and the \code{make-vector} primitive operator for creating an array,
+whose arguments are the length of the array and an initial value for
+all the elements in the array. The \code{vector-length},
+\code{vector-ref}, and \code{vector-ref!} operators that we defined
+for tuples become overloaded for use with arrays.
+%
+We also include integer multiplication in \LangArray{}, as it is
+useful in many examples involving arrays such as computing the
+inner-product of two arrays (Figure~\ref{fig:inner-product}).
+
+
+\begin{figure}[tp]
+\centering
+\fbox{
+  \begin{minipage}{0.96\textwidth}
+    \small
+\[
+\begin{array}{lcl}
+  \Type &::=& \ldots \mid \LP \key{Vectorof}~\Type \RP \\
+  \Exp &::=& \gray{ \Int \mid \CREAD{} \mid \CNEG{\Exp}
+     \mid \CADD{\Exp}{\Exp} \mid \CSUB{\Exp}{\Exp} }  \mid \CMUL{\Exp}{\Exp}\\
+    &\mid&  \gray{ \Var \mid \CLET{\Var}{\Exp}{\Exp} }\\
+    &\mid& \gray{\key{\#t} \mid \key{\#f} 
+     \mid \LP\key{and}\;\Exp\;\Exp\RP 
+     \mid \LP\key{or}\;\Exp\;\Exp\RP 
+     \mid \LP\key{not}\;\Exp\RP } \\
+    &\mid& \gray{ \LP\key{eq?}\;\Exp\;\Exp\RP \mid \CIF{\Exp}{\Exp}{\Exp} } \\
+    &\mid& \gray{ \LP\key{vector}\;\Exp\ldots\RP \mid
+          \LP\key{vector-ref}\;\Exp\;\Int\RP} \\
+    &\mid& \gray{\LP\key{vector-set!}\;\Exp\;\Int\;\Exp\RP\mid \LP\key{void}\RP
+    \mid \LP\Exp \; \Exp\ldots\RP } \\
+    &\mid& \gray{ \LP \key{procedure-arity}~\Exp\RP 
+    \mid \CLAMBDA{\LP\LS\Var \key{:} \Type\RS\ldots\RP}{\Type}{\Exp} } \\
+  &\mid& \gray{ \CSETBANG{\Var}{\Exp}
+  \mid \CBEGIN{\Exp\ldots}{\Exp}
+  \mid \CWHILE{\Exp}{\Exp} } \\
+  &\mid& \CMAKEVEC{\Exp}{\Exp} \\
+  \Def &::=& \gray{ \CDEF{\Var}{\LS\Var \key{:} \Type\RS\ldots}{\Type}{\Exp} } \\
+  \LangArray{} &::=& \gray{\Def\ldots \; \Exp}
+\end{array}
+\]
+\end{minipage}
+}
+\caption{The concrete syntax of \LangArray{}, extending \LangLoop{} (Figure~\ref{fig:Rwhile-concrete-syntax}).}
+\label{fig:Rvecof-concrete-syntax}
+\end{figure}
+
+
+\begin{figure}[tp]
+\begin{lstlisting}
+(define (inner-product [A : (Vectorof Integer)] [B : (Vectorof Integer)]
+                       [n : Integer]) : Integer
+  (let ([i 0])
+    (let ([prod 0])
+      (begin
+        (while (< i n)
+          (begin
+            (set! prod (+ prod (* (vector-ref A i)
+                                  (vector-ref B i))))
+            (set! i (+ i 1))
+            ))
+        prod))))
+  
+
+(let ([A (make-vector 2 2)])
+  (let ([B (make-vector 2 3)])
+    (+ (inner-product A B 2)
+       30)))
+\end{lstlisting}
+\caption{Example program that computes the inner-product
+  of two arrays.}
+\label{fig:inner-product}
+\end{figure}
+
+
+The type checker for \LangArray{} is define in
+Figure~\ref{fig:type-check-Rvecof}. The result type of
+\code{make-vector} is \code{(Vectorof T)} where \code{T} is the type
+of the intializing expression.  The length expression is required to
+have type \code{Integer}. The type checking of the operators
+\code{vector-length}, \code{vector-ref}, and \code{vector-set!}  is
+updated to handle the situation where the vector has type
+\code{Vectorof}. In these cases we translate the operators to their
+\code{vectorof} form so that later passes can easily distinguish
+between operations on tuples versus arrays. We override the
+\code{operator-types} method to provide the type signature for
+multiplication: it takes two integers and returns an integer.  To
+support injection and projection of arrays to the \code{Any} type
+(Section~\ref{sec:Rany-lang}), we also override the \code{flat-ty?}
+predicate.
+
+\begin{figure}[tbp]
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
+(define type-check-Rvecof-class
+  (class type-check-Rwhile-class
+    (super-new)
+    (inherit check-type-equal?)
+
+    (define/override (flat-ty? ty)
+      (match ty
+        ['(Vectorof Any) #t]
+        [else (super flat-ty? ty)]))
+    
+    (define/override (operator-types)
+      (append '((* . ((Integer Integer) . Integer)))
+              (super operator-types)))
+    
+    (define/override (type-check-exp env)
+      (lambda (e)
+        (define recur (type-check-exp env))
+        (match e
+          [(Prim 'make-vector (list e1 e2))
+           (define-values (e1^ t1) (recur e1))
+           (define-values (e2^ elt-type) (recur e2))
+           (define vec-type `(Vectorof ,elt-type))
+           (values (HasType (Prim 'make-vector (list e1^ e2^)) vec-type)
+                   vec-type)]
+          [(Prim 'vector-ref (list e1 e2))
+           (define-values (e1^ t1) (recur e1))
+           (define-values (e2^ t2) (recur e2))
+           (match* (t1 t2)
+             [(`(Vectorof ,elt-type) 'Integer)
+              (values (Prim 'vectorof-ref (list e1^ e2^)) elt-type)]
+             [(other wise) ((super type-check-exp env) e)])]
+          [(Prim 'vector-set! (list e1 e2 e3) )
+           (define-values (e-vec t-vec) (recur e1))
+           (define-values (e2^ t2) (recur e2))
+           (define-values (e-arg^ t-arg) (recur e3))
+           (match t-vec
+             [`(Vectorof ,elt-type)
+              (check-type-equal? elt-type t-arg e)
+              (values (Prim 'vectorof-set! (list e-vec e2^ e-arg^))  'Void)]
+             [else ((super type-check-exp env) e)])]
+          [(Prim 'vector-length (list e1))
+           (define-values (e1^ t1) (recur e1))
+           (match t1
+             [`(Vectorof ,t)
+              (values (Prim 'vectorof-length (list e1^))  'Integer)]
+             [else ((super type-check-exp env) e)])]
+          [else ((super type-check-exp env) e)])))
+    ))
+
+(define (type-check-Rvecof p)
+  (send (new type-check-Rvecof-class) type-check-program p))
+\end{lstlisting}
+\caption{Type checker for the \LangArray{} language.}
+\label{fig:type-check-Rvecof}
+\end{figure}
+
+The interpreter for \LangArray{} is defined in
+Figure~\ref{fig:interp-Rvecof}.  The \code{make-vector} operator is
+implemented with Racket's \code{make-vector} function and
+multiplication is \code{fx*}, multiplication for \code{fixnum}
+integers.
+
+\begin{figure}[tbp]
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize]
+(define interp-Rvecof-class
+  (class interp-Rwhile-class
+    (super-new)
+
+    (define/override (interp-op op)
+      (verbose "Rvecof/interp-op" op)
+      (match op
+        ['make-vector make-vector]
+        ['* fx*]
+        [else (super interp-op op)]))
+    ))
+
+(define (interp-Rvecof p)
+  (send (new interp-Rvecof-class) interp-program p))
+\end{lstlisting}
+\caption{Interpreter for \LangArray{}.}
+\label{fig:interp-Rvecof}
+\end{figure}
+
+
+\subsection{Data Representation}
+\label{sec:array-rep}
+
+Just like tuples, we store arrays on the heap which means that the
+garbage collector will need to inspect arrays. An immediate thought is
+to use the same representation for arrays that we use for tuples.
+However, we limit tuples to a length of $50$ so that their length and
+pointer mask can fit into the 64-bit tag at the beginning of each
+tuple (Section~\ref{sec:data-rep-gc}). We intend arrays to allow
+millions of elements, so we need more bits to store the length.
+However, because arrays are homogeneous, we only need $1$ bit for the
+pointer mask instead of one bit per array elements.  Finally, the
+garbage collector will need to be able to distinguish between tuples
+and arrays, so we need to reserve $1$ bit for that purpose.  So we
+arrive at the following layout for the 64-bit tag at the beginning of
+an array:
+\begin{itemize}
+\item The right-most bit is the forwarding bit, just like in a tuple.
+  A $0$ indicates it is a forwarding pointer and a $1$ indicates
+  it is not.
+  
+\item The next bit to the left is the pointer mask. A $0$ indicates
+  that none of the elements are pointers to the heap and a $1$
+  indicates that all of the elements are pointers.
+
+\item The next $61$ bits store the length of the array.
+
+\item The left-most bit distinguishes between a tuple ($0$) versus an
+  array ($1$).
+\end{itemize}
+
+
+Recall that in Chapter~\ref{ch:type-dynamic}, we use a $3$-bit tag to
+differentiate the kinds of values that have been injected into the
+\code{Any} type. We use the bit pattern \code{110} (or $6$ in decimal)
+to indicate that the value is an array.
+
+In the following subsections we provide hints regarding how to update
+the passes to handle arrays.
+
+
+\subsection{Reveal Casts}
+
+The array-access operators \code{vectorof-ref} and
+\code{vectorof-set!} are similar to the \code{any-vector-ref} and
+\code{any-vector-set!} operators of Chapter~\ref{ch:type-dynamic} in
+that the type checker cannot tell whether the index will be in bounds,
+so the bounds check must be performed at run time.  Recall that the
+\code{reveal-casts} pass (Section~\ref{sec:reveal-casts-Rany}) wraps
+an \code{If} arround a vector reference for update to check whether
+the index is less than the length.  You should do the same for
+\code{vectorof-ref} and \code{vectorof-set!} .
+
+In addition, the handling of the \code{any-vector} operators in
+\code{reveal-casts} needs to be updated to account for arrays that are
+injected to \code{Any}. For the \code{any-vector-length} operator, the
+generated code should test whether the tag is for tuples (\code{010})
+or arrays (\code{110}) and then dispatch to either
+\code{any-vector-length} or \code{any-vectorof-length}.  For the later
+we add a case in \code{select-instructions} to generate the
+appropriate instructions for accessing the array length from the
+header of an array.
+
+For the \code{any-vector-ref} and \code{any-vector-set!} operators,
+the generated code needs to check that the index is less than the
+vector length, so like the code for \code{any-vector-length}, check
+the tag to determine whether to use \code{any-vector-length} or
+\code{any-vectorof-length} for this purpose.  Once the bounds checking
+is complete, the generated code can use \code{any-vector-ref} and
+\code{any-vector-set!} for both tuples and arrays because the
+instructions used for those operators do not look at the tag at the
+front of the tuple or array.
+
+\subsection{Expose Allocation}
+
+This pass should translate the \code{make-vector} operator into
+lower-level operations. In particular, the new AST node
+$\LP\key{AllocateArray}~\Exp~\Type\RP$ allocates an array of the
+length specified by the $\Exp$, but does not initialize the elements
+of the array. (Analogous to the \code{Allocate} AST node for tuples.)
+The $\Type$ argument must be $\LP\key{Vectorof}~T\RP$ where $T$ is the
+element type for the array. Regarding the initialization of the array,
+we recommend generated a \code{while} loop that uses
+\code{vector-set!} to put the initializing value into every element of
+the array.
+
+\subsection{Remove Complex Operands}
+
+Add cases in the \code{rco-atom} and \code{rco-exp} for
+\code{AllocateArray}. In particular, an \code{AllocateArray} node is
+complex and its subexpression must be atomic.
+
+\subsection{Explicate Control}
+
+Add cases for \code{AllocateArray} to \code{explicate-tail} and
+\code{explicate-assign}.
+
+\subsection{Select Instructions}
+
+Generate instructions for \code{AllocateArray} similar to those for
+\code{Allocate} in Section~\ref{sec:select-instructions-gc} except
+that the tag at the front of the array should instead use the
+representation discussed in Section~\ref{sec:array-rep}.
+
+Regarding \code{vectorof-length}, extract the length from the tag
+according to the representation discussed in
+Section~\ref{sec:array-rep}.
+
+The instructions generated for \code{vectorof-ref} differ from those
+for \code{vector-ref} (Section~\ref{sec:select-instructions-gc}) in
+that the index is not a constant so the offset must be computed at
+runtime, similar to the instructions generated for
+\code{any-vector-of-ref} (Section~\ref{sec:select-Rany}).  The same is
+true for \code{vectorof-set!}.  Also, the \code{vectorof-set!} may
+appear in an assignment and as a stand-alone statement, so make sure
+to handle both situations in this pass.
+
+Finally, the instructions for \code{any-vectorof-length} should be
+similar to those for \code{vectorof-length}, except that one must
+first project the array by writing zeroes into the $3$-bit tag
+
+\begin{exercise}\normalfont
+
+Implement a compiler for the \LangArray{} language by extending your
+compiler for \LangLoop{}. Test your compiler on a half dozen new
+programs, including the one in Figure~\ref{fig:inner-product} and also
+a program that multiplies two matrices. Note that matrices are
+2-dimensional arrays, but those can be encoded into 1-dimensional
+arrays by laying out each row in the array, one after the next.
+  
+\end{exercise}
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \chapter{Gradual Typing}
@@ -11227,8 +11554,8 @@ adding or removing type annotations on parameters and
 variables~\citep{Anderson:2002kd,Siek:2006bh}.
 %
 The concrete syntax of \LangGrad{} is defined in
-Figure~\ref{fig:r9-concrete-syntax} and its abstract syntax is defined
-in Figure~\ref{fig:r9-syntax}. The main syntactic difference between
+Figure~\ref{fig:Rgrad-concrete-syntax} and its abstract syntax is defined
+in Figure~\ref{fig:Rgrad-syntax}. The main syntactic difference between
 \LangLoop{} and \LangGrad{} is the additional \itm{param} and \itm{ret}
 non-terminals that make type annotations optional. The return types
 are not optional in the abstract syntax; the parser fills in
@@ -11267,8 +11594,8 @@ syntax.
 \]
 \end{minipage}
 }
-\caption{The concrete syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:r8-concrete-syntax}).}
-\label{fig:r9-concrete-syntax}
+\caption{The concrete syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:Rwhile-concrete-syntax}).}
+\label{fig:Rgrad-concrete-syntax}
 \end{figure}
 
 \begin{figure}[tp]
@@ -11294,8 +11621,8 @@ syntax.
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:r8-syntax}).}
-\label{fig:r9-syntax}
+\caption{The abstract syntax of \LangGrad{}, extending \LangLoop{} (Figure~\ref{fig:Rwhile-syntax}).}
+\label{fig:Rgrad-syntax}
 \end{figure}
 
 
@@ -11385,7 +11712,7 @@ types, such as the \code{(Integer -> Integer)} annotation on parameter
 new \code{Cast} form that is inserted by the type checker.  Thus, the
 output of the type checker is a program in the \LangCast{} language, which
 adds \code{Cast} to \LangLoop{}, as shown in
-Figure~\ref{fig:r9-prime-syntax}.
+Figure~\ref{fig:Rgrad-prime-syntax}.
 
 \begin{figure}[tp]
 \centering
@@ -11400,8 +11727,8 @@ Figure~\ref{fig:r9-prime-syntax}.
 \]
 \end{minipage}
 }
-\caption{The abstract syntax of \LangCast{}, extending \LangLoop{} (Figure~\ref{fig:r8-syntax}).}
-\label{fig:r9-prime-syntax}
+\caption{The abstract syntax of \LangCast{}, extending \LangLoop{} (Figure~\ref{fig:Rwhile-syntax}).}
+\label{fig:Rgrad-prime-syntax}
 \end{figure}
 
 
@@ -12134,7 +12461,7 @@ before the \code{vector-ref}.
 \label{sec:reveal-casts-gradual}
 
 Recall that the \code{reveal-casts} pass
-(Section~\ref{sec:reveal-casts-r6}) is responsible for lowering
+(Section~\ref{sec:reveal-casts-Rany}) is responsible for lowering
 \code{Inject} and \code{Project} into lower-level operations.  In
 particular, \code{Project} turns into a conditional expression that
 inspects the tag and retrieves the underlying value.  Here we need to
@@ -12229,7 +12556,7 @@ We have another batch of vector operations to deal with, those for the
 \code{any-vector-ref} when there is a \code{vector-ref} on something
 of type \code{Any}, and similarly for \code{any-vector-set!}  and
 \code{any-vector-length} (Figure~\ref{fig:type-check-Rgradual-1}). In
-Section~\ref{sec:select-r6} we selected instructions for these
+Section~\ref{sec:select-Rany} we selected instructions for these
 operations based on the idea that the underlying value was a real
 vector. But in the current setting, the underlying value is of type
 \code{PVector}. So \code{any-vector-ref} can be translates to
@@ -12418,8 +12745,8 @@ vector of Booleans (and a function on Booleans).
 \label{fig:map-vec-poly}
 \end{figure}
 
-Figure~\ref{fig:r10-concrete-syntax} defines the concrete syntax of
-\LangPoly{} and Figure~\ref{fig:r10-syntax} defines the abstract
+Figure~\ref{fig:Rpoly-concrete-syntax} defines the concrete syntax of
+\LangPoly{} and Figure~\ref{fig:Rpoly-syntax} defines the abstract
 syntax. We add a second form for function definitions in which a type
 declaration comes before the \code{define}. In the abstract syntax,
 the return type in the \code{Def} is \code{Any}, but that should be
@@ -12447,8 +12774,8 @@ polymorphic types and type variables.
 \end{minipage}
 }
 \caption{The concrete syntax of \LangPoly{}, extending \LangLoop{}
-    (Figure~\ref{fig:r8-concrete-syntax}).}
-\label{fig:r10-concrete-syntax}
+    (Figure~\ref{fig:Rwhile-concrete-syntax}).}
+\label{fig:Rpoly-concrete-syntax}
 \end{figure}
 
 \begin{figure}[tp]
@@ -12468,8 +12795,8 @@ polymorphic types and type variables.
 \end{minipage}
 }
 \caption{The abstract syntax of \LangPoly{}, extending \LangLoop{}
-    (Figure~\ref{fig:r8-syntax}).}
-\label{fig:r10-syntax}
+    (Figure~\ref{fig:Rwhile-syntax}).}
+\label{fig:Rpoly-syntax}
 \end{figure}
 
 By including polymorphic types in the $\Type$ non-terminal we choose
@@ -12544,7 +12871,7 @@ Figure~\ref{fig:well-formed-types} recursively inspects a type, making
 sure that each type variable has been defined.
 
 The output language of the type checker is \LangInst{}, defined in
-Figure~\ref{fig:r10-prime-syntax}. The type checker combines the type
+Figure~\ref{fig:Rpoly-prime-syntax}. The type checker combines the type
 declaration and polymorphic function into a single definition, using
 the \code{Poly} form, to make polymorphic functions more convenient to
 process in next pass of the compiler.
@@ -12566,8 +12893,8 @@ process in next pass of the compiler.
 \end{minipage}
 }
 \caption{The abstract syntax of \LangInst{}, extending \LangLoop{}
-    (Figure~\ref{fig:r8-syntax}).}
-\label{fig:r10-prime-syntax}
+    (Figure~\ref{fig:Rwhile-syntax}).}
+\label{fig:Rpoly-prime-syntax}
 \end{figure}
 
 The output of the type checker on the polymorphic \code{map-vec}
@@ -13193,7 +13520,7 @@ registers.
 \section{Concrete Syntax for Intermediate Languages}
 
 The concrete syntax of \LangAny{} is defined in
-Figure~\ref{fig:r6-concrete-syntax}.
+Figure~\ref{fig:Rany-concrete-syntax}.
 
 \begin{figure}[tp]
 \centering
@@ -13222,7 +13549,7 @@ Figure~\ref{fig:r6-concrete-syntax}.
 }
 \caption{The concrete syntax of \LangAny{}, extending \LangLam{}
   (Figure~\ref{fig:Rlam-syntax}) with \key{Any}.}
-\label{fig:r6-concrete-syntax}
+\label{fig:Rany-concrete-syntax}
 \end{figure}
 
 The concrete syntax for \LangCVar{}, \LangCIf{}, \LangCVec{} and \LangCFun{} is

defs.tex

@@ -8,6 +8,7 @@
 \newcommand{\LangCIf}{\ensuremath{C_{\ttm{If}}}} %C1
 \newcommand{\LangIfANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{if}}}} %R2
 \newcommand{\LangVec}{\ensuremath{R_{\ttm{Vec}}}} %R3
+\newcommand{\LangStruct}{\ensuremath{R^{\ttm{Struct}}_{\ttm{Vec}}}} %R^s3
 \newcommand{\LangCVec}{\ensuremath{C_{\ttm{Vec}}}} %C2
 \newcommand{\LangVecANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{Vec}}}} %R3
 \newcommand{\LangAlloc}{\ensuremath{R_{\ttm{Alloc}}}} %R3'
@@ -29,6 +30,7 @@
 \newcommand{\LangLoopAlloc}{\ensuremath{R^{\ttm{Alloc}}_{\ttm{While}}}} %R'8
 \newcommand{\LangCLoop}{\ensuremath{C_{\circlearrowleft}}} %C7
 \newcommand{\LangLoopANF}{\ensuremath{R^{\mathsf{ANF}}_{\ttm{While}}}} %R8
+\newcommand{\LangArray}{\ensuremath{R^{\ttm{Vecof}}_{\ttm{While}}}} %R^s3
 \newcommand{\LangGrad}{\ensuremath{R_{\ttm{?}}}} %R9
 \newcommand{\LangCast}{\ensuremath{R_{\ttm{cast}}}} %R9'
 \newcommand{\LangProxy}{\ensuremath{R_{\ttm{proxy}}}} %R8''
@@ -89,11 +91,13 @@
 \newcommand{\PROGRAMDEFS}[2]{\code{(ProgramDefs}~#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{\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}
 \newcommand{\CBEGIN}[2]{\LP\key{begin}~#1~#2\RP}
+\newcommand{\CMAKEVEC}[2]{\LP\key{make-vector}~#1~#2\RP}
 \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}