--- 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.
*}