1 theory Readme

     2 imports Base

     3 begin

     4 

     5 chapter {* Comments for Authors *}

     6 

     7 text {*

     8 

     9   \begin{itemize}

    10   \item This tutorial can be compiled on the command-line with:

    11 

    12   @{text [display] "$ isabelle make"}

    13 

    14   You very likely need a recent snapshot of Isabelle in order to compile

    15   the tutorial. Some parts of the tutorial also rely on compilation with

    16   PolyML.

    17 

    18   \item You can include references to other Isabelle manuals using the 

    19   reference names from those manuals. To do this the following

    20   four \LaTeX{} commands are defined:

    21   

    22   \begin{center}

    23   \begin{tabular}{l|c|c}

    24    & Chapters & Sections\\\hline

    25   Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\

    26   Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\

    27   \end{tabular}

    28   \end{center}

    29 

    30   So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 

    31   in the implementation manual, namely \ichcite{ch:logic}.

    32 

    33   \item There are various document antiquotations defined for the 

    34   tutorial. They allow to check the written text against the current

    35   Isabelle code and also allow to show responses of the ML-compiler.

    36   Therefore authors are strongly encouraged to use antiquotations wherever

    37   appropriate.

    38   

    39   The following antiquotations are defined:

    40 

    41   \begin{itemize}

    42   \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used

    43   for displaying any ML-ex\-pression, because the antiquotation checks whether

    44   the expression is valid ML-code. The @{text "for"}- and @{text

    45   "in"}-arguments are optional. The former is used for evaluating open

    46   expressions by giving a list of free variables. The latter is used to

    47   indicate in which structure or structures the ML-expression should be

    48   evaluated. Examples are:

    49   

    50   \begin{center}\small

    51   \begin{tabular}{lll}

    52   @{text "@{ML \"1 + 3\"}"}         &                 & @{ML "1 + 3"}\\

    53   @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\

    54   @{text "@{ML Ident in OuterLex}"} &                 & @{ML Ident in OuterLex}\\

    55   \end{tabular}

    56   \end{center}

    57 

    58   \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to

    59   display ML-expressions and their response.  The first expression is checked

    60   like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern

    61   that specifies the result the first expression produces. This pattern can

    62   contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the

    63   first expression will be checked against this pattern. Examples are:

    64 

    65   \begin{center}\small

    66   \begin{tabular}{l}

    67   @{text "@{ML_response \"1+2\" \"3\"}"}\\

    68   @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}

    69   \end{tabular}

    70   \end{center}

    71 

    72   which produce respectively

    73 

    74   \begin{center}\small

    75   \begin{tabular}{p{3cm}p{3cm}}

    76   @{ML_response "1+2" "3"} &  

    77   @{ML_response "(1+2,3)" "(3,\<dots>)"}

    78   \end{tabular}

    79   \end{center}

    80   

    81   Note that this antiquotation can only be used when the result can be

    82   constructed: it does not work when the code produces an exception or returns 

    83   an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).

    84 

    85   \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just

    86   like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,

    87   except that the result-specification is not checked. Use this antiquotation

    88   when the result cannot be constructed or the code generates an

    89   exception. Examples are:

    90 

    91   \begin{center}\small

    92   \begin{tabular}{ll}

    93   @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\

    94                                & @{text "\"a + b = c\"}"}\smallskip\\ 

    95   @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ 

    96                                & @{text "\"Exception FAIL raised\"}"}

    97   \end{tabular}

    98   \end{center}

    99 

   100   which produce respectively

   101 

   102   \begin{center}\small

   103   \begin{tabular}{p{7.2cm}}

   104   @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\

   105   @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}

   106   \end{tabular}

   107   \end{center}

   108   

   109   This output mimics to some extend what the user sees when running the

   110   code.

   111 

   112   \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be

   113   used to show erroneous code. Neither the code nor the response will be

   114   checked. An example is:

   115 

   116   \begin{center}\small

   117   \begin{tabular}{ll}

   118   @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\

   119                                     & @{text "\"Type unification failed \<dots>\"}"}

   120   \end{tabular}

   121   \end{center}

   122 

   123   \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when

   124   referring to a file. It checks whether the file exists.  An example

   125   is 

   126 

   127   @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}

   128   \end{itemize}

   129 

   130   The listed antiquotations honour options including @{text "[display]"} and 

   131   @{text "[quotes]"}. For example

   132 

   133   \begin{center}\small

   134   @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}

   135   \end{center}

   136 

   137   whereas

   138   

   139   \begin{center}\small

   140   @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}

   141   \end{center}

   142   

   143   \item Functions and value bindings cannot be defined inside antiquotations; they need

   144   to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}

   145   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 

   146   the tutorial, however, ensures that the environment markers are not printed.

   147 

   148   \item Line numbers can be printed using 

   149   \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}

   150   for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The

   151   tag is \isa{\%linenosgray} when the numbered text should be gray. 

   152 

   153   \end{itemize}

   154 

   155 *}

   156 

   157 

   158 

   159 end