# HG changeset patch # User Christian Urban # Date 1227491468 -3600 # Node ID a0edabf14457d326900724f4a046915503c0e295 # Parent 609f9ef73494becba6ed17cc2ff277040a807d78 added more material diff -r 609f9ef73494 -r a0edabf14457 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Sat Nov 01 15:20:36 2008 +0100 +++ b/CookBook/FirstSteps.thy Mon Nov 24 02:51:08 2008 +0100 @@ -28,7 +28,7 @@ text {* The easiest and quickest way to include code in a theory is - by using the \isacommand{ML} command. For example\smallskip + by using the \isacommand{ML}-command. For example\smallskip \isa{\isacommand{ML} \isacharverbatimopen\isanewline @@ -36,11 +36,11 @@ \isacharverbatimclose\isanewline @{ML_text "> 7"}\smallskip} - Expressions inside \isacommand{ML} commands are immediately evaluated, + Expressions inside \isacommand{ML}-commands are immediately evaluated, like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of - your Isabelle environment. The code inside the \isacommand{ML} command + your Isabelle environment. The code inside the \isacommand{ML}-command can also contain value and function bindings, and even those can be - undone when the proof script is retracted. From now on we will drop the + undone when the proof script is retracted. In what follows we will drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever we show code and its response. @@ -81,10 +81,10 @@ a function. 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 + output this funtion generates will be overwritten as soon as an error is raised. Therefore for printing anything more serious and elaborate, the function @{ML tracing} should be used. This function writes all output into - a separate tracing buffer. + a separate tracing buffer. For example @{ML [display] "tracing \"foo\""} @@ -119,18 +119,19 @@ section {* Antiquotations *} text {* - The main advantage of embedding all code - in a theory is that the code can contain references to entities defined - on the logical level of Isabelle. This is done using antiquotations. - For example, one can print out the name of - the current theory by typing + The main advantage of embedding all code in a theory is that the code can + contain references to entities defined on the logical level of Isabelle (by + this we mean definitions, theorems, terms and so on). This is done using + antiquotations. For example, one can print out the name of the current + theory by typing + @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"} where @{text "@{theory}"} is an antiquotation that is substituted with the - current theory (remember that we assumed we are inside the theory CookBook). - The name of this theory can be extracted using the function - @{ML "Context.theory_name"}. + current theory (remember that we assumed we are inside the theory + @{ML_text FirstSteps}). The name of this theory can be extracted using + the function @{ML "Context.theory_name"}. Note, however, that antiquotations are statically scoped, that is the value is determined at ``compile-time'', not ``run-time''. For example the function @@ -155,7 +156,7 @@ @{ML [display] "@{thm allI}"} @{ML [display] "@{simpset}"} - While antiquotations have many applications, they were originally introduced to + While antiquotations nowadays have many applications, they were originally introduced to avoid explicit bindings for theorems such as *} @@ -164,19 +165,21 @@ *} text {* - 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. 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. + 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 + 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. + *} section {* Terms and Types *} text {* - One way to construct terms of Isabelle on the ML level is by using the antiquotation - \mbox{@{text "@{term \}"}}: + One way to construct terms of Isabelle on the ML-level is by using the antiquotation + \mbox{@{text "@{term \}"}}. For example @{ML_response [display] "@{term \"(a::nat) + b = c\"}" "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} @@ -292,18 +295,33 @@ which theory they are defined. Guessing such internal names can sometimes be quite hard. Therefore Isabellle provides the antiquotation @{text "@{const_name \}"} which does the expansion automatically, for example: -*} - -text {* + + @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) - (FIXME: how to construct types manually) + Similarly, types can be constructed for example as follows: + +*} + +ML {* +fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) +*} + +text {* + which can be equally written as +*} + +ML {* +fun make_fun_type tau1 tau2 = tau1 --> tau2 +*} + +text {* \begin{readmore} There are many functions in @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms - easier.\end{readmore} + and types easier.\end{readmore} Have a look at these files and try to solve the following two exercises: @@ -327,14 +345,14 @@ *} -section {* Type Checking *} +section {* Type-Checking *} text {* 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 turns 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 @@ -386,7 +404,7 @@ shows "Q t" (*<*)oops(*>*) text {* - on the ML level:\footnote{Note that @{text "|>"} is reverse + on the ML-level:\footnote{Note that @{text "|>"} is reverse application. This combinator, and several variants are defined in @{ML_file "Pure/General/basics.ML"}.} @@ -395,7 +413,7 @@ val thy = @{theory} val assm1 = cterm_of thy @{prop \"\(x::nat). P x \ Q x\"} - val assm2 = cterm_of thy @{prop \"((P::nat\bool) t)\"} + val assm2 = cterm_of thy @{prop \"(P::nat\bool) t\"} val Pt_implies_Qt = assume assm1 @@ -447,14 +465,13 @@ @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ #(C)"} - where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals. + where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open + 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 \ prop"} is just the identity function and used as a syntactic marker. - (FIXME: maybe show how this is printed on the screen) - \begin{readmore} For more on goals see \isccite{sec:tactical-goals}. \end{readmore} @@ -476,7 +493,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 from the tutorial~\cite{isa-tutorial} into ML: *} lemma disj_swap: "P \ Q \ Q \ P" diff -r 609f9ef73494 -r a0edabf14457 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Sat Nov 01 15:20:36 2008 +0100 +++ b/CookBook/Parsing.thy Mon Nov 24 02:51:08 2008 +0100 @@ -32,7 +32,7 @@ *} -section {* Building Up Generic Parsers *} +section {* Building Generic Parsers *} text {* @@ -63,12 +63,15 @@ It is used for example in the function @{ML "(op !!)"} (see below). \end{itemize} - (FIXME: do the exception need to be explained, because the user cannot use them from ``outside''?) + However, note that these exception 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 + Scan.one}, in that it takes a predicate as argument and then parses exactly + one item from the input list satisfying this prediate. For example the + following parser either consumes an @{ML_text [quotes] "h"} or a @{ML_text + [quotes] "w"}: - Slightly more general than the parser @{ML "(op $$)"} is the function @{ML Scan.one}, in that it - takes a predicate as argument and then parses exactly one item from the input list - satisfying this prediate. For example the following parser either consumes an - @{ML_text [quotes] "h"} or a @{ML_text [quotes] "w"}: @{ML_response [display] "let @@ -132,6 +135,9 @@ end" "((\"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. + 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 followed by @{ML_text q}, or start a completely different parser @{ML_text r}, @@ -214,6 +220,16 @@ @{ML "Scan.repeat1"} is similar, but requires that the parser @{ML_text "p"} 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 + 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. + 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 first the parser @{ML_text p} and upon successful completion applies the @@ -264,10 +280,10 @@ generating precise error messages. The following\footnote{There is something funny going on with the pretty printing of the result token list.} -@{ML_response [display] "OuterSyntax.scan Position.none \"hello world\"" -"[OuterLex.Token (\,(OuterLex.Ident, \"hello\"),\), - OuterLex.Token (\,(OuterLex.Space, \" \"),\), - OuterLex.Token (\,(OuterLex.Ident, \"world\"),\)]"} +@{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\"" +"[Token (\,(OuterLex.Ident, \"hello\"),\), + Token (\,(OuterLex.Space, \" \"),\), + Token (\,(OuterLex.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 @@ -275,10 +291,10 @@ later on will require spaces, comments and the like to have been filtered out. If we parse -@{ML_response [display] "OuterSyntax.scan Position.none \"inductive|for\"" -"[OuterLex.Token (\,(OuterLex.Command, \"inductive\"),\), - OuterLex.Token (\,(OuterLex.Keyword, \"|\"),\), - OuterLex.Token (\,(OuterLex.Keyword, \"for\"),\)]"} +@{ML_response_fake [display] "OuterSyntax.scan Position.none \"inductive|for\"" +"[Token (\,(OuterLex.Command, \"inductive\"),\), + Token (\,(OuterLex.Keyword, \"|\"),\), + Token (\,(OuterLex.Keyword, \"for\"),\)]"} we obtain a list consiting of only command and keyword tokens. If you want to see which keywords and commands are currently known, use @@ -316,7 +332,7 @@ The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty list of items recognised by the parser @{ML_text p}, where the items are - separated by @{ML_text s}. For example + separated by the string @{ML_text s}. For example @{ML_response [display] "let @@ -326,14 +342,62 @@ 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"}. @{ML "OuterParse.enum1"} works similarly, - except that the parsed list must be non-empty. + 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\" +in + Scan.finite OuterLex.stopper (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input +end" +"([\"in\",\"in\",\"in\"],[])"} + + The function @{ML "OuterParse.!!!"} can be used to force termination of the + parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), + except that the error message is fixed to be @{text [quotes] "Outer syntax error"} + with a relatively precise description of the failure. For example: + +@{ML_response_fake [display] +"let + val input = OuterSyntax.scan Position.none \"in|\" + val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\" +in + Scan.error (OuterParse.!!! parse_bar_then_in) input +end" +"Exception ERROR \"Outer syntax error: keyword \"|\" expected, +but keyword in was found\" raised" +} *} -text {* FIXME explain @{ML "OuterParse.!!!"} *} + +ML {* +let + val input = filter OuterLex.is_proper (OuterSyntax.scan Position.none "(in foo)") +in + OuterParse.target input +end +*} + +section {* Positional Information *} + +text {* + + @{ML OuterParse.position} + +*} + +ML {* + OuterParse.position +*} + section {* Parsing Inner Syntax *} diff -r 609f9ef73494 -r a0edabf14457 CookBook/Readme.thy --- a/CookBook/Readme.thy Sat Nov 01 15:20:36 2008 +0100 +++ b/CookBook/Readme.thy Mon Nov 24 02:51:08 2008 +0100 @@ -7,7 +7,7 @@ text {* \begin{itemize} - \item You can make references to other Isabelle manuals using the + \item You can include references to other Isabelle manuals using the reference names from those manuals. To do this the following four latex commands are defined: @@ -25,21 +25,40 @@ \item There are various document antiquotations defined for the cookbook so that written text can be kept in sync with the Isabelle code and also that responses of the ML-compiler can be shown. - For example + The are: \begin{itemize} - \item[$\bullet$] @{text "@{ML \"\\"}"} - \item[$\bullet$] @{text "@{ML_open \"\\"}"} - \item[$\bullet$] @{text "@{ML_response \"\\"}"} - \item[$\bullet$] @{text "@{ML_response_fake \"\\"}"} - \item[$\bullet$] @{text "@{ML_file \"\\"}"} + \item[$\bullet$] {\bf @{text "@{ML \"\\"}"}} Should be used for value computations. It checks whether + the ML-expression is valid ML-code, but only works for closed expression. + \item[$\bullet$] {\bf @{text "@{ML_open \"\\" for \}"}} Works like @{ML_text ML}-antiquotation except, + that it can also deal with open expressions and expressions that need to be evaluated inside structures. + The free variables or structures need to be listed after the @{ML_text "for"}. For example + @{text "@{ML_open \"a + b\" for a b}"}. + \item[$\bullet$] {\bf @{text "@{ML_response \"\\" \"\\"}"}} The first + expression is checked like in the antiquotation @{text "@{ML \"\\"}"}; the + second is a pattern that specifies the result the first expression + produces. This specification can contain @{text [quotes] "\"} for parts that + can be omitted. The actual response will be checked against the + specification. For example @{text "@{ML_response \"(1+2,3)\" + \"(3,\)\"}"}. This antiquotation can only be used when the result can be + constructed. It does not work when the code produces an exception or is an + abstract datatype (like @{ML_type thm} or @{ML_type cterm}). + + \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\\" \"\\"}"}} Works like the + @{ML_text ML_response}-anti\-quotation, except that the result-specification is not + checked. + \item[$\bullet$] {\bf @{text "@{ML_file \"\\"}"}} Should be used when referring to a file. + It checks whether the file exists. \end{itemize} - (FIXME: explain their usage) + \item Functions and value bindings cannot be defined inside antiquotations; they need + to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} + environments. Some \LaTeX-hack, however, does not print the environment markers. \end{itemize} *} + end \ No newline at end of file diff -r 609f9ef73494 -r a0edabf14457 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Sat Nov 01 15:20:36 2008 +0100 +++ b/CookBook/antiquote_setup.ML Mon Nov 24 02:51:08 2008 +0100 @@ -24,7 +24,6 @@ fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; -fun ml_decl txt = txt fun output_ml_open ml src ctxt ((txt,ovars),pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); diff -r 609f9ef73494 -r a0edabf14457 cookbook.pdf Binary file cookbook.pdf has changed