diff --git a/doc/01.tex b/doc/01.tex index fb461b949..ceacbb5aa 100644 --- a/doc/01.tex +++ b/doc/01.tex @@ -1,114 +1,6 @@ -\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} - -\makeatletter - -\makeatother - -\definecolor{shadecolor}{gray}{1.00} -\definecolor{darkgray}{gray}{0.30} - -\newcommand{\set}[1]{\{#1\}} -\newcommand{\angled}[1]{\langle {#1} \rangle} -\newcommand{\fib}{\rightarrow_{\mathit{fib}}} -\newcommand{\fibm}{\Rightarrow_{\mathit{fib}}} -\newcommand{\oo}[1]{{#1}^o} -\newcommand{\inml}[1]{\mbox{\lstinline{#1}}} -\newcommand{\goal}{\mathfrak G} -\newcommand{\inmath}[1]{\mbox{$#1$}} -\newcommand{\sembr}[1]{\llbracket{#1}\rrbracket} - -\newcommand{\withenv}[2]{{#1}\vdash{#2}} -\newcommand{\ruleno}[1]{\eqno[\textsc{#1}]} -\newcommand{\trule}[2]{\dfrac{#1}{#2}} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\newcommand{\nredrule}[3]{ - \begin{array}{cl} - \textsf{[{#1}]}& - \begin{array}{c} - #2 \\ - \hline - \raisebox{-1pt}{\ensuremath{#3}} - \end{array} - \end{array}} - -\newcommand{\naxiom}[2]{ - \begin{array}{cl} - \textsf{[{#1}]} & \raisebox{-1pt}{\ensuremath{#2}} - \end{array}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={fun}{{$\lambda$}}1 {->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Introduction: Languages, Semantics, Interpreters, Compilers\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - -\section{Language and semantics} +\section{Introduction: Languages, Semantics, Interpreters, Compilers} + +\subsection{Language and semantics} A language is a collection of programs. A program is an \emph{abstract syntax tree} (AST), which describes the hierarchy of constructs. An abstract syntax of a programming language describes the format of abstract syntax trees of programs in this language. Thus, a language is a set of constructive @@ -123,7 +15,7 @@ $$ where $\mathscr D$ is some \emph{semantic domain}. The choice of the domain is at our command; for example, for Turing-complete languages $\mathscr D$ can be the set of all partially-recursive (computable) functions. -\section{Interpreters} +\subsection{Interpreters} In reality, the semantics often is described using \emph{interpreters}: @@ -155,7 +47,7 @@ operational, denotational or game semantics, etc.) Pragmatically: if you have a good implementation of a good programming language you trust, you can write interpreters of other languages. -\section{Compilers} +\subsection{Compilers} A compiler is just a language transformer @@ -176,7 +68,7 @@ And, again, we expect compilers to be defined in terms of some implementation la its semantics in ocaml possesses the following property (fill the rest yourself). -\section{The first example: language of expressions} +\subsection{The first example: language of expressions} Abstract syntax: @@ -250,7 +142,3 @@ Important observations: \item This concrete semantics is \emph{strict}: for a binary operator both its arguments are evaluated unconditionally; thus, for example, \lstinline|1 !! x| is undefined in empty state. \end{enumerate} - - - -\end{document} diff --git a/doc/02.tex b/doc/02.tex index 88f3dd4f7..43f117af6 100644 --- a/doc/02.tex +++ b/doc/02.tex @@ -1,118 +1,6 @@ -\documentclass{article} +\section{Statements, Stack Machine, Stack Machine Compiler} -\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} - -\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}} - -\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#2\padding}{#3}} -\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}{#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}} - -\newcommand{\meta}[1]{{\mathcal{#1}}} -\renewcommand{\emptyset}{\varnothing} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={fun}{{$\lambda$}}1 {->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Statements, Stack Machine, Stack Machine Compiler\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - -\section{Statements} +\subsection{Statements} More interesting language~--- a language of simple statements: @@ -225,7 +113,7 @@ As for the statement, with the aid of the relation ``$\Rightarrow$'' we can defi \label{bs_sm} \end{figure} -\section{A Compiler for the Stack Machine} +\subsection{A Compiler for the Stack Machine} A compiler of the statement language into the stack machine is a total mapping @@ -257,5 +145,3 @@ And now the main dish: \sembr{\llang{$S_1$;$\;S_2$}}_{comp}&=&\sembr{S_1}_{comp}\llang{@}\sembr{S_2}_{comp} \end{array} \] - -\end{document} diff --git a/doc/03.tex b/doc/03.tex index cca85795c..1ba5d39e4 100644 --- a/doc/03.tex +++ b/doc/03.tex @@ -1,122 +1,4 @@ -\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}} - -\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#2\padding}{#3}} -\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}{#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} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={fun}{{$\lambda$}}1 {->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Structural Induction\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - -%\section{Structural Induction} - +\section{Structural Induction} \begin{figure} \begin{subfigure}{\textwidth} @@ -285,5 +167,3 @@ configurations, since they are never affected by the remaining instructions. Taking into account the semantics of \llang{BINOP $\otimes$} and applying the compositionality lemma, the theorem follows. \end{itemize} \end{proof} - -\end{document} diff --git a/doc/04.tex b/doc/04.tex index 59786738e..bcfb5cb30 100644 --- a/doc/04.tex +++ b/doc/04.tex @@ -1,121 +1,6 @@ -\documentclass{article} +\title{Control Flow Constructs} -\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}} - -\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#2\padding}{#3}} -\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}{#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} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={fun}{{$\lambda$}}1 {->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Control Flow Constructs\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - -\section{Structural Control Flow} +\subsection{Structural Control Flow} We add a few structural control flow constructs to the language: @@ -143,27 +28,27 @@ In the concrete syntax for the constructs we add the closing keywords ``\llang{i \[\trans{c}{\llang{skip}}{c}\ruleno{Skip$_{bs}$}\] \[ \crule{\trans{c}{\mbox{$S_1$}}{c^\prime}} - {\trans{c}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}} + {\trans{c=\inbr{s, \_, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}} {\sembr{e}\;s\ne 0}\ruleno{If-True$_{bs}$} \] \[ \crule{\trans{c}{\mbox{$S_2$}}{c^\prime}} - {\trans{c}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}} + {\trans{c=\inbr{s, \_, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}} {\sembr{e}\;s=0}\ruleno{If-False$_{bs}$} \] \[ \crule{\trans{c}{\llang{$S$}}{c^\prime},\;\trans{c^\prime}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}} - {\trans{c}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}} + {\trans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}} {\sembr{e}\;s\ne 0}\ruleno{While-True$_{bs}$} \] \[ -\ctrans{c}{\llang{while $\;e\;$ do $\;S\;$}}{c}{\sembr{e}\;s=0}\ruleno{While-False$_{bs}$} +\ctrans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c}{\sembr{e}\;s=0}\ruleno{While-False$_{bs}$} \] \caption{Big-step operational semantics for control flow statements} \label{bs_stmt_cf} \end{figure} -\section{Extended Stack Machine} +\subsection{Extended Stack Machine} In order to compile the extended language into a program for the stack machine the latter has to be extended. First, we introduce a set of label names @@ -223,7 +108,7 @@ Finally, the top-level semantics for the extended stack machine can be redefined \forall p\in\mathscr P,\,\forall i\in\mathbb Z^*\;:\;\sembr{p}_{SM}\;i=o\Leftrightarrow\withenv{p}{\trans{\inbr{\epsilon, \inbr{\bot, i, \epsilon}}}{p}{\inbr{\_, \inbr{\_, \_, o}}}} \] -\section{Syntax Extensions} +\subsection{Syntax Extensions} With the structural control flow constructs already implemented, it is rather simple to ``saturate'' the language with more elaborated control constructs, using the method of \emph{syntactic extension}. Namely, we may introduce the following constructs @@ -331,5 +216,3 @@ loop using syntax extension: \end{tabular} However, for nested \lstinline{repeat} constructs the size of extended program is exponential w.r.t. the nesting depth, which makes the whole idea unreasonable. - -\end{document} diff --git a/doc/05.tex b/doc/05.tex index 631a4e56a..25aa943db 100644 --- a/doc/05.tex +++ b/doc/05.tex @@ -1,120 +1,3 @@ -\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}} - -\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#2\padding}{#3}} -\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}{#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} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for, local}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Procedures\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - \section{Procedures} Procedures are unit-returning functions. We consider adding procedures as a separate step, since introducing full-fledged functions would require @@ -283,4 +166,3 @@ Now we specify additional rules for the new instructions: \[ \withenv{P}{\trans{\inbr{\epsilon,\,st,\,c}}{\llang{END}p}{\inbr{\epsilon,\,st,\,c}}}\ruleno{EndStop$_{SM}$} \] -\end{document} diff --git a/doc/06.tex b/doc/06.tex index 2e8bd9be5..6521a34b3 100644 --- a/doc/06.tex +++ b/doc/06.tex @@ -1,124 +1,6 @@ -\documentclass{article} +\section{Functions} -\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#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} - -\definecolor{light-gray}{gray}{0.90} -\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} - -\lstdefinelanguage{ocaml}{ -keywords={let, begin, end, in, match, type, and, fun, -function, try, with, class, object, method, of, rec, repeat, until, -while, not, do, done, as, val, inherit, module, sig, @type, struct, -if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for, local, return, read, write}, -sensitive=true, -%basicstyle=\small, -commentstyle=\scriptsize\rmfamily, -keywordstyle=\ttfamily\bfseries, -identifierstyle=\ttfamily, -basewidth={0.5em,0.5em}, -columns=fixed, -fontadjust=true, -literate={->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, -morecomment=[s]{(*}{*)} -} - -\lstset{ -mathescape=true, -%basicstyle=\small, -identifierstyle=\ttfamily, -keywordstyle=\bfseries, -commentstyle=\scriptsize\rmfamily, -basewidth={0.5em,0.5em}, -fontadjust=true, -escapechar=!, -language=ocaml -} - -\sloppy - -\newcommand{\ocaml}{\texttt{OCaml}\xspace} - -\theoremstyle{definition} - -\title{Functions\\ - (the first draft) -} - -\author{Dmitry Boulytchev} - -\begin{document} - -\maketitle - -\section{Functions in Expressions} +\subsection{Functions in Expressions} At the syntax level function calls are introduced with the following construct: @@ -177,7 +59,7 @@ The rules inself are summarized in the Fig.~\ref{bs_expr}. Note the use of doubl \label{bs_expr} \end{figure} -\section{Return Statement} +\subsection{Return Statement} In order to make it possible to return values from procedures we add a return statement to the language of statements: @@ -269,12 +151,12 @@ The rules themselves are shown on Fig.~\ref{bs_cps}. Note, the rule for the call \] \[\trule{\begin{array}{c} - {\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}}}\\ - \Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}}\\ - \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, n}}} - \end{array} - } - {\withenv{K,\,\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, n}}}} + {\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}}}\\ + \Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}} \\ + \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, \hbox{---}}}}\\ + \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, \hbox{---}}}{K}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}} + \end{array}} + {\withenv{K,\,\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}} \ruleno{Call} \] @@ -292,5 +174,3 @@ The rules themselves are shown on Fig.~\ref{bs_cps}. Note, the rule for the call \caption{Continuation-passing Style Semantics for Statements} \label{bs_cps} \end{figure} - -\end{document} diff --git a/doc/lectures.tex b/doc/lectures.tex new file mode 100644 index 000000000..a29c722d4 --- /dev/null +++ b/doc/lectures.tex @@ -0,0 +1,128 @@ +\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#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}} + +\definecolor{light-gray}{gray}{0.90} +\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}} + +\lstdefinelanguage{ocaml}{ +keywords={let, begin, end, in, match, type, and, fun, +function, try, with, class, object, method, of, rec, repeat, until, +while, not, do, done, as, val, inherit, module, sig, @type, struct, +if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for, local, return, read, write}, +sensitive=true, +%basicstyle=\small, +commentstyle=\scriptsize\rmfamily, +keywordstyle=\ttfamily\bfseries, +identifierstyle=\ttfamily, +basewidth={0.5em,0.5em}, +columns=fixed, +fontadjust=true, +literate={->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1, +morecomment=[s]{(*}{*)} +} + +\lstset{ +mathescape=true, +%basicstyle=\small, +identifierstyle=\ttfamily, +keywordstyle=\bfseries, +commentstyle=\scriptsize\rmfamily, +basewidth={0.5em,0.5em}, +fontadjust=true, +escapechar=!, +language=ocaml +} + +\sloppy + +\newcommand{\ocaml}{\texttt{OCaml}\xspace} + +\theoremstyle{definition} + +\title{Introduction to Programming Languages, Compilers and Tools} + +\author{Dmitry Boulytchev} + +\begin{document} + +\maketitle + +\input{01} +\input{02} +\input{03} +\input{04} +\input{05} +\input{06} +\input{07} + +\end{document} diff --git a/regression/orig/test050.log b/regression/orig/test050.log new file mode 100644 index 000000000..042e35506 --- /dev/null +++ b/regression/orig/test050.log @@ -0,0 +1 @@ +> 2 diff --git a/regression/test050.expr b/regression/test050.expr new file mode 100644 index 000000000..6430356b2 --- /dev/null +++ b/regression/test050.expr @@ -0,0 +1,5 @@ +n := read (); +x := [1]; +y := [x, x]; +y[1][0] := 2; +write (y[0][0]) \ No newline at end of file diff --git a/regression/test050.input b/regression/test050.input new file mode 100644 index 000000000..573541ac9 --- /dev/null +++ b/regression/test050.input @@ -0,0 +1 @@ +0 diff --git a/src/Language.ml b/src/Language.ml index 33a0fd4ed..f33dca018 100644 --- a/src/Language.ml +++ b/src/Language.ml @@ -11,7 +11,7 @@ open Combinators module Value = struct - @type t = Int of int | String of string | Array of t list | Sexp of string * t list with show + @type t = Int of int | String of bytes | Array of t array | Sexp of string * t list (*with show*) let to_int = function | Int n -> n @@ -34,22 +34,22 @@ module Value = | Sexp (t, _) -> t | _ -> failwith "symbolic expression expected" - let update_string s i x = String.init (String.length s) (fun j -> if j = i then x else s.[j]) - let update_array a i x = List.init (List.length a) (fun j -> if j = i then x else List.nth a j) + let update_string s i x = Bytes.set s i x; s + let update_array a i x = a.(i) <- x; a let string_val v = let buf = Buffer.create 128 in let append s = Buffer.add_string buf s in let rec inner = function | Int n -> append (string_of_int n) - | String s -> append "\""; append s; append "\"" - | Array a -> let n = List.length a in - append "["; List.iteri (fun i a -> (if i > 0 then append ", "); inner a) a; append "]" + | String s -> append "\""; append @@ Bytes.to_string s; append "\"" + | Array a -> let n = Array.length a in + append "["; Array.iteri (fun i a -> (if i > 0 then append ", "); inner a) a; append "]" | Sexp (t, a) -> let n = List.length a in append "`"; append t; (if n > 0 then (append " ("; List.iteri (fun i a -> (if i > 0 then append ", "); inner a) a; append ")")) in inner v; - Buffer.contents buf + Bytes.of_string @@ Buffer.contents buf end @@ -125,13 +125,13 @@ module Builtin = | ".elem" -> let [b; j] = args in (st, i, o, let i = Value.to_int j in Some (match b with - | Value.String s -> Value.of_int @@ Char.code s.[i] - | Value.Array a -> List.nth a i + | Value.String s -> Value.of_int @@ Char.code (Bytes.get s i) + | Value.Array a -> a.(i) | Value.Sexp (_, a) -> List.nth a i ) ) - | ".length" -> (st, i, o, Some (Value.of_int (match List.hd args with Value.Sexp (_, a) | Value.Array a -> List.length a | Value.String s -> String.length s))) - | ".array" -> (st, i, o, Some (Value.of_array args)) + | ".length" -> (st, i, o, Some (Value.of_int (match List.hd args with Value.Sexp (_, a) -> List.length a | Value.Array a -> Array.length a | Value.String s -> Bytes.length s))) + | ".array" -> (st, i, o, Some (Value.of_array @@ Array.of_list args)) | ".stringval" -> let [a] = args in (st, i, o, Some (Value.of_string @@ Value.string_val a)) end @@ -202,7 +202,7 @@ module Expr = let rec eval env ((st, i, o, r) as conf) expr = match expr with | Const n -> (st, i, o, Some (Value.of_int n)) - | String s -> (st, i, o, Some (Value.of_string s)) + | String s -> (st, i, o, Some (Value.of_string @@ Bytes.of_string s)) | StringVal s -> let (st, i, o, Some s) = eval env conf s in (st, i, o, Some (Value.of_string @@ Value.string_val s)) @@ -351,7 +351,7 @@ module Stmt = let i = Value.to_int i in (match a with | Value.String s when tl = [] -> Value.String (Value.update_string s i (Char.chr @@ Value.to_int v)) - | Value.Array a -> Value.Array (Value.update_array a i (update (List.nth a i) v tl)) + | Value.Array a -> Value.Array (Value.update_array a i (update a.(i) v tl)) ) in State.update x (match is with [] -> v | _ -> update (State.eval st x) v is) st @@ -378,7 +378,7 @@ module Stmt = | Case (e, bs) -> let (_, _, _, Some v) as conf' = Expr.eval env conf e in let rec branch ((st, i, o, _) as conf) = function - | [] -> failwith (Printf.sprintf "Pattern matching failed: no branch is selected while matching %s\n" (show(Value.t) v)) + | [] -> failwith (Printf.sprintf "Pattern matching failed: no branch is selected while matching %s\n" "" (*show(Value.t) v*)) | (patt, body)::tl -> let rec match_patt patt v st = let update x v = function @@ -389,9 +389,9 @@ module Stmt = | Pattern.Named (x, p), v -> update x v (match_patt p v st ) | Pattern.Wildcard , _ -> st | Pattern.Sexp (t, ps), Value.Sexp (t', vs) when t = t' && List.length ps = List.length vs -> match_list ps vs st - | Pattern.Array ps , Value.Array vs when List.length ps = List.length vs -> match_list ps vs st + | Pattern.Array ps , Value.Array vs when List.length ps = Array.length vs -> match_list ps (Array.to_list vs) st | Pattern.Const n , Value.Int n' when n = n' -> st - | Pattern.String s , Value.String s' when s = s' -> st + | Pattern.String s , Value.String s' when s = Bytes.to_string s' -> st | Pattern.Boxed , Value.String _ | Pattern.Boxed , Value.Array _ | Pattern.UnBoxed , Value.Int _ @@ -483,7 +483,7 @@ let eval (defs, body) i = (object method definition env f args ((st, i, o, r) as conf) = try - let xs, locs, s = snd @@ M.find f m in + let xs, locs, s = snd @@ M.find f m in let st' = List.fold_left (fun st (x, a) -> State.update x a st) (State.enter st (xs @ locs)) (List.combine xs args) in let st'', i', o', r' = Stmt.eval env (st', i, o, r) Skip s in (State.leave st'' st, i', o', r') diff --git a/src/SM.ml b/src/SM.ml index 118548281..10c1b5d46 100644 --- a/src/SM.ml +++ b/src/SM.ml @@ -60,7 +60,7 @@ let rec eval env ((cstack, stack, ((st, i, o) as c)) as conf) = function (match insn with | BINOP op -> let y::x::stack' = stack in eval env (cstack, (Value.of_int @@ Expr.to_func op (Value.to_int x) (Value.to_int y)) :: stack', c) prg' | CONST i -> eval env (cstack, (Value.of_int i)::stack, c) prg' - | STRING s -> eval env (cstack, (Value.of_string s)::stack, c) prg' + | STRING s -> eval env (cstack, (Value.of_string @@ Bytes.of_string s)::stack, c) prg' | SEXP (s, n) -> let vs, stack' = split n stack in eval env (cstack, (Value.sexp s @@ List.rev vs)::stack', c) prg' | LD x -> eval env (cstack, State.eval st x :: stack, c) prg' @@ -87,7 +87,7 @@ let rec eval env ((cstack, stack, ((st, i, o) as c)) as conf) = function | TAG (t, n) -> let x::stack' = stack in eval env (cstack, (Value.of_int @@ match x with Value.Sexp (t', a) when t' = t && List.length a = n -> 1 | _ -> 0) :: stack', c) prg' | ARRAY n -> let x::stack' = stack in - eval env (cstack, (Value.of_int @@ match x with Value.Array a when List.length a = n -> 1 | _ -> 0) :: stack', c) prg' + eval env (cstack, (Value.of_int @@ match x with Value.Array a when Array.length a = n -> 1 | _ -> 0) :: stack', c) prg' | PATT StrCmp -> let x::y::stack' = stack in eval env (cstack, (Value.of_int @@ match x, y with (Value.String xs, Value.String ys) when xs = ys -> 1 | _ -> 0) :: stack', c) prg' | PATT Array -> let x::stack' = stack in