theory Readme+ −
imports Base+ −
begin+ −
+ −
chapter \<open>Comments for Authors\<close>+ −
+ −
text \<open>+ −
+ −
\begin{itemize}+ −
\item This tutorial can be compiled on the command-line with:+ −
+ −
@{text [display] "$ isabelle build -c -v -d . Cookbook"}+ −
+ −
You very likely need a recent snapshot of Isabelle in order to compile+ −
the tutorial. Some parts of the tutorial also rely on compilation with+ −
PolyML.+ −
+ −
\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:+ −
+ −
\begin{center}+ −
\begin{tabular}{l|c|c}+ −
& Chapters & Sections\\\hline+ −
Implementation Manual & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\+ −
Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
So \<open>\ichcite{ch:logic}\<close> yields a reference for the chapter about logic + −
in the implementation manual, namely \ichcite{ch:logic}.+ −
+ −
\item There are various document antiquotations defined for the + −
tutorial. They allow to check the written text against the current+ −
Isabelle code and also allow to show responses of the ML-compiler.+ −
Therefore authors are strongly encouraged to use antiquotations wherever+ −
appropriate.+ −
+ −
The following antiquotations are defined:+ −
+ −
\begin{itemize}+ −
\item[$\bullet$] \<open>@{ML \<open>expr\<close> for vars in structs}\<close> should be used+ −
for displaying any ML-ex\-pression, because the antiquotation checks whether+ −
the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open+ −
expressions by giving a list of free variables. The latter is used to+ −
indicate in which structure or structures the ML-expression should be+ −
evaluated. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{lll}+ −
\<open>@{ML \<open>1 + 3\<close>}\<close> & & @{ML \<open>1 + 3\<close>}\\+ −
\<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\+ −
\<open>@{ML explode in Symbol}\<close> & & @{ML explode in Symbol}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to+ −
display ML-expressions and their response. The first expression is checked+ −
like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern+ −
that specifies the result the first expression produces. This pattern can+ −
contain @{text [quotes] "_"} (which will be printed as @{text [quotes] "\<dots>"}) + −
for parts that you like to omit. The response of the+ −
first expression will be checked against this pattern. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{l}+ −
\<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\+ −
\<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}\<close>+ −
\end{tabular}+ −
\end{center}+ −
+ −
which produce respectively+ −
+ −
\begin{center}\small+ −
\begin{tabular}{p{3cm}p{3cm}}+ −
@{ML_matchresult \<open>1+2\<close> \<open>3\<close>} & + −
@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}+ −
\end{tabular}+ −
\end{center}+ −
+ −
Note that this antiquotation can only be used when the result can be+ −
constructed: it does not work when the code produces an exception or returns + −
an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).+ −
+ −
\item[$\bullet$] \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> works just+ −
like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above,+ −
except that the result-specification is not checked. Use this antiquotation+ −
when the result cannot be constructed or the code generates an+ −
exception. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
\<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>\<close>\\+ −
& \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ + −
\<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ + −
& \<open>\<open>Exception FAIL raised\<close>}\<close>+ −
\end{tabular}+ −
\end{center}+ −
+ −
which produce respectively+ −
+ −
\begin{center}\small+ −
\begin{tabular}{p{7.2cm}}+ −
@{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\+ −
@{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>}+ −
\end{tabular}+ −
\end{center}+ −
+ −
This output mimics to some extend what the user sees when running the+ −
code.+ −
+ −
\item[$\bullet$] \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> can be+ −
used to show erroneous code. Neither the code nor the response will be+ −
checked. An example is:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
\<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\+ −
& \<open>"Type unification failed \<dots>"}\<close>+ −
\end{tabular}+ −
\end{center}+ −
+ −
\item[$\bullet$] \<open>@{ML_response \<open>expr\<close>}\<close> can be+ −
used to show the expression and the corresponding output. An example is:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
\<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close>+ −
\end{tabular}+ −
\end{center}+ −
+ −
which produces+ −
+ −
\begin{center}\small+ −
@{ML_response \<open>1 upto 10\<close>}+ −
\end{center}+ −
+ −
You can give a second argument for the expected response. This is matched against the actual+ −
response by crude wildcard matching where whitespace and \<open>\<dots>\<close> are treated as wildcard.+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
\<open>@{ML_response\<close> & \<open>\<open>1 upto 20\<close>\<close>\\+ −
& \<open>"[1, 2, 3, 4, 5, 6\<dots>\<close>\\+ −
& \<open>18, 19, 20]"}\<close>\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
will produce+ −
+ −
@{ML_response \<open>1 upto 20\<close>+ −
\<open>[1, 2, 3, 4, 5, 6\<dots> + −
18, 19, 20]\<close>}+ −
+ −
Note that exceptions are also converted to strings and can thus be checked in the response + −
string.+ −
+ −
@{ML_response \<open>error "hallo"\<close>+ −
\<open>hallo\<close>}+ −
+ −
So as a rule of thumb, to facilitate result checking use prefer this order:+ −
\begin{enumerate}+ −
\item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> + −
\item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>+ −
\item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>+ −
\item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>+ −
\end{enumerate}+ −
+ −
\item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when+ −
referring to a file. It checks whether the file exists. An example+ −
is + −
+ −
@{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>}+ −
\end{itemize}+ −
+ −
The listed antiquotations honour options including \<open>[display]\<close> and + −
\<open>[gray]\<close>. For example+ −
+ −
+ −
\item Functions and value bindings cannot be defined inside antiquotations; they need+ −
to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>+ −
environments. In this way they are also checked by the compiler. Some \LaTeX-hack in + −
the tutorial, however, ensures that the environment markers are not printed.+ −
+ −
\item Line numbers can be printed using + −
\isacommand{ML} \isa{\%linenos}~\<open>\<verbopen> \<dots> \<verbclose>\<close>+ −
for ML-code or \isacommand{lemma} \isa{\%linenos} \<open>...\<close> for proofs. The+ −
tag is \isa{\%linenosgray} when the numbered text should be gray. + −
+ −
\end{itemize}+ −
+ −
\<close>+ −
+ −
+ −
+ −
end+ −