# HG changeset patch
# User wenzelm
# Date 1257710405 -3600
# Node ID a08e6c1cbc049574df6cc7e8205755df01f9a91b
# Parent  96730ad673be1eb3177b90e33fcd1aa66b14e18a
updated functor Theory_Data, Proof_Data, Generic_Data;

diff -r 96730ad673be -r a08e6c1cbc04 NEWS
--- a/NEWS	Sun Nov 08 19:15:37 2009 +0100
+++ b/NEWS	Sun Nov 08 21:00:05 2009 +0100
@@ -236,6 +236,11 @@
 
 *** ML ***
 
+* Theory and context data is now introduced by the simplified and
+modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
+to be pure, but the old TheoryDataFun for mutable data (with explicit
+copy operation) is still available for some time.
+
 * Removed some old-style infix operations using polymorphic equality.
 INCOMPATIBILITY.
 
diff -r 96730ad673be -r a08e6c1cbc04 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Nov 08 19:15:37 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Nov 08 21:00:05 2009 +0100
@@ -177,8 +177,8 @@
   update will result in two related, valid theories.
 
   \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
-  "thy"} that holds a copy of the same data.  The result is not
-  related to the original; the original is unchanged.
+  "thy"} with the same data.  The result is not related to the
+  original; the original is unchanged.
 
   \item @{ML_type theory_ref} represents a sliding reference to an
   always valid theory; updates on the original are propagated
@@ -298,25 +298,18 @@
 
 subsection {* Context data \label{sec:context-data} *}
 
-text {*
-  The main purpose of theory and proof contexts is to manage arbitrary
-  data.  New data types can be declared incrementally at compile time.
-  There are separate declaration mechanisms for any of the three kinds
-  of contexts: theory, proof, generic.
+text {* The main purpose of theory and proof contexts is to manage
+  arbitrary (pure) data.  New data types can be declared incrementally
+  at compile time.  There are separate declaration mechanisms for any
+  of the three kinds of contexts: theory, proof, generic.
 
-  \paragraph{Theory data} may refer to destructive entities, which are
-  maintained in direct correspondence to the linear evolution of
-  theory values, including explicit copies.\footnote{Most existing
-  instances of destructive theory data are merely historical relics
-  (e.g.\ the destructive theorem storage, and destructive hints for
-  the Simplifier and Classical rules).}  A theory data declaration
-  needs to implement the following SML signature:
+  \paragraph{Theory data} declarations need to implement the following
+  SML signature:
 
   \medskip
   \begin{tabular}{ll}
   @{text "\<type> T"} & representing type \\
   @{text "\<val> empty: T"} & empty default value \\
-  @{text "\<val> copy: T \<rightarrow> T"} & refresh impure data \\
   @{text "\<val> extend: T \<rightarrow> T"} & re-initialize on import \\
   @{text "\<val> merge: T \<times> T \<rightarrow> T"} & join on import \\
   \end{tabular}
@@ -324,13 +317,10 @@
 
   \noindent The @{text "empty"} value acts as initial default for
   \emph{any} theory that does not declare actual data content; @{text
-  "copy"} maintains persistent integrity for impure data, it is just
-  the identity for pure values; @{text "extend"} is acts like a
-  unitary version of @{text "merge"}, both operations should also
-  include the functionality of @{text "copy"} for impure data.
+  "extend"} is acts like a unitary version of @{text "merge"}.
 
-  \paragraph{Proof context data} is purely functional.  A declaration
-  needs to implement the following SML signature:
+  \paragraph{Proof context data} declarations need to implement the
+  following SML signature:
 
   \medskip
   \begin{tabular}{ll}
@@ -343,52 +333,48 @@
   value from the given background theory.
 
   \paragraph{Generic data} provides a hybrid interface for both theory
-  and proof data.  The declaration is essentially the same as for
-  (pure) theory data, without @{text "copy"}.  The @{text "init"}
-  operation for proof contexts merely selects the current data value
-  from the background theory.
+  and proof data.  The @{text "init"} operation for proof contexts is
+  predefined to select the current data value from the background
+  theory.
 
   \bigskip A data declaration of type @{text "T"} results in the
   following interface:
 
   \medskip
   \begin{tabular}{ll}
-  @{text "init: theory \<rightarrow> T"} \\
   @{text "get: context \<rightarrow> T"} \\
   @{text "put: T \<rightarrow> context \<rightarrow> context"} \\
   @{text "map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context"} \\
   \end{tabular}
   \medskip
 
-  \noindent Here @{text "init"} is only applicable to impure theory
-  data to install a fresh copy persistently (destructive update on
-  uninitialized has no permanent effect).  The other operations provide
-  access for the particular kind of context (theory, proof, or generic
-  context).  Note that this is a safe interface: there is no other way
-  to access the corresponding data slot of a context.  By keeping
-  these operations private, a component may maintain abstract values
-  authentically, without other components interfering.
+  \noindent These other operations provide access for the particular
+  kind of context (theory, proof, or generic context).  Note that this
+  is a safe interface: there is no other way to access the
+  corresponding data slot of a context.  By keeping these operations
+  private, a component may maintain abstract values authentically,
+  without other components interfering.
 *}
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_functor TheoryDataFun} \\
-  @{index_ML_functor ProofDataFun} \\
-  @{index_ML_functor GenericDataFun} \\
+  @{index_ML_functor Theory_Data} \\
+  @{index_ML_functor Proof_Data} \\
+  @{index_ML_functor Generic_Data} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
+  \item @{ML_functor Theory_Data}@{text "(spec)"} declares data for
   type @{ML_type theory} according to the specification provided as
   argument structure.  The resulting structure provides data init and
   access operations as described above.
 
