--- 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 \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?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 \<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.
+
+ 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 *)
(**************************************************)