
diff -r c39f83d8daeb -r 26e5b41faa74 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Sun Feb 15 18:58:21 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Feb 16 17:17:24 2009 +0000
@@ -1,5 +1,5 @@
 theory Parsing
-imports Base 
+imports Base "Package/Simple_Inductive_Package"
 
 begin
 
@@ -528,78 +528,30 @@
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 
 text {*
-  There are a number of special purpose parsers that help with parsing specifications
-  of functions, inductive definitions and so on. For example the 
-  @{ML OuterParse.target} reads a target in order to indicate a locale.
+  There are a number of special purpose parsers that help with parsing
+  specifications for functions, inductive definitions and so on. In
+  Capter~\ref{chp:package}, for example, we will need to parse specifications
+  for inductive predicates of the form:
+*}
 
-@{ML_response [display,gray]
-"let 
-  val input = filtered_input \"(in test)\"
-in 
-  parse OuterParse.target input 
-end" "(\"test\",[])"}
-  
-  The function @{ML OuterParse.opt_target} makes this parser ``optional'', that
-  is wrapping the result into an option type and returning @{ML NONE} if no
-  target is present.
+simple_inductive
+  even and odd
+where
+  even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
 
-  The function @{ML OuterParse.fixes} reads an \isacommand{and}-separated 
-  list of constants that can include type annotations and syntax translations. 
-  For example:\footnote{Note that in the code we need to write 
-  @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
-  in the compound type.}
-*}
+simple_inductive 
+  trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl\<iota> R x x"
+| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
 
 text {*
-
-@{ML_response [display,gray]
-"let
-  val input = filtered_input 
-        \"foo::\\\"int \<Rightarrow> bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\"
-in
-   parse OuterParse.fixes input
-end"
-"([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)), 
-  (bar, SOME \<dots>, NoSyn), 
-  (blonk, NONE, NoSyn)],[])"}  
-
-  Whenever types are given, then they are stored in the @{ML SOME}s.
-  If a syntax translation is present for a constant, then it is
-  stored in the @{ML Mixfix} data structure; no syntax translation is
-  indicated by @{ML NoSyn}.
- 
-  (FIXME: should for-fixes take any syntax annotation?)
-
-  @{ML OuterParse.for_fixes} is an ``optional'' that prefixes 
-  @{ML OuterParse.fixes} with the command \isacommand{for}.
-  (FIXME give an example and explain more)
-
-@{ML_response [display,gray]
-"let
-  val input = filtered_input 
-        \"for foo::\\\"int \<Rightarrow> bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\"
-in
-   parse OuterParse.for_fixes input
-end"
-"([(foo, SOME \<dots>, Mixfix (\"FOO\",[100],100)), 
-  (bar, SOME \<dots>, NoSyn), 
-  (blonk, NONE, NoSyn)],[])"}  
-
+  For this we are going to use the parser:
 *}
 
-
-ML{*let 
-  val input = filtered_input "test_lemma[intro,foo,elim,dest!,bar]:"
-in 
-  parse (SpecParse.thm_name ":") input 
-     |> fst |> snd |> (Attrib.pretty_attribs @{context}) |> (map Pretty.string_of)
-end*}
-
-text {*
-  (FIXME: why is intro, elim and dest treated differently from bar?) 
-*}
-
-ML{*val spec_parser = 
+ML %linenosgray{*val spec_parser = 
     OuterParse.opt_target --
     OuterParse.fixes -- 
     OuterParse.for_fixes --
@@ -610,6 +562,9 @@
                 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
+  To see what it returns, let us parse the string corresponding to the 
+  definition of @{term even} and @{term odd}:
+
 @{ML_response [display,gray]
 "let
   val input = filtered_input
@@ -625,13 +580,85 @@
      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+
+  As can be seen, the result is a ``nested'' four-tuple consisting of an 
+  optional locale; a list of variables with optional type-annotation and optional 
+  syntax-annotation; a list of for-fixes (fixed variables); and a list of rules 
+  where each rule has optionally a name and an attribute.
+
+  In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target 
+  in order to indicate a locale in which the specification is made. For example
+
+@{ML_response [display,gray]
+"parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
+  
+  The function @{ML OuterParse.opt_target} returns @{ML NONE}, if no target is given.
+
+  The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated 
+  list of variables that can include type annotations and syntax translations. 
+  For example:\footnote{Note that in the code we need to write 
+  @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
+  in the compound type.}
+
+@{ML_response [display,gray]
+"let
+  val input = filtered_input 
+        \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+in
+   parse OuterParse.fixes input
+end"
+"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn), 
+  (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), 
+  (blonk, NONE, NoSyn)],[])"}  
 *}
 
-text {* 
-  The (outer?) parser for the package: returns optionally a locale; 
-  a list of predicate constants with optional type-annotation and 
-  optional syntax-annotation; a list of for-fixes (fixed parameters); 
-  and a list of rules where each rule has optionally a name and an attribute.
+text {*
+  Whenever types are given, they are stored in the @{ML SOME}s. Since types
+  are part of the inner syntax they are strings with some printing directives. 
+  If a syntax translation is present for a variable, then it is
+  stored in the @{ML Mixfix} datastructure; no syntax translation is
+  indicated by @{ML NoSyn}.
+
+  \begin{readmore}
+  The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+  \end{readmore}
+
+  Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the
+  same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, 
+  but requires that this list is prefixed by the keyword \isacommand{for}.
+
+@{ML_response [display,gray]
+"parse OuterParse.for_fixes (filtered_input \"for foo and bar\")"
+"([(foo, NONE, NoSyn), (bar, NONE, NoSyn)],[])"}  
+
+  Lines 5 to 9 include the parser for a list of introduction rules, that is propositions 
+  with theorem annotations. The introduction rules are propositions parsed 
+  by @{ML OuterParse.prop}. However, they can include an optional theorem name plus
+  some attributes. For example
+
+@{ML_response [display,gray] "let 
+  val input = filtered_input \"foo_lemma[intro,dest!]:\"
+  val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input 
+in 
+  (name, map Args.dest_src attrib)
+end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
+ 
+  The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
+  @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
+  attributes. If you want to print out all currently known attributes a theorem 
+  can have, you can use the function:
+*}
+
+ML{*Attrib.print_attributes @{theory}*}
+
+text {*
+  For the inductive definitions described above only the attibutes @{text "[intro]"} and
+  @{text "[simp]"} make sense.
+
+  \begin{readmore}
+  Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} 
+  and @{ML_file "Pure/Isar/args.ML"}.
+  \end{readmore}
 *}
 
 section {* New Commands and Keyword Files\label{sec:newcommand} *}




