# HG changeset patch # User Christian Urban # Date 1254567699 -7200 # Node ID c0cae24b9d463d87f6d1beac3a2a5d64dcd9e8ec # Parent ce754ad78bc9146d02496ab2d085e5e5b4f1597f updated to new Isabelle; more work on the data section diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/Base.thy Sat Oct 03 13:01:39 2009 +0200 @@ -17,7 +17,7 @@ ML {* (* FIXME ref *) -val file_name = ref (NONE : string option) +val file_name = Unsynchronized.ref (NONE : string option) fun write_file txt = case !file_name of 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. *} diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/General.thy Sat Oct 03 13:01:39 2009 +0200 @@ -1000,7 +1000,7 @@ of theorems. *} -ML{*val my_thms = ref ([] : thm list)*} +ML{*val my_thms = Unsynchronized.ref ([] : thm list)*} text {* The purpose of this reference is to store a list of theorems. diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/Helper/Command/Command.thy Sat Oct 03 13:01:39 2009 +0200 @@ -40,7 +40,7 @@ *} ML {* -val r = ref (NONE:(unit -> term) option) +val r = Unsynchronized.ref (NONE:(unit -> term) option) *} ML{* let diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/Intro.thy Sat Oct 03 13:01:39 2009 +0200 @@ -207,8 +207,9 @@ \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, - \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. - He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. + \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} + and helped with recipe \ref{rec:timing}. Parts of the section \ref{sec:storing} + are by him. \item {\bf Jeremy Dawson} wrote the first version of the chapter about parsing. diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/Parsing.thy Sat Oct 03 13:01:39 2009 +0200 @@ -1089,7 +1089,7 @@ *} -ML_val{*val r = ref (NONE:(unit -> term) option)*} +ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} ML{*let fun after_qed thm_name thms lthy = LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/ROOT.ML --- a/ProgTutorial/ROOT.ML Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/ROOT.ML Sat Oct 03 13:01:39 2009 +0200 @@ -1,4 +1,4 @@ -set quick_and_dirty; +quick_and_dirty := true; no_document use_thy "Base"; no_document use_thy "Package/Simple_Inductive_Package"; diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/Solutions.thy Sat Oct 03 13:01:39 2009 +0200 @@ -273,7 +273,7 @@ ML{*fun term_tree n = let - val count = ref 0; + val count = Unsynchronized.ref 0; fun term_tree_aux n = case n of diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/antiquote_setup.ML Sat Oct 03 13:01:39 2009 +0200 @@ -63,6 +63,13 @@ val output_struct = gen_output_struct (K output) val output_struct_ind = gen_output_struct output_indexed +(* prints functors; no checks *) +fun gen_output_funct outfn {context = ctxt, ...} txt = + (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) + +val output_funct = gen_output_funct (K output) +val output_funct_ind = gen_output_funct output_indexed + (* checks and prints types *) fun gen_output_type outfn {context = ctxt, ...} txt = (eval_fn ctxt (ml_type txt); @@ -95,6 +102,8 @@ val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind +val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct +val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind val _ = ThyOutput.antiquotation "ML_response" two_args output_response val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/output_tutorial.ML --- a/ProgTutorial/output_tutorial.ML Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/output_tutorial.ML Sat Oct 03 13:01:39 2009 +0200 @@ -5,8 +5,8 @@ (* rebuilding the output function from ThyOutput in order to *) (* enable the options [gray, linenos] *) -val gray = ref false -val linenos = ref false +val gray = Unsynchronized.ref false +val linenos = Unsynchronized.ref false fun output txt = diff -r ce754ad78bc9 -r c0cae24b9d46 progtutorial.pdf Binary file progtutorial.pdf has changed