# HG changeset patch
# User wenzelm
# Date 1371729192 -7200
# Node ID 24018d1167a33e0fb7fe2233684667b3ec144ef4
# Parent  f00e4d8dde4c1d02560133c43a484c2e6cb6c11e
more on managed evaluation;

diff -r f00e4d8dde4c -r 24018d1167a3 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Thu Jun 20 11:27:43 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Thu Jun 20 13:53:12 2013 +0200
@@ -1806,4 +1806,101 @@
   to implement a mailbox as synchronized variable over a purely
   functional queue. *}
 
+
+section {* Managed evaluation *}
+
+text {* Execution of Standard ML follows the model of strict
+  functional evaluation with optional exceptions.  Evaluation happens
+  whenever some function is applied to (sufficiently many)
+  arguments. The result is either an explicit value or an implicit
+  exception.
+
+  \emph{Managed evaluation} in Isabelle/ML organizes expressions and
+  results to control certain physical side-conditions, to say more
+  specifically when and how evaluation happens.  For example, the
+  Isabelle/ML library supports lazy evaluation with memoing, parallel
+  evaluation via futures, asynchronous evaluation via promises,
+  evaluation with time limit etc.
+
+  \medskip An \emph{unevaluated expression} is represented either as
+  unit abstraction @{verbatim "fn () => a"} of type
+  @{verbatim "unit -> 'a"} or as regular function
+  @{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}.  Both forms
+  occur routinely, and special care is required to tell them apart ---
+  the static type-system of SML is only of limited help here.
+
+  The first form is more intuitive: some combinator @{text "(unit ->
+  'a) -> 'a"} applies the given function to @{text "()"} to initiate
+  the postponed evaluation process.  The second form is more flexible:
+  some combinator @{text "('a -> 'b) -> 'a -> 'b"} acts like a
+  modified form of function application; several such combinators may
+  be cascaded to modify a given function, before it is ultimately
+  applied to some argument.
+
+  \medskip \emph{Reified results} make the disjoint sum of regular
+  values versions exceptional situations explicit as ML datatype:
+  @{text "'a result = Res of 'a | Exn of exn"}.  This is typically
+  used for administrative purposes, to store the overall outcome of an
+  evaluation process.
+
+  \emph{Parallel exceptions} aggregate reified results, such that
+  multiple exceptions are digested as a collection in canonical form
+  that identifies exceptions according to their original occurrence.
+  This is particular important for parallel evaluation via futures
+  \secref{sec:futures}, which are organized as acyclic graph of
+  evaluations that depend on other evaluations: exceptions stemming
+  from shared sub-graphs are exposed exactly once and in the order of
+  their original occurrence (e.g.\ when printed at the toplevel).
+  Interrupt counts as neutral element here: it is treated as minimal
+  information about some canceled evaluation process, and is absorbed
+  by the presence of regular program exceptions.  *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type "'a Exn.result"} \\
+  @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
+  @{index_ML Exn.release: "'a Exn.result -> 'a"} \\
+  @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
+  @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
+
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type @{ML_type "'a Exn.result"} represents the disjoint sum of
+  ML results explicitly, with constructor @{ML Exn.Res} for regular
+  values and @{ML "Exn.Exn"} for exceptions.
+
+  \item @{ML Exn.capture}~@{text "f x"} manages the evaluation of
+  @{text "f x"} such that exceptions are made explicit as @{ML
+  "Exn.Exn"}.  Note that this includes physical interrupts (see also
+  \secref{sec:exceptions}), so the same precautions apply to user
+  code: interrupts must not be absorbed accidentally!
+
+  \item @{ML Exn.interruptible_capture} is similar to @{ML
+  Exn.capture}, but interrupts are immediately re-raised as required
+  for user code.
+
+  \item @{ML Exn.release}~@{text "result"} releases the original
+  runtime result, exposing its regular value or raising the reified
+  exception.
+
+  \item @{ML Par_Exn.release_all}~@{text "results"} combines results
+  that were produced independently (e.g.\ by parallel evaluation).  If
+  all results are regular values, that list is returned.  Otherwise,
+  the collection of all exceptions is raised, wrapped-up as collective
+  parallel exception.  Note that the latter prevents access to
+  individual exceptions by conventional @{verbatim "handle"} of SML.
+
+  \item @{ML Par_Exn.release_first} is similar to @{ML
+  Par_Exn.release_all}, but only the first exception that has occurred
+  in the original evaluation process is raised again, the others are
+  ignored.  That single exception may get handled by conventional
+  means in SML.
+
+  \end{description}
+*}
+
+
 end