diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Parsing.thy --- 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 "} + 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 "} + @{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 \ False\"" "True \ 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 \ True\""}, we obtain the following + proof state: + + @{ML_response_fake_both [display] "foobar \"True \ True\"" +"goal (1 subgoal): +1. True \ True"} + + and we can build the proof + + @{text [display] "foobar \"True \ 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 {*