src/Doc/IsarImplementation/ML.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 56399 386e4cb7ad68
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29755
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29646
diff changeset
     1
theory "ML"
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29646
diff changeset
     2
imports Base
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29646
diff changeset
     3
begin
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
     4
39822
0de42180febe basic setup for Chapter 0: Isabelle/ML;
wenzelm
parents: 36164
diff changeset
     5
chapter {* Isabelle/ML *}
20489
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
     6
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
     7
text {* Isabelle/ML is best understood as a certain culture based on
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
     8
  Standard ML.  Thus it is not a new programming language, but a
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
     9
  certain way to use SML at an advanced level within the Isabelle
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    10
  environment.  This covers a variety of aspects that are geared
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    11
  towards an efficient and robust platform for applications of formal
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    12
  logic with fully foundational proof construction --- according to
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    13
  the well-known \emph{LCF principle}.  There is specific
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    14
  infrastructure with library modules to address the needs of this
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    15
  difficult task.  For example, the raw parallel programming model of
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    16
  Poly/ML is presented as considerably more abstract concept of
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    17
  \emph{future values}, which is then used to augment the inference
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    18
  kernel, proof interpreter, and theory loader accordingly.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    19
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    20
  The main aspects of Isabelle/ML are introduced below.  These
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    21
  first-hand explanations should help to understand how proper
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    22
  Isabelle/ML is to be read and written, and to get access to the
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    23
  wealth of experience that is expressed in the source text and its
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    24
  history of changes.\footnote{See
54703
499f92dc6e45 more antiquotations;
wenzelm
parents: 54387
diff changeset
    25
  @{url "http://isabelle.in.tum.de/repos/isabelle"} for the full
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    26
  Mercurial history.  There are symbolic tags to refer to official
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    27
  Isabelle releases, as opposed to arbitrary \emph{tip} versions that
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    28
  merely reflect snapshots that are never really up-to-date.}  *}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    29
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
    30
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    31
section {* Style and orthography *}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    32
39879
wenzelm
parents: 39878
diff changeset
    33
text {* The sources of Isabelle/Isar are optimized for
wenzelm
parents: 39878
diff changeset
    34
  \emph{readability} and \emph{maintainability}.  The main purpose is
wenzelm
parents: 39878
diff changeset
    35
  to tell an informed reader what is really going on and how things
wenzelm
parents: 39878
diff changeset
    36
  really work.  This is a non-trivial aim, but it is supported by a
wenzelm
parents: 39878
diff changeset
    37
  certain style of writing Isabelle/ML that has emerged from long
wenzelm
parents: 39878
diff changeset
    38
  years of system development.\footnote{See also the interesting style
wenzelm
parents: 39878
diff changeset
    39
  guide for OCaml
54703
499f92dc6e45 more antiquotations;
wenzelm
parents: 54387
diff changeset
    40
  @{url "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"}
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    41
  which shares many of our means and ends.}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    42
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    43
  The main principle behind any coding style is \emph{consistency}.
39879
wenzelm
parents: 39878
diff changeset
    44
  For a single author of a small program this merely means ``choose
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    45
  your style and stick to it''.  A complex project like Isabelle, with
39879
wenzelm
parents: 39878
diff changeset
    46
  long years of development and different contributors, requires more
wenzelm
parents: 39878
diff changeset
    47
  standardization.  A coding style that is changed every few years or
wenzelm
parents: 39878
diff changeset
    48
  with every new contributor is no style at all, because consistency
wenzelm
parents: 39878
diff changeset
    49
  is quickly lost.  Global consistency is hard to achieve, though.
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    50
  Nonetheless, one should always strive at least for local consistency
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    51
  of modules and sub-systems, without deviating from some general
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    52
  principles how to write Isabelle/ML.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    53
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    54
  In a sense, good coding style is like an \emph{orthography} for the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    55
  sources: it helps to read quickly over the text and see through the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    56
  main points, without getting distracted by accidental presentation
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    57
  of free-style code.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    58
*}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    59
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    60
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    61
subsection {* Header and sectioning *}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    62
39879
wenzelm
parents: 39878
diff changeset
    63
