--- a/CookBook/FirstSteps.thy Mon Nov 24 02:51:08 2008 +0100
+++ b/CookBook/FirstSteps.thy Tue Nov 25 05:19:27 2008 +0000
@@ -7,10 +7,9 @@
text {*
- Isabelle programming is done in Standard ML.
- Just like lemmas and proofs, SML-code in Isabelle is part of a
- theory. If you want to follow the code written in this chapter, we
- assume you are working inside the theory defined by
+ Isabelle programming is done in SML. Just like lemmas and proofs, SML-code
+ in Isabelle is part of a theory. If you want to follow the code written in
+ this chapter, we assume you are working inside the theory defined by
\begin{center}
\begin{tabular}{@ {}l}
@@ -64,16 +63,16 @@
text {*
- During developments you might find it necessary to quickly inspect some data
+ During development you might find it necessary to inspect some data
in your code. This can be done in a ``quick-and-dirty'' fashion using
the function @{ML "warning"}. For example
@{ML [display] "warning \"any string\""}
- will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle.
- If you develop under PolyML, then there is a convenient, though again
- ``quick-and-dirty'', method for converting values into strings,
- for example:
+ will print out @{ML_text [quotes] "any string"} inside the response buffer
+ of Isabelle. This function expects a string. If you develop under PolyML,
+ then there is a convenient, though again ``quick-and-dirty'', method for
+ converting values into strings, for example:
@{ML [display] "warning (makestring 1)"}
@@ -82,13 +81,13 @@
The funtion @{ML "warning"} should only be used for testing purposes, because any
output this funtion generates will be overwritten as soon as an error is
- raised. Therefore for printing anything more serious and elaborate, the
+ raised. For printing anything more serious and elaborate, the
function @{ML tracing} should be used. This function writes all output into
a separate tracing buffer. For example
@{ML [display] "tracing \"foo\""}
- It is also possible to redirect the channel where the @{ML_text "foo"} is
+ It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is
printed to a separate file, e.g. to prevent Proof General from choking on massive
amounts of trace output. This rediretion can be achieved using the code
*}
@@ -156,7 +155,7 @@
@{ML [display] "@{thm allI}"}
@{ML [display] "@{simpset}"}
- While antiquotations nowadays have many applications, they were originally introduced to
+ While antiquotations have many applications, they were originally introduced to
avoid explicit bindings for theorems such as
*}
@@ -168,7 +167,7 @@
These bindings were difficult to maintain and also could be accidentally
overwritten by the user. This usually broke definitional
packages. Antiquotations solve this problem, since they are ``linked''
- statically at compile-time. However, that also sometimes limits there
+ statically at compile-time. However, that also sometimes limits their
applicability. In the course of this introduction, we will learn more about
these antiquotations: they greatly simplify Isabelle programming since one
can directly access all kinds of logical elements from ML.
@@ -184,7 +183,7 @@
@{ML_response [display] "@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
- This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
+ This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
representation of this term. This internal representation corresponds to the
datatype @{ML_type "term"}.
@@ -222,7 +221,7 @@
@{ML [display] "print_depth 50"}
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
- inserting the invisible @{text "Trueprop"} coercions whenever necessary.
+ inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
Consider for example
@{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"}
@@ -234,7 +233,7 @@
@{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
@{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
- which does not.
+ which does not (since it is already constructed using the meta-implication).
Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
@@ -283,7 +282,7 @@
to both functions.
One tricky point in constructing terms by hand is to obtain the
- fully qualified name for constants. For example the names for @{text "zero"} or
+ fully qualified name for constants. For example the names for @{text "zero"} and
@{text "+"} are more complex than one first expects, namely
\begin{center}
@@ -300,7 +299,7 @@
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
- Similarly, types can be constructed for example as follows:
+ Similarly, types can be constructed manually, for example as follows:
*}
@@ -352,14 +351,14 @@
We can freely construct and manipulate terms, since they are just
arbitrary unchecked trees. However, we eventually want to see if a
term is well-formed, or type checks, relative to a theory.
- Type-checking is done via the function @{ML cterm_of}, which turns
+ Type-checking is done via the function @{ML cterm_of}, which converts
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
Unlike @{ML_type term}s, which are just trees, @{ML_type
"cterm"}s are abstract objects that are guaranteed to be
- type-correct, and that can only be constructed via the official
- interfaces.
+ type-correct, and that can only be constructed via the ``official
+ interfaces''.
- Type checking is always relative to a theory context. For now we can use
+ Type checking is always relative to a theory context. For now we use
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
For example we can write
@@ -383,7 +382,7 @@
\begin{exercise}
Check that the function defined in Exercise~\ref{fun:revsum} returns a
- result that type checks.
+ result that type-checks.
\end{exercise}
*}
@@ -391,9 +390,9 @@
section {* Theorems *}
text {*
- Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
- abstract objects that can only be built by going through the kernel
- interfaces, which means that all your proofs will be checked.
+ Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
+ that can only be built by going through interfaces, which means that all your proofs
+ will be checked.
To see theorems in ``action'', let us give a proof for the following statement
*}
@@ -444,7 +443,7 @@
\begin{readmore}
- For how the functions @{text "assume"}, @{text "forall_elim"} etc work
+ For the functions @{text "assume"}, @{text "forall_elim"} etc
see \isccite{sec:thms}. The basic functions for theorems are defined in
@{ML_file "Pure/thm.ML"}.
\end{readmore}
@@ -469,7 +468,7 @@
subgoals.
Since the goal @{term C} can potentially be an implication, there is a
@{text "#"} wrapped around it, which prevents that premises are
- misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
+ misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
prop"} is just the identity function and used as a syntactic marker.
\begin{readmore}
@@ -484,8 +483,8 @@
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
sequences. However in day-to-day Isabelle programming, one rarely
constructs sequences explicitly, but uses the predefined tactic
- combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}).
- (FIXME: Pointer to the old reference manual)
+ combinators (tacticals) instead. See @{ML_file "Pure/tctical.ML"}
+ for the code; see Chapters 3 and 4 in the old Isabelle Reference Manual.
\end{readmore}
While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
@@ -493,7 +492,7 @@
exception of possibly instantiating schematic variables.
To see how tactics work, let us transcribe a simple @{text apply}-style
- proof from the tutorial~\cite{isa-tutorial} into ML:
+ proof into ML:
*}
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -510,7 +509,7 @@
(empty in the proof at hand)
with the variables @{text xs} that will be generalised once the
goal is proved. The @{text "tac"} is the tactic which proves the goal and which
- can make use of the local assumptions.
+ can make use of the local assumptions (there are none in this example).
@{ML_response_fake [display]
"let
--- a/CookBook/Parsing.thy Mon Nov 24 02:51:08 2008 +0100
+++ b/CookBook/Parsing.thy Tue Nov 25 05:19:27 2008 +0000
@@ -21,7 +21,7 @@
\begin{readmore}
The library
- for writing parser combinators can be split up, roughly, into two parts.
+ for writing parser combinators is split up, roughly, into two parts.
The first part consists of a collection of generic parser combinators defined
in the structure @{ML_struct Scan} in the file
@{ML_file "Pure/General/scan.ML"}. The second part of the library consists of
@@ -37,7 +37,7 @@
text {*
Let us first have a look at parsing strings using generic parsing combinators.
- The function @{ML "(op $$)"} takes a string and will ``consume'' this string from
+ The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from
a given input list of strings. ``Consume'' in this context means that it will
return a pair consisting of this string and the rest of the input list.
For example:
@@ -63,7 +63,7 @@
It is used for example in the function @{ML "(op !!)"} (see below).
\end{itemize}
- However, note that these exception private to the parser and cannot be accessed
+ However, note that these exceptions are private to the parser and cannot be accessed
by the programmer (for example to handle them).
Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
@@ -108,7 +108,7 @@
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing funtion
- for parsers, except that they discard the item parsed by the first (respectively second)
+ for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example
@{ML_response [display]
@@ -136,7 +136,16 @@
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
The function @{ML Scan.option} works similarly, except no default value can
- be given and in the failure case this parser does nothing.
+ be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
+
+@{ML_response [display]
+"let
+ val p = Scan.option ($$ \"h\")
+ val input1 = (explode \"hello\")
+ val input2 = (explode \"world\")
+in
+ (p input1, p input2)
+end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
The function @{ML "(op !!)"} helps to produce appropriate error messages
during parsing. For example if one wants to parse that @{ML_text p} is immediately
@@ -157,7 +166,7 @@
caused by the
failure of @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation
can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of
- parsing in case of failure and invokes an error message. For example if we invoke the parser
+ parsing in case of a failure and invokes an error message. For example if we invoke the parser
@{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
@@ -184,7 +193,7 @@
Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want
to generate the correct error message for p-followed-by-q, then
- we have to write, for example
+ we have to write:
*}
ML {*
@@ -221,14 +230,15 @@
succeeds at least once.
Also note that the parser would have aborted with the exception @{ML_text MORE}, if
- we had run it only on just @{ML_text [quotes] "hhhh"}. This can be awoided using
+ we had run it only on just @{ML_text [quotes] "hhhh"}. This can be avoided using
the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With
them we can write
@{ML_response [display] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
- However, the Isabelle-develloper rarely needs to do this kind of wrapping manually.
+ However, this kind of manually wrapping needs to be done only very rarely
+ in practise, because it is already done by the infrastructure for you.
After parsing succeeded, one nearly always wants to apply a function on the parsed
items. This is done using the function @{ML_open "(p >> f)" for p f} which runs
@@ -272,31 +282,58 @@
The structure @{ML_struct OuterLex} defines several kinds of token (for example
@{ML "OuterLex.Ident"} for identifiers, @{ML "OuterLex.Keyword"} for keywords and
- @{ML "OuterLex.Command"} for commands). Some parsers take into account the
+ @{ML "OuterLex.Command"} for commands). Some token parsers take into account the
kind of token.
- We can generate a token list using the function @{ML "OuterSyntax.scan"}, which we give
- below @{ML "Position.none"} as argument since, at the moment, we are not interested in
- generating precise error messages. The following\footnote{There is something funny
- going on with the pretty printing of the result token list.}
+ We can generate a token list out of a string using the function @{ML
+ "OuterSyntax.scan"}, which we give below @{ML "Position.none"} as argument
+ since, at the moment, we are not interested in generating precise error
+ messages. The following
@{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\""
-"[Token (\<dots>,(OuterLex.Ident, \"hello\"),\<dots>),
- Token (\<dots>,(OuterLex.Space, \" \"),\<dots>),
- Token (\<dots>,(OuterLex.Ident, \"world\"),\<dots>)]"}
+"[Token (\<dots>,(Ident, \"hello\"),\<dots>),
+ Token (\<dots>,(Space, \" \"),\<dots>),
+ Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
+
+ produces three tokens where the first and the last are identifiers, since
+ @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match any
+ other syntactic category.\footnote{Note that because of a possible a bug in
+ the PolyML runtime system the result is printed as @{text "?"}, instead of
+ the token.} The second indicates a space.
+
+ Many parsing functions later on will require spaces, comments and the like
+ to have been filtered out. In what follows below, we are going to use the
+ functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
+
- produces three tokens where the first and the last are identifiers, since
- @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match
- any other category. The second indicates a space. Many parsing functions
- later on will require spaces, comments and the like to have been filtered out.
+@{ML_response_fake [display]
+"let
+ val input = OuterSyntax.scan Position.none \"hello world\"
+in
+ filter OuterLex.is_proper input
+end"
+"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
+
+ For convenience we are going to use the function
+
+*}
+
+ML {*
+fun filtered_input str =
+ filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
+*}
+
+text {*
+
If we parse
-@{ML_response_fake [display] "OuterSyntax.scan Position.none \"inductive|for\""
-"[Token (\<dots>,(OuterLex.Command, \"inductive\"),\<dots>),
- Token (\<dots>,(OuterLex.Keyword, \"|\"),\<dots>),
- Token (\<dots>,(OuterLex.Keyword, \"for\"),\<dots>)]"}
+@{ML_response_fake [display]
+"filtered_input \"inductive | for\""
+"[Token (\<dots>,(Command, \"inductive\"),\<dots>),
+ Token (\<dots>,(Keyword, \"|\"),\<dots>),
+ Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
- we obtain a list consiting of only command and keyword tokens.
+ we obtain a list consiting of only a command and two keyword tokens.
If you want to see which keywords and commands are currently known, use
the following (you might have to adjust the @{ML print_depth} in order to
see the complete list):
@@ -310,11 +347,11 @@
"([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}
Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
-
+
@{ML_response [display]
"let
- val input1 = OuterSyntax.scan Position.none \"where for\"
- val input2 = OuterSyntax.scan Position.none \"|in\"
+ val input1 = filtered_input \"where for\"
+ val input2 = filtered_input \"| in\"
in
(OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
end"
@@ -324,7 +361,7 @@
@{ML_response [display]
"let
- val input = OuterSyntax.scan Position.none \"|in\"
+ val input = filtered_input \"| in\"
in
(OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
end"
@@ -336,24 +373,23 @@
@{ML_response [display]
"let
- val input = OuterSyntax.scan Position.none \"in|in|in\\n\"
+ val input = filtered_input \"in | in | in end\"
in
(OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
end"
"([\"in\",\"in\",\"in\"],[\<dots>])"}
- @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
- be non-empty.
-
- Note that we had to add a @{ML_text [quotes] "\\n"} at the end of the parsed
- string, otherwise the parser would have consumed all tokens and then failed with
- the exception @{ML_text "MORE"}. Like in the previous section, we can avoid
- this exception using the wrapper @{ML Scan.finite}. This time, however, we
- have to use the ``stopper-token'' @{ML OuterLex.stopper}. We can write
+ @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
+ be non-empty. Note that we had to add a @{ML_text [quotes] "end"} at the end
+ of the parsed string, otherwise the parser would have consumed all tokens
+ and then failed with the exception @{ML_text "MORE"}. Like in the previous
+ section, we can avoid this exception using the wrapper @{ML
+ Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
+ OuterLex.stopper}. We can write
@{ML_response [display]
"let
- val input = OuterSyntax.scan Position.none \"in|in|in\"
+ val input = filtered_input \"in | in | in\"
in
Scan.finite OuterLex.stopper (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
end"
@@ -366,7 +402,7 @@
@{ML_response_fake [display]
"let
- val input = OuterSyntax.scan Position.none \"in|\"
+ val input = filtered_input \"in |\"
val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
in
Scan.error (OuterParse.!!! parse_bar_then_in) input
@@ -377,15 +413,6 @@
*}
-
-ML {*
-let
- val input = filter OuterLex.is_proper (OuterSyntax.scan Position.none "(in foo)")
-in
- OuterParse.target input
-end
-*}
-
section {* Positional Information *}
text {*
@@ -410,6 +437,19 @@
*}
+ML {*
+ OuterParse.opt_target
+*}
+
+ML {*
+ OuterParse.opt_target --
+ OuterParse.fixes --
+ OuterParse.for_fixes --
+ Scan.optional (OuterParse.$$$ "where" |--
+ OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+
+*}
+
text {* (FIXME funny output for a proposition) *}