| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Sat, 17 Oct 2020 13:14:19 +0100 | |
| changeset 782 | be79edaf06e1 | 
| parent 743 | f063a6cd5d91 | 
| child 785 | 6fce7c99ebfa | 
| permissions | -rw-r--r-- | 
| 661 | 1  | 
% !TEX program = xelatex  | 
| 743 | 2  | 
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
 | 
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
3  | 
\usepackage{../slides}
 | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
4  | 
\usepackage{../graphics}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
145 
diff
changeset
 | 
5  | 
\usepackage{../langs}
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
145 
diff
changeset
 | 
6  | 
\usepackage{../data}
 | 
| 33 | 7  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
8  | 
\hfuzz=220pt  | 
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
9  | 
|
| 
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
10  | 
\pgfplotsset{compat=1.11}
 | 
| 
145
 
920f675b4ed1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
144 
diff
changeset
 | 
11  | 
|
| 722 | 12  | 
|
13  | 
% a hand written lexer for SML  | 
|
14  | 
% https://ponyo.org/  | 
|
15  | 
% https://github.com/eatonphil/ponyo/blob/master/src/Sml/Lexer.sml  | 
|
16  | 
||
17  | 
||
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
18  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}  
 | 
| 33 | 19  | 
|
| 445 | 20  | 
\renewcommand{\slidecaption}{CFL 04, King's College London}
 | 
| 33 | 21  | 
|
22  | 
\begin{document}
 | 
|
23  | 
||
24  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
25  | 
\begin{frame}[t]
 | 
| 33 | 26  | 
\frametitle{%
 | 
27  | 
  \begin{tabular}{@ {}c@ {}}
 | 
|
28  | 
\\[-3mm]  | 
|
| 445 | 29  | 
\LARGE Compilers and \\[-2mm]  | 
| 743 | 30  | 
\LARGE Formal Languages\\[3mm]  | 
| 33 | 31  | 
  \end{tabular}}
 | 
32  | 
||
33  | 
\normalsize  | 
|
34  | 
  \begin{center}
 | 
|
35  | 
  \begin{tabular}{ll}
 | 
|
| 660 | 36  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 743 | 37  | 
%Office Hours: & Thursdays 12 -- 14\\  | 
38  | 
%Location: & N7.07 (North Wing, Bush House)\\  | 
|
| 660 | 39  | 
Slides \& Progs: & KEATS (also homework is there)\\  | 
| 33 | 40  | 
  \end{tabular}
 | 
41  | 
  \end{center}
 | 
|
| 660 | 42  | 
|
| 743 | 43  | 
|
44  | 
  \begin{center}
 | 
|
45  | 
    \begin{tikzpicture}
 | 
|
46  | 
\node[drop shadow,fill=white,inner sep=0pt]  | 
|
47  | 
      {\footnotesize\rowcolors{1}{capri!10}{white}
 | 
|
48  | 
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
 | 
|
49  | 
1 Introduction, Languages & 6 While-Language \\  | 
|
50  | 
2 Regular Expressions, Derivatives & 7 Compilation, JVM \\  | 
|
51  | 
3 Automata, Regular Languages & 8 Compiling Functional Languages \\  | 
|
52  | 
          \cellcolor{blue!50}
 | 
|
53  | 
4 Lexing, Tokenising & 9 Optimisations \\  | 
|
54  | 
5 Grammars, Parsing & 10 LLVM \\ \hline  | 
|
55  | 
        \end{tabular}%
 | 
|
56  | 
};  | 
|
57  | 
    \end{tikzpicture}
 | 
|
58  | 
  \end{center}
 | 
|
| 
270
 
4dbeaf43031d
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
59  | 
\end{frame}
 | 
| 574 | 60  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
61  | 
||
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
62  | 
|
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
63  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
144
 
0cb61bed557d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
142 
diff
changeset
 | 
64  | 
\begin{frame}[c]
 | 
| 661 | 65  | 
\frametitle{Coursework}
 | 
66  | 
||
67  | 
\begin{itemize}
 | 
|
68  | 
\item \bl{$\der\,c\,(r^+) \dn \der\,c (r\cdot r^*)$}\quad given
 | 
|
69  | 
that \bl{$r^+ \dn r\cdot r^*$}
 | 
|
70  | 
\end{itemize}\bigskip\pause
 | 
|
71  | 
||
72  | 
\begin{center}
 | 
|
73  | 
\begin{tabular}{lcl}
 | 
|
74  | 
\bl{$\der\,c\,(r\cdot r^*)$} & \bl{$\dn$} & 
 | 
|
75  | 
\only<2-4>{if \bl{$nullable\,r$}}%
 | 
|
76  | 
\only<5>{\bl{$(\der\,c\,r)\cdot r^*$}}\\
 | 
|
77  | 
& &  | 
|
78  | 
 \only<2>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, \der\,c\,(r^*)$}}%
 | 
|
79  | 
 \only<3>{then \bl{$(\der\,c\,r)\cdot r^* \,+\, (\der\,c\,r)\cdot r^*$}}%
 | 
|
80  | 
 \only<4>{then \bl{$(\der\,c\,r)\cdot r^*$}}\\
 | 
|
81  | 
 & & \only<2-4>{else \bl{$(\der\,c\,r)\cdot r^*$}}
 | 
|
82  | 
\end{tabular}  
 | 
|
83  | 
\end{center}  
 | 
|
84  | 
\end{frame}
 | 
|
85  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
86  | 
||
87  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
88  | 
\begin{frame}[c]
 | 
|
89  | 
  \frametitle{Coursework (2)}
 | 
|
90  | 
||
91  | 
  \begin{itemize}
 | 
|
92  | 
  \item \bl{\texttt{CFUN(f: Char => Boolean)}}
 | 
|
93  | 
  \end{itemize}\medskip
 | 
|
94  | 
||
95  | 
  \begin{center}
 | 
|
96  | 
  \begin{tabular}{l}
 | 
|
97  | 
  \bl{\texttt{CHAR(c: Char)}} \bl{$\dn$}\\
 | 
|
98  | 
     \quad\bl{\texttt{CFUN(\_ == c)}}\medskip\\
 | 
|
99  | 
  \bl{\texttt{RANGE(cs: Set[Char])}} \bl{$\dn$}\\
 | 
|
100  | 
     \quad\bl{\texttt{CFUN(cs.contains(\_))}}\medskip\\
 | 
|
101  | 
  \bl{\texttt{ALL}} \bl{$\dn$}\\
 | 
|
102  | 
     \quad\bl{\texttt{CFUN((c: Char) => true)}}\\
 | 
|
103  | 
  \end{tabular}  
 | 
|
104  | 
  \end{center}  
 | 
|
105  | 
\end{frame}
 | 
|
106  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 743 | 107  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
108  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
109  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
110  | 
\begin{frame}[c]
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
111  | 
\frametitle{The Goal of this Course}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
112  | 
\mbox{}\\[-26mm]\mbox{}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
113  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
114  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
115  | 
  \begin{tikzpicture}[scale=1,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
116  | 
                      node/.style={
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
117  | 
rectangle,rounded corners=3mm,  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
118  | 
very thick,draw=black!50,  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
119  | 
minimum height=18mm, minimum width=20mm,  | 
| 743 | 120  | 
top color=white,bottom color=black!20,drop shadow}]  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
121  | 
|
| 578 | 122  | 
  \node at (3.05, 1.8) {\Large\bf Write a compiler};
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
123  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
124  | 
  \node (0) at (-2.3,0) {}; 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
