diff --git a/doc/01.tex b/doc/01.tex index 43c83be24..bd396b5e7 100644 --- a/doc/01.tex +++ b/doc/01.tex @@ -90,7 +90,7 @@ Semantics of expressions: $\Sigma$ is the set of all states. \end{itemize} -Empty state $\bot$: undefined for any variable. +Empty state $\Lambda$: undefined for any variable. Denotational style of semantic description: diff --git a/doc/02.tex b/doc/02.tex index 078b52665..c6271347c 100644 --- a/doc/02.tex +++ b/doc/02.tex @@ -48,7 +48,7 @@ With the relation ``$\Rightarrow$'' defined we can abbreviate the ``surface'' se \setarrow{\xRightarrow} \[ -\forall S\in\mathscr S,\,\forall \iota\in\mathbb Z^*\;:\;\sembr{S}_{\mathscr S} \iota = o \Leftrightarrow \trans{\inbr{\bot, i, \epsilon}}{S}{\inbr{\_, \_, o}} +\forall S\in\mathscr S,\,\forall \iota\in\mathbb Z^*\;:\;\sembr{S}_{\mathscr S} \iota = o \Leftrightarrow \trans{\inbr{\Lambda, i, \epsilon}}{S}{\inbr{\_, \_, o}} \] @@ -102,7 +102,7 @@ now we have one axiom and six inference rules (one per instruction). As for the statement, with the aid of the relation ``$\Rightarrow$'' we can define the surface semantics of stack machine: \[ -\forall p\in\mathscr P,\,\forall i\in\mathbb Z^*\;:\;\sembr{p}_{SM}\;i=o\Leftrightarrow\trans{\inbr{\epsilon, \inbr{\bot, i, \epsilon}}}{p}{\inbr{\_, \inbr{\_, \_, o}}} +\forall p\in\mathscr P,\,\forall i\in\mathbb Z^*\;:\;\sembr{p}_{SM}\;i=o\Leftrightarrow\trans{\inbr{\epsilon, \inbr{\Lambda, i, \epsilon}}}{p}{\inbr{\_, \inbr{\_, \_, o}}} \] \begin{figure}[t] diff --git a/doc/04.tex b/doc/04.tex index e05b3a0f0..6e8272882 100644 --- a/doc/04.tex +++ b/doc/04.tex @@ -115,7 +115,7 @@ All existing rules have to be rewritten~--- we need to formally add a $\withenv{ Finally, the top-level semantics for the extended stack machine can be redefined as follows: \[ -\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}}}} +\forall p\in\mathscr P,\,\forall i\in\mathbb Z^*\;:\;\sembr{p}_{SM}\;i=o\Leftrightarrow\withenv{p}{\trans{\inbr{\epsilon, \inbr{\lambda, i, \epsilon}}}{p}{\inbr{\_, \inbr{\_, \_, o}}}} \] \subsection{Syntax Extensions} diff --git a/doc/05.tex b/doc/05.tex index 850f48b81..5ed29f898 100644 --- a/doc/05.tex +++ b/doc/05.tex @@ -87,14 +87,14 @@ Then, updating the state: As an empty state, we take the following triple: \[ -\bot=\inbr{\bot,\,\emptyset,\,\bot} +\Lambda=\inbr{\Lambda,\,\emptyset,\,\Lambda} \] Finally, we need two transformations for states: \[ \begin{array}{rcl} - \primi{enter}{\inbr{\sigma_g,\,\_,\,\_}\,S} & = & \inbr{\sigma_g,\,S,\,\bot}\\ + \primi{enter}{\inbr{\sigma_g,\,\_,\,\_}\,S} & = & \inbr{\sigma_g,\,S,\,\Lambda}\\ \primi{leave}{\inbr{\sigma_g,\,\_,\,\_}\,\inbr{\_,\,S,\,\sigma_l}}& = & \inbr{\sigma_g,\,S,\,\sigma_l} \end{array} \] diff --git a/doc/08.tex b/doc/08.tex new file mode 100644 index 000000000..717544532 --- /dev/null +++ b/doc/08.tex @@ -0,0 +1,215 @@ +\section{S-expressions and Pattern Matching} + +S-expressions can be considered as arrays with additionally attached \emph{tags} (of constructors). We denote +the set of all constructors as $\mathscr C$: + +\[ +\mathscr{C}=\{C_1, C_2, \dots\} +\] + +Thus, the set of all S-expressions can be described as + +\[ +\mathscr{S}_{exp}=\mathscr{C}\times\mathscr{A}(\mathscr{V}) +\] + +In the concrete syntax constructors are represented by identifiers started with capital letters (A-Z). As +being represented as augmented arrays, the values of S-expressions can be manipulated by array +primitives (in particular, their elements can be accessed and assigned using square brackets); like arrays +they are stored in abstract memory and accessed via locations. + +\subsection{S-expressions on expression level} + +At the expression level S-expressions are represented by a single additional syntactic form: + +\[ +\mathscr{E} += \mathscr{C}\mathscr{E}^* +\] + +In the concrete syntax this form is represented by expressions ``\lstinline|C (e$_1$, e$_1$, ..., e$_k$)|'' or just ``\lstinline|C|'' +if no constructor arguments are specified. The semantics of this form of expression is straightforward: all arguments are +sequentially evauated left-to right and their values are packed into an array with appropriate tag attached: + +\setsubarrow{_{\mathscr E}} +\arraycolsep=10pt +\[\trule{\begin{array}{c} + \withenv{\Phi}{\trans{c_j}{e_j}{c_{j+1}}},\,j\in [0..k]\\ + \inbr{s,\,\mu,\,l_m,\,i,\,o,\,\_}=c_{k+1} + \end{array} + } + {\withenv{\Phi}{\trans{c_0}{C\mathtt{(}e_0, e_1,...,e_k\mathtt{)}}{\inbr{s,\,\mu\,[l_m\gets(C, (k+1,\,\lambda n.\primi{val}{c_n}))],\,l_{m+1},\,i,\,o,\,l_m}}}} + \ruleno{S$_{exp}$} +\] + + +\subsection{Patterns Matching} + +Pattern-matching is a new control construct which allows to discriminate between different constructors of S-expressions. Pattern-matching is added at +the statement level, its abstract syntax is as follows: + +\[ +\mathscr S += \primi{case}\,\mathscr{E}\,(\mathscr{P}\times\mathscr{S})^* +\] + +Here $\mathscr P$ stands for a new syntactic category~--- \emph{patterns} (see below). In the concrete syntax: + +\begin{lstlisting} + case $e$ of $p_1$ -> $s_1$ | ... | $p_k$ -> $s_k$ esac +\end{lstlisting} + +where $e$~--- expression (\emph{scrutinee}), $p_i$~--- patterns, $s_i$~--- statements. + +The syntactic category of patterns is defined as follows: + +\[ +\mathscr P = \_ \mid \mathscr X \mid C \mathscr{P}^* +\] + +In the concrete syntax: ``\lstinline|_|'', ``\lstinline|x|'', ``\lstinline|C ($p_1$, $p_2$, ..., $p_k$)|'' or just ``\lstinline|C|'', +where $x$~--- variable, $C$~--- constructor, $p_i$~--- patterns. Informally speaking, each pattern describes a +set of S-expressions and a set of bindings of variables to sub sub-expression of each of these expressions. To specify +this precisly we introduce the following semantics for patterns: for a pattern $p$ and abstract memory function $\mu$ we +define + +\[ +\sembr{p}^\mu : \mathscr{V}\to\bot\uplus(2^{\mathscr X}\times(\mathscr{X}\to\mathscr{V})) +\] + +$\sembr{p}^\mu$ defines a procedure to inspect a value $v$; as a result either $\bot$ (which can be interpreted as a witness that $v$ +does not belong to the set of values defined by $p$) or a set of variables in the patterns with their bindings is returned. +The definition is as follows: + +\[ +\begin{array}{rclcl} + \sembr{\_}^\mu\; v &=& \inbr{\emptyset,\,\mbox{empty state}} & & \\ + \sembr{x}^\mu\; v &=& \inbr{\{x\},\, [x \gets v]} & & \\ + \sembr{C (p_1, p_2, \dots, p_k)}^\mu\; l &=& \bigoplus_i\,(\sembr{p_i}^\mu\;v_i) &,& \mu\,(l)=C\,(v_1,v_2,\dots,v_k)\\ + \sembr{p}^\mu\; v &=& \bot &,& \mbox{otherwise} +\end{array} +\] + +where $\bigoplus$ unions the bindings: + +\[ +\begin{array}{rcl} + \bot \oplus \_ & = & \bot \\ + \_ \oplus \bot & = & \bot \\ + \inbr{S_1,\,\sigma_1} \oplus \inbr{S_2,\,\sigma_2} & = & \inbr{S_1\cup S_2,\,\lambda x . \left\{ + \begin{array}{rcl} + \sigma_2\, x &,& x\in S_2\\ + \sigma_1\, x &,& x\in S_1\setminus S_2 + \end{array} + \right.} +\end{array} +\] + +As pattern matching may introduce new bindings, we need also to modify the definition of state: + +\[ +\Sigma=(\mathscr X\to \mathscr V) \times (2^{\mathscr X} \times (\mathscr X\to \mathscr V))^* +\] + + +Now we have one global state and a list of local scopes with sets of variables and their bindings. The redefined state primitives +look like the follows. Evaluating in the state: + + +\[ +\begin{array}{rcl} + \inbr{\sigma_g,\,\epsilon}\;x&=&\sigma_g\;x\\ + \inbr{\sigma_g,\,\inbr{S,\,\sigma_l}::t}\;x&=& + \left\{\begin{array}{rcl} + \sigma_l\;x & , & x\in S\\ + \inbr{\sigma_g,\,t}\;x & , & x\not\in S + \end{array} + \right. +\end{array} +\] + +Updating the state: + +\[ + \inbr{\sigma_g,\,s}[x\gets z]=\primi{update}{\inbr{\sigma_g,\,s}\;\epsilon\;x\;z} +\] + +where $\primi{update}{}$ is defined as follows: + +\[ +\begin{array}{rcl} + \primi{update}{\inbr{\sigma_g,\,\epsilon}\;s\;x\;z}&=&\inbr{\sigma_g[x\gets z],\,s}\\ + \primi{update}{\inbr{\sigma_g,\,\inbr{S,\,\sigma_l}::t}\;s\;x\;z}&=&\left\{ + \begin{array}{rcl} + \inbr{\sigma_g,\,s\llang{@}\inbr{S,\,\sigma_l[x\gets z]}t} &,&x\in S\\ + \primi{update}{\inbr{\sigma_g,\,t}\;s\llang{@}\inbr{S,\,\sigma_l}\;x\;z} &,&x\not\in S + \end{array}\right. +\end{array} +\] + +Empty state: + +\[ +\Lambda=\inbr{\Lambda,\,\epsilon} +\] + +Primitives $\primi{enter}{}$/$\primi{leave}{}$: + +\[ +\begin{array}{rcl} + \primi{enter}{\inbr{\sigma_g,\,\_}\,S} & = & \inbr{\sigma_g,\,\inbr{S,\,\Lambda}}\\ + \primi{leave}{\inbr{\sigma_g,\,\_}\,\inbr{\_,\,t}}& = & \inbr{\sigma_g,\,t} +\end{array} +\] + +We will also need two additional primitives to push/drop new scopes: + +\[ +\begin{array}{rcl} + \primi{push}{\inbr{\sigma_g,\,t}\;s}&=&\inbr{\sigma_g,\,s::t}\\ + \primi{drop}{\inbr{\sigma_g,\,\_::t}}&=&\inbr{\sigma_g,\,t} +\end{array} +\] + +We will also use these primitives for the whole configurations, meaning that they apply only to their state parts and leave +all other components intact. + +To specify big-step semantics for pattern-matching we need a yet another ``intrinsic'' statement +$\primi{leave}{}$ (remember, the first one was ``$\diamond$''). The rules are shown on Fig.~\ref{pattern_matching}; note, +we need an additional transition relation ``${\setsubarrow{_{\mathscr P}}\transarrow{}\subarrow}$'' to reflect the top-down +pattern-matching discipline. + +\begin{figure} + \[\trule{\withenv{\llang{skip},\,\Phi}{\trans{\primi{drop}{c}}{K}{c^\prime}}} + {\withenv{K,\,\Phi}{\trans{c}{\primi{leave}{}}{c^\prime}}} + \ruleno{Leave} + \] + + \[\trule{\begin{array}{cc} + {\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{c^\prime}}} & {\setsubarrow{_{\mathscr P}}\withenv{K,\,\Phi}{\trans{c^\prime}{\inbr{\primi{val}{c^\prime},\,ps}}{c^{\prime\prime}}}} + \end{array} + } + {\withenv{K,\,\Phi}{\trans{c}{\llang{case $\;e\;$ $\;ps$}}{c^{\prime\prime}}}} + \ruleno{Case} + \] + + \setsubarrow{_{\mathscr P}} + + \[\trule{\begin{array}{cc} + \sembr{p}^{\primi{mem}{c}}\;v=r\;(\neq\bot) & \withenv{\primi{leave}{}\diamond K,\,\Phi}{\trans{\primi{push}{c\;r}}{s}{c^\prime}} + \end{array} + } + {\withenv{K,\,\Phi}{\trans{c}{\inbr{v,\,\inbr{p,\,s}::t}}{c^\prime}}} + \ruleno{PatternMatched} + \] + + \[\trule{\begin{array}{cc} + \sembr{p}^{\primi{mem}{c}}\;v=\bot & \withenv{K,\,\Phi}{\trans{c}{\inbr{v,\,t}}{c^\prime}} + \end{array} + } + {\withenv{K,\,\Phi}{\trans{c}{\inbr{v,\,\inbr{p,\,s}::t}}{c^\prime}}} + \ruleno{PatternNotMatched} + \] + + \caption{Continuation-passing Style Semantics for Pattern Matching} + \label{pattern_matching} +\end{figure} + diff --git a/doc/lectures.out b/doc/lectures.out index 22a2ca2f6..50ab82cdd 100755 --- a/doc/lectures.out +++ b/doc/lectures.out @@ -1,22 +1,25 @@ -\BOOKMARK [1][-]{section.1}{Introduction:\040Languages,\040Semantics,\040Interpreters,\040Compilers}{}% 1 -\BOOKMARK [2][-]{subsection.1.1}{Language\040and\040semantics}{section.1}% 2 +\BOOKMARK [1][-]{section.1}{Introduction: Languages, Semantics, Interpreters, Compilers}{}% 1 +\BOOKMARK [2][-]{subsection.1.1}{Language and semantics}{section.1}% 2 \BOOKMARK [2][-]{subsection.1.2}{Interpreters}{section.1}% 3 \BOOKMARK [2][-]{subsection.1.3}{Compilers}{section.1}% 4 -\BOOKMARK [2][-]{subsection.1.4}{The\040first\040example:\040language\040of\040expressions}{section.1}% 5 -\BOOKMARK [1][-]{section.2}{Statements,\040Stack\040Machine,\040Stack\040Machine\040Compiler}{}% 6 +\BOOKMARK [2][-]{subsection.1.4}{The first example: language of expressions}{section.1}% 5 +\BOOKMARK [1][-]{section.2}{Statements, Stack Machine, Stack Machine Compiler}{}% 6 \BOOKMARK [2][-]{subsection.2.1}{Statements}{section.2}% 7 -\BOOKMARK [1][-]{section.3}{Stack\040Machine}{}% 8 -\BOOKMARK [2][-]{subsection.3.1}{A\040Compiler\040for\040the\040Stack\040Machine}{section.3}% 9 -\BOOKMARK [1][-]{section.4}{Structural\040Induction}{}% 10 -\BOOKMARK [2][-]{subsection.4.1}{Structural\040Control\040Flow}{section.4}% 11 -\BOOKMARK [2][-]{subsection.4.2}{Extended\040Stack\040Machine}{section.4}% 12 -\BOOKMARK [2][-]{subsection.4.3}{Syntax\040Extensions}{section.4}% 13 +\BOOKMARK [1][-]{section.3}{Stack Machine}{}% 8 +\BOOKMARK [2][-]{subsection.3.1}{A Compiler for the Stack Machine}{section.3}% 9 +\BOOKMARK [1][-]{section.4}{Structural Induction}{}% 10 +\BOOKMARK [2][-]{subsection.4.1}{Structural Control Flow}{section.4}% 11 +\BOOKMARK [2][-]{subsection.4.2}{Extended Stack Machine}{section.4}% 12 +\BOOKMARK [2][-]{subsection.4.3}{Syntax Extensions}{section.4}% 13 \BOOKMARK [1][-]{section.5}{Procedures}{}% 14 -\BOOKMARK [1][-]{section.6}{Extended\040Stack\040Machine}{}% 15 +\BOOKMARK [1][-]{section.6}{Extended Stack Machine}{}% 15 \BOOKMARK [1][-]{section.7}{Functions}{}% 16 -\BOOKMARK [2][-]{subsection.7.1}{Functions\040in\040Expressions}{section.7}% 17 -\BOOKMARK [2][-]{subsection.7.2}{Return\040Statement}{section.7}% 18 -\BOOKMARK [1][-]{section.8}{Arrays\040and\040strings}{}% 19 -\BOOKMARK [2][-]{subsection.8.1}{Adding\040arrays\040on\040expression\040level}{section.8}% 20 -\BOOKMARK [2][-]{subsection.8.2}{Adding\040arrays\040on\040statement\040level}{section.8}% 21 +\BOOKMARK [2][-]{subsection.7.1}{Functions in Expressions}{section.7}% 17 +\BOOKMARK [2][-]{subsection.7.2}{Return Statement}{section.7}% 18 +\BOOKMARK [1][-]{section.8}{Arrays and strings}{}% 19 +\BOOKMARK [2][-]{subsection.8.1}{Adding arrays on expression level}{section.8}% 20 +\BOOKMARK [2][-]{subsection.8.2}{Adding arrays on statement level}{section.8}% 21 \BOOKMARK [2][-]{subsection.8.3}{Strings}{section.8}% 22 +\BOOKMARK [1][-]{section.9}{S-expressions and Pattern Matching}{}% 23 +\BOOKMARK [2][-]{subsection.9.1}{S-expressions on expression level}{section.9}% 24 +\BOOKMARK [2][-]{subsection.9.2}{Patterns Matching}{section.9}% 25 diff --git a/doc/lectures.pdf b/doc/lectures.pdf index 0d6499723..1e2f56b37 100755 Binary files a/doc/lectures.pdf and b/doc/lectures.pdf differ diff --git a/regression/x86only/Makefile b/regression/x86only/Makefile index 3584822b1..12df5a26d 100644 --- a/regression/x86only/Makefile +++ b/regression/x86only/Makefile @@ -1,4 +1,4 @@ -TESTS=$(basename $(wildcard test*.expr)) +TESTS=$(sort $(basename $(wildcard test*.expr))) RC=../../src/rc.opt diff --git a/regression/x86only/test001.expr b/regression/x86only/test001.expr index 3e1dca2d7..998a9d542 100644 --- a/regression/x86only/test001.expr +++ b/regression/x86only/test001.expr @@ -9,7 +9,7 @@ fun insert (tree, value) { esac } -tree := Empty; +local i, tree = Empty; for i := 0, i <= 10, i := i+1 do printf ("%s\n", tree.string); diff --git a/regression/x86only/test002.expr b/regression/x86only/test002.expr index c0c5b5dc9..9f3ecd3b1 100644 --- a/regression/x86only/test002.expr +++ b/regression/x86only/test002.expr @@ -1,4 +1,6 @@ -fun collect_ints_acc (v, tail) local i { +fun collect_ints_acc (v, tail) { + local i; + case v of a@#unboxed -> return Cons (a, tail) | #string -> return tail diff --git a/regression/x86only/test003.expr b/regression/x86only/test003.expr index d4bab0736..f6a6c05fc 100644 --- a/regression/x86only/test003.expr +++ b/regression/x86only/test003.expr @@ -1,9 +1,9 @@ -lists := [ +local lists = [ {}, {1, 2, 3, 4}, {{1}, {2, 3}, {4, {5, 6}}}, 1 : 2 : 3 : 4 : {} -]; +], i; for i := 0, i