--- 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} *}