125  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
126  | 
  \node (A) at (0,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
127  | 
  \node [below right] at (A.north west) {lexer};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
128  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
129  | 
  \node (B) at (3,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
130  | 
\node [below right=1mm] at (B.north west)  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
131  | 
    {\mbox{}\hspace{-1mm}parser};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
132  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
133  | 
  \node (C) at (6,0)  [node] {};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
134  | 
\node [below right] at (C.north west)  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
135  | 
    {\mbox{}\hspace{-1mm}code gen};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
136  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
137  | 
  \node (1) at (8.4,0) {}; 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
138  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
139  | 
\draw [->,line width=4mm] (0) -- (A);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
140  | 
\draw [->,line width=4mm] (A) -- (B);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
141  | 
\draw [->,line width=4mm] (B) -- (C);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
142  | 
\draw [->,line width=4mm] (C) -- (1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
143  | 
  \end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
144  | 
  \end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
145  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
146  | 
Today a lexer.  | 
| 579 | 147  | 
|
148  | 
\only<2>{
 | 
|
149  | 
\begin{textblock}{1}(6,9.8)
 | 
|
150  | 
\begin{tabular}{c}
 | 
|
151  | 
\includegraphics[scale=0.13]{../pics/rosetta.jpg}\\[-2mm]
 | 
|
152  | 
\footnotesize lexing $\Rightarrow$ recognising words (Stone of Rosetta)  | 
|
153  | 
\end{tabular}
 | 
|
154  | 
\end{textblock}}
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
155  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
156  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
157  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
158  | 
\begin{frame}[c]
 | 
| 578 | 159  | 
\frametitle{Regular Expressions}
 | 
160  | 
||
161  | 
In programming languages they are often used to recognise:\medskip  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
162  | 
|
| 578 | 163  | 
\begin{itemize}
 | 
| 662 | 164  | 
\item operands, digits  | 
| 578 | 165  | 
\item identifiers  | 
166  | 
\item numbers (non-leading zeros)  | 
|
167  | 
\item keywords  | 
|
168  | 
\item comments  | 
|
169  | 
\end{itemize}\bigskip
 | 
|
170  | 
||
171  | 
\mbox{}\hfill\bl{\url{http://www.regexper.com}}
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
172  | 
\end{frame}
 | 
| 578 | 173  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
174  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
175  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
176  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
177  | 
\begin{frame}[c]
 | 
| 521 | 178  | 
\frametitle{Lexing: Test Case}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
179  | 
|
| 743 | 180  | 
??%\mbox{\lstinputlisting[language=While]{../progs/fib.while}}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
181  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
182  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
183  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
184  | 
|
| 578 | 185  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
186  | 
%\begin{frame}[c]
 | 
|
187  | 
%\frametitle{?? Test Case}
 | 
|
188  | 
%  | 
|
189  | 
%\mbox{\lstinputlisting[language=While]{../progs/collatz.while}}
 | 
|
190  | 
%  | 
|
191  | 
%\end{frame}
 | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
192  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
193  | 
|
| 35 | 194  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
195  | 
\begin{frame}[t]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
196  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
197  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
198  | 
\begin{center}\large
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
199  | 
\code{"if true then then 42 else +"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
200  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
201  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
202  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
203  | 
\begin{tabular}{@{}l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
204  | 
KEYWORD: \\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
205  | 
\hspace{5mm}{if}, {then}, {else},\\ 
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
206  | 
WHITESPACE:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
207  | 
\hspace{5mm}{" "}, {$\backslash$n},\\ 
 | 
| 521 | 208  | 
IDENTIFIER:\\  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
209  | 
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$\\ 
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
210  | 
NUM:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
211  | 
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
212  | 
OP:\\  | 
| 521 | 213  | 
\hspace{5mm}+, -, *, \%, <, <=\\
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
214  | 
COMMENT:\\  | 
| 
277
 
8eb3261294ba
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
274 
diff
changeset
 | 
215  | 
\hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
216  | 
\end{tabular}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
217  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
218  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
219  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
220  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
221  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
222  | 
\begin{frame}[t]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
223  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
224  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
225  | 
\begin{center}\large
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
226  | 
\code{"if true then then 42 else +"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
227  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
228  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
229  | 
\only<1>{
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
230  | 
\small\begin{tabular}{l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
231  | 
KEYWORD(if),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
232  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
233  | 
IDENT(true),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
234  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
235  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
236  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
237  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
238  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
239  | 
NUM(42),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
240  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
241  | 
KEYWORD(else),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
242  | 
WHITESPACE,\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
243  | 
OP(+)  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
244  | 
\end{tabular}}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
245  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
246  | 
\only<2>{
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
247  | 
\small\begin{tabular}{l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
248  | 
KEYWORD(if),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
249  | 
IDENT(true),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
250  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
251  | 
KEYWORD(then),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
252  | 
NUM(42),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
253  | 
KEYWORD(else),\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
254  | 
OP(+)  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
255  | 
\end{tabular}}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
256  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
257  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
258  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
259  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
260  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
261  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
262  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
263  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
264  | 
There is one small problem with the tokenizer. How should we  | 
| 578 | 265  | 
tokenize\ldots?  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
266  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
267  | 
\begin{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
268  | 
\large\code{"x-3"}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
269  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
270  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
271  | 
\tt  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
272  | 
\begin{tabular}{@{}l}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
273  | 
ID: \ldots\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
274  | 
OP:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
275  | 
\hspace{5mm}\texttt{"+"}, \texttt{"-"}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
276  | 
NUM:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
277  | 
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {''0''}\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
278  | 
NUMBER:\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
279  | 
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
280  | 
\end{tabular}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
281  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
282  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
283  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
284  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
285  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
286  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
287  | 
The same problem with\medskip  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
288  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
289  | 
\[  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
290  | 
\bl{(ab + a) \cdot (c + bc)}
 | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
291  | 
\]\medskip  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
292  | 
|
| 662 | 293  | 
and the string $\bl{abc}$.\pause\bigskip
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
294  | 
|
| 662 | 295  | 
Or, keywords are \code{if} etc and identifiers are 
 | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
296  | 
letters followed by ``letters + numbers + \_''$^*$  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
297  | 
|
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
298  | 
\[  | 
| 578 | 299  | 
\bl{if}\qquad\bl{iffoo}
 | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
300  | 
\]  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
301  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
302  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
303  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
304  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
305  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
306  | 
\begin{frame}[c]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
307  | 
\frametitle{POSIX: Two Rules}
 | 
| 33 | 308  | 
|
| 38 | 309  | 
\begin{itemize}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
310  | 
\item Longest match rule (``maximal munch rule''): The  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
311  | 
longest initial substring matched by any regular expression is taken  | 
| 
278
 
c7890e677e06
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
277 
diff
changeset
 | 
312  | 
as the next token.\bigskip  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
313  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
314  | 
\item Rule priority:  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
315  | 
For a particular longest initial substring, the first regular  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
316  | 
expression that can match determines the token.  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
317  | 
\end{itemize}\bigskip\bigskip\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
318  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
319  | 
\small  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
320  | 
\hfill most posix matchers are buggy\\  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
321  | 
\footnotesize  | 
| 
353
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
322  | 
\hfill  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
323  | 
\url{http://www.haskell.org/haskellwiki/Regex_Posix}
 | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
324  | 
\smallskip\pause  | 
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
325  | 
|
| 
 
b88670c5d04b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
352 
diff
changeset
 | 
326  | 
\hfill \small traditional lexers are fast, but hairy  | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
327  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
328  | 
%\url{http://www.technologyreview.com/tr10/?year=2011}  
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
329  | 
%finite deterministic automata/ nondeterministic automaton  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
330  | 
%\item problem with infix operations, for example i-12  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
331  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
332  | 
\end{frame}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
333  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
334  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
335  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
336  | 
\begin{frame}[c]
 | 
| 581 | 337  | 
\frametitle{Sulzmann \& Lu Matcher}
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
338  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
339  | 
We want to match the string \bl{$abc$} using \bl{$r_1$}:
 | 
| 38 | 340  | 
|
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
341  | 
\begin{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
342  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
343  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
344  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
345  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
346  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
347  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
348  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
349  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
 | 
| 521 | 350  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable?$}}};\pause
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
351  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
352  | 
\draw[->,line width=1mm] (r4) -- (v4);\pause  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
353  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
354  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
355  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
356  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
357  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
358  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
359  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
360  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
361  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
362  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
272
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
363  | 
\end{tikzpicture}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
364  | 
\end{center}
 | 
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
365  | 
|
| 
 
1446bc47a294
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
270 
diff
changeset
 | 
366  | 
\end{frame}
 | 
| 33 | 367  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
368  | 
||
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
369  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
370  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
371  | 
\frametitle{Regexes and Values}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
372  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
373  | 
Regular expressions and their corresponding values:  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
374  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
375  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
376  | 
\begin{columns}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
377  | 
\begin{column}{3cm}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
378  | 
\begin{tabular}{@{}rrl@{}}
 | 
| 445 | 379  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
 | 
380  | 
           & \bl{$\mid$} & \bl{$\ONE$}   \\
 | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
381  | 
           & \bl{$\mid$} & \bl{$c$}          \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
382  | 
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
383  | 
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
384  | 
\\  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
385  | 
           & \bl{$\mid$} & \bl{$r^*$}         \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
386  | 
\\  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
387  | 
  \end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
388  | 
\end{column}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
389  | 
\begin{column}{3cm}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
390  | 
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
391  | 
  \bl{$v$} & \bl{$::=$}  & \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
392  | 
           &             & \bl{$Empty$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
393  | 
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
 | 
| 
279
 
f406c6677b8c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
278 
diff
changeset
 | 
394  | 
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
395  | 
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
396  | 
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
 | 
| 578 | 397  | 
           & \bl{$\mid$} & \bl{$Stars\,[]$}      \\
 | 
398  | 
           & \bl{$\mid$} & \bl{$Stars\,[v_1,\ldots\,v_n]$} \\
 | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
399  | 
  \end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
400  | 
\end{column}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
401  | 
\end{columns}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
402  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
403  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
404  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
405  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
406  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
407  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
408  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
409  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
410  | 
{\small\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
411  | 
xleftmargin=-5mm] {../progs/app01.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
412  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
413  | 
{\small\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
414  | 
xleftmargin=-5mm] {../progs/app02.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
415  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
416  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
417  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
418  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
419  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
420  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
421  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
422  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
423  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
424  | 
\begin{textblock}{10}(3,5)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
425  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
426  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
427  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
428  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
429  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
430  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
431  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
432  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
433  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
434  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
435  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
436  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
437  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
438  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
439  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
440  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
441  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
442  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
443  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
444  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
445  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
446  | 
\end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
447  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
448  | 
|
| 662 | 449  | 
\only<1->{
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
450  | 
\begin{textblock}{6}(1,0.8)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
451  | 
\begin{bubble}[6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
452  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
453  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
454  | 
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
 | 
| 445 | 455  | 
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
 | 
456  | 
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
 | 
|
457  | 
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
458  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
459  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
460  | 
\end{textblock}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
461  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
462  | 
\only<2->{
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
463  | 
\begin{textblock}{6}(5,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
464  | 
\begin{bubble}[7.6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
465  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
466  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
467  | 
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
468  | 
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
469  | 
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
470  | 
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
471  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
472  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
473  | 
\end{textblock}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
474  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
475  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
476  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
477  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
478  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
479  | 
\frametitle{Flatten}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
480  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
481  | 
Obtaining the string underlying a value:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
482  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
483  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
484  | 
\begin{tabular}{lcl}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
485  | 
  \bl{$|Empty|$}     & \bl{$\dn$} & \bl{$[]$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
486  | 
  \bl{$|Char(c)|$}   & \bl{$\dn$} & \bl{$[c]$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
487  | 
  \bl{$|Left(v)|$}   & \bl{$\dn$} & \bl{$|v|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
488  | 
  \bl{$|Right(v)|$}  & \bl{$\dn$} & \bl{$|v|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
489  | 
  \bl{$|Seq(v_1,v_2)|$}& \bl{$\dn$} & \bl{$|v_1| \,@\, |v_2|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
490  | 
  \bl{$|[v_1,\ldots ,v_n]|$} & \bl{$\dn$} & \bl{$|v_1| \,@\ldots @\, |v_n|$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
491  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
492  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
493  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
494  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
495  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
496  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
497  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
498  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
499  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
500  | 
\begin{textblock}{10}(3,5)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
501  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
502  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
503  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
504  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
505  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
506  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
507  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
508  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
509  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
510  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
511  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
512  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
513  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
514  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
515  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
516  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
517  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
518  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
519  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
520  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
521  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
522  | 
\end{tikzpicture}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
523  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
524  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
525  | 
\begin{textblock}{6}(1,0.8)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
526  | 
\begin{bubble}[6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
527  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
528  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
529  | 
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
 | 
| 445 | 530  | 
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
 | 
531  | 
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
 | 
|
532  | 
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
533  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
534  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
535  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
536  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
537  | 
\begin{textblock}{6}(1,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
538  | 
\begin{bubble}[7.6cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
539  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
540  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
541  | 
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
542  | 
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
543  | 
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
544  | 
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
545  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
546  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
547  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
548  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
549  | 
\begin{textblock}{6}(12,11.4)
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
550  | 
\begin{bubble}[2cm]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
551  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
552  | 
\begin{tabular}{ll}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
553  | 
\bl{$|v_1|$}: & \bl{$abc$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
554  | 
\bl{$|v_2|$}: & \bl{$bc$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
555  | 
\bl{$|v_3|$}: & \bl{$c$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
556  | 
\bl{$|v_4|$}: & \bl{$[]$}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
557  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
558  | 
\end{bubble}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
559  | 
\end{textblock}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
560  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
561  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
562  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
563  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
564  | 
|
| 662 | 565  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
566  | 
\begin{frame}[c]
 | 
|
567  | 
  \frametitle{Mkeps}
 | 
|
568  | 
||
569  | 
Finding a (posix) value for recognising the empty string:  | 
|
570  | 
||
571  | 
  \begin{center}
 | 
|
572  | 
  \begin{tabular}{lcl}
 | 
|
573  | 
    \bl{$mkeps\,(\ONE)$}  & \bl{$\dn$}  & \bl{$Empty$}\\
 | 
|
574  | 
    \bl{$mkeps\,(r_1 + r_2)$} & \bl{$\dn$}  & \bl{if $nullable(r_1)$}  \\
 | 
|
575  | 
                            &             & \bl{then $Left(mkeps(r_1))$}\\
 | 
|
576  | 
                            &             & \bl{else $Right(mkeps(r_2))$}\\
 | 
|
577  | 
    \bl{$mkeps\,(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$Seq(mkeps(r_1),mkeps(r_2))$}\\
 | 
|
578  | 
    \bl{$mkeps\,(r^*)$}      & \bl{$\dn$} & \bl{$Stars\,[]$}  \\
 | 
|
579  | 
  \end{tabular}
 | 
|
580  | 
  \end{center}
 | 
|
581  | 
||
582  | 
  \end{frame}
 | 
|
583  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
584  | 
||
585  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
586  | 
  \begin{frame}[c]
 | 
|
587  | 
  \frametitle{Inject}
 | 
|
588  | 
||
589  | 
  Injecting (``Adding'') a character to a value\\[-12mm]\mbox{}
 | 
|
590  | 
||
591  | 
  \begin{center}
 | 
|
592  | 
  \begin{tabular}{@{\hspace{-3mm}}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
 | 
|
593  | 
    \bl{$inj\,(c)\,c\,(Empty)$} & \bl{$\dn$}  & \bl{$Char\,c$}\\
 | 
|
594  | 
    \bl{$inj\,(r_1 + r_2)\,c\,(Left(v))$} & \bl{$\dn$}  & \bl{$Left(inj\,r_1\,c\,v)$}\\
 | 
|
595  | 
    \bl{$inj\,(r_1 + r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Right(inj\,r_2\,c\,v)$}\\
 | 
|
596  | 
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Seq(v_1,v_2))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
 | 
|
597  | 
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Left(Seq(v_1,v_2)))$} & \bl{$\dn$}  & \bl{$Seq(inj\,r_1\,c\,v_1,v_2)$}\\
 | 
|
598  | 
    \bl{$inj\,(r_1 \cdot r_2)\,c\,(Right(v))$} & \bl{$\dn$}  & \bl{$Seq(mkeps(r_1),inj\,r_2\,c\,v)$}\\
 | 
|
599  | 
    \bl{$inj\,(r^*)\,c\,(Seq(v,Stars\,vs))$} & \bl{$\dn$}  & \bl{$Stars\,(inj\,r\,c\,v\,::\,vs)$}\\
 | 
|
600  | 
  \end{tabular}
 | 
|
601  | 
  \end{center}\bigskip
 | 
|
602  | 
||
603  | 
\footnotesize  | 
|
604  | 
  \begin{tabular}{l@{\hspace{2mm}}l}
 | 
|
605  | 
  \bl{$inj$}: & 1st arg $\mapsto$ a rexp; 2nd arg $\mapsto$ a character; 
 | 
|
606  | 
3rd arg $\mapsto$ a value\\  | 
|
607  | 
& result $\mapsto$ a value  | 
|
608  | 
  \end{tabular}
 | 
|
609  | 
  \end{frame}
 | 
|
610  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
611  | 
||
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
612  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
613  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
614  | 
\frametitle{Lexing}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
615  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
616  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
617  | 
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
618  | 
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
619  | 
  \bl{$lex\,r\,c::s$} & \bl{$\dn$}  & \bl{$inj\,r\,c\,lex(der(c,r), s)$}\\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
620  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
621  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
622  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
623  | 
\footnotesize  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
624  | 
\bl{$lex$}: returns a value
 | 
| 
280
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
625  | 
|
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
626  | 
\begin{center}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
627  | 
\begin{tikzpicture}[scale=2,node distance=1.0cm,every node/.style={minimum size=6mm}]
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
628  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
629  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
630  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
631  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
632  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
633  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
634  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
635  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
636  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
637  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
638  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
639  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
640  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
641  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
642  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
643  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
644  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
645  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
646  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
647  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
648  | 
\end{tikzpicture}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
649  | 
\end{center}
 | 
| 
 
267bd65b2e29
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
279 
diff
changeset
 | 
650  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
651  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
652  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
653  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
654  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
655  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
656  | 
\frametitle{Records}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
657  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
658  | 
\begin{itemize}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
659  | 
\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
660  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
661  | 
\item \bl{$nullable(x:r) \dn nullable(r)$}
 | 
| 671 | 662  | 
\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
 | 
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
663  | 
\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
664  | 
\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
665  | 
\end{itemize}\bigskip\bigskip\pause
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
666  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
667  | 
\small  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
668  | 
for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
669  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
670  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
671  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
672  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
673  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
674  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
675  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
676  | 
\begin{itemize}
 | 
| 445 | 677  | 
\item A regular expression for email addresses  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
678  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
679  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
680  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
681  | 
(name: \bl{$[a\mbox{-}z0\mbox{-}9\_\!\_\,.-]^+$})\bl{$\cdot @\cdot$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
682  | 
\qquad(domain: \bl{$[a\mbox{-}z0\mbox{-}9\,.-]^+$}) \bl{$\cdot .\cdot$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
683  | 
\qquad\qquad(top\_level: \bl{$[a\mbox{-}z\,.]^{\{2,6\}}$})
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
684  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
685  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
686  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
687  | 
\bl{\[
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
688  | 
\texttt{christian.urban@kcl.ac.uk}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
689  | 
\]}  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
690  | 
|
| 445 | 691  | 
\item the result environment:  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
692  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
693  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
694  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
695  | 
\bl{$[(name:\texttt{christian.urban}),$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
696  | 
\bl{$\phantom{[}(domain:\texttt{kcl}),$}\\ 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
697  | 
\bl{$\phantom{[}(top\_level:\texttt{ac.uk})]$}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
698  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
699  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
700  | 
\end{itemize}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
701  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
702  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
703  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
704  | 
|
| 
273
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
705  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
706  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
707  | 
\begin{frame}[c]
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
708  | 
\frametitle{While Tokens}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
709  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
710  | 
\begin{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
711  | 
\begin{tabular}{rcl}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
712  | 
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
713  | 
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
714  | 
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
715  | 
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
716  | 
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
717  | 
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
718  | 
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
719  | 
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
720  | 
\end{tabular}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
721  | 
\end{center}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
722  | 
|
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
723  | 
\end{frame}
 | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
724  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
b56d5e4468c0
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
272 
diff
changeset
 | 
725  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
726  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
727  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
728  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
729  | 
\begin{frame}[c]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
730  | 
\frametitle{Simplification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
731  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
732  | 
\begin{itemize}
 | 
| 522 | 733  | 
\item If we simplify after the derivative, then we are building the  | 
| 578 | 734  | 
value for the simplified regular expression, but \alert{\textbf{not}} for the original
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
735  | 
regular expression.  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
736  | 
\end{itemize}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
737  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
738  | 
\begin{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
739  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
740  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
741  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
742  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
743  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
744  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
745  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
746  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
747  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
748  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
749  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
750  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
751  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
752  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
753  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
754  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
755  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
756  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
757  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
758  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
759  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
760  | 
\end{tikzpicture}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
761  | 
\end{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
762  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
763  | 
\small  | 
| 445 | 764  | 
\hspace{4.5cm}\bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
765  | 
$\mapsto$  | 
| 445 | 766  | 
\bl{$\ONE$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
767  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
768  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
769  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
770  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
771  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
772  | 
\begin{frame}[c]
 | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
773  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
774  | 
Normally we would have  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
775  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
776  | 
  \begin{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
777  | 
  \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
778  | 
  \end{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
779  | 
|
| 
452
 
0b707b614dac
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
451 
diff
changeset
 | 
780  | 
and answer how this regular expression matches the empty string  | 
| 578 | 781  | 
with the value  | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
782  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
783  | 
  \begin{center}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
784  | 
  \bl{$Right(Right(Empty))$}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
785  | 
  \end{center}\bigskip
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
786  | 
|
| 578 | 787  | 
  But now we simplify this to \bl{$\ONE$} and would produce \bl{$Empty$} (see \textit{mkeps}).
 | 
| 
447
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
788  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
789  | 
\end{frame}
 | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
790  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
791  | 
|
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
792  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
68769db65185
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
445 
diff
changeset
 | 
793  | 
\begin{frame}[c]
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
794  | 
\frametitle{Rectification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
795  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
796  | 
\def\arraystretch{1.05}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
797  | 
\begin{center}
 | 
| 445 | 798  | 
\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l@{\hspace{8mm}}l}
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
799  | 
& & & \hspace{5mm}rectification \\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
800  | 
& & & \hspace{5mm}functions:\\
 | 
| 445 | 801  | 
\bl{$r \cdot \ZERO$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
 | 
802  | 
\bl{$\ZERO \cdot r$} & $\mapsto$ & \bl{$\ZERO$} & \\ 
 | 
|
803  | 
\bl{$r \cdot \ONE$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,v, f_2\,Empty)$}\\ 
 | 
|
804  | 
\bl{$\ONE \cdot r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Seq(f_1\,Empty, f_2\,v)$}\\ 
 | 
|
805  | 
\bl{$r + \ZERO$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}\\ 
 | 
|
806  | 
\bl{$\ZERO + r$} & $\mapsto$ & \bl{$r$}   & \bl{$\lambda f_1\,f_2\,v.\, Right(f_2\,v)$}\\
 | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
807  | 
\bl{$r + r$} & $\mapsto$ & \bl{$r$} & \bl{$\lambda f_1\,f_2\,v.\, Left(f_1\,v)$}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
808  | 
\end{tabular}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
809  | 
\end{center}\medskip\pause
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
810  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
811  | 
\small  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
812  | 
old \bl{$simp$} returns a rexp;\\
 | 
| 445 | 813  | 
new \bl{$simp$} returns a rexp and a rectification~function.
 | 
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
814  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
815  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
816  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
817  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
818  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
819  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
820  | 
\frametitle{Rectification}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
821  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
822  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
823  | 
\begin{tabular}{l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
824  | 
\bl{$simp(r)$}:\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
825  | 
\quad case \bl{$r = r_1 + r_2$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
826  | 
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
827  | 
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
 | 
| 445 | 828  | 
\qquad case \bl{$r_{1s} = \ZERO$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
829  | 
       return \bl{$(r_{2s}, \lambda v. \,Right(f_{2s}(v)))$}\\
 | 
| 445 | 830  | 
\qquad case \bl{$r_{2s} = \ZERO$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
831  | 
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
832  | 
\qquad case \bl{$r_{1s} = r_{2s}$}:
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
833  | 
       return \bl{$(r_{1s}, \lambda v. \,Left(f_{1s}(v)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
834  | 
\qquad otherwise:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
835  | 
       return \bl{$(r_{1s} + r_{2s}, f_{alt}(f_{1s}, f_{2s}))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
836  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
837  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
838  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
839  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
840  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
841  | 
\begin{tabular}{l@{\hspace{1mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
842  | 
\bl{$f_{alt}(f_1, f_2) \dn$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
843  | 
\qquad \bl{$\lambda v.\,$} case \bl{$v = Left(v')$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
844  | 
      & return \bl{$Left(f_1(v'))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
845  | 
\qquad \phantom{$\lambda v.\,$} case \bl{$v = Right(v')$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
846  | 
      & return \bl{$Right(f_2(v'))$}\\      
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
847  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
848  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
849  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
850  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
851  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
852  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
853  | 
|
| 445 | 854  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
855  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
856  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
857  | 
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
858  | 
xleftmargin=-5mm] {../progs/app05.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
859  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
860  | 
\end{frame}
 | 
| 445 | 861  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
862  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
863  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
864  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
865  | 
\frametitle{Rectification}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
866  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
867  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
868  | 
\begin{tabular}{@{\hspace{-3mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
869  | 
\bl{$simp(r)$}:\ldots\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
870  | 
\quad case \bl{$r = r_1 \cdot r_2$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
871  | 
\qquad let \bl{$(r_{1s}, f_{1s}) = simp(r_1)$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
872  | 
\qquad \phantom{let} \bl{$(r_{2s}, f_{2s}) = simp(r_2)$}\smallskip\\
 | 
| 445 | 873  | 
\qquad case \bl{$r_{1s} = \ZERO$}: 
 | 
874  | 
       return \bl{$(\ZERO, f_{error})$}\\
 | 
|
875  | 
\qquad case \bl{$r_{2s} = \ZERO$}: 
 | 
|
876  | 
       return \bl{$(\ZERO, f_{error})$}\\
 | 
|
877  | 
\qquad case \bl{$r_{1s} = \ONE$}: 
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
878  | 
return \bl{$(r_{2s}, \lambda v. \,Seq(f_{1s}(Empty), f_{2s}(v)))$}\\
 | 
| 445 | 879  | 
\qquad case \bl{$r_{2s} = \ONE$}: 
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
880  | 
return \bl{$(r_{1s}, \lambda v. \,Seq(f_{1s}(v), f_{2s}(Empty)))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
881  | 
\qquad otherwise:  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
882  | 
       return \bl{$(r_{1s} \cdot r_{2s}, f_{seq}(f_{1s}, f_{2s}))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
883  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
884  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
885  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
886  | 
\small  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
887  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
888  | 
\begin{tabular}{l@{\hspace{1mm}}l}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
889  | 
\bl{$f_{seq}(f_1, f_2) \dn$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
890  | 
\qquad \bl{$\lambda v.\,$ case $v = Seq(v_1, v_2)$}: 
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
891  | 
      & return \bl{$Seq(f_1(v_1), f_2(v_2))$}\\
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
892  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
893  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
894  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
895  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
896  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
897  | 
|
| 451 | 898  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
899  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
900  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
901  | 
{\footnotesize\lstinputlisting[language=Scala,numbers=none,
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
902  | 
xleftmargin=-5mm] {../progs/app06.scala}}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
903  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
904  | 
\end{frame}
 | 
| 451 | 905  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
906  | 
||
907  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
908  | 
\begin{frame}[t]
 | 
|
909  | 
\frametitle{Rectification Example}
 | 
|
910  | 
||
911  | 
\begin{center}
 | 
|
912  | 
\bl{$\only<1>{(b \cdot c)}%
 | 
|
913  | 
     \only<2-3>{(\underline{b \cdot c})}%
 | 
|
914  | 
     \only<1-3>{+}% 
 | 
|
915  | 
     \only<1>{(\ZERO + \ONE)}%
 | 
|
916  | 
     \only<2-3>{(\underline{\ZERO + \ONE})}$}%
 | 
|
917  | 
\only<4->{%
 | 
|
918  | 
\bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
 | 
|
919  | 
}  | 
|
920  | 
$\mapsto$  | 
|
921  | 
\bl{$(b \cdot c) + \ONE$}
 | 
|
922  | 
\end{center}\bigskip
 | 
|
923  | 
||
924  | 
\onslide<3->{%
 | 
|
925  | 
\begin{center}
 | 
|
926  | 
\begin{tabular}{lcl}
 | 
|
927  | 
\bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
 | 
|
928  | 
\bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
 | 
|
929  | 
\end{tabular}
 | 
|
930  | 
\end{center}}
 | 
|
931  | 
||
932  | 
\only<4>{%
 | 
|
933  | 
\begin{center}
 | 
|
934  | 
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
935  | 
\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
 | 
|
936  | 
\quad \bl{$\lambda v.\,$} 
 | 
|
937  | 
        case \bl{$v = Left(v')$}: 
 | 
|
938  | 
      & return \bl{$Left(f_{s1}(v'))$}\\
 | 
|
939  | 
\quad \phantom{$\lambda v.\,$} 
 | 
|
940  | 
        case \bl{$v = Right(v')$}: 
 | 
|
941  | 
      & return \bl{$Right(f_{s2}(v'))$}\\ 
 | 
|
942  | 
\end{tabular}
 | 
|
943  | 
\end{center}}%
 | 
|
944  | 
\only<5->{%
 | 
|
945  | 
\begin{center}
 | 
|
946  | 
\begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
947  | 
\only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
 | 
|
948  | 
\quad \bl{$\lambda v.\,$} 
 | 
|
949  | 
        case \bl{$v = Left(v')$}: 
 | 
|
950  | 
      & return \bl{$Left(v')$}\\
 | 
|
951  | 
\quad \phantom{$\lambda v.\,$} 
 | 
|
952  | 
        case \bl{$v = Right(v')$}: 
 | 
|
953  | 
      & return \bl{$Right(Right(v'))$}\\ 
 | 
|
954  | 
\end{tabular}
 | 
|
955  | 
\end{center}}%
 | 
|
956  | 
||
957  | 
\only<6->{%
 | 
|
958  | 
\begin{center}
 | 
|
959  | 
\begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
 | 
|
960  | 
\bl{$\textit{mkeps}$} simplified case: &
 | 
|
961  | 
\bl{$\textit{Right}(\textit{Empty})$}\\
 | 
|
962  | 
rectified case: &  | 
|
963  | 
\bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
 | 
|
964  | 
\end{tabular}
 | 
|
965  | 
\end{center}}%
 | 
|
966  | 
||
967  | 
\end{frame}
 | 
|
968  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
969  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
970  | 
|
| 
274
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
971  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
972  | 
\begin{frame}[c]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
973  | 
\frametitle{Lexing with Simplification}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
974  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
975  | 
\begin{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
976  | 
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
977  | 
  \bl{$lex\,r\,[]$} & \bl{$\dn$}  & \bl{if $nullable(r)$ then $mkeps(r)$ else $error$}\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
978  | 
  \bl{$lex\,r\,c::s$} & \bl{$\dn$}  & \bl{let $(r', frect) = simp(der(c, r))$}\smallskip\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
979  | 
                      & & \bl{$inj\,r\,c\,(frect(lex(r', s)))$}\\
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
980  | 
\end{tabular}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
981  | 
\end{center}\bigskip
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
982  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
983  | 
\begin{center}\small
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
984  | 
\begin{tikzpicture}[node distance=1.1cm,every node/.style={minimum size=7mm}]
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
985  | 
\node (r1)  {\bl{$r_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
986  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
987  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
988  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
989  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
990  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
991  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
992  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
993  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
994  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
995  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
996  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
997  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
998  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
999  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1000  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1001  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1002  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1003  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1004  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1005  | 
\end{tikzpicture}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1006  | 
\end{center}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1007  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1008  | 
|
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1009  | 
\end{frame}
 | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1010  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
21f0f24424ab
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
273 
diff
changeset
 | 
1011  | 
|
| 451 | 1012  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
1013  | 
\begin{frame}[c]
 | 
|
1014  | 
\frametitle{Environments}
 | 
|
1015  | 
||
1016  | 
Obtaining the ``recorded'' parts of a value:  | 
|
1017  | 
||
1018  | 
\begin{center}
 | 
|
1019  | 
\begin{tabular}{lcl}
 | 
|
1020  | 
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1021  | 
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1022  | 
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1023  | 
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1024  | 
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
 | 
|
| 578 | 1025  | 
  \bl{$env(Stars\,[v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
 | 
| 451 | 1026  | 
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
 | 
1027  | 
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
 | 
|
1028  | 
\end{tabular}
 | 
|
1029  | 
\end{center}
 | 
|
1030  | 
||
1031  | 
\end{frame}
 | 
|
1032  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1033  | 
||
1034  | 
||
1035  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1036  | 
\begin{frame}[c]
 | 
|
1037  | 
\frametitle{While Tokens}
 | 
|
1038  | 
||
1039  | 
\begin{center}
 | 
|
1040  | 
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
 | 
|
1041  | 
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
 | 
|
1042  | 
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
 | 
|
1043  | 
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
 | 
|
1044  | 
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
 | 
|
1045  | 
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
 | 
|
1046  | 
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
 | 
|
1047  | 
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
 | 
|
1048  | 
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
 | 
|
1049  | 
\end{tabular}
 | 
|
1050  | 
\end{center}
 | 
|
1051  | 
||
1052  | 
\end{frame}
 | 
|
1053  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1054  | 
||
1055  | 
||
1056  | 
||
1057  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1058  | 
\begin{frame}[t]
 | 
|
1059  | 
||
1060  | 
\consolas  | 
|
1061  | 
\begin{center}
 | 
|
1062  | 
\code{"if true then then 42 else +"}
 | 
|
1063  | 
\end{center}
 | 
|
1064  | 
||
1065  | 
\only<1>{
 | 
|
1066  | 
\small\begin{tabular}{l}
 | 
|
1067  | 
KEYWORD(if),\\  | 
|
1068  | 
WHITESPACE,\\  | 
|
1069  | 
IDENT(true),\\  | 
|
1070  | 
WHITESPACE,\\  | 
|
1071  | 
KEYWORD(then),\\  | 
|
1072  | 
WHITESPACE,\\  | 
|
1073  | 
KEYWORD(then),\\  | 
|
1074  | 
WHITESPACE,\\  | 
|
1075  | 
NUM(42),\\  | 
|
1076  | 
WHITESPACE,\\  | 
|
1077  | 
KEYWORD(else),\\  | 
|
1078  | 
WHITESPACE,\\  | 
|
1079  | 
OP(+)  | 
|
1080  | 
\end{tabular}}
 | 
|
1081  | 
||
1082  | 
\only<2>{
 | 
|
1083  | 
\small\begin{tabular}{l}
 | 
|
1084  | 
KEYWORD(if),\\  | 
|
1085  | 
IDENT(true),\\  | 
|
1086  | 
KEYWORD(then),\\  | 
|
1087  | 
KEYWORD(then),\\  | 
|
1088  | 
NUM(42),\\  | 
|
1089  | 
KEYWORD(else),\\  | 
|
1090  | 
OP(+)  | 
|
1091  | 
\end{tabular}}
 | 
|
1092  | 
||
1093  | 
\end{frame}
 | 
|
1094  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1095  | 
||
1096  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1097  | 
\begin{frame}[c]
 | 
|
| 521 | 1098  | 
\frametitle{Lexer: Two Rules}
 | 
| 451 | 1099  | 
|
1100  | 
\begin{itemize}
 | 
|
1101  | 
\item Longest match rule (``maximal munch rule''): The  | 
|
1102  | 
longest initial substring matched by any regular expression is taken  | 
|
1103  | 
as next token.\bigskip  | 
|
1104  | 
||
1105  | 
\item Rule priority:  | 
|
1106  | 
For a particular longest initial substring, the first regular  | 
|
1107  | 
expression that can match determines the token.  | 
|
1108  | 
||
1109  | 
\end{itemize}
 | 
|
1110  | 
||
1111  | 
%\url{http://www.technologyreview.com/tr10/?year=2011}
 | 
|
1112  | 
||
1113  | 
%finite deterministic automata/ nondeterministic automaton  | 
|
1114  | 
||
1115  | 
%\item problem with infix operations, for example i-12  | 
|
1116  | 
||
1117  | 
||
1118  | 
\end{frame}
 | 
|
1119  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1120  | 
||
1121  | 
||
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1122  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1123  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1124  | 
\begin{frame}[c]
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1125  | 
\begin{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1126  | 
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
 | 
| 578 | 1127  | 
\bl{$zeroable(\ZERO)$}      & \bl{$\dn$} & \bl{$true$}\\
 | 
1128  | 
\bl{$zeroable(\ONE)$}         & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
|
| 445 | 1129  | 
\bl{$zeroable(c)$}                & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
1130  | 
\bl{$zeroable(r_1 + r_2)$}        & \bl{$\dn$} & \bl{$zeroable(r_1) \wedge zeroable(r_2)$}\\ 
 | 
|
1131  | 
\bl{$zeroable(r_1 \cdot r_2)$}    & \bl{$\dn$} & \bl{$zeroable(r_1) \vee zeroable(r_2)$}\\
 | 
|
1132  | 
\bl{$zeroable(r^*)$}              & \bl{$\dn$} & \bl{$\textit{false}$}\\
 | 
|
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1133  | 
\end{tabular}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1134  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1135  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1136  | 
\begin{center}
 | 
| 445 | 1137  | 
\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
 | 
| 
352
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1138  | 
\end{center}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1139  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1140  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1141  | 
\end{frame}
 | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1142  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1143  | 
|
| 
 
1e1b0fe66107
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
283 
diff
changeset
 | 
1144  | 
|
| 743 | 1145  | 
|
1146  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1147  | 
\begin{frame}[c]
 | 
|
1148  | 
\frametitle{\begin{tabular}{c}Last Week\\[-2mm] 
 | 
|
1149  | 
            Regexes and Values\end{tabular}}
 | 
|
1150  | 
||
1151  | 
Regular expressions and their corresponding values:  | 
|
1152  | 
||
1153  | 
\begin{center}
 | 
|
1154  | 
\begin{columns}
 | 
|
1155  | 
\begin{column}{3cm}
 | 
|
1156  | 
\begin{tabular}{@{}rrl@{}}
 | 
|
1157  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
 | 
|
1158  | 
           & \bl{$\mid$} & \bl{$\ONE$}   \\
 | 
|
1159  | 
           & \bl{$\mid$} & \bl{$c$}          \\
 | 
|
1160  | 
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
 | 
|
1161  | 
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
 | 
|
1162  | 
\\  | 
|
1163  | 
           & \bl{$\mid$} & \bl{$r^*$}         \\
 | 
|
1164  | 
  \end{tabular}
 | 
|
1165  | 
\end{column}
 | 
|
1166  | 
\begin{column}{3cm}
 | 
|
1167  | 
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
 | 
|
1168  | 
  \bl{$v$} & \bl{$::=$}  & \\
 | 
|
1169  | 
           &             & \bl{$Empty$}   \\
 | 
|
1170  | 
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
 | 
|
1171  | 
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
 | 
|
1172  | 
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
 | 
|
1173  | 
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
 | 
|
1174  | 
           & \bl{$\mid$} & \bl{$Stars [v_1,\ldots\,v_n]$} \\
 | 
|
1175  | 
  \end{tabular}
 | 
|
1176  | 
\end{column}
 | 
|
1177  | 
\end{columns}
 | 
|
1178  | 
\end{center}
 | 
|
1179  | 
||
1180  | 
||
1181  | 
\end{frame}
 | 
|
1182  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1183  | 
||
1184  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1185  | 
\begin{frame}[c]
 | 
|
1186  | 
||
1187  | 
\begin{textblock}{10}(3,5)
 | 
|
1188  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
|
1189  | 
\node (r1)  {\bl{$r_1$}};
 | 
|
1190  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
|
1191  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
|
1192  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
|
1193  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
|
1194  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
|
1195  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
|
1196  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
|
1197  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
|
1198  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
|
1199  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
|
1200  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
|
1201  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
|
1202  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
|
1203  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
|
1204  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
|
1205  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
|
1206  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
|
1207  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
|
1208  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
|
1209  | 
\end{tikzpicture}
 | 
|
1210  | 
\end{textblock}
 | 
|
1211  | 
||
1212  | 
\begin{textblock}{6}(1,0.8)
 | 
|
1213  | 
\begin{bubble}[6cm]
 | 
|
1214  | 
\small  | 
|
1215  | 
\begin{tabular}{ll}
 | 
|
1216  | 
\bl{$r_1$}: & \bl{$a \cdot (b \cdot c)$}\\
 | 
|
1217  | 
\bl{$r_2$}: & \bl{$\ONE \cdot (b \cdot c)$}\\
 | 
|
1218  | 
\bl{$r_3$}: & \bl{$(\ZERO \cdot (b \cdot c)) + (\ONE \cdot c)$}\\
 | 
|
1219  | 
\bl{$r_4$}: & \bl{$(\ZERO \cdot (b \cdot c)) + ((\ZERO \cdot c) + \ONE)$}\\
 | 
|
1220  | 
\end{tabular}
 | 
|
1221  | 
\end{bubble}
 | 
|
1222  | 
\end{textblock}
 | 
|
1223  | 
||
1224  | 
\begin{textblock}{6}(1,11.4)
 | 
|
1225  | 
\begin{bubble}[7.6cm]
 | 
|
1226  | 
\small  | 
|
1227  | 
\begin{tabular}{ll}
 | 
|
1228  | 
\bl{$v_1$}: & \bl{$Seq(Char(a), Seq(Char(b), Char(c)))$}\\
 | 
|
1229  | 
\bl{$v_2$}: & \bl{$Seq(Empty, Seq(Char(b), Char(c)))$}\\
 | 
|
1230  | 
\bl{$v_3$}: & \bl{$Right(Seq(Empty, Char(c)))$}\\
 | 
|
1231  | 
\bl{$v_4$}: & \bl{$Right(Right(Empty))$}\\
 | 
|
1232  | 
\end{tabular}
 | 
|
1233  | 
\end{bubble}
 | 
|
1234  | 
\end{textblock}
 | 
|
1235  | 
||
1236  | 
\begin{textblock}{6}(12,11.4)
 | 
|
1237  | 
\begin{bubble}[2cm]
 | 
|
1238  | 
\small  | 
|
1239  | 
\begin{tabular}{ll}
 | 
|
1240  | 
\bl{$|v_1|$}: & \bl{$abc$}\\
 | 
|
1241  | 
\bl{$|v_2|$}: & \bl{$bc$}\\
 | 
|
1242  | 
\bl{$|v_3|$}: & \bl{$c$}\\
 | 
|
1243  | 
\bl{$|v_4|$}: & \bl{$[]$}
 | 
|
1244  | 
\end{tabular}
 | 
|
1245  | 
\end{bubble}
 | 
|
1246  | 
\end{textblock}
 | 
|
1247  | 
||
1248  | 
||
1249  | 
\end{frame}
 | 
|
1250  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1251  | 
||
1252  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1253  | 
\begin{frame}[c]
 | 
|
1254  | 
\frametitle{Simplification}
 | 
|
1255  | 
||
1256  | 
\begin{itemize}
 | 
|
1257  | 
\item If we simplify after the derivative, then we are builing the  | 
|
1258  | 
value for the simplified regular expression, but \emph{not} for the original
 | 
|
1259  | 
regular expression.  | 
|
1260  | 
\end{itemize}
 | 
|
1261  | 
||
1262  | 
\begin{center}
 | 
|
1263  | 
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
 | 
|
1264  | 
\node (r1)  {\bl{$r_1$}};
 | 
|
1265  | 
\node (r2) [right=of r1] {\bl{$r_2$}};
 | 
|
1266  | 
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};
 | 
|
1267  | 
\node (r3) [right=of r2] {\bl{$r_3$}};
 | 
|
1268  | 
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};
 | 
|
1269  | 
\node (r4) [right=of r3] {\bl{$r_4$}};
 | 
|
1270  | 
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};
 | 
|
1271  | 
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$nullable$}}};
 | 
|
1272  | 
\node (v4) [below=of r4] {\bl{$v_4$}};
 | 
|
1273  | 
\draw[->,line width=1mm] (r4) -- (v4);  | 
|
1274  | 
\node (v3) [left=of v4] {\bl{$v_3$}};
 | 
|
1275  | 
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};
 | 
|
1276  | 
\node (v2) [left=of v3] {\bl{$v_2$}};
 | 
|
1277  | 
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};
 | 
|
1278  | 
\node (v1) [left=of v2] {\bl{$v_1$}};
 | 
|
1279  | 
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};
 | 
|
1280  | 
\draw[->,line width=0.5mm] (r3) -- (v3);  | 
|
1281  | 
\draw[->,line width=0.5mm] (r2) -- (v2);  | 
|
1282  | 
\draw[->,line width=0.5mm] (r1) -- (v1);  | 
|
1283  | 
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
 | 
|
1284  | 
\end{tikzpicture}
 | 
|
1285  | 
\end{center}
 | 
|
1286  | 
||
1287  | 
\small  | 
|
1288  | 
\hspace{4.5cm}\bl{$(b \cdot c) + (\ZERO + \ONE)$}
 | 
|
1289  | 
$\mapsto$  | 
|
1290  | 
\bl{$(b \cdot c) + \ONE$}
 | 
|
1291  | 
||
1292  | 
\end{frame}
 | 
|
1293  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1294  | 
||
1295  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1296  | 
% \begin{frame}[t]
 | 
|
1297  | 
||
1298  | 
% \begin{center}
 | 
|
1299  | 
% \bl{$\only<1>{(b \cdot c)}%
 | 
|
1300  | 
%      \only<2-3>{(\underline{b \cdot c})}%
 | 
|
1301  | 
%      \only<1-3>{+}% 
 | 
|
1302  | 
%      \only<1>{(\ZERO + \ONE)}%
 | 
|
1303  | 
%      \only<2-3>{(\underline{\ZERO + \ONE})}$}%
 | 
|
1304  | 
% \only<4->{%
 | 
|
1305  | 
% \bl{$\underline{(b \cdot c) + (\ZERO + \ONE)}$}%
 | 
|
1306  | 
% }  | 
|
1307  | 
% $\mapsto$  | 
|
1308  | 
% \bl{$(b \cdot c) + \ONE$}
 | 
|
1309  | 
% \end{center}\bigskip
 | 
|
1310  | 
||
1311  | 
% \onslide<3->{%
 | 
|
1312  | 
% \begin{center}
 | 
|
1313  | 
% \begin{tabular}{lcl}
 | 
|
1314  | 
% \bl{$f_{s1}$} & \bl{$=$} & \bl{$\lambda v.v$}\\
 | 
|
1315  | 
% \bl{$f_{s2}$} & \bl{$=$} & \bl{$\lambda v. \textit{Right}(v)$}
 | 
|
1316  | 
% \end{tabular}
 | 
|
1317  | 
% \end{center}}
 | 
|
1318  | 
||
1319  | 
% \only<4>{%
 | 
|
1320  | 
% \begin{center}
 | 
|
1321  | 
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
1322  | 
% \bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}\\
 | 
|
1323  | 
% \quad \bl{$\lambda v.\,$} 
 | 
|
1324  | 
%         case \bl{$v = Left(v')$}: 
 | 
|
1325  | 
%       & return \bl{$Left(f_{s1}(v'))$}\\
 | 
|
1326  | 
% \quad \phantom{$\lambda v.\,$} 
 | 
|
1327  | 
%         case \bl{$v = Right(v')$}: 
 | 
|
1328  | 
%       & return \bl{$Right(f_{s2}(v'))$}\\ 
 | 
|
1329  | 
% \end{tabular}
 | 
|
1330  | 
% \end{center}}%
 | 
|
1331  | 
% \only<5->{%
 | 
|
1332  | 
% \begin{center}
 | 
|
1333  | 
% \begin{tabular}{@{}l@{\hspace{1mm}}l@{}}
 | 
|
1334  | 
% \only<5->{\phantom{\bl{$f_{alt}(f_{s1}, f_{s2}) \dn$}}}\\
 | 
|
1335  | 
% \quad \bl{$\lambda v.\,$} 
 | 
|
1336  | 
%         case \bl{$v = Left(v')$}: 
 | 
|
1337  | 
%       & return \bl{$Left(v')$}\\
 | 
|
1338  | 
% \quad \phantom{$\lambda v.\,$} 
 | 
|
1339  | 
%         case \bl{$v = Right(v')$}: 
 | 
|
1340  | 
%       & return \bl{$Right(Right(v'))$}\\ 
 | 
|
1341  | 
% \end{tabular}
 | 
|
1342  | 
% \end{center}}%
 | 
|
1343  | 
||
1344  | 
% \only<6->{%
 | 
|
1345  | 
% \begin{center}
 | 
|
1346  | 
% \begin{tabular}{@{}l@{\hspace{4mm}}l@{}}
 | 
|
1347  | 
% \bl{$\textit{mkeps}$} simplified case: &
 | 
|
1348  | 
% \bl{$\textit{Right}(\textit{Empty})$}\\
 | 
|
1349  | 
% rectified case: &  | 
|
1350  | 
% \bl{$\textit{Right}(\textit{Right}(\textit{Empty}))$}
 | 
|
1351  | 
% \end{tabular}
 | 
|
1352  | 
% \end{center}}%
 | 
|
1353  | 
||
1354  | 
% \end{frame}
 | 
|
1355  | 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1356  | 
||
1357  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1358  | 
\begin{frame}[c]
 | 
|
1359  | 
\frametitle{Records}
 | 
|
1360  | 
||
1361  | 
\begin{itemize}
 | 
|
1362  | 
\item new regex: \bl{$(x:r)$}\hspace{7mm}new value: \bl{$Rec(x,v)$}\medskip\pause
 | 
|
1363  | 
||
1364  | 
\item \bl{$nullable(x:r) \dn nullable(r)$}
 | 
|
1365  | 
\item \bl{$der\,c\,(x:r) \dn der\,c\,r$}
 | 
|
1366  | 
\item \bl{$mkeps(x:r) \dn Rec(x, mkeps(r))$}
 | 
|
1367  | 
\item \bl{$inj\,(x:r)\,c\,v \dn Rec(x, inj\,r\,c\,v)$}
 | 
|
1368  | 
\end{itemize}\bigskip\bigskip\pause
 | 
|
1369  | 
||
1370  | 
\small  | 
|
1371  | 
for extracting subpatterns \bl{$(z: ((x:ab) + (y:ba))$}
 | 
|
1372  | 
||
1373  | 
\end{frame}
 | 
|
1374  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1375  | 
||
1376  | 
||
1377  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1378  | 
\begin{frame}[c]
 | 
|
1379  | 
\frametitle{Environments}
 | 
|
1380  | 
||
1381  | 
Obtaining the ``recorded'' parts of a value:  | 
|
1382  | 
||
1383  | 
\begin{center}
 | 
|
1384  | 
\begin{tabular}{lcl}
 | 
|
1385  | 
  \bl{$env(Empty)$}     & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1386  | 
  \bl{$env(Char(c))$}   & \bl{$\dn$} & \bl{$[]$}\\
 | 
|
1387  | 
  \bl{$env(Left(v))$}   & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1388  | 
  \bl{$env(Right(v))$}  & \bl{$\dn$} & \bl{$env(v)$}\\
 | 
|
1389  | 
  \bl{$env(Seq(v_1,v_2))$}& \bl{$\dn$} & \bl{$env(v_1) \,@\, env(v_2)$}\\
 | 
|
1390  | 
  \bl{$env(Stars [v_1,\ldots ,v_n])$} & \bl{$\dn$} & 
 | 
|
1391  | 
     \bl{$env(v_1) \,@\ldots @\, env(v_n)$}\\
 | 
|
1392  | 
  \bl{$env(Rec(x:v))$} & \bl{$\dn$} & \bl{$(x:|v|) :: env(v)$}\\
 | 
|
1393  | 
\end{tabular}
 | 
|
1394  | 
\end{center}
 | 
|
1395  | 
||
1396  | 
\end{frame}
 | 
|
1397  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1398  | 
||
1399  | 
||
1400  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1401  | 
\begin{frame}[c]
 | 
|
1402  | 
\frametitle{While Tokens}
 | 
|
1403  | 
||
1404  | 
\begin{center}
 | 
|
1405  | 
\begin{tabular}{@{}r@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
 | 
|
1406  | 
\pcode{WHILE\_REGS} & $\dn$ & \raisebox{-1mm}{\large(}\pcode{("k" : KEYWORD)} +\\ 
 | 
|
1407  | 
                  &       & \phantom{(}\pcode{("i" : ID)} +\\ 
 | 
|
1408  | 
                  &       & \phantom{(}\pcode{("o" : OP)} + \\
 | 
|
1409  | 
                  &       & \phantom{(}\pcode{("n" : NUM)} + \\
 | 
|
1410  | 
                  &       & \phantom{(}\pcode{("s" : SEMI)} +\\ 
 | 
|
1411  | 
                  &       & \phantom{(}\pcode{("p" : (LPAREN + RPAREN))} +\\ 
 | 
|
1412  | 
                  &       & \phantom{(}\pcode{("b" : (BEGIN + END))} +\\ 
 | 
|
1413  | 
                  &       & \phantom{(}\pcode{("w" : WHITESPACE)}\raisebox{-1mm}{\large)$^*$}
 | 
|
1414  | 
\end{tabular}
 | 
|
1415  | 
\end{center}
 | 
|
1416  | 
||
1417  | 
\end{frame}
 | 
|
1418  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1419  | 
||
1420  | 
||
1421  | 
||
1422  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1423  | 
\begin{frame}[t]
 | 
|
1424  | 
||
1425  | 
\consolas  | 
|
1426  | 
\begin{center}
 | 
|
1427  | 
\code{"if true then then 42 else +"}
 | 
|
1428  | 
\end{center}
 | 
|
1429  | 
||
1430  | 
\only<1>{
 | 
|
1431  | 
\small\begin{tabular}{l}
 | 
|
1432  | 
KEYWORD(if),\\  | 
|
1433  | 
WHITESPACE,\\  | 
|
1434  | 
IDENT(true),\\  | 
|
1435  | 
WHITESPACE,\\  | 
|
1436  | 
KEYWORD(then),\\  | 
|
1437  | 
WHITESPACE,\\  | 
|
1438  | 
KEYWORD(then),\\  | 
|
1439  | 
WHITESPACE,\\  | 
|
1440  | 
NUM(42),\\  | 
|
1441  | 
WHITESPACE,\\  | 
|
1442  | 
KEYWORD(else),\\  | 
|
1443  | 
WHITESPACE,\\  | 
|
1444  | 
OP(+)  | 
|
1445  | 
\end{tabular}}
 | 
|
1446  | 
||
1447  | 
\only<2>{
 | 
|
1448  | 
\small\begin{tabular}{l}
 | 
|
1449  | 
KEYWORD(if),\\  | 
|
1450  | 
IDENT(true),\\  | 
|
1451  | 
KEYWORD(then),\\  | 
|
1452  | 
KEYWORD(then),\\  | 
|
1453  | 
NUM(42),\\  | 
|
1454  | 
KEYWORD(else),\\  | 
|
1455  | 
OP(+)  | 
|
1456  | 
\end{tabular}}
 | 
|
1457  | 
||
1458  | 
\end{frame}
 | 
|
1459  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1460  | 
||
1461  | 
||
1462  | 
||
1463  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1464  | 
%\begin{frame}[c]
 | 
|
1465  | 
%\frametitle{Coursework: PLs (16)}
 | 
|
1466  | 
%  | 
|
1467  | 
%\begin{itemize}
 | 
|
1468  | 
%\item Java (16)  | 
|
1469  | 
%\item C++, C, C\# (14)  | 
|
1470  | 
%\item JavaScript (10)  | 
|
1471  | 
%\item Scala (9)  | 
|
1472  | 
%\item Python (9)  | 
|
1473  | 
%\item PHP (6)  | 
|
1474  | 
%\item Haskell (3)  | 
|
1475  | 
%\item Ruby (4)  | 
|
1476  | 
%\item Bash, Perl, Powershell (2)  | 
|
1477  | 
%\item TypeScript (1)  | 
|
1478  | 
%\item R (1)  | 
|
1479  | 
%\item Coconut (1)  | 
|
1480  | 
%\item Pascal (1)  | 
|
1481  | 
%\end{itemize}  
 | 
|
1482  | 
%  | 
|
1483  | 
%\end{frame}
 | 
|
1484  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1485  | 
||
1486  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1487  | 
%\begin{frame}[c]
 | 
|
1488  | 
%\frametitle{Coursework: Nullable}
 | 
|
1489  | 
%  | 
|
1490  | 
%\begin{center}
 | 
|
1491  | 
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
 | 
|
1492  | 
%  \bl{$nullable([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
 | 
|
1493  | 
%  \bl{$nullable(r^+)$}                   & \bl{$\dn$} & $?$\\
 | 
|
1494  | 
%  \bl{$nullable(r^?)$}                   & \bl{$\dn$} & $?$\\
 | 
|
1495  | 
%  \bl{$nullable(r^{\{n\}})$}              & \bl{$\dn$} & $?$\\
 | 
|
1496  | 
%  \bl{$nullable(r^{\{n..\}})$}            & \bl{$\dn$} & $?$\\
 | 
|
1497  | 
%  \bl{$nullable(r^{\{..n\}})$}            & \bl{$\dn$} & $?$\\
 | 
|
1498  | 
%  \bl{$nullable(r^{\{n..m\}})$}           & \bl{$\dn$} & $?$\\
 | 
|
1499  | 
%  \bl{$nullable(\sim{}r)$}               & \bl{$\dn$} & $?$\\
 | 
|
1500  | 
%  | 
|
1501  | 
%\end{tabular}
 | 
|
1502  | 
%\end{center}
 | 
|
1503  | 
%  | 
|
1504  | 
%\end{frame}
 | 
|
1505  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1506  | 
||
1507  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1508  | 
%\begin{frame}[c]
 | 
|
1509  | 
%%%\frametitle{Coursework: der}
 | 
|
1510  | 
%  | 
|
1511  | 
%\begin{center}
 | 
|
1512  | 
%\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 | 
|
1513  | 
%  \bl{$der\, c\, ([c_1 c_2 \ldots c_n])$}  & \bl{$\dn$} & $?$\\
 | 
|
1514  | 
%  \bl{$der\, c\, (r^+)$}                   & \bl{$\dn$} & $?$\\
 | 
|
1515  | 
%  \bl{$der\, c\, (r^?)$}                   & \bl{$\dn$} & $?$\\
 | 
|
1516  | 
%  \bl{$der\, c\, (r^{\{n\}})$}              & \bl{$\dn$} &
 | 
|
1517  | 
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{n-\liningnums{1}\}}$}\\
 | 
|
1518  | 
%  \bl{$der\, c\, (r^{\{n..\}})$}            & \bl{$\dn$} &
 | 
|
1519  | 
%     \bl{$if\;n=0\;then (der\,c\,r)\cdot r^*$}\\
 | 
|
1520  | 
%  & & \bl{$\phantom{if\;n=0\;}else \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..\}}$}\\
 | 
|
1521  | 
%  \bl{$der\, c\, (r^{\{..n\}})$}            & \bl{$\dn$} &
 | 
|
1522  | 
%     \bl{$if\;n=0\;then\;\ZERO\;else\;(der\,c\,r)\cdot r^{\{..n-\liningnums{1}\}}$}\\
 | 
|
1523  | 
%  | 
|
1524  | 
%  \bl{$der\, c\, (r^{\{n..m\}})$}          & \bl{$\dn$} &
 | 
|
1525  | 
%     \bl{$if\;n = 0 \wedge m = 0\;then\;\ZERO\; else$}\\
 | 
|
1526  | 
%  \multicolumn{3}{l}{\bl{$if\;n = 0 \wedge m > 0\;then\;(der\,c\,r)\cdot r^{\{..m-\liningnums{1}\}}$}}\\
 | 
|
1527  | 
%  \multicolumn{3}{l}{\bl{$\phantom{if\;n = 0 \wedge m > 0\;}else
 | 
|
1528  | 
%          \;(der\,c\,r)\cdot r^{\{n-\liningnums{1}..m-\liningnums{1}\}}$}}\\
 | 
|
1529  | 
%  \bl{$der\, c\, (\sim{}r)$}              & \bl{$\dn$} & $?$\\
 | 
|
1530  | 
%\end{tabular}
 | 
|
1531  | 
%\end{center}
 | 
|
1532  | 
%  | 
|
1533  | 
%\end{frame}
 | 
|
1534  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1535  | 
||
1536  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1537  | 
%\begin{frame}[c]
 | 
|
1538  | 
%\frametitle{Coursework: CFUN}
 | 
|
1539  | 
%  | 
|
1540  | 
%\begin{center}
 | 
|
1541  | 
%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
 | 
|
1542  | 
%  \bl{$nullable(CFUN(\_))$}  & \bl{$\dn$} & \bl{$false$}\\
 | 
|
1543  | 
%  \bl{$der\,c\,(CFUN(f))$}   & \bl{$\dn$} &
 | 
|
1544  | 
%     \bl{$if\;f(c)\;then\;\ONE\;else\;\ZERO$}\bigskip\\
 | 
|
1545  | 
%  \bl{$CHAR(c)$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;c=d)$}\\
 | 
|
1546  | 
%  \bl{$CSET([c_1,\ldots,c_n])$} & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;d\in [c_1,\ldots,c_n])$}\\
 | 
|
1547  | 
%  \bl{$ALL$}                   & \bl{$\dn$} & \bl{$CFUN(\lambda{}d.\;true)$}\\                                                      
 | 
|
1548  | 
%\end{tabular}
 | 
|
1549  | 
%\end{center}
 | 
|
1550  | 
%  | 
|
1551  | 
%\end{frame}
 | 
|
1552  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
1553  | 
||
1554  | 
||
| 33 | 1555  | 
\end{document}
 | 
1556  | 
||
1557  | 
%%% Local Variables:  | 
|
1558  | 
%%% mode: latex  | 
|
1559  | 
%%% TeX-master: t  | 
|
1560  | 
%%% End:  | 
|
1561  |