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