# HG changeset patch
# User wenzelm
# Date 1286483058 -3600
# Node ID 61e7935a6858db715e4ba7ad30e03efe814bae1e
# Parent  0de42180febe998ec6149b9c92b9c9c2b95ac1d1
more on Isabelle/ML;

diff -r 0de42180febe -r 61e7935a6858 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 07 19:05:42 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 07 21:24:18 2010 +0100
@@ -4,4 +4,126 @@
 
 chapter {* Isabelle/ML *}
 
+text {* Isabelle/ML is best understood as a certain culture based on
+  Standard ML.  Thus it is not a new programming language, but a
+  certain way to use SML at an advanced level within the Isabelle
+  environment.  This covers a variety of aspects that are geared
+  towards an efficient and robust platform for applications of formal
+  logic with fully foundational proof construction --- according to
+  the well-known \emph{LCF principle}.  There are specific library
+  modules and infrastructure to address the needs for such difficult
+  tasks.  For example, the raw parallel programming model of Poly/ML
+  is presented as considerably more abstract concept of \emph{future
+  values}, which is then used to augment the inference kernel, proof
+  interpreter, and theory loader accordingly.
+
+  The main aspects of Isabelle/ML are introduced below.  These
+  first-hand explanations should help to understand how proper
+  Isabelle/ML is to be read and written, and to get access to the
+  wealth of experience that is expressed in the source text and its
+  history of changes.\footnote{See
+  \url{http://isabelle.in.tum.de/repos/isabelle} for the full
+  Mercurial history.  There are symbolic tags to refer to official
+  Isabelle releases, as opposed to arbitrary \emph{tip} versions that
+  merely reflect snapshots that are never really up-to-date.}  *}
+
+
+section {* SML embedded into Isabelle/Isar *}
+
+text {* ML and Isabelle/Isar are intertwined via an open-ended
+  bootstrap process that provides more and more programming facilities
+  and logical content in an alternating manner.  Bootstrapping starts
+  from the raw environment of existing implementations of Standard ML
+  (most notably Poly/ML but also SML/NJ).  Isabelle/Pure marks the
+  point where the original ML toplevel is superseded by the Isar
+  toplevel that maintains a uniform environment for arbitrary ML
+  values (see also \secref{sec:context}).  This formal context holds
+  logical entities as well as ML compiler bindings, among many other
+  things.
+
+  Object-logics, such as Isabelle/HOL, are built within the
+  Isabelle/ML/Isar environment of Pure by introducing suitable
+  theories with associated ML text (either inlined or as separate
+  files).
+
+  Implementing tools within the Isabelle framework means to work with
+  ML within the Isar context in the same manner: raw Standard ML is
+  normally never encountered again.
+*}
+
+section {* Isar ML commands *}
+
+text {* The primary Isar source language provides various facilities
+  to open a ``window'' to the underlying ML compiler.  Especially see
+  @{command_ref "use"} and @{command_ref "ML"} in
+  \cite{isabelle-isar-ref} --- both commands are exactly the same,
+  only the source text is provided via a file vs.\ inlined,
+  respectively.  *}
+
+text %mlex {* The following artificial example demonstrates basic ML
+  programming within the implicit Isar theory context, without
+  referring to logical entities yet.
+*}
+
+ML {*
+  fun factorial 0 = 1
+    | factorial n = n * factorial (n - 1)
+*}
+
+text {* \noindent The ML binding of @{ML factorial} is really managed
+  by the Isabelle environment, i.e.\ that function is not yet
+  accessible in the preceding paragraph, nor in a different theory
+  that is independent from the current one in the import hierarchy.
+
+  Removing the above ML declaration from the source text will remove
+  any trace of this definition as expected.  The Isabelle/ML toplevel
+  environment is managed in a \emph{stateless} way: unlike the raw ML
+  toplevel, there are no global side-effects involved.
+
+  \bigskip The next example shows how to embed ML into Isar proofs.
+  Instead of @{command_ref "ML"} for theory text, we use @{command_ref
+  "ML_prf"}: its effect on the ML environment is local to the whole
+  proof body, while ignoring its internal block structure.  *}
+
+example_proof
+  ML_prf {* val a = 1 *}
+  { -- {* proof block ignored by ML environment *}
+    ML_prf {* val b = a + 1 *}
+  } -- {* proof block ignored by ML environment *}
+  ML_prf {* val c = b + 1 *}
+qed
+
+text {* \noindent By side-stepping the normal Isar scoping rules,
+  embedded ML code can refer to the different contexts explicitly, and
+  manipulate corresponding entities, e.g.\ export a fact from a
+  block context.
+
+  \bigskip The diagnostic ML commands @{command_ref ML_val} and
+  @{command_ref ML_command} do not affect the underlying context, and
+  can be used anywhere, e.g.\ to produce long strings of digits as
+  follows: *}
+
+ML_val {* factorial 100 *}
+ML_command {* writeln (string_of_int (factorial 100)) *}
+
+example_proof
+  ML_val {* factorial 100 *}
+  ML_command {* writeln (string_of_int (factorial 100)) *}
+qed
+
+text {* \noindent Note that @{command ML_val} and @{command
+  ML_command} only differ in the output (or lack thereof) of ML
+  toplevel results. *}
+
+
+section {* Compile-time context *}
+
+text FIXME
+
+
+section {* Antiquotations *}
+
+text FIXME
+
+
 end
\ No newline at end of file