# HG changeset patch # User Christian Urban # Date 1227590367 0 # Node ID 3d4b49921cdb418c325a784939cab19a1a39d0e5 # Parent a0edabf14457d326900724f4a046915503c0e295 tuned diff -r a0edabf14457 -r 3d4b49921cdb CookBook/FirstSteps.thy --- 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 =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} - 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 \}"} 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\", \) $ Free (\"x\", \)"} @@ -234,7 +233,7 @@ @{ML_response [display] "@{term \"P x \ Q x\"}" "Const (\"==>\", \) $ \ $ \"} @{ML_response [display] "@{prop \"P x \ Q x\"}" "Const (\"==>\", \) $ \ $ \"} - which does not. + which does not (since it is already constructed using the meta-implication). Types can be constructed using the antiquotation @{text "@{typ \}"}. 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 \ + misinterpreted as open subgoals. The wrapper @{text "# :: prop \ 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 \ Q \ Q \ 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 diff -r a0edabf14457 -r 3d4b49921cdb CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Nov 24 02:51:08 2008 +0100 +++ b/CookBook/Intro.thy Tue Nov 25 05:19:27 2008 +0000 @@ -16,10 +16,10 @@ text {* This cookbook targets an audience who already knows how to use Isabelle for writing theories and proofs. We also assume that readers are - familiar with Standard ML, the programming language in which + familiar with Standard ML (SML), the programming language in which most of Isabelle is implemented. If you are unfamiliar with either of these two subjects, you should first work through the Isabelle/HOL - tutorial \cite{isa-tutorial} or Paulson's book on Standard ML + tutorial \cite{isa-tutorial} or Paulson's book on SML \cite{paulson-ml2}. *} @@ -57,12 +57,9 @@ learn from other people's code. \end{description} - Since Isabelle is not a finished product, these manuals, just like - the implementation itself, are always under construction. This can - be difficult and frustrating at times, especially when interfaces changes - occur frequently. But it is a reality that progress means changing - things (FIXME: need some short and convincing comment that this - is a strategy, not a problem that should be solved). + The Cookbook is written in such a way that the code examples in it are + synchronised with fairly recent versions of the code. + *} diff -r a0edabf14457 -r 3d4b49921cdb CookBook/Parsing.thy --- 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 (\,(OuterLex.Ident, \"hello\"),\), - Token (\,(OuterLex.Space, \" \"),\), - Token (\,(OuterLex.Ident, \"world\"),\)]"} +"[Token (\,(Ident, \"hello\"),\), + Token (\,(Space, \" \"),\), + Token (\,(Ident, \"world\"),\)]"} + + 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 (\,(Ident, \"hello\"), \), Token (\,(Ident, \"world\"), \)]"} + + 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 (\,(OuterLex.Command, \"inductive\"),\), - Token (\,(OuterLex.Keyword, \"|\"),\), - Token (\,(OuterLex.Keyword, \"for\"),\)]"} +@{ML_response_fake [display] +"filtered_input \"inductive | for\"" +"[Token (\,(Command, \"inductive\"),\), + Token (\,(Keyword, \"|\"),\), + Token (\,(Keyword, \"for\"),\)]"} - 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 @@ "([\"}\",\"{\",\],[\"\\",\"\\",\])"} 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\"],[\])"} - @{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) *} diff -r a0edabf14457 -r 3d4b49921cdb cookbook.pdf Binary file cookbook.pdf has changed