--- 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 \<and> False\"" "True \<and> False"}
+ \begin{isabelle}
+ \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+ @{text "> True \<and> 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 \<and> True\""}, we obtain the following
+ If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following
proof state:
- @{ML_response_fake_both [display,gray] "foobar \"True \<and> True\""
-"goal (1 subgoal):
-1. True \<and> True"}
+ \begin{isabelle}
+ \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+ @{text "goal (1 subgoal)"}\\
+ @{text "1. True \<and> True"}
+ \end{isabelle}
and we can build the proof
- @{text [display,gray] "foobar \"True \<and> True\"
-apply(rule conjI)
-apply(rule TrueI)+
-done"}
+ \begin{isabelle}
+ \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+ \isacommand{apply}@{text "(rule conjI)"}\\
+ \isacommand{apply}@{text "(rule TrueI)+"}\\
+ \isacommand{done}
+ \end{isabelle}
+
(FIXME What does @{text "Toplevel.theory"}?)