--- a/CookBook/Parsing.thy Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Parsing.thy Wed Jan 14 16:46:07 2009 +0000
@@ -1,5 +1,5 @@
theory Parsing
-imports Base
+imports Base
begin
@@ -556,70 +556,78 @@
section {* New Commands and Creating Keyword Files *}
text {*
- Often new commands, for example for providing a new definitional principle,
- need to be programmed. While this is not difficult to do on the ML-level,
+ Often new commands, for example for providing new definitional principles,
+ need to be implemented. While this is not difficult on the ML-level,
new commands, in order to be useful, need to be recognised by
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{foo} in what follows.
+ 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
+*}
-@{ML [display]
-"let
- val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
- val flag = OuterKeyword.thy_decl
+ML {*
+let
+ val do_nothing = Scan.succeed (Toplevel.theory I)
+ val kind = OuterKeyword.thy_decl
in
- OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+ OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end
+*}
+text {*
The function @{ML OuterSyntax.command} expects a name for the command, a
- short description, a flag (which we will explain later on more thoroughly) and 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
later).
- While this is everything we have to do on the ML-level, we need
- now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral
- to recognise \isacommand{foo} as a command. Such a keyword file can be generated with
- the command-line
+ 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
+
+
+ @{text [display] "$ isabelle keywords -k foobar some-log-files"}
- @{text [display] "$ isabelle keywords -k foo <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
+ 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
+ complete code.
- The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
- the case above the generated file will be named @{text "isar-keywords-foo.el"}. 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 complete code.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{figure}[t]
- \begin{boxedminipage}{\textwidth}
+ \begin{boxedminipage}{\textwidth}\small
\isacommand{theory}~@{text Command}\\
\isacommand{imports}~@{text Main}\\
\isacommand{begin}\\
\isacommand{ML}~\isa{\isacharverbatimopen}\\
@{ML
"let
- val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
- val flag = OuterKeyword.thy_decl
+ val do_nothing = Scan.succeed (Toplevel.theory I)
+ val kind = OuterKeyword.thy_decl
in
- OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
+ OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
end"}\\
\isa{\isacharverbatimclose}\\
\isacommand{end}
\end{boxedminipage}
\caption{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{foo}.\label{fig:commandtheory}}
+ the command \isacommand{foobar}.\label{fig:commandtheory}}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- 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{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the
- installation of Isabelle. So log files for them are already available. If not, then they
- can be conveniently compiled using build-script from the distribution
+ 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
@{text [display]
"$ ./build -m \"Pure\"
@@ -632,23 +640,23 @@
For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory
with
- @{text [display] "$ isabelle mkdir FooCommand"}
+ @{text [display] "$ isabelle mkdir FoobarCommand"}
This creates a directory containing the files
@{text [display]
"./IsaMakefile
-./FooCommand/ROOT.ML
-./FooCommand/document
-./FooCommand/document/root.tex"}
+./FoobarCommand/ROOT.ML
+./FoobarCommand/document
+./FoobarCommand/document/root.tex"}
- We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
+ We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
and add the line
@{text [display] "use_thy \"Command\";"}
- to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing
+ to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
@{text [display] "$ isabelle make"}
@@ -663,50 +671,139 @@
@{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
- In this directory are the files
+ on the Unix prompt. This directory should include the files
@{text [display]
"Pure.gz
HOL.gz
Pure-ProofGeneral.gz
-HOL-FooCommand.gz"}
+HOL-FoobarCommand.gz"}
- They are used for creating the keyword files with the command
+ They are the ones we use for creating the keyword files. The corresponding Unix command
+ is
@{text [display]
-"$ isabelle keywords -k foo
- $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
+"$ isabelle keywords -k foobar
+ $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
- The result is the file @{text "isar-keywords-foo.el"}. This file needs to be
- copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
- this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
+ 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
+ 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
+ "-k foobar"}, i.e.
- @{text [display] "isabelle -k foo <a-theory-file>"}
+ @{text [display] "$ isabelle -k foobar a-theory-file"}
If we now run the original code
+*}
- @{ML [display]
-"let
- val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
- val flag = OuterKeyword.thy_decl
+ML {*
+let
+ val do_nothing = Scan.succeed (Toplevel.theory I)
+ val kind = OuterKeyword.thy_decl
in
- OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+ OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end
+*}
- then we can make use of \isacommand{foo}! Similarly with any other new command.
+text {*
+ then we can make use of \isacommand{foobar}! 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 change the
+ 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
+ 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
+ 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
+*}
+
+ML {*
+let
+ val trace_prop =
+ OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
+ val kind = OuterKeyword.thy_decl
+in
+ OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
+end
+*}
+
+text {*
+ Now we can type for example
+
+ @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
+
+ and see the proposition in the tracing buffer.
+
+ Note that so far we used @{ML thy_decl in OuterKeyword} as 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,
+ 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
+ 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 set the kind indicator to @{ML thy_goal in OuterKeyword}.
+*}
+
+ML %linenumbers {*let
+ fun set_up_thm str ctxt =
+ let
+ val prop = Syntax.read_prop ctxt str
+ in
+ Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
+ end;
+
+ val prove_prop = OuterParse.prop >>
+ (fn str => Toplevel.print o
+ Toplevel.local_theory_to_proof NONE (set_up_thm str))
+
+ val kind = OuterKeyword.thy_goal
+in
+ OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
+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.
+
+ If we now type @{text "foobar \"True \<and> True\""}, we obtain the following
+ proof state:
+
+ @{ML_response_fake_both [display] "foobar \"True \<and> True\""
+"goal (1 subgoal):
+1. True \<and> True"}
+
+ and we can build the proof
+
+ @{text [display] "foobar \"True \<and> True\"
+apply(rule conjI)
+apply(rule TrueI)+
+done"}
+
+ (FIXME What does @{text "Toplevel.theory"}?)
+
(FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-
*}
-
-
-
chapter {* Parsing *}
text {*