diff -r 8ad407e77ea0 -r ae2f0b40c840 ProgTutorial/Parsing.thy --- 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 ""} & @{text "::="} & @{text " | ()"}\\ + @{text ""} & @{text "::="} & @{text " * | "}\\ + @{text ""} & @{text "::="} & @{text " + | "}\\ + \end{tabular} + \end{center} + + Hint: Be careful with recursive parsers. + \end{exercise} *} section {* Parsers for ML-Code (TBD) *}