text {* Isabelle source files have a certain standardized header
wenzelm
parents: 39878
diff changeset
    64
  format (with precise spacing) that follows ancient traditions
wenzelm
parents: 39878
diff changeset
    65
  reaching back to the earliest versions of the system by Larry
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40508
diff changeset
    66
  Paulson.  See @{file "~~/src/Pure/thm.ML"}, for example.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    67
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    68
  The header includes at least @{verbatim Title} and @{verbatim
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    69
  Author} entries, followed by a prose description of the purpose of
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    70
  the module.  The latter can range from a single line to several
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    71
  paragraphs of explanations.
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    72
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    73
  The rest of the file is divided into sections, subsections,
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    74
  subsubsections, paragraphs etc.\ using a simple layout via ML
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    75
  comments as follows.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    76
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    77
\begin{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    78
(*** section ***)
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    79
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    80
(** subsection **)
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    81
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    82
(* subsubsection *)
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    83
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    84
(*short paragraph*)
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    85
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    86
(*
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    87
  long paragraph,
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    88
  with more text
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    89
*)
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    90
\end{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    91
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    92
  As in regular typography, there is some extra space \emph{before}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    93
  section headings that are adjacent to plain text (not other headings
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    94
  as in the example above).
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    95
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
    96
  \medskip The precise wording of the prose text given in these
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
    97
  headings is chosen carefully to introduce the main theme of the
39879
wenzelm
parents: 39878
diff changeset
    98
  subsequent formal ML text.
wenzelm
parents: 39878
diff changeset
    99
*}
wenzelm
parents: 39878
diff changeset
   100
wenzelm
parents: 39878
diff changeset
   101
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   102
subsection {* Naming conventions *}
39879
wenzelm
parents: 39878
diff changeset
   103
wenzelm
parents: 39878
diff changeset
   104
text {* Since ML is the primary medium to express the meaning of the
wenzelm
parents: 39878
diff changeset
   105
  source text, naming of ML entities requires special care.
wenzelm
parents: 39878
diff changeset
   106
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   107
  \paragraph{Notation.}  A name consists of 1--3 \emph{words} (rarely
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   108
  4, but not more) that are separated by underscore.  There are three
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   109
  variants concerning upper or lower case letters, which are used for
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   110
  certain ML categories as follows:
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   111
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   112
  \medskip
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   113
  \begin{tabular}{lll}
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   114
  variant & example & ML categories \\\hline
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   115
  lower-case & @{ML_text foo_bar} & values, types, record fields \\
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   116
  capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   117
  upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   118
  \end{tabular}
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   119
  \medskip
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   120
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   121
  For historical reasons, many capitalized names omit underscores,
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   122
  e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
47180
c14fda8fee38 improving spelling
bulwahn
parents: 46262
diff changeset
   123
  Genuine mixed-case names are \emph{not} used, because clear division
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   124
  of words is essential for readability.\footnote{Camel-case was
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   125
  invented to workaround the lack of underscore in some early
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   126
  non-ASCII character sets.  Later it became habitual in some language
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   127
  communities that are now strong in numbers.}
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   128
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   129
  A single (capital) character does not count as ``word'' in this
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   130
  respect: some Isabelle/ML names are suffixed by extra markers like
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   131
  this: @{ML_text foo_barT}.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   132
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   133
  Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   134
  foo'}, @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   135
  foo''''} or more.  Decimal digits scale better to larger numbers,
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   136
  e.g.\ @{ML_text foo0}, @{ML_text foo1}, @{ML_text foo42}.
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   137
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   138
  \paragraph{Scopes.}  Apart from very basic library modules, ML
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   139
  structures are not ``opened'', but names are referenced with
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   140
  explicit qualification, as in @{ML Syntax.string_of_term} for
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   141
  example.  When devising names for structures and their components it
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   142
  is important aim at eye-catching compositions of both parts, because
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   143
  this is how they are seen in the sources and documentation.  For the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   144
  same reasons, aliases of well-known library functions should be
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   145
  avoided.
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   146
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   147
  Local names of function abstraction or case/let bindings are
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   148
  typically shorter, sometimes using only rudiments of ``words'',
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   149
  while still avoiding cryptic shorthands.  An auxiliary function
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   150
  called @{ML_text helper}, @{ML_text aux}, or @{ML_text f} is
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   151
  considered bad style.
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   152
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   153
  Example:
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   154
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   155
  \begin{verbatim}
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   156
  (* RIGHT *)
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   157
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   158
  fun print_foo ctxt foo =
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   159
    let
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   160
      fun print t = ... Syntax.string_of_term ctxt t ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   161
    in ... end;
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   162
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   163
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   164
  (* RIGHT *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   165
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   166
  fun print_foo ctxt foo =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   167
    let
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   168
      val string_of_term = Syntax.string_of_term ctxt;
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   169
      fun print t = ... string_of_term t ...
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   170
    in ... end;
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   171
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   172
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   173
  (* WRONG *)
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   174
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   175
  val string_of_term = Syntax.string_of_term;
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   176
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   177
  fun print_foo ctxt foo =
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   178
    let
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   179
      fun aux t = ... string_of_term ctxt t ...
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   180
    in ... end;
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   181
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   182
  \end{verbatim}
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   183
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   184
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   185
  \paragraph{Specific conventions.} Here are some specific name forms
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   186
  that occur frequently in the sources.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   187
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   188
  \begin{itemize}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   189
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   190
  \item A function that maps @{ML_text foo} to @{ML_text bar} is
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   191
  called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   192
  @{ML_text foo2bar}, @{ML_text bar_from_foo}, @{ML_text
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   193
  bar_for_foo}, or @{ML_text bar4foo}).
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   194
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   195
  \item The name component @{ML_text legacy} means that the operation
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   196
  is about to be discontinued soon.
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   197
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   198
  \item The name component @{ML_text old} means that this is historic
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   199
  material that might disappear at some later stage.
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   200
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   201
  \item The name component @{ML_text global} means that this works
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   202
  with the background theory instead of the regular local context
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   203
  (\secref{sec:context}), sometimes for historical reasons, sometimes
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   204
  due a genuine lack of locality of the concept involved, sometimes as
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   205
  a fall-back for the lack of a proper context in the application
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   206
  code.  Whenever there is a non-global variant available, the
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   207
  application should be migrated to use it with a proper local
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   208
  context.
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   209
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   210
  \item Variables of the main context types of the Isabelle/Isar
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   211
  framework (\secref{sec:context} and \chref{ch:local-theory}) have
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   212
  firm naming conventions as follows:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   213
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   214
  \begin{itemize}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   215
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   216
  \item theories are called @{ML_text thy}, rarely @{ML_text theory}
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   217
  (never @{ML_text thry})
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   218
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   219
  \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   220
  context} (never @{ML_text ctx})
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   221
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   222
  \item generic contexts are called @{ML_text context}, rarely
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   223
  @{ML_text ctxt}
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   224
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   225
  \item local theories are called @{ML_text lthy}, except for local
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   226
  theories that are treated as proof context (which is a semantic
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   227
  super-type)
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   228
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   229
  \end{itemize}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   230
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   231
  Variations with primed or decimal numbers are always possible, as
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   232
  well as sematic prefixes like @{ML_text foo_thy} or @{ML_text
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   233
  bar_ctxt}, but the base conventions above need to be preserved.
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   234
  This allows to visualize the their data flow via plain regular
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   235
  expressions in the editor.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   236
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   237
  \item The main logical entities (\secref{ch:logic}) have established
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   238
  naming convention as follows:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   239
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   240
  \begin{itemize}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   241
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   242
  \item sorts are called @{ML_text S}
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   243
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   244
  \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   245
  ty} (never @{ML_text t})
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   246
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   247
  \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   248
  tm} (never @{ML_text trm})
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   249
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   250
  \item certified types are called @{ML_text cT}, rarely @{ML_text
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   251
  T}, with variants as for types
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   252
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   253
  \item certified terms are called @{ML_text ct}, rarely @{ML_text
52733
wenzelm
parents: 52421
diff changeset
   254
  t}, with variants as for terms (never @{ML_text ctrm})
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   255
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   256
  \item theorems are called @{ML_text th}, or @{ML_text thm}
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   257
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   258
  \end{itemize}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   259
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   260
  Proper semantic names override these conventions completely.  For
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   261
  example, the left-hand side of an equation (as a term) can be called
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   262
  @{ML_text lhs} (not @{ML_text lhs_tm}).  Or a term that is known
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   263
  to be a variable can be called @{ML_text v} or @{ML_text x}.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   264
40310
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   265
  \item Tactics (\secref{sec:tactics}) are sufficiently important to
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   266
  have specific naming conventions.  The name of a basic tactic
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   267
  definition always has a @{ML_text "_tac"} suffix, the subgoal index
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   268
  (if applicable) is always called @{ML_text i}, and the goal state
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   269
  (if made explicit) is usually called @{ML_text st} instead of the
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   270
  somewhat misleading @{ML_text thm}.  Any other arguments are given
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   271
  before the latter two, and the general context is given first.
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   272
  Example:
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   273
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   274
  \begin{verbatim}
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   275
  fun my_tac ctxt arg1 arg2 i st = ...
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   276
  \end{verbatim}
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   277
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   278
  Note that the goal state @{ML_text st} above is rarely made
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   279
  explicit, if tactic combinators (tacticals) are used as usual.
a0698ec82e6e more on naming tactics;
wenzelm
parents: 40302
diff changeset
   280
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   281
  \end{itemize}
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   282
*}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   283
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   284
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   285
subsection {* General source layout *}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   286
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   287
text {* The general Isabelle/ML source layout imitates regular
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   288
  type-setting to some extent, augmented by the requirements for
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   289
  deeply nested expressions that are commonplace in functional
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   290
  programming.
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   291
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   292
  \paragraph{Line length} is 80 characters according to ancient
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   293
  standards, but we allow as much as 100 characters (not
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   294
  more).\footnote{Readability requires to keep the beginning of a line
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   295
  in view while watching its end.  Modern wide-screen displays do not
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   296
  change the way how the human brain works.  Sources also need to be
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   297
  printable on plain paper with reasonable font-size.} The extra 20
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   298
  characters acknowledge the space requirements due to qualified
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   299
  library references in Isabelle/ML.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   300
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   301
  \paragraph{White-space} is used to emphasize the structure of
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   302
  expressions, following mostly standard conventions for mathematical
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   303
  typesetting, as can be seen in plain {\TeX} or {\LaTeX}.  This
39879
wenzelm
parents: 39878
diff changeset
   304
  defines positioning of spaces for parentheses, punctuation, and
wenzelm
parents: 39878
diff changeset
   305
  infixes as illustrated here:
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   306
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   307
  \begin{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   308
  val x = y + z * (a + b);
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   309
  val pair = (a, b);
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   310
  val record = {foo = 1, bar = 2};
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   311
  \end{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   312
39879
wenzelm
parents: 39878
diff changeset
   313
  Lines are normally broken \emph{after} an infix operator or
wenzelm
parents: 39878
diff changeset
   314
  punctuation character.  For example:
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   315
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   316
  \begin{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   317
  val x =
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   318
    a +
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   319
    b +
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   320
    c;
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   321
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   322
  val tuple =
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   323
   (a,
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   324
    b,
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   325
    c);
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   326
  \end{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   327
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   328
  Some special infixes (e.g.\ @{ML_text "|>"}) work better at the
39879
wenzelm
parents: 39878
diff changeset
   329
  start of the line, but punctuation is always at the end.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   330
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   331
  Function application follows the tradition of @{text "\<lambda>"}-calculus,
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   332
  not informal mathematics.  For example: @{ML_text "f a b"} for a
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   333
  curried function, or @{ML_text "g (a, b)"} for a tupled function.
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   334
  Note that the space between @{ML_text g} and the pair @{ML_text
39879
wenzelm
parents: 39878
diff changeset
   335
  "(a, b)"} follows the important principle of
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   336
  \emph{compositionality}: the layout of @{ML_text "g p"} does not
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   337
  change when @{ML_text "p"} is refined to the concrete pair
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   338
  @{ML_text "(a, b)"}.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   339
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   340
  \paragraph{Indentation} uses plain spaces, never hard
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   341
  tabulators.\footnote{Tabulators were invented to move the carriage
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   342
  of a type-writer to certain predefined positions.  In software they
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   343
  could be used as a primitive run-length compression of consecutive
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   344
  spaces, but the precise result would depend on non-standardized
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   345
  editor configuration.}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   346
39879
wenzelm
parents: 39878
diff changeset
   347
  Each level of nesting is indented by 2 spaces, sometimes 1, very
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   348
  rarely 4, never 8 or any other odd number.
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   349
39879
wenzelm
parents: 39878
diff changeset
   350
  Indentation follows a simple logical format that only depends on the
wenzelm
parents: 39878
diff changeset
   351
  nesting depth, not the accidental length of the text that initiates
wenzelm
parents: 39878
diff changeset
   352
  a level of nesting.  Example:
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   353
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   354
  \begin{verbatim}
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   355
  (* RIGHT *)
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   356
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   357
  if b then
39879
wenzelm
parents: 39878
diff changeset
   358
    expr1_part1
wenzelm
parents: 39878
diff changeset
   359
    expr1_part2
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   360
  else
39879
wenzelm
parents: 39878
diff changeset
   361
    expr2_part1
wenzelm
parents: 39878
diff changeset
   362
    expr2_part2
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   363
39880
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   364
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   365
  (* WRONG *)
7deb6a741626 more on "Naming conventions";
wenzelm
parents: 39879
diff changeset
   366
39879
wenzelm
parents: 39878
diff changeset
   367
  if b then expr1_part1
wenzelm
parents: 39878
diff changeset
   368
            expr1_part2
wenzelm
parents: 39878
diff changeset
   369
  else expr2_part1
wenzelm
parents: 39878
diff changeset
   370
       expr2_part2
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   371
  \end{verbatim}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   372
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   373
  The second form has many problems: it assumes a fixed-width font
39879
wenzelm
parents: 39878
diff changeset
   374
  when viewing the sources, it uses more space on the line and thus
wenzelm
parents: 39878
diff changeset
   375
  makes it hard to observe its strict length limit (working against
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   376
  \emph{readability}), it requires extra editing to adapt the layout
39879
wenzelm
parents: 39878
diff changeset
   377
  to changes of the initial text (working against
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   378
  \emph{maintainability}) etc.
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   379
39879
wenzelm
parents: 39878
diff changeset
   380
  \medskip For similar reasons, any kind of two-dimensional or tabular
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   381
  layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
39879
wenzelm
parents: 39878
diff changeset
   382
  avoided.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   383
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   384
  \paragraph{Complex expressions} that consist of multi-clausal
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   385
  function definitions, @{ML_text handle}, @{ML_text case},
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   386
  @{ML_text let} (and combinations) require special attention.  The
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   387
  syntax of Standard ML is quite ambitious and admits a lot of
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   388
  variance that can distort the meaning of the text.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   389
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   390
  Clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   391
  @{ML_text case} get extra indentation to indicate the nesting
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   392
  clearly.  Example:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   393
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   394
  \begin{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   395
  (* RIGHT *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   396
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   397
  fun foo p1 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   398
        expr1
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   399
    | foo p2 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   400
        expr2
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   401
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   402
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   403
  (* WRONG *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   404
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   405
  fun foo p1 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   406
    expr1
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   407
    | foo p2 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   408
    expr2
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   409
  \end{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   410
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   411
  Body expressions consisting of @{ML_text case} or @{ML_text let}
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   412
  require care to maintain compositionality, to prevent loss of
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   413
  logical indentation where it is especially important to see the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   414
  structure of the text.  Example:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   415
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   416
  \begin{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   417
  (* RIGHT *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   418
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   419
  fun foo p1 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   420
        (case e of
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   421
          q1 => ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   422
        | q2 => ...)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   423
    | foo p2 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   424
        let
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   425
          ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   426
        in
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   427
          ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   428
        end
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   429
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   430
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   431
  (* WRONG *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   432
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   433
  fun foo p1 = case e of
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   434
      q1 => ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   435
    | q2 => ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   436
    | foo p2 =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   437
    let
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   438
      ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   439
    in
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   440
      ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   441
    end
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   442
  \end{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   443
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   444
  Extra parentheses around @{ML_text case} expressions are optional,
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   445
  but help to analyse the nesting based on character matching in the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   446
  editor.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   447
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   448
  \medskip There are two main exceptions to the overall principle of
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   449
  compositionality in the layout of complex expressions.
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   450
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   451
  \begin{enumerate}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   452
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   453
  \item @{ML_text "if"} expressions are iterated as if there would be
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   454
  a multi-branch conditional in SML, e.g.
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   455
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   456
  \begin{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   457
  (* RIGHT *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   458
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   459
  if b1 then e1
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   460
  else if b2 then e2
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   461
  else e3
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   462
  \end{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   463
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   464
  \item @{ML_text fn} abstractions are often layed-out as if they
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   465
  would lack any structure by themselves.  This traditional form is
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   466
  motivated by the possibility to shift function arguments back and
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   467
  forth wrt.\ additional combinators.  Example:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   468
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   469
  \begin{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   470
  (* RIGHT *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   471
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   472
  fun foo x y = fold (fn z =>
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   473
    expr)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   474
  \end{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   475
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   476
  Here the visual appearance is that of three arguments @{ML_text x},
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   477
  @{ML_text y}, @{ML_text z}.
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   478
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   479
  \end{enumerate}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   480
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   481
  Such weakly structured layout should be use with great care.  Here
40153
wenzelm
parents: 40149
diff changeset
   482
  are some counter-examples involving @{ML_text let} expressions:
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   483
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   484
  \begin{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   485
  (* WRONG *)
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   486
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   487
  fun foo x = let
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   488
      val y = ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   489
    in ... end
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   490
41162
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   491
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   492
  (* WRONG *)
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   493
40153
wenzelm
parents: 40149
diff changeset
   494
  fun foo x = let
wenzelm
parents: 40149
diff changeset
   495
    val y = ...
wenzelm
parents: 40149
diff changeset
   496
  in ... end
wenzelm
parents: 40149
diff changeset
   497
41162
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   498
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   499
  (* WRONG *)
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   500
39881
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   501
  fun foo x =
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   502
  let
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   503
    val y = ...
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   504
  in ... end
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   505
  \end{verbatim}
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   506
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   507
  \medskip In general the source layout is meant to emphasize the
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   508
  structure of complex language expressions, not to pretend that SML
40aee0b95ddf more on "Style and orthography";
wenzelm
parents: 39880
diff changeset
   509
  had a completely different syntax (say that of Haskell or Java).
39878
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   510
*}
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   511
31dd361a3060 more on "Style and orthography";
wenzelm
parents: 39875
diff changeset
   512
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   513
section {* SML embedded into Isabelle/Isar *}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   514
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   515
text {* ML and Isar are intertwined via an open-ended bootstrap
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   516
  process that provides more and more programming facilities and
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   517
  logical content in an alternating manner.  Bootstrapping starts from
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   518
  the raw environment of existing implementations of Standard ML
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   519
  (mainly Poly/ML, but also SML/NJ).
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   520
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   521
  Isabelle/Pure marks the point where the original ML toplevel is
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   522
  superseded by the Isar toplevel that maintains a uniform context for
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   523
  arbitrary ML values (see also \secref{sec:context}).  This formal
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   524
  environment holds ML compiler bindings, logical entities, and many
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   525
  other things.  Raw SML is never encountered again after the initial
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   526
  bootstrap of Isabelle/Pure.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   527
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   528
  Object-logics like Isabelle/HOL are built within the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   529
  Isabelle/ML/Isar environment by introducing suitable theories with
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   530
  associated ML modules, either inlined or as separate files.  Thus
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   531
  Isabelle/HOL is defined as a regular user-space application within
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   532
  the Isabelle framework.  Further add-on tools can be implemented in
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   533
  ML within the Isar context in the same manner: ML is part of the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   534
  standard repertoire of Isabelle, and there is no distinction between
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   535
  ``user'' and ``developer'' in this respect.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   536
*}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   537
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   538
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   539
subsection {* Isar ML commands *}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   540
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   541
text {* The primary Isar source language provides facilities to ``open
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   542
  a window'' to the underlying ML compiler.  Especially see the Isar
51295
71fc3776c453 discontinued redundant 'use' command;
wenzelm
parents: 51058
diff changeset
   543
  commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   544
  same way, only the source text is provided via a file vs.\ inlined,
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   545
  respectively.  Apart from embedding ML into the main theory
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   546
  definition like that, there are many more commands that refer to ML
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   547
  source, such as @{command_ref setup} or @{command_ref declaration}.
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   548
  Even more fine-grained embedding of ML into Isar is encountered in
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   549
  the proof method @{method_ref tactic}, which refines the pending
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   550
  goal state via a given expression of type @{ML_type tactic}.
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   551
*}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   552
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   553
text %mlex {* The following artificial example demonstrates some ML
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   554
  toplevel declarations within the implicit Isar theory context.  This
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   555
  is regular functional programming without referring to logical
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   556
  entities yet.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   557
*}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   558
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   559
ML {*
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   560
  fun factorial 0 = 1
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   561
    | factorial n = n * factorial (n - 1)
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   562
*}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   563
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   564
text {* Here the ML environment is already managed by Isabelle, i.e.\
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   565
  the @{ML factorial} function is not yet accessible in the preceding
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   566
  paragraph, nor in a different theory that is independent from the
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   567
  current one in the import hierarchy.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   568
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   569
  Removing the above ML declaration from the source text will remove
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   570
  any trace of this definition as expected.  The Isabelle/ML toplevel
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   571
  environment is managed in a \emph{stateless} way: unlike the raw ML
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   572
  toplevel there are no global side-effects involved
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   573
  here.\footnote{Such a stateless compilation environment is also a
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   574
  prerequisite for robust parallel compilation within independent
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   575
  nodes of the implicit theory development graph.}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   576
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   577
  \medskip The next example shows how to embed ML into Isar proofs, using
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   578
 @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}.
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   579
  As illustrated below, the effect on the ML environment is local to
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   580
  the whole proof body, ignoring the block structure.
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   581
*}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   582
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   583
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   584
begin
39851
7219a771ab63 more examples;
wenzelm
parents: 39850
diff changeset
   585
  ML_prf %"ML" {* val a = 1 *}
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   586
  {
39851
7219a771ab63 more examples;
wenzelm
parents: 39850
diff changeset
   587
    ML_prf %"ML" {* val b = a + 1 *}
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   588
  } -- {* Isar block structure ignored by ML environment *}
39851
7219a771ab63 more examples;
wenzelm
parents: 39850
diff changeset
   589
  ML_prf %"ML" {* val c = b + 1 *}
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   590
end
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   591
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   592
text {* By side-stepping the normal scoping rules for Isar proof
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   593
  blocks, embedded ML code can refer to the different contexts and
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   594
  manipulate corresponding entities, e.g.\ export a fact from a block
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   595
  context.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   596
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   597
  \medskip Two further ML commands are useful in certain situations:
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   598
  @{command_ref ML_val} and @{command_ref ML_command} are
39824
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   599
  \emph{diagnostic} in the sense that there is no effect on the
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   600
  underlying environment, and can thus used anywhere (even outside a
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   601
  theory).  The examples below produce long strings of digits by
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   602
  invoking @{ML factorial}: @{command ML_val} already takes care of
679075565542 misc tuning;
wenzelm
parents: 39823
diff changeset
   603
  printing the ML toplevel result, but @{command ML_command} is silent
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   604
  so we produce an explicit output message.  *}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   605
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   606
ML_val {* factorial 100 *}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   607
ML_command {* writeln (string_of_int (factorial 100)) *}
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   608
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   609
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   610
begin
52417
wenzelm
parents: 52416
diff changeset
   611
  ML_val {* factorial 100 *}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   612
  ML_command {* writeln (string_of_int (factorial 100)) *}
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40800
diff changeset
   613
end
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   614
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   615
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   616
subsection {* Compile-time context *}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   617
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   618
text {* Whenever the ML compiler is invoked within Isabelle/Isar, the
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   619
  formal context is passed as a thread-local reference variable.  Thus
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   620
  ML code may access the theory context during compilation, by reading
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   621
  or writing the (local) theory under construction.  Note that such
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   622
  direct access to the compile-time context is rare.  In practice it
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   623
  is typically done via some derived ML functions instead.
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   624
*}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   625
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   626
text %mlref {*
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   627
  \begin{mldecls}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   628
  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   629
  @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 55838
diff changeset
   630
  @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 55838
diff changeset
   631
  @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   632
  \end{mldecls}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   633
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   634
  \begin{description}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   635
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   636
  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   637
  context of the ML toplevel --- at compile time.  ML code needs to
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   638
  take care to refer to @{ML "ML_Context.the_generic_context ()"}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   639
  correctly.  Recall that evaluation of a function body is delayed
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   640
  until actual run-time.
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   641
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   642
  \item @{ML "Context.>>"}~@{text f} applies context transformation
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   643
  @{text f} to the implicit context of the ML toplevel.
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   644
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 55838
diff changeset
   645
  \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
39850
f4c614ece7ed moved bind_thm(s) to implementation manual;
wenzelm
parents: 39835
diff changeset
   646
  theorems produced in ML both in the (global) theory context and the
f4c614ece7ed moved bind_thm(s) to implementation manual;
wenzelm
parents: 39835
diff changeset
   647
  ML toplevel, associating it with the provided name.  Theorems are
f4c614ece7ed moved bind_thm(s) to implementation manual;
wenzelm
parents: 39835
diff changeset
   648
  put into a global ``standard'' format before being stored.
f4c614ece7ed moved bind_thm(s) to implementation manual;
wenzelm
parents: 39835
diff changeset
   649
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 55838
diff changeset
   650
  \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   651
  singleton fact.
39850
f4c614ece7ed moved bind_thm(s) to implementation manual;
wenzelm
parents: 39835
diff changeset
   652
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   653
  \end{description}
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   654
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   655
  It is important to note that the above functions are really
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   656
  restricted to the compile time, even though the ML compiler is
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   657
  invoked at run-time.  The majority of ML code either uses static
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   658
  antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   659
  proof context at run-time, by explicit functional abstraction.
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 39824
diff changeset
   660
*}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   661
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   662
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   663
subsection {* Antiquotations \label{sec:ML-antiq} *}
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   664
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   665
text {* A very important consequence of embedding SML into Isar is the
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   666
  concept of \emph{ML antiquotation}.  The standard token language of
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   667
  ML is augmented by special syntactic entities of the following form:
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   668
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54703
diff changeset
   669
  @{rail \<open>
53167
4e7ddd76e632 discontinued unused antiquotation blocks;
wenzelm
parents: 53163
diff changeset
   670
  @{syntax_def antiquote}: '@{' nameref args '}'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54703
diff changeset
   671
  \<close>}
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   672
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
   673
  Here @{syntax nameref} and @{syntax args} are regular outer syntax
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   674
  categories \cite{isabelle-isar-ref}.  Attributes and proof methods
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   675
  use similar syntax.
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   676
39827
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   677
  \medskip A regular antiquotation @{text "@{name args}"} processes
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   678
  its arguments by the usual means of the Isar source language, and
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   679
  produces corresponding ML source text, either as literal
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   680
  \emph{inline} text (e.g. @{text "@{term t}"}) or abstract
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   681
  \emph{value} (e.g. @{text "@{thm th}"}).  This pre-compilation
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   682
  scheme allows to refer to formal entities in a robust manner, with
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   683
  proper static scoping and with some degree of logical checking of
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   684
  small portions of the code.
d829ce302ca4 basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents: 39825
diff changeset
   685
*}
39823
61e7935a6858 more on Isabelle/ML;
wenzelm
parents: 39822
diff changeset
   686
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   687
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   688
subsection {* Printing ML values *}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   689
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   690
text {* The ML compiler knows about the structure of values according
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   691
  to their static type, and can print them in the manner of the
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   692
  toplevel loop, although the details are non-portable.  The
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   693
  antiquotations @{ML_antiquotation_def "make_string"} and
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   694
  @{ML_antiquotation_def "print"} provide a quasi-portable way to
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   695
  refer to this potential capability of the underlying ML system in
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   696
  generic Isabelle/ML sources.
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   697
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   698
  This is occasionally useful for diagnostic or demonstration
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   699
  purposes.  Note that production-quality tools require proper
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   700
  user-level error messages. *}
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   701
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   702
text %mlantiq {*
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   703
  \begin{matharray}{rcl}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   704
  @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   705
  @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   706
  \end{matharray}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   707
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54703
diff changeset
   708
  @{rail \<open>
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   709
  @@{ML_antiquotation make_string}
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   710
  ;
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   711
  @@{ML_antiquotation print} @{syntax name}?
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 54703
diff changeset
   712
  \<close>}
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   713
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   714
  \begin{description}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   715
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   716
  \item @{text "@{make_string}"} inlines a function to print arbitrary
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   717
  values similar to the ML toplevel.  The result is compiler dependent
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   718
  and may fall back on "?" in certain situations.
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   719
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   720
  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   721
  unit"} to output the result of @{text "@{make_string}"} above,
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   722
  together with the source position of the antiquotation.  The default
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   723
  output function is @{ML writeln}.
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   724
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   725
  \end{description}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   726
*}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   727
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   728
text %mlex {* The following artificial examples show how to produce
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   729
  adhoc output of ML values for debugging purposes. *}
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   730
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   731
ML {*
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   732
  val x = 42;
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   733
  val y = true;
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   734
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   735
  writeln (@{make_string} {x = x, y = y});
56399
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   736
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   737
  @{print} {x = x, y = y};
386e4cb7ad68 added ML antiquotation @{print};
wenzelm
parents: 56303
diff changeset
   738
  @{print tracing} {x = x, y = y};
51636
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   739
*}
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   740
e49bf0be79ba document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
wenzelm
parents: 51295
diff changeset
   741
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   742
section {* Canonical argument order \label{sec:canonical-argument-order} *}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   743
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   744
text {* Standard ML is a language in the tradition of @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   745
  "\<lambda>"}-calculus and \emph{higher-order functional programming},
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   746
  similar to OCaml, Haskell, or Isabelle/Pure and HOL as logical
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   747
  languages.  Getting acquainted with the native style of representing
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   748
  functions in that setting can save a lot of extra boiler-plate of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   749
  redundant shuffling of arguments, auxiliary abstractions etc.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   750
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   751
  Functions are usually \emph{curried}: the idea of turning arguments
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   752
  of type @{text "\<tau>\<^sub>i"} (for @{text "i \<in> {1, \<dots> n}"}) into a result of
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   753
  type @{text "\<tau>"} is represented by the iterated function space
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   754
  @{text "\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>"}.  This is isomorphic to the well-known
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   755
  encoding via tuples @{text "\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>"}, but the curried
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   756
  version fits more smoothly into the basic calculus.\footnote{The
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   757
  difference is even more significant in higher-order logic, because
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   758
  the redundant tuple structure needs to be accommodated by formal
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   759
  reasoning.}
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   760
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   761
  Currying gives some flexiblity due to \emph{partial application}.  A
53071
wenzelm
parents: 52733
diff changeset
   762
  function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   763
  and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   764
  etc.  How well this works in practice depends on the order of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   765
  arguments.  In the worst case, arguments are arranged erratically,
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   766
  and using a function in a certain situation always requires some
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   767
  glue code.  Thus we would get exponentially many oppurtunities to
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   768
  decorate the code with meaningless permutations of arguments.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   769
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   770
  This can be avoided by \emph{canonical argument order}, which
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   771
  observes certain standard patterns and minimizes adhoc permutations
40229
wenzelm
parents: 40153
diff changeset
   772
  in their application.  In Isabelle/ML, large portions of text can be
52416
wenzelm
parents: 51636
diff changeset
   773
  written without auxiliary operations like @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times>
wenzelm
parents: 51636
diff changeset
   774
  \<alpha>"} or @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} (the latter not
wenzelm
parents: 51636
diff changeset
   775
  present in the Isabelle/ML library).
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   776
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   777
  \medskip The basic idea is that arguments that vary less are moved
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   778
  further to the left than those that vary more.  Two particularly
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   779
  important categories of functions are \emph{selectors} and
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   780
  \emph{updates}.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   781
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   782
  The subsequent scheme is based on a hypothetical set-like container
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   783
  of type @{text "\<beta>"} that manages elements of type @{text "\<alpha>"}.  Both
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   784
  the names and types of the associated operations are canonical for
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   785
  Isabelle/ML.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   786
52416
wenzelm
parents: 51636
diff changeset
   787
  \begin{center}
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   788
  \begin{tabular}{ll}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   789
  kind & canonical name and type \\\hline
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   790
  selector & @{text "member: \<beta> \<rightarrow> \<alpha> \<rightarrow> bool"} \\
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   791
  update & @{text "insert: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} \\
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   792
  \end{tabular}
52416
wenzelm
parents: 51636
diff changeset
   793
  \end{center}
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   794
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   795
  Given a container @{text "B: \<beta>"}, the partially applied @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   796
  "member B"} is a predicate over elements @{text "\<alpha> \<rightarrow> bool"}, and
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   797
  thus represents the intended denotation directly.  It is customary
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   798
  to pass the abstract predicate to further operations, not the
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   799
  concrete container.  The argument order makes it easy to use other
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   800
  combinators: @{text "forall (member B) list"} will check a list of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   801
  elements for membership in @{text "B"} etc. Often the explicit
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   802
  @{text "list"} is pointless and can be contracted to @{text "forall
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   803
  (member B)"} to get directly a predicate again.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   804
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   805
  In contrast, an update operation varies the container, so it moves
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   806
  to the right: @{text "insert a"} is a function @{text "\<beta> \<rightarrow> \<beta>"} to
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   807
  insert a value @{text "a"}.  These can be composed naturally as
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   808
  @{text "insert c \<circ> insert b \<circ> insert a"}.  The slightly awkward
40229
wenzelm
parents: 40153
diff changeset
   809
  inversion of the composition order is due to conventional
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   810
  mathematical notation, which can be easily amended as explained
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   811
  below.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   812
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   813
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   814
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   815
subsection {* Forward application and composition *}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   816
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   817
text {* Regular function application and infix notation works best for
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   818
  relatively deeply structured expressions, e.g.\ @{text "h (f x y + g
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   819
  z)"}.  The important special case of \emph{linear transformation}
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   820
  applies a cascade of functions @{text "f\<^sub>n (\<dots> (f\<^sub>1 x))"}.  This
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   821
  becomes hard to read and maintain if the functions are themselves
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   822
  given as complex expressions.  The notation can be significantly
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   823
  improved by introducing \emph{forward} versions of application and
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   824
  composition as follows:
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   825
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   826
  \medskip
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   827
  \begin{tabular}{lll}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   828
  @{text "x |> f"} & @{text "\<equiv>"} & @{text "f x"} \\
41162
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   829
  @{text "(f #> g) x"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   830
  \end{tabular}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   831
  \medskip
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   832
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   833
  This enables to write conveniently @{text "x |> f\<^sub>1 |> \<dots> |> f\<^sub>n"} or
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   834
  @{text "f\<^sub>1 #> \<dots> #> f\<^sub>n"} for its functional abstraction over @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   835
  "x"}.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   836
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   837
  \medskip There is an additional set of combinators to accommodate
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   838
  multiple results (via pairs) that are passed on as multiple
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   839
  arguments (via currying).
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   840
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   841
  \medskip
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   842
  \begin{tabular}{lll}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   843
  @{text "(x, y) |-> f"} & @{text "\<equiv>"} & @{text "f x y"} \\
41162
2181c47a02fe more correct ML snippets that are unchecked;
wenzelm
parents: 40964
diff changeset
   844
  @{text "(f #-> g) x"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   845
  \end{tabular}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   846
  \medskip
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   847
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   848
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   849
text %mlref {*
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   850
  \begin{mldecls}
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 42665
diff changeset
   851
  @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 42665
diff changeset
   852
  @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 42665
diff changeset
   853
  @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 42665
diff changeset
   854
  @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   855
  \end{mldecls}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   856
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   857
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   858
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   859
subsection {* Canonical iteration *}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   860
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   861
text {* As explained above, a function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   862
  understood as update on a configuration of type @{text "\<beta>"},
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   863
  parametrized by arguments of type @{text "\<alpha>"}.  Given @{text "a: \<alpha>"}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   864
  the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   865
  homogeneously on @{text "\<beta>"}.  This can be iterated naturally over a
53071
wenzelm
parents: 52733
diff changeset
   866
  list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f a\<^sub>n"}.
wenzelm
parents: 52733
diff changeset
   867
  The latter expression is again a function @{text "\<beta> \<rightarrow> \<beta>"}.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   868
  It can be applied to an initial configuration @{text "b: \<beta>"} to
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   869
  start the iteration over the given list of arguments: each @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   870
  "a"} in @{text "a\<^sub>1, \<dots>, a\<^sub>n"} is applied consecutively by updating a
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   871
  cumulative configuration.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   872
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   873
  The @{text fold} combinator in Isabelle/ML lifts a function @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   874
  "f"} as above to its iterated version over a list of arguments.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   875
  Lifting can be repeated, e.g.\ @{text "(fold \<circ> fold) f"} iterates
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   876
  over a list of lists as expected.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   877
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   878
  The variant @{text "fold_rev"} works inside-out over the list of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   879
  arguments, such that @{text "fold_rev f \<equiv> fold f \<circ> rev"} holds.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   880
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   881
  The @{text "fold_map"} combinator essentially performs @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   882
  "fold"} and @{text "map"} simultaneously: each application of @{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   883
  "f"} produces an updated configuration together with a side-result;
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   884
  the iteration collects all such side-results as a separate list.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   885
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   886
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   887
text %mlref {*
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   888
  \begin{mldecls}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   889
  @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   890
  @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   891
  @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   892
  \end{mldecls}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   893
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   894
  \begin{description}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   895
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   896
  \item @{ML fold}~@{text f} lifts the parametrized update function
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   897
  @{text "f"} to a list of parameters.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   898
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   899
  \item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   900
  "f"}, but works inside-out.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   901
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   902
  \item @{ML fold_map}~@{text "f"} lifts the parametrized update
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   903
  function @{text "f"} (with side-result) to a list of parameters and
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   904
  cumulative side-results.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   905
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   906
  \end{description}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   907
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   908
  \begin{warn}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   909
  The literature on functional programming provides a multitude of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   910
  combinators called @{text "foldl"}, @{text "foldr"} etc.  SML97
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   911
  provides its own variations as @{ML List.foldl} and @{ML
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   912
  List.foldr}, while the classic Isabelle library also has the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   913
  historic @{ML Library.foldl} and @{ML Library.foldr}.  To avoid
52416
wenzelm
parents: 51636
diff changeset
   914
  unnecessary complication and confusion, all these historical
wenzelm
parents: 51636
diff changeset
   915
  versions should be ignored, and @{ML fold} (or @{ML fold_rev}) used
wenzelm
parents: 51636
diff changeset
   916
  exclusively.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   917
  \end{warn}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   918
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   919
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   920
text %mlex {* The following example shows how to fill a text buffer
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   921
  incrementally by adding strings, either individually or from a given
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   922
  list.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   923
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   924
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   925
ML {*
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   926
  val s =
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   927
    Buffer.empty
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   928
    |> Buffer.add "digits: "
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   929
    |> fold (Buffer.add o string_of_int) (0 upto 9)
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   930
    |> Buffer.content;
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   931
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   932
  @{assert} (s = "digits: 0123456789");
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   933
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   934
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   935
text {* Note how @{ML "fold (Buffer.add o string_of_int)"} above saves
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   936
  an extra @{ML "map"} over the given list.  This kind of peephole
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   937
  optimization reduces both the code size and the tree structures in
52416
wenzelm
parents: 51636
diff changeset
   938
  memory (``deforestation''), but it requires some practice to read
wenzelm
parents: 51636
diff changeset
   939
  and write fluently.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   940
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   941
  \medskip The next example elaborates the idea of canonical
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   942
  iteration, demonstrating fast accumulation of tree content using a
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   943
  text buffer.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   944
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   945
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   946
ML {*
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   947
  datatype tree = Text of string | Elem of string * tree list;
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   948
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   949
  fun slow_content (Text txt) = txt
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   950
    | slow_content (Elem (name, ts)) =
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   951
        "<" ^ name ^ ">" ^
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   952
        implode (map slow_content ts) ^
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   953
        "</" ^ name ^ ">"
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   954
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   955
  fun add_content (Text txt) = Buffer.add txt
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   956
    | add_content (Elem (name, ts)) =
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   957
        Buffer.add ("<" ^ name ^ ">") #>
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   958
        fold add_content ts #>
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   959
        Buffer.add ("</" ^ name ^ ">");
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   960
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   961
  fun fast_content tree =
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   962
    Buffer.empty |> add_content tree |> Buffer.content;
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   963
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   964
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   965
text {* The slow part of @{ML slow_content} is the @{ML implode} of
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   966
  the recursive results, because it copies previously produced strings
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   967
  again.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   968
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   969
  The incremental @{ML add_content} avoids this by operating on a
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
   970
  buffer that is passed through in a linear fashion.  Using @{ML_text
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   971
  "#>"} and contraction over the actual buffer argument saves some
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   972
  additional boiler-plate.  Of course, the two @{ML "Buffer.add"}
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   973
  invocations with concatenated strings could have been split into
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   974
  smaller parts, but this would have obfuscated the source without
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   975
  making a big difference in allocations.  Here we have done some
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   976
  peephole-optimization for the sake of readability.
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   977
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   978
  Another benefit of @{ML add_content} is its ``open'' form as a
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   979
  function on buffers that can be continued in further linear
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   980
  transformations, folding etc.  Thus it is more compositional than
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   981
  the naive @{ML slow_content}.  As realistic example, compare the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   982
  old-style @{ML "Term.maxidx_of_term: term -> int"} with the newer
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   983
  @{ML "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   984
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   985
  Note that @{ML fast_content} above is only defined as example.  In
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   986
  many practical situations, it is customary to provide the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   987
  incremental @{ML add_content} only and leave the initialization and
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
   988
  termination to the concrete application by the user.
39883
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   989
*}
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   990
3d3d6038bdaa more on "Canonical argument order";
wenzelm
parents: 39881
diff changeset
   991
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
   992
section {* Message output channels \label{sec:message-channels} *}
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   993
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   994
text {* Isabelle provides output channels for different kinds of
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   995
  messages: regular output, high-volume tracing information, warnings,
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   996
  and errors.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   997
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   998
  Depending on the user interface involved, these messages may appear
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
   999
  in different text styles or colours.  The standard output for
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1000
  terminal sessions prefixes each line of warnings by @{verbatim
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1001
  "###"} and errors by @{verbatim "***"}, but leaves anything else
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1002
  unchanged.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1003
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1004
  Messages are associated with the transaction context of the running
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1005
  Isar command.  This enables the front-end to manage commands and
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1006
  resulting messages together.  For example, after deleting a command
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1007
  from a given theory document version, the corresponding message
39872
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1008
  output can be retracted from the display.
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1009
*}
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1010
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1011
text %mlref {*
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1012
  \begin{mldecls}
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1013
  @{index_ML writeln: "string -> unit"} \\
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1014
  @{index_ML tracing: "string -> unit"} \\
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1015
  @{index_ML warning: "string -> unit"} \\
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1016
  @{index_ML error: "string -> 'a"} \\
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1017
  \end{mldecls}
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1018
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1019
  \begin{description}
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1020
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1021
  \item @{ML writeln}~@{text "text"} outputs @{text "text"} as regular
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1022
  message.  This is the primary message output operation of Isabelle
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1023
  and should be used by default.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1024
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1025
  \item @{ML tracing}~@{text "text"} outputs @{text "text"} as special
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1026
  tracing message, indicating potential high-volume output to the
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1027
  front-end (hundreds or thousands of messages issued by a single
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1028
  command).  The idea is to allow the user-interface to downgrade the
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1029
  quality of message display to achieve higher throughput.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1030
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1031
  Note that the user might have to take special actions to see tracing
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1032
  output, e.g.\ switch to a different output window.  So this channel
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1033
  should not be used for regular output.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1034
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1035
  \item @{ML warning}~@{text "text"} outputs @{text "text"} as
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1036
  warning, which typically means some extra emphasis on the front-end
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1037
  side (color highlighting, icons, etc.).
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1038
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1039
  \item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1040
  "text"} and thus lets the Isar toplevel print @{text "text"} on the
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1041
  error channel, which typically means some extra emphasis on the
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1042
  front-end side (color highlighting, icons, etc.).
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1043
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1044
  This assumes that the exception is not handled before the command
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1045
  terminates.  Handling exception @{ML ERROR}~@{text "text"} is a
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1046
  perfectly legal alternative: it means that the error is absorbed
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1047
  without any message output.
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1048
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1049
  \begin{warn}
54387
890e983cb07b tuned signature;
wenzelm
parents: 53982
diff changeset
  1050
  The actual error channel is accessed via @{ML Output.error_message}, but
51058
98c48d023136 some updates concerning Proof General;
wenzelm
parents: 48985
diff changeset
  1051
  the old interaction protocol of Proof~General \emph{crashes} if that
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1052
  function is used in regular ML code: error output and toplevel
52416
wenzelm
parents: 51636
diff changeset
  1053
  command failure always need to coincide in classic TTY interaction.
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1054
  \end{warn}
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1055
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1056
  \end{description}
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1057
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1058
  \begin{warn}
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1059
  Regular Isabelle/ML code should output messages exclusively by the
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1060
  official channels.  Using raw I/O on \emph{stdout} or \emph{stderr}
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1061
  instead (e.g.\ via @{ML TextIO.output}) is apt to cause problems in
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1062
  the presence of parallel and asynchronous processing of Isabelle
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1063
  theories.  Such raw output might be displayed by the front-end in
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1064
  some system console log, with a low chance that the user will ever
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1065
  see it.  Moreover, as a genuine side-effect on global process
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1066
  channels, there is no proper way to retract output when Isar command
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1067
  transactions are reset by the system.
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39859
diff changeset
  1068
  \end{warn}
39872
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1069
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1070
  \begin{warn}
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1071
  The message channels should be used in a message-oriented manner.
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1072
  This means that multi-line output that logically belongs together is
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1073
  issued by a \emph{single} invocation of @{ML writeln} etc.\ with the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1074
  functional concatenation of all message constituents.
39872
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1075
  \end{warn}
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1076
*}
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1077
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1078
text %mlex {* The following example demonstrates a multi-line
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1079
  warning.  Note that in some situations the user sees only the first
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1080
  line, so the most important point should be made first.
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1081
*}
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1082
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1083
ML_command {*
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1084
  warning (cat_lines
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1085
   ["Beware the Jabberwock, my son!",
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1086
    "The jaws that bite, the claws that catch!",
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1087
    "Beware the Jubjub Bird, and shun",
2b88d00d6790 more on messages;
wenzelm
parents: 39871
diff changeset
  1088
    "The frumious Bandersnatch!"]);
39835
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1089
*}
6cefd96bb71d modernized version of "Message output channels";
wenzelm
parents: 39830
diff changeset
  1090
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1091
39867
a8363532cd4d somewhat modernized version of "Thread-safe programming";
wenzelm
parents: 39866
diff changeset
  1092
section {* Exceptions \label{sec:exceptions} *}
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1093
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1094
text {* The Standard ML semantics of strict functional evaluation
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1095
  together with exceptions is rather well defined, but some delicate
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1096
  points need to be observed to avoid that ML programs go wrong
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1097
  despite static type-checking.  Exceptions in Isabelle/ML are
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1098
  subsequently categorized as follows.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1099
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1100
  \paragraph{Regular user errors.}  These are meant to provide
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1101
  informative feedback about malformed input etc.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1102
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1103
  The \emph{error} function raises the corresponding \emph{ERROR}
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1104
  exception, with a plain text message as argument.  \emph{ERROR}
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1105
  exceptions can be handled internally, in order to be ignored, turned
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1106
  into other exceptions, or cascaded by appending messages.  If the
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1107
  corresponding Isabelle/Isar command terminates with an \emph{ERROR}
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1108
  exception state, the toplevel will print the result on the error
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1109
  channel (see \secref{sec:message-channels}).
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1110
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1111
  It is considered bad style to refer to internal function names or
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1112
  values in ML source notation in user error messages.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1113
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1114
  Grammatical correctness of error messages can be improved by
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1115
  \emph{omitting} final punctuation: messages are often concatenated
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1116
  or put into a larger context (e.g.\ augmented with source position).
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1117
  By not insisting in the final word at the origin of the error, the
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1118
  system can perform its administrative tasks more easily and
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1119
  robustly.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1120
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1121
  \paragraph{Program failures.}  There is a handful of standard
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1122
  exceptions that indicate general failure situations, or failures of
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1123
  core operations on logical entities (types, terms, theorems,
39856
wenzelm
parents: 39855
diff changeset
  1124
  theories, see \chref{ch:logic}).
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1125
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1126
  These exceptions indicate a genuine breakdown of the program, so the
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1127
  main purpose is to determine quickly what has happened where.
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1128
  Traditionally, the (short) exception message would include the name
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1129
  of an ML function, although this is no longer necessary, because the
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1130
  ML runtime system prints a detailed source position of the
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
  1131
  corresponding @{ML_text raise} keyword.
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1132
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1133
  \medskip User modules can always introduce their own custom
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1134
  exceptions locally, e.g.\ to organize internal failures robustly
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1135
  without overlapping with existing exceptions.  Exceptions that are
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1136
  exposed in module signatures require extra care, though, and should
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1137
  \emph{not} be introduced by default.  Surprise by users of a module
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1138
  can be often minimized by using plain user errors instead.
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1139
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1140
  \paragraph{Interrupts.}  These indicate arbitrary system events:
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1141
  both the ML runtime system and the Isabelle/ML infrastructure signal
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1142
  various exceptional situations by raising the special
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1143
  \emph{Interrupt} exception in user code.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1144
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1145
  This is the one and only way that physical events can intrude an
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1146
  Isabelle/ML program.  Such an interrupt can mean out-of-memory,
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1147
  stack overflow, timeout, internal signaling of threads, or the user
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1148
  producing a console interrupt manually etc.  An Isabelle/ML program
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1149
  that intercepts interrupts becomes dependent on physical effects of
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1150
  the environment.  Even worse, exception handling patterns that are
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1151
  too general by accident, e.g.\ by mispelled exception constructors,
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1152
  will cover interrupts unintentionally and thus render the program
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1153
  semantics ill-defined.
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1154
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1155
  Note that the Interrupt exception dates back to the original SML90
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1156
  language definition.  It was excluded from the SML97 version to
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1157
  avoid its malign impact on ML program semantics, but without
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1158
  providing a viable alternative.  Isabelle/ML recovers physical
40229
wenzelm
parents: 40153
diff changeset
  1159
  interruptibility (which is an indispensable tool to implement
wenzelm
parents: 40153
diff changeset
  1160
  managed evaluation of command transactions), but requires user code
wenzelm
parents: 40153
diff changeset
  1161
  to be strictly transparent wrt.\ interrupts.
39854
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1162
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1163
  \begin{warn}
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1164
  Isabelle/ML user code needs to terminate promptly on interruption,
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1165
  without guessing at its meaning to the system infrastructure.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1166
  Temporary handling of interrupts for cleanup of global resources
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1167
  etc.\ needs to be followed immediately by re-raising of the original
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1168
  exception.
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1169
  \end{warn}
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1170
*}
7480a7a159cb more on "Exceptions";
wenzelm
parents: 39851
diff changeset
  1171
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1172
text %mlref {*
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1173
  \begin{mldecls}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1174
  @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1175
  @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
55838
e120a15b0ee6 more antiquotations;
wenzelm
parents: 55837
diff changeset
  1176
  @{index_ML_exception ERROR: string} \\
e120a15b0ee6 more antiquotations;
wenzelm
parents: 55837
diff changeset
  1177
  @{index_ML_exception Fail: string} \\
39856
wenzelm
parents: 39855
diff changeset
  1178
  @{index_ML Exn.is_interrupt: "exn -> bool"} \\
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1179
  @{index_ML reraise: "exn -> 'a"} \\
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56199
diff changeset
  1180
  @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1181
  \end{mldecls}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1182
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1183
  \begin{description}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1184
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1185
  \item @{ML try}~@{text "f x"} makes the partiality of evaluating
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1186
  @{text "f x"} explicit via the option datatype.  Interrupts are
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1187
  \emph{not} handled here, i.e.\ this form serves as safe replacement
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
  1188
  for the \emph{unsafe} version @{ML_text "(SOME"}~@{text "f
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
  1189
  x"}~@{ML_text "handle _ => NONE)"} that is occasionally seen in
52417
wenzelm
parents: 52416
diff changeset
  1190
  books about SML97, not Isabelle/ML.
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1191
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1192
  \item @{ML can} is similar to @{ML try} with more abstract result.
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1193
39856
wenzelm
parents: 39855
diff changeset
  1194
  \item @{ML ERROR}~@{text "msg"} represents user errors; this
40126
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1195
  exception is normally raised indirectly via the @{ML error} function
916cb4a28ffd misc tuning;
wenzelm
parents: 40110
diff changeset
  1196
  (see \secref{sec:message-channels}).
39856
wenzelm
parents: 39855
diff changeset
  1197
wenzelm
parents: 39855
diff changeset
  1198
  \item @{ML Fail}~@{text "msg"} represents general program failures.
wenzelm
parents: 39855
diff changeset
  1199
wenzelm
parents: 39855
diff changeset
  1200
  \item @{ML Exn.is_interrupt} identifies interrupts robustly, without
wenzelm
parents: 39855
diff changeset
  1201
  mentioning concrete exception constructors in user code.  Handled
wenzelm
parents: 39855
diff changeset
  1202
  interrupts need to be re-raised promptly!
wenzelm
parents: 39855
diff changeset
  1203
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1204
  \item @{ML reraise}~@{text "exn"} raises exception @{text "exn"}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1205
  while preserving its implicit position information (if possible,
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1206
  depending on the ML platform).
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1207
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56199
diff changeset
  1208
  \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 40126
diff changeset
  1209
  "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1210
  a full trace of its stack of nested exceptions (if possible,
53739
599d8c324477 repaired latex (cf. 84522727f9d3);
wenzelm
parents: 53709
diff changeset
  1211
  depending on the ML platform).
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1212
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 56199
diff changeset
  1213
  Inserting @{ML Runtime.exn_trace} into ML code temporarily is
53709
84522727f9d3 improved printing of exception trace in Poly/ML 5.5.1;
wenzelm
parents: 53167
diff changeset
  1214
  useful for debugging, but not suitable for production code.
39855
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1215
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1216
  \end{description}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1217
*}
d4299b415879 more on "Exceptions";
wenzelm
parents: 39854
diff changeset
  1218
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1219
text %mlantiq {*
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1220
  \begin{matharray}{rcl}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1221
  @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1222
  \end{matharray}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1223
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1224
  \begin{description}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1225
40110
93e7935d4cb5 added ML antiquotation @{assert};
wenzelm
parents: 39883
diff changeset
  1226
  \item @{text "@{assert}"} inlines a function
93e7935d4cb5 added ML antiquotation @{assert};
wenzelm
parents: 39883
diff changeset
  1227
  @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is
93e7935d4cb5 added ML antiquotation @{assert};
wenzelm
parents: 39883
diff changeset
  1228
  @{ML false}.  Due to inlining the source position of failed
93e7935d4cb5 added ML antiquotation @{assert};
wenzelm
parents: 39883
diff changeset
  1229
  assertions is included in the error output.
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1230
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1231
  \end{description}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1232
*}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39864
diff changeset
  1233