A09 arrays builtins

.travis.yml

@@ -0,0 +1,8 @@
+language: c
+services:
+  - docker
+before_install:
+    - docker pull berezun/cw-2020
+    - docker run -d -it --name cw-2020 -v $(pwd):/usr/share/compiler-2020 berezun/cw-2020
+script:
+     docker exec -it cw-2020 sh test.sh

Makefile

@@ -0,0 +1,13 @@
+.PHONY: all 
+
+all:
+	make -C src
+	make -C runtime
+	make -C regression
+
+clean:
+	make clean -C src
+	make clean -C runtime
+	make clean -C regression
+
+

lectures/02.tex

@@ -0,0 +1,298 @@
+\documentclass{article}
+
+\usepackage{amssymb, amsmath}
+\usepackage{alltt}
+\usepackage{pslatex}
+\usepackage{epigraph}
+\usepackage{verbatim}
+\usepackage{latexsym}
+\usepackage{array}
+\usepackage{comment}
+\usepackage{makeidx}
+\usepackage{listings}
+\usepackage{indentfirst}
+\usepackage{verbatim}
+\usepackage{color}
+\usepackage{url}
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{stmaryrd}
+\usepackage{amsmath, amsthm, amssymb}
+\usepackage{graphicx}
+\usepackage{euscript}
+\usepackage{mathtools}
+\usepackage{mathrsfs}
+\usepackage{multirow,bigdelim}
+\usepackage{subcaption}
+\usepackage{placeins}
+
+\makeatletter
+
+\makeatother
+
+\definecolor{shadecolor}{gray}{1.00}
+\definecolor{darkgray}{gray}{0.30}
+
+\def\transarrow{\xrightarrow}
+\newcommand{\setarrow}[1]{\def\transarrow{#1}}
+
+\def\padding{\phantom{X}}
+\newcommand{\setpadding}[1]{\def\padding{#1}}
+
+\def\subarrow{}
+\newcommand{\setsubarrow}[1]{\def\subarrow{#1}}
+
+\newcommand{\trule}[2]{\frac{#1}{#2}}
+\newcommand{\crule}[3]{\frac{#1}{#2},\;{#3}}
+\newcommand{\withenv}[2]{{#1}\vdash{#2}}
+\newcommand{\trans}[3]{{#1}\transarrow{\padding{\textstyle #2}\padding}\subarrow{#3}}
+\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}\subarrow{#3},\;{#4}}
+\newcommand{\llang}[1]{\mbox{\lstinline[mathescape]|#1|}}
+\newcommand{\pair}[2]{\inbr{{#1}\mid{#2}}}
+\newcommand{\inbr}[1]{\left<{#1}\right>}
+\newcommand{\highlight}[1]{\color{red}{#1}}
+\newcommand{\ruleno}[1]{\eqno[\scriptsize\textsc{#1}]}
+\newcommand{\rulename}[1]{\textsc{#1}}
+\newcommand{\inmath}[1]{\mbox{$#1$}}
+\newcommand{\lfp}[1]{fix_{#1}}
+\newcommand{\gfp}[1]{Fix_{#1}}
+\newcommand{\vsep}{\vspace{-2mm}}
+\newcommand{\supp}[1]{\scriptsize{#1}}
+\newcommand{\sembr}[1]{\llbracket{#1}\rrbracket}
+\newcommand{\cd}[1]{\texttt{#1}}
+\newcommand{\free}[1]{\boxed{#1}}
+\newcommand{\binds}{\;\mapsto\;}
+\newcommand{\dbi}[1]{\mbox{\bf{#1}}}
+\newcommand{\sv}[1]{\mbox{\textbf{#1}}}
+\newcommand{\bnd}[2]{{#1}\mkern-9mu\binds\mkern-9mu{#2}}
+\newtheorem{lemma}{Lemma}
+\newtheorem{theorem}{Theorem}
+\newcommand{\meta}[1]{{\mathcal{#1}}}
+\renewcommand{\emptyset}{\varnothing}
+\newcommand{\dom}[1]{\mathtt{dom}\;{#1}}
+\newcommand{\primi}[2]{\mathbf{#1}\;{#2}}
+
+\definecolor{light-gray}{gray}{0.90}
+\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}}
+
+\lstdefinelanguage{lama}{
+keywords={read, write, skip,if,then,else,elif,fi,while,do,od,repeat,until,for,fun,local,public,return,import,length,
+string,case,of,esac,when,boxed,unboxed,string,sexp,array,infix,infixl,infixr,at,before,after,true,false,eta,lazy},
+sensitive=true,
+basicstyle=\small,
+%commentstyle=\scriptsize\rmfamily,
+keywordstyle=\ttfamily\bfseries,
+identifierstyle=\ttfamily,
+basewidth={0.5em,0.5em},
+columns=fixed,
+fontadjust=true,
+literate={->}{{$\to$}}3,
+morecomment=[s][\ttfamily]{(*}{*)},
+morecomment=[l][\ttfamily]{--}
+}
+
+\lstset{
+mathescape=true,
+basicstyle=\small,
+identifierstyle=\ttfamily,
+keywordstyle=\bfseries,
+commentstyle=\scriptsize\rmfamily,
+basewidth={0.5em,0.5em},
+fontadjust=true,
+escapechar=!,
+language=lama
+}
+
+\sloppy
+
+\newcommand{\lama}{$\lambda\kern -.1667em\lower -.5ex\hbox{$a$}\kern -.1000em\lower .2ex\hbox{$\mathcal M$}\kern -.1000em\lower -.5ex\hbox{$a$}$\xspace}
+
+\theoremstyle{definition}
+
+\author{Dmitry Boulytchev}
+
+\begin{document}
+
+\renewcommand{\arraystretch}{1.5}
+
+\section{Statements}
+
+More interesting language~--- a language of simple statements:
+
+\[
+\renewcommand{\arraystretch}{1}
+\begin{array}{rcl}  
+  \mathscr S & = & \mbox{\lstinline|skip|} \\
+             &   & \mathscr X \mbox{\lstinline|:=|} \;\mathscr E \\
+             &   & \mbox{\lstinline|read (|} \mathscr X \mbox{\lstinline|)|} \\
+             &   & \mbox{\lstinline|write (|} \mathscr E \mbox{\lstinline|)|} \\
+             &   & \mathscr S \mbox{\lstinline|;|} \mathscr S
+\end{array}
+\]
+
+Here $\mathscr E, \mathscr X$ stand for the sets of expressions and variables, as in the previous lecture.
+Informally, the language allows to write a striaght-line programs which transform an input stream of integers into
+output stream of integers.
+
+Again, we define the semantics for this language 
+
+\[
+\sembr{\bullet}_{\mathscr S} : \mathscr S \mapsto \mathbb Z^* \to \mathbb Z^*
+\]
+
+with the semantic domain of partial functions from integer streams to integer streams. Again, we will
+use \emph{big-step operational semantics}: we define a ternary relation ``$\Rightarrow_{\mathscr S}$''
+
+\[
+\Rightarrow_{\mathscr S} \subseteq \mathscr C \times \mathscr S \times \mathscr C
+\]
+
+where $\mathscr C$~--- a set of possible \emph{configurations} during a program execution.
+We will write $c_1\xRightarrow{S}_{\mathscr S}c_2$ instead of $(c_1, S, c_2)\in\Rightarrow_{\mathscr S}$ and informally
+interpret the former as ``the execution of a statement $S$ in a configuration $c_1$ completes with the configuration
+$c_2$''.
+
+The set of all configuration is defined as
+
+\[
+\begin{array}{rcl}
+  \mathscr C &=& \Sigma \times \mathscr W\\
+  \mathscr W &=& \mathbb Z^* \times \mathbb Z^*
+\end{array}
+\]
+
+where $\mathscr W$~--- a set of \emph{worlds}, each of which escapsulates some input-output stream pair. For
+simplicity, we define the following operations for worlds:
+
+\[
+\begin{array}{rcl}
+  \primi{read}{\inbr{xi,\,o}}    & = & \inbr{x,\,\inbr{i,\,o}}\\
+  \primi{write}{x\,\inbr{i,\,o}} & = & \inbr{i,\,ox}\\
+  \primi{out}{\inbr{i,\,o}}      & = & o
+\end{array}
+\]
+
+The relation ``$\Rightarrow_{\mathscr S}$'' is defined by the following deductive system (see Fig.~\ref{bs_stmt}). The first
+three rules are \emph{axioms} as they do not have any premises. Note, according to these rules sometimes a program
+cannot do a step in a given configuration: a value of an expression can be undefined in a given state in rules
+$\rulename{Assign}$ and $\rulename{Write}$, and there can be no input value in rule $\rulename{Read}$. This style of
+a semantics description is called big-step operational semantics, since the results of a computation are
+immediately observable at the right hand side of ``$\Rightarrow$'' and, thus, the computation is performed in
+a single ``big'' step. And, again, this style of a semantic description can be used to easily implement a
+reference interpreter.
+
+With the relation ``$\Rightarrow_{\mathscr S}$'' defined we can abbreviate the ``surface'' semantics for the language of statements:
+
+\setarrow{\xRightarrow}
+\setsubarrow{_{\mathscr S}}
+\[
+\trule{\trans{\inbr{\Lambda,\,\inbr{i,\,\epsilon}}}{S}{\inbr{\sigma,\,\omega}}}
+      {\sembr{S}_{\mathscr S}i=\primi{out}{\omega}}
+\]
+
+
+\begin{figure}[t]
+\arraycolsep=10pt
+\[\trans{c}{\llang{skip}}{c}\ruleno{Skip}\]
+\[\trans{\inbr{\sigma,\, \omega}}{\llang{x := $\;\;e$}}{\inbr{\sigma\,[x\gets\sembr{e}_{\mathscr E}\;\sigma],\,\omega}}\ruleno{Assign}\]
+\[\trule{\inbr{z,\,\omega^\prime}=\primi{read}{\omega}}
+        {\trans{\inbr{\sigma,\, \omega}}{\llang{read ($x$)}}{\inbr{\sigma\,[x\gets z],\,\omega^\prime}}}\ruleno{Read}\]
+\[\trans{\inbr{\sigma,\, \omega}}{\llang{write ($e$)}}{\inbr{\sigma,\, \primi{write}{(\sembr{e}_{\mathscr E}\;\sigma)\, \omega}}}\ruleno{Write}\]
+\[\trule{\begin{array}{cc}
+            \trans{c_1}{S_1}{c^\prime} & \trans{c^\prime}{S_2}{c_2}
+         \end{array}}
+        {\trans{c_1}{S_1\llang{;}S_2}{c_2}}\ruleno{Seq}\]
+\caption{Big-step operational semantics for statements}
+\label{bs_stmt}
+\end{figure}
+
+\section{Stack Machine}
+
+Stack machine is a simple abstract computational device, which can be used as a convenient model to constructively describe
+the compilation process.
+
+In short, stack machine operates on the same configurations, as the language of statements, plus a stack of integers. The
+computation, performed by the stack machine, is controlled by a program, which is described as follows:
+
+\[
+\renewcommand{\arraystretch}{1}
+\begin{array}{rcl}
+  \mathscr I & = & \llang{BINOP $\;\otimes$} \\
+             &   & \llang{CONST $\;\mathbb N$} \\
+             &   & \llang{READ} \\
+             &   & \llang{WRITE} \\
+             &   & \llang{LD $\;\mathscr X$} \\
+             &   & \llang{ST $\;\mathscr X$} \\
+  \mathscr P & = & \epsilon \\
+             &   & \mathscr I\mathscr P
+\end{array}
+\]
+
+Here the syntax category $\mathscr I$ stands for \emph{instructions}, $\mathscr P$~--- for \emph{programs}; thus, a program is a finite
+string of instructions.
+
+The semantics of stack machine program can be described, again, in the form of big-step operational semantics. This time the set of
+stack machine configurations is
+
+\[
+\mathscr C_{SM} = \mathbb Z^* \times \mathscr C
+\]
+
+where the first component is a stack, and the second~--- a configuration as in the semantics of statement language. The rules are shown on Fig.~\ref{bs_sm}; note,
+now we have one axiom and six inference rules (one per instruction).
+
+\setsubarrow{_{\mathscr{SM}}}
+
+As for the statement, with the aid of the relation ``$\Rightarrow_{\mathscr{SM}}$'' we can define the surface semantics of stack machine:
+
+\[
+\trule{\trans{\inbr{\epsilon,\,\inbr{\Lambda,\,\inbr{i,\,\epsilon}}}}{p}{\inbr{s, \inbr{\sigma,\,\omega}}}}
+      {\sembr{p}_{\mathscr{SM}}\;i=\primi{out}{\omega}}
+\]
+
+\begin{figure}[t]
+  \[\trans{c}{\epsilon}{c}\ruleno{Stop$_{SM}$}\]
+  \[\trule{\trans{\inbr{(x\oplus y)s, c}}{p}{c^\prime}}{\trans{\inbr{yxs, c}}{[\llang{BINOP $\;\otimes$}]p}{c^\prime}}\ruleno{Binop$_{SM}$}\]
+  \[\trule{\trans{\inbr{zs, c}}{p}{c^\prime}}{\trans{\inbr{s, c}}{[\llang{CONST $\;z$}]p}{c^\prime}}\ruleno{Const$_{SM}$}\]
+  \[\trule{\inbr{z,\,\omega^\prime}=\primi{read}{\omega},\,\trans{\inbr{zs, \inbr{\sigma,\,\omega^\prime}}}{p}{c^\prime}}{\trans{\inbr{s, \inbr{\sigma,\,\omega}}}{\llang{READ}\,p}{c^\prime}}\ruleno{Read$_{SM}$}\]
+  \[\trule{\trans{\inbr{s,\,\inbr{\sigma,\,\primi{write}{z\,\omega}}}}{p}{c^\prime}}{\trans{\inbr{zs,\, \inbr{\sigma,\,\omega}}}{\llang{WRITE}\,p}{c^\prime}}\ruleno{Write$_{SM}$}\]
+  \[\trule{\trans{\inbr{(\sigma\;x)s,\, \inbr{\sigma,\,\omega}}}{p}{c^\prime}}{\trans{\inbr{s,\, \inbr{\sigma,\,\omega}}}{[\llang{LD $\;x$}]p}{c^\prime}}\ruleno{LD$_{SM}$}\]
+  \[\trule{\trans{\inbr{s,\, \inbr{\sigma[x\gets z],\,\omega}}}{p}{c^\prime}}{\trans{\inbr{zs,\, \inbr{\sigma,\,\omega}}}{[\llang{ST $\;x$}]p}{c^\prime}}\ruleno{ST$_{SM}$}\]
+  \caption{Big-step operational semantics for stack machine}
+  \label{bs_sm}
+\end{figure}
+
+\section{A Compiler for the Stack Machine}
+
+A compiler of the statement language into the stack machine is a total mapping
+
+\[
+\sembr{\bullet}^{comp} : \mathscr S \mapsto \mathscr P
+\]
+
+We can describe the compiler in the form of denotational semantics for the source language. In fact, we can treat the compiler as a \emph{static} semantics, which
+maps each program into its stack machine equivalent.
+
+As the source language consists of two syntactic categories (expressions and statments), the compiler has to be ``bootstrapped'' from the compiler for expressions
+$\sembr{\bullet}_{\mathscr E}^{comp}$:
+
+\[
+\begin{array}{rcl}
+  \sembr{x}_{\mathscr E}^{comp}&=&\llang{[LD $\;x$]}\\
+  \sembr{n}_{\mathscr E}^{comp}&=&\llang{[CONST $\;n$]}\\
+  \sembr{A\otimes B}_{\mathscr E}^{comp}&=&\sembr{A}_{\mathscr E}^{comp}\sembr{B}_{\mathscr E}^{comp}[\llang{BINOP $\;\otimes$}]
+\end{array}
+\]
+
+And now the main dish:
+
+\[
+\begin{array}{rcl}
+  \sembr{\llang{$x$ := $e$}}^{comp}&=&\sembr{e}_{\mathscr E}^{comp}\llang{[ST $\;x$]}\\
+  \sembr{\llang{read ($x$)}}^{comp}&=&\llang{[READ][ST $\;x$]}\\
+  \sembr{\llang{write ($e$)}}^{comp}&=&\sembr{e}_{\mathscr E}^{comp}\llang{[WRITE]}\\
+  \sembr{\llang{$S_1$;$\;S_2$}}^{comp}&=&\sembr{S_1}^{comp}\sembr{S_2}^{comp}
+\end{array}
+\]
+
+\end{document}