
diff -r 2b7c08d90e2e -r 92f6a772e013 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Sep 28 01:21:27 2009 +0200
@@ -6,6 +6,17 @@
 chapter {* First Steps *}
 
 text {*
+   \begin{flushright}
+  {\em
+  ``We will most likely never realize the full importance of painting the Tower,\\ 
+  that it is the essential element in the conservation of metal works and the\\ 
+  more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
+  Gustave Eiffel, In The 300-Meter Tower.\footnote{The Eiffel Tower has been 
+  re-painted 18 times since its initial construction, an average of once every 
+  seven years. It takes more than a year for a team of 25 painters to paint the Tower 
+  from top to bottom.}\\[1ex]
+  \end{flushright}
+
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
   Isabelle must be part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
@@ -672,13 +683,23 @@
 *}
 
 
-section {* Antiquotations *}
+section {* ML-Antiquotations *}
 
 text {*
   The main advantage of embedding all code in a theory is that the code can
   contain references to entities defined on the logical level of Isabelle. By
-  this we mean definitions, theorems, terms and so on. This kind of reference is
-  realised with antiquotations, sometimes also referred to as ML-antiquotations.  
+  this we mean definitions, theorems, terms and so on. This kind of reference
+  is realised with ML-antiquotations, often also referred to as just
+  antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
+  which have very different purpose and infrastructures. The first kind,
+  described in this section, are \emph{ML-antiquotations}. They are used to
+  refer to entities (like terms, types etc) from Isabelle's logic layer inside
+  ML-code. The other kind of antiquotations are \emph{document} antiquotations. They
+  are used only in the text parts of Isabelle and their purpose is to print
+  logical entities inside \LaTeX-documents. They are part of the user level
+  and therefore we are not interested in them in this Tutorial, except in
+  Appendix \ref{rec:docantiquotations} where we show how to implement your own
+  document antiquotations.}
   For example, one can print out the name of the current
   theory by typing
 
@@ -782,12 +803,13 @@
 
   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
-  also difficult to read. In the next section we will see how the (build in)
+  also difficult to read. In the next chapter we will see how the (build in)
   antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
   restriction of this antiquotation is that it does not allow you to use
   schematic variables. If you want to have an antiquotation that does not have
-  this restriction, you can implement your own using the function @{ML_ind 
-  ML_Antiquote.inline}. The code is as follows.
+  this restriction, you can implement your own using the function @{ML_ind
+  ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is
+  as follows.
 *}
 
 ML %linenosgray{*ML_Antiquote.inline "term_pat"
@@ -801,35 +823,96 @@
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind  read_term_pattern in
   ProofContext} (Line 4); the next two lines print the term so that the
-  ML-system can understand them. An example of this antiquotation is as
-  follows.
+  ML-system can understand them. The function @{ML atomic in ML_Syntax}
+  just encloses the term in parentheses. An example for the usage of this 
+  antiquotation is:
 
   @{ML_response_fake [display,gray]
   "@{term_pat \"Suc (?x::nat)\"}"
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
-  which is the internal representation of the term @{text "Suc ?x"}.
+  which shows the internal representation of the term @{text "Suc ?x"}.
 
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
-  for most antiquotations. 
+  for most antiquotations. Most of the basic operations on ML-syntax are implemented 
+  in @{ML_file "Pure/ML/ml_syntax.ML"}.
   \end{readmore}
+*}
+
+section {* Storing Data (TBD) *}
+
+text {*
+  Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we 
+  explain this mechanism. 
+*}
+
+ML{*signature UNIVERSAL_TYPE =
+sig
+  type t
+
+  val embed: unit -> ('a -> t) * (t -> 'a option)
+end*}
+
+ML{*structure U:> UNIVERSAL_TYPE =
+   struct
+      type t = exn
+
+      fun 'a embed () =
+         let
+            exception E of 'a
+            fun project (e: t): 'a option =
+               case e of
+                  E a => SOME a
+                | _ => NONE
+         in
+            (E, project)
+         end
+   end*}
 
-  Note one source of possible confusion about antiquotations. There are two kinds 
-  of them in Isabelle, which have very different purpose and infrastructures. The 
-  first kind, described in this section, are \emph{ML-antiquotations}. They are 
-  used to refer to entities (like terms, types etc) from Isabelle's logic layer 
-  inside ML-code. They are ``linked'' statically at compile-time, which  limits 
-  sometimes their usefulness in  cases where, for example, terms needs to be 
-  built up dynamically.  
+text {*
+  The idea is that type t is the universal type and that each call to embed
+  returns a new pair of functions (inject, project), where inject embeds a
+  value into the universal type and project extracts the value from the
+  universal type. A pair (inject, project) returned by embed works together in
+  that project u will return SOME v if and only if u was created by inject
+  v. If u was created by a different function inject', then project returns
+  NONE.
+
+  in library.ML
+*}
+
+ML_val{*structure Object = struct type T = exn end; *}
 
-  The other kind of antiquotations are \emph{document} antiquotations. 
-  They are used only in the text parts of Isabelle and their purpose is to print 
-  logical entities inside \LaTeX-documents. They are part of the user level and
-  therefore we are not interested in them in this Tutorial, except in 
-  Appendix \ref{rec:docantiquotations} where we show how to implement your 
-  own document antiquotations. 
-*}
+ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
+   struct
+      val (intIn: int -> U.t, intOut) = U.embed ()
+      val r: U.t ref = ref (intIn 13)
+      val s1 =
+         case intOut (!r) of
+            NONE => "NONE"
+          | SOME i => Int.toString i
+      val (realIn: real -> U.t, realOut) = U.embed ()
+      val _ = r := realIn 13.0
+      val s2 =
+         case intOut (!r) of
+            NONE => "NONE"
+          | SOME i => Int.toString i
+      val s3 =
+         case realOut (!r) of
+            NONE => "NONE"
+          | SOME x => Real.toString x
+      val _ = tracing (implode [s1, " ", s2, " ", s3, "\n"])
+   end*}
+
+ML_val{*structure t = Test(U) *} 
+
+ML_val{*structure Datatab = Table(type key = int val ord = int_ord);*}
+
+ML {* LocalTheory.restore *}
+ML {* LocalTheory.set_group *}
+
+
 
 (*
 section {* Do Not Try This At Home! *}




