# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258479611 -3600
# Node ID 8ad407e77ea0e923823b2d08a25f3b793642b7a0
# Parent  4cc6df387ce93859554a5010020aba1d4c32eafc
added example by Lukas Bulwahn

diff -r 4cc6df387ce9 -r 8ad407e77ea0 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Sun Nov 15 13:47:31 2009 +0100
+++ b/ProgTutorial/Intro.thy	Tue Nov 17 18:40:11 2009 +0100
@@ -194,6 +194,7 @@
   \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
   \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
   \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
+  \item @{text "S"} for sorts; ML-type: @{ML_type sort}
   \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
   \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
   \item @{text thy} for theories; ML-type: @{ML_type theory}
@@ -226,6 +227,9 @@
   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   are by him.
 
+  \item {\bf Lukas Bulwahn} made me aware of the problems with recursive
+  parsers.
+
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.
 
@@ -255,6 +259,4 @@
   \input{pversion}
 *}
 
-
-
 end
diff -r 4cc6df387ce9 -r 8ad407e77ea0 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sun Nov 15 13:47:31 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Nov 17 18:40:11 2009 +0100
@@ -372,7 +372,70 @@
 "Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
 
-  (FIXME: In which situations is this useful? Give examples.) 
+  \footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.} 
+
+  Be aware of recursive parsers. Suppose you want to read strings
+  separated by commas and by parentheses into a tree. We assume 
+  the trees are represented by the datatype:
+*}
+
+ML{*datatype tree = 
+    Lf of string 
+  | Br of tree * tree*}
+
+text {*
+  Since nested parentheses should be treated in a meaningful way---for example
+  the string @{text [quotes] "((A))"} should be read into a single 
+  leaf---you might implement the following parser.
+*}
+
+ML{*fun parse_basic s = 
+  $$ s >> Lf 
+  || $$ "(" |-- parse_tree s --| $$ ")"  
+and parse_tree s = 
+  parse_basic s --| $$ "," -- parse_tree s >> Br 
+  || parse_basic s*}
+
+text {*
+  The parameter @{text "s"} is the string over which the tree is parsed. The
+  parser @{ML parse_basic} reads either a leaf or a tree enclosed in
+  parentheses. The parser @{ML parse_tree} reads either a pair of trees
+  separated by a comma, or acts like @{ML parse_basic}. Unfortunately,
+  because of the mutual recursion, this parser will immediately run into a
+  loop, even if it is called without any input. For example
+
+  @{ML_response_fake_both [display, gray]
+  "parse_tree \"A\""
+  "*** Exception- TOPLEVEL_ERROR raised"}
+
+  raises an exception indicating that the stack limit is reached. Such
+  looping parser are not useful at all, because of ML's strict evaluation of
+  arguments. Therefore we need to delay the execution of the
+  parser until an input is given. This can be done by adding the parsed
+  string as an explicit argument.
+*}
+
+ML{*fun parse_basic s xs = 
+  ($$ s >> Lf 
+   || $$ "(" |-- parse_tree s --| $$ ")") xs 
+and parse_tree s xs = 
+  (parse_basic s --| $$ "," -- parse_tree s >> Br 
+   || parse_basic s) xs*}
+
+text {*
+  While the type of the parser is unchanged by the addition, its behaviour 
+  changed: with this version of the parser the execution is delayed until 
+  some string is  applied for the argument @{text "xs"}. This gives us 
+  exactly the parser what we wanted. An example is as follows:
+
+  @{ML_response [display, gray]
+  "let
+  val input = Symbol.explode \"(A,((A))),A\"
+in
+  Scan.finite Symbol.stopper (parse_tree \"A\") input
+end"
+  "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
+
 
   \begin{exercise}\label{ex:scancmts}
   Write a parser that parses an input string so that any comment enclosed
diff -r 4cc6df387ce9 -r 8ad407e77ea0 ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Sun Nov 15 13:47:31 2009 +0100
+++ b/ProgTutorial/document/root.tex	Tue Nov 17 18:40:11 2009 +0100
@@ -159,6 +159,7 @@
         Stefan & Berghofer\\
         Jasmin & Blanchette\\
         Sascha & Böhme\\
+        Lukas & Bulwahn\\
         Jeremy & Dawson\\
         Alexander & Krauss\\
         Christian & Sternagel\\ 
diff -r 4cc6df387ce9 -r 8ad407e77ea0 progtutorial.pdf
Binary file progtutorial.pdf has changed