
diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -57,7 +57,7 @@
 *}
 
 ML %gray {* 
-  val r = ref 0
+  val r = Unsynchronized.ref 0
   fun f n = n + 1 
 *}
 
@@ -274,7 +274,7 @@
   @{text "?Q"} and so on. They are needed in order to able to
   instantiate theorems when they are applied. For example the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
-  instantiation of @{text "?P"} and @{text "?Q"} 
+  instantiation of @{text "?P"} and @{text "?Q"}. 
 
   @{ML_response_fake [display, gray]
   "tracing (string_of_thm @{context} @{thm conjI})"
@@ -844,7 +844,7 @@
   \end{readmore}
 *}
 
-section {* Storing Data in Isabelle *}
+section {* Storing Data in Isabelle\label{sec:storing} *}
 
 text {*
   Isabelle provides mechanisms for storing (and retrieving) arbitrary
@@ -914,18 +914,20 @@
   This runtime error is the reason why ML is still type-sound despite
   containing a universal type.
 
-  Now, Isabelle heavily uses this mechanism to store all sorts of data: theorem lists,
-  simpsets, facts etc.  Roughly speaking, there are two places where data can 
-  be stored: in \emph{theories} and in \emph{proof contexts}. Again
-  roughly speaking, data such as simpsets need to be stored in a theory,
-  since they need to be maintained across proofs and even theories.
-  On the other hands, data such as facts change inside a proof and
-  therefore need to be maintained inside a proof 
-  context.\footnote{\bf TODO: explain more bout this.} 
+  Now, Isabelle heavily uses this mechanism for storing all sorts of
+  data: theorem lists, simpsets, facts etc.  Roughly speaking, there are two
+  places where data can be stored: in \emph{theories} and in \emph{proof
+  contexts}. Again roughly speaking, data such as simpsets need to be stored
+  in a theory, since they need to be maintained across proofs and even across
+  theories.  On the other hand, data such as facts change inside a proof and
+  are only relevant to the proof at hand. Therefore such data needs to be 
+  maintained inside a proof context.\footnote{\bf TODO: explain more about 
+  this in a separate section.}
 
-  For both theories and proof contexts there are convenient functors that help
+  For theories and proof contexts there are, respectively, the functors 
+  @{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help
   with the data storage. Below we show how to implement a table in which we
-  can store theorems that can be looked up according to a string key. The
+  can store theorems and look them up according to a string key. The
   intention is to be able to look up introduction rules for logical
   connectives. Such a table might be useful in an automatic proof procedure
   and therefore it makes sense to store this data inside a theory.  The code
@@ -949,9 +951,9 @@
   roughly to the operations performed on theories.\footnote{\bf FIXME: Say more
   about the assumptions of these operations.} The result structure @{ML_text Data}
   contains functions for accessing the table (@{ML Data.get}) and for updating
-  it (@{ML Data.map}). There are also two more functions, which however we
-  ignore here. Below we define two auxiliary functions, which help us with
-  accessing the table.
+  it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and 
+  @{ML Data.put}), which however we ignore here. Below we define two auxiliary 
+  functions, which help us with accessing the table.
 *}
 
 ML{*val lookup = Symtab.lookup o Data.get
@@ -969,8 +971,9 @@
 *}
 
 text {*
-  The use of \isacommand{setup} makes sure the table in the current theory 
-  is updated. The lookup can now be performed as follows.
+  The use of the command \isacommand{setup} makes sure the table in the 
+  \emph{current} theory is updated. The lookup can now be performed as 
+  follows.
 
   @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
@@ -984,78 +987,87 @@
 setup %gray {* update "op &" @{thm TrueI} *}
 
 text {*
-  and lookup now produces the introduction rule for @{term "True"}
+  and @{ML lookup} now produces the introduction rule for @{term "True"}
   
 @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
 "SOME \"True\""}
 
   there are no references involved. This is one of the most fundamental
-  coding conventions for programming in Isabelle. References would interfere
-  with the multithreaded execution model of Isabelle.\footnote{\bf FIXME: say more}
-  
-  \begin{readmore}
-  Isabelle contains implementations of several container data structures,
-  including association lists in @{ML_file "Pure/General/alist.ML"},
-  tables and symtables in @{ML_file "Pure/General/table.ML"}, and
-  directed graphs in @{ML_file "Pure/General/graph.ML"}.
-  \end{readmore}
-
-  Storing data in a proof context is similar. With the following code we
-  can store a list of terms in a proof context. 
+  coding conventions for programming in Isabelle. References would 
+  interfere with the multithreaded execution model of Isabelle and also
+  defeat the undo-mechanism in proof scripts. For this consider the 
+  following data container where we maintain a reference to a list of 
+  integers.
 *}
 
-ML{*structure Data = ProofDataFun
-  (type T = term list
-   val init = (K []))*}
+ML{*structure WrongRefData = TheoryDataFun
+  (type T = (int list) Unsynchronized.ref
+   val empty = Unsynchronized.ref []
+   val copy = I
+   val extend = I
+   fun merge _ = fst)*}
 
 text {*
-  The function we have to specify has to produce a list once a context 
-  is initialised (taking the theory into account from which the 
-  context is derived). We choose to just return the empty list. Next 
-  we define two auxiliary functions for updating the list with a given
-  term and printing the list. 
+  We initialise the reference with the empty list. Consequently a first 
+  lookup produces @{ML "ref []" in Unsynchronized}.
+
+  @{ML_response_fake [display,gray]
+  "WrongRefData.get @{theory}"
+  "ref []"}
+
+  For updating the reference we use the following function.
+*}
+
+ML{*fun ref_update n = WrongRefData.map 
+      (fn r => let val _ = r := n::(!r) in r end)*}
+
+text {*
+  As above we update the reference with the command 
+  \isacommand{setup}. 
 *}
 
