diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/Parsing.thy Fri Jan 16 14:57:36 2009 +0000 @@ -192,7 +192,7 @@ see the error message properly, we need to prefix the parser with the function @{ML "Scan.error"}. For example - @{ML_response_fake [display,gray] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))" + @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" "Exception Error \"foo\" raised"} This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} @@ -557,8 +557,9 @@ ProofGeneral. This results in some subtle configuration issues, which we will explain in this section. - Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows. - To keep things simple this command does nothing at all. On the ML-level it can be defined as + To keep things simple, let us start with a ``silly'' command that does nothing + at all. We shall name this command \isacommand{foobar}. On the ML-level it can be + defined as *} ML{*let @@ -569,22 +570,22 @@ end *} text {* - The function @{ML OuterSyntax.command} expects a name for the command, a + The crucial function @{ML OuterSyntax.command} expects a name for the command, a short description, a kind indicator (which we will explain later on more thoroughly) and a - parser for a top-level transition function (its purpose will also explained + parser producing a top-level transition function (its purpose will also explained later). While this is everything we have to do on the ML-level, we need a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral to recognise \isacommand{foobar} as a command. Such a keyword file can be - generated with the command-line + generated with the command-line: - @{text [display] "$ isabelle keywords -k foobar some-log-files"} + @{text [display] "$ isabelle keywords -k foobar some_log_files"} - The option @{text "-k foobar"} indicates which postfix the keyword file will - obtain. In the case above the generated file will be named @{text - "isar-keywords-foobar.el"}. However, this command requires log files to be + 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 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 @@ -617,10 +618,13 @@ For our purposes it is sufficient to use the log files for the theories @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"} containing the new - \isacommand{foobar}-command. @{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 distribution + \isacommand{foobar}-command. If you target another 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 + distribution + @{text [display] "$ ./build -m \"Pure\" @@ -635,7 +639,7 @@ @{text [display] "$ isabelle mkdir FoobarCommand"} - This creates a directory containing the files + This generates a directory containing the files @{text [display] "./IsaMakefile @@ -653,18 +657,17 @@ @{text [display] "$ isabelle make"} - We created finally all the necessary log files. They are typically stored + We created finally all the necessary log files. They are stored in the directory @{text [display] "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"} - or something similar depending on your Isabelle distribution and architecture. - Let us assume the name of this directory is stored in the shell variable - @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing + or something similar depending on your Isabelle distribution and architecture. + One quick way to assign a shell variable to this directory is by typing @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} - on the Unix prompt. This directory should include the files + on the Unix prompt. The directory should include the files @{text [display] "Pure.gz @@ -672,21 +675,22 @@ Pure-ProofGeneral.gz HOL-FoobarCommand.gz"} - They are the ones we use for creating the keyword files. The corresponding Unix command - is + They are the ones we need for creating 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] "$ isabelle keywords -k foobar $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"} The result is the file @{text "isar-keywords-foobar.el"}. It should contain the - string @{text "foobar"} twice (check for example that @{text [quotes] "grep foobar + 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 use this keyword file, we have to start it with the option @{text + Isabelle aware of this keyword file, we have to start it with the option @{text "-k foobar"}, i.e. - @{text [display] "$ isabelle -k foobar a-theory-file"} + @{text [display] "$ isabelle -k foobar a_theory_file"} If we now run the original code *} @@ -699,19 +703,17 @@ end *} text {* - then we can make use of \isacommand{foobar}! Similarly with any other new command. + then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}! + Similarly with any other new command. - In the example above, we built the theories on top of the HOL-logic. If you - target other logics, such as Nominal or ZF, then you need to adapt the - log files appropriately. - At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit + 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 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 the the - @{text do_nothing}-function, which because of @{ML Scan.succeed} does not parse + 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 @@ -729,22 +731,25 @@ text {* Now we can type for example - @{ML_response_fake_both [display,gray] "foobar \"True \ False\"" "True \ False"} + \begin{isabelle} + \isacommand{foobar}~@{text [quotes] "True \ False"}\\ + @{text "> True \ False"} + \end{isabelle} and see the proposition in the tracing buffer. - Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator + 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, however, + \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 \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 behaviour, we have to use the kind indicator @{ML thy_goal in OuterKeyword}. - Below we change \isacommand{foobar} is such a way that an proposition as - argument and then start a proof in order to prove it. Therefore in Line 13 + Below we change \isacommand{foobar} so that it expects 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}. *} @@ -766,25 +771,30 @@ end *} text {* - The function @{text set_up_thm} takes a string (the proposition) and a context. - The context is necessary in order to convert the string into a proper proposition - using the function @{ML Syntax.read_prop}. In Line 6 we use the function - @{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to - 11 contain the parser for the proposition. + 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. - If we now type @{text "foobar \"True \ True\""}, we obtain the following + If we now type \isacommand{foobar}~@{text [quotes] "True \ True"}, we obtain the following proof state: - @{ML_response_fake_both [display,gray] "foobar \"True \ True\"" -"goal (1 subgoal): -1. True \ True"} + \begin{isabelle} + \isacommand{foobar}~@{text [quotes] "True \ False"}\\ + @{text "goal (1 subgoal)"}\\ + @{text "1. True \ True"} + \end{isabelle} and we can build the proof - @{text [display,gray] "foobar \"True \ True\" -apply(rule conjI) -apply(rule TrueI)+ -done"} + \begin{isabelle} + \isacommand{foobar}~@{text [quotes] "True \ False"}\\ + \isacommand{apply}@{text "(rule conjI)"}\\ + \isacommand{apply}@{text "(rule TrueI)+"}\\ + \isacommand{done} + \end{isabelle} + (FIXME What does @{text "Toplevel.theory"}?)