--- a/ProgTutorial/Parsing.thy	Tue Nov 17 18:40:11 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Nov 17 20:36:18 2009 +0100
@@ -674,6 +674,22 @@
   @{ML_file "Pure/General/position.ML"}.
   \end{readmore}
 
+  \begin{exercise}\label{ex:contextfree}
+  Write a parser for the context-free grammar representing arithmetic 
+  expressions with addition and multiplication. As usual, multiplication 
+  binds stronger than addition, and both of them nest to the right. 
+  The context-free grammar is defined as:
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{text "<Basic>"}  & @{text "::="} & @{text "<Number> | (<Expr>)"}\\
+  @{text "<Factor>"} & @{text "::="} & @{text "<Basic> * <Factor> | <Basic>"}\\
+  @{text "<Expr>"}   & @{text "::="} & @{text "<Factor> + <Expr>  | <Factor>"}\\
+  \end{tabular}
+  \end{center}
+
+  Hint: Be careful with recursive parsers.
+  \end{exercise}
 *}
 
 section {* Parsers for ML-Code (TBD) *}

--- a/ProgTutorial/Solutions.thy	Tue Nov 17 18:40:11 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Nov 17 20:36:18 2009 +0100
@@ -82,9 +82,25 @@
 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 *}
 
-text {* \solution{ex:dyckhoff} *}
+text {* \solution{ex:contextfree} *}
+
+ML{*datatype expr = 
+   Number of int
+ | Mult of expr * expr 
+ | Add of expr * expr
 
-text {*
+fun parse_basic xs =
+  (OuterParse.nat >> Number 
+   || OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs
+and parse_factor xs =
+  (parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult 
+   || parse_basic) xs
+and parse_expr xs =
+  (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 
+   || parse_factor) xs*}
+
+
+text {* \solution{ex:dyckhoff} 
   The axiom rule can be implemented with the function @{ML atac}. The other
   rules correspond to the theorems:
 

Binary file progtutorial.pdf has changed