# HG changeset patch # User Christian Urban # Date 1232117856 0 # Node ID f6f8f8ba1eb1c5ec3cf4cd28fd15209330e781b0 # Parent bcbcf5c839ae6ec11273111f94e660f0e6d69e59 tuned 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"}?) diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/Recipes/Antiquotes.thy Fri Jan 16 14:57:36 2009 +0000 @@ -15,18 +15,21 @@ Document antiquotations can be used for ensuring consistent type-setting of various entities in a document. They can also be used for sophisticated \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you - obtain a list of all available document antiquotations and their options. + obtain a list of all currently available document antiquotations and their options. Below we give the code for two additional antiquotations that can be used to typeset ML-code and also to check whether the given code actually compiles. This provides a sanity check for the code and also allows one to keep documents in sync with other code, for example Isabelle. - We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This - antiquotation takes a piece of code as argument. The code is checked - by sending the ML-expression @{text [quotes] "val _ = \"} containing the - given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} - in Line 4 below). The complete code of the antiquotation is as follows: + We first describe the antiquotation @{text "ML_checked"} with the syntax: + + @{text [display] "@{ML_checked \"a_piece_of_code\"}"} + + The code is checked by sending the ML-expression @{text [quotes] "val _ = + a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML + "ML_Context.eval_in"} in Line 4 below). The complete code of the + antiquotation is as follows: *} @@ -44,16 +47,16 @@ Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, in this case the code given as argument. As mentioned before, this argument - is send to the ML-compiler in the line 4 using the function @{ML ml_val}, - which constructs an apropriate ML-expression. + is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, + which constructs the appropriate ML-expression. If the code is ``approved'' by the compiler, then the output function @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the code. This function expects that the code is a list of strings where each string correspond to a line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" for txt} which produces this list according to linebreaks. There are a number of options for antiquotations - that are observed by @{ML ThyOutput.output_list} when printing the code (for - example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). + that are observed by @{ML ThyOutput.output_list} when printing the code (including + @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). \begin{readmore} For more information about options of antiquotations see \rsccite{sec:antiq}). @@ -62,7 +65,6 @@ Since we used the argument @{ML "Position.none"}, the compiler cannot give specific information about the line number, in case an error is detected. We can improve the code above slightly by writing - *} ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) = @@ -84,22 +86,24 @@ somebody changes the definition of \mbox{@{ML "(op +)"}}. - The second antiquotation extends the first by allowing also to give - hints what the result of the ML-code should be and to check the consistency of - the actual result with these hints. For this we are going to implement the - antiquotation - @{text "@{ML_resp \"expr\" \"pat\"}"} - whose first argument is the ML-code and the second is a pattern specifying - the result. To add some convenience and allow dealing with large outputs, - the user can give a partial specification including abbreviations - @{text [quotes] "\"}. + The second antiquotation we describe extends the first by allowing also to give + a pattern that specifies what the result of the ML-code should be and to check + the consistency of the actual result with the given pattern. For this we are going + to implement the antiquotation + + @{text [display] "@{ML_resp \"a_piece_of_code\" \"pattern\"}"} + + To add some convenience and also to deal with large outputs, + the user can give a partial specification by giving the abbreviation + @{text [quotes] "\"}. For example @{text "(\,\)"} for a pair. - Whereas in the antiquotation @{text "@{ML_checked \"expr\"}"} above, we have - sent the expression - @{text [quotes] "val _ = expr"} to the compiler, in this antiquotation the wildcard - @{text "_"} we will be replaced by a proper pattern constructed the hints. To - do this we need to replace the @{text [quotes] "\"} by @{text [quotes] "_"} - before sending the code to the compiler. The following function will do this: + Whereas in the antiquotation @{text "@{ML_checked \"piece_of_code\"}"} above, + we have sent the expression + @{text [quotes] "val _ = piece_of_code"} to the compiler, in the second the + wildcard @{text "_"} we will be replaced by a proper pattern. To do this we + need to replace the @{text [quotes] "\"} by + @{text [quotes] "_"} before sending the code to the compiler. The following + function will do this: *} @@ -154,8 +158,8 @@ @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\)"} In both cases, the check by the compiler ensures that code and result match. A limitation - of this antiquotation is that the hints can only be given for results that can actually - be constructed as a pattern. This excludes values that are abstract datatypes, like + of this antiquotation, however, is that the hints can only be given in case + they can be constructed as a pattern. This excludes values that are abstract datatypes, like theorems or cterms. *} diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/Recipes/Config.thy Fri Jan 16 14:57:36 2009 +0000 @@ -12,7 +12,7 @@ {\bf Solution:} This can be achieved using configuration values.\smallskip - Assume you want to control three values, say @{ML_text bval} containing a + Assume you want to control three values, namely @{ML_text bval} containing a boolean, @{ML_text ival} containing an integer and @{ML_text sval} containing a string. These values can be declared on the ML-level with *} @@ -23,7 +23,7 @@ text {* where each value needs to be given a default. To enable these values, they need to - be set up using + be set up by *} setup {* setup_bval *} diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/Recipes/NamedThms.thy Fri Jan 16 14:57:36 2009 +0000 @@ -48,9 +48,11 @@ text {* and query the remaining ones with: -@{ML_response_fake_both [display,gray] "thm foo" -"?C -?B"} + \begin{isabelle} + \isacommand{thm}~@{text "foo"}\\ + @{text "> ?C"}\\ + @{text "> ?B"}\\ + \end{isabelle} On the ML-level the rules marked with @{text "foo"} an be retrieved using the function @{ML FooRules.get}: diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/document/root.tex --- a/CookBook/document/root.tex Thu Jan 15 13:42:28 2009 +0000 +++ b/CookBook/document/root.tex Fri Jan 16 14:57:36 2009 +0000 @@ -60,7 +60,7 @@ % this is to draw a gray box around code \makeatletter\newenvironment{graybox}{% \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}% - \colorbox{gray!10}{\usebox{\@tempboxa}} + \colorbox{gray!20}{\usebox{\@tempboxa}} }\makeatother %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff -r bcbcf5c839ae -r f6f8f8ba1eb1 cookbook.pdf Binary file cookbook.pdf has changed