浏览代码

finished draft of gradual

Jeremy Siek 3 年之前
父节点
当前提交
ed54729c01
共有 3 个文件被更改,包括 420 次插入123 次删除
  1. 1 0
      TimesAPriori_MIT.cls
  2. 394 119
      book.tex
  3. 25 4
      defs.tex

+ 1 - 0
TimesAPriori_MIT.cls

@@ -1823,6 +1823,7 @@ Chapter \arabic{chapter}}%
 \thickmuskip=3mu%
 \thickmuskip=3mu%
 }%
 }%
 
 
+\RequirePackage{multind} % has to be loaded before hyperref for links in index. -Jeremy
 \RequirePackage[bookmarks=true,bookmarksnumbered=true,bookmarksopenlevel=1,colorlinks=false,breaklinks,linkcolor=black,citecolor=black,urlcolor=black,hidelinks]{hyperref}%
 \RequirePackage[bookmarks=true,bookmarksnumbered=true,bookmarksopenlevel=1,colorlinks=false,breaklinks,linkcolor=black,citecolor=black,urlcolor=black,hidelinks]{hyperref}%
 \ifxetex\relax\else\usepackage{breakurl}\fi%
 \ifxetex\relax\else\usepackage{breakurl}\fi%
 %\ifluatex\relax\else\usepackage{breakurl}\fi%
 %\ifluatex\relax\else\usepackage{breakurl}\fi%

+ 394 - 119
book.tex