-  \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous to
-  @{ML_functor TheoryDataFun} for type @{ML_type Proof.context}.
+  \item @{ML_functor Proof_Data}@{text "(spec)"} is analogous to
+  @{ML_functor Theory_Data} for type @{ML_type Proof.context}.
 
-  \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous to
-  @{ML_functor TheoryDataFun} for type @{ML_type Context.generic}.
+  \item @{ML_functor Generic_Data}@{text "(spec)"} is analogous to
+  @{ML_functor Theory_Data} for type @{ML_type Context.generic}.
 
   \end{description}
 *}
diff -r 96730ad673be -r a08e6c1cbc04 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Nov 08 19:15:37 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun Nov 08 21:00:05 2009 +0100
@@ -201,8 +201,8 @@
   stepping stone in the linear development of \isa{thy}.  The next
   update will result in two related, valid theories.
 
-  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The result is not
-  related to the original; the original is unchanged.
+  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data.  The result is not related to the
+  original; the original is unchanged.
 
   \item \verb|theory_ref| represents a sliding reference to an
   always valid theory; updates on the original are propagated
@@ -356,37 +356,28 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The main purpose of theory and proof contexts is to manage arbitrary
-  data.  New data types can be declared incrementally at compile time.
-  There are separate declaration mechanisms for any of the three kinds
-  of contexts: theory, proof, generic.
+The main purpose of theory and proof contexts is to manage
+  arbitrary (pure) data.  New data types can be declared incrementally
+  at compile time.  There are separate declaration mechanisms for any
+  of the three kinds of contexts: theory, proof, generic.
 
-  \paragraph{Theory data} may refer to destructive entities, which are
-  maintained in direct correspondence to the linear evolution of
-  theory values, including explicit copies.\footnote{Most existing
-  instances of destructive theory data are merely historical relics
-  (e.g.\ the destructive theorem storage, and destructive hints for
-  the Simplifier and Classical rules).}  A theory data declaration
-  needs to implement the following SML signature:
+  \paragraph{Theory data} declarations need to implement the following
+  SML signature:
 
   \medskip
   \begin{tabular}{ll}
   \isa{{\isasymtype}\ T} & representing type \\
   \isa{{\isasymval}\ empty{\isacharcolon}\ T} & empty default value \\
-  \isa{{\isasymval}\ copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
   \isa{{\isasymval}\ extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
   \isa{{\isasymval}\ merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
   \end{tabular}
   \medskip
 
   \noindent The \isa{empty} value acts as initial default for
-  \emph{any} theory that does not declare actual data content; \isa{copy} maintains persistent integrity for impure data, it is just
-  the identity for pure values; \isa{extend} is acts like a
-  unitary version of \isa{merge}, both operations should also
-  include the functionality of \isa{copy} for impure data.
+  \emph{any} theory that does not declare actual data content; \isa{extend} is acts like a unitary version of \isa{merge}.
 
-  \paragraph{Proof context data} is purely functional.  A declaration
-  needs to implement the following SML signature:
+  \paragraph{Proof context data} declarations need to implement the
+  following SML signature:
 
   \medskip
   \begin{tabular}{ll}
@@ -399,31 +390,27 @@
   value from the given background theory.
 
   \paragraph{Generic data} provides a hybrid interface for both theory
-  and proof data.  The declaration is essentially the same as for
-  (pure) theory data, without \isa{copy}.  The \isa{init}
-  operation for proof contexts merely selects the current data value
-  from the background theory.
+  and proof data.  The \isa{init} operation for proof contexts is
+  predefined to select the current data value from the background
+  theory.
 
   \bigskip A data declaration of type \isa{T} results in the
   following interface:
 
   \medskip
   \begin{tabular}{ll}
-  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
   \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
   \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
   \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
   \end{tabular}
   \medskip
 
-  \noindent Here \isa{init} is only applicable to impure theory
-  data to install a fresh copy persistently (destructive update on
-  uninitialized has no permanent effect).  The other operations provide
-  access for the particular kind of context (theory, proof, or generic
-  context).  Note that this is a safe interface: there is no other way
-  to access the corresponding data slot of a context.  By keeping
-  these operations private, a component may maintain abstract values
-  authentically, without other components interfering.%
+  \noindent These other operations provide access for the particular
+  kind of context (theory, proof, or generic context).  Note that this
+  is a safe interface: there is no other way to access the
+  corresponding data slot of a context.  By keeping these operations
+  private, a component may maintain abstract values authentically,
+  without other components interfering.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -435,23 +422,23 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML functor}{TheoryDataFun}\verb|functor TheoryDataFun| \\
-  \indexdef{}{ML functor}{ProofDataFun}\verb|functor ProofDataFun| \\
-  \indexdef{}{ML functor}{GenericDataFun}\verb|functor GenericDataFun| \\
+  \indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\
+  \indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\
+  \indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
+  \item \verb|Theory_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
   type \verb|theory| according to the specification provided as
   argument structure.  The resulting structure provides data init and
   access operations as described above.
 
-  \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
-  \verb|TheoryDataFun| for type \verb|Proof.context|.
+  \item \verb|Proof_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
+  \verb|Theory_Data| for type \verb|Proof.context|.
 
-  \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
-  \verb|TheoryDataFun| for type \verb|Context.generic|.
+  \item \verb|Generic_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
+  \verb|Theory_Data| for type \verb|Context.generic|.
 
   \end{description}%
 \end{isamarkuptext}%