diff -r 7ff1a681f758 -r cf471fa86091 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Thu May 24 15:22:25 2012 +0100 +++ b/ProgTutorial/Parsing.thy Sat Jun 16 15:25:47 2012 +0100 @@ -935,16 +935,17 @@ *} -section {* New Commands and Keyword Files\label{sec:newcommand} *} +section {* New Commands\label{sec:newcommand} *} text {* 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. + need to be implemented. While this is not difficult on the ML-level and + jEdit, in order to be compatible, new commands need also to be recognised + by ProofGeneral. This results in some subtle configuration issues, which we will + explain in the next section. Here we just describe how to define new commands + to work with jEdit. - To keep things simple, let us start with a ``silly'' command that does nothing + 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: *} @@ -953,19 +954,142 @@ val do_nothing = Scan.succeed (Local_Theory.background_theory I) val kind = Keyword.thy_decl in - Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing + Outer_Syntax.local_theory ("foobar", kind) + "description of foobar" + do_nothing +end *} + +text {* + The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, + a kind indicator (which we will explain later more thoroughly), a + short description and a + parser producing a local theory transition (its purpose will also explained + later). Before you can use any new command, you have to ``announce'' it in the + \isacommand{keyword}-section of theory header. In our running example we need + to write + + \begin{graybox} + \isacommand{theory}~@{text Foo}\\ + \isacommand{imports}~@{text Main}\\ + \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\ + ... + \end{graybox} + + whereby you have to declare again that the new keyword is of the appropriate + kind---for \isacommand{foobar} it is @{text "thy_decl"}. Another possible kind + is @{text "thy_goal"} and also to omit the kind entirely, in which case you declare a + keyword (something that is part of a command). After you announced the new command, + you can type in your theory +*} + +foobar + +text {* + At the moment the command \isacommand{foobar} is not very useful. Let us + refine it a bit next by letting it take a proposition as argument and + printing this proposition inside the tracing buffer. For this the crucial + part of a command is the function that determines the behaviour + of the command. In the code above we used a ``do-nothing''-function, which + because of @{ML_ind succeed in Scan} does not parse any argument, but immediately + returns the simple function @{ML "Local_Theory.background_theory I"}. We can + replace this code by a function that first parses a proposition (using the + parser @{ML Parse.prop}), then prints out some tracing + information (using the function @{text trace_prop}) and + finally does nothing. For this you can write: +*} + +ML %grayML{*let + fun trace_prop str = + Local_Theory.background_theory (fn ctxt => (tracing str; ctxt)) + + val kind = Keyword.thy_decl +in + Outer_Syntax.local_theory ("foobar_trace", kind) + "traces a proposition" + (Parse.prop >> trace_prop) end *} text {* - The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, a - short description, a kind indicator (which we will explain later more thoroughly) and a - parser producing a local theory transition (its purpose will also explained - later). + The command is now \isacommand{foobar\_trace} and can be used to + see the proposition in the tracing buffer (remember you need to announce + every new command in the header of the theory). +*} + +foobar_trace "True \ False" + +text {* + Note that so far we used @{ML_ind thy_decl in Keyword} as the kind + indicator for the new 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, commands + are expected to parse some arguments, for example a proposition, and then + ``open up'' a proof in order to prove the proposition (for example + \isacommand{lemma}) or prove some other properties (for example + \isacommand{function}). To achieve this kind of behaviour, you have to use + the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML + "local_theory_to_proof" in Outer_Syntax} to set up the command. + Below we show the command \isacommand{foobar\_goal} which takes a + proposition as argument and then starts a proof in order to prove + it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in + Keyword}. +*} + +ML%linenosgray{*let + fun goal_prop str ctxt = + let + val prop = Syntax.read_prop ctxt str + in + Proof.theorem NONE (K I) [[(prop, [])]] ctxt + end + + val kind = Keyword.thy_goal +in + Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) + "proves a proposition" + (Parse.prop >> goal_prop) +end *} - While this is everything you have to do on the ML-level, you 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 {* + The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be + proved) and a context as argument. The context is necessary in order to be able to use + @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition. + In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the + proposition. Its argument @{ML NONE} stands for a locale (which we chose to + omit); the argument @{ML "(K I)"} stands for a function that determines what + should be done with the theorem once it is proved (we chose to just forget + about it). + + If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \ True"}, + you obtain the following proof state: +*} + +foobar_goal "True \ True" +txt {* + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}\medskip + + and can prove the proposition as follows. +*} +apply(rule conjI) +apply(rule TrueI)+ +done + +text {* + While this is everything you have to do for a new command when using jEdit, + things are not as simple when using Emacs and ProofGeneral. We explain the details + next. +*} + + +section {* Proof-General and Keyword Files *} + +text {* + In order to use a new command in Emacs and Proof-General, you need a keyword + file that can be loaded by ProofGeneral. To keep things simple we take as + running example the command \isacommand{foobar} from the previous section. + + A keyword file can be generated with the command-line: @{text [display] "$ isabelle keywords -k foobar some_log_files"} @@ -983,6 +1107,7 @@ \begin{graybox}\small \isacommand{theory}~@{text Command}\\ \isacommand{imports}~@{text Main}\\ + \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\ \isacommand{begin}\\ \isacommand{ML}~@{text "\"}\\ @{ML @@ -990,7 +1115,9 @@ val do_nothing = Scan.succeed (Local_Theory.background_theory I) val kind = Keyword.thy_decl in - Outer_Syntax.local_theory (\"foobar\", kind) \"description of foobar\" do_nothing + Outer_Syntax.local_theory (\"foobar\", kind) + \"description of foobar\" + do_nothing end"}\\ @{text "\"}\\ \isacommand{end} @@ -1046,7 +1173,7 @@ If the compilation succeeds, you have finally created all the necessary log files. They are stored in the directory - @{text [display] "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"} + @{text [display] "~/.isabelle/heaps/Isabelle2012/polyml-5.2.1_x86-linux/log"} or something similar depending on your Isabelle distribution and architecture. One quick way to assign a shell variable to this directory is by typing @@ -1081,114 +1208,22 @@ @{text [display] "$ isabelle emacs -k foobar a_theory_file"} If you now build a theory on top of @{text "Command.thy"}, - then you can use the command \isacommand{foobar}. You can just write -*} - -foobar + then you can now use the command \isacommand{foobar} + in Proof-General -text {* - but you will not see any action as we chose to implement this command to do - nothing. The point of this command is only to show the procedure of how - to interact with ProofGeneral. A similar procedure has to be done with any + A similar procedure has to be done with any other new command, and also any new keyword that is introduced with the function @{ML_ind define in Keyword}. For example: *} ML %grayML{*val _ = Keyword.define ("blink", NONE) *} -text {* - At the moment the command \isacommand{foobar} is not very useful. Let us - refine it a bit next by letting it take 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 a ``do-nothing''-function, which - because of @{ML_ind succeed in Scan} does not parse any argument, but immediately - returns the simple function @{ML "Local_Theory.background_theory I"}. We can - replace this code by a function that first parses a proposition (using the - parser @{ML Parse.prop}), then prints out the tracing - information (using a new function @{text trace_prop}) and - finally does nothing. For this you can write: -*} - -ML %grayML{*let - fun trace_prop str = - Local_Theory.background_theory (fn ctxt => (tracing str; ctxt)) - - val kind = Keyword.thy_decl -in - Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" - (Parse.prop >> trace_prop) -end *} - -text {* - The command is now \isacommand{foobar\_trace} and can be used to - see the proposition in the tracing buffer. -*} - -foobar_trace "True \ False" text {* - Note that so far we used @{ML_ind thy_decl in Keyword} 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, commands - are expected to parse some arguments, for example a proposition, and then - ``open up'' a proof in order to prove the proposition (for example - \isacommand{lemma}) or prove some other properties (for example - \isacommand{function}). To achieve this kind of behaviour, you have to use - the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML - "local_theory_to_proof" in Outer_Syntax} to set up the command. Note, - however, once you change the ``kind'' of a command from @{ML thy_decl in - Keyword} to @{ML thy_goal in Keyword} then the keyword file needs - to be re-created! - - Below we show the command \isacommand{foobar\_goal} which takes a - proposition as argument and then starts a proof in order to prove - it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in - Keyword}. + Also if the kind of a command changes, from @{text "thy_decl"} to + @{text "thy_goal"} say, you need to recreate the keyword file. *} -ML%linenosgray{*let - fun goal_prop str lthy = - let - val prop = Syntax.read_prop lthy str - in - Proof.theorem NONE (K I) [[(prop, [])]] lthy - end - - val kind = Keyword.thy_goal -in - Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition" - (Parse.prop >> goal_prop) -end *} - -text {* - The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be - proved) and a context as argument. The context is necessary in order to be able to use - @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition. - In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the - proposition. Its argument @{ML NONE} stands for a locale (which we chose to - omit); the argument @{ML "(K I)"} stands for a function that determines what - should be done with the theorem once it is proved (we chose to just forget - about it). Line 9 contains the parser for the proposition. - - If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \ True"}, - you obtain the following proof state -*} - -foobar_goal "True \ True" -txt {* - \begin{minipage}{\textwidth} - @{subgoals [display]} - \end{minipage}\medskip - - and can prove the proposition as follows. -*} -apply(rule conjI) -apply(rule TrueI)+ -done - text {* {\bf TBD below} @@ -1197,7 +1232,7 @@ *} ML {* -structure Result = Proof_Data( +structure Result = Proof_Data ( type T = unit -> term fun init thy () = error "Result") @@ -1398,13 +1433,15 @@ \end{minipage} *} (*<*)oops(*>*) -method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *} +method_setup test = {* + Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *} lemma "True" apply(test) oops -method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *} +method_setup joker = {* + Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *} lemma "False" apply(joker)