-ML{*fun update trm = Data.map (fn xs => trm::xs)
-
-fun print ctxt =
-  case (Data.get ctxt) of
-    [] => tracing "Empty!"
-  | xs => tracing (string_of_terms ctxt xs)*}
+setup %gray{* ref_update 1 *}
 
 text {*
-  Next we start with the context given by @{text "@{context}"} and 
-  update it in various ways. 
+  A lookup in the current theory gives then the expected list 
+  @{ML "ref [1]" in Unsynchronized}.
+
+  @{ML_response_fake [display,gray]
+  "WrongRefData.get @{theory}"
+  "ref [1]"}
+
+  So far everything is as expected. But, the trouble starts if we attempt
+  to backtrack to ``before'' the \isacommand{setup}-command. There, we 
+  would expect that the list is empty again. But since it is stored in 
+  a reference, Isabelle has no control over it. So it is not
+  empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, 
+  if we execute the \isacommand{setup}-command again, we do not obtain 
+  @{ML "ref [1]" in Unsynchronized}, but
 
   @{ML_response_fake [display,gray]
-"let
-  val ctxt    = @{context}
-  val ctxt'   = ctxt   |> update @{term \"False\"}
-                       |> update @{term \"True \<and> True\"} 
-  val ctxt''  = ctxt   |> update @{term \"1::nat\"}
-  val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
-in
-  print ctxt; 
-  print ctxt';
-  print ctxt'';
-  print ctxt'''
-end"
-"Empty!
-True \<and> True, False
-1
-2, 1"}
+  "WrongRefData.get @{theory}"
+  "ref [1, 1]"}
+
+  Now imagine how often you go backwards and forwards in your proof scripts. 
+  By using references in Isabelle code, you are bound to cause all
+  hell to break lose. Therefore observe the coding convention: 
+  Do not use references for storing data!
 
-  Many functions in Isabelle manage and update data in a similar
-  fashion. Consequently, such calculation with contexts occur frequently in
-  Isabelle code, although the ``context flow'' is usually only linear.
+  \begin{readmore}
+  The functors for data storage are defined in @{ML_file "Pure/context.ML"}.
+  Isabelle contains implementations of several container data structures,
+  including association lists in @{ML_file "Pure/General/alist.ML"},
+  directed graphs in @{ML_file "Pure/General/graph.ML"}. and 
+  tables and symtables in @{ML_file "Pure/General/table.ML"}.
+  \end{readmore}
 
-  A special instance of the mechanisms described above are configuration
-  values. They are used to in order to configure tools by the user without
-  having to resort to the ML-level. Assume you want the user to control three
-  values, say @{text bval} containing a boolean, @{text ival} containing an
-  integer and @{text sval} containing a string. These values can be declared
-  by
+  A special instance of the data storage mechanism described above are
+  configuration values. They are used to enable users to configure tools
+  without having to resort to the ML-level (and also to avoid
+  references). Assume you want the user to control three values, say @{text
+  bval} containing a boolean, @{text ival} containing an integer and @{text
+  sval} containing a string. These values can be declared by
 *}
 
 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
@@ -1081,7 +1093,7 @@
 
 text {*
   On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}:
+  function @{ML Config.get}.
 
   @{ML_response [display,gray] "Config.get @{context} bval" "true"}
 
@@ -1089,6 +1101,61 @@
   For more information about configuration values see 
   @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
   \end{readmore}
+
+  Storing data in a proof context is done in a similar fashion. The
+  corresponding functor is @{ML_funct_ind ProofDataFun}. With the 
+  following code we can store a list of terms in a proof context. 
+*}
+
+ML{*structure Data = ProofDataFun
+  (type T = term list
+   fun init _ = [])*}
+
+text {*
+  The function we have to specify has to produce a list once a context 
+  is initialised (taking the theory into account from which the 
+  context is derived). We choose to just return the empty list. Next 
+  we define two auxiliary functions for updating the list with a given
+  term and printing the list. 
+*}
+
+ML{*fun update trm = Data.map (fn xs => trm::xs)
+
+fun print ctxt =
+  case (Data.get ctxt) of
+    [] => tracing "Empty!"
+  | xs => tracing (string_of_terms ctxt xs)*}
+
+text {*
+  Next we start with the context given by the antiquotation 
+  @{text "@{context}"} and update it in various ways. 
+
+  @{ML_response_fake [display,gray]
+"let
+  val ctxt    = @{context}
+  val ctxt'   = ctxt   |> update @{term \"False\"}
+                       |> update @{term \"True \<and> True\"} 
+  val ctxt''  = ctxt   |> update @{term \"1::nat\"}
+  val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
+in
+  print ctxt; 
+  print ctxt';
+  print ctxt'';
+  print ctxt'''
+end"
+"Empty!
+True \<and> True, False
+1
+2, 1"}
+
+  Many functions in Isabelle manage and update data in a similar
+  fashion. Consequently, such calculation with contexts occur frequently in
+  Isabelle code, although the ``context flow'' is usually only linear.
+  Note also that the calculation above has no effect on the underlying
+  theory. Once we throw away the contexts, we have no access to their
+  associated data. This is different to theories, where the command 
+  \isacommand{setup} registers the data with the current and future 
+  theories, and therefore can access the data potentially indefinitely. 
 *}
 
 




