src/Doc/Implementation/ML.thy
author wenzelm
Fri Aug 05 16:30:53 2016 +0200 (2016-08-05)
changeset 63610 4b40b8196dc7
parent 63215 c7de5b311909
child 63680 6e1e8b5abbfa
permissions -rw-r--r--
Sidekick parser for isabelle-ml and sml mode;
     1 (*:maxLineLen=78:*)
     2 
     3 theory "ML"
     4 imports Base
     5 begin
     6 
     7 chapter \<open>Isabelle/ML\<close>
     8 
     9 text \<open>
    10   Isabelle/ML is best understood as a certain culture based on Standard ML.
    11   Thus it is not a new programming language, but a certain way to use SML at
    12   an advanced level within the Isabelle environment. This covers a variety of
    13   aspects that are geared towards an efficient and robust platform for
    14   applications of formal logic with fully foundational proof construction ---
    15   according to the well-known \<^emph>\<open>LCF principle\<close>. There is specific
    16   infrastructure with library modules to address the needs of this difficult
    17   task. For example, the raw parallel programming model of Poly/ML is
    18   presented as considerably more abstract concept of \<^emph>\<open>futures\<close>, which is then
    19   used to augment the inference kernel, Isar theory and proof interpreter, and
    20   PIDE document management.
    21 
    22   The main aspects of Isabelle/ML are introduced below. These first-hand
    23   explanations should help to understand how proper Isabelle/ML is to be read
    24   and written, and to get access to the wealth of experience that is expressed
    25   in the source text and its history of changes.\<^footnote>\<open>See @{url
    26   "http://isabelle.in.tum.de/repos/isabelle"} for the full Mercurial history.
    27   There are symbolic tags to refer to official Isabelle releases, as opposed
    28   to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
    29   really up-to-date.\<close>
    30 \<close>
    31 
    32 
    33 section \<open>Style and orthography\<close>
    34 
    35 text \<open>
    36   The sources of Isabelle/Isar are optimized for \<^emph>\<open>readability\<close> and
    37   \<^emph>\<open>maintainability\<close>. The main purpose is to tell an informed reader what is
    38   really going on and how things really work. This is a non-trivial aim, but
    39   it is supported by a certain style of writing Isabelle/ML that has emerged
    40   from long years of system development.\<^footnote>\<open>See also the interesting style guide
    41   for OCaml @{url
    42   "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"} which shares
    43   many of our means and ends.\<close>
    44 
    45   The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
    46   author of a small program this merely means ``choose your style and stick to
    47   it''. A complex project like Isabelle, with long years of development and
    48   different contributors, requires more standardization. A coding style that
    49   is changed every few years or with every new contributor is no style at all,
    50   because consistency is quickly lost. Global consistency is hard to achieve,
    51   though. Nonetheless, one should always strive at least for local consistency
    52   of modules and sub-systems, without deviating from some general principles
    53   how to write Isabelle/ML.
    54 
    55   In a sense, good coding style is like an \<^emph>\<open>orthography\<close> for the sources: it
    56   helps to read quickly over the text and see through the main points, without
    57   getting distracted by accidental presentation of free-style code.
    58 \<close>
    59 
    60 
    61 subsection \<open>Header and sectioning\<close>
    62 
    63 text \<open>
    64   Isabelle source files have a certain standardized header format (with
    65   precise spacing) that follows ancient traditions reaching back to the
    66   earliest versions of the system by Larry Paulson. See @{file
    67   "~~/src/Pure/thm.ML"}, for example.
    68 
    69   The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a
    70   prose description of the purpose of the module. The latter can range from a
    71   single line to several paragraphs of explanations.
    72 
    73   The rest of the file is divided into chapters, sections, subsections,
    74   subsubsections, paragraphs etc.\ using a simple layout via ML comments as
    75   follows.
    76 
    77   @{verbatim [display]
    78 \<open>  (**** chapter ****)
    79  
    80   (*** section ***)
    81 
    82   (** subsection **)
    83 
    84   (* subsubsection *)
    85 
    86   (*short paragraph*)
    87 
    88   (*
    89     long paragraph,
    90     with more text
    91   *)\<close>}
    92 
    93   As in regular typography, there is some extra space \<^emph>\<open>before\<close> section
    94   headings that are adjacent to plain text, but not other headings as in the
    95   example above.
    96 
    97   \<^medskip>
    98   The precise wording of the prose text given in these headings is chosen
    99   carefully to introduce the main theme of the subsequent formal ML text.
   100 \<close>
   101 
   102 
   103 subsection \<open>Naming conventions\<close>
   104 
   105 text \<open>
   106   Since ML is the primary medium to express the meaning of the source text,
   107   naming of ML entities requires special care.
   108 \<close>
   109 
   110 paragraph \<open>Notation.\<close>
   111 text \<open>
   112   A name consists of 1--3 \<^emph>\<open>words\<close> (rarely 4, but not more) that are separated
   113   by underscore. There are three variants concerning upper or lower case
   114   letters, which are used for certain ML categories as follows:
   115 
   116   \<^medskip>
   117   \begin{tabular}{lll}
   118   variant & example & ML categories \\\hline
   119   lower-case & @{ML_text foo_bar} & values, types, record fields \\
   120   capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
   121   upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
   122   \end{tabular}
   123   \<^medskip>
   124 
   125   For historical reasons, many capitalized names omit underscores, e.g.\
   126   old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}. Genuine
   127   mixed-case names are \<^emph>\<open>not\<close> used, because clear division of words is
   128   essential for readability.\<^footnote>\<open>Camel-case was invented to workaround the lack
   129   of underscore in some early non-ASCII character sets. Later it became
   130   habitual in some language communities that are now strong in numbers.\<close>
   131 
   132   A single (capital) character does not count as ``word'' in this respect:
   133   some Isabelle/ML names are suffixed by extra markers like this: @{ML_text
   134   foo_barT}.
   135 
   136   Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text foo'},
   137   @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text foo''''} or more.
   138   Decimal digits scale better to larger numbers, e.g.\ @{ML_text foo0},
   139   @{ML_text foo1}, @{ML_text foo42}.
   140 \<close>
   141 
   142 paragraph\<open>Scopes.\<close>
   143 text \<open>
   144   Apart from very basic library modules, ML structures are not ``opened'', but
   145   names are referenced with explicit qualification, as in @{ML
   146   Syntax.string_of_term} for example. When devising names for structures and
   147   their components it is important to aim at eye-catching compositions of both
   148   parts, because this is how they are seen in the sources and documentation.
   149   For the same reasons, aliases of well-known library functions should be
   150   avoided.
   151 
   152   Local names of function abstraction or case/let bindings are typically
   153   shorter, sometimes using only rudiments of ``words'', while still avoiding
   154   cryptic shorthands. An auxiliary function called @{ML_text helper},
   155   @{ML_text aux}, or @{ML_text f} is considered bad style.
   156 
   157   Example:
   158 
   159   @{verbatim [display]
   160 \<open>  (* RIGHT *)
   161 
   162   fun print_foo ctxt foo =
   163     let
   164       fun print t = ... Syntax.string_of_term ctxt t ...
   165     in ... end;
   166 
   167 
   168   (* RIGHT *)
   169 
   170   fun print_foo ctxt foo =
   171     let
   172       val string_of_term = Syntax.string_of_term ctxt;
   173       fun print t = ... string_of_term t ...
   174     in ... end;
   175 
   176 
   177   (* WRONG *)
   178 
   179   val string_of_term = Syntax.string_of_term;
   180 
   181   fun print_foo ctxt foo =
   182     let
   183       fun aux t = ... string_of_term ctxt t ...
   184     in ... end;\<close>}
   185 \<close>
   186 
   187 paragraph \<open>Specific conventions.\<close>
   188 text \<open>
   189   Here are some specific name forms that occur frequently in the sources.
   190 
   191   \<^item> A function that maps @{ML_text foo} to @{ML_text bar} is called @{ML_text
   192   foo_to_bar} or @{ML_text bar_of_foo} (never @{ML_text foo2bar}, nor
   193   @{ML_text bar_from_foo}, nor @{ML_text bar_for_foo}, nor @{ML_text
   194   bar4foo}).
   195 
   196   \<^item> The name component @{ML_text legacy} means that the operation is about to
   197   be discontinued soon.
   198 
   199   \<^item> The name component @{ML_text global} means that this works with the
   200   background theory instead of the regular local context
   201   (\secref{sec:context}), sometimes for historical reasons, sometimes due a
   202   genuine lack of locality of the concept involved, sometimes as a fall-back
   203   for the lack of a proper context in the application code. Whenever there is
   204   a non-global variant available, the application should be migrated to use it
   205   with a proper local context.
   206 
   207   \<^item> Variables of the main context types of the Isabelle/Isar framework
   208   (\secref{sec:context} and \chref{ch:local-theory}) have firm naming
   209   conventions as follows:
   210 
   211     \<^item> theories are called @{ML_text thy}, rarely @{ML_text theory}
   212     (never @{ML_text thry})
   213 
   214     \<^item> proof contexts are called @{ML_text ctxt}, rarely @{ML_text
   215     context} (never @{ML_text ctx})
   216 
   217     \<^item> generic contexts are called @{ML_text context}
   218 
   219     \<^item> local theories are called @{ML_text lthy}, except for local
   220     theories that are treated as proof context (which is a semantic
   221     super-type)
   222 
   223   Variations with primed or decimal numbers are always possible, as well as
   224   semantic prefixes like @{ML_text foo_thy} or @{ML_text bar_ctxt}, but the
   225   base conventions above need to be preserved. This allows to emphasize their
   226   data flow via plain regular expressions in the text editor.
   227 
   228   \<^item> The main logical entities (\secref{ch:logic}) have established naming
   229   convention as follows:
   230 
   231     \<^item> sorts are called @{ML_text S}
   232 
   233     \<^item> types are called @{ML_text T}, @{ML_text U}, or @{ML_text ty} (never
   234     @{ML_text t})
   235 
   236     \<^item> terms are called @{ML_text t}, @{ML_text u}, or @{ML_text tm} (never
   237     @{ML_text trm})
   238 
   239     \<^item> certified types are called @{ML_text cT}, rarely @{ML_text T}, with
   240     variants as for types
   241 
   242     \<^item> certified terms are called @{ML_text ct}, rarely @{ML_text t}, with
   243     variants as for terms (never @{ML_text ctrm})
   244 
   245     \<^item> theorems are called @{ML_text th}, or @{ML_text thm}
   246 
   247   Proper semantic names override these conventions completely. For example,
   248   the left-hand side of an equation (as a term) can be called @{ML_text lhs}
   249   (not @{ML_text lhs_tm}). Or a term that is known to be a variable can be
   250   called @{ML_text v} or @{ML_text x}.
   251 
   252   \<^item> Tactics (\secref{sec:tactics}) are sufficiently important to have specific
   253   naming conventions. The name of a basic tactic definition always has a
   254   @{ML_text "_tac"} suffix, the subgoal index (if applicable) is always called
   255   @{ML_text i}, and the goal state (if made explicit) is usually called
   256   @{ML_text st} instead of the somewhat misleading @{ML_text thm}. Any other
   257   arguments are given before the latter two, and the general context is given
   258   first. Example:
   259 
   260   @{verbatim [display] \<open>  fun my_tac ctxt arg1 arg2 i st = ...\<close>}
   261 
   262   Note that the goal state @{ML_text st} above is rarely made explicit, if
   263   tactic combinators (tacticals) are used as usual.
   264 
   265   A tactic that requires a proof context needs to make that explicit as seen
   266   in the \<^verbatim>\<open>ctxt\<close> argument above. Do not refer to the background theory of
   267   \<^verbatim>\<open>st\<close> -- it is not a proper context, but merely a formal certificate.
   268 \<close>
   269 
   270 
   271 subsection \<open>General source layout\<close>
   272 
   273 text \<open>
   274   The general Isabelle/ML source layout imitates regular type-setting
   275   conventions, augmented by the requirements for deeply nested expressions
   276   that are commonplace in functional programming.
   277 \<close>
   278 
   279 paragraph \<open>Line length\<close>
   280 text \<open>
   281   is limited to 80 characters according to ancient standards, but we allow as
   282   much as 100 characters (not more).\<^footnote>\<open>Readability requires to keep the
   283   beginning of a line in view while watching its end. Modern wide-screen
   284   displays do not change the way how the human brain works. Sources also need
   285   to be printable on plain paper with reasonable font-size.\<close> The extra 20
   286   characters acknowledge the space requirements due to qualified library
   287   references in Isabelle/ML.
   288 \<close>
   289 
   290 paragraph \<open>White-space\<close>
   291 text \<open>
   292   is used to emphasize the structure of expressions, following mostly standard
   293   conventions for mathematical typesetting, as can be seen in plain {\TeX} or
   294   {\LaTeX}. This defines positioning of spaces for parentheses, punctuation,
   295   and infixes as illustrated here:
   296 
   297   @{verbatim [display]
   298 \<open>  val x = y + z * (a + b);
   299   val pair = (a, b);
   300   val record = {foo = 1, bar = 2};\<close>}
   301 
   302   Lines are normally broken \<^emph>\<open>after\<close> an infix operator or punctuation
   303   character. For example:
   304 
   305   @{verbatim [display]
   306 \<open>
   307   val x =
   308     a +
   309     b +
   310     c;
   311 
   312   val tuple =
   313    (a,
   314     b,
   315     c);
   316 \<close>}
   317 
   318   Some special infixes (e.g.\ @{ML_text "|>"}) work better at the start of the
   319   line, but punctuation is always at the end.
   320 
   321   Function application follows the tradition of \<open>\<lambda>\<close>-calculus, not informal
   322   mathematics. For example: @{ML_text "f a b"} for a curried function, or
   323   @{ML_text "g (a, b)"} for a tupled function. Note that the space between
   324   @{ML_text g} and the pair @{ML_text "(a, b)"} follows the important
   325   principle of \<^emph>\<open>compositionality\<close>: the layout of @{ML_text "g p"} does not
   326   change when @{ML_text "p"} is refined to the concrete pair @{ML_text "(a,
   327   b)"}.
   328 \<close>
   329 
   330 paragraph \<open>Indentation\<close>
   331 text \<open>
   332   uses plain spaces, never hard tabulators.\<^footnote>\<open>Tabulators were invented to move
   333   the carriage of a type-writer to certain predefined positions. In software
   334   they could be used as a primitive run-length compression of consecutive
   335   spaces, but the precise result would depend on non-standardized text editor
   336   configuration.\<close>
   337 
   338   Each level of nesting is indented by 2 spaces, sometimes 1, very rarely 4,
   339   never 8 or any other odd number.
   340 
   341   Indentation follows a simple logical format that only depends on the nesting
   342   depth, not the accidental length of the text that initiates a level of
   343   nesting. Example:
   344 
   345   @{verbatim [display]
   346 \<open>  (* RIGHT *)
   347 
   348   if b then
   349     expr1_part1
   350     expr1_part2
   351   else
   352     expr2_part1
   353     expr2_part2
   354 
   355 
   356   (* WRONG *)
   357 
   358   if b then expr1_part1
   359             expr1_part2
   360   else expr2_part1
   361        expr2_part2\<close>}
   362 
   363   The second form has many problems: it assumes a fixed-width font when
   364   viewing the sources, it uses more space on the line and thus makes it hard
   365   to observe its strict length limit (working against \<^emph>\<open>readability\<close>), it
   366   requires extra editing to adapt the layout to changes of the initial text
   367   (working against \<^emph>\<open>maintainability\<close>) etc.
   368 
   369   \<^medskip>
   370   For similar reasons, any kind of two-dimensional or tabular layouts,
   371   ASCII-art with lines or boxes of asterisks etc.\ should be avoided.
   372 \<close>
   373 
   374 paragraph \<open>Complex expressions\<close>
   375 text \<open>
   376   that consist of multi-clausal function definitions, @{ML_text handle},
   377   @{ML_text case}, @{ML_text let} (and combinations) require special
   378   attention. The syntax of Standard ML is quite ambitious and admits a lot of
   379   variance that can distort the meaning of the text.
   380 
   381   Multiple clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
   382   @{ML_text case} get extra indentation to indicate the nesting clearly.
   383   Example:
   384 
   385   @{verbatim [display]
   386 \<open>  (* RIGHT *)
   387 
   388   fun foo p1 =
   389         expr1
   390     | foo p2 =
   391         expr2
   392 
   393 
   394   (* WRONG *)
   395 
   396   fun foo p1 =
   397     expr1
   398     | foo p2 =
   399     expr2\<close>}
   400 
   401   Body expressions consisting of @{ML_text case} or @{ML_text let} require
   402   care to maintain compositionality, to prevent loss of logical indentation
   403   where it is especially important to see the structure of the text. Example:
   404 
   405   @{verbatim [display]
   406 \<open>  (* RIGHT *)
   407 
   408   fun foo p1 =
   409         (case e of
   410           q1 => ...
   411         | q2 => ...)
   412     | foo p2 =
   413         let
   414           ...
   415         in
   416           ...
   417         end
   418 
   419 
   420   (* WRONG *)
   421 
   422   fun foo p1 = case e of
   423       q1 => ...
   424     | q2 => ...
   425     | foo p2 =
   426     let
   427       ...
   428     in
   429       ...
   430     end\<close>}
   431 
   432   Extra parentheses around @{ML_text case} expressions are optional, but help
   433   to analyse the nesting based on character matching in the text editor.
   434 
   435   \<^medskip>
   436   There are two main exceptions to the overall principle of compositionality
   437   in the layout of complex expressions.
   438 
   439   \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch
   440   conditionals, e.g.
   441 
   442   @{verbatim [display]
   443 \<open>  (* RIGHT *)
   444 
   445   if b1 then e1
   446   else if b2 then e2
   447   else e3\<close>}
   448 
   449   \<^enum> @{ML_text fn} abstractions are often layed-out as if they would lack any
   450   structure by themselves. This traditional form is motivated by the
   451   possibility to shift function arguments back and forth wrt.\ additional
   452   combinators. Example:
   453 
   454   @{verbatim [display]
   455 \<open>  (* RIGHT *)
   456 
   457   fun foo x y = fold (fn z =>
   458     expr)\<close>}
   459 
   460   Here the visual appearance is that of three arguments @{ML_text x},
   461   @{ML_text y}, @{ML_text z} in a row.
   462 
   463 
   464   Such weakly structured layout should be use with great care. Here are some
   465   counter-examples involving @{ML_text let} expressions:
   466 
   467   @{verbatim [display]
   468 \<open>  (* WRONG *)
   469 
   470   fun foo x = let
   471       val y = ...
   472     in ... end
   473 
   474 
   475   (* WRONG *)
   476 
   477   fun foo x = let
   478     val y = ...
   479   in ... end
   480 
   481 
   482   (* WRONG *)
   483 
   484   fun foo x =
   485   let
   486     val y = ...
   487   in ... end
   488 
   489 
   490   (* WRONG *)
   491 
   492   fun foo x =
   493     let
   494       val y = ...
   495     in
   496       ... end\<close>}
   497 
   498   \<^medskip>
   499   In general the source layout is meant to emphasize the structure of complex
   500   language expressions, not to pretend that SML had a completely different
   501   syntax (say that of Haskell, Scala, Java).
   502 \<close>
   503 
   504 
   505 section \<open>ML embedded into Isabelle/Isar\<close>
   506 
   507 text \<open>
   508   ML and Isar are intertwined via an open-ended bootstrap process that
   509   provides more and more programming facilities and logical content in an
   510   alternating manner. Bootstrapping starts from the raw environment of
   511   existing implementations of Standard ML (mainly Poly/ML).
   512 
   513   Isabelle/Pure marks the point where the raw ML toplevel is superseded by
   514   Isabelle/ML within the Isar theory and proof language, with a uniform
   515   context for arbitrary ML values (see also \secref{sec:context}). This formal
   516   environment holds ML compiler bindings, logical entities, and many other
   517   things.
   518 
   519   Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar
   520   environment by introducing suitable theories with associated ML modules,
   521   either inlined within \<^verbatim>\<open>.thy\<close> files, or as separate \<^verbatim>\<open>.ML\<close> files that are
   522   loading from some theory. Thus Isabelle/HOL is defined as a regular
   523   user-space application within the Isabelle framework. Further add-on tools
   524   can be implemented in ML within the Isar context in the same manner: ML is
   525   part of the standard repertoire of Isabelle, and there is no distinction
   526   between ``users'' and ``developers'' in this respect.
   527 \<close>
   528 
   529 
   530 subsection \<open>Isar ML commands\<close>
   531 
   532 text \<open>
   533   The primary Isar source language provides facilities to ``open a window'' to
   534   the underlying ML compiler. Especially see the Isar commands @{command_ref
   535   "ML_file"} and @{command_ref "ML"}: both work the same way, but the source
   536   text is provided differently, via a file vs.\ inlined, respectively. Apart
   537   from embedding ML into the main theory definition like that, there are many
   538   more commands that refer to ML source, such as @{command_ref setup} or
   539   @{command_ref declaration}. Even more fine-grained embedding of ML into Isar
   540   is encountered in the proof method @{method_ref tactic}, which refines the
   541   pending goal state via a given expression of type @{ML_type tactic}.
   542 \<close>
   543 
   544 text %mlex \<open>
   545   The following artificial example demonstrates some ML toplevel declarations
   546   within the implicit Isar theory context. This is regular functional
   547   programming without referring to logical entities yet.
   548 \<close>
   549 
   550 ML \<open>
   551   fun factorial 0 = 1
   552     | factorial n = n * factorial (n - 1)
   553 \<close>
   554 
   555 text \<open>
   556   Here the ML environment is already managed by Isabelle, i.e.\ the @{ML
   557   factorial} function is not yet accessible in the preceding paragraph, nor in
   558   a different theory that is independent from the current one in the import
   559   hierarchy.
   560 
   561   Removing the above ML declaration from the source text will remove any trace
   562   of this definition, as expected. The Isabelle/ML toplevel environment is
   563   managed in a \<^emph>\<open>stateless\<close> way: in contrast to the raw ML toplevel, there are
   564   no global side-effects involved here.\<^footnote>\<open>Such a stateless compilation
   565   environment is also a prerequisite for robust parallel compilation within
   566   independent nodes of the implicit theory development graph.\<close>
   567 
   568   \<^medskip>
   569   The next example shows how to embed ML into Isar proofs, using @{command_ref
   570   "ML_prf"} instead of @{command_ref "ML"}. As illustrated below, the effect
   571   on the ML environment is local to the whole proof body, but ignoring the
   572   block structure.
   573 \<close>
   574 
   575 notepad
   576 begin
   577   ML_prf %"ML" \<open>val a = 1\<close>
   578   {
   579     ML_prf %"ML" \<open>val b = a + 1\<close>
   580   } \<comment> \<open>Isar block structure ignored by ML environment\<close>
   581   ML_prf %"ML" \<open>val c = b + 1\<close>
   582 end
   583 
   584 text \<open>
   585   By side-stepping the normal scoping rules for Isar proof blocks, embedded ML
   586   code can refer to the different contexts and manipulate corresponding
   587   entities, e.g.\ export a fact from a block context.
   588 
   589   \<^medskip>
   590   Two further ML commands are useful in certain situations: @{command_ref
   591   ML_val} and @{command_ref ML_command} are \<^emph>\<open>diagnostic\<close> in the sense that
   592   there is no effect on the underlying environment, and can thus be used
   593   anywhere. The examples below produce long strings of digits by invoking @{ML
   594   factorial}: @{command ML_val} takes care of printing the ML toplevel result,
   595   but @{command ML_command} is silent so we produce an explicit output
   596   message.
   597 \<close>
   598 
   599 ML_val \<open>factorial 100\<close>
   600 ML_command \<open>writeln (string_of_int (factorial 100))\<close>
   601 
   602 notepad
   603 begin
   604   ML_val \<open>factorial 100\<close>
   605   ML_command \<open>writeln (string_of_int (factorial 100))\<close>
   606 end
   607 
   608 
   609 subsection \<open>Compile-time context\<close>
   610 
   611 text \<open>
   612   Whenever the ML compiler is invoked within Isabelle/Isar, the formal context
   613   is passed as a thread-local reference variable. Thus ML code may access the
   614   theory context during compilation, by reading or writing the (local) theory
   615   under construction. Note that such direct access to the compile-time context
   616   is rare. In practice it is typically done via some derived ML functions
   617   instead.
   618 \<close>
   619 
   620 text %mlref \<open>
   621   \begin{mldecls}
   622   @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\
   623   @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
   624   @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
   625   @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   626   \end{mldecls}
   627 
   628     \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of
   629     the ML toplevel --- at compile time. ML code needs to take care to refer to
   630     @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation
   631     of a function body is delayed until actual run-time.
   632 
   633     \<^descr> @{ML "Context.>>"}~\<open>f\<close> applies context transformation \<open>f\<close> to the implicit
   634     context of the ML toplevel.
   635 
   636     \<^descr> @{ML ML_Thms.bind_thms}~\<open>(name, thms)\<close> stores a list of theorems produced
   637     in ML both in the (global) theory context and the ML toplevel, associating
   638     it with the provided name.
   639 
   640     \<^descr> @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to
   641     a singleton fact.
   642 
   643   It is important to note that the above functions are really restricted to
   644   the compile time, even though the ML compiler is invoked at run-time. The
   645   majority of ML code either uses static antiquotations
   646   (\secref{sec:ML-antiq}) or refers to the theory or proof context at
   647   run-time, by explicit functional abstraction.
   648 \<close>
   649 
   650 
   651 subsection \<open>Antiquotations \label{sec:ML-antiq}\<close>
   652 
   653 text \<open>
   654   A very important consequence of embedding ML into Isar is the concept of
   655   \<^emph>\<open>ML antiquotation\<close>. The standard token language of ML is augmented by
   656   special syntactic entities of the following form:
   657 
   658   @{rail \<open>
   659   @{syntax_def antiquote}: '@{' name args '}'
   660   \<close>}
   661 
   662   Here @{syntax name} and @{syntax args} are outer syntax categories, as
   663   defined in @{cite "isabelle-isar-ref"}.
   664 
   665   \<^medskip>
   666   A regular antiquotation \<open>@{name args}\<close> processes its arguments by the usual
   667   means of the Isar source language, and produces corresponding ML source
   668   text, either as literal \<^emph>\<open>inline\<close> text (e.g.\ \<open>@{term t}\<close>) or abstract
   669   \<^emph>\<open>value\<close> (e.g. \<open>@{thm th}\<close>). This pre-compilation scheme allows to refer to
   670   formal entities in a robust manner, with proper static scoping and with some
   671   degree of logical checking of small portions of the code.
   672 \<close>
   673 
   674 
   675 subsection \<open>Printing ML values\<close>
   676 
   677 text \<open>
   678   The ML compiler knows about the structure of values according to their
   679   static type, and can print them in the manner of its toplevel, although the
   680   details are non-portable. The antiquotations @{ML_antiquotation_def
   681   "make_string"} and @{ML_antiquotation_def "print"} provide a quasi-portable
   682   way to refer to this potential capability of the underlying ML system in
   683   generic Isabelle/ML sources.
   684 
   685   This is occasionally useful for diagnostic or demonstration purposes. Note
   686   that production-quality tools require proper user-level error messages,
   687   avoiding raw ML values in the output.
   688 \<close>
   689 
   690 text %mlantiq \<open>
   691   \begin{matharray}{rcl}
   692   @{ML_antiquotation_def "make_string"} & : & \<open>ML_antiquotation\<close> \\
   693   @{ML_antiquotation_def "print"} & : & \<open>ML_antiquotation\<close> \\
   694   \end{matharray}
   695 
   696   @{rail \<open>
   697   @@{ML_antiquotation make_string}
   698   ;
   699   @@{ML_antiquotation print} @{syntax name}?
   700   \<close>}
   701 
   702   \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to
   703   the ML toplevel. The result is compiler dependent and may fall back on "?"
   704   in certain situations. The value of configuration option @{attribute_ref
   705   ML_print_depth} determines further details of output.
   706 
   707   \<^descr> \<open>@{print f}\<close> uses the ML function \<open>f: string -> unit\<close> to output the result
   708   of \<open>@{make_string}\<close> above, together with the source position of the
   709   antiquotation. The default output function is @{ML writeln}.
   710 \<close>
   711 
   712 text %mlex \<open>
   713   The following artificial examples show how to produce adhoc output of ML
   714   values for debugging purposes.
   715 \<close>
   716 
   717 ML_val \<open>
   718   val x = 42;
   719   val y = true;
   720 
   721   writeln (@{make_string} {x = x, y = y});
   722 
   723   @{print} {x = x, y = y};
   724   @{print tracing} {x = x, y = y};
   725 \<close>
   726 
   727 
   728 section \<open>Canonical argument order \label{sec:canonical-argument-order}\<close>
   729 
   730 text \<open>
   731   Standard ML is a language in the tradition of \<open>\<lambda>\<close>-calculus and
   732   \<^emph>\<open>higher-order functional programming\<close>, similar to OCaml, Haskell, or
   733   Isabelle/Pure and HOL as logical languages. Getting acquainted with the
   734   native style of representing functions in that setting can save a lot of
   735   extra boiler-plate of redundant shuffling of arguments, auxiliary
   736   abstractions etc.
   737 
   738   Functions are usually \<^emph>\<open>curried\<close>: the idea of turning arguments of type
   739   \<open>\<tau>\<^sub>i\<close> (for \<open>i \<in> {1, \<dots> n}\<close>) into a result of type \<open>\<tau>\<close> is represented by the
   740   iterated function space \<open>\<tau>\<^sub>1 \<rightarrow> \<dots> \<rightarrow> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>. This is isomorphic to the
   741   well-known encoding via tuples \<open>\<tau>\<^sub>1 \<times> \<dots> \<times> \<tau>\<^sub>n \<rightarrow> \<tau>\<close>, but the curried version
   742   fits more smoothly into the basic calculus.\<^footnote>\<open>The difference is even more
   743   significant in HOL, because the redundant tuple structure needs to be
   744   accommodated extraneous proof steps.\<close>
   745 
   746   Currying gives some flexibility due to \<^emph>\<open>partial application\<close>. A function
   747   \<open>f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>\<close> can be applied to \<open>x: \<tau>\<^sub>1\<close> and the remaining \<open>(f x): \<tau>\<^sub>2
   748   \<rightarrow> \<tau>\<close> passed to another function etc. How well this works in practice depends
   749   on the order of arguments. In the worst case, arguments are arranged
   750   erratically, and using a function in a certain situation always requires
   751   some glue code. Thus we would get exponentially many opportunities to
   752   decorate the code with meaningless permutations of arguments.
   753 
   754   This can be avoided by \<^emph>\<open>canonical argument order\<close>, which observes certain
   755   standard patterns and minimizes adhoc permutations in their application. In
   756   Isabelle/ML, large portions of text can be written without auxiliary
   757   operations like \<open>swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>\<close> or \<open>C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)\<close> (the
   758   latter is not present in the Isabelle/ML library).
   759 
   760   \<^medskip>
   761   The main idea is that arguments that vary less are moved further to the left
   762   than those that vary more. Two particularly important categories of
   763   functions are \<^emph>\<open>selectors\<close> and \<^emph>\<open>updates\<close>.
   764 
   765   The subsequent scheme is based on a hypothetical set-like container of type
   766   \<open>\<beta>\<close> that manages elements of type \<open>\<alpha>\<close>. Both the names and types of the
   767   associated operations are canonical for Isabelle/ML.
   768 
   769   \begin{center}
   770   \begin{tabular}{ll}
   771   kind & canonical name and type \\\hline
   772   selector & \<open>member: \<beta> \<rightarrow> \<alpha> \<rightarrow> bool\<close> \\
   773   update & \<open>insert: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> \\
   774   \end{tabular}
   775   \end{center}
   776 
   777   Given a container \<open>B: \<beta>\<close>, the partially applied \<open>member B\<close> is a predicate
   778   over elements \<open>\<alpha> \<rightarrow> bool\<close>, and thus represents the intended denotation
   779   directly. It is customary to pass the abstract predicate to further
   780   operations, not the concrete container. The argument order makes it easy to
   781   use other combinators: \<open>forall (member B) list\<close> will check a list of
   782   elements for membership in \<open>B\<close> etc. Often the explicit \<open>list\<close> is pointless
   783   and can be contracted to \<open>forall (member B)\<close> to get directly a predicate
   784   again.
   785 
   786   In contrast, an update operation varies the container, so it moves to the
   787   right: \<open>insert a\<close> is a function \<open>\<beta> \<rightarrow> \<beta>\<close> to insert a value \<open>a\<close>. These can be
   788   composed naturally as \<open>insert c \<circ> insert b \<circ> insert a\<close>. The slightly awkward
   789   inversion of the composition order is due to conventional mathematical
   790   notation, which can be easily amended as explained below.
   791 \<close>
   792 
   793 
   794 subsection \<open>Forward application and composition\<close>
   795 
   796 text \<open>
   797   Regular function application and infix notation works best for relatively
   798   deeply structured expressions, e.g.\ \<open>h (f x y + g z)\<close>. The important
   799   special case of \<^emph>\<open>linear transformation\<close> applies a cascade of functions \<open>f\<^sub>n
   800   (\<dots> (f\<^sub>1 x))\<close>. This becomes hard to read and maintain if the functions are
   801   themselves given as complex expressions. The notation can be significantly
   802   improved by introducing \<^emph>\<open>forward\<close> versions of application and composition
   803   as follows:
   804 
   805   \<^medskip>
   806   \begin{tabular}{lll}
   807   \<open>x |> f\<close> & \<open>\<equiv>\<close> & \<open>f x\<close> \\
   808   \<open>(f #> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |> g\<close> \\
   809   \end{tabular}
   810   \<^medskip>
   811 
   812   This enables to write conveniently \<open>x |> f\<^sub>1 |> \<dots> |> f\<^sub>n\<close> or \<open>f\<^sub>1 #> \<dots> #>
   813   f\<^sub>n\<close> for its functional abstraction over \<open>x\<close>.
   814 
   815   \<^medskip>
   816   There is an additional set of combinators to accommodate multiple results
   817   (via pairs) that are passed on as multiple arguments (via currying).
   818 
   819   \<^medskip>
   820   \begin{tabular}{lll}
   821   \<open>(x, y) |-> f\<close> & \<open>\<equiv>\<close> & \<open>f x y\<close> \\
   822   \<open>(f #-> g) x\<close> & \<open>\<equiv>\<close> & \<open>x |> f |-> g\<close> \\
   823   \end{tabular}
   824   \<^medskip>
   825 \<close>
   826 
   827 text %mlref \<open>
   828   \begin{mldecls}
   829   @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
   830   @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
   831   @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
   832   @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
   833   \end{mldecls}
   834 \<close>
   835 
   836 
   837 subsection \<open>Canonical iteration\<close>
   838 
   839 text \<open>
   840   As explained above, a function \<open>f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>\<close> can be understood as update on
   841   a configuration of type \<open>\<beta>\<close>, parameterized by an argument of type \<open>\<alpha>\<close>. Given
   842   \<open>a: \<alpha>\<close> the partial application \<open>(f a): \<beta> \<rightarrow> \<beta>\<close> operates homogeneously on \<open>\<beta>\<close>.
   843   This can be iterated naturally over a list of parameters \<open>[a\<^sub>1, \<dots>, a\<^sub>n]\<close> as
   844   \<open>f a\<^sub>1 #> \<dots> #> f a\<^sub>n\<close>. The latter expression is again a function \<open>\<beta> \<rightarrow> \<beta>\<close>. It
   845   can be applied to an initial configuration \<open>b: \<beta>\<close> to start the iteration
   846   over the given list of arguments: each \<open>a\<close> in \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> is applied
   847   consecutively by updating a cumulative configuration.
   848 
   849   The \<open>fold\<close> combinator in Isabelle/ML lifts a function \<open>f\<close> as above to its
   850   iterated version over a list of arguments. Lifting can be repeated, e.g.\
   851   \<open>(fold \<circ> fold) f\<close> iterates over a list of lists as expected.
   852 
   853   The variant \<open>fold_rev\<close> works inside-out over the list of arguments, such
   854   that \<open>fold_rev f \<equiv> fold f \<circ> rev\<close> holds.
   855 
   856   The \<open>fold_map\<close> combinator essentially performs \<open>fold\<close> and \<open>map\<close>
   857   simultaneously: each application of \<open>f\<close> produces an updated configuration
   858   together with a side-result; the iteration collects all such side-results as
   859   a separate list.
   860 \<close>
   861 
   862 text %mlref \<open>
   863   \begin{mldecls}
   864   @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   865   @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   866   @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   867   \end{mldecls}
   868 
   869   \<^descr> @{ML fold}~\<open>f\<close> lifts the parametrized update function \<open>f\<close> to a list of
   870   parameters.
   871 
   872   \<^descr> @{ML fold_rev}~\<open>f\<close> is similar to @{ML fold}~\<open>f\<close>, but works inside-out, as
   873   if the list would be reversed.
   874 
   875   \<^descr> @{ML fold_map}~\<open>f\<close> lifts the parametrized update function \<open>f\<close> (with
   876   side-result) to a list of parameters and cumulative side-results.
   877 
   878 
   879   \begin{warn}
   880   The literature on functional programming provides a confusing multitude of
   881   combinators called \<open>foldl\<close>, \<open>foldr\<close> etc. SML97 provides its own variations
   882   as @{ML List.foldl} and @{ML List.foldr}, while the classic Isabelle library
   883   also has the historic @{ML Library.foldl} and @{ML Library.foldr}. To avoid
   884   unnecessary complication, all these historical versions should be ignored,
   885   and the canonical @{ML fold} (or @{ML fold_rev}) used exclusively.
   886   \end{warn}
   887 \<close>
   888 
   889 text %mlex \<open>
   890   The following example shows how to fill a text buffer incrementally by
   891   adding strings, either individually or from a given list.
   892 \<close>
   893 
   894 ML_val \<open>
   895   val s =
   896     Buffer.empty
   897     |> Buffer.add "digits: "
   898     |> fold (Buffer.add o string_of_int) (0 upto 9)
   899     |> Buffer.content;
   900 
   901   @{assert} (s = "digits: 0123456789");
   902 \<close>
   903 
   904 text \<open>
   905   Note how @{ML "fold (Buffer.add o string_of_int)"} above saves an extra @{ML
   906   "map"} over the given list. This kind of peephole optimization reduces both
   907   the code size and the tree structures in memory (``deforestation''), but it
   908   requires some practice to read and write fluently.
   909 
   910   \<^medskip>
   911   The next example elaborates the idea of canonical iteration, demonstrating
   912   fast accumulation of tree content using a text buffer.
   913 \<close>
   914 
   915 ML \<open>
   916   datatype tree = Text of string | Elem of string * tree list;
   917 
   918   fun slow_content (Text txt) = txt
   919     | slow_content (Elem (name, ts)) =
   920         "<" ^ name ^ ">" ^
   921         implode (map slow_content ts) ^
   922         "</" ^ name ^ ">"
   923 
   924   fun add_content (Text txt) = Buffer.add txt
   925     | add_content (Elem (name, ts)) =
   926         Buffer.add ("<" ^ name ^ ">") #>
   927         fold add_content ts #>
   928         Buffer.add ("</" ^ name ^ ">");
   929 
   930   fun fast_content tree =
   931     Buffer.empty |> add_content tree |> Buffer.content;
   932 \<close>
   933 
   934 text \<open>
   935   The slowness of @{ML slow_content} is due to the @{ML implode} of the
   936   recursive results, because it copies previously produced strings again and
   937   again.
   938 
   939   The incremental @{ML add_content} avoids this by operating on a buffer that
   940   is passed through in a linear fashion. Using @{ML_text "#>"} and contraction
   941   over the actual buffer argument saves some additional boiler-plate. Of
   942   course, the two @{ML "Buffer.add"} invocations with concatenated strings
   943   could have been split into smaller parts, but this would have obfuscated the
   944   source without making a big difference in performance. Here we have done
   945   some peephole-optimization for the sake of readability.
   946 
   947   Another benefit of @{ML add_content} is its ``open'' form as a function on
   948   buffers that can be continued in further linear transformations, folding
   949   etc. Thus it is more compositional than the naive @{ML slow_content}. As
   950   realistic example, compare the old-style @{ML "Term.maxidx_of_term: term ->
   951   int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in
   952   Isabelle/Pure.
   953 
   954   Note that @{ML fast_content} above is only defined as example. In many
   955   practical situations, it is customary to provide the incremental @{ML
   956   add_content} only and leave the initialization and termination to the
   957   concrete application to the user.
   958 \<close>
   959 
   960 
   961 section \<open>Message output channels \label{sec:message-channels}\<close>
   962 
   963 text \<open>
   964   Isabelle provides output channels for different kinds of messages: regular
   965   output, high-volume tracing information, warnings, and errors.
   966 
   967   Depending on the user interface involved, these messages may appear in
   968   different text styles or colours. The standard output for batch sessions
   969   prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by \<^verbatim>\<open>***\<close>, but leaves
   970   anything else unchanged. The message body may contain further markup and
   971   formatting, which is routinely used in the Prover IDE @{cite
   972   "isabelle-jedit"}.
   973 
   974   Messages are associated with the transaction context of the running Isar
   975   command. This enables the front-end to manage commands and resulting
   976   messages together. For example, after deleting a command from a given theory
   977   document version, the corresponding message output can be retracted from the
   978   display.
   979 \<close>
   980 
   981 text %mlref \<open>
   982   \begin{mldecls}
   983   @{index_ML writeln: "string -> unit"} \\
   984   @{index_ML tracing: "string -> unit"} \\
   985   @{index_ML warning: "string -> unit"} \\
   986   @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
   987   \end{mldecls}
   988 
   989   \<^descr> @{ML writeln}~\<open>text\<close> outputs \<open>text\<close> as regular message. This is the
   990   primary message output operation of Isabelle and should be used by default.
   991 
   992   \<^descr> @{ML tracing}~\<open>text\<close> outputs \<open>text\<close> as special tracing message, indicating
   993   potential high-volume output to the front-end (hundreds or thousands of
   994   messages issued by a single command). The idea is to allow the
   995   user-interface to downgrade the quality of message display to achieve higher
   996   throughput.
   997 
   998   Note that the user might have to take special actions to see tracing output,
   999   e.g.\ switch to a different output window. So this channel should not be
  1000   used for regular output.
  1001 
  1002   \<^descr> @{ML warning}~\<open>text\<close> outputs \<open>text\<close> as warning, which typically means some
  1003   extra emphasis on the front-end side (color highlighting, icons, etc.).
  1004 
  1005   \<^descr> @{ML error}~\<open>text\<close> raises exception @{ML ERROR}~\<open>text\<close> and thus lets the
  1006   Isar toplevel print \<open>text\<close> on the error channel, which typically means some
  1007   extra emphasis on the front-end side (color highlighting, icons, etc.).
  1008 
  1009   This assumes that the exception is not handled before the command
  1010   terminates. Handling exception @{ML ERROR}~\<open>text\<close> is a perfectly legal
  1011   alternative: it means that the error is absorbed without any message output.
  1012 
  1013   \begin{warn}
  1014   The actual error channel is accessed via @{ML Output.error_message}, but
  1015   this is normally not used directly in user code.
  1016   \end{warn}
  1017 
  1018 
  1019   \begin{warn}
  1020   Regular Isabelle/ML code should output messages exclusively by the official
  1021   channels. Using raw I/O on \<^emph>\<open>stdout\<close> or \<^emph>\<open>stderr\<close> instead (e.g.\ via @{ML
  1022   TextIO.output}) is apt to cause problems in the presence of parallel and
  1023   asynchronous processing of Isabelle theories. Such raw output might be
  1024   displayed by the front-end in some system console log, with a low chance
  1025   that the user will ever see it. Moreover, as a genuine side-effect on global
  1026   process channels, there is no proper way to retract output when Isar command
  1027   transactions are reset by the system.
  1028   \end{warn}
  1029 
  1030   \begin{warn}
  1031   The message channels should be used in a message-oriented manner. This means
  1032   that multi-line output that logically belongs together is issued by a single
  1033   invocation of @{ML writeln} etc.\ with the functional concatenation of all
  1034   message constituents.
  1035   \end{warn}
  1036 \<close>
  1037 
  1038 text %mlex \<open>
  1039   The following example demonstrates a multi-line warning. Note that in some
  1040   situations the user sees only the first line, so the most important point
  1041   should be made first.
  1042 \<close>
  1043 
  1044 ML_command \<open>
  1045   warning (cat_lines
  1046    ["Beware the Jabberwock, my son!",
  1047     "The jaws that bite, the claws that catch!",
  1048     "Beware the Jubjub Bird, and shun",
  1049     "The frumious Bandersnatch!"]);
  1050 \<close>
  1051 
  1052 text \<open>
  1053   \<^medskip>
  1054   An alternative is to make a paragraph of freely-floating words as follows.
  1055 \<close>
  1056 
  1057 ML_command \<open>
  1058   warning (Pretty.string_of (Pretty.para
  1059     "Beware the Jabberwock, my son! \
  1060     \The jaws that bite, the claws that catch! \
  1061     \Beware the Jubjub Bird, and shun \
  1062     \The frumious Bandersnatch!"))
  1063 \<close>
  1064 
  1065 text \<open>
  1066   This has advantages with variable window / popup sizes, but might make it
  1067   harder to search for message content systematically, e.g.\ by other tools or
  1068   by humans expecting the ``verse'' of a formal message in a fixed layout.
  1069 \<close>
  1070 
  1071 
  1072 section \<open>Exceptions \label{sec:exceptions}\<close>
  1073 
  1074 text \<open>
  1075   The Standard ML semantics of strict functional evaluation together with
  1076   exceptions is rather well defined, but some delicate points need to be
  1077   observed to avoid that ML programs go wrong despite static type-checking.
  1078   Exceptions in Isabelle/ML are subsequently categorized as follows.
  1079 \<close>
  1080 
  1081 paragraph \<open>Regular user errors.\<close>
  1082 text \<open>
  1083   These are meant to provide informative feedback about malformed input etc.
  1084 
  1085   The \<^emph>\<open>error\<close> function raises the corresponding @{ML ERROR} exception, with a
  1086   plain text message as argument. @{ML ERROR} exceptions can be handled
  1087   internally, in order to be ignored, turned into other exceptions, or
  1088   cascaded by appending messages. If the corresponding Isabelle/Isar command
  1089   terminates with an @{ML ERROR} exception state, the system will print the
  1090   result on the error channel (see \secref{sec:message-channels}).
  1091 
  1092   It is considered bad style to refer to internal function names or values in
  1093   ML source notation in user error messages. Do not use \<open>@{make_string}\<close> nor
  1094   \<open>@{here}\<close>!
  1095 
  1096   Grammatical correctness of error messages can be improved by \<^emph>\<open>omitting\<close>
  1097   final punctuation: messages are often concatenated or put into a larger
  1098   context (e.g.\ augmented with source position). Note that punctuation after
  1099   formal entities (types, terms, theorems) is particularly prone to user
  1100   confusion.
  1101 \<close>
  1102 
  1103 paragraph \<open>Program failures.\<close>
  1104 text \<open>
  1105   There is a handful of standard exceptions that indicate general failure
  1106   situations, or failures of core operations on logical entities (types,
  1107   terms, theorems, theories, see \chref{ch:logic}).
  1108 
  1109   These exceptions indicate a genuine breakdown of the program, so the main
  1110   purpose is to determine quickly what has happened where. Traditionally, the
  1111   (short) exception message would include the name of an ML function, although
  1112   this is no longer necessary, because the ML runtime system attaches detailed
  1113   source position stemming from the corresponding @{ML_text raise} keyword.
  1114 
  1115   \<^medskip>
  1116   User modules can always introduce their own custom exceptions locally, e.g.\
  1117   to organize internal failures robustly without overlapping with existing
  1118   exceptions. Exceptions that are exposed in module signatures require extra
  1119   care, though, and should \<^emph>\<open>not\<close> be introduced by default. Surprise by users
  1120   of a module can be often minimized by using plain user errors instead.
  1121 \<close>
  1122 
  1123 paragraph \<open>Interrupts.\<close>
  1124 text \<open>
  1125   These indicate arbitrary system events: both the ML runtime system and the
  1126   Isabelle/ML infrastructure signal various exceptional situations by raising
  1127   the special @{ML Exn.Interrupt} exception in user code.
  1128 
  1129   This is the one and only way that physical events can intrude an Isabelle/ML
  1130   program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
  1131   internal signaling of threads, or a POSIX process signal. An Isabelle/ML
  1132   program that intercepts interrupts becomes dependent on physical effects of
  1133   the environment. Even worse, exception handling patterns that are too
  1134   general by accident, e.g.\ by misspelled exception constructors, will cover
  1135   interrupts unintentionally and thus render the program semantics
  1136   ill-defined.
  1137 
  1138   Note that the Interrupt exception dates back to the original SML90 language
  1139   definition. It was excluded from the SML97 version to avoid its malign
  1140   impact on ML program semantics, but without providing a viable alternative.
  1141   Isabelle/ML recovers physical interruptibility (which is an indispensable
  1142   tool to implement managed evaluation of command transactions), but requires
  1143   user code to be strictly transparent wrt.\ interrupts.
  1144 
  1145   \begin{warn}
  1146   Isabelle/ML user code needs to terminate promptly on interruption, without
  1147   guessing at its meaning to the system infrastructure. Temporary handling of
  1148   interrupts for cleanup of global resources etc.\ needs to be followed
  1149   immediately by re-raising of the original exception.
  1150   \end{warn}
  1151 \<close>
  1152 
  1153 text %mlref \<open>
  1154   \begin{mldecls}
  1155   @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
  1156   @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
  1157   @{index_ML_exception ERROR: string} \\
  1158   @{index_ML_exception Fail: string} \\
  1159   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
  1160   @{index_ML Exn.reraise: "exn -> 'a"} \\
  1161   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
  1162   \end{mldecls}
  1163 
  1164   \<^descr> @{ML try}~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via the
  1165   option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form serves
  1166   as safe replacement for the \<^emph>\<open>unsafe\<close> version @{ML_text "(SOME"}~\<open>f
  1167   x\<close>~@{ML_text "handle _ => NONE)"} that is occasionally seen in books about
  1168   SML97, but not in Isabelle/ML.
  1169 
  1170   \<^descr> @{ML can} is similar to @{ML try} with more abstract result.
  1171 
  1172   \<^descr> @{ML ERROR}~\<open>msg\<close> represents user errors; this exception is normally
  1173   raised indirectly via the @{ML error} function (see
  1174   \secref{sec:message-channels}).
  1175 
  1176   \<^descr> @{ML Fail}~\<open>msg\<close> represents general program failures.
  1177 
  1178   \<^descr> @{ML Exn.is_interrupt} identifies interrupts robustly, without mentioning
  1179   concrete exception constructors in user code. Handled interrupts need to be
  1180   re-raised promptly!
  1181 
  1182   \<^descr> @{ML Exn.reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
  1183   position information (if possible, depending on the ML platform).
  1184 
  1185   \<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~\<open>e\<close>@{ML_text ")"} evaluates
  1186   expression \<open>e\<close> while printing a full trace of its stack of nested exceptions
  1187   (if possible, depending on the ML platform).
  1188 
  1189   Inserting @{ML Runtime.exn_trace} into ML code temporarily is useful for
  1190   debugging, but not suitable for production code.
  1191 \<close>
  1192 
  1193 text %mlantiq \<open>
  1194   \begin{matharray}{rcl}
  1195   @{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
  1196   \end{matharray}
  1197 
  1198   \<^descr> \<open>@{assert}\<close> inlines a function @{ML_type "bool -> unit"} that raises @{ML
  1199   Fail} if the argument is @{ML false}. Due to inlining the source position of
  1200   failed assertions is included in the error output.
  1201 \<close>
  1202 
  1203 
  1204 section \<open>Strings of symbols \label{sec:symbols}\<close>
  1205 
  1206 text \<open>
  1207   A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in Isabelle/ML --- raw ML
  1208   characters are normally not encountered at all. Isabelle strings consist of
  1209   a sequence of symbols, represented as a packed string or an exploded list of
  1210   strings. Each symbol is in itself a small string, which has either one of
  1211   the following forms:
  1212 
  1213     \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
  1214 
  1215     \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
  1216 
  1217     \<^enum> a regular symbol ``\<^verbatim>\<open>\<ident>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
  1218 
  1219     \<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
  1220 
  1221     \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of
  1222     printable characters excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
  1223     ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
  1224 
  1225     \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
  1226     of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
  1227 
  1228   The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
  1229   \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
  1230   symbols and control symbols, but a fixed collection of standard symbols is
  1231   treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is classified as a letter, which
  1232   means it may occur within regular Isabelle identifiers.
  1233 
  1234   The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit
  1235   character sequences are passed-through unchanged. Unicode/UCS data in UTF-8
  1236   encoding is processed in a non-strict fashion, such that well-formed code
  1237   sequences are recognized accordingly. Unicode provides its own collection of
  1238   mathematical symbols, but within the core Isabelle/ML world there is no link
  1239   to the standard collection of Isabelle regular symbols.
  1240 
  1241   \<^medskip>
  1242   Output of Isabelle symbols depends on the print mode. For example, the
  1243   standard {\LaTeX} setup of the Isabelle document preparation system would
  1244   present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually
  1245   works by mapping a finite subset of Isabelle symbols to suitable Unicode
  1246   characters.
  1247 \<close>
  1248 
  1249 text %mlref \<open>
  1250   \begin{mldecls}
  1251   @{index_ML_type "Symbol.symbol": string} \\
  1252   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
  1253   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
  1254   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
  1255   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
  1256   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
  1257   \end{mldecls}
  1258   \begin{mldecls}
  1259   @{index_ML_type "Symbol.sym"} \\
  1260   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
  1261   \end{mldecls}
  1262 
  1263   \<^descr> Type @{ML_type "Symbol.symbol"} represents individual Isabelle symbols.
  1264 
  1265   \<^descr> @{ML "Symbol.explode"}~\<open>str\<close> produces a symbol list from the packed form.
  1266   This function supersedes @{ML "String.explode"} for virtually all purposes
  1267   of manipulating text in Isabelle!\<^footnote>\<open>The runtime overhead for exploded strings
  1268   is mainly that of the list structure: individual symbols that happen to be a
  1269   singleton string do not require extra memory in Poly/ML.\<close>
  1270 
  1271   \<^descr> @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
  1272   "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard symbols
  1273   according to fixed syntactic conventions of Isabelle, cf.\ @{cite
  1274   "isabelle-isar-ref"}.
  1275 
  1276   \<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the
  1277   different kinds of symbols explicitly, with constructors @{ML
  1278   "Symbol.Char"}, @{ML "Symbol.UTF8"}, @{ML "Symbol.Sym"}, @{ML
  1279   "Symbol.Control"}, @{ML "Symbol.Raw"}, @{ML "Symbol.Malformed"}.
  1280 
  1281   \<^descr> @{ML "Symbol.decode"} converts the string representation of a symbol into
  1282   the datatype version.
  1283 \<close>
  1284 
  1285 paragraph \<open>Historical note.\<close>
  1286 text \<open>
  1287   In the original SML90 standard the primitive ML type @{ML_type char} did not
  1288   exists, and @{ML_text "explode: string -> string list"} produced a list of
  1289   singleton strings like @{ML "raw_explode: string -> string list"} in
  1290   Isabelle/ML today. When SML97 came out, Isabelle did not adopt its somewhat
  1291   anachronistic 8-bit or 16-bit characters, but the idea of exploding a string
  1292   into a list of small strings was extended to ``symbols'' as explained above.
  1293   Thus Isabelle sources can refer to an infinite store of user-defined
  1294   symbols, without having to worry about the multitude of Unicode encodings
  1295   that have emerged over the years.
  1296 \<close>
  1297 
  1298 
  1299 section \<open>Basic data types\<close>
  1300 
  1301 text \<open>
  1302   The basis library proposal of SML97 needs to be treated with caution. Many
  1303   of its operations simply do not fit with important Isabelle/ML conventions
  1304   (like ``canonical argument order'', see
  1305   \secref{sec:canonical-argument-order}), others cause problems with the
  1306   parallel evaluation model of Isabelle/ML (such as @{ML TextIO.print} or @{ML
  1307   OS.Process.system}).
  1308 
  1309   Subsequently we give a brief overview of important operations on basic ML
  1310   data types.
  1311 \<close>
  1312 
  1313 
  1314 subsection \<open>Characters\<close>
  1315 
  1316 text %mlref \<open>
  1317   \begin{mldecls}
  1318   @{index_ML_type char} \\
  1319   \end{mldecls}
  1320 
  1321   \<^descr> Type @{ML_type char} is \<^emph>\<open>not\<close> used. The smallest textual unit in Isabelle
  1322   is represented as a ``symbol'' (see \secref{sec:symbols}).
  1323 \<close>
  1324 
  1325 
  1326 subsection \<open>Strings\<close>
  1327 
  1328 text %mlref \<open>
  1329   \begin{mldecls}
  1330   @{index_ML_type string} \\
  1331   \end{mldecls}
  1332 
  1333   \<^descr> Type @{ML_type string} represents immutable vectors of 8-bit characters.
  1334   There are operations in SML to convert back and forth to actual byte
  1335   vectors, which are seldom used.
  1336 
  1337   This historically important raw text representation is used for
  1338   Isabelle-specific purposes with the following implicit substructures packed
  1339   into the string content:
  1340 
  1341     \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with @{ML
  1342     Symbol.explode} as key operation;
  1343   
  1344     \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with
  1345     @{ML YXML.parse_body} as key operation.
  1346 
  1347   Note that Isabelle/ML string literals may refer Isabelle symbols like
  1348   ``\<^verbatim>\<open>\<alpha>\<close>'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a consequence
  1349   of Isabelle treating all source text as strings of symbols, instead of raw
  1350   characters.
  1351 \<close>
  1352 
  1353 text %mlex \<open>
  1354   The subsequent example illustrates the difference of physical addressing of
  1355   bytes versus logical addressing of symbols in Isabelle strings.
  1356 \<close>
  1357 
  1358 ML_val \<open>
  1359   val s = "\<A>";
  1360 
  1361   @{assert} (length (Symbol.explode s) = 1);
  1362   @{assert} (size s = 4);
  1363 \<close>
  1364 
  1365 text \<open>
  1366   Note that in Unicode renderings of the symbol \<open>\<A>\<close>, variations of encodings
  1367   like UTF-8 or UTF-16 pose delicate questions about the multi-byte
  1368   representations of its codepoint, which is outside of the 16-bit address
  1369   space of the original Unicode standard from the 1990-ies. In Isabelle/ML it
  1370   is just ``\<^verbatim>\<open>\<A>\<close>'' literally, using plain ASCII characters beyond any
  1371   doubts.
  1372 \<close>
  1373 
  1374 
  1375 subsection \<open>Integers\<close>
  1376 
  1377 text %mlref \<open>
  1378   \begin{mldecls}
  1379   @{index_ML_type int} \\
  1380   \end{mldecls}
  1381 
  1382   \<^descr> Type @{ML_type int} represents regular mathematical integers, which are
  1383   \<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in
  1384   practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
  1385   32-bit Poly/ML, and much higher for 64-bit systems.\<close>
  1386 
  1387   Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
  1388   @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
  1389   "~~/src/Pure/General/integer.ML"} provides some additional operations.
  1390 \<close>
  1391 
  1392 
  1393 subsection \<open>Rational numbers\<close>
  1394 
  1395 text %mlref \<open>
  1396   \begin{mldecls}
  1397   @{index_ML_type Rat.rat} \\
  1398   \end{mldecls}
  1399 
  1400   \<^descr> Type @{ML_type Rat.rat} represents rational numbers, based on the
  1401   unbounded integers of Poly/ML.
  1402 
  1403   Literal rationals may be written with special antiquotation syntax
  1404   \<^verbatim>\<open>@\<close>\<open>int\<close>\<^verbatim>\<open>/\<close>\<open>nat\<close> or \<^verbatim>\<open>@\<close>\<open>int\<close> (without any white space). For example
  1405   \<^verbatim>\<open>@~1/4\<close> or \<^verbatim>\<open>@10\<close>. The ML toplevel pretty printer uses the same format.
  1406 
  1407   Standard operations are provided via ad-hoc overloading of \<^verbatim>\<open>+\<close>, \<^verbatim>\<open>-\<close>, \<^verbatim>\<open>*\<close>,
  1408   \<^verbatim>\<open>/\<close>, etc.
  1409 \<close>
  1410 
  1411 
  1412 subsection \<open>Time\<close>
  1413 
  1414 text %mlref \<open>
  1415   \begin{mldecls}
  1416   @{index_ML_type Time.time} \\
  1417   @{index_ML seconds: "real -> Time.time"} \\
  1418   \end{mldecls}
  1419 
  1420   \<^descr> Type @{ML_type Time.time} represents time abstractly according to the
  1421   SML97 basis library definition. This is adequate for internal ML operations,
  1422   but awkward in concrete time specifications.
  1423 
  1424   \<^descr> @{ML seconds}~\<open>s\<close> turns the concrete scalar \<open>s\<close> (measured in seconds) into
  1425   an abstract time value. Floating point numbers are easy to use as
  1426   configuration options in the context (see \secref{sec:config-options}) or
  1427   system options that are maintained externally.
  1428 \<close>
  1429 
  1430 
  1431 subsection \<open>Options\<close>
  1432 
  1433 text %mlref \<open>
  1434   \begin{mldecls}
  1435   @{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\
  1436   @{index_ML is_some: "'a option -> bool"} \\
  1437   @{index_ML is_none: "'a option -> bool"} \\
  1438   @{index_ML the: "'a option -> 'a"} \\
  1439   @{index_ML these: "'a list option -> 'a list"} \\
  1440   @{index_ML the_list: "'a option -> 'a list"} \\
  1441   @{index_ML the_default: "'a -> 'a option -> 'a"} \\
  1442   \end{mldecls}
  1443 \<close>
  1444 
  1445 text \<open>
  1446   Apart from @{ML Option.map} most other operations defined in structure
  1447   @{ML_structure Option} are alien to Isabelle/ML and never used. The
  1448   operations shown above are defined in @{file
  1449   "~~/src/Pure/General/basics.ML"}.
  1450 \<close>
  1451 
  1452 
  1453 subsection \<open>Lists\<close>
  1454 
  1455 text \<open>
  1456   Lists are ubiquitous in ML as simple and light-weight ``collections'' for
  1457   many everyday programming tasks. Isabelle/ML provides important additions
  1458   and improvements over operations that are predefined in the SML97 library.
  1459 \<close>
  1460 
  1461 text %mlref \<open>
  1462   \begin{mldecls}
  1463   @{index_ML cons: "'a -> 'a list -> 'a list"} \\
  1464   @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
  1465   @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
  1466   @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
  1467   @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
  1468   \end{mldecls}
  1469 
  1470   \<^descr> @{ML cons}~\<open>x xs\<close> evaluates to \<open>x :: xs\<close>.
  1471 
  1472   Tupled infix operators are a historical accident in Standard ML. The curried
  1473   @{ML cons} amends this, but it should be only used when partial application
  1474   is required.
  1475 
  1476   \<^descr> @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat lists as a
  1477   set-like container that maintains the order of elements. See @{file
  1478   "~~/src/Pure/library.ML"} for the full specifications (written in ML). There
  1479   are some further derived operations like @{ML union} or @{ML inter}.
  1480 
  1481   Note that @{ML insert} is conservative about elements that are already a
  1482   @{ML member} of the list, while @{ML update} ensures that the latest entry
  1483   is always put in front. The latter discipline is often more appropriate in
  1484   declarations of context data (\secref{sec:context-data}) that are issued by
  1485   the user in Isar source: later declarations take precedence over earlier
  1486   ones. \<close>
  1487 
  1488 text %mlex \<open>
  1489   Using canonical @{ML fold} together with @{ML cons} (or similar standard
  1490   operations) alternates the orientation of data. The is quite natural and
  1491   should not be altered forcible by inserting extra applications of @{ML rev}.
  1492   The alternative @{ML fold_rev} can be used in the few situations, where
  1493   alternation should be prevented.
  1494 \<close>
  1495 
  1496 ML_val \<open>
  1497   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
  1498 
  1499   val list1 = fold cons items [];
  1500   @{assert} (list1 = rev items);
  1501 
  1502   val list2 = fold_rev cons items [];
  1503   @{assert} (list2 = items);
  1504 \<close>
  1505 
  1506 text \<open>
  1507   The subsequent example demonstrates how to \<^emph>\<open>merge\<close> two lists in a natural
  1508   way.
  1509 \<close>
  1510 
  1511 ML_val \<open>
  1512   fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
  1513 \<close>
  1514 
  1515 text \<open>
  1516   Here the first list is treated conservatively: only the new elements from
  1517   the second list are inserted. The inside-out order of insertion via @{ML
  1518   fold_rev} attempts to preserve the order of elements in the result.
  1519 
  1520   This way of merging lists is typical for context data
  1521   (\secref{sec:context-data}). See also @{ML merge} as defined in @{file
  1522   "~~/src/Pure/library.ML"}.
  1523 \<close>
  1524 
  1525 
  1526 subsection \<open>Association lists\<close>
  1527 
  1528 text \<open>
  1529   The operations for association lists interpret a concrete list of pairs as a
  1530   finite function from keys to values. Redundant representations with multiple
  1531   occurrences of the same key are implicitly normalized: lookup and update
  1532   only take the first occurrence into account.
  1533 \<close>
  1534 
  1535 text \<open>
  1536   \begin{mldecls}
  1537   @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
  1538   @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
  1539   @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
  1540   \end{mldecls}
  1541 
  1542   \<^descr> @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update} implement the
  1543   main ``framework operations'' for mappings in Isabelle/ML, following
  1544   standard conventions for their names and types.
  1545 
  1546   Note that a function called \<^verbatim>\<open>lookup\<close> is obliged to express its partiality
  1547   via an explicit option element. There is no choice to raise an exception,
  1548   without changing the name to something like \<open>the_element\<close> or \<open>get\<close>.
  1549 
  1550   The \<open>defined\<close> operation is essentially a contraction of @{ML is_some} and
  1551   \<^verbatim>\<open>lookup\<close>, but this is sufficiently frequent to justify its independent
  1552   existence. This also gives the implementation some opportunity for peep-hole
  1553   optimization.
  1554 
  1555 
  1556   Association lists are adequate as simple implementation of finite mappings
  1557   in many practical situations. A more advanced table structure is defined in
  1558   @{file "~~/src/Pure/General/table.ML"}; that version scales easily to
  1559   thousands or millions of elements.
  1560 \<close>
  1561 
  1562 
  1563 subsection \<open>Unsynchronized references\<close>
  1564 
  1565 text %mlref \<open>
  1566   \begin{mldecls}
  1567   @{index_ML_type "'a Unsynchronized.ref"} \\
  1568   @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
  1569   @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
  1570   @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
  1571   \end{mldecls}
  1572 \<close>
  1573 
  1574 text \<open>
  1575   Due to ubiquitous parallelism in Isabelle/ML (see also
  1576   \secref{sec:multi-threading}), the mutable reference cells of Standard ML
  1577   are notorious for causing problems. In a highly parallel system, both
  1578   correctness \<^emph>\<open>and\<close> performance are easily degraded when using mutable data.
  1579 
  1580   The unwieldy name of @{ML Unsynchronized.ref} for the constructor for
  1581   references in Isabelle/ML emphasizes the inconveniences caused by
  1582   mutability. Existing operations @{ML "!"} and @{ML_op ":="} are unchanged,
  1583   but should be used with special precautions, say in a strictly local
  1584   situation that is guaranteed to be restricted to sequential evaluation ---
  1585   now and in the future.
  1586 
  1587   \begin{warn}
  1588   Never @{ML_text "open Unsynchronized"}, not even in a local scope!
  1589   Pretending that mutable state is no problem is a very bad idea.
  1590   \end{warn}
  1591 \<close>
  1592 
  1593 
  1594 section \<open>Thread-safe programming \label{sec:multi-threading}\<close>
  1595 
  1596 text \<open>
  1597   Multi-threaded execution has become an everyday reality in Isabelle since
  1598   Poly/ML 5.2.1 and Isabelle2008. Isabelle/ML provides implicit and explicit
  1599   parallelism by default, and there is no way for user-space tools to ``opt
  1600   out''. ML programs that are purely functional, output messages only via the
  1601   official channels (\secref{sec:message-channels}), and do not intercept
  1602   interrupts (\secref{sec:exceptions}) can participate in the multi-threaded
  1603   environment immediately without further ado.
  1604 
  1605   More ambitious tools with more fine-grained interaction with the environment
  1606   need to observe the principles explained below.
  1607 \<close>
  1608 
  1609 
  1610 subsection \<open>Multi-threading with shared memory\<close>
  1611 
  1612 text \<open>
  1613   Multiple threads help to organize advanced operations of the system, such as
  1614   real-time conditions on command transactions, sub-components with explicit
  1615   communication, general asynchronous interaction etc. Moreover, parallel
  1616   evaluation is a prerequisite to make adequate use of the CPU resources that
  1617   are available on multi-core systems.\<^footnote>\<open>Multi-core computing does not mean
  1618   that there are ``spare cycles'' to be wasted. It means that the continued
  1619   exponential speedup of CPU performance due to ``Moore's Law'' follows
  1620   different rules: clock frequency has reached its peak around 2005, and
  1621   applications need to be parallelized in order to avoid a perceived loss of
  1622   performance. See also @{cite "Sutter:2005"}.\<close>
  1623 
  1624   Isabelle/Isar exploits the inherent structure of theories and proofs to
  1625   support \<^emph>\<open>implicit parallelism\<close> to a large extent. LCF-style theorem proving
  1626   provides almost ideal conditions for that, see also @{cite "Wenzel:2009"}.
  1627   This means, significant parts of theory and proof checking is parallelized
  1628   by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and
  1629   6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}.
  1630 
  1631   \<^medskip>
  1632   ML threads lack the memory protection of separate processes, and operate
  1633   concurrently on shared heap memory. This has the advantage that results of
  1634   independent computations are directly available to other threads: abstract
  1635   values can be passed without copying or awkward serialization that is
  1636   typically required for separate processes.
  1637 
  1638   To make shared-memory multi-threading work robustly and efficiently, some
  1639   programming guidelines need to be observed. While the ML system is
  1640   responsible to maintain basic integrity of the representation of ML values
  1641   in memory, the application programmer needs to ensure that multi-threaded
  1642   execution does not break the intended semantics.
  1643 
  1644   \begin{warn}
  1645   To participate in implicit parallelism, tools need to be thread-safe. A
  1646   single ill-behaved tool can affect the stability and performance of the
  1647   whole system.
  1648   \end{warn}
  1649 
  1650   Apart from observing the principles of thread-safeness passively, advanced
  1651   tools may also exploit parallelism actively, e.g.\ by using library
  1652   functions for parallel list operations (\secref{sec:parlist}).
  1653 
  1654   \begin{warn}
  1655   Parallel computing resources are managed centrally by the Isabelle/ML
  1656   infrastructure. User programs should not fork their own ML threads to
  1657   perform heavy computations.
  1658   \end{warn}
  1659 \<close>
  1660 
  1661 
  1662 subsection \<open>Critical shared resources\<close>
  1663 
  1664 text \<open>
  1665   Thread-safeness is mainly concerned about concurrent read/write access to
  1666   shared resources, which are outside the purely functional world of ML. This
  1667   covers the following in particular.
  1668 
  1669     \<^item> Global references (or arrays), i.e.\ mutable memory cells that persist
  1670     over several invocations of associated operations.\<^footnote>\<open>This is independent of
  1671     the visibility of such mutable values in the toplevel scope.\<close>
  1672 
  1673     \<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O channels,
  1674     environment variables, current working directory.
  1675 
  1676     \<^item> Writable resources in the file-system that are shared among different
  1677     threads or external processes.
  1678 
  1679   Isabelle/ML provides various mechanisms to avoid critical shared resources
  1680   in most situations. As last resort there are some mechanisms for explicit
  1681   synchronization. The following guidelines help to make Isabelle/ML programs
  1682   work smoothly in a concurrent environment.
  1683 
  1684   \<^item> Avoid global references altogether. Isabelle/Isar maintains a uniform
  1685   context that incorporates arbitrary data declared by user programs
  1686   (\secref{sec:context-data}). This context is passed as plain value and user
  1687   tools can get/map their own data in a purely functional manner.
  1688   Configuration options within the context (\secref{sec:config-options})
  1689   provide simple drop-in replacements for historic reference variables.
  1690 
  1691   \<^item> Keep components with local state information re-entrant. Instead of poking
  1692   initial values into (private) global references, a new state record can be
  1693   created on each invocation, and passed through any auxiliary functions of
  1694   the component. The state record contain mutable references in special
  1695   situations, without requiring any synchronization, as long as each
  1696   invocation gets its own copy and the tool itself is single-threaded.
  1697 
  1698   \<^item> Avoid raw output on \<open>stdout\<close> or \<open>stderr\<close>. The Poly/ML library is
  1699   thread-safe for each individual output operation, but the ordering of
  1700   parallel invocations is arbitrary. This means raw output will appear on some
  1701   system console with unpredictable interleaving of atomic chunks.
  1702 
  1703   Note that this does not affect regular message output channels
  1704   (\secref{sec:message-channels}). An official message id is associated with
  1705   the command transaction from where it originates, independently of other
  1706   transactions. This means each running Isar command has effectively its own
  1707   set of message channels, and interleaving can only happen when commands use
  1708   parallelism internally (and only at message boundaries).
  1709 
  1710   \<^item> Treat environment variables and the current working directory of the
  1711   running process as read-only.
  1712 
  1713   \<^item> Restrict writing to the file-system to unique temporary files. Isabelle
  1714   already provides a temporary directory that is unique for the running
  1715   process, and there is a centralized source of unique serial numbers in
  1716   Isabelle/ML. Thus temporary files that are passed to to some external
  1717   process will be always disjoint, and thus thread-safe.
  1718 \<close>
  1719 
  1720 text %mlref \<open>
  1721   \begin{mldecls}
  1722   @{index_ML File.tmp_path: "Path.T -> Path.T"} \\
  1723   @{index_ML serial_string: "unit -> string"} \\
  1724   \end{mldecls}
  1725 
  1726   \<^descr> @{ML File.tmp_path}~\<open>path\<close> relocates the base component of \<open>path\<close> into the
  1727   unique temporary directory of the running Isabelle/ML process.
  1728 
  1729   \<^descr> @{ML serial_string}~\<open>()\<close> creates a new serial number that is unique over
  1730   the runtime of the Isabelle/ML process.
  1731 \<close>
  1732 
  1733 text %mlex \<open>
  1734   The following example shows how to create unique temporary file names.
  1735 \<close>
  1736 
  1737 ML_val \<open>
  1738   val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
  1739   val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
  1740   @{assert} (tmp1 <> tmp2);
  1741 \<close>
  1742 
  1743 
  1744 subsection \<open>Explicit synchronization\<close>
  1745 
  1746 text \<open>
  1747   Isabelle/ML provides explicit synchronization for mutable variables over
  1748   immutable data, which may be updated atomically and exclusively. This
  1749   addresses the rare situations where mutable shared resources are really
  1750   required. Synchronization in Isabelle/ML is based on primitives of Poly/ML,
  1751   which have been adapted to the specific assumptions of the concurrent
  1752   Isabelle environment. User code should not break this abstraction, but stay
  1753   within the confines of concurrent Isabelle/ML.
  1754 
  1755   A \<^emph>\<open>synchronized variable\<close> is an explicit state component associated with
  1756   mechanisms for locking and signaling. There are operations to await a
  1757   condition, change the state, and signal the change to all other waiting
  1758   threads. Synchronized access to the state variable is \<^emph>\<open>not\<close> re-entrant:
  1759   direct or indirect nesting within the same thread will cause a deadlock!
  1760 \<close>
  1761 
  1762 text %mlref \<open>
  1763   \begin{mldecls}
  1764   @{index_ML_type "'a Synchronized.var"} \\
  1765   @{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
  1766   @{index_ML Synchronized.guarded_access: "'a Synchronized.var ->
  1767   ('a -> ('b * 'a) option) -> 'b"} \\
  1768   \end{mldecls}
  1769 
  1770     \<^descr> Type @{ML_type "'a Synchronized.var"} represents synchronized variables
  1771     with state of type @{ML_type 'a}.
  1772 
  1773     \<^descr> @{ML Synchronized.var}~\<open>name x\<close> creates a synchronized variable that is
  1774     initialized with value \<open>x\<close>. The \<open>name\<close> is used for tracing.
  1775 
  1776     \<^descr> @{ML Synchronized.guarded_access}~\<open>var f\<close> lets the function \<open>f\<close> operate
  1777     within a critical section on the state \<open>x\<close> as follows: if \<open>f x\<close> produces
  1778     @{ML NONE}, it continues to wait on the internal condition variable,
  1779     expecting that some other thread will eventually change the content in a
  1780     suitable manner; if \<open>f x\<close> produces @{ML SOME}~\<open>(y, x')\<close> it is satisfied and
  1781     assigns the new state value \<open>x'\<close>, broadcasts a signal to all waiting threads
  1782     on the associated condition variable, and returns the result \<open>y\<close>.
  1783 
  1784   There are some further variants of the @{ML Synchronized.guarded_access}
  1785   combinator, see @{file "~~/src/Pure/Concurrent/synchronized.ML"} for
  1786   details.
  1787 \<close>
  1788 
  1789 text %mlex \<open>
  1790   The following example implements a counter that produces positive integers
  1791   that are unique over the runtime of the Isabelle process:
  1792 \<close>
  1793 
  1794 ML_val \<open>
  1795   local
  1796     val counter = Synchronized.var "counter" 0;
  1797   in
  1798     fun next () =
  1799       Synchronized.guarded_access counter
  1800         (fn i =>
  1801           let val j = i + 1
  1802           in SOME (j, j) end);
  1803   end;
  1804 
  1805   val a = next ();
  1806   val b = next ();
  1807   @{assert} (a <> b);
  1808 \<close>
  1809 
  1810 text \<open>
  1811   \<^medskip>
  1812   See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox
  1813   as synchronized variable over a purely functional list.
  1814 \<close>
  1815 
  1816 
  1817 section \<open>Managed evaluation\<close>
  1818 
  1819 text \<open>
  1820   Execution of Standard ML follows the model of strict functional evaluation
  1821   with optional exceptions. Evaluation happens whenever some function is
  1822   applied to (sufficiently many) arguments. The result is either an explicit
  1823   value or an implicit exception.
  1824 
  1825   \<^emph>\<open>Managed evaluation\<close> in Isabelle/ML organizes expressions and results to
  1826   control certain physical side-conditions, to say more specifically when and
  1827   how evaluation happens. For example, the Isabelle/ML library supports lazy
  1828   evaluation with memoing, parallel evaluation via futures, asynchronous
  1829   evaluation via promises, evaluation with time limit etc.
  1830 
  1831   \<^medskip>
  1832   An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction \<^verbatim>\<open>fn
  1833   () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of type
  1834   \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required to
  1835   tell them apart --- the static type-system of SML is only of limited help
  1836   here.
  1837 
  1838   The first form is more intuitive: some combinator \<open>(unit -> 'a) -> 'a\<close>
  1839   applies the given function to \<open>()\<close> to initiate the postponed evaluation
  1840   process. The second form is more flexible: some combinator \<open>('a -> 'b) -> 'a
  1841   -> 'b\<close> acts like a modified form of function application; several such
  1842   combinators may be cascaded to modify a given function, before it is
  1843   ultimately applied to some argument.
  1844 
  1845   \<^medskip>
  1846   \<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions
  1847   exceptional situations explicit as ML datatype: \<open>'a result = Res of 'a | Exn
  1848   of exn\<close>. This is typically used for administrative purposes, to store the
  1849   overall outcome of an evaluation process.
  1850 
  1851   \<^emph>\<open>Parallel exceptions\<close> aggregate reified results, such that multiple
  1852   exceptions are digested as a collection in canonical form that identifies
  1853   exceptions according to their original occurrence. This is particular
  1854   important for parallel evaluation via futures \secref{sec:futures}, which
  1855   are organized as acyclic graph of evaluations that depend on other
  1856   evaluations: exceptions stemming from shared sub-graphs are exposed exactly
  1857   once and in the order of their original occurrence (e.g.\ when printed at
  1858   the toplevel). Interrupt counts as neutral element here: it is treated as
  1859   minimal information about some canceled evaluation process, and is absorbed
  1860   by the presence of regular program exceptions.
  1861 \<close>
  1862 
  1863 text %mlref \<open>
  1864   \begin{mldecls}
  1865   @{index_ML_type "'a Exn.result"} \\
  1866   @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
  1867   @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
  1868   @{index_ML Exn.release: "'a Exn.result -> 'a"} \\
  1869   @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
  1870   @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
  1871   \end{mldecls}
  1872 
  1873   \<^descr> Type @{ML_type "'a Exn.result"} represents the disjoint sum of ML results
  1874   explicitly, with constructor @{ML Exn.Res} for regular values and @{ML
  1875   "Exn.Exn"} for exceptions.
  1876 
  1877   \<^descr> @{ML Exn.capture}~\<open>f x\<close> manages the evaluation of \<open>f x\<close> such that
  1878   exceptions are made explicit as @{ML "Exn.Exn"}. Note that this includes
  1879   physical interrupts (see also \secref{sec:exceptions}), so the same
  1880   precautions apply to user code: interrupts must not be absorbed
  1881   accidentally!
  1882 
  1883   \<^descr> @{ML Exn.interruptible_capture} is similar to @{ML Exn.capture}, but
  1884   interrupts are immediately re-raised as required for user code.
  1885 
  1886   \<^descr> @{ML Exn.release}~\<open>result\<close> releases the original runtime result, exposing
  1887   its regular value or raising the reified exception.
  1888 
  1889   \<^descr> @{ML Par_Exn.release_all}~\<open>results\<close> combines results that were produced
  1890   independently (e.g.\ by parallel evaluation). If all results are regular
  1891   values, that list is returned. Otherwise, the collection of all exceptions
  1892   is raised, wrapped-up as collective parallel exception. Note that the latter
  1893   prevents access to individual exceptions by conventional \<^verbatim>\<open>handle\<close> of ML.
  1894 
  1895   \<^descr> @{ML Par_Exn.release_first} is similar to @{ML Par_Exn.release_all}, but
  1896   only the first (meaningful) exception that has occurred in the original
  1897   evaluation process is raised again, the others are ignored. That single
  1898   exception may get handled by conventional means in ML.
  1899 \<close>
  1900 
  1901 
  1902 subsection \<open>Parallel skeletons \label{sec:parlist}\<close>
  1903 
  1904 text \<open>
  1905   Algorithmic skeletons are combinators that operate on lists in parallel, in
  1906   the manner of well-known \<open>map\<close>, \<open>exists\<close>, \<open>forall\<close> etc. Management of
  1907   futures (\secref{sec:futures}) and their results as reified exceptions is
  1908   wrapped up into simple programming interfaces that resemble the sequential
  1909   versions.
  1910 
  1911   What remains is the application-specific problem to present expressions with
  1912   suitable \<^emph>\<open>granularity\<close>: each list element corresponds to one evaluation
  1913   task. If the granularity is too coarse, the available CPUs are not
  1914   saturated. If it is too fine-grained, CPU cycles are wasted due to the
  1915   overhead of organizing parallel processing. In the worst case, parallel
  1916   performance will be less than the sequential counterpart!
  1917 \<close>
  1918 
  1919 text %mlref \<open>
  1920   \begin{mldecls}
  1921   @{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\
  1922   @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
  1923   \end{mldecls}
  1924 
  1925   \<^descr> @{ML Par_List.map}~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> is like @{ML "map"}~\<open>f [x\<^sub>1, \<dots>,
  1926   x\<^sub>n]\<close>, but the evaluation of \<open>f x\<^sub>i\<close> for \<open>i = 1, \<dots>, n\<close> is performed in
  1927   parallel.
  1928 
  1929   An exception in any \<open>f x\<^sub>i\<close> cancels the overall evaluation process. The
  1930   final result is produced via @{ML Par_Exn.release_first} as explained above,
  1931   which means the first program exception that happened to occur in the
  1932   parallel evaluation is propagated, and all other failures are ignored.
  1933 
  1934   \<^descr> @{ML Par_List.get_some}~\<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> produces some \<open>f x\<^sub>i\<close> that is of
  1935   the form \<open>SOME y\<^sub>i\<close>, if that exists, otherwise \<open>NONE\<close>. Thus it is similar to
  1936   @{ML Library.get_first}, but subject to a non-deterministic parallel choice
  1937   process. The first successful result cancels the overall evaluation process;
  1938   other exceptions are propagated as for @{ML Par_List.map}.
  1939 
  1940   This generic parallel choice combinator is the basis for derived forms, such
  1941   as @{ML Par_List.find_some}, @{ML Par_List.exists}, @{ML Par_List.forall}.
  1942 \<close>
  1943 
  1944 text %mlex \<open>
  1945   Subsequently, the Ackermann function is evaluated in parallel for some
  1946   ranges of arguments.
  1947 \<close>
  1948 
  1949 ML_val \<open>
  1950   fun ackermann 0 n = n + 1
  1951     | ackermann m 0 = ackermann (m - 1) 1
  1952     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1));
  1953 
  1954   Par_List.map (ackermann 2) (500 upto 1000);
  1955   Par_List.map (ackermann 3) (5 upto 10);
  1956 \<close>
  1957 
  1958 
  1959 subsection \<open>Lazy evaluation\<close>
  1960 
  1961 text \<open>
  1962   Classic lazy evaluation works via the \<open>lazy\<close>~/ \<open>force\<close> pair of operations:
  1963   \<open>lazy\<close> to wrap an unevaluated expression, and \<open>force\<close> to evaluate it once
  1964   and store its result persistently. Later invocations of \<open>force\<close> retrieve the
  1965   stored result without another evaluation. Isabelle/ML refines this idea to
  1966   accommodate the aspects of multi-threading, synchronous program exceptions
  1967   and asynchronous interrupts.
  1968 
  1969   The first thread that invokes \<open>force\<close> on an unfinished lazy value changes
  1970   its state into a \<^emph>\<open>promise\<close> of the eventual result and starts evaluating it.
  1971   Any other threads that \<open>force\<close> the same lazy value in the meantime need to
  1972   wait for it to finish, by producing a regular result or program exception.
  1973   If the evaluation attempt is interrupted, this event is propagated to all
  1974   waiting threads and the lazy value is reset to its original state.
  1975 
  1976   This means a lazy value is completely evaluated at most once, in a
  1977   thread-safe manner. There might be multiple interrupted evaluation attempts,
  1978   and multiple receivers of intermediate interrupt events. Interrupts are
  1979   \<^emph>\<open>not\<close> made persistent: later evaluation attempts start again from the
  1980   original expression.
  1981 \<close>
  1982 
  1983 text %mlref \<open>
  1984   \begin{mldecls}
  1985   @{index_ML_type "'a lazy"} \\
  1986   @{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
  1987   @{index_ML Lazy.value: "'a -> 'a lazy"} \\
  1988   @{index_ML Lazy.force: "'a lazy -> 'a"} \\
  1989   \end{mldecls}
  1990 
  1991   \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type \<^verbatim>\<open>'a\<close>.
  1992 
  1993   \<^descr> @{ML Lazy.lazy}~\<open>(fn () => e)\<close> wraps the unevaluated expression \<open>e\<close> as
  1994   unfinished lazy value.
  1995 
  1996   \<^descr> @{ML Lazy.value}~\<open>a\<close> wraps the value \<open>a\<close> as finished lazy value. When
  1997   forced, it returns \<open>a\<close> without any further evaluation.
  1998 
  1999   There is very low overhead for this proforma wrapping of strict values as
  2000   lazy values.
  2001 
  2002   \<^descr> @{ML Lazy.force}~\<open>x\<close> produces the result of the lazy value in a
  2003   thread-safe manner as explained above. Thus it may cause the current thread
  2004   to wait on a pending evaluation attempt by another thread.
  2005 \<close>
  2006 
  2007 
  2008 subsection \<open>Futures \label{sec:futures}\<close>
  2009 
  2010 text \<open>
  2011   Futures help to organize parallel execution in a value-oriented manner, with
  2012   \<open>fork\<close>~/ \<open>join\<close> as the main pair of operations, and some further variants;
  2013   see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy values,
  2014   futures are evaluated strictly and spontaneously on separate worker threads.
  2015   Futures may be canceled, which leads to interrupts on running evaluation
  2016   attempts, and forces structurally related futures to fail for all time;
  2017   already finished futures remain unchanged. Exceptions between related
  2018   futures are propagated as well, and turned into parallel exceptions (see
  2019   above).
  2020 
  2021   Technically, a future is a single-assignment variable together with a
  2022   \<^emph>\<open>task\<close> that serves administrative purposes, notably within the \<^emph>\<open>task
  2023   queue\<close> where new futures are registered for eventual evaluation and the
  2024   worker threads retrieve their work.
  2025 
  2026   The pool of worker threads is limited, in correlation with the number of
  2027   physical cores on the machine. Note that allocation of runtime resources may
  2028   be distorted either if workers yield CPU time (e.g.\ via system sleep or
  2029   wait operations), or if non-worker threads contend for significant runtime
  2030   resources independently. There is a limited number of replacement worker
  2031   threads that get activated in certain explicit wait conditions, after a
  2032   timeout.
  2033 
  2034   \<^medskip>
  2035   Each future task belongs to some \<^emph>\<open>task group\<close>, which represents the
  2036   hierarchic structure of related tasks, together with the exception status a
  2037   that point. By default, the task group of a newly created future is a new
  2038   sub-group of the presently running one, but it is also possible to indicate
  2039   different group layouts under program control.
  2040 
  2041   Cancellation of futures actually refers to the corresponding task group and
  2042   all its sub-groups. Thus interrupts are propagated down the group hierarchy.
  2043   Regular program exceptions are treated likewise: failure of the evaluation
  2044   of some future task affects its own group and all sub-groups. Given a
  2045   particular task group, its \<^emph>\<open>group status\<close> cumulates all relevant exceptions
  2046   according to its position within the group hierarchy. Interrupted tasks that
  2047   lack regular result information, will pick up parallel exceptions from the
  2048   cumulative group status.
  2049 
  2050   \<^medskip>
  2051   A \<^emph>\<open>passive future\<close> or \<^emph>\<open>promise\<close> is a future with slightly different
  2052   evaluation policies: there is only a single-assignment variable and some
  2053   expression to evaluate for the \<^emph>\<open>failed\<close> case (e.g.\ to clean up resources
  2054   when canceled). A regular result is produced by external means, using a
  2055   separate \<^emph>\<open>fulfill\<close> operation.
  2056 
  2057   Promises are managed in the same task queue, so regular futures may depend
  2058   on them. This allows a form of reactive programming, where some promises are
  2059   used as minimal elements (or guards) within the future dependency graph:
  2060   when these promises are fulfilled the evaluation of subsequent futures
  2061   starts spontaneously, according to their own inter-dependencies.
  2062 \<close>
  2063 
  2064 text %mlref \<open>
  2065   \begin{mldecls}
  2066   @{index_ML_type "'a future"} \\
  2067   @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
  2068   @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
  2069   @{index_ML Future.join: "'a future -> 'a"} \\
  2070   @{index_ML Future.joins: "'a future list -> 'a list"} \\
  2071   @{index_ML Future.value: "'a -> 'a future"} \\
  2072   @{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\
  2073   @{index_ML Future.cancel: "'a future -> unit"} \\
  2074   @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
  2075   @{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\
  2076   @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
  2077   \end{mldecls}
  2078 
  2079   \<^descr> Type @{ML_type "'a future"} represents future values over type \<^verbatim>\<open>'a\<close>.
  2080 
  2081   \<^descr> @{ML Future.fork}~\<open>(fn () => e)\<close> registers the unevaluated expression \<open>e\<close>
  2082   as unfinished future value, to be evaluated eventually on the parallel
  2083   worker-thread farm. This is a shorthand for @{ML Future.forks} below, with
  2084   default parameters and a single expression.
  2085 
  2086   \<^descr> @{ML Future.forks}~\<open>params exprs\<close> is the general interface to fork several
  2087   futures simultaneously. The \<open>params\<close> consist of the following fields:
  2088 
  2089     \<^item> \<open>name : string\<close> (default @{ML "\"\""}) specifies a common name for the
  2090     tasks of the forked futures, which serves diagnostic purposes.
  2091 
  2092     \<^item> \<open>group : Future.group option\<close> (default @{ML NONE}) specifies an optional
  2093     task group for the forked futures. @{ML NONE} means that a new sub-group
  2094     of the current worker-thread task context is created. If this is not a
  2095     worker thread, the group will be a new root in the group hierarchy.
  2096 
  2097     \<^item> \<open>deps : Future.task list\<close> (default @{ML "[]"}) specifies dependencies on
  2098     other future tasks, i.e.\ the adjacency relation in the global task queue.
  2099     Dependencies on already finished tasks are ignored.
  2100 
  2101     \<^item> \<open>pri : int\<close> (default @{ML 0}) specifies a priority within the task
  2102     queue.
  2103 
  2104     Typically there is only little deviation from the default priority @{ML
  2105     0}. As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means
  2106     ``high priority''.
  2107 
  2108     Note that the task priority only affects the position in the queue, not
  2109     the thread priority. When a worker thread picks up a task for processing,
  2110     it runs with the normal thread priority to the end (or until canceled).
  2111     Higher priority tasks that are queued later need to wait until this (or
  2112     another) worker thread becomes free again.
  2113 
  2114     \<^item> \<open>interrupts : bool\<close> (default @{ML true}) tells whether the worker thread
  2115     that processes the corresponding task is initially put into interruptible
  2116     state. This state may change again while running, by modifying the thread
  2117     attributes.
  2118 
  2119     With interrupts disabled, a running future task cannot be canceled. It is
  2120     the responsibility of the programmer that this special state is retained
  2121     only briefly.
  2122 
  2123   \<^descr> @{ML Future.join}~\<open>x\<close> retrieves the value of an already finished future,
  2124   which may lead to an exception, according to the result of its previous
  2125   evaluation.
  2126 
  2127   For an unfinished future there are several cases depending on the role of
  2128   the current thread and the status of the future. A non-worker thread waits
  2129   passively until the future is eventually evaluated. A worker thread
  2130   temporarily changes its task context and takes over the responsibility to
  2131   evaluate the future expression on the spot. The latter is done in a
  2132   thread-safe manner: other threads that intend to join the same future need
  2133   to wait until the ongoing evaluation is finished.
  2134 
  2135   Note that excessive use of dynamic dependencies of futures by adhoc joining
  2136   may lead to bad utilization of CPU cores, due to threads waiting on other
  2137   threads to finish required futures. The future task farm has a limited
  2138   amount of replacement threads that continue working on unrelated tasks after
  2139   some timeout.
  2140 
  2141   Whenever possible, static dependencies of futures should be specified
  2142   explicitly when forked (see \<open>deps\<close> above). Thus the evaluation can work from
  2143   the bottom up, without join conflicts and wait states.
  2144 
  2145   \<^descr> @{ML Future.joins}~\<open>xs\<close> joins the given list of futures simultaneously,
  2146   which is more efficient than @{ML "map Future.join"}~\<open>xs\<close>.
  2147 
  2148   Based on the dependency graph of tasks, the current thread takes over the
  2149   responsibility to evaluate future expressions that are required for the main
  2150   result, working from the bottom up. Waiting on future results that are
  2151   presently evaluated on other threads only happens as last resort, when no
  2152   other unfinished futures are left over.
  2153 
  2154   \<^descr> @{ML Future.value}~\<open>a\<close> wraps the value \<open>a\<close> as finished future value,
  2155   bypassing the worker-thread farm. When joined, it returns \<open>a\<close> without any
  2156   further evaluation.
  2157 
  2158   There is very low overhead for this proforma wrapping of strict values as
  2159   futures.
  2160 
  2161   \<^descr> @{ML Future.map}~\<open>f x\<close> is a fast-path implementation of @{ML
  2162   Future.fork}~\<open>(fn () => f (\<close>@{ML Future.join}~\<open>x))\<close>, which avoids the full
  2163   overhead of the task queue and worker-thread farm as far as possible. The
  2164   function \<open>f\<close> is supposed to be some trivial post-processing or projection of
  2165   the future result.
  2166 
  2167   \<^descr> @{ML Future.cancel}~\<open>x\<close> cancels the task group of the given future, using
  2168   @{ML Future.cancel_group} below.
  2169 
  2170   \<^descr> @{ML Future.cancel_group}~\<open>group\<close> cancels all tasks of the given task
  2171   group for all time. Threads that are presently processing a task of the
  2172   given group are interrupted: it may take some time until they are actually
  2173   terminated. Tasks that are queued but not yet processed are dequeued and
  2174   forced into interrupted state. Since the task group is itself invalidated,
  2175   any further attempt to fork a future that belongs to it will yield a
  2176   canceled result as well.
  2177 
  2178   \<^descr> @{ML Future.promise}~\<open>abort\<close> registers a passive future with the given
  2179   \<open>abort\<close> operation: it is invoked when the future task group is canceled.
  2180 
  2181   \<^descr> @{ML Future.fulfill}~\<open>x a\<close> finishes the passive future \<open>x\<close> by the given
  2182   value \<open>a\<close>. If the promise has already been canceled, the attempt to fulfill
  2183   it causes an exception.
  2184 \<close>
  2185 
  2186 end