@@ -37,7 +37,7 @@
 \newcommand{\python}[1]{{\if\edition\pythonEd #1\fi}}
 \newcommand{\python}[1]{{\if\edition\pythonEd #1\fi}}
 
 
 %% For multiple indices:
 %% For multiple indices:
-\usepackage{multind}
+%\usepackage{multind}  moved this to the file TimesAPriori_MIT.cls. -Jeremy
 \makeindex{subject}
 \makeindex{subject}
 %\makeindex{authors}
 %\makeindex{authors}
 
 
@@ -489,9 +489,8 @@ called \emph{concrete syntax}. We use concrete syntax to concisely
 write down and talk about programs. Inside the compiler, we use
 write down and talk about programs. Inside the compiler, we use
 \emph{abstract syntax trees} (ASTs) to represent programs in a way
 \emph{abstract syntax trees} (ASTs) to represent programs in a way
 that efficiently supports the operations that the compiler needs to
 that efficiently supports the operations that the compiler needs to
-perform.\index{subject}{concrete syntax}\index{subject}{abstract syntax}\index{subject}{abstract
-  syntax tree}\index{subject}{AST}\index{subject}{program}\index{subject}{parse} The translation
-from concrete syntax to abstract syntax is a process called
+perform.\index{subject}{concrete syntax}\index{subject}{abstract syntax}\index{subject}{abstract syntax tree}\index{subject}{AST}\index{subject}{program}\index{subject}{parse}
+The translation from concrete syntax to abstract syntax is a process called
 \emph{parsing}~\citep{Aho:2006wb}. We do not cover the theory and
 \emph{parsing}~\citep{Aho:2006wb}. We do not cover the theory and
 implementation of parsing in this book.
 implementation of parsing in this book.
 %
 %
@@ -679,7 +678,8 @@ by using a single structure.
 
 
 {\if\edition\pythonEd
 {\if\edition\pythonEd
 We use a Python \code{class} for each kind of node.
 We use a Python \code{class} for each kind of node.
-The following is the class definition for constants.
+The following is the class definition for
+constants.
 \begin{lstlisting}
 \begin{lstlisting}
 class Constant:
 class Constant:
     def __init__(self, value):
     def __init__(self, value):
@@ -701,8 +701,8 @@ class UnaryOp:
         self.operand = operand
         self.operand = operand
 \end{lstlisting}
 \end{lstlisting}
 The specific operation is specified by the \code{op} parameter.  For
 The specific operation is specified by the \code{op} parameter.  For
-example, the class \code{USub} is for unary subtraction. (More unary
-operators are introduced in later chapters.) To create an AST that
+example, the class \code{USub} is for unary subtraction.
+(More unary operators are introduced in later chapters.) To create an AST that
 negates the number $8$, we write the following.
 negates the number $8$, we write the following.
 \begin{lstlisting}
 \begin{lstlisting}
 neg_eight = UnaryOp(USub(), eight)
 neg_eight = UnaryOp(USub(), eight)
@@ -736,8 +736,8 @@ class BinOp:
 \end{lstlisting}
 \end{lstlisting}
 Similar to \code{UnaryOp}, the specific operation is specified by the
 Similar to \code{UnaryOp}, the specific operation is specified by the
 \code{op} parameter, which for now is just an instance of the
 \code{op} parameter, which for now is just an instance of the
-\code{Add} class. So to create the AST node that adds negative eight
-to some user input, we write the following.
+\code{Add} class. So to create the AST
+node that adds negative eight to some user input, we write the following.
 \begin{lstlisting}
 \begin{lstlisting}
 ast1_1 = BinOp(read, Add(), neg_eight)
 ast1_1 = BinOp(read, Add(), neg_eight)
 \end{lstlisting}
 \end{lstlisting}
@@ -758,7 +758,7 @@ programs as abstract syntax trees.
 \label{sec:grammar}
 \label{sec:grammar}
 \index{subject}{integer}
 \index{subject}{integer}
 \index{subject}{literal}
 \index{subject}{literal}
-\index{subject}{constant}
+%\index{subject}{constant}
 
 
 A programming language can be thought of as a \emph{set} of programs.
 A programming language can be thought of as a \emph{set} of programs.
 The set is typically infinite (one can always create larger and larger
 The set is typically infinite (one can always create larger and larger
@@ -1011,6 +1011,20 @@ defined in Figure~\ref{fig:r0-concrete-syntax}.
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
+\python{
+  \index{subject}{Constant@\texttt{Constant}}
+  \index{subject}{UnaryOp@\texttt{UnaryOp}}
+  \index{subject}{USub@\texttt{USub}}
+  \index{subject}{inputint@\texttt{input\_int}}
+  \index{subject}{Call@\texttt{Call}}
+  \index{subject}{Name@\texttt{Name}}  
+  \index{subject}{BinOp@\texttt{BinOp}}
+  \index{subject}{Add@\texttt{Add}}
+  \index{subject}{Sub@\texttt{Sub}}
+  \index{subject}{print@\texttt{print}}
+  \index{subject}{Expr@\texttt{Expr}}
+  \index{subject}{Module@\texttt{Module}}
+}
 \caption{The abstract syntax of \LangInt{}.}
 \caption{The abstract syntax of \LangInt{}.}
 \label{fig:r0-syntax}
 \label{fig:r0-syntax}
 \end{figure}
 \end{figure}
@@ -1850,7 +1864,7 @@ The \LangVar{} language includes assignment statements, which define a
 variable for use in later statements and initializes the variable with
 variable for use in later statements and initializes the variable with
 the value of an expression.  The abstract syntax for assignment is
 the value of an expression.  The abstract syntax for assignment is
 defined in Figure~\ref{fig:Lvar-syntax}.  The concrete syntax for
 defined in Figure~\ref{fig:Lvar-syntax}.  The concrete syntax for
-assignment is
+assignment is \index{subject}{Assign@\texttt{Assign}}
 \begin{lstlisting}
 \begin{lstlisting}
 |$\itm{var}$| = |$\itm{exp}$|
 |$\itm{var}$| = |$\itm{exp}$|
 \end{lstlisting}
 \end{lstlisting}
@@ -2862,7 +2876,7 @@ that uses a reserved register to fix outstanding problems.
 \fi}
 \fi}
 
 
 {\if\edition\pythonEd
 {\if\edition\pythonEd
-\begin{tikzpicture}[baseline=(current  bounding  box.center)]
+\begin{tikzpicture}[baseline=(current  bounding  box.center),scale=0.90]
 \node (Lvar) at (0,2)  {\large \LangVar{}};
 \node (Lvar) at (0,2)  {\large \LangVar{}};
 \node (Lvar-2) at (3,2)  {\large \LangVarANF{}};
 \node (Lvar-2) at (3,2)  {\large \LangVarANF{}};
 \node (x86-1) at (3,0)  {\large \LangXVar{}};
 \node (x86-1) at (3,0)  {\large \LangXVar{}};
@@ -6649,8 +6663,9 @@ The concrete and abstract syntax of the \LangIf{} language are defined in
 Figures~\ref{fig:Lif-concrete-syntax} and~\ref{fig:Lif-syntax},
 Figures~\ref{fig:Lif-concrete-syntax} and~\ref{fig:Lif-syntax},
 respectively. The \LangIf{} language includes all of 
 respectively. The \LangIf{} language includes all of 
 \LangVar{} {(shown in gray)}, the Boolean literals \TRUE{} and
 \LangVar{} {(shown in gray)}, the Boolean literals \TRUE{} and
-\FALSE{},\racket{ and} the \code{if} expression\python{, and the
-  \code{if}  statement}. We expand the set of operators to include
+\FALSE{}, \racket{and} the \code{if} expression%
+\python{, and the \code{if}  statement}.
+We expand the set of operators to include
 \begin{enumerate}
 \begin{enumerate}
 \item the logical operators \key{and}, \key{or}, and \key{not},
 \item the logical operators \key{and}, \key{or}, and \key{not},
 \item the \racket{\key{eq?} operation}\python{\key{==} and \key{!=} operations}
 \item the \racket{\key{eq?} operation}\python{\key{==} and \key{!=} operations}
@@ -6753,7 +6768,7 @@ respectively. The \LangIf{} language includes all of
 \end{figure}
 \end{figure}
 
 
 \begin{figure}[tp]
 \begin{figure}[tp]
-\begin{minipage}{0.66\textwidth}
+%\begin{minipage}{0.66\textwidth}
 \begin{tcolorbox}[colback=white]
 \begin{tcolorbox}[colback=white]
 \centering
 \centering
 {\if\edition\racketEd    
 {\if\edition\racketEd    
@@ -6781,7 +6796,29 @@ respectively. The \LangIf{} language includes all of
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
-\end{minipage}
+%\end{minipage}
+\index{subject}{True@\TRUE{}}\index{subject}{False@\FALSE{}}
+\index{subject}{IfExp@\IFNAME{}}
+\python{\index{subject}{IfStmt@\IFSTMTNAME{}}}
+\index{subject}{and@\ANDNAME{}}
+\index{subject}{or@\ORNAME{}}
+\index{subject}{not@\NOTNAME{}}
+\index{subject}{equal@\EQNAME{}}
+  \python{\index{subject}{not equal@\NOTEQNAME{}}}
+  \racket{
+    \index{subject}{lessthan@\texttt{<}}
+    \index{subject}{lessthaneq@\texttt{<=}}
+    \index{subject}{greaterthan@\texttt{>}}
+    \index{subject}{greaterthaneq@\texttt{>=}}
+  }
+\python{
+  \index{subject}{BoolOp@\texttt{BoolOp}}
+  \index{subject}{Compare@\texttt{Compare}}
+  \index{subject}{Lt@\texttt{Lt}}
+  \index{subject}{LtE@\texttt{LtE}}
+  \index{subject}{Gt@\texttt{Gt}}
+  \index{subject}{GtE@\texttt{GtE}}
+}
 \caption{The abstract syntax of \LangIf{}.}
 \caption{The abstract syntax of \LangIf{}.}
 \label{fig:Lif-syntax}
 \label{fig:Lif-syntax}
 \end{figure}
 \end{figure}
@@ -7464,8 +7501,8 @@ in Figure~\ref{fig:c1-syntax}.
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
-\caption{The concrete syntax of the \LangCIf{} intermediate language,
-  an extension of \LangCVar{} (Figure~\ref{fig:c0-concrete-syntax}).}
+\caption{The concrete syntax of the \LangCIf{} intermediate language%
+  \racket{, an extension of \LangCVar{} (Figure~\ref{fig:c0-concrete-syntax})}.}
 \label{fig:c1-concrete-syntax}
 \label{fig:c1-concrete-syntax}
 \end{figure}
 \end{figure}
 
 
@@ -7494,6 +7531,11 @@ in Figure~\ref{fig:c1-syntax}.
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
+\racket{
+  \index{subject}{IfStmt@\IFSTMTNAME{}}
+}
+\index{subject}{Goto@\texttt{Goto}}
+\index{subject}{Return@\texttt{Return}}
 \caption{The abstract syntax of \LangCIf{}\racket{, an extension of \LangCVar{}
 \caption{The abstract syntax of \LangCIf{}\racket{, an extension of \LangCVar{}
   (Figure~\ref{fig:c0-syntax})}.}
   (Figure~\ref{fig:c0-syntax})}.}
 \label{fig:c1-syntax}
 \label{fig:c1-syntax}
@@ -7825,6 +7867,7 @@ upcoming \code{explicate\_control} pass.
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
+\python{\index{subject}{Begin@\texttt{Begin}}}
 \caption{\LangIfANF{} is \LangIf{} in monadic normal form
 \caption{\LangIfANF{} is \LangIf{} in monadic normal form
   (extends \LangVarANF in Figure~\ref{fig:Lvar-anf-syntax}).}
   (extends \LangVarANF in Figure~\ref{fig:Lvar-anf-syntax}).}
 \label{fig:Lif-anf-syntax}
 \label{fig:Lif-anf-syntax}
@@ -9183,7 +9226,7 @@ conclusion:
 \end{tikzpicture}
 \end{tikzpicture}
 \fi}
 \fi}
 {\if\edition\pythonEd
 {\if\edition\pythonEd
-\begin{tikzpicture}[baseline=(current  bounding  box.center)]
+\begin{tikzpicture}[baseline=(current  bounding  box.center),scale=0.90]
 \node (Lif-1) at (0,2)  {\large \LangIf{}};
 \node (Lif-1) at (0,2)  {\large \LangIf{}};
 \node (Lif-2) at (3,2)  {\large \LangIf{}};
 \node (Lif-2) at (3,2)  {\large \LangIf{}};
 \node (Lif-3) at (6,2)  {\large \LangIfANF{}};
 \node (Lif-3) at (6,2)  {\large \LangIfANF{}};
@@ -9897,7 +9940,9 @@ the condition remains true.
 \]
 \]
 \fi}
 \fi}
 \end{tcolorbox}
 \end{tcolorbox}
-
+\python{
+  \index{subject}{While@\texttt{While}}
+  }
 \caption{The abstract syntax of \LangLoop{}, extending \LangIf{} (Figure~\ref{fig:Lif-syntax}).}
 \caption{The abstract syntax of \LangLoop{}, extending \LangIf{} (Figure~\ref{fig:Lif-syntax}).}
 \label{fig:Lwhile-syntax}
 \label{fig:Lwhile-syntax}
 \end{figure}
 \end{figure}
@@ -10384,7 +10429,8 @@ def analyze_dataflow(G, transfer, bottom, join):
     worklist = deque(G.vertices)
     worklist = deque(G.vertices)
     while worklist:
     while worklist:
         node = worklist.pop()
         node = worklist.pop()
-        input = reduce(join, [mapping[v] for v in trans_G.adjacent(node)], bottom)
+        inputs = [mapping[v] for v in trans_G.adjacent(node)]
+        input = reduce(join, inputs, bottom)
         output = transfer(node, input)
         output = transfer(node, input)
         if output != mapping[node]:
         if output != mapping[node]:
             mapping[node] = output
             mapping[node] = output
@@ -10939,7 +10985,7 @@ indefinite, that is, a tuple lives forever from the programmer's
 viewpoint. Of course, from an implementer's viewpoint, it is important
 viewpoint. Of course, from an implementer's viewpoint, it is important
 to reclaim the space associated with a tuple when it is no longer
 to reclaim the space associated with a tuple when it is no longer
 needed, which is why we also study \emph{garbage collection}
 needed, which is why we also study \emph{garbage collection}
-\index{garbage collection} techniques in this chapter.
+\index{subject}{garbage collection} techniques in this chapter.
 
 
 Section~\ref{sec:r3} introduces the \LangVec{} language including its
 Section~\ref{sec:r3} introduces the \LangVec{} language including its
 interpreter and type checker. The \LangVec{} language extends the \LangLoop{}
 interpreter and type checker. The \LangVec{} language extends the \LangLoop{}
@@ -20098,33 +20144,42 @@ def main() -> int:
 \section{Differentiate Proxies}
 \section{Differentiate Proxies}
 \label{sec:differentiate-proxies}
 \label{sec:differentiate-proxies}
 
 
-So far the job of differentiating tuples and tuple proxies has been
-the job of the interpreter.
-\racket{For example, the interpreter for \LangCast{}
-implements \code{vector-ref} using the \code{guarded-vector-ref}
-function in Figure~\ref{fig:guarded-tuple}.}
+So far the responsibility of differentiating tuples and tuple proxies
+has been the job of the interpreter.
+%
+\racket{For example, the interpreter for \LangCast{} implements
+  \code{vector-ref} using the \code{guarded-vector-ref} function in
+  Figure~\ref{fig:guarded-tuple}.}
+%
 In the \code{differentiate\_proxies} pass we shift this responsibility
 In the \code{differentiate\_proxies} pass we shift this responsibility
 to the generated code.
 to the generated code.
 
 
-We begin by designing the output language \LangPVec.  In \LangGrad{}
-we used the type \racket{\code{Vector}}\python{\code{tuple}} for both
-real tuples and tuple proxies\python{ and similarly for \code{list} types}.
-In \LangPVec we return the
-\racket{\code{Vector}}\python{\code{tuple}} type to its original
-meaning, as the type of real tuples, and we introduce a new type,
-\racket{\code{PVector}}\python{\code{ProxyOrTupleType}}, whose values
+We begin by designing the output language \LangPVec{}.  In \LangGrad{}
+we used the type \TUPLETYPENAME{} for both
+real tuples and tuple proxies.
+\python{Similarly, we use the type \code{list} for both arrays and
+array proxies.}
+In \LangPVec{} we return the
+\TUPLETYPENAME{} type to its original
+meaning, as the type of just tuples, and we introduce a new type,
+\PTUPLETYNAME{}, whose values
 can be either real tuples or tuple
 can be either real tuples or tuple
-proxies. 
-for creating and using values of type \code{PVector}.
-This new type comes with a suite of new primitive operations
-%We don't need to introduce a new type to represent tuple proxies.
-A proxy is represented by a tuple containing three things: 1) the
+proxies.
+Likewise, we return the
+\ARRAYTYPENAME{} type to its original
+meaning, as the type of arrays, and we introduce a new type,
+\PARRAYTYNAME{}, whose values
+can be either arrays or array proxies.
+These new types come with a suite of new primitive operations
+
+{\if\edition\racketEd    
+A tuple proxy is represented by a tuple containing three things: 1) the
 underlying tuple, 2) a tuple of functions for casting elements that
 underlying tuple, 2) a tuple of functions for casting elements that
 are read from the tuple, and 3) a tuple of functions for casting
 are read from the tuple, and 3) a tuple of functions for casting
 values to be written to the tuple. So we define the following
 values to be written to the tuple. So we define the following
 abbreviation for the type of a tuple proxy:
 abbreviation for the type of a tuple proxy:
 \[
 \[
-\itm{Proxy} (T\ldots \Rightarrow T'\ldots)
+\itm{TupleProxy} (T\ldots \Rightarrow T'\ldots)
 = (\ttm{Vector}~\PTUPLETY{T\ldots} ~R~ W) \to \PTUPLETY{T' \ldots})
 = (\ttm{Vector}~\PTUPLETY{T\ldots} ~R~ W) \to \PTUPLETY{T' \ldots})
 \]
 \]
 where $R = (\ttm{Vector}~(T\to T') \ldots)$ and
 where $R = (\ttm{Vector}~(T\to T') \ldots)$ and
@@ -20137,7 +20192,7 @@ Next we describe each of the new primitive operations.
   (\key{PVector} $T \ldots$)]\ \\
   (\key{PVector} $T \ldots$)]\ \\
 %
 %
   This operation brands a vector as a value of the \code{PVector} type.
   This operation brands a vector as a value of the \code{PVector} type.
-\item[\code{inject-proxy} : $\itm{Proxy}(T\ldots \Rightarrow T'\ldots)$
+\item[\code{inject-proxy} : $\itm{TupleProxy}(T\ldots \Rightarrow T'\ldots)$
   $\to$ (\key{PVector} $T' \ldots$)]\ \\
   $\to$ (\key{PVector} $T' \ldots$)]\ \\
 %
 %
   This operation brands a vector proxy as value of the \code{PVector} type.
   This operation brands a vector proxy as value of the \code{PVector} type.
@@ -20168,42 +20223,140 @@ Next we describe each of the new primitive operations.
   Given a tuple proxy, this operation writes a value to the $i$th element
   Given a tuple proxy, this operation writes a value to the $i$th element
   of the tuple.
   of the tuple.
 \end{description}
 \end{description}
+\fi}
 
 
-\python{
-  Similarly, we introduce the \code{ProxyOrListType} for arrays.
-  UNDER CONSTRUCTION
-}
+{\if\edition\pythonEd
+
+A tuple proxy is represented by a tuple containing 1) the underlying
+tuple and 2) a tuple of functions for casting elements that are read
+from the tuple. The \LangPVec{} language includes the following AST
+classes and primitive functions.
+
+\begin{description}
+\item[\code{InjectTuple}] \ \\
+%
+  This AST node brands a tuple as a value of the \PTUPLETYNAME{} type.
+\item[\code{InjectTupleProxy}]\ \\
+%
+  This AST node brands a tuple proxy as value of the \PTUPLETYNAME{} type.
+\item[\code{is\_tuple\_proxy}]\ \\
+%
+  This primitive returns true if the value is a tuple proxy and false
+  if it is a tuple.
+\item[\code{project\_tuple}]\ \\
+%
+  Converts a tuple that is branded as \PTUPLETYNAME{}
+  back to a tuple.
+  
+\item[\code{proxy\_tuple\_len}]\ \\
+%
+  Given a tuple proxy, returns the length of the underlying tuple.
+  
+\item[\code{proxy\_tuple\_load}]\ \\
+%
+  Given a tuple proxy, returns the $i$th element of the underlying
+  tuple.
+  
+\end{description}
+
+An array proxy is represented by a tuple containing 1) the underlying
+array, 2) a function for casting elements that are read from the
+array, and 3) a function for casting elements that are written to the
+array.  The \LangPVec{} language includes the following AST classes
+and primitive functions.
+
+\begin{description}
+\item[\code{InjectList}]\ \\
+  This AST node brands an array as a value of the \PARRAYTYNAME{} type.
 
 
-Now to discuss the translation that differentiates tuples from
-proxies. First, every type annotation in the program is translated
-(recursively) to replace \code{Vector} with \code{PVector}.  Next, we
-insert uses of \code{PVector} operations in the appropriate
+\item[\code{InjectListProxy}]\ \\
+%
+  This AST node brands a array proxy as value of the \PARRAYTYNAME{} type.
+\item[\code{is\_array\_proxy}]\ \\
+%
+  Returns true if the value is a array proxy and false if it is an
+  array.
+\item[\code{project\_array}]\ \\
+%
+  Converts an array that is branded as \PARRAYTYNAME{} back to an
+  array.
+  
+\item[\code{proxy\_array\_len}]\ \\
+%
+  Given a array proxy, returns the length of the underlying array.
+  
+\item[\code{proxy\_array\_load}]\ \\
+%
+  Given a array proxy, returns the $i$th element of the underlying
+  array.
+
+\item[\code{proxy\_array\_store}]\ \\
+%  
+    Given an array proxy, writes a value to the $i$th element of the
+    underlying array.
+\end{description}
+
+\fi}
+
+Now to discuss the translation that differentiates tuples and arrays
+from proxies. First, every type annotation in the program is
+translated (recursively) to replace \TUPLETYPENAME{} with \PTUPLETYNAME{}.
+Next, we insert uses of \PTUPLETYNAME{} operations in the appropriate
 places. For example, we wrap every tuple creation with an
 places. For example, we wrap every tuple creation with an
-\code{inject-vector}.
+\racket{\code{inject-vector}}\python{\code{InjectTupleProxy}}.
+{\if\edition\racketEd    
 \begin{lstlisting}
 \begin{lstlisting}
 (vector |$e_1 \ldots e_n$|)
 (vector |$e_1 \ldots e_n$|)
 |$\Rightarrow$|
 |$\Rightarrow$|
 (inject-vector (vector |$e'_1 \ldots e'_n$|))
 (inject-vector (vector |$e'_1 \ldots e'_n$|))
 \end{lstlisting}
 \end{lstlisting}
-The \code{raw-vector} operator that we introduced in the previous
+\fi}
+{\if\edition\pythonEd    
+\begin{lstlisting}
+Tuple(|$e_1, \ldots, e_n$|)
+|$\Rightarrow$|
+InjectTuple(Tuple(|$e'_1, \ldots, e'_n$|))
+\end{lstlisting}
+\fi}
+The \racket{\code{raw-vector}}\python{\code{RawTuple}}
+AST node that we introduced in the previous
 section does not get injected.
 section does not get injected.
+{\if\edition\racketEd    
 \begin{lstlisting}
 \begin{lstlisting}
 (raw-vector |$e_1 \ldots e_n$|)
 (raw-vector |$e_1 \ldots e_n$|)
 |$\Rightarrow$|
 |$\Rightarrow$|
 (vector |$e'_1 \ldots e'_n$|)
 (vector |$e'_1 \ldots e'_n$|)
 \end{lstlisting}
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd    
+\begin{lstlisting}
+RawTuple(|$e_1, \ldots, e_n$|)
+|$\Rightarrow$|
+Tuple(|$e'_1, \ldots, e'_n$|)
+\end{lstlisting}
+\fi}
 
 
-The \code{vector-proxy} primitive translates as follows.
+The \racket{\code{vector-proxy}}\python{\code{TupleProxy}} AST translates as follows.
+{\if\edition\racketEd    
 \begin{lstlisting}
 \begin{lstlisting}
 (vector-proxy |$e_1~e_2~e_3$|)
 (vector-proxy |$e_1~e_2~e_3$|)
 |$\Rightarrow$|
 |$\Rightarrow$|
 (inject-proxy (vector |$e'_1~e'_2~e'_3$|))
 (inject-proxy (vector |$e'_1~e'_2~e'_3$|))
 \end{lstlisting}
 \end{lstlisting}
+\fi}
+{\if\edition\pythonEd
+\begin{lstlisting}
+TupleProxy(|$e_1, e_2, T_1, T_2$|)
+|$\Rightarrow$|
+InjectTupleProxy(Tuple(|$e'_1,e'_2, T'_1, T'_2$|))
+\end{lstlisting}
+\fi}
 
 
-We translate the tuple operations into conditional expressions that
-check whether the value is a proxy and then dispatch to either the
-appropriate proxy tuple operation or the regular tuple operation.
-For example, the following is the translation for \code{vector-ref}.
+We translate the element access operations into conditional
+expressions that check whether the value is a proxy and then dispatch
+to either the appropriate proxy tuple operation or the regular tuple
+operation.
+{\if\edition\racketEd    
 \begin{lstlisting}
 \begin{lstlisting}
 (vector-ref |$e_1$| |$i$|)
 (vector-ref |$e_1$| |$i$|)
 |$\Rightarrow$|
 |$\Rightarrow$|
@@ -20212,16 +20365,24 @@ For example, the following is the translation for \code{vector-ref}.
     (proxy-vector-ref |$v$| |$i$|)
     (proxy-vector-ref |$v$| |$i$|)
     (vector-ref (project-vector |$v$|) |$i$|)
     (vector-ref (project-vector |$v$|) |$i$|)
 \end{lstlisting}
 \end{lstlisting}
-Note in the case of a real tuple, we must apply \code{project-vector}
-before the \code{vector-ref}.
+\fi}
+%
+Note that in the branch for a tuple, we must apply
+\racket{\code{project-vector}} \python{project\_tuple} before reading
+from the tuple.
+
+The translation of array operations is similar to the ones for tuples.
+
 
 
 \section{Reveal Casts}
 \section{Reveal Casts}
 \label{sec:reveal-casts-gradual}
 \label{sec:reveal-casts-gradual}
 
 
-Recall that the \code{reveal-casts} pass
+{\if\edition\racketEd    
+Recall that the \code{reveal\_casts} pass
 (Section~\ref{sec:reveal-casts-Lany}) is responsible for lowering
 (Section~\ref{sec:reveal-casts-Lany}) is responsible for lowering
-\code{Inject} and \code{Project} into lower-level operations.  In
-particular, \code{Project} turns into a conditional expression that
+\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
 inspects the tag and retrieves the underlying value.  Here we need to
 augment the translation of \code{Project} to handle the situation when
 augment the translation of \code{Project} to handle the situation when
 the target type is \code{PVector}.  Instead of using
 the target type is \code{PVector}.  Instead of using
@@ -20235,71 +20396,127 @@ the target type is \code{PVector}.  Instead of using
         (if (eq? (proxy-vector-length |$\itm{tup}$|) |$n$|) |$\itm{tup}$| (exit)))
         (if (eq? (proxy-vector-length |$\itm{tup}$|) |$n$|) |$\itm{tup}$| (exit)))
       (exit)))
       (exit)))
 \end{lstlisting}
 \end{lstlisting}
+\fi}
+%
+{\if\edition\pythonEd
+Recall that the $\itm{tagof}$ function determines the bits used to
+identify values of different types and it is used in the \code{reveal\_casts}
+pass in the translation of \code{Project}. The \PTUPLETYNAME{} and
+\PARRAYTYNAME{} types can be mapped to $010$ in binary ($2$ is
+decimal), just like the tuple and array types.
+\fi}  
+%
+Otherwise, the only other changes are adding cases that copy the new AST nodes.
 
 
 
 
 \section{Closure Conversion}
 \section{Closure Conversion}
 \label{sec:closure-conversion-gradual}
 \label{sec:closure-conversion-gradual}
 
 
-The closure conversion pass only requires one minor adjustment.  The
-auxiliary function that translates type annotations needs to be
-updated to handle the \code{PVector} type.
-
-\section{Explicate Control}
-\label{sec:explicate-control-gradual}
-
-Update the \code{explicate\_control} pass to handle the new primitive
-operations on the \code{PVector} type.
+The auxiliary function that translates type annotations needs to be
+updated to handle the \PTUPLETYNAME{} and \PARRAYTYNAME{} types.
+%
+Otherwise, the only other changes are adding cases that copy the new AST nodes.
 
 
 \section{Select Instructions}
 \section{Select Instructions}
 \label{sec:select-instructions-gradual}
 \label{sec:select-instructions-gradual}
 
 
 Recall that the \code{select\_instructions} pass is responsible for
 Recall that the \code{select\_instructions} pass is responsible for
 lowering the primitive operations into x86 instructions.  So we need
 lowering the primitive operations into x86 instructions.  So we need
-to translate the new \code{PVector} operations to x86.  To do so, the
-first question we need to answer is how to differentiate the two
-kinds of values (tuples and proxies) that can inhabit \code{PVector}.
-We need just one bit to accomplish this, and use the bit in position
-$57$ of the 64-bit tag at the front of every tuple (see
-Figure~\ref{fig:tuple-rep}). So far, this bit has been set to $0$, so
-for \code{inject-vector} we leave it that way.
+to translate the new operations on \PTUPLETYNAME{} and \PARRAYTYNAME{}
+to x86.  To do so, the first question we need to answer is how to
+differentiate between tuple and tuples proxies, and likewise for
+arrays and array proxies.  We need just one bit to accomplish this,
+and use the bit in position $63$ of the 64-bit tag at the front of
+every tuple (see Figure~\ref{fig:tuple-rep}) or array
+(Section~\ref{sec:array-rep}). So far, this bit has been set to $0$,
+so for \racket{\code{inject-vector}}\python{\code{InjectTuple}} we leave
+it that way.
+{\if\edition\racketEd    
 \begin{lstlisting}
 \begin{lstlisting}
 (Assign |$\itm{lhs}$| (Prim 'inject-vector (list |$e_1$|)))
 (Assign |$\itm{lhs}$| (Prim 'inject-vector (list |$e_1$|)))
 |$\Rightarrow$|  
 |$\Rightarrow$|  
 movq |$e'_1$|, |$\itm{lhs'}$|
 movq |$e'_1$|, |$\itm{lhs'}$|
 \end{lstlisting}
 \end{lstlisting}
-On the other hand, \code{inject-proxy} sets bit $57$ to $1$.
+\fi}
+{\if\edition\pythonEd    
 \begin{lstlisting}
 \begin{lstlisting}
+Assign([|$\itm{lhs}$|], InjectTuple(|$e_1$|))
+|$\Rightarrow$|  
+movq |$e'_1$|, |$\itm{lhs'}$|
+\end{lstlisting}
+\fi}
+\python{The translation for \code{InjectList} is just a move instruction.}
+\noindent On the other hand,
+\racket{\code{inject-proxy}}\python{\code{InjectTupleProxy}} sets bit
+$63$ to $1$.
+%
+{\if\edition\racketEd
+\begin{lstlisting}  
 (Assign |$\itm{lhs}$| (Prim 'inject-proxy (list |$e_1$|)))
 (Assign |$\itm{lhs}$| (Prim 'inject-proxy (list |$e_1$|)))
 |$\Rightarrow$|  
 |$\Rightarrow$|  
 movq |$e'_1$|, %r11
 movq |$e'_1$|, %r11
-movq |$(1 << 57)$|, %rax
+movq |$(1 << 63)$|, %rax
+orq 0(%r11), %rax
+movq %rax, 0(%r11)
+movq %r11, |$\itm{lhs'}$|
+\end{lstlisting}
+\fi}
+{\if\edition\pythonEd
+\begin{lstlisting}  
+Assign([|$\itm{lhs}$|], InjectTupleProxy(|$e_1$|))
+|$\Rightarrow$|  
+movq |$e'_1$|, %r11
+movq |$(1 << 63)$|, %rax
 orq 0(%r11), %rax
 orq 0(%r11), %rax
 movq %rax, 0(%r11)
 movq %rax, 0(%r11)
 movq %r11, |$\itm{lhs'}$|
 movq %r11, |$\itm{lhs'}$|
 \end{lstlisting}
 \end{lstlisting}
+\fi}
+\python{\noindent The translation for \code{InjectListProxy} should set bit $63$
+  of the tag and also bit $62$, to differentiate between arrays and tuples.}
 
 
-The \code{proxy?} operation consumes the information so carefully
-stashed away by \code{inject-vector} and \code{inject-proxy}.  It
-isolates the $57$th bit to tell whether the value is a real tuple or
+The \racket{\code{proxy?} operation consumes}
+\python{\code{is\_tuple\_proxy} and \code{is\_array\_proxy} operations consume}
+the information so carefully
+stashed away by the injections.  It
+isolates the $63$rd bit to tell whether the value is a tuple/array or
 a proxy.
 a proxy.
+%
+{\if\edition\racketEd
 \begin{lstlisting}
 \begin{lstlisting}
-(Assign |$\itm{lhs}$| (Prim 'proxy? (list e)))
+(Assign |$\itm{lhs}$| (Prim 'proxy? (list |$e_1$|)))
 |$\Rightarrow$|
 |$\Rightarrow$|
 movq |$e_1'$|, %r11
 movq |$e_1'$|, %r11
 movq 0(%r11), %rax
 movq 0(%r11), %rax
-sarq $57, %rax
+sarq $63, %rax
 andq $1, %rax
 andq $1, %rax
 movq %rax, |$\itm{lhs'}$|
 movq %rax, |$\itm{lhs'}$|
 \end{lstlisting}
 \end{lstlisting}
+\fi}%
+%
+{\if\edition\pythonEd
+\begin{lstlisting}
+Assign([|$\itm{lhs}$|], Call(Name('is_tuple_proxy'), [|$e_1$|]))
+|$\Rightarrow$|
+movq |$e_1'$|, %r11
+movq 0(%r11), %rax
+sarq $63, %rax
+andq $1, %rax
+movq %rax, |$\itm{lhs'}$|
+\end{lstlisting}
+\fi}%
+%
+The \racket{\code{project-vector} operation is}
+\python{\code{project\_tuple} and \code{project\_array} operations are}
+straightforward to translate, so we leave that up to the reader.
 
 
-The \code{project-vector} operation is straightforward to translate,
-so we leave it up to the reader.
-
-Regarding the \code{proxy-vector} operations, the runtime provides
-procedures that implement them (they are recursive functions!)  so
-here we simply need to translate these tuple operations into the
-appropriate function call. For example, here is the translation for
-\code{proxy-vector-ref}.
+Regarding the element access operations for tuples and arrays, the
+runtime provides procedures that implement them (they are recursive
+functions!)  so here we simply need to translate these tuple
+operations into the appropriate function call. For example, here is
+the translation for
+\racket{\code{proxy-vector-ref}}\python{\code{proxy\_tuple\_load}}.
+{\if\edition\racketEd
 \begin{lstlisting}
 \begin{lstlisting}
 (Assign |$\itm{lhs}$| (Prim 'proxy-vector-ref (list |$e_1$| |$e_2$|)))
 (Assign |$\itm{lhs}$| (Prim 'proxy-vector-ref (list |$e_1$| |$e_2$|)))
 |$\Rightarrow$|
 |$\Rightarrow$|
@@ -20308,48 +20525,103 @@ movq |$e_2'$|, %rsi
 callq proxy_vector_ref
 callq proxy_vector_ref
 movq %rax, |$\itm{lhs'}$|
 movq %rax, |$\itm{lhs'}$|
 \end{lstlisting}
 \end{lstlisting}
-
-We have another batch of tuple operations to deal with, those for the
-\CANYTY{} type. Recall that the type checker for \LangGrad{}
-generates an \code{any-vector-ref} when there is a \code{vector-ref}
-on something of type \CANYTY{}, and similarly for
-\code{any-vector-set!}  and \code{any-vector-length}
-(Figure~\ref{fig:type-check-Lgradual-1}). In
+\fi}
+{\if\edition\pythonEd
+\begin{lstlisting}
+Assign([|$\itm{lhs}$|], Call(Name('proxy_tuple_load'), [|$e_1$|, |$e_2$|]))
+|$\Rightarrow$|
+movq |$e_1'$|, %rdi
+movq |$e_2'$|, %rsi
+callq proxy_vector_ref
+movq %rax, |$\itm{lhs'}$|
+\end{lstlisting}
+\fi}
+We translate 
+\racket{\code{proxy-vectof-ref}}\python{\code{proxy\_array\_load}}
+to \code{proxy\_vecof\_ref},
+\racket{\code{proxy-vectof-set!}}\python{\code{proxy\_array\_store}}
+to \code{proxy\_vecof\_set}, and
+\racket{\code{proxy-vectof-length}}\python{\code{proxy\_array\_len}}
+to \code{proxy\_vecof\_length}.
+
+We have another batch of operations to deal with, those for the
+\CANYTY{} type. Recall that overload resolution
+(Section~\ref{sec:gradual-resolution}) generates an
+\racket{\code{any-vector-ref}}\python{\code{any\_load\_unsafe}} when
+there is a element access on something of type \CANYTY{}, and
+similarly for
+\racket{\code{any-vector-set!}}\python{\code{any\_store\_unsafe}} and
+\racket{\code{any-vector-length}}\python{\code{any\_len}}. In
 Section~\ref{sec:select-Lany} we selected instructions for these
 Section~\ref{sec:select-Lany} we selected instructions for these
-operations based on the idea that the underlying value was a real
-tuple. But in the current setting, the underlying value is of type
-\code{PVector}. So \code{any-vector-ref} can be translated follows. We
-begin by projecting the underlying value out of the tagged value and
-then call the \code{proxy\_vector\_ref} procedure in the runtime.
+operations based on the idea that the underlying value was a tuple or
+array. But in the current setting, the underlying value is of type
+\PTUPLETYNAME{} or \PARRAYTYNAME{}.  We have added two runtime
+functions to deal with this: \code{proxy\_vec\_ref},
+\code{proxy\_vec\_set}, and
+\code{proxy\_vec\_length}, that inspect bit $62$ of the tag
+to determine whether the value is a tuple or array, and then
+dispatches to the the appropriate function for
+tuples (e.g. \code{proxy\_vector\_ref}) or arrays
+(e.g. \code{proxy\_vecof\_ref}).
+%
+So \racket{\code{any-vector-ref}}\python{\code{any\_load\_unsafe}}
+can be translated follows.
+We begin by projecting the underlying value out of the tagged value and
+then call the \code{proxy\_vec\_ref} procedure in the runtime.
+{\if\edition\racketEd
 \begin{lstlisting}
 \begin{lstlisting}
-(Assign |$\itm{lhs}$| (Prim 'any-vector-ref (list |$e_1$| |$e_2$|)))
+(Assign |$\itm{lhs}$| (Prim 'any-vec-ref (list |$e_1$| |$e_2$|)))
+|$\Rightarrow$|
 movq |$\neg 111$|, %rdi
 movq |$\neg 111$|, %rdi
 andq |$e_1'$|, %rdi
 andq |$e_1'$|, %rdi
 movq |$e_2'$|, %rsi
 movq |$e_2'$|, %rsi
-callq proxy_vector_ref
+callq proxy_vec_ref
+movq %rax, |$\itm{lhs'}$|
+\end{lstlisting}
+\fi}
+{\if\edition\pythonEd
+\begin{lstlisting}
+Assign([|$\itm{lhs}$|], Call(Name('any_load_unsafe'), [|$e_1$|, |$e_2$|]))
+|$\Rightarrow$|
+movq |$\neg 111$|, %rdi
+andq |$e_1'$|, %rdi
+movq |$e_2'$|, %rsi
+callq proxy_vec_ref
 movq %rax, |$\itm{lhs'}$|
 movq %rax, |$\itm{lhs'}$|
 \end{lstlisting}
 \end{lstlisting}
-The \code{any-vector-set!} and \code{any-vector-length} operators can
-be translated in a similar way.
+\fi}
+\noindent The \racket{\code{any-vector-set!}}\python{\code{any\_store\_unsafe}}
+and \racket{\code{any-vector-length}}\python{\code{any\_len}} operators 
+are translated in a similar way. Alternatively, you could generate
+instructions to open-code
+the \code{proxy\_vec\_ref}, \code{proxy\_vec\_set},
+and \code{proxy\_vec\_length} functions.
 
 
 \begin{exercise}\normalfont\normalsize
 \begin{exercise}\normalfont\normalsize
   Implement a compiler for the gradually-typed \LangGrad{} language by
   Implement a compiler for the gradually-typed \LangGrad{} language by
   extending and adapting your compiler for \LangLam{}. Create 10 new
   extending and adapting your compiler for \LangLam{}. Create 10 new
   partially-typed test programs. In addition to testing with these
   partially-typed test programs. In addition to testing with these
   new programs, also test your compiler on all the tests for \LangLam{}
   new programs, also test your compiler on all the tests for \LangLam{}
-  and tests for \LangDyn{}. Sometimes you may get a type checking error
-  on the \LangDyn{} programs but you can adapt them by inserting
-  a cast to the \CANYTY{} type around each subexpression
-  causing a type error. While \LangDyn{} does not have explicit casts,
-  you can induce one by wrapping the subexpression \code{e}
-  with a call to an un-annotated identity function, like this:
-  \code{((lambda (x) x) e)}.
+  and tests for \LangDyn{}.
+%
+  \racket{Sometimes you may get a type checking error on the
+    \LangDyn{} programs but you can adapt them by inserting a cast to
+    the \CANYTY{} type around each subexpression causing a type
+    error. While \LangDyn{} does not have explicit casts, you can
+    induce one by wrapping the subexpression \code{e} with a call to
+    an un-annotated identity function, like this: \code{((lambda (x) x) e)}.}
+%
+  \python{Sometimes you may get a type checking error on the
+    \LangDyn{} programs but you can adapt them by inserting a
+    temporary variable of type \CANYTY{} that is initialized with the
+    troublesome expression.}
 \end{exercise}
 \end{exercise}
 
 
 \begin{figure}[p]
 \begin{figure}[p]
 \begin{tcolorbox}[colback=white]  
 \begin{tcolorbox}[colback=white]  
 \begin{tikzpicture}[baseline=(current  bounding  box.center),scale=0.85]
 \begin{tikzpicture}[baseline=(current  bounding  box.center),scale=0.85]
-\node (Lgradual) at (9,4)  {\large \LangGrad{}};
+\node (Lgradual) at (12,4)  {\large \LangGrad{}};
+\node (Lgradualr) at (9,4)  {\large \LangGrad{}};
 \node (Lgradualp) at (6,4)  {\large \LangCast{}};
 \node (Lgradualp) at (6,4)  {\large \LangCast{}};
 \node (Llambdapp) at (3,4)  {\large \LangProxy{}};
 \node (Llambdapp) at (3,4)  {\large \LangProxy{}};
 \node (Llambdaproxy) at (0,4)  {\large \LangPVec{}};
 \node (Llambdaproxy) at (0,4)  {\large \LangPVec{}};
@@ -20374,12 +20646,14 @@ be translated in a similar way.
 
 
 
 
 \path[->,bend right=15] (Lgradual) edge [above] node
 \path[->,bend right=15] (Lgradual) edge [above] node
-     {\ttfamily\footnotesize type\_check} (Lgradualp);
+     {\ttfamily\footnotesize resolve} (Lgradualr);
+\path[->,bend right=15] (Lgradualr) edge [above] node
+     {\ttfamily\footnotesize cast\_insert} (Lgradualp);
 \path[->,bend right=15] (Lgradualp) edge [above] node
 \path[->,bend right=15] (Lgradualp) edge [above] node
      {\ttfamily\footnotesize lower\_casts} (Llambdapp);
      {\ttfamily\footnotesize lower\_casts} (Llambdapp);
 \path[->,bend right=15] (Llambdapp) edge [above] node
 \path[->,bend right=15] (Llambdapp) edge [above] node
      {\ttfamily\footnotesize differentiate.} (Llambdaproxy);
      {\ttfamily\footnotesize differentiate.} (Llambdaproxy);
-\path[->,bend left=15] (Llambdaproxy) edge [right] node
+\path[->,bend left=15] (Llambdaproxy) edge [left] node
      {\ttfamily\footnotesize shrink} (Llambdaproxy-2);
      {\ttfamily\footnotesize shrink} (Llambdaproxy-2);
 \path[->,bend left=15] (Llambdaproxy-2) edge [above] node
 \path[->,bend left=15] (Llambdaproxy-2) edge [above] node
      {\ttfamily\footnotesize uniquify} (Llambdaproxy-3);
      {\ttfamily\footnotesize uniquify} (Llambdaproxy-3);
@@ -21465,7 +21739,8 @@ registers.
 \printbibliography
 \printbibliography
 
 
 %\printindex{authors}{Author Index}
 %\printindex{authors}{Author Index}
-\printindex{subject}{Subject Index}
+\printindex{subject}{Index}
+
 
 
 
 
 \end{document}
 \end{document}

+ 25 - 4
defs.tex

@@ -71,12 +71,12 @@
 \newcommand{\LangCast}{$\Lang_{\mathsf{Cast}}$} %R9'
 \newcommand{\LangCast}{$\Lang_{\mathsf{Cast}}$} %R9'
 \newcommand{\LangCastM}{\Lang_{\mathsf{Cast}}} %R9'
 \newcommand{\LangCastM}{\Lang_{\mathsf{Cast}}} %R9'
 \newcommand{\LangProxy}{\ensuremath{\Lang_{\mathsf{Proxy}}}} %R8''
 \newcommand{\LangProxy}{\ensuremath{\Lang_{\mathsf{Proxy}}}} %R8''
-\newcommand{\LangPVec}{\ensuremath{\Lang_{\mathsf{PVec}}}} %R8''
-\newcommand{\LangPVecFunRef}{\ensuremath{\Lang^{\mathsf{FunRef}}_{\mathsf{PVec}}}} %R8''
-\newcommand{\LangPVecAlloc}{\ensuremath{\Lang^{\mathsf{Alloc}}_{\mathsf{PVec}}}} %R8''
+\newcommand{\LangPVec}{\ensuremath{\Lang_{\mathsf{POr}}}} %R8''
+\newcommand{\LangPVecFunRef}{\ensuremath{\Lang^{\mathsf{FunRef}}_{\mathsf{POr}}}} %R8''
+\newcommand{\LangPVecAlloc}{\ensuremath{\Lang^{\mathsf{Alloc}}_{\mathsf{POr}}}} %R8''
 \newcommand{\LangPoly}{\ensuremath{\Lang_{\mathsf{Poly}}}} %R10
 \newcommand{\LangPoly}{\ensuremath{\Lang_{\mathsf{Poly}}}} %R10
 \newcommand{\LangInst}{\ensuremath{\Lang_{\mathsf{Inst}}}} %R'10
 \newcommand{\LangInst}{\ensuremath{\Lang_{\mathsf{Inst}}}} %R'10
-\newcommand{\LangCLoopPVec}{\ensuremath{\CLang^{\mathsf{PVec}}_{\circlearrowleft}}} %Cp7
+\newcommand{\LangCLoopPVec}{\ensuremath{\CLang^{\mathsf{POr}}_{\circlearrowleft}}} %Cp7
 
 
 \newcommand{\LangXVar}{$\mathrm{x86}_{\mathsf{Var}}$} % pseudo x86_0
 \newcommand{\LangXVar}{$\mathrm{x86}_{\mathsf{Var}}$} % pseudo x86_0
 \newcommand{\LangXASTInt}{\ensuremath{\mathrm{x86}_{\mathsf{Int}}}} % x86_0
 \newcommand{\LangXASTInt}{\ensuremath{\mathrm{x86}_{\mathsf{Int}}}} % x86_0
@@ -145,9 +145,14 @@
 \newcommand{\CUNIOP}[2]{\LP #1~#2 \RP}
 \newcommand{\CUNIOP}[2]{\LP #1~#2 \RP}
 \newcommand{\BINOP}[3]{\key{(Prim}~#1~\code{(}#2~#3\code{))}}
 \newcommand{\BINOP}[3]{\key{(Prim}~#1~\code{(}#2~#3\code{))}}
 \newcommand{\CBINOP}[3]{\LP #1~#2~#3\RP}
 \newcommand{\CBINOP}[3]{\LP #1~#2~#3\RP}
+\newcommand{\EQNAME}{\key{eq?}}
 \newcommand{\CEQ}[2]{\LP\key{eq?}~#1~#2\RP}
 \newcommand{\CEQ}[2]{\LP\key{eq?}~#1~#2\RP}
+\newcommand{\IFNAME}{\key{If}}
 \newcommand{\IF}[3]{\key{(If}\,#1~#2~#3\key{)}}
 \newcommand{\IF}[3]{\key{(If}\,#1~#2~#3\key{)}}
 \newcommand{\CIF}[3]{\LP\key{if}~#1~#2~#3\RP}
 \newcommand{\CIF}[3]{\LP\key{if}~#1~#2~#3\RP}
+\newcommand{\ANDNAME}{\key{and}}
+\newcommand{\ORNAME}{\key{or}}
+\newcommand{\NOTNAME}{\key{not}}
 \newcommand{\AND}[2]{\key{(Prim}~\code{'and}~\code{(}#1~#2\code{))}}
 \newcommand{\AND}[2]{\key{(Prim}~\code{'and}~\code{(}#1~#2\code{))}}
 \newcommand{\OR}[2]{\key{(Prim}~\code{'or}~\code{(}#1~#2\code{))}}
 \newcommand{\OR}[2]{\key{(Prim}~\code{'or}~\code{(}#1~#2\code{))}}
 \newcommand{\CAND}[2]{\CBINOP{\key{and}}{#1}{#2}}
 \newcommand{\CAND}[2]{\CBINOP{\key{and}}{#1}{#2}}
@@ -155,11 +160,15 @@
 \newcommand{\INTTY}{{\key{Integer}}}
 \newcommand{\INTTY}{{\key{Integer}}}
 \newcommand{\INTTYPE}{{\key{Integer}}}
 \newcommand{\INTTYPE}{{\key{Integer}}}
 \newcommand{\BOOLTY}{{\key{Boolean}}}
 \newcommand{\BOOLTY}{{\key{Boolean}}}
+\newcommand{\TUPLETYPENAME}{\key{Vector}}
+\newcommand{\ARRAYTYPENAME}{\key{Vectorof}}
 \newcommand{\VECTY}[1]{\LP\key{Vector}~#1\RP}
 \newcommand{\VECTY}[1]{\LP\key{Vector}~#1\RP}
 \newcommand{\ARRAYTY}[1]{\LP\key{Vectorof}~#1\RP}
 \newcommand{\ARRAYTY}[1]{\LP\key{Vectorof}~#1\RP}
 \newcommand{\CARRAYTY}[1]{\LP\key{Vectorof}~#1\RP}
 \newcommand{\CARRAYTY}[1]{\LP\key{Vectorof}~#1\RP}
 \newcommand{\ANYTY}{\key{Any}}
 \newcommand{\ANYTY}{\key{Any}}
 \newcommand{\CANYTY}{\key{Any}}
 \newcommand{\CANYTY}{\key{Any}}
+\newcommand{\PTUPLETYNAME}{\key{PVector}}
+\newcommand{\PARRAYTYNAME}{\key{PVectorof}}
 \newcommand{\PTUPLETY}[1]{\LP\key{PVector}~#1\RP}
 \newcommand{\PTUPLETY}[1]{\LP\key{PVector}~#1\RP}
 \newcommand{\CPTUPLETY}[1]{\LP\key{PVector}~#1\RP}
 \newcommand{\CPTUPLETY}[1]{\LP\key{PVector}~#1\RP}
 \newcommand{\CPROGRAM}[2]{\LP\code{CProgram}~#1~#2\RP}
 \newcommand{\CPROGRAM}[2]{\LP\code{CProgram}~#1~#2\RP}
@@ -184,6 +193,8 @@
 %% Use BEGIN instead of LET -Jeremy
 %% Use BEGIN instead of LET -Jeremy
 %% \newcommand{\LET}[3]{\key{Let}\LP #1 \key{,} #2 \key{,} #3 \RP}
 %% \newcommand{\LET}[3]{\key{Let}\LP #1 \key{,} #2 \key{,} #3 \RP}
 %% \newcommand{\CLET}[3]{\key{let}~#1~\key{=}~#2~\key{in}~#3}
 %% \newcommand{\CLET}[3]{\key{let}~#1~\key{=}~#2~\key{in}~#3}
+\newcommand{\PTUPLETYNAME}{\key{ProxyOrTupleType}}
+\newcommand{\PARRAYTYNAME}{\key{ProxyOrListType}}
 \newcommand{\PTUPLETY}[1]{\key{ProxyOrTupleType}\LP#1\RP}
 \newcommand{\PTUPLETY}[1]{\key{ProxyOrTupleType}\LP#1\RP}
 \newcommand{\CPTUPLETY}[1]{\key{ProxyOrTupleType}\LP#1\RP}
 \newcommand{\CPTUPLETY}[1]{\key{ProxyOrTupleType}\LP#1\RP}
 \newcommand{\PARRAYTY}[1]{\key{ProxyOrListType}\LP#1\RP}
 \newcommand{\PARRAYTY}[1]{\key{ProxyOrListType}\LP#1\RP}
@@ -209,6 +220,8 @@
 \newcommand{\CUNIOP}[2]{#1~#2}
 \newcommand{\CUNIOP}[2]{#1~#2}
 \newcommand{\BINOP}[3]{\key{BinOp}\LP #1 \code{,} #2 \code{,} #3 \RP}
 \newcommand{\BINOP}[3]{\key{BinOp}\LP #1 \code{,} #2 \code{,} #3 \RP}
 \newcommand{\CBINOP}[3]{#2~#1~#3}
 \newcommand{\CBINOP}[3]{#2~#1~#3}
+\newcommand{\EQNAME}{\key{Eq}}
+\newcommand{\NOTEQNAME}{\key{NotEq}}
 \newcommand{\CEQ}[2]{#1~\code{==}~#2}
 \newcommand{\CEQ}[2]{#1~\code{==}~#2}
 \newcommand{\CGET}[2]{#1 \LS #2 \RS}
 \newcommand{\CGET}[2]{#1 \LS #2 \RS}
 \newcommand{\GET}[2]{\key{Subscript}\LP #1 \code{,} #2 \code{,} \code{Load()} \RP}
 \newcommand{\GET}[2]{\key{Subscript}\LP #1 \code{,} #2 \code{,} \code{Load()} \RP}
@@ -222,8 +235,12 @@
 \newcommand{\CCMP}[3]{#2~#1~#3}
 \newcommand{\CCMP}[3]{#2~#1~#3}
 \newcommand{\TRUE}{\key{True}}
 \newcommand{\TRUE}{\key{True}}
 \newcommand{\FALSE}{\key{False}}
 \newcommand{\FALSE}{\key{False}}
+\newcommand{\IFNAME}{\key{IfExp}}
 \newcommand{\IF}[3]{\key{IfExp}\LP #1 \code{,} #2 \code{,} #3 \RP}
 \newcommand{\IF}[3]{\key{IfExp}\LP #1 \code{,} #2 \code{,} #3 \RP}
 \newcommand{\CIF}[3]{#2~\key{if}~#1~\key{else}~#3}
 \newcommand{\CIF}[3]{#2~\key{if}~#1~\key{else}~#3}
+\newcommand{\ANDNAME}{\key{and}}
+\newcommand{\ORNAME}{\key{or}}
+\newcommand{\NOTNAME}{\key{not}}
 \newcommand{\AND}[2]{\BOOLOP{\key{And()}}{#1}{#2}}
 \newcommand{\AND}[2]{\BOOLOP{\key{And()}}{#1}{#2}}
 \newcommand{\CAND}[2]{#1~\key{and}~#2}
 \newcommand{\CAND}[2]{#1~\key{and}~#2}
 \newcommand{\OR}[2]{\BOOLOP{\key{Or()}}{#1}{#2}}
 \newcommand{\OR}[2]{\BOOLOP{\key{Or()}}{#1}{#2}}
@@ -232,6 +249,8 @@
 \newcommand{\BOOLTY}{{\key{bool}}}
 \newcommand{\BOOLTY}{{\key{bool}}}
 \newcommand{\ANYTY}{{\key{AnyType}}}
 \newcommand{\ANYTY}{{\key{AnyType}}}
 \newcommand{\CANYTY}{{\key{Any}}}
 \newcommand{\CANYTY}{{\key{Any}}}
+\newcommand{\TUPLETYPENAME}{\key{TupleType}}
+\newcommand{\ARRAYTYPENAME}{\key{ListType}}
 \newcommand{\VECTY}[1]{{\key{TupleType}\LP\LS #1 \RS\RP}}
 \newcommand{\VECTY}[1]{{\key{TupleType}\LP\LS #1 \RS\RP}}
 \newcommand{\ARRAYTY}[1]{\key{ListType}\LP#1\RP}
 \newcommand{\ARRAYTY}[1]{\key{ListType}\LP#1\RP}
 \newcommand{\CARRAYTY}[1]{\key{list}\LS#1\RS}
 \newcommand{\CARRAYTY}[1]{\key{list}\LS#1\RS}
@@ -312,6 +331,7 @@
 \newcommand{\TAILCALL}[2]{\key{(TailCall}~#1~#2\code{)}}
 \newcommand{\TAILCALL}[2]{\key{(TailCall}~#1~#2\code{)}}
 \newcommand{\CASSIGN}[2]{#1~\key{=}~#2\key{;}}
 \newcommand{\CASSIGN}[2]{#1~\key{=}~#2\key{;}}
 \newcommand{\ASSIGN}[2]{\key{(Assign}~#1~#2\key{)}}
 \newcommand{\ASSIGN}[2]{\key{(Assign}~#1~#2\key{)}}
+\newcommand{\IFSTMTNAME}{\key{IfStmt}}
 \newcommand{\IFSTMT}[3]{\key{(IfStmt}\,#1~#2~#3\key{)}}
 \newcommand{\IFSTMT}[3]{\key{(IfStmt}\,#1~#2~#3\key{)}}
 \newcommand{\RETURN}[1]{\key{(Return}~#1\key{)}}
 \newcommand{\RETURN}[1]{\key{(Return}~#1\key{)}}
 \newcommand{\CRETURN}[1]{\key{return}~#1\key{;}}
 \newcommand{\CRETURN}[1]{\key{return}~#1\key{;}}
@@ -334,6 +354,7 @@
 \newcommand{\ASSIGN}[2]{\key{Assign}\LP\LS #1\RS\key{, }#2\RP}
 \newcommand{\ASSIGN}[2]{\key{Assign}\LP\LS #1\RS\key{, }#2\RP}
 \newcommand{\CANNASSIGN}[3]{#1~\key{:}~#2~\key{=}~#3}
 \newcommand{\CANNASSIGN}[3]{#1~\key{:}~#2~\key{=}~#3}
 \newcommand{\ANNASSIGN}[3]{\key{AnnAssign}\LP#1\key{, }#2\key{, }#3\key{, 0}\RP}
 \newcommand{\ANNASSIGN}[3]{\key{AnnAssign}\LP#1\key{, }#2\key{, }#3\key{, 0}\RP}
+\newcommand{\IFSTMTNAME}{\key{If}}
 \newcommand{\IFSTMT}[3]{\key{If}\LP #1 \code{, } #2 \code{, } #3 \RP}
 \newcommand{\IFSTMT}[3]{\key{If}\LP #1 \code{, } #2 \code{, } #3 \RP}
 \newcommand{\CIFSTMT}[3]{\key{if}~#1\code{:}~#2~\code{else:}~#3}
 \newcommand{\CIFSTMT}[3]{\key{if}~#1\code{:}~#2~\code{else:}~#3}
 \newcommand{\CBEGIN}[2]{\key{begin:}~#1~#2}
 \newcommand{\CBEGIN}[2]{\key{begin:}~#1~#2}