diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/Readme.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ProgTutorial/Readme.thy Thu Mar 19 13:28:16 2009 +0100 @@ -0,0 +1,159 @@ +theory Readme +imports Base +begin + +chapter {* Comments for Authors *} + +text {* + + \begin{itemize} + \item This tutorial can be compiled on the command-line with: + + @{text [display] "$ isabelle make"} + + 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 & @{text "\\ichcite{\}"} & @{text "\\isccite{\}"}\\ + Isar Reference Manual & @{text "\\rchcite{\}"} & @{text "\\rsccite{\}"}\\ + \end{tabular} + \end{center} + + So @{text "\\ichcite{ch:logic}"} 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$] @{text "@{ML \"expr\" for vars in structs}"} should be used + for displaying any ML-ex\-pression, because the antiquotation checks whether + the expression is valid ML-code. The @{text "for"}- and @{text + "in"}-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} + @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ + @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\ + @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ + \end{tabular} + \end{center} + + \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to + display ML-expressions and their response. The first expression is checked + like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern + that specifies the result the first expression produces. This pattern can + contain @{text [quotes] "\"} 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} + @{text "@{ML_response \"1+2\" \"3\"}"}\\ + @{text "@{ML_response \"(1+2,3)\" \"(3,\)\"}"} + \end{tabular} + \end{center} + + which produce respectively + + \begin{center}\small + \begin{tabular}{p{3cm}p{3cm}} + @{ML_response "1+2" "3"} & + @{ML_response "(1+2,3)" "(3,\)"} + \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$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just + like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} 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} + @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ + & @{text "\"a + b = c\"}"}\smallskip\\ + @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ + & @{text "\"Exception FAIL raised\"}"} + \end{tabular} + \end{center} + + which produce respectively + + \begin{center}\small + \begin{tabular}{p{7.2cm}} + @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\ + @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} + \end{tabular} + \end{center} + + This output mimics to some extend what the user sees when running the + code. + + \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} 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} + @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\ + & @{text "\"Type unification failed \\"}"} + \end{tabular} + \end{center} + + \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when + referring to a file. It checks whether the file exists. An example + is + + @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"} + \end{itemize} + + The listed antiquotations honour options including @{text "[display]"} and + @{text "[quotes]"}. For example + + \begin{center}\small + @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} + \end{center} + + whereas + + \begin{center}\small + @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} + \end{center} + + \item Functions and value bindings cannot be defined inside antiquotations; they need + to be included inside \isacommand{ML}~@{text "\ \ \"} + 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}~@{text "\ \ \"} + for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The + tag is \isa{\%linenosgray} when the numbered text should be gray. + + \end{itemize} + +*} + + + +end \ No newline at end of file