--- a/ProgTutorial/Parsing.thy Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Parsing.thy Wed Apr 01 12:26:56 2009 +0100
@@ -195,7 +195,7 @@
@{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
"Exception Error \"foo\" raised"}
- This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"}
+ This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
@@ -349,8 +349,6 @@
section {* Parsing Theory Syntax *}
text {*
- (FIXME: context parser)
-
Most of the time, however, Isabelle developers have to deal with parsing
tokens, not strings. These token parsers have the type:
*}
@@ -619,12 +617,14 @@
for inductive predicates of the form:
*}
+(*
simple_inductive
even and odd
where
even0: "even 0"
| evenS: "odd n \<Longrightarrow> even (Suc n)"
| oddS: "even n \<Longrightarrow> odd (Suc n)"
+*)
text {*
For this we are going to use the parser:
@@ -679,7 +679,7 @@
val input = filtered_input
\"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
in
- parse OuterParse.fixes input
+ parse OuterParse.fixes input
end"
"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn),
(bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)),
@@ -699,10 +699,10 @@
\end{readmore}
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
- list of introduction rules, that is propositions with theorem
- annotations. The introduction rules are propositions parsed by @{ML
- OuterParse.prop}. However, they can include an optional theorem name plus
- some attributes. For example
+ list of introduction rules, that is propositions with theorem annotations
+ such as rule names and attributes. The introduction rules are propositions
+ parsed by @{ML OuterParse.prop}. However, they can include an optional
+ theorem name plus some attributes. For example
@{ML_response [display,gray] "let
val input = filtered_input \"foo_lemma[intro,dest!]:\"
@@ -752,8 +752,6 @@
section {* New Commands and Keyword Files\label{sec:newcommand} *}
text {*
- (FIXME: update to the right command setup --- is this still needed?)
-
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
@@ -766,16 +764,16 @@
*}
ML{*let
- val do_nothing = Scan.succeed (Toplevel.theory I)
+ val do_nothing = Scan.succeed (LocalTheory.theory I)
val kind = OuterKeyword.thy_decl
in
- OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+ OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
end *}
text {*
- The crucial function @{ML OuterSyntax.command} expects a name for the command, a
- short description, a kind indicator (which we will explain later on more thoroughly) and a
- parser producing a top-level transition function (its purpose will also explained
+ The crucial function @{ML OuterSyntax.local_theory} 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).
While this is everything you have to do on the ML-level, you need a keyword
@@ -803,15 +801,15 @@
\isacommand{ML}~@{text "\<verbopen>"}\\
@{ML
"let
- val do_nothing = Scan.succeed (Toplevel.theory I)
+ val do_nothing = Scan.succeed (LocalTheory.theory I)
val kind = OuterKeyword.thy_decl
in
- OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
+ OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
end"}\\
@{text "\<verbclose>"}\\
\isacommand{end}
\end{graybox}
- \caption{\small The file @{text "Command.thy"} is necessary for generating a log
+ \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{foobar}.\label{fig:commandtheory}}
\end{figure}
@@ -909,25 +907,24 @@
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 Scan.succeed} does not parse any argument, but immediately
- returns the simple toplevel function @{ML "Toplevel.theory I"}. We can
+ returns the simple function @{ML "LocalTheory.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 (using a new top-level function @{text trace_top_lvl}) and
+ information (using a new function @{text trace_prop}) and
finally does nothing. For this you can write:
*}
ML{*let
- fun trace_top_lvl str =
+ fun trace_prop str =
LocalTheory.theory (fn lthy => (tracing str; lthy))
- val trace_prop = OuterParse.prop >> trace_top_lvl
-
+ val trace_prop_parser = OuterParse.prop >> trace_prop
val kind = OuterKeyword.thy_decl
in
- OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop
+ OuterSyntax.local_theory "foobar" "traces a proposition"
+ kind trace_prop_parser
end *}
-
text {*
Now you can type
@@ -938,17 +935,19 @@
and see the proposition in the tracing buffer.
- Note that so far we used @{ML thy_decl in OuterKeyword} 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
+ Note that so far we used @{ML thy_decl in OuterKeyword} 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 thy_goal in OuterKeyword}. Note, however, once you change the
- ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword}
- then the keyword file needs to be re-created!
+ \isacommand{function}). To achieve this kind of behaviour, you have to use
+ the kind indicator @{ML thy_goal in OuterKeyword} and the function @{ML
+ "local_theory_to_proof" in OuterSyntax} to set up the command. Note,
+ however, once you change the ``kind'' of a command from @{ML thy_decl in
+ OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
+ to be re-created!
Below we change \isacommand{foobar} so that it takes a proposition as
argument and then starts a proof in order to prove it. Therefore in Line 13,
@@ -956,34 +955,32 @@
*}
ML%linenosgray{*let
- fun set_up_thm str ctxt =
+ fun prove_prop str ctxt =
let
val prop = Syntax.read_prop ctxt str
in
Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt
end;
- val prove_prop = OuterParse.prop >>
- (fn str => Toplevel.print o
- Toplevel.local_theory_to_proof NONE (set_up_thm str))
-
+ val prove_prop_parser = OuterParse.prop >> prove_prop
val kind = OuterKeyword.thy_goal
in
- OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
+ OuterSyntax.local_theory_to_proof "foobar" "proving a proposition"
+ kind prove_prop_parser
end *}
text {*
- The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be
+ The function @{text prove_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 Syntax.read_prop}, which converts a string into a proper proposition.
In Line 6 the function @{ML Proof.theorem_i} 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). Lines 9 to 11 contain the parser for the proposition.
+ about it). Line 9 contains the parser for the proposition.
If you now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, you obtain the following
- proof state:
+ proof state
\begin{isabelle}
\isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
@@ -991,7 +988,7 @@
@{text "1. True \<and> True"}
\end{isabelle}
- and you can build the proof
+ and you can build the following proof
\begin{isabelle}
\isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
@@ -1000,12 +997,6 @@
\isacommand{done}
\end{isabelle}
-
-
- (FIXME What do @{ML "Toplevel.theory"}
- @{ML "Toplevel.print"}
- @{ML Toplevel.local_theory} do?)
-
(FIXME read a name and show how to store theorems)
*}