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 \ even (Suc n)" +| oddS: "even n \ 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 \ bool\\\""} in order to properly escape the double quotes - in the compound type.} -*} +simple_inductive + trcl\ for R :: "'a \ 'a \ bool" +where + base: "trcl\ R x x" +| step: "trcl\ R x y \ R y z \ trcl\ R x z" text {* - -@{ML_response [display,gray] -"let - val input = filtered_input - \"foo::\\\"int \ bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\" -in - parse OuterParse.fixes input -end" -"([(foo, SOME \, Mixfix (\"FOO\",[100],100)), - (bar, SOME \, 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 \ bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\" -in - parse OuterParse.for_fixes input -end" -"([(foo, SOME \, Mixfix (\"FOO\",[100],100)), - (bar, SOME \, 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,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ 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 \ bool\\\""} in order to properly escape the double quotes + in the compound type.} + +@{ML_response [display,gray] +"let + val input = filtered_input + \"foo::\\\"int \ bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\" +in + parse OuterParse.fixes input +end" +"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \ 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\", []), \), ((\"dest\", [\]), \)])"} + + 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} *}