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