isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:5fbeeac2901b
+:e7519207c2b7
 theory Parsing
 imports Base
 begin
 chapter {* Parsing *}
 ML {* OuterSyntax.command *}
 section {* New Commands and Creating Keyword Files *}
 text {*
-Often new commands, for example for providing a new definitional principle,
+Often new commands, for example for providing new definitional principles,
-need to be programmed. While this is not difficult to do on the ML-level,
+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
+ML {*
-val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
+let
-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"}
+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
+While this is everything we have to do on the ML-level, we need a keyword
-now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral
+file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
-to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with
+recognise \isacommand{foobar} as a command. Such a keyword file can be
-the command-line
+generated with the command-line
-@{text [display] "$ isabelle keywords -k foo <some-log-files>"}
+@{text [display] "$ isabelle keywords -k foobar some-log-files"}
-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
+The option @{text "-k foobar"} indicates which postfix the keyword file will
-requires log files to be present (in order to extract the keywords from them).
+obtain. In the case above the generated file will be named @{text
-To generate these log files, we first package the code above into a separate theory file
+"isar-keywords-foobar.el"}. However, this command requires log files to be
-named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code.
+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 do_nothing = Scan.succeed (Toplevel.theory I)
-val flag = OuterKeyword.thy_decl
+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
+For our purposes it is sufficient to use the log files for the theories
-our purposes it is sufficient to use the log files for the theories @{text "Pure"},
+@{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
-@{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
+the theory @{text "Command.thy"} containing the new
-containing the new \isacommand{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the
+\isacommand{foobar}-command. @{text Pure} and @{text HOL} are usually
-installation of Isabelle. So log files for them are already available. If not, then they
+compiled during the installation of Isabelle. So log files for them should be
-can be conveniently compiled using build-script from the distribution
+already available. If not, then they can be conveniently compiled using
+build-script from the Isabelle distribution
 @{text [display]
 "$ ./build -m \"Pure\"
 $ ./build -m \"HOL\""}
 @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
 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
+./FoobarCommand/ROOT.ML
-./FooCommand/document
+./FoobarCommand/document
-./FooCommand/document/root.tex"}
+./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"}
 We created finally all the necessary log files. They are typically stored
 in the directory
 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
 @{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 keywords -k foobar
-$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
+$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
+The result is the file @{text "isar-keywords-foobar.el"}. It should contain the
-copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
+string @{text "foobar"} twice (check for example that @{text [quotes] "grep foobar
-this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
+isar-keywords-foobar.el"} returns something non-empty).  This keyword file
+needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
-@{text [display] "isabelle -k foo <a-theory-file>"}
+Isabelle use this keyword file, we have to start it with the option @{text
+"-k foobar"}, i.e.
+@{text [display] "$ isabelle -k foobar a-theory-file"}
 If we now run the original code
+*}
-@{ML [display]
-"let
+ML {*
-val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
+let
-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"}
+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 {*

changeset 68	e7519207c2b7
parent 67	5fbeeac2901b
child 69	19106a9975c1