--- a/ProgTutorial/Parsing.thy Sat Jun 16 15:25:47 2012 +0100
+++ b/ProgTutorial/Parsing.thy Mon Jun 18 14:49:09 2012 +0100
@@ -4,6 +4,7 @@
chapter {* Parsing\label{chp:parsing} *}
+
text {*
\begin{flushright}
{\em An important principle underlying the success and popularity of Unix\\ is
@@ -940,33 +941,16 @@
text {*
Often new commands, for example for providing new definitional principles,
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
+ jEdit, in order to be backwards compatible, new commands need also to be recognised
+ by Proof-General. 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.
- 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 %grayML{*let
- 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
-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
+ Let us start with a ``silly'' command that does nothing at all. We
+ shall name this command \isacommand{foobar}. Before you can
+ implement any new command, you have to ``announce'' it in the
+ \isacommand{keyword}-section of theory header. For \isacommand{foobar}
+ we need to write something like
\begin{graybox}
\isacommand{theory}~@{text Foo}\\
@@ -975,44 +959,71 @@
...
\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
+ whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
+ command. Another possible kind is @{text "thy_goal"}, or you can
+ also to omit the kind entirely, in which case you declare a keyword
+ (something that is part of a command).
+
+ Now you can implement \isacommand{foobar} as:
*}
+ML %grayML{*let
+ val do_nothing = Scan.succeed (Local_Theory.background_theory I)
+in
+ Outer_Syntax.local_theory @{command_spec "foobar"}
+ "description of foobar"
+ do_nothing
+end *}
+
+text {*
+ The crucial function @{ML_ind local_theory in Outer_Syntax} expects
+ the name for the command, a kind indicator, a short description and
+ a parser producing a local theory transition (explained later). For the
+ name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
+ After this, you can write in your theory
+*}
+
+
foobar
-text {*
+
+text {*
+ Remember that this only works in jEdit. In order to let Proof-General
+ recognise this command, a keyword file needs to be generated (see next
+ section).
+
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:
+ printing this proposition inside the tracing buffer. We announce the
+ command as
+
+ \begin{graybox}
+ \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
+ \end{graybox}
+
+ 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 the parser @{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)
+ Outer_Syntax.local_theory @{command_spec "foobar_trace"}
"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 (remember you need to announce
- every new command in the header of the theory).
+ see the proposition in the tracing buffer.
*}
foobar_trace "True \<and> False"
@@ -1030,8 +1041,14 @@
"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}.
+ it. Therefore, we need to announce this command in the header
+ as @{text "thy_goal"}
+
+ \begin{graybox}
+ \isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}
+ \end{graybox}
+
+ Then we can write:
*}
ML%linenosgray{*let
@@ -1041,10 +1058,8 @@
in
Proof.theorem NONE (K I) [[(prop, [])]] ctxt
end
-
- val kind = Keyword.thy_goal
in
- Outer_Syntax.local_theory_to_proof ("foobar_goal", kind)
+ Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"}
"proves a proposition"
(Parse.prop >> goal_prop)
end *}
@@ -1076,6 +1091,82 @@
done
text {*
+ The final new command we describe is
+ \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
+ to take a proposition and open a corresponding proof-state that
+ allows us to give a proof for it. However, unlike
+ \isacommand{lemma}, the proposition will be given as an
+ ML-value. Such a command is quite useful during development
+ of a tool that generates a goal on the ML-level and you want to see
+ whether it is provable. In addition you also want that the proved
+ proposition can be given a lemma name that can be referenced later on.
+
+ The first problem of this new command is to parse some text as
+ ML-source and then interpret it as a term. For the parsing we can
+ use the function @{ML_ind "ML_source" in Parse} in the structure
+ @{ML_struct Parse}. For running the ML-interpreter we need the
+ following scaffolding code.
+*}
+
+ML %grayML{*
+structure Result = Proof_Data (
+ type T = unit -> term
+ fun init thy () = error "Result")
+
+val result_cookie = (Result.get, Result.put, "Result.put") *}
+
+text {*
+ With this in place we can write the code for \isacommand{foobar\_prove}.
+*}
+
+ML %linenosgray{*let
+ fun after_qed thm_name thms lthy =
+ Local_Theory.note (thm_name, (flat thms)) lthy |> snd
+
+ fun setup_proof (thm_name, (txt, pos)) lthy =
+ let
+ val trm = Code_Runtime.value lthy result_cookie ("", txt)
+ in
+ Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy
+ end
+
+ val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
+in
+ Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"}
+ "proving a proposition"
+ (parser >> setup_proof)
+end*}
+
+text {*
+ In Line 12, we implement a parser that first reads in an optional lemma name (terminated
+ by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML
+ text and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
+ in the structure @{ML_struct Code_Runtime}. Once the ML-text has been turned into a term,
+ the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
+ function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem,
+ once it is proven, under the user given name @{text "thm_name"}.
+
+ We can now give take a term, for example
+*}
+
+ML %grayML{*val prop_true = @{prop "True"}*}
+
+text {*
+ and give a proove for it using \isacommand{foobar\_prove}:
+*}
+
+foobar_prove test: prop_true
+apply(rule TrueI)
+done
+
+text {*
+ Finally we can test whether the lemma has been stored under the given name.
+
+ \begin{isabelle}
+ \isacommand{thm}~@{text "test"}\\
+ @{text "> "}~@{thm TrueI}
+ \end{isabelle}
+
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.
@@ -1113,9 +1204,8 @@
@{ML
"let
val do_nothing = Scan.succeed (Local_Theory.background_theory I)
- val kind = Keyword.thy_decl
in
- Outer_Syntax.local_theory (\"foobar\", kind)
+ Outer_Syntax.local_theory @{command_spec \"foobar\"}
\"description of foobar\"
do_nothing
end"}\\
@@ -1231,38 +1321,9 @@
*}
-ML {*
-structure Result = Proof_Data (
- type T = unit -> term
- fun init thy () = error "Result")
-val result_cookie = (Result.get, Result.put, "Result.put")
-*}
-
-ML %grayML{*let
- fun after_qed thm_name thms lthy =
- Local_Theory.note (thm_name, (flat thms)) lthy |> snd
- fun setup_proof (thm_name, (txt, pos)) lthy =
- let
- val trm = Code_Runtime.value lthy result_cookie ("", txt)
- in
- Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
- end
- val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
-
-in
- Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal)
- "proving a proposition"
- (parser >> setup_proof)
-end*}
-
-(*
-foobar_prove test: {* @{prop "True"} *}
-apply(rule TrueI)
-done
-*)
(*
ML {*