# HG changeset patch # User Christian Urban # Date 1225370211 -3600 # Node ID 4daf913fdbe12402894922a83c89d40c281f2de8 # Parent 81e2d73f719165dd6ae33caca85e27a3390d4676 hakked latex so that it does not display ML {* *}; general tuning diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/FirstSteps.thy Thu Oct 30 13:36:51 2008 +0100 @@ -24,6 +24,8 @@ section {* Including ML-Code *} + + text {* The easiest and quickest way to include code in a theory is by using the \isacommand{ML} command. For example\smallskip @@ -37,18 +39,8 @@ 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 - can also contain value and function bindings. However on such \isacommand{ML} - commands the undo operation behaves slightly counter-intuitive, because - if you define\smallskip - -\isa{\isacommand{ML} -\isacharverbatimopen\isanewline -\hspace{5mm}@{ML_text "val foo = true"}\isanewline -\isacharverbatimclose\isanewline -@{ML_text "> true"}\smallskip} - - then Isabelle's undo operation has no effect on the definition of - @{ML_text "foo"}. Note that from now on we will drop the + 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 \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever we show code and its response. @@ -78,7 +70,7 @@ @{ML [display] "warning \"any string\""} - will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle. + 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: @@ -101,7 +93,7 @@ amounts of trace output. This rediretion can be achieved using the code *} -ML {* +ML{* val strip_specials = let fun strip ("\^A" :: _ :: cs) = strip cs @@ -113,7 +105,7 @@ Output.tracing_fn := (fn s => (TextIO.output (stream, (strip_specials s)); TextIO.output (stream, "\n"); - TextIO.flushOut stream)); + TextIO.flushOut stream)); *} text {* @@ -163,8 +155,8 @@ @{ML [display] "@{thm allI}"} @{ML [display] "@{simpset}"} - While antiquotations have many uses, they were introduced to avoid explicit - bindings for theorems such as + While antiquotations have many applications, they were originally introduced to + avoid explicit bindings for theorems such as *} ML {* @@ -172,14 +164,12 @@ *} text {* - These bindings were difficult to maintain and also could be overwritten - by bindings introduced by the user. This had the potential to break - definitional packages. This additional layer of maintenance complexity - can be avoided by using antiquotations, 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. 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 *} @@ -208,10 +198,8 @@ Sometimes the internal representation of terms can be surprisingly different from what you see at the user level, because the layers of - parsing/type checking/pretty printing can be quite elaborate. -*} + parsing/type-checking/pretty printing can be quite elaborate. -text {* \begin{exercise} Look at the internal term representation of the following terms, and find out why they are represented like this. @@ -246,24 +234,14 @@ which does not. Types can be constructed using the antiquotation @{text "@{typ \}"}. For example - - *} - - -text {* @{ML_response_fake [display] "@{typ \"bool \ nat\"}" "bool \ nat"} - (FIXME: Unlike the term antiquotation, @{text "@{typ \}"} does not print the - internal representation. Is there a reason for this, that needs to be explained - here?) - \begin{readmore} Types are described in detail in \isccite{sec:types}. Their definition and many useful operations can be found in @{ML_file "Pure/type.ML"}. \end{readmore} - - *} +*} section {* Constructing Terms and Types Manually *} @@ -271,7 +249,7 @@ text {* While antiquotations are very convenient for constructing terms and types, - they can only construct fixed terms. Unfortunately, one often needs to construct them + they can only construct fixed terms. Unfortunately, one often needs to construct terms dynamically. For example, a function that returns the implication @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the typ @{term "\"} as arguments can only be written as @@ -289,7 +267,8 @@ text {* The reason is that one cannot pass the arguments @{term P}, @{term Q} and - @{term "tau"} into an antiquotation. For example the following does not work. + @{term "tau"} into an antiquotation. For example the following does not work as + expected. *} ML {* @@ -350,6 +329,8 @@ section {* Type Checking *} +ML {* cterm_of @{theory} @{term "a + b = c"} *} + text {* We can freely construct and manipulate terms, since they are just @@ -364,11 +345,15 @@ Type checking is always relative to a theory context. For now we can use the @{ML "@{theory}"} antiquotation to get hold of the current theory. - For example we can write: + For example we can write + + @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"} + + or use the antiquotation @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} - and + A slightly more elaborate example is @{ML_response_fake [display] "let diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Parsing.thy Thu Oct 30 13:36:51 2008 +0100 @@ -15,7 +15,7 @@ Isabelle uses a rather general and sophisticated algorithm due to Earley, which is driven by priority grammars. Parsers for outer syntax are built up by functional parsing combinators. These combinators are a well-established technique for parsing, - which has, for example, been described in Paulson's classic book \cite{paulson-ml2}. + which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}. Isabelle developers are usually concerned with writing these outer syntax parsers, either for new definitional packages or for calling tactics with specific arguments. @@ -110,11 +110,11 @@ @{ML_response [display] "let - val just_h = ($$ \"h\") |-- ($$ \"e\") - val just_e = ($$ \"h\") --| ($$ \"e\") + val just_e = ($$ \"h\") |-- ($$ \"e\") + val just_h = ($$ \"h\") --| ($$ \"e\") val input = (explode \"hello\") in - (just_h input, just_e input) + (just_e input, just_h input) end" "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"} @@ -182,7 +182,7 @@ *} ML {* - fun p_followed_by_q p q r = +fun p_followed_by_q p q r = let val err = (fn _ => p ^ " is not followed by " ^ q) in @@ -258,7 +258,9 @@ 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). + @{ML "OuterLex.Command"} for commands). Some 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 @@ -269,7 +271,7 @@ OuterLex.Token (\,(OuterLex.Space, \" \"),\), OuterLex.Token (\,(OuterLex.Ident, \"world\"),\)]"} - produces three token where the first and the last are identifiers, since + 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. If we parse @@ -278,7 +280,18 @@ OuterLex.Token (\,(OuterLex.Keyword, \"|\"),\), OuterLex.Token (\,(OuterLex.Keyword, \"for\"),\)]"} - we obtain a list of command/keyword token. + we obtain a list of command and 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): + +@{ML_response_fake [display] +"let + val (keywords, commands) = OuterKeyword.get_lexicons () +in + (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) +end" +"([\"}\",\"{\",\],[\"\\",\"\\",\])"} Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example @@ -314,7 +327,10 @@ end" "([\"in\",\"in\",\"in\"],[\])"} - @{ML_open "OuterParse.enum1"} works similarly, except that the 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 "FAIL"}. @{ML "OuterParse.enum1"} works similarly, + except that the parsed list must be non-empty. *} @@ -331,7 +347,7 @@ *} -text {* FIXME funny output for a proposition *} +text {* (FIXME funny output for a proposition) *} @@ -562,21 +578,36 @@ *} -text {* - FIXME + + - @{text " - begin{verbatim} - type token = T.token ; - val toks : token list = OuterSyntax.scan ``theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }'' ; +ML {* + val toks = OuterSyntax.scan Position.none + "theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ; +*} + +ML {* print_depth 20 ; - List.map T.text_of toks ; - val proper_toks = List.filter T.is_proper toks ; - List.map T.kind_of proper_toks ; - List.map T.unparse proper_toks ; - List.map T.val_of proper_toks ; - end{verbatim}"} +*} + +ML {* + map OuterLex.text_of toks ; +*} + +ML {* + val proper_toks = filter OuterLex.is_proper toks ; +*} +ML {* + map OuterLex.kind_of proper_toks +*} + +ML {* + map OuterLex.unparse proper_toks ; +*} + +ML {* + OuterLex.stopper *} text {* diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Readme.thy --- a/CookBook/Readme.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Readme.thy Thu Oct 30 13:36:51 2008 +0100 @@ -8,7 +8,7 @@ \begin{itemize} \item You can make references to other Isabelle manuals using the - reference names from those manuals. For this the following + reference names from those manuals. To do this the following four latex commands are defined: \begin{center} diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Recipes/Antiquotes.thy Thu Oct 30 13:36:51 2008 +0100 @@ -1,24 +1,31 @@ theory Antiquotes -imports Main +imports "../Base" begin -section {* Two Document Antiquotations *} +section {* Useful Document Antiquotations *} text {* + {\bf Problem:} + How to keep ML-code included in a document in sync with the actual code.\smallskip - For writing documents using Isabelle it is often uesful to use - document antiquotations. Below we give the code for such an - antiquotation that typesets ML-code and also checks whether - the code is actually correct. In this way one can achieve that the - document is always in sync with code. + {\bf Solution:} This can be achieved using document antiquotations.\smallskip + + Document antiquotations are a convenient method for type-setting consitently + a group of items in a document. They can also be used for sophisticated + \LaTeX hacking. - Below we introduce the antiquotation @{text "@{ML_checked \"\\"}"} which - takes a piece of code as argument. We will check this code by sending - the ML-expression @{text "val _ = \"} to the ML-compiler (i.e.~the - function @{ML "ML_Context.eval_in"}). The code for this antiquotation - is as follows: + Below we give the code for two such + antiquotations that can be used to typeset ML-code and also to check whether + the code is actually compiles. In this way one can relatively easily + keep documents in sync with code. + + We first describe the antiquotation @{text "@{ML_checked \"\\"}"} which + takes a piece of code as argument. This code is checked by sending + the ML-expression @{text "val _ = \"} containing the given code to the + ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code + for this antiquotation is as follows: *} ML {* @@ -26,7 +33,8 @@ fun output_ml ml src ctxt txt = (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) + ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt + (space_explode "\n" txt)) val _ = ThyOutput.add_commands [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))] @@ -37,21 +45,25 @@ Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the code is approved by the compiler, the output function @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} - pretty prints the code. There are a number of options that are observed - when printing the code (for example @{text "[display]"}; for more information - about the options see \rsccite{sec:antiq}). + pretty prints the code. This function expects that the code is a list of strings + according to the line breaks (therefore the + @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list). + There are a number of options that are observed by @{ML ThyOutput.output_list} + when printing the code (for example @{text "[display]"} and @{text "[source]"}; + for more information about these options see \rsccite{sec:antiq}). - Since we - used the argument @{ML "Position.none"}, the compiler cannot give specific + Since we used the argument @{ML "Position.none"}, the compiler cannot give specific information about the line number where an error might have occurred. We can improve this code slightly by writing + The second *} ML {* fun output_ml ml src ctxt (txt,pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml txt); - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) + ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt + (space_explode "\n" txt)) val _ = ThyOutput.add_commands [("ML_checked", ThyOutput.args @@ -59,16 +71,12 @@ *} text {* - where the antiquotation can also handle position information. - (FIXME: say something about OuterParse.position) - *} ML {* - fun ml_pat (rhs, pat) = - let val pat' = implode (map (fn "\\" => "_" | s => s) (Symbol.explode pat)) + let val pat' = implode (map (fn "\" => "_" | s => s) (Symbol.explode pat)) in "val " ^ pat' ^ " = " ^ rhs end; @@ -80,7 +88,6 @@ (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) - *} diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Recipes/NamedThms.thy Thu Oct 30 13:36:51 2008 +0100 @@ -9,46 +9,53 @@ {\bf Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules. Users should be able to declare @{text foo}-rules in the theory, - which are then used by some method.\smallskip + which are then used in a method.\smallskip - {\bf Solution:} This can be achieved using + {\bf Solution:} This can be achieved using named theorem lists.\smallskip + + Named theorem lists can be set up using the code *} + ML {* - structure FooRules = NamedThmsFun( - val name = "foo" - val description = "Rules for foo" - ); +structure FooRules = NamedThmsFun ( + val name = "foo" + val description = "Rules for foo"); *} - -setup FooRules.setup +(*<*)setup FooRules.setup(*>*) text {* + and the command + + @{ML_text [display] "setup FooRules.setup"} + This code declares a context data slot where the theorems are stored, an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options to adding and deleting theorems) and an internal ML interface to retrieve and modify the theorems. Furthermore, the facts are made available on the user level under the dynamic - fact name @{text foo}. For example: + fact name @{text foo}. For example we can declare two lemmas to be of the kind + @{ML_text foo}: *} lemma rule1[foo]: "A" sorry lemma rule2[foo]: "B" sorry +text {* undeclare them: *} + declare rule1[foo del] +text {* and query them: *} + thm foo text {* In an ML-context the rules marked with @{ML_text "foo"} an be retrieved using -*} -ML {* FooRules.get @{context} *} + @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"} - -text {* \begin{readmore} For more information see @{ML_file "Pure/Tools/named_thms.ML"}. \end{readmore} diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Solutions.thy Thu Oct 30 13:36:51 2008 +0100 @@ -7,20 +7,20 @@ text {* \solution{fun:revsum} *} ML {* - fun rev_sum t = - let - fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u - | dest_sum u = [u] - in - foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) - end; +fun rev_sum t = +let + fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u + | dest_sum u = [u] + in + foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) + end; *} text {* \solution{fun:makesum} *} ML {* - fun make_sum t1 t2 = - HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) +fun make_sum t1 t2 = + HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} end \ No newline at end of file diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/document/root.tex --- a/CookBook/document/root.tex Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/document/root.tex Thu Oct 30 13:36:51 2008 +0100 @@ -9,8 +9,16 @@ \usepackage{rail} \usepackage{url} \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry} +\usepackage{pdfsetup} -% Cross references to other manuals: +\urlstyle{rm} +\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text +\renewcommand{\isastyleminor}{\tt\slshape}% +\renewcommand{\isastyle}{\small\tt\slshape}% +\isadroptag{theory} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% For cross references to the other manuals: \usepackage{xr} \externaldocument[I-]{implementation} \newcommand{\impref}[1]{\ref{I-#1}} @@ -21,41 +29,54 @@ \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} -\usepackage{pdfsetup} - -\urlstyle{rm} -\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text -\renewcommand{\isastyleminor}{\tt\slshape}% -\renewcommand{\isastyle}{\small\tt\slshape}% -\isadroptag{theory} - +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sane default for proof documents \parindent 0pt\parskip 0.6ex -% for comments on the margin +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% to work around a problem with \isanewline +\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% FIXME: WHAT DOES THIS DO? +\renewenvironment{isabelle} +{\begin{trivlist}\begin{isabellebody}\small\item\relax} +{\end{isabellebody}\end{trivlist}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% for exercises, comments and readmores +\newtheorem{exercise}{Exercise}[section] +\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} + \newcommand{\readmoremarginpar}[1]% {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} \newenvironment{readmore}% {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} -% to work around a problem with \isanewline -\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} - -\renewenvironment{isabelle} -{\begin{trivlist}\begin{isabellebody}\small\item\relax} -{\end{isabellebody}\end{trivlist}} - -% for exercises and comments -\newtheorem{exercise}{Exercise}[section] -\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} - +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% FIXME: THIS SHOULD NOT BE USED ANYMORE % a table environment with proper indentation -\newenvironment{mytable}{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}{\end{tabular}\end{trivlist}} +\newenvironment{mytable} +{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}} +{\end{tabular}\end{trivlist}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \hyphenation{Isabelle} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% this hack is for getting rid of the ML {* ... *} +% scaffolding around function definitions +\newenvironment{vanishML}{% +\renewcommand{\isacommand}[1]{}% +\renewcommand{\isacharverbatimopen}{}% +\renewcommand{\isacharverbatimclose}{}% +\hspace{-1.5mm}\mbox{}}{} + +\renewcommand{\isatagML}{\begin{vanishML}} +\renewcommand{\endisatagML}{\end{vanishML}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{document} \title{\mbox{}\\[-10ex] @@ -71,7 +92,6 @@ \tableofcontents - % generated text of all theories \input{session} diff -r 81e2d73f7191 -r 4daf913fdbe1 cookbook.pdf Binary file cookbook.pdf has changed