
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 \"\<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                                            *)
 (**************************************************)




