diff -r f6f8f8ba1eb1 -r f2dea0465bb4 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Jan 16 14:57:36 2009 +0000 +++ b/CookBook/Parsing.thy Fri Jan 23 17:50:35 2009 +0000 @@ -189,7 +189,7 @@ "Exception ABORT raised"} then the parsing aborts and the error message @{text "foo"} is printed out. In order to - see the error message properly, we need to prefix the parser with the function + see the error message, we need to prefix the parser with the function @{ML "Scan.error"}. For example @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" @@ -353,17 +353,17 @@ The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}. \end{readmore} - The structure @{ML_struct OuterLex} defines several kinds of token (for example + The structure @{ML_struct OuterLex} defines several kinds of tokens (for example @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and @{ML "Command" in OuterLex} for commands). Some token parsers take into account the - kind of token. + kind of tokens. *} text {* For the examples below, we can generate a token list out of a string using the function @{ML "OuterSyntax.scan"}, which we give below @{ML "Position.none"} as argument since, at the moment, we are not interested in - generating precise error messages. The following + generating precise error messages. The following code @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" @@ -375,7 +375,7 @@ @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any other syntactic category.\footnote{Note that because of a possible a bug in the PolyML runtime system the result is printed as @{text "?"}, instead of - the token.} The second indicates a space. + the tokens.} The second indicates a space. Many parsing functions later on will require spaces, comments and the like to have already been filtered out. So from now on we are going to use the @@ -409,7 +409,7 @@ we obtain a list consisting of only a command and two keyword tokens. If you want to see which keywords and commands are currently known, type in - the following (you might have to adjust the @{ML print_depth} in order to + the following code (you might have to adjust the @{ML print_depth} in order to see the complete list): @{ML_response_fake [display,gray] @@ -454,7 +454,7 @@ "([\"in\",\"in\",\"in\"],[\])"} @{ML "OuterParse.enum1"} works similarly, except that the parsed list must - be non-empty. Note that we had to add an @{text [quotes] "foo"} at the end + be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the end of the parsed string, otherwise the parser would have consumed all tokens and then failed with the exception @{text "MORE"}. Like in the previous section, we can avoid this exception using the wrapper @{ML @@ -470,7 +470,7 @@ end" "([\"in\",\"in\",\"in\"],[])"} - The following function will help us later to run examples + The following function will help to run examples. *} @@ -585,7 +585,7 @@ The option @{text "-k foobar"} indicates which postfix the name of the keyword file will be assigned. In the case above the generated file will be named @{text - "isar-keywords-foobar.el"}. As indicated, this command requires log files to be + "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be present (in order to extract the keywords from them). To generate these log files, we first package the code above into a separate theory file named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the @@ -608,21 +608,21 @@ end"}\\ \isa{\isacharverbatimclose}\\ \isacommand{end} - \end{graybox} - \caption{The file @{text "Command.thy"} is necessary for generating a log + \end{graybox}\\[-4mm] + \caption{\small The file @{text "Command.thy"} is necessary for generating a log file. This log file enables Isabelle to generate a keyword file containing the command \isacommand{foobar}.\label{fig:commandtheory}} \end{figure} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - For our purposes it is sufficient to use the log files for the theories + For our purposes it is sufficient to use the log files of the theories @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as - the theory @{text "Command.thy"} containing the new - \isacommand{foobar}-command. If you target another logics besides HOL, such + the log file for the theory @{text "Command.thy"}, which contains the new + \isacommand{foobar}-command. If you target other logics besides HOL, such as Nominal or ZF, then you need to adapt the log files appropriately. @{text Pure} and @{text HOL} are usually compiled during the installation of Isabelle. So log files for them should be already available. If not, then - they can be conveniently compiled using build-script from the Isabelle + they can be conveniently compiled with the help of the build-script from the Isabelle distribution @@ -675,8 +675,8 @@ Pure-ProofGeneral.gz HOL-FoobarCommand.gz"} - They are the ones we need for creating the keyword files. Assuming the name - of the directory is in @{text "ISABELLE_LOGS"}, + From them we create the keyword files. Assuming the name + of the directory is in @{text "$ISABELLE_LOGS"}, then the Unix command for creating the keyword file is: @{text [display] @@ -687,53 +687,48 @@ string @{text "foobar"} twice (check for example that @{text "grep foobar isar-keywords-foobar.el"} returns something non-empty). This keyword file needs to be copied into the directory @{text "~/.isabelle/etc"}. To make - Isabelle aware of this keyword file, we have to start it with the option @{text + Isabelle aware of this keyword file, we have to start Isabelle with the option @{text "-k foobar"}, i.e. @{text [display] "$ isabelle -k foobar a_theory_file"} - If we now run the original code -*} - -ML{*let - val do_nothing = Scan.succeed (Toplevel.theory I) - val kind = OuterKeyword.thy_decl -in - OuterSyntax.command "foobar" "description of foobar" kind do_nothing -end *} - -text {* - then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}! + If we now build a theory on top of @{text "Command.thy"}, + then we can make use of the command \isacommand{foobar}. Similarly with any other new command. - At the moment \isacommand{foobar} is not very useful. Let us next refine it a bit - by taking a proposition as argument and printing this proposition inside + At the moment \isacommand{foobar} is not very useful. Let us refine it a bit + next by taking a proposition as argument and printing this proposition inside the tracing buffer. - The crucial part of a command is the function that determines - the behaviour of the command. In the code above we used a - ``do-nothing''-function, which because of @{ML Scan.succeed} does not parse - any argument, but immediately returns the simple toplevel function - @{ML "Toplevel.theory I"}. We can replace this code by a function that first - parses a proposition (using the parser @{ML OuterParse.prop}), then prints out - the tracing information and finally does nothing. For this we can write + The crucial part of a command is the function that determines the behaviour + of the command. In the code above we used a ``do-nothing''-function, which + because of @{ML Scan.succeed} does not parse any argument, but immediately + returns the simple toplevel function @{ML "Toplevel.theory I"}. We can + replace this code by a function that first parses a proposition (using the + parser @{ML OuterParse.prop}), then prints out the tracing + information (using a new top-level function @{text trace_top_lvl}) and + finally does nothing. For this we can write + *} ML{*let - val trace_prop = - OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I))) + fun trace_top_lvl str = + Toplevel.theory (fn thy => (tracing str; thy)) + + val trace_prop = OuterParse.prop >> trace_top_lvl + val kind = OuterKeyword.thy_decl in OuterSyntax.command "foobar" "traces a proposition" kind trace_prop end *} text {* - Now we can type for example + Now we can type \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ False"}\\ - @{text "> True \ False"} + @{text "> \"True \ False\""} \end{isabelle} and see the proposition in the tracing buffer. @@ -741,14 +736,14 @@ Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator for the command. This means that the command finishes as soon as the arguments are processed. Examples of this kind of commands are - \isacommand{definition} and \isacommand{declare}. In other cases + \isacommand{definition} and \isacommand{declare}. In other cases, commands are expected to parse some arguments, for example a proposition, - and then ``open up'' a proof in order to prove the proposition (think of + and then ``open up'' a proof in order to prove the proposition (for example \isacommand{lemma}) or prove some other properties (for example in - \isacommand{function}). To achieve this behaviour, we have to use the kind + \isacommand{function}). To achieve this kind of behaviour, we have to use the kind indicator @{ML thy_goal in OuterKeyword}. - Below we change \isacommand{foobar} so that it expects a proposition as + Below we change \isacommand{foobar} so that it takes a proposition as argument and then starts a proof in order to prove it. Therefore in Line 13 below, we set the kind indicator to @{ML thy_goal in OuterKeyword}. *} @@ -758,7 +753,7 @@ let val prop = Syntax.read_prop ctxt str in - Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt + Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt end; val prove_prop = OuterParse.prop >> @@ -774,8 +769,11 @@ The function @{text set_up_thm} takes a string (the proposition to be proved) and a context. The context is necessary in order to be able to use @{ML Syntax.read_prop}, which converts a string into a proper proposition. - In Line 6 the function @{ML Proof.theorem_i} starts the proof for the - proposition. In Lines 9 to 11 contain the parser for the proposition. + In Line 6 the function @{ML Proof.theorem_i} starts the proof for the + proposition. Its argument @{ML NONE} stands for a locale (which we chose to + omit); the argument @{ML "(K I)"} stands for a function that determines what + should be done with the theorem once it is proved (we chose to just forget + about it). In Lines 9 to 11 contain the parser for the proposition. If we now type \isacommand{foobar}~@{text [quotes] "True \ True"}, we obtain the following proof state: @@ -796,12 +794,16 @@ \end{isabelle} - (FIXME What does @{text "Toplevel.theory"}?) + (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?) (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser) + (FIXME read a name and show how to store theorems) + + (FIXME possibly also read a locale) *} +(*<*) chapter {* Parsing *} text {* @@ -852,9 +854,9 @@ \begin{verbatim} open StringCvt ; type ('res, 'src) ex_reader = 'src -> 'res * 'src - (* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *) + ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader fun ex_reader rdr src = Option.valOf (rdr src) ; - (* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *) + reader : ('res, 'src) ex_reader -> ('res, 'src) reader fun reader exrdr src = SOME (exrdr src) handle _ => NONE ; \end{verbatim} @@ -1469,7 +1471,6 @@ *} - +(*>*) - -end \ No newline at end of file +end \ No newline at end of file