diff -r f76135c6c527 -r ce754ad78bc9 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Oct 01 10:19:21 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Fri Oct 02 15:38:14 2009 +0200 @@ -187,8 +187,8 @@ be displayed by the infrastructure. - (FIXME Mention how to work with @{ML_ind debug in Toplevel} and - @{ML_ind profiling in Toplevel}.) + \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and + @{ML_ind profiling in Toplevel}.} *} (* FIXME @@ -610,7 +610,7 @@ "acc_incs 1 ||>> (fn x => (x, x + 2))" "(((((\"\", 1), 2), 3), 4), 6)"} - (FIXME: maybe give a ``real world'' example for this combinator) + \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.} *} text {* @@ -678,9 +678,9 @@ contains further information about combinators. \end{readmore} - (FIXME: find a good exercise for combinators) + \footnote{\bf FIXME: find a good exercise for combinators} - (FIXME: say something about calling conventions) + \footnote{\bf FIXME: say something about calling conventions} *} @@ -798,9 +798,9 @@ @{text "> "}~@{thm TrueConj_def} \end{isabelle} - (FIXME give a better example why bindings are important; maybe + \footnote{\bf FIXME give a better example why bindings are important; maybe give a pointer to \isacommand{local\_setup}; if not, then explain - why @{ML snd} is needed) + why @{ML snd} is needed.} It is also possible to define your own antiquotations. But you should exercise care when introducing new ones, as they can also make your code @@ -844,20 +844,32 @@ \end{readmore} *} -section {* Storing Data in Isabelle (TBD) *} +section {* Storing Data in Isabelle *} text {* - Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we - explain them, let us digress: Convenitional wisdom has it that - ML's type-system ensures that for example an @{ML_type "'a list"} can only - hold elements of the same type, namely @{ML_type "'a"}. Still, by some arguably - accidental features of ML, one can implement a universal type. In Isabelle it - is implemented as @{ML_type Universal.universal}. This type allows one to - inject and project elements of different type into for example into a list. - We will show this by storing an integer and boolean in a list. What is important - that access to the data is done in a type-safe manner. + Isabelle provides mechanisms for storing (and retrieving) arbitrary + data. Before we delve into the details, let us digress a bit. Conventional + wisdom has it that the type-system of ML ensures that for example an + @{ML_type "'a list"} can only hold elements of the same type, namely + @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a + universal type in ML, although by some arguably accidental features of ML. + This universal type can be used to store data of different type into a single list. + It allows one to inject and to project data of \emph{arbitrary} type. This is + in contrast to datatypes, which only allow injection and projection of data for + some fixed collection of types. In light of the conventional wisdom cited + above it is important to keep in mind that the universal type does not + destroy type-safety of ML: storing and accessing the data can only be done + in a type-safe manner. - Let us first define projection and injection functions for booleans and integers. + \begin{readmore} + In Isabelle the universal type is implemented as the type @{ML_type + Universal.universal} in the file + @{ML_file "Pure/ML-Systems/universal.ML"}. + \end{readmore} + + We will show the usage of the universal type by storing an integer and + a boolean into a single list. Let us first define injection and projection + functions for booleans and integers into and from @{ML_type Universal.universal}. *} ML{*local @@ -871,34 +883,216 @@ end*} text {* - We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as - its two elements. -*} - -ML{* val list = [inject_int 13, inject_bool true]*} - -ML {* - project_int (nth list 0) + Using the injection functions, we can inject the integer @{ML_text "13"} + and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and + then store them in a @{ML_type "Universal.universal list"} as follows: *} -ML {* - project_bool (nth list 1) +ML{*val foo_list = +let + val thirteen = inject_int 13 + val truth_val = inject_bool true +in + [thirteen, truth_val] +end*} + +text {* + The data can be retrieved using the projection functions. + + @{ML_response [display, gray] +"(project_int (nth foo_list 0), project_bool (nth foo_list 1))" +"(13, true)"} + + Notice that we access the integer as an integer and the boolean as + a boolean. If we attempt to access the integer as a boolean, then we get + a runtime error. + + @{ML_response_fake [display, gray] +"project_bool (nth foo_list 0)" +"*** Exception- Match raised"} + + 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.} + + For both theories and proof contexts there are convenient functors 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 + 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 + for the table is: *} -ML {* - Context.the_thread_data (); - Context.display_names @{theory}; - Context.pretty_thy @{theory} - |> Pretty.string_of - |> tracing +ML %linenosgray{*structure Data = TheoryDataFun + (type T = thm Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true))*} + +text {* + In order to store data in a theory, we have to specify the type of the data + (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which + stands for tables in which @{ML_type string}s can be looked up producing an associated + @{ML_type thm}. We also have to specify four functions: how to initialise + the data storage (Line 3), how to copy it (Line 4), how to extend it (Line + 5) and how two tables should be merged (Line 6). These functions correspond + 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. +*} + +ML{*val lookup = Symtab.lookup o Data.get +fun update k v = Data.map (Symtab.update (k, v))*} + +text {* + Since we want to store introduction rules associated with their + logical connective, we can fill the table as follows. +*} + +setup %gray {* + update "op &" @{thm conjI} #> + update "op -->" @{thm impI} #> + update "All" @{thm allI} *} text {* + The use of \isacommand{setup} makes sure the table in the current theory + is updated. The lookup can now be performed as follows. + + @{ML_response_fake [display, gray] +"lookup @{theory} \"op &\"" +"SOME \"\?P; ?Q\ \ ?P \ ?Q\""} + + An important point to note is that these tables (and data in general) + need to be treated in a purely functional fashion. Although + we can update the table as follows +*} + +setup %gray {* update "op &" @{thm TrueI} *} + +text {* + and 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} - @{ML_file "Pure/ML-Systems/universal.ML"} + 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. +*} + +ML{*structure Data = ProofDataFun + (type T = term list + val init = (K []))*} + +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 @{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. + + 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 +*} + +ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false +val (ival, setup_ival) = Attrib.config_int "ival" 0 +val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} + +text {* + where each value needs to be given a default. To enable these values, they need to + be set up with +*} + +setup %gray {* + setup_bval #> + setup_ival +*} + +text {* + The user can now manipulate the values from the user-level of Isabelle + with the command +*} + +declare [[bval = true, ival = 3]] + +text {* + On the ML-level these values can be retrieved using the + function @{ML Config.get}: + + @{ML_response [display,gray] "Config.get @{context} bval" "true"} + + \begin{readmore} + For more information about configuration values see + @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. \end{readmore} *} + + (**************************************************) (* bak *) (**************************************************)