Added pattern-matching in lectures

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:
 

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]

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}

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}
 \]

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}